# Lambda Calculus: Church encoding

## Pairs

True = T: λab. a False = F: λab. b

Pair : λx. λy. λf. f x y First : λp. p (λx. λy. x) Second: λp. p (λx. λy. y)

First (Pair α β) = First (Pair α β) = (λp. p (λx. λy. x)) ((λx. λy. λf. f x y) α β) = (λp. p (λx. λy. x)) (λf. f α β) = (λf. f α β) (λx. λy. x) = (λx. λy. x) α β = (λy. α) β = α

## List

4 different representations of lists:

* Build each list node from two pairs (to allow for empty lists)
* Build each list node from one pair
* Represent the list using the _right fold function_
* Repr list using Scott encoding that takes cases of match expression as args

### Two pairs as a list node

A nonempty list can implemented by a Church pair

* `First` contains the head
* `Second` contains the tail

However this does not give a representation of the empty list, because there is no "null" pointer. To represent null, the pair may be wrapped in another pair, giving free values:

* `First` is the null pointer (empty list)
* `Second.First` contains the head
* `Second.Second` contains the tail

Using this idea the basic list operations can be defined like this:

Nil = pair T T IsNil = first Cons = λh. λt. pair F (pair h t) Head = λz. First (Second z) Tail = λz. Second (Second z)

In a nil node second is never accessed, provided that head and tail are only applied to nonempty lists.

### One pair as a list node

Cons = Pair Head = First Tail = Second Nil = F IsNil = λl. l (λh. λt. λd. F) T

where the last definition is a special case of the general

process-list: λl. l (λh. λt. λd. head-tail-clause) nil-clause

### Represent the list using right fold

As an alternative to the encoding using Church pairs, a list can be encoded by identifying it with its right fold function. For example, a list of three elements x, y and z can be encoded by a higher-order function that when applied to a combinator c and a value n returns c x (c y (c z n)).

https://en.wikipedia.org/wiki/Church\_encoding#List\_encodings
