25
$\begingroup$

As stated in the title, I wonder any relation and difference between CIC and ITT. Could someone explain or point to me some literature that compares these two systems? Thanks.

$\endgroup$
  • 3
    $\begingroup$ To me ITT means "Intuitionnistic Type Theory" which could mean a number of things. In particular there are a large number of subtle variations from the original Martin-Lof description(s!), and it would help discussion if you gave the reference which describes the ITT you are thinking of. The short answer is this: ITT in the Martin-Lof sense without universe is a sub-theory of the CoC. In the presence of universes but no inductive types, you can crush all the universes into the single impredicative universe of the CoC. With large inductive types and large elimination, things are more complex. $\endgroup$ – cody Aug 1 '11 at 15:54
  • 1
    $\begingroup$ Ah and a good discussion of some of these things can be found in Geuvers : cs.ru.nl/~herman/PUBS/CC_CHiso.ps.gz $\endgroup$ – cody Aug 1 '11 at 16:00
  • $\begingroup$ Thanks for the comments and linked paper, cody. It looks what I am seeking for. $\endgroup$ – day Aug 2 '11 at 8:56
  • 1
    $\begingroup$ A pdf version of the paper mentioned by @cody: cs.ru.nl/~herman/PUBS/CC_CHiso.pdf $\endgroup$ – Steven Shaw Jul 8 '16 at 11:51
24
+100
$\begingroup$

I've already answered somewhat, but I'll try to give a more detailed overview of the type theoretical horizon, if you will.

I'm a bit fuzzy on the historical specifics, so more informed readers will have to forgive me (and correct me!). The basic story is that Curry had uncovered the basic correspondence between simply-typed combinators (or $\lambda$-terms) and propositional logic, which was extended by Howard to cover first-order logic, and IIRC independently discovered by de Bruijn in investigations around the hugely influential Automath system.

The Automath system was a refinement of Church's simple type theory which itself was a dramatic simplification of Russel and Whitehead's type theory with universes and the axiom of reducibility. This was relatively well-known logical terrain by the 1960s.

However, giving a coherent, simple, foundational system that encompassed both proof and term systems was still a very open question by 1970, and a first answer was given by Per Martin-Löf. He gives a very philosophical overview On the Meaning of the Logical Constants and the Justification of Logical Laws. He reasons that both in logic and mathematics, the meaning of constructions can be given by examining the introduction rules which allow the formation of those constructions as judgements, e.g. for conjunction $$ \frac{\vdash A\quad \vdash B}{\vdash A\wedge B}$$

Determines the corresponding elimination rule. He then gave a very powerful foundational system based on such judgements, allowing him to give a foundational system similar to Automath using very few syntactic constructions. Girard found that this system was contradictory, prompting Martin-Löf to adopt "Russel-style" predicative universes, severely limiting the expressiveness of the theory (by effectively removing the axiom of reducibility) and making it slightly more complex (but had the advantage of making it consistent).

The elegant constructions allowing for the definition of the logical symbols didn't work anymore though, which prompted M-L to introduce them in a different form, as inductively defined families. This is a very powerful idea, as it allows defining everything from judgmental equality and logical operators to natural numbers and functional data-types as they appear in computer science. Note that each family we add is akin to adding a number of axioms, which need to be justified as consistent in each instance. This system (dependent types + universes + inductive families) is usually what is referred to as ITT.

However there was some lingering frustration, as the powerful but simple foundational system was inconsistent, and the resulting system was more complex, and somewhat weak (in the sense that it was difficult to develop much of the modern mathematical framework in it). Enter Thierry Coquand, who with his supervisor Gerard Huet, introduced the Calculus of Constructions (CoC), which mostly solved these issues: a unified approach to proofs and data-types, a powerful (impredicative) foundational system and the ability to define "constructions" of the logical or mathematical variety. This eventually matured into an actual implementation of a system designed as a modern alternative to Automath, culminating in the Coq system we know and love.

I highly suggest this foundational paper on CoC, as Thierry knows a ridiculous amount about the historical development of type theory, and probably explains this much better than I. You might also want to check out his article on type theory, though it doesn't explain the C-H correspondence in much detail.

$\endgroup$
  • 5
    $\begingroup$ It might be worth remarking that the CoC, for all the power of its impredivative construction of data types, cannot prove induction, and later authors (e.g. Paulin-Mohring) extended the CoC with with inductive constructions a la Martin-Löf, yielding the Calculus of Inductive Constructions, which is used in Coq. $\endgroup$ – Martin Berger Mar 2 '15 at 21:57
  • 1
    $\begingroup$ Yes, I forgot to comment on this. However, adding the simple axiom $1\neq 0$ suffices (for a suitable encoding of the concepts involved). $\endgroup$ – cody Mar 2 '15 at 23:31
  • 1
    $\begingroup$ Inductive types were added to improve the computational behavior in addition to this. $\endgroup$ – cody Mar 2 '15 at 23:31
  • 1
    $\begingroup$ Well, the predecessor function can not be computed in constant time using the impredicative definition for natural numbers. See e.g. here or here. $\endgroup$ – cody Mar 3 '15 at 14:15
  • 1
    $\begingroup$ Yes, Church numerals, but a similar result is going to hold for more sensible data-types like linked lists. The Turing Machine example tends to suggest that Turing Machines are not well-suited for practical computation either! :) $\endgroup$ – cody Mar 16 '15 at 19:45

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.