Testing equivalence of Hakaru programs

[JacquesCarette]

As issue #75 mentions, an issue from long ago is resurfacing: how do we test that two Hakaru programs are 'trivially' equivalent. I think we'd like to be able to abstract over alpha-equivalence, commutativity-associativity of + and * and && and || . We might want to not worry about some amount of polynomial arithmetic. Although I must admit that I would like to not consider

x + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 +0

equivalent to

x

! [The point is that, in a test, we'd want to know if we're spitting out lots of + 0 that we were not expecting.]

Suggestion: we create a new (simple) data-type in Haskell which is first-order (we can use gensym to generate fresh names) that represents Hakaru programs, for the sole purpose of equivalence testing. This would be a 'throwaway' representation. Its only guarantee would be that it produces a 'normal form' with respect to a set of rules (such as alpha-equivalence, etc) that we deem to be 'trivial'.

[ccshan]

It seems @yuriy0 is working on this (9c7dc0eab156a342801909b521469ec06da899f4)? Thanks!

[JacquesCarette]

Yes, he has been. Not quite sure the exact status, but there definitely has been forward progress.

[yuriy0]

It seems @yuriy0 is working on this (9c7dc0e)? Thanks!

This was the first step; that change should handle associativity and commutativity for NAryOps. It is the slower and simpler of the two proposed implementations at last weeks meeting. This implementation is essentially what you called 'bipartite graph matching'. The other implementation probably requires changing all of alphaEq to return an Ordering.

This does not address the issue of x + negate(y) vs x - y; or of polynomial normals form, e.g.:

### Failure in: 5:RoundTrip:2:16:t46
x0 <~ normal(4, 5)
return (match (x0 < 3): 
         true: (x0 * x0)          --
         false: (x0 - 1))
but got:
x03 <~ normal(4, 5)
return (match (x03 < 3): 
         true: (x03 ^ 2)          --
         false: (x03 - 1))

but at least the latter is highly non-trivial.

[ccshan]

Are we done here?

[JacquesCarette]

alpha, associativity and commutativity are done. polynomial normal form is not. But it could be split off into a separate issue, as it is a problem for fewer tests.

[ccshan]

And I don't even know that we want polynomial normal form for testing equivalence...

[JacquesCarette]

We want to at least deal with - sanely. The rest is indeed up for discussion.

[ccshan]

Maybe the problem with - is that the Maple parser should parse a-b in Maple into negation in Hakaru?

[zaxtax]

There is no minus in the Hakaru AST. There is only addition with negation applied to the second argument.

On Tue, Jun 20, 2017 at 10:12 PM, Chung-chieh Shan <notifications@github.com

wrote:

Maybe the problem with - is that the Maple parser should parse a-b in Maple into negation in Hakaru?

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/hakaru-dev/hakaru/issues/79#issuecomment-309942683, or mute the thread https://github.com/notifications/unsubscribe-auth/AAAhUckZL3DtsTAD9CyTDYxqoDSIU5UIks5sGHwAgaJpZM4NxYID .

[yuriy0]

The changes to literals allow us to specify precisely the program which is produced by Maple (i.e. in terms of x + negate(y) vs x - y) so this is fixed, at least until we find two equivalent programs which differ by more than x + negate(y) vs x - y.