<p>Regarding decidable type checking: this depends on whether you consider your λ-calculus with or without type annotations. System F (a.k.a second-order λ-calculus) has the three properties you cited, but it is proved that there is no algorithm that, given a System F term without type annotations, says whether this term can have a System F type.</p>

<p>In λ-calculi where types depend on terms (e.g. the Calculus of Constructions), it is necessary to decide when two terms are convertible (the same modulo β-reduction) during typing. This is done by checking that their normal forms are equal. The existence of normal forms and the possibility of computing them are ensured by the three properties cited.</p>

<p>The existence of nonterminating computations is a problem if you use type theory as a foundation of mathematics (this is what the first answer alludes to). A nonterminating term in a language that does not enforce termination, such as OCaml, may have type ∀X.X, also known as "False".</p>

<p>On the other hand, as pointed out before, nonterminating computations are not necessarily a problem if you use your type system for a programming language. First, certain computations are nonterminating (e.g. an operating system, the control loop of a user interface, of an airplane fly-by-wire system...); but it may be argued that such computations typically consist of a big loop whose body waits for an event and then executes a terminating computation. Furthermore, in a language such as Coq where you must prove termination, termination proofs are often very very tedious, to the extent that people often prefer to add an artificial extra argument initialized to a very high value, with some error condition if reaching zero, rather than proving termination,.</p>

CC BY-SA 3.0
2014-04-05T11:55:20.793Z
2014-04-05T11:55:20.793Z
David Monniaux
<p>Type theories have multiple uses, and with each kind of usage comes a different
notion of correctness. They two key uses are</p>

<ul>
<li><p>As a <strong>foundation of mathematics</strong>. In this context correctness means
primarily that we can't deduce falisity.</p></li>
<li><p>As a <strong>tool in programming</strong>. Here correctness means primarily that that
well-typed programs "don't go wrong" in Milner's famous words, i.e. that they do not
exhibit a certain forms of error, such as trying to execute 3 +
"hello".</p></li>
</ul>

<p>Both notions of correctness are related, but not the same.</p>

<p>Gödel's second incompleteness theorem puts serious restrictions in the way of showing the 'correctness' of type theories as a foundation of mathematics. The best you can hope for is to show 'correctness' (understood as consistency) relative to some other foundation, e.g. by giving a set-theoretic model.</p>

<p>The key thing we worry about with type theories is  that a given type-theory is inconsistent because we can define a non-terminating term. Modern type-theories are fairly complicated beasts, and it's quite easy to make them too powerful  so  that a fix-point combinator
becomes definable. Such fixpoint combinators inhabit every type, making the type-theory inconsistent as a foundation of mathematics. Since fixpoint combinators can be subtle, it is quite easy to overlook how one's typing system allows them to be defined. Indeed, famous foundationalists have a habit of
proposing foundations of mathematics that are unsound for this reason.  For example Martin-L&ouml;f's original proposal for type-theory made the kind of types itself a type (that approach to typing is now referred to as Type:Type). This is
extremely convenient, and gives you the most general form of impredicative polymorphism. Alas,  Girard discovered that this was unsound, when he managed to express the Burali-Forti paradox in Type:Type, see <a href="https://cs.stackexchange.com/questions/12929/example-of-a-false-proposition-when-assuming-type-type">this discussion</a> for more details.  Every since, Martin-L&ouml;f's type theories have been predicative, but with added inductive definitions to recover (much of) the expressive power of impredicativity.</p>

<p>Encoding a type theory in another foundation such as set theory gives us a fuzzy feeling of security: it says there are unlikely to be  an obvious unsoundness bugs in our type-theory. The justification behind this intuition is strictly empirical (!): in the century of since Cantor invented and Zermelo formalised it, nobody has found a soundness bug in conventional set theory. (As an aside, this situation is similar to cryptography where we trust RSA, Diffie-Hellman, AES or 3DES for little other reason than that they have withstood sustained attempts at breaking.)</p>

<p>Note that while a system with Type:Type is wrong as a foundation of
mathematics, it is perfectly acceptable as a typing system for
programming languages, because we can still show that no typeable program goes "wrong". </p>

<p>Regarding proof techniques for correctness, the different properties you mention relate to different notions
of correctness. Termination is the key step to showing correctness
of a type-theory as a foundation of mathematics, while subject
reduction is usually the key step to showing that a type-theory
is usable as a tool in programming. Note that since a termination
proof is the high-road to consistency as a foundation, by
G&ouml;del's second incompleteness theorem, we can prove termination of a type-theory only by using a stronger system.</p>

CC BY-SA 3.0
2014-04-04T19:58:34.903Z
And what constitutes a set theoretic model of a type theory?
Konstantin Solomatov
CC BY-SA 3.0
2014-04-04T20:00:35.377Z
On Gödel theorem, it says that we can't prove a consistency of a system within itself, however, we can get some philosophical explanation, which are not as precise as mathematical proof help a lot.
Konstantin Solomatov
CC BY-SA 3.0
2014-04-04T20:05:17.577Z
You can have a look at [Sets in Types, Types in Sets](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.55.1709&rep=rep1&type=pdf) by B. Werner.
Martin Berger
CC BY-SA 3.0
2014-04-05T23:07:00.123Z
Note that the proof of the Church-Rosser property is often (subtlety) used in the proof of termination, in addition to ensuring that type-checking is decidable in case of termination.
cody
CC BY-SA 3.0
2014-04-04T19:46:25.207Z
2014-04-05T12:36:30.003Z
2014-04-05T12:36:30.003Z
Martin Berger
<p>How to "proof"  that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one?</p>

<p>When type theories are introduced for example in Luo's book, the following properties are proved:</p>

<ul>
<li>Subject reduction</li>
<li>Reduction termination</li>
<li>Church-Rosser property</li>
</ul>

<p>As far as I understand, what these properties describe is that we have a decidable type checking, and that the language of type theory is meaningful in some sense, but nothing more than this.</p>

<p>I asked a question on violation of strict positivity for inductive types (<a href="https://cstheory.stackexchange.com/questions/21882/example-of-where-violation-of-strict-positivity-condition-in-inductive-types-lea">Example of where violation of strict positivity condition in inductive types leads to inconsistency</a>) and in the answer I was told that non strictly positive types might lead to non existence of set theoretic model. Why we need type theoretic model here? And what it gives to us?</p>

<lo.logic><type-theory><dependent-type>
"Correctness" of type theory
Konstantin Solomatov
# "Correctness" of type theory

(Asked by: username_0 on 2014-04-04)

How to "proof" that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one?

When type theories are introduced for example in Luo's book, the following properties are proved:

* Subject reduction
* Reduction termination
* Church-Rosser property

As far as I understand, what these properties describe is that we have a decidable type checking, and that the language of type theory is meaningful in some sense, but nothing more than this.

I asked a question on violation of strict positivity for inductive types ([Example of where violation of strict positivity condition in inductive types leads to inconsistency](https://cstheory.stackexchange.com/questions/21882/example-of-where-violation-of-strict-positivity-condition-in-inductive-types-lea)) and in the answer I was told that non strictly positive types might lead to non existence of set theoretic model. Why we need type theoretic model here? And what it gives to us?

**Tags:** lo.logic, type-theory, dependent-type

---

## 2 answers

### Answer by username_2 on 2014-04-04. Score: 11 | Accepted answer

Type theories have multiple uses, and with each kind of usage comes a different
notion of correctness. They two key uses are

* As a **foundation of mathematics**. In this context correctness means
  primarily that we can't deduce falisity.
* As a **tool in programming**. Here correctness means primarily that that
  well-typed programs "don't go wrong" in Milner's famous words, i.e. that they do not
  exhibit a certain forms of error, such as trying to execute 3 +
  "hello".

Both notions of correctness are related, but not the same.

Gödel's second incompleteness theorem puts serious restrictions in the way of showing the 'correctness' of type theories as a foundation of mathematics. The best you can hope for is to show 'correctness' (understood as consistency) relative to some other foundation, e.g. by giving a set-theoretic model.

The key thing we worry about with type theories is that a given type-theory is inconsistent because we can define a non-terminating term. Modern type-theories are fairly complicated beasts, and it's quite easy to make them too powerful so that a fix-point combinator
becomes definable. Such fixpoint combinators inhabit every type, making the type-theory inconsistent as a foundation of mathematics. Since fixpoint combinators can be subtle, it is quite easy to overlook how one's typing system allows them to be defined. Indeed, famous foundationalists have a habit of
proposing foundations of mathematics that are unsound for this reason. For example Martin-Löf's original proposal for type-theory made the kind of types itself a type (that approach to typing is now referred to as Type:Type). This is
extremely convenient, and gives you the most general form of impredicative polymorphism. Alas, Girard discovered that this was unsound, when he managed to express the Burali-Forti paradox in Type:Type, see [this discussion](https://cs.stackexchange.com/questions/12929/example-of-a-false-proposition-when-assuming-type-type) for more details. Every since, Martin-Löf's type theories have been predicative, but with added inductive definitions to recover (much of) the expressive power of impredicativity.

Encoding a type theory in another foundation such as set theory gives us a fuzzy feeling of security: it says there are unlikely to be an obvious unsoundness bugs in our type-theory. The justification behind this intuition is strictly empirical (!): in the century of since Cantor invented and Zermelo formalised it, nobody has found a soundness bug in conventional set theory. (As an aside, this situation is similar to cryptography where we trust RSA, Diffie-Hellman, AES or 3DES for little other reason than that they have withstood sustained attempts at breaking.)

Note that while a system with Type:Type is wrong as a foundation of
mathematics, it is perfectly acceptable as a typing system for
programming languages, because we can still show that no typeable program goes "wrong".

Regarding proof techniques for correctness, the different properties you mention relate to different notions
of correctness. Termination is the key step to showing correctness
of a type-theory as a foundation of mathematics, while subject
reduction is usually the key step to showing that a type-theory
is usable as a tool in programming. Note that since a termination
proof is the high-road to consistency as a foundation, by
Gödel's second incompleteness theorem, we can prove termination of a type-theory only by using a stronger system.

> **Comments:**
> **username_0**: And what constitutes a set theoretic model of a type theory?  
> **username_0**: On Gödel theorem, it says that we can't prove a consistency of a system within itself, however, we can get some philosophical explanation, which are not as precise as mathematical proof help a lot.  
> **username_2**: You can have a look at [Sets in Types, Types in Sets](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.55.1709&rep=rep1&type=pdf) by B. Werner.  
> **username_3**: Note that the proof of the Church-Rosser property is often (subtlety) used in the proof of termination, in addition to ensuring that type-checking is decidable in case of termination.  

---

### Answer by username_1 on 2014-04-05. Score: 2

Regarding decidable type checking: this depends on whether you consider your λ-calculus with or without type annotations. System F (a.k.a second-order λ-calculus) has the three properties you cited, but it is proved that there is no algorithm that, given a System F term without type annotations, says whether this term can have a System F type.

In λ-calculi where types depend on terms (e.g. the Calculus of Constructions), it is necessary to decide when two terms are convertible (the same modulo β-reduction) during typing. This is done by checking that their normal forms are equal. The existence of normal forms and the possibility of computing them are ensured by the three properties cited.

The existence of nonterminating computations is a problem if you use type theory as a foundation of mathematics (this is what the first answer alludes to). A nonterminating term in a language that does not enforce termination, such as OCaml, may have type ∀X.X, also known as "False".

On the other hand, as pointed out before, nonterminating computations are not necessarily a problem if you use your type system for a programming language. First, certain computations are nonterminating (e.g. an operating system, the control loop of a user interface, of an airplane fly-by-wire system...); but it may be argued that such computations typically consist of a big loop whose body waits for an event and then executes a terminating computation. Furthermore, in a language such as Coq where you must prove termination, termination proofs are often very very tedious, to the extent that people often prefer to add an artificial extra argument initialized to a very high value, with some error condition if reaching zero, rather than proving termination,.


---

