search

evinism / lambda-explorer

Tutorial / REPL for the lambda calculus
https://lambdaexplorer.com/
MIT License
63 stars 9 forks source link

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

Open anton-trunov opened 7 years ago

anton-trunov commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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

evinism commented 7 years ago

implemented in https://github.com/evinism/lambda-explorer/pull/51, still waiting on getting the book so i actually know what i'm doing

anton-trunov commented 7 years ago

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