λ-cube
https://cstheory.stackexchange.com/questions/36054/how-do-you-get-the-calculus-of-constructions-from-the-other-points-in-the-lambda
First, to reiterate one of cody's points, the Calculus of Inductive Constructions (which Coq's kernel is based on) is very different from the Calculus of Constructions. It is best thought of as starting at Martin-Löf type theory with universes, and then adding a sort Prop at the bottom of the type hierarchy. This is a very different beast than the original CoC, which is best thought of as a dependent version of F-omega. (For instance, CiC has set-theoretic models and the CoC doesn't.)
That said, the lambda-cube (of which the CoC is a member) is typically presented as a pure type system for reasons of economy in the number of typing rules. By treating sorts, types, and terms as elements of the same syntactic category, you can write down many fewer rules and your proofs get quite a bit less redundant as well.
However, for understanding, it can be helpful to separate out the different categories explicitly. We can introduce three syntactic categories, kinds (ranged over by the metavariable k), types (ranged over by the metavariable A), and terms (ranged over by the metavariable e). Then all eight systems can be understood as variations on what is permitted at each of the three levels.
λ→ (Simply-typed lambda calculus)
k ::= ∗
A ::= p | A → B
e ::= x | λx:A.e | e e
This is the basic typed lambda calculus. There is a single kind ∗, which is the kind of types. The types themselves are atomic types p and function types A → B. Terms are variables, abstractions or applications.
λω_ (STLC + higher-kinded type operators)
k ::= ∗ | k → k
A ::= a | p | A → B | λa:k.A | A B
e ::= x | λx:A.e | e e
The STLC only permits abstraction at the level of terms. If we add it at the level of types, then we add a new kind k → k which is the type of type-level functions, and abstraction λa:k.A and application A B at the type level as well. So now we don't have polymorphism, but we do have type operators.
If memory serves, this system does not have any more computational power than the STLC; it just gives you the ability to abbreviate types.
λ2 (System F)
k ::= ∗
A ::= a | p | A → B | ∀a:k. A
e ::= x | λx:A.e | e e | Λa:k. e | e A
Instead of adding type operators, we could have added polymorphism. At the type level, we add ∀a:k. A which is a polymorphic type former, and at the term level, we add abstraction over types Λa:k. e and type application e A.
This system is much more powerful than the STLC -- it is as strong as second-order arithmetic.
λω (System F-omega)
k ::= ∗ | k → k
A ::= a | p | A → B | ∀a:k. A | λa:k.A | A B
e ::= x | λx:A.e | e e | Λa:k. e | e A
If we have both type operators and polymorphism, we get F-omega. This system is more or less the kernel type theory of most modern functional languages (like ML and Haskell). It is also vastly more powerful than System F -- it is equivalent in strength to higher order arithmetic.
λP (LF)
k ::= ∗ | Πx:A. k
A ::= a | p | Πx:A. B | Λx:A.B | A e
e ::= x | λx:A.e | e e
Instead of polymorphism, we could have gone in the direction of dependency from simply-typed lambda calculus. If you permitted the function type to let its argument be used in the return type (ie, write Πx:A. B(x) instead of A → B), then you get λP. To make this really useful, we have to extend the set of kinds with a kind of type operators which take terms as arguments Πx:A. k , and so we have to add a corresponding abstraction Λx:A.B and application A e at the type level as well.
This system is sometimes called LF, or the Edinburgh Logical Framework.
It has the same computational strength as the simply-typed lambda calculus.
λP2 (no special name)
k ::= ∗ | Πx:A. k
A ::= a | p | Πx:A. B | ∀a:k.A | Λx:A.B | A e
e ::= x | λx:A.e | e e | Λa:k. e | e A
We can also add polymorphism to λP, to get λP2. This system is not often used, so it doesn't have a particular name. (The one paper I've read which used it is Herman Geuvers' Induction is Not Derivable in Second Order Dependent Type Theory.)
This system has the same strength as System F.
λPω_ (no special name)
k ::= ∗ | Πx:A. k | Πa:k. k'
A ::= a | p | Πx:A. B | Λx:A.B | A e | λa:k.A | A B
e ::= x | λx:A.e | e e
We could also add type operators to λP, to get λPω_. This involves adding a kind Πa:k. k' for type operators, and corresponding type-level abstraction Λx:A.B and application A e.
Since there's again no jump in computational strength over the STLC, this system should also make a fine basis for a logical framework, but no one has done it.
λPω (the Calculus of Constructions)
k ::= ∗ | Πx:A. k | Πa:k. k'
A ::= a | p | Πx:A. B | ∀a:k.A | Λx:A.B | A e | λa:k.A | A B
e ::= x | λx:A.e | e e | Λa:k. e | e A
Finally, we get to λPω, the Calculus of Constructions, by taking λPω_ and adding a polymorphic type former ∀a:k.A and term-level abstraction Λa:k. e and application e A for it.
The types of this system are much more expressive than in F-omega, but it has the same computational strength.