5
$\begingroup$

I've seen often stated that Lambda Calculus can be used for mathematical proofing but I haven't yet seen any example how it is actually used for the task.

Is there a simple example, lambda abstraction or application that can be shown to be a valid mathematical proof? For example what does it take to make a Church numeral successor function regarded as a mathematical proof?

$\endgroup$
  • $\begingroup$ Lambda calculus is mostly there for other things. For example, I used it, like, two weeks ago in my lecture, to show the difference between the evaluation orders that leads to laziness vs. strictness and call-by-name vs. call-by-value. $\endgroup$ – Oleg Lobachev Dec 15 '17 at 20:54
  • $\begingroup$ LC as a symbolic manipulation method is interesting to compare with mathematical equation manipulation method, thus as a candidate for a universal mathematical language. But seemingly as an untyped form, it is not so useful... That bites a bit of the halo of being simple and universal after all. $\endgroup$ – MarkokraM Dec 15 '17 at 21:11
6
$\begingroup$

So, the trick is that the untyped lambda calculus is not very useful as a mathematical proof, since it has non-halting terms.

Lambda Calculus as a proof system is most useful with types, particularly in terms of the Curry-Howard Isomorphism. Phillip Wadler has a great article outlining this.

The basic idea is that lambda abstraction corresponds to the way that you prove an implication. To write a function of type $A \to B$, you assume you have a value of type $A$, and use it to construct a return value of type $B$. This is exactly how you prove $A \implies B$: assume that $A$ holds, then use this to prove $B$.

Not every lambda term corresponds to a mathematical proof in the sense we're used to, although each term can be regarded as a proof that its type is inhabited. In particular, to prove anything really useful, you need dependent types, where types are allowed to be indexed by values.

For Church-Numerals, their typed version if $\forall a \ldotp a \to (a \to a) \to a$, which, when interpreted as a proposition, is really boring. It's saying that if something holds, and it implies itself, then that something still holds.

For more information on the various type systems for Lambda Calculi, I'd start with the Lambda Cube.

$\endgroup$
  • 1
    $\begingroup$ Again, very helpful. Explains exactly what I needed to know. $\endgroup$ – MarkokraM Dec 17 '17 at 7:52

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.