lambda-explorer
lambda-explorer copied to clipboard
evinism
The tool does not recognize `λn. n` as eta-equivalent to the Church 1 (`λfn. f n`).
This might prevent it from recognizing E := λmn. n m as a solution to the exponentiation problem. (I can't check it right now). But it certainly does not help when testing.
Thank you so much for contributing! I guess I'd love to know a little more about the theory here-- do we generally consider eta equivalence rather than just alpha equivalence when asking "is this church numeral 1?"
Most sources seem to do so. E.g. when converting from a Church numeral to, say, integer one usually passes a (+1) function as the first argument and 0 as the second -- λfz. f z gets converted to 1, so does λx. x.
Solid, I'll implement that then(or you can if you want)! some links for reference would be good, too, if you're willing.
Off the top of my head: Wikipedia and "Types and Programming Languages" by B. Pierce assume eta-equivalence.
implemented in https://github.com/evinism/lambda-explorer/pull/51, still waiting on getting the book so i actually know what i'm doing