Church numerals: Difference between revisions

Line 1,786:

I feel we need an example from the original Lambda Calculus. I am here using a dialect that I invented that differs from real untyped Lambda Calculus in two ways:

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.

# 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`~~ 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.

# I have named expressions introduced by `let`. For example, ''let succ = λn.λf.λx.n f (f x)'' means that ''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.

Line 1,828:

Note that since integers in Lambda Calculus are usually defined in terms of Church Numerals, the functions to convert between the two are both the identity function.

=={{header|Lambdatalk}}==