Church numerals: Difference between revisions

1.# Variables can be longer than single letters. In canonical lambda calculus `''xy`'' would be considered an application of `''x`'' to `''y`''. In my dialect, it is the free variable `''xy`''. This change is made purely to allow readable variable names.

2.# I have named expressions introduced by `let`. For example, `''let succ = λn.λf.λx.n f (f x)`'' means that `such`''succ'' stands for the function on the right hand side. Conceptually, it is just syntactical sugar for `''λsucc.( .... everything else that follows ...) (λn.λf.λx.n f (f x))''. In particular, it does not introduce conventional recursion into the language.