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$

2 Answers 2

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, 2020 at 16:46
0
$\begingroup$

This is not Curry-Howard, but a separate line of development that gets confused with it, that arises mostly from DeBruijn. Coq is an evolutionary descendant of AutoMath (A Description On ArXiv), which I put up a resurrected, revived version of here AutoMath on GitHub. In the file laying out the syntax (currently under "SyntaxNew.txt"), you'll see a description of the syntax and of the type-proposition correspondence. It, along with Martin-Löf are higher-order type theories that adopt an approach substantially different from that laid out by the Curry-Howard correspondence.

Its main feature is that types can be indexed, and the index type - itself - is included in the type system ... hence: "higher order". The product type $(∏x∈A)B(x)$ corresponds, roughly, to the bounded quantifier $(∀x∈A)B(x)$, but doubles over as an analogue of the conditional $A ⊃ B$, if $B$ is independent of $x$. So, it's conflating $(∀x∈A)B = A ⊃ B$, in that case, treating the index type $A$, itself, as a proposition.

AutoMath includes this feature. It also includes operators, and I don't know if Coq has this. Thus, an operator $O(x)$ may be defined as type $B$ for variables $x$ of type $A$. This corresponds to the assertion $A ⊢ B$, which should not be confused with the conditional $A ⊃ B$. (The relation between the two, in most formulations of logic, is that $⊢ A ⊃ B$ if and only if $A ⊢ B$, so that $⊃$ internalizes $⊢$.)

There's an "internal" λ-abstraction, that goes with the product type, so that if $b(x): B(x)$ for all $x: A$, then $(Λx∈A)b(x): (∏x∈A)B(x)$. That the epitome of a type-inference rule in Martin-Löf. In AutoMath (in the form I revised its resurrection to), the corresponding syntax is $[A x: b(x)]$. This should be contrasted with the "external" λ that goes with the assertions $⊢$ and that is encapsulated by the syntax for operator definitions. I believe Coq makes a similar distinction.

For AutoMath, the "application" type rule would then by that if $F: (∏x∈A)B(x)$ and $a: A$ then $F<a>: B(a)$. In contrast, for the operator $O$, described above, one would just have $O(a): B$, when $a: A$. So, there is a corresponding distinction between an "internal" function application - that goes with both the modus ponens rule for $⊃$ and instantiation rule for $∀$ - versus operator application, which goes with the assertion $⊢$.

For higher-order type theories you also have the "sum" types $(∑x∈A)B(x)$ which double over as the analogue of the bounded existential quantifier $(∃x∈A)B(x)$ and, when $B$ is independent of $x$, conjunction $A∧B$ ... thereby conflating $(∃x∈A)B = A ∧ B$ in that case. AutoMath has no support for sum types. The type-checking rule is that $(a,b(a)): (∃x∈A)B(x)$ provides a witness $b(a): B(a)$ to a solution $x = a$ to $B(x)$, for $a: A$, where $b(x): B(x)$, for $x: A$.

An approach closer to the spirit of Curry-Howard, for quantifiers, would drop the distinction between internal and external λ's and treat the quantifiers essentially as just infinitary analogues of the conjunction (for $∀$) and disjunction (for $∃$), similar to what Dana Scott does in The Algebraic Interpretation of Quantifiers: Intuitionistic and Classical [PDF], particularly as seen in the formulas of Theorem 7.2 in the linked reference $$ ⟦∃x·Φ(x)⟧_T = ⋁_{τ∈\text{Term}} ⟦Φ(τ)⟧_T,\quad ⟦∀x·Φ(x)⟧_T = ⋀_{τ∈\text{Term}} ⟦Φ(τ)⟧_T $$ (where $T$ is the name of whatever first-order theory is being formalized) which corresponds to the rules $$ (∃x)B_x ⊢ D ⇔ B_t ⊢ D,\text{ for all terms }t,\quad C ⊢ (∀x)A_x ⇔ C ⊢ A_t,\text{ for all terms }t $$ (where $C$ and $D$ are both independent of $x$) that generalize the rules for finite $n$-tuples (for $n = 0$ and $n = 2$): $$ ⊥ ⊢ D ⇔\text{ always },\quad C ⊢ ⊤ ⇔\text{ always },\\ A ∨ B ⊢ D ⇔ A ⊢ D\text{ and }B ⊢ D,\quad C ⊢ A ∧ B ⇔ C ⊢ A\text{ and }C ⊢ B, $$ to infinite-tuples. (Footnote: he goes beyond this theorem in following sections.)

An operator algebra suitable for this, with $∘$ given by: $$ f: A ⊃ B,\quad g: B ⊃ C,\quad ⇒ \quad g ∘ f: A ⊃ C $$ might look like the following: $$ f_x:C ⊃ A_x\text{ for all }x ⇒ ⟨x∷f_x⟩: C ⊃ ∀x·A_x,\\ π_t: ∀x·A_x ⊃ A_t\text{, for all terms }t,\\ π_t ∘ ⟨x∷f_x⟩ = f_t,\\ h: C ⊃ ∀x·A_x ⇒ h =⟨x∷π_x ∘ h⟩ $$ for $∀$ (where $C$ is independent of $x$), with corresponding rules for infinite-tuples: $$ a_x: A_x\text{ for all }x ⇒ (x∷a_x): ∀x·A_x,\\ c:C → ⟨x∷f_x⟩c = (x∷f_x c),\\ π_t (x∷a_x) = a_t,\\ p: ∀x·A_x ⇒ p =(x∷π_x p) $$ and a dual operator set for $∃$: $$ g_x: B_x ⊃ D\text{ for all }x ⇒ [g_x∷x]: ∀x·B_x ⊃ D,\\ σ_t: B_t ⊃ ∃x·B_x\text{, for all terms }t,\\ [g_x∷x] ∘ σ_t = g_t,\\ h: ∀x·B_x ⊃ D ⇒ h =[h ∘ σ_x∷x] $$ (where $D$ is independent of $x$). These would be examples of proofs within this algebra $$ [⟨x∷σ_x ∘ π_y⟩∷y]: ∃y·∀x·A_{xy} ⊃ ∀x·∃y·A_{xy},\\ λh·λp·(x∷(π_x h)(π_x p)): ∀x·(A_x ⊃ B_x) ⊃ ∀x·A_x ⊃ ∀x·B_x. $$

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .