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!
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.