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).

Improve this question
$\endgroup$
5
  • $\begingroup$ Perhaps "Is Type : Type possible in an affine type theory?" is a better title? $\endgroup$
    – Andrej Bauer
    Jul 18, 2018 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, 2018 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, 2018 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, 2018 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, 2018 at 0:36

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
5
  • 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, 2018 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, 2018 at 16:06
  • $\begingroup$ Oh I see. Objection withdrawn then :) $\endgroup$
    – Stella Biderman
    Jul 19, 2018 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, 2018 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, 2018 at 22:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.