Lambda Calculus: Church vs Peano

n this task we will implement an alternative representation of natural numbers in lambda calculus, modeled after Peano number. Peano numbers are a simple way of representing the natural numbers using only a zero value and a successor function.

More precisely, Peano numbers are nested pairs. The number 0 is represented as a pair of FALSE and FALSE, and a number N + 1 is represented as a pair of TRUE and the number N. In other words, we can define the zero value PZERO and the successor function PSUCC as follows:

let PZERO = PAIR FALSE FALSE     -- Zero
let PSUCC = n -> PAIR TRUE n    -- Successor

Using PZERO and PSUCC we can easily define any Peano numeral, for example:

let PONE   = PSUCC PZERO   -- 1
let PTWO   = PSUCC PONE    -- 2
let PTHREE = PSUCC PTWO    -- 3

1.1. Reducing one

1.2. Is zero

1.2. Decrement

1.3. Church to Peano

1.3. Peano to Church