Is this Church encoding of lists correct?

Question

Types and Programming Languages by Pierce introduces Church encoding of lists in Exercise 5.2.8 on p63 and p500:

nil = λc. λn. n;
cons = λh. λt. λc. λn. c h (t c n);
head = λl. l (λh.λt.h) fls;
tail = λl.
        fst (l (λx. λp. pair (snd p) (cons x (snd p)))
            (pair nil nil));
isnil = λl. l (λh.λt.fls) tru;

Is fls in head correct? If I am corrrect, fls is Church encoding of Boolean value false.

Thanks.

Answer 1

Yes, $\mathsf {fls}$ is correct.

The reason is the following. If $l$ is a list of the form $\mathsf {cons}\, h\, t$, then we want $\mathsf {head}\, l$ to reduce to $h$. But if $l$ is the list $\mathsf {nil}$, then $\mathsf {head}\, l$ should be undefined. In untyped lambda-calculus, we can define $\mathsf {head}$ so that $\mathsf {head}\, \mathsf {nil}$ reduces to $\mathsf {fls}$, the Boolean value false.

You can check now that the definition is correct:

\begin{align*} \mathsf {head}\, (\mathsf {cons}\, h\, t) & = (\lambda l. l \, (\lambda h. \lambda t. h) \, \mathsf {fls}) (\mathsf {cons}\, h\, t) \\ & \to (\lambda l. l \, (\lambda h. \lambda t. h) \, \mathsf {fls}) (\lambda c. \lambda n. c\, h\, (t\, c\, n)) \\ & \to (\lambda c. \lambda n. c\, h\, (t\, c\, n)) (\lambda h. \lambda t. h) \, \mathsf {fls} \\ & \to (\lambda n. (\lambda h. \lambda t. h) h (t \, (\lambda h. \lambda t. h)\, n)) \, \mathsf {fls} \\ & \to (\lambda h. \lambda t. h) h (t \, (\lambda h. \lambda t. h) \, \mathsf {fls}) \\ & \to (\lambda t. h) (t \, (\lambda h. \lambda t. h) \, \mathsf {fls}) \\ & \to h \end{align*}

\begin{align*} \mathsf {head} \, \mathsf {nil} & = (\lambda l. l \, (\lambda h. \lambda t. h) \, \mathsf {fls}) \, \mathsf {nil} \\ & = (\lambda l. l \, (\lambda h. \lambda t. h) \, \mathsf {fls}) \, \mathsf (\lambda c. \lambda n. n) \\ & \to (\lambda c. \lambda n. n) (\lambda h. \lambda t. h) \, \mathsf {fls} \\ & \to (\lambda n. n) \, \mathsf {fls} \\ & \to \mathsf {fls} \end{align*}