0
$\begingroup$

I am trying to understand how the type theory of the COQ theorem prover (calculus of constructions or CIC) works. Wikipedia states that it can be considered an extension of the Curry-Howard isomorphism.

For constructive propositional logic the Curry-Howard isomorphism states that types can be seen as propositions, and proofs as programs. For types/propositions $A,B$, propositions can be viewed as types in the following way (propositions on the left, types on the right, $\Leftrightarrow$ denoting correspondence)

$$A\rightarrow B \Leftrightarrow A\Rightarrow B$$ $$A\land B \Leftrightarrow A\times B$$ $$A\lor B\Leftrightarrow A+B$$

Then, for example, proving that

$$\forall A\forall B: A\rightarrow A\lor B,$$ where $A,B$ are interpreted as types can be seen as a proof that for any types $A,B$, the type $A\Rightarrow A+B$ exists. Proof of this fact can be converted into program and vice versa. In this case the program would simply return an $x\in A$, e.g. the left side of the pair, thereby showing the type exists.

Ok, so now to the question. CIC implements a predicate logic. How are the terms $\forall x: A.B$, $\lambda x: A.B$ interpreted in the correspondence? An example would be fine. Keep in mind I am very new to this $\lambda$ notation.

$\endgroup$
1
$\begingroup$

$\forall x: A.B$ is a type. It is interpreted as a terminating algorithm that takes in an $A$ and produces a $B$ as a result.

Under the Curry-Howard correspondence we interpret this as the logical statement that A implies B.


$\lambda x: A. M$ is a function. It takes an input $x$ of type $A$ and returns $M$ (which might reference $x$).

Under the Curry-Howard correspondence this is interpreted as a proof of $A$ implies $B$ (when $M$ has type $B$)..

$\endgroup$
1
  • $\begingroup$ Is there a chance you could give an example of some proposition regarding naturals for example? $\endgroup$ – Dole Sep 17 '20 at 16:46

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.