Remix.run Logo
tromp 3 hours ago

Any lambda term is equivalent to a combinatory term over a one-point basis (like λxλyλz. x z (y (λ_.z)) [1]). One difference is that lambda calculus doesn't distinguish between functions and numbers, and in this case no additional constant (like 1) is needed.

[1] https://github.com/tromp/AIT/blob/master/ait/minbase.lam