evinism / lambda-explorer

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

Somehow deal with the fact that meaningful variables don't necessarily have normal forms. #24

Closed evinism closed 7 years ago

evinism commented 7 years ago

Take into consideration the "divide" operator: (λn.((λf.(λx.x x) (λx.f (x x))) (λc.λn.λm.λf.λx.(λd.(λn.n (λx.(λa.λb.b)) (λa.λb.a)) d ((λf.λx.x) f x) (f (c d m f x))) ((λm.λn.n(λn.λf.λx.n(λg.λh.h(gf))(λu.x)(λu.u))m)nm))) ((λn.λf.λx.f(nfx))n))

You can't currently assign that to a variable (because I think it doesn't have a normal form), but it looks like it works if you do the application inline.

Maybe we don't compute normal forms of definitions?

anton-trunov commented 7 years ago

Maybe we don't compute normal forms of definitions?

Sure, that's the way to go. Definitions are entities of the metalanguage, so reductions should not be performed in the bodies of definitions.

evinism commented 7 years ago

Fixed in https://github.com/evinism/lambda-explorer/pull/45