apply-reduction-relation* insensitive to alpha-equivalence

[howell]

I'm working on a model that makes use of Redex's binding forms support (which has been great). However, I ran into something unexpected today: apply-reduction-relation* returned a list of 16 terms, all of which were alpha-equivalent? to one another.

This was even more surprising given that I had looked at the traces output for reducing the term in question which had merged alpha-equivalent terms.

Using this previous commit as a template, I was able to get apply-reduction-relation* behaving the way I expected for my language by using the equivalence and hash constructs from binding-forms.rkt (see here).

(It has occurred to me that maybe this is the desired behavior for apply-reduction-relation*, though I'm not sure why that would be; I would be interested to hear)

[howell]

any thoughts on this?

I don't think I made this clear in my initial report, but I patched my local version of Redex to consider alpha-equivalence in apply-reduction-relation* (see here) which I'd be happy to submit as a PR if that is indeed the desired behavior.

[paulstansifer]

I believe that the current behavior of `apply-reduction-relation*` is just the result of an oversight on my part; alpha-equivalence was supposed to be the notion of equality everywhere possible.

[rfindler]

Was there an alpha equal hash defined elsewhere in redex already? (I have a vague memory of one but I am not sure.)

[paulstansifer]

I had to check, too. It already existed, and is based on `canonicalize`.

…

On Tue, May 23, 2017 at 4:20 PM, Robby Findler ***@***.***> wrote: Was there an alpha equal hash defined elsewhere in redex already? (I have a vague memory of one but I am not sure.) — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#96 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAAFl-LA7s3WwspEJf8bXyfyQFfGboF8ks5r8z99gaJpZM4NV6Hs> .

[howell]

There is make-α-hash in binding-forms.rkt which I missed on my first go around. I can update my patch to use make-α-hash (as well as the code that I copied went off of implementing the same functionality for traces).

I have one bit of uncertainty with making this change, though. The loop inside traverse-reduction-graph uses a path variable for an immutable hash that needs to use alpha-equivalence. I can either convert it to a mutable hash using make-α-hash, or add a make-immutable-α-hash function and use that instead.

I'm uncertain about which way to go because there is a comment suggesting this path variable has been the subject of performance tuning and I want to be careful where I tread in that regard!

[rfindler]

I think we need a make-immutable-α-hash function. Thanks for helping out with this!

[wilbowma]

Are this and #102 closed by 24f0c5c?

[rfindler]

Oh, rats! I totally forgot about this and just changed only one part of the problem! I'm sorry about that.

So, no, they aren't closed, because I changed only the one for that specific bug.

Looking at the diff, I think that the fixes to traces and stepper are still needed. But test cases are also needed.

Shall I do that?

And where do we stand with the performance issues? I am guessing that there is not much to be helped there. We knew that alpha stuff would slow various things down, but I can try to investigate if there is a specific file that's problematically slower.

[wilbowma]

For apply-reduction-relation*, it actually improves performance in my experience. So I don't see any reason to not merge #102, other than the minor issue of using the depricated interface.

#103 is my attempt to make similar changes to judgment forms and metafunctions, but it really hurts performance.

[rfindler]

@howell do you have the example (or one like it) that returned too many things so I can add it to the test suites?

[howell]

I wasn't able to reproduce the errors I was getting in the model I was working on at the time. I had to remove some binding directives to be able to run the model, which may be related.

The directive

(facet X A ([D S #:refers-to (shadow D X)] ...))

now produces an error message

define-language: found the same binder, X, at different depths, 1 and 0

Redex used to accept this directive, and as far as I could tell interpreted it the way I intended.

[wilbowma]

Think this should have been closed by #102

[rfindler]

Thanks!