#kse

Curry–Howard Correspondence

The Curry–Howard correspondence (also known as the Curry–Howard isomorphism) is a profound insight that draws a bridge between logic and computation. It establishes a direct correspondence between:

Propositions in logic ↔ Types in programming
Proofs of propositions ↔ Programs (or lambda terms)

In essence:

“A proof is a program, and a proposition is a type.”

The Core Idea

Curry–Howard reveals a beautiful symmetry:

Programming (Lambda Calculus)	Logic (Intuitionistic)
Types in λ→	Formulas in Intuitionistic Logic
Terms (λ-terms / programs)	Proofs of those formulas

The correspondence says:

Every type in lambda calculus is a logical proposition,
and every well-typed term is a proof of that proposition.

Examples

⊢ λ x . x : α \to α

This is the identity function in lambda calculus, and it corresponds to the logical tautology:

“If $α$ is true, then $α$ is true.”
In logic: $α \to α$

✅ This expression is always valid—a tautology.
📌 In programming: the identity function is always safe to use.
📌 In logic: this is always provable.

🧠 Every combinator (no free variables, empty context) in lambda calculus is a tautology in logic.

Why?

Because combinators like I, K, and S are closed, well-typed lambda terms.
By Curry–Howard, this means they prove valid logical formulas.

I combinator (λx.x)

Type: $α \to α$
Logic: $α \to α$ (tautology)

K combinator (λx.λy.x)

Type: $α \to (β \to α)$
Logic: If $α$ is true, then $β \to α$ . Always true.

S combinator (λf.λg.λx. f x (g x))

Type: $(β \to γ) \to ((α \to β) \to (α \to γ))$
Logic: If $β \to γ$ is true, and $α \to β$ is true, then $α \to γ$ is true.
This is a more complex tautology, expressing function application associativity.

Intuitionistic Logic Calculus and Proof Rules

Let’s explore how logic operates from a syntactic viewpoint, using sequent calculus—a way to formally derive logical statements. The whiteboard and the transcript you're working from outline the basic rules of implication in intuitionistic (constructive) logic, focusing on how implications are introduced, applied, and reasoned with.

Suppose you have a collection of assumptions (sequentions) like:

α_{1}, α_{2}, \dots, α_{n}

These are your axioms, or known truths (called a context, often denoted as $Γ$ ). You then derive some new conclusion, say:

Γ ⊢ β

This means:

“From assumptions $Γ$ , I can prove $β$ .”

But here's a catch!

If your assumptions are contradictory (e.g., $α$ and $\neg α$ ), you can “prove” anything—even nonsense. That’s a broken theory.

💥 So it’s your responsibility to make sure your list of assumptions is sound and consistent.

Some Rules of Implication-Only Logic

We’re working with a fragment of logic that deals only with implications ( $\to$ ). This system is called implicational logic, a part of intuitionistic logic (aka constructive logic).

Let’s build our logic system using three core rules:

Rule 1: Axiom (Identity Rule)

If something is assumed, you can use it.

Γ, α ⊢ α

This simply says:

“If $α$ is in your context, then $α$ is provable.”

✅ This is your starting point in any logical derivation.

Rule 2: Modus Ponens (Application Rule)

If you know that $α \to β$ is true, and $α$ is true,
then you can conclude $β$ .

\frac{Γ ⊢ α \to β Γ ⊢ α}{Γ ⊢ β}

This is the famous rule of Modus Ponens (MP):

“If you say, ‘if it rains, the street will be wet’ and also know that ‘it rains’ — then you can conclude: ‘the street is wet.’”

💡 It's not just how you prove something, but also what you assume in the process.

Rule 3: Implication Introduction

If assuming $α$ leads you to prove $β$ , then you can conclude the implication $α \to β$ itself.

\frac{Γ, α ⊢ β}{Γ ⊢ α \to β}

This rule is all about building functions (in lambda calculus) or constructing implications (in logic):

“If assuming $α$ allows me to get to $β$ , then I’ll just write down the implication $α \to β$ .”

This is how we define implications logically.

Transition to Logic

Let’s now talk about one of the most beautiful insights of the Curry–Howard correspondence — how we move from a lambda term to its logical meaning.

Take the following lambda term:

⊢ λ x . λ y . x

It has the type:

α \to (β \to α)

Now here’s the cool part:

🧠 To get the logical formula, you just strip away the lambdas and keep the type!

So:

Lambda term:

λ x . λ y . x

Type:

α \to (β \to α)

The type alone becomes your logical proposition:

α \to (β \to α)

✅ This is a tautology in logic — it’s always true.

So the transformation from lambda calculus to logic looks like this:

Lambda Term	Logical Proposition
$λ x . x$	$α \to α$
$λ x . λ y . x$	$α \to (β \to α)$
$λ f . λ g . λ x . f (g x)$	$(β \to γ) \to ((α \to β) \to (α \to γ))$

Just remove the lambdas, and what remains is the logical skeleton — the type tells you the structure of the reasoning.

The Challenge

Look at this proposition:

α \to (α \to α)

It’s clearly a tautology in logic. But now try to construct a lambda term for it. You might write:

λ x . λ y . x

This makes sense: we take two arguments of type $α$ , and return the first.
So we have:

λ x . λ y . x : α \to (α \to α)

✅ Looks good.

But here's the problem:
That’s Not the Only Possibility!

You could also write:

λ x . λ y . y

Which gives:

α \to (α \to α)

Again! And this is also a valid lambda term, a valid function, but with a different behavior!

And this one:

λ x . λ y . x (or) λ x . λ y . y or anything else that returns a value of type α

So multiple different lambda terms can have the same type.

What’s the Issue?

When going from lambda → logic, it's straightforward:
You always get one formula — the type.

But when going from logic → lambda, it's not uniquely determined.

There could be many different terms with the same type.
Logic tells you what is provable, but it doesn't tell you how.

Logic = Specification, Lambda = Implementation

You can think of it this way:

The formula $α \to (α \to α)$ is like a spec:
"Given an $α$ , produce a function from $α$ to $α$ ."
But how you implement that function? That’s your choice.
Do you return the first argument? The second? Apply one to another?

That’s why this direction (Logic → Lambda) is trickier.
You're constructing a program from a proof, and there may be many valid implementations.

Absolutely — let's shift the lens to something more mathematical and familiar: theorems and proofs.

💡 Logic as Theorems, Lambda as Proofs

Imagine you're in a math class.

You see a statement on the board:

“If a number is even, then doubling it is also even.”

This statement is a logical formula. It’s a theorem — something that might be provable.

But how do we prove it? Well, you could:

Provide an algebraic argument,
Use induction,
Or even just give a few examples if your professor is being generous.

Each of these is a proof — a specific way of showing the theorem is true.

🧠 In Curry–Howard:

Theorem (logical formula) = Type
Proof (evidence or argument) = Lambda term (program)

So What’s the Problem Again?

When going from:

Proof → Theorem:
It's like reading a completed proof and saying,
"Ah yes, this proves the statement 'if x is even, 2x is even.'"
✅ Clear, one direction, always works.
Theorem → Proof:
It's like being told:
"Here’s the statement. Now you go and prove it."
😬 That’s much harder — and you might find many different proofs!

🔁 Multiple Proofs, One Theorem

For example:

Theorem:
$α \to (α \to α)$

There are multiple “proofs” (lambda terms) of it:

$λ x . λ y . x$
$λ x . λ y . y$
$λ x . λ y . (x)$
...and so on.

All valid — all prove the same theorem — but they differ in how they do it.

So:

From a proof, you can always find the theorem it proves.
From a theorem, you must construct a proof — and there may be many ways.

🧪 So What Can We Do With That?

Here's where things get even more interesting:
Since there can be many lambda terms for a single formula, it means:

We might find multiple ways to prove the same thing,
Some proofs might be long and complex,
Others might be shorter, more elegant.

Now imagine you’re working with a complex classical theorem — like something from number theory or analysis. You could:

Translate that theorem into a type (using Curry–Howard).
Try to construct lambda terms (proofs) for it.
Maybe even brute-force all possible lambda terms of that type.
And who knows? You might discover a simpler proof you hadn’t thought of before.

🧠 Proofs become searchable.
💡 Lambda calculus lets us enumerate and explore proofs as data.
🤖 This opens the door to automated proof discovery — not just verifying, but inventing.

🔄 Beta Reduction Preserves Meaning

And here's an important technical detail:
If you find a lambda term $U$ that has type $α$ , and you simplify it using β-reduction, the simplified version $U^{'}$ still has the same type:

U \to_{β} U^{'} \Rightarrow U : α \Rightarrow U^{'} : α

This is a theorem in lambda calculus:

β-reduction preserves types.

So, you can simplify your lambda term without fear — it remains a proof of the same theorem.
That means:

We can look for more compact or more efficient terms,
And still be confident that they prove the same thing.

💡 Final Intuition

Think of it this way:

A theorem is like saying “there exists a path to the mountaintop.”
A lambda term is the trail you choose to hike.
There might be a steep, winding road…

But maybe, just maybe, there’s a shortcut through the forest 🏞️

Curry–Howard says:

"Let’s map the terrain, explore every route, and maybe discover a simpler way to the truth."