CODEWITHSUNDEEP
lambdalambda-calculuschurch-encoding
bookmonkie
bookmonkie

Reputation: 449

Is the following a legit successor function for lambda calculus ? (Church Numeral)

I have read from the books that, the successor for Church Numerals is of the form: (\lambda n f x. f (n f x) )

Last night I came up with this: (\lambda a b c. (a b) (b c) )

I believe it also performs the functionality of a successor function. However I am not 100% positive my reductions are correct. Can someone examine it and tell me?

The following is my reduction: let a church numeral be (\lambda f x. f^n x), where f^n x is actually a short version of (f(f(f(f...(x))).. It represents the number n. The expected result should be n+1, that is (\lambda f x. f^{n+1} x)

(\lambda a b c. (a b) (b c) )(\lambda f x. f^n x)

= (\lambda b c. ( (\lambda f x. f^n x) b) (b c) ) // a replaced

= (\lambda b c. ( (\lambda x. b^n x) (b c) ) // f replaced

= (\lambda b c. ( (\lambda x. b^n x) (b c) ) // not 100% sure, can I replace x with (b c)?

= (\lambda b c. ( b^n (b c) )

= (\lambda b c. ( b^(n+1) c )

Is this reduction correct, especially from step 3 to 4? Thanks!

Upvotes: 2

Views: 1396

Answers (2)

Andrea Asperti
Andrea Asperti

Reputation: 1003

A way to understand the two definitions of the successor function is to start from the sum:

plus = \n,m,x,y. n x (m x y)

then we can define 

succ1 = \n. plus one n 
succ2 = \n. plus n one

where one = \x,y.x y

simplifying the two terms, we get

succ1 = \n,x,y. one x (n x y) 
      = \n,x,y. x (n x y)
succ2 = \n,x,y. n x (one x y) 
      = \n,x,y. n x (x y)

Upvotes: 0

Petr
Petr

Reputation: 63389

Yes, it is correct. There is no problem with substituting b c for x. See the substitution rule. Although b and c are bound, they're bound above both terms in question, so they have the same meaning at both places.

Upvotes: 1

Related Questions