beginner question about Curry-Howard Correspondence

Stream: new members

[rzeta0]

I want to check I understand (well enough) the Curry-Howard Correspondence and how it enables systems like Lean+Mathlib to check proofs.

I drew the following diagram to help me think about it - it is based on blogs I have read and some YouTube videos I watched on the subject.

Screenshot 2025-01-23 at 01.03.47.png

I think the following is correct but tell me if I'm wrong:

• The Curry-Howard Correspondence says there is a correspondence between logical propositions and function types, and between proofs of those logical propositions and the function themselves.
• Example, logical conjunction corresponds to a product type
• Example, logical implication corresponds to function application
• A program that is of a given type, is a proof of the logical proposition corresponding to that function type.
• In addition, the mechanical process of simplifying proofs corresponds to the process of evaluating program functions
• For example, (A → B) ∧ A can be simplified to B, and in the code a function of type A→B can be evaluated if we have an "inhabited" A, to give us a B.
• All of the above is only true for programming languages that are (1) well-typed, and (2) purely functional - otherwise the can't depend on the functions/programs to behave in the way we expect logical propositions and operations do.

[Aaron Liu]

rzeta0 said:

• The Curry-Howard Correspondence says there is a correspondence between logical propositions and function types, and between proofs of those logical propositions and the function themselves.

Sort of? If you restrict the meaning of "logical proposition" or you extend the meaning of "function type".

The Curry-Howard correspondence came about because someone thought that some rules for typing and some rules for logical deduction were similar.

If you only look at function types and you only look at the logical formulas constructed by "implication", then there is a direct correspondence between "logical statements" and "function types" - just replace the implication symbol with the function arrow everywhere! Since both structures are syntactically a binary tree, it doesn't matter what you label the operation as.

What is more interesting is that there is also the correspondence between (intuitionistic) proofs of an implicational formula and inhabitants of a function type. Here's an example:

Theorem. For all propositions P and Q,
(P implies (P implies Q)) implies (P implies Q).
Proof.

Suppose P implies (P implies Q). Then

Suppose P. Then

Since both P and P implies (P implies Q), then P implies Q.
Since both P and P implies Q, then Q.

Since by assuming P we arrived at Q, then P implies Q.

Since by assuming P implies (P implies Q) we arrived at P implies Q, then
(P implies (P implies Q)) implies (P implies Q).

Claim. Forall types P and Q, the function type (P → P → Q) → P → Q is always inhabited.
Proof. We have the inhabitant

fun (two_p_get_q : P → P → Q) =>
  let p_get_q : P → Q := fun (p_object : P) =>
    let p_get_q : P → Q := two_p_get_q p_object
    let q_object : Q := p_get_q p_object
    q_object
  p_get_q

Do you see the similarities between these two? The Suppose in the proof has turned into fun in the type theory interpretation. Similarly, the modus ponens rule of inference has turned into function application.
It turns out we can extend this correspondence beyond just reasoning with implication being like function types. Logical conjunction (∧ statements) can be modeled as product types, disjunction (∨ statements) can be modeled as sum types, falsehood can be modeled as an Empty type, etc.

[Abraham Solomon]

rzeta0 said:

I want to check I understand (well enough) the Curry-Howard Correspondence and how it enables systems like Lean+Mathlib to check proofs.

I drew the following diagram to help me think about it - it is based on blogs I have read and some YouTube videos I watched on the subject.

Screenshot 2025-01-23 at 01.03.47.png

I think the following is correct but tell me if I'm wrong:

• The Curry-Howard Correspondence says there is a correspondence between logical propositions and function types, and between proofs of those logical propositions and the function themselves.
• Example, logical conjunction corresponds to a product type
• Example, logical implication corresponds to function application
• A program that is of a given type, is a proof of the logical proposition corresponding to that function type.
• In addition, the mechanical process of simplifying proofs corresponds to the process of evaluating program functions
• For example, (A → B) ∧ A can be simplified to B, and in the code a function of type A→B can be evaluated if we have an "inhabited" A, to give us a B.
• All of the above is only true for programming languages that are (1) well-typed, and (2) purely functional - otherwise the can't depend on the functions/programs to behave in the way we expect logical propositions and operations do.

For clarity sake, whilst that is generally of CHC -- in lean #eval is not always that, pretty sure it corresponds more to #reduce(in the diagram).

[rzeta0]

Thanks both, and Aaron I will print out your two_p_get_q example to read more deeply on the train today.