> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/340-lambda-calculi/lambda-calculus-encodings/encodings/church-pair3.md). # 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)).