Calculus of Constructions

As an additional extension to the hierarchy of logical systems we’ve discussed, we’ll consider type theory. In type theory, every “term” has a “type” and operations are restricted to terms of a certain type.

Type theory was created to avoid paradoxes in a variety of formal logics and rewrite systems. For example, Russell’s paradox is not applicable since every sentence has its own type.

The most powerful concept in Coq is not about Coq; it’s the calculus of constructions. Coq is just a lot of awesome automation machinery on top of that.

Calculus of Constructions is a type theory based on intuitionistic logic and simply typed lambda calculus. Together with Dependent Types, Inductive Types, Recursion, they provide a neat way to do proofs.

To demonstrate why they are powerful, let’s consider one of the inference rules as an example:
{\displaystyle {\Gamma ,x:A\vdash B:K\qquad \qquad \Gamma ,x:A\vdash N:B \over {\Gamma \vdash (\lambda x:A.N):(\forall x:A.B):K}}}

What this means is that if above the line holds, then so does everything below the line.

In this case, K is either a Prop or a Type. For simplicity, assume K is Type. To translate it, it means that:
1. If we have a judgment x of type A, from which it follows that B : K (B is a Type)
2. If we have a judgment x of type A, from which it follows that N : B (N has type of B)
then we can deduce that
(\x : A . N) has type (\forall (x : A) . B), and the term (\forall (x : A) . B) has type Type.

In other words, this is the rule that ties together lambda abstraction and universal quantification. It also says that a universal quantification is a type.

This rule is the reason why this flows nicely:

(* Make sure you have enabled "Display all basic low-level contents" *)
Definition test (s : Set) : bool := true.

Check test.                 (* test : forall _ : Set, bool *)

Check forall _ : Set, bool. (* forall _ : Set, bool : Type *)

Other data types are encoded similarly as with Church Numerals.

The interesting thing about this system is that it has the strong normalization property, which means that every sequence of rewrites eventually terminates.

While this is not useful for IO, it is very useful for proofs.

In any case, we can take advantage of IO by extracting code to other languages as seen in Coq to Haskell.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s