Show that term cons works by showing all beta reductions

Question

I'm new to functional programming.

So the terms cons appends an element to the front of the list. Where cons ≜ λx:λl:λc:λn: c x (l c n).

How should I go about proving that cons works correctly using beta reduction for a sample function. For example reducing cons 3[2,1] to [3,2,1]? Is there a formula like for the artihmetic operations in lambda? I'm a bit confused on how to approach this comapred to a arithmetic operation (i.e. addtion or multiplication).

Thanks.

Answer 1

$[3,2,1]$ is just syntactic sugar for $\mathsf{cons} \, 3 \, (\mathsf{cons} \, 2 \, (\mathsf{cons} \, 1 \, \mathsf{nil}))$. $[3,2,1]$ is $\mathsf{cons} \, 3 \, [2,1]$ by definition of the $[\ldots]$ notation.

Because $\mathsf{cons}$ is part of the definition of lists, it isn't meaningful to ask whether $\mathsf{cons}$ is correct on its own. The meaningful question is whether the definition of lists is correct as a whole. (More precisely, that's the definition of an encoding of lists in the lambda calculus.) Another way to look at it is that the goal isn't to prove that the definition of cons is correct, but that it's consistent with the rest of the definition of lists.

There are several, equivalent ways to define lists as an abstract type. Lists are an abstract type, defined by a number of functions and properties involving these functions. Lists are an abstract data type, so the functions can be classified into three groups: constructors (which build “bigger” lists from smaller lists and other stuff), destructors (which “break down” lists into smaller lists and other stuff) and other functions which can be built out of constructors and destructors. Any simple definition of lists uses two constructors: $\mathsf{nil}$ which is the empty list, and $\mathsf{cons}$ which takes two arguments, an element and a list, and returns a new list. The “most fundamental” (and easiest to reason with, but not easiest to understand) definition uses one destructor $\mathsf{case}$, and satisfies the following equations for any terms $f$, $g$, $h$, $t$ such that $t$ is a list: $$ \begin{align} \mathsf{case}\,\mathsf{nil}\,f\,g &= f \\ \mathsf{case}\,(\mathsf{cons}\,h\,t)\,f\,g &= g \, h \, t \\ \end{align} $$ An encoding of this abstract type in the lambda calculus is the definition of three lambda terms $\mathsf{nil}$, $\mathsf{cons}$ and $\mathsf{case}$. Proving the correctness of this encoding means proving that the equation above holds.

Another, equivalent, definition of lists uses three destructors $\mathsf{empty}$, $\mathsf{head}$ and $\mathsf{tail}$ with the following equations (which presuppose the existence of booleans) for any terms $h$, $t$ such that $t$ is a list: $$ \begin{align} \mathsf{empty}\,\mathsf{nil} &= \mathsf{true} \\ \mathsf{empty}\,(\mathsf{cons}\,h\,t) &= \mathsf{false} \\ \mathsf{head}\,(\mathsf{cons}\,h\,t) &= h \\ \mathsf{tail}\,(\mathsf{cons}\,h\,t) &= t \\ \end{align} $$ An encoding of this abstract type in the lambda calculus is the definition of five lambda terms $\mathsf{nil}$, $\mathsf{cons}$, $\mathsf{empty}$, $\mathsf{head}$ and $\mathsf{tail}$. Proving the correctness of this encoding means proving that the equation above holds.