Hacker News new | ask | show | jobs
by hollerith 381 days ago
Yeah. It is coming back to me now: in lambda calc, there is no universe of values to which the universe of lambda expressions might be mapped. Instead, there is a process called lambda reduction that maps the set of all lambda expressions to the set of lambda expressions in normal form.

The expression λf.λx.f(f(fx)) for example is in normal form. The number 3 and the string "3" do not exist in the formalism, but at least some of the time, λf.λx.x is used to represent 0, λf.λx.fx to represent 1, λf.λx.f(fx) to represent 2, λf.λx.f(f(fx)) to represent 3, etc.

Again, lambda calc precedes the digital computer.