patternMinor
Mathematical proofs implemented purely by Lambda Calculus
Viewed 0 times
calculusimplementedpurelylambdamathematicalproofs
Problem
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?
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?
Solution
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.
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.
Context
StackExchange Computer Science Q#85557, answer score: 6
Revisions (0)
No revisions yet.