Proofs are programs, and programs are proofs. That’s basically what the Curry-Howard correspondance says.
Proofs can be transformed in programs, and programs can be transformed into proofs. If you have a proof, you can get a program out of it for free. If you have the right kind of program, it also serves as a proof. As a category theorist might say, proofs are isomorphic to programs.
Proofs ≅ \cong ≅ Programs
Direct Proofs and Functions
While learning about direct proofs in math, it helped me to think of a direct proof as a simple function that I was trying to write. For example, let’s say we need to prove the following:
if a a a and b b b are odd numbers, then a + b a + b a+b is even
Using the method of direct proof, we need to show how adding any two odd numbers together results in an even number.
We can think of this proof like a little function we are trying to write:
function addOdds ( a : OddNumber , b : OddNumber ) : EvenNumber { }
Using algebra, we could “fill in” this “function” like so:
We know that by the definition of an odd number, any odd number can represented by 2 n + 1 2n + 1 2n+1 where n n n is any integer. So let’s take two odd numbers and add them together.
( 2 x + 1 ) + ( 2 y + 1 ) (2x + 1) + (2y + 1) ( 2 x + 1 ) + ( 2 y + 1 )
Using some algebraic steps we can manipulate these numbers to show that this results in an even number. By definition, an even number can be shown as 2 n 2n 2n where n n n is any integer. So let’s try to rearrange what we’ve got to give us something in the form of 2 n 2n 2n, which we know is an even number.
( 2 x + 1 ) + ( 2 y + 1 ) = 2 x + 2 y + 2 = 2 ( x + y + 1 ) (2x + 1) + (2y + 1) \\= 2x + 2y + 2 \\= 2(x + y + 1) ( 2 x + 1 ) + ( 2 y + 1 ) = 2 x + 2 y + 2 = 2 ( x + y + 1 )
Now we know that x x x, y y y and 1 1 1 are integers, and we know that the sum of any integers is an integer. So we could call the sum of these integers n n n, an integer. x + y + 1 = n x + y + 1 = n x+y+1=n
Therefore we have our even number! Let’s look at the whole process.
a + b = ( 2 x + 1 ) + ( 2 y + 1 ) = 2 x + 2 y + 2 = 2 ( x + y + 1 ) = 2 n a + b \\= (2x + 1) + (2y + 1) \\= 2x + 2y + 2 \\= 2(x + y + 1) \\= 2n a + b = ( 2 x + 1 ) + ( 2 y + 1 ) = 2 x + 2 y + 2 = 2 ( x + y + 1 ) = 2 n
Just as if we were writing a function, we took an input (in this case two odd numbers) and we “proved” that we could add these together and output an even number. The whole process felt a lot like trying to write a function that took an input and trying to manipulate the value(s) to match the return type of the function.
In fact, here’s what the process could look like if we did it all in TypeScript.
type Integer = number ; type OddNumber = { coefficient : 2 , term : Integer , constant : 1 , } type EvenNumber = { coefficient : 2 , term : Integer , constant : 0 , } function addOdds ( a : OddNumber , b : OddNumber ) : EvenNumber { const n = ( a . term + b . term + 1 ) as Integer ; return { coefficient : 2 , term : n , constant : 0 , } ; }
Try it on the TS Playground
Here we did the exact same thing as we did in the proof, just translated to TypeScript. And just like that, we have a working program that will add up any two odd numbers and give us an even number.
Inductive Proofs and Recursive Functions
There’s a more striking relationship between proofs and programs when we start looking at math proofs using induction. These work exactly like recursive functions, as pointed out in HTDP.
In particular let’s think about inductive proofs where we have something like, “For all integers n ≥ a n \geq a n≥a, a property P ( n ) P(n) P(n) is true.”
The underlying logic is the same as writing a basic recursive function for an input that is above some value.
Induction Proof Recursive Function Prove P ( a ) P(a) P ( a ) Define the base case for a value a a a Assume P ( k ) P(k) P ( k ) is true if k k k is any value ≥ a \geq a ≥ a . This is called the “inductive hypothesis.” Use the function f(k) recursively, assuming it works with any value k k k which is ≥ a \geq a ≥ a . This is called the recursive “leap of faith.” Show that if P ( k ) P(k) P ( k ) is true, then P ( k + 1 ) P(k+1) P ( k + 1 ) is also true Given any input greater than a a a , the base case, write the code to show how you can combine the value of f(k) with something else to produce a proper result for f(k+1)
For example, let’s look at a very simple recursive function for computing the length of an array:
function arrayLength < T > ( arr : T [ ] ) : number { if ( arr . length === 0 ) { return 0 ; } const k = arr . slice ( 1 ) ; return arrayLength ( k ) + 1 ; }
No matter how big of an array we put into this function, it will always return the correct length. (Assuming we don’t exceed maximum recursion depth and blow out the stack. ????)
Turning a proof into a program
Now let’s look at something more interesting. Earlier we said that proofs are programs. Let’s take an interesting proof using induction and see how it translates directly into a recursive program!
In Sussana S. Epp’s Discrete Mathematics with Applications she gives the example of a simple but interesting proof using induction. She explained how some people argue that without a pennies (1¢ coins), there would be lots of values that you wouldn’t be able to pay for. But actually, if you had only 3¢ and 5¢ coins, you could pay for any value greater than 7¢. Or, to state it a bit more formally:
“For any value n equal to or above 8¢, n cents can be obtained using 3¢ and 5¢ coins.”
To prove this, we can use the method of proof by induction.
Show that it’s true with the base value: 8¢ Assume that this will work for any value ≥ \geq ≥ 8¢ Show how it will work for any value ≥ \geq ≥ 8¢ + + + 1¢
First, we need to prove that this is true for the base value: 8¢.
Done. 3 ¢ + 5 ¢ = 8 ¢ 3¢ + 5¢ = 8¢ 3¢+5¢=8¢
Second, we will blindly assume that we can make change using 3¢ and 5¢ for any value equal to or greater than 8¢. This is the inductive hypothesis.
Third, using this assumption, we need to show how we can always make change for something 1¢ more.
Given any pile of 3¢ and 5¢ coins valued at least 8¢, we need to show how we can make a value 1¢ more. Well, if we have a pile like that there are two options:
If there’s a 5¢ coin in the pile we can replace it with two 3¢ coins. This gives us 1¢ more. If there’s no 5¢ coin in the pile, than there must be at least three 3¢ coins, because we know that the value has to be at least 8¢. We can replace those three 3¢ coins with two 5¢ coins. This gives us 1¢ more.
And there, using the magic of mathematical induction, we’ve proven that we can make change for any value of at least 8¢ using only 3¢ and 5¢ coins!
But that’s not all, because we have the proof, we automatically have a program that will make this change for us!
All we need to do is translate the exact same logic into a language that a computer can run. Let’s use TypeScript.
type Coin = 3 | 5 ; function makeChange ( amount : number ) : Coin [ ] { if ( amount < 8 ) { throw new Error ( "Amount must be at least 8¢" ) ; } }
Following the inductive logic above, the first thing we need to do is define the base case for our recursive function. This is the same thing as proving the statement with the base value.
type Coin = 3 | 5 ; function makeChange ( amount : number ) : Coin [ ] { if ( amount < 8 ) { throw new Error ( "Amount must be at least 8¢" ) ; } if ( amount === 8 ) { return [ 5 , 3 ] ; } }
From this point on we will just assume that our function will work for any values of at least 8 that we give it. Here we see that the “inductive hypothesis” and the “recursive leap of faith” are the same thing.
Now all we need to do is show that given any pile of change at least 8¢ big, we can make one 1¢ bigger. We’ll use the exact same logic as the proof above.
type Coin = 3 | 5 ; function makeChange ( cents : number ) : Coin [ ] { if ( cents < 8 ) { throw new Error ( "ERROR: Amount must be at least 8¢" ) ; } if ( cents === 8 ) { return [ 5 , 3 ] ; } const pile = makeChange ( cents - 1 ) ; if ( pile . includes ( 5 ) ) { return replaceCoins ( pile , 5 , 1 , [ 3 , 3 ] ) ; } return replaceCoins ( pile , 3 , 3 , [ 5 , 5 ] ) ; }
All we have left to do is write that one little helper function replaceCoins that takes the pile and replaces our coins for us.
function replaceCoins ( coins : Coin [ ] , coin : Coin , n : number , replacement : Coin [ ] , ) : Coin [ ] { const pile = [ ... coins ] ; for ( let i = 0 ; i < n ; i ++ ) { const d = pile . findIndex ( x => x === coin ) ; pile . splice ( d , 1 ) ; } return [ ... pile , ... replacement ] ; }
And voila! Thanks to the Curry-Howard correspondence, we’ve just translated our proof into a working program! Not only do we know this is possible, we can see exactly how the change is made for any given value.