September 22, 1999 | Perl and the Lambda Calculus | Slide #28 |

We want

ADD =mn.(IF (IS_ZEROm)n(ADD (PREDm) (SUCCn)))

First, a brief digression

If

*f*is a function, and*f*(*x*) =*x*, we say*x*is a*fixed point*of*f*Example: 0 is a fixed point for the `square' function

Consider this function:

R =g.mn.(IF (IS_ZEROm)n(g(PREDm) (SUCCn)))

`R`transforms some function*g*in a rather bizarre wayBut notice that if

`ADD`is the addition function we desire, then

(RADD) ==ADD

So the elusive addition function is a

*fixed point*of`R`

Next | Copyright © 1999 M-J. Dominus |