The tool does not recognize `λn. n` as eta-equivalent to the Church 1 (`λfn. f n`).

[anton-trunov]

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.

[evinism]

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?"

[anton-trunov]

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.

[evinism]

Solid, I'll implement that then(or you can if you want)!
some links for reference would be good, too, if you're willing.

[anton-trunov]

Off the top of my head: Wikipedia and "Types and Programming Languages" by B. Pierce assume eta-equivalence.

[evinism]

implemented in #51, still waiting on getting the book so i actually know what i'm doing

[anton-trunov]

Cool! Will try the tool again in some time! Thanks!

[evinism]

Hahaha a whole career later and I'm finally taking a look back at this project. My copy of TAPL actually makes no mention of eta equivalence, nor is it clear that it exists in Wikipedia, and so I'm less convinced it's necessary as an addition to the project. I believe the issue you found SHOULD actually be fixed, but via an existing and long-standing executor bug (!!!) solved in #136

Regardless, with a healthy dose of claude, i've added a toggle for doing beta-eta reduction.

[anton-trunov]

Wow, this is just amazing, what modern GenAI can do to us :) Reigniting old passions and all that