7
$\begingroup$

Question

If a pure type system has a terminating proof language, can we have Type : Type at the logic level without causing paradoxes (i.e., without causing ∀ (x : *) -> x to be inhabited)?

Example

Suppose we take a pure type theory such as the Calculus of Constructions, restrict functions to be affine (at most 1 variable uses) and add constructs for stratified duplications - see here for details. That language - which we could call EACC (Elementary Affine Calculus of Constructions) has a normalizing untyped fragment. That is, the reduction of any term - even ill-typed ones - is guaranteed to terminate due to the reduction rules (and, in particular, the restriction that duplicated terms can not change their levels).

$\endgroup$
  • $\begingroup$ Perhaps "Is Type : Type possible in an affine type theory?" is a better title? $\endgroup$ – Andrej Bauer Jul 18 '18 at 16:31
  • $\begingroup$ @AndrejBauer perhaps it needs a better body actually, I used EAL as an example but the actual question is if a terminating proof language makes Type : Type possible. $\endgroup$ – MaiaVictor Jul 18 '18 at 17:29
  • 1
    $\begingroup$ For basic type:type background I found these helpful: konne.me/2015/08/17/paradoxes.html The coq source is in his github repo github.com/konne88/konne88.github.io . There is also a very nice agda version: gist.github.com/favonia/cc7a504839c5fbb3ebc6 $\endgroup$ – user833970 Jul 19 '18 at 14:20
  • $\begingroup$ I'd like to try to look with more detail into your EACC. Are variables classified into affine and non-affine? Do these form separate environments? Why strange syntax with '$'. "$v x y" = "let v = x in y" right? Is v required to be affine? $\endgroup$ – Łukasz Lew Jul 19 '18 at 18:48
  • $\begingroup$ I think that in Coquand's "An Analysis of Girard's Paradox" he shows a type system (from Martin Lof) with type:type which is terminating but where every type has an inhabitant. $\endgroup$ – user833970 Aug 12 '18 at 0:36
8
$\begingroup$

The 'logic' of the contradiction with Type:Type is that you can create a term of any type including 'empty' type by 'cheating' by never returning. This is essentially the only way to cheat because of subject reduction and the subformula properties.

Subject reduction states that evaluation of terms preserves their type. If you have subject reduction and strong normalization (through whatever means), then you can infer that if you have a term of type T, you have a term of type T in a normal form - without any redexes (cuts) in it.

You have to go over all your type rules and verify that all of them have subformula property except the cut rule (which normalization eliminates). I.e you have to verify that if one of the non-cut rules were to produce a term of type T then you'll have one of its premises produce the term of type T (perhaps somewhere deeper in the derivation tree). AFAIK every good type system requires sub-formula property (I'd like to learn of examples that contradict it).

Since type derivations are supposed to be finite trees, and you have no axiom (0 premises) rule to introduce a term of an empty type, you can prove by induction that no tree can build a term of an empty type.

To reiterate, the role of normalization is that cut rule does not have sub-formula property, so we have to eliminate it first while preserving the type of the term.

This is the general sketch of Gentzen's proofs of consistency of logics.

$\endgroup$
  • 2
    $\begingroup$ In order to do that, I would have to perform the work that I described that needs to be done on an unfamiliar set of rules linked by Maia. I'm not confident enough that I would not make a mistake. $\endgroup$ – Łukasz Lew Jul 19 '18 at 16:05
  • $\begingroup$ Also, one might notice that I'm quite fuzzy about the subformula property, I would be happy to read some example of it in action. $\endgroup$ – Łukasz Lew Jul 19 '18 at 16:06
  • $\begingroup$ Oh I see. Objection withdrawn then :) $\endgroup$ – Stella Biderman Jul 19 '18 at 16:06
  • $\begingroup$ I love this answer, thanks for it! If I understand correctly, the cut rule for linear λ-calculus is better in that sense since it has the subformula property, right? $\endgroup$ – MaiaVictor Sep 27 '18 at 4:10
  • $\begingroup$ Cut rule (even linear) does not have sub-formula property since the cut-out formula is disappearing. That's why cut elimination (even in linear logic) is so important. $\endgroup$ – Łukasz Lew Sep 27 '18 at 22:04

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.