Repository navigation
effectively detect and handle alpha conversions #3
Description
I don't attempt to do renaming at all when beta reducing, so naming collisions can sometimes happen. Not sure an exact test string to trigger this-- but it's something like replacing with something that has a free variable into somewhere where that variable is bound.
Activity
[-]effectively detect and handle alpha conversion[/-][+]effectively detect and handle alpha conversions[/+]evinism commentedon May 1, 2017
with the new parser this should be easier, because we can just create new subscripts.
evinism commentedon May 2, 2017
one possible recreation: at normal form of
(λa.λb.ab)b,bshould still be a free variable, and thebwithin the lambda expression should be renamed. Currently, it's not.For an easier test, I realize:
(λa.λb.a(a(b)))λa.λb.a(a(b))should be church numeral 4.evinism commentedon May 12, 2017
this is much more important now that variable assignment works in some fashion
evinism commentedon May 18, 2017
Kinda done with a placeholder ε₂ or whatever value. Doesn't look in the context to determine next available, just makes one it hasn't generated yet. Good enough for now.
evinism commentedon May 21, 2017
Hopefully in the future, we'll get context aware renaming of variables.
evinism commentedon Jan 13, 2019
This is finally finally done!!!