There is an example of Church numeral, on the secion
Encoding Datatypes of
lambda calculus's wikipedia page.
One way of thinking about the Church numeral n, which is often useful when analysing programs, is as an instruction 'repeat n times'. For example, using the PAIR and NIL functions defined below, one can define a function that constructs a (linked) list of n elements all equal to x by repeating 'prepend another x element' n times, starting from an empty list. The lambda term is
λn.λx.n (PAIR x) NIL By varying what is being repeated, and varying what argument that function being repeated is applied to, a great many different effects can be achieved.
By varying what is being repeated, and varying what argument that function being repeated is applied to, a great many different effects can be achieved.
We can define a successor function, which takes a Church numeral n and returns n + 1 by adding another application of f, where '(mf)x' means the function 'f' is applied 'm' times on 'x':
SUCC := λn.λf.λx.f (n f x)
I don't understand what the
SUCC means right now. Since "the PAIR and NIL functions" are "defined below", let's skip them for now and consider
SUCC means here? Does it mean
succeed or something else?
I am trying to use Scheme language to define
(define succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
Am I right? If so, what can this
succ function do? If not, what is the right definition, and what can it do?
Can you give me some example to explain this? If I can understand
SUCC I think I can understand
PLUS which defined just below it.