2
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ How the proof will look like depends on what do you mean by the correctness of cons. Correctness of a function is defined relative to some function specification. There is no “absolute correctness”. Since people do not prove such trivial things, I can't guess what specification you have in mind. $\endgroup$ – beroal Jan 28 at 18:22
2
$\begingroup$

$[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.

$\endgroup$
2
  • $\begingroup$ The OP already gave a definition of cons, so your musings about different ways of defining lists are irrelevant. $\endgroup$ – beroal Jan 28 at 18:18
  • $\begingroup$ @beroal If you think that, you've completely missed the point of the answer. The point is to figure out the rest of the definition of lists. Because otherwise, you don't have any concept of what might make the definition of cons "correct". Correctness is consistency with the other parts of the definition. $\endgroup$ – Gilles 'SO- stop being evil' Jan 28 at 18:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.