Let user define fixed-point combinators

evinism / lambda-explorer

Tutorial / REPL for the lambda calculus

https://lambdaexplorer.com/

MIT License

62 stars 9 forks source link

Let user define fixed-point combinators #41

Closed anton-trunov closed 7 years ago

anton-trunov commented 7 years ago

We cannot define Y := λf. (λx. f (xx)) (λx. f (xx)) because the bodies of definitions get evaluated, which obviously causes a runtime error. Of course, there is a work around this issue: instead of writing Y rec_func one can substitute manually the RHS of Y into the formula.

anton-trunov commented 7 years ago

Oh, it's a duplicate of #24