1
$\begingroup$

What are the differences between the rule $$ \frac{\Gamma\vdash a:A\quad \Gamma \vdash b:B}{\Gamma \vdash T(a,b) \text{ type}} \quad (\text{Rule 1}) $$ and the rule $$ \frac{}{\Gamma,a:A,b:B\vdash T(a,b)\text{ type}} \quad (\text{Rule 2}) $$

What I mean is, how do we know which rule to use in each situation? For example, in the definition of universes, a version of the first rule is used:

$$\frac{}{\Gamma \vdash U \text{ type}}\quad \frac{\Gamma\vdash a:U}{\Gamma \vdash \text{El}(a) \text{ type}}.$$

Why don't we use the following rule instead (at least I've never seen it used in the definition of universes): $$\frac{}{\Gamma,a:U\vdash \text{El}(a)\text{ type}}?$$

One difference that I see is that in Rule 1, $B$ cannot depend on $a:A$, but in Rule 2, it can (but not necessarily does). Is it true then that Rule 2 is more general, in the sense that whenever Rule 1 can be used, Rule 2 can be also used, but not vice versa?

$\endgroup$

3 Answers 3

2
$\begingroup$

I wasn't going to add an answer, because I think the other two are sufficient, but I noticed something in another question that failed to come across from them, I suppose.

I'm going to write your two rules somewhat more suggestively:

$$ \frac{Γ ⊢ X : A \quad Γ ⊢ Y : B}{Γ ⊢ T(X,Y)\ \mathsf{type}} \qquad \frac{}{Γ,x:A,y:B⊢ T(x,y)\ \mathsf{type}} $$

Note that I've capitalized $X$ and $Y$ in Rule 1, and not in Rule 2.

A significant difference between these two rules is that in Rule 1, $X$ and $Y$ are metavariables ranging over terms of the theory, while in Rule 2 they are object variables within the theory. This means that Rule 2 only states that we are allowed to form the type $T$ applied to two variables.

A consequence of this is that in theories that use rules like Rule 2, a substitution rule is essential to form compound types. But, it is typical for type theories to be designed so that substitution is an admissible rule. This means that any derivation that uses the rule could be systematically transformed to eliminate uses of the rule (although it might be inconvenient to write things that way). The reason this is possible with Rule 1 is that you can just push the substitution up to the subterms and obtain another valid instance of the rule, but you cannot substitute a term for a bound variable in the context (as one of the other answers points out). That is, you can eliminate the binding from the context and substitute a term for its later occurrences (that is what the substitution rule does), but you cannot 'bind' a compound term in the context.

However, this does not mean that object variables in the context should never be mentioned in rules. For instance, the rule for $Π$ introduction is:

$$\frac{Γ,x:A⊢ E : B}{Γ ⊢ λx. E : Π_{x:A}B}$$

The difference here is that $x$ actually must be an object variable for this to work. It is a bound variable in the $λ$ term and $Π$ type, so it must be an object variable. It does not make sense to try to restate this like Rule 1, schematic over a metavariable standing in for a term, because you cannot form a lambda binding an arbitrary term any more than you can assert a type for an arbitrary term in the context. Similarly, the formation rules for types with bound variables also need to mention non-schematic structure in the context.

This presents no obstacle to admissible substitution, though. One does not substitute for bound variables, any more than one substitutes into the variables within the context.

$\endgroup$
1
$\begingroup$

Your Rule 2 is not more general than Rule 1, and I would not consider your Rule 2 to be a well-formed inference rule. I would recommend reading the "Preliminaries" section in Appendix A of the HoTT book to review what a context and a judgement mean. The judgement $\Gamma \vdash a : A$ means "under the context $\Gamma$, the expression $a$ has type $A$." Notably, $\Gamma$ is a context, which means that it has the form $$ x_1 : A_1, \dots, x_n : A_n $$ where $x_1,\dots,x_n$ are all variables and $A_1,\dots,A_n$ are all types, with $A_i$ being well-formed under the context $x_1 : A_1,\dots, x_{i-1} : A_{i-1}$.

Because $\Gamma$ is a context, we can't just add arbitrary facts to this context, the facts need to be of the form $x : A$ where $x$ is a variable and $A$ is a type. For example, consider this rule: $$ \frac{\Gamma \vdash e_1 : A \quad \Gamma \vdash e_2 : A}{\Gamma \vdash e_1 =_A e_2 \text{ type}} $$ This rule would allow us to come to a conclusion like: $$ \frac{\emptyset \vdash 1+2 : int \quad \emptyset \vdash 3+5 : int}{\emptyset \vdash 1+2 =_{int} 3+5 \text{ type}} $$ This kind of conclusion makes sense, $1+2 =_{int} 3+5$ is clearly a valid type under the empty context.

However, what if we used the corresponding "Rule 2" to this rule? $$ \frac{}{\Gamma, e_1 : A, e_2 : A \vdash e_1 =_A e_2 \text{ type}} $$ Then, we would get a conclusion like $$ \frac{}{1+2 : int, 3+5 : int \vdash 1+2 =_{int} 3+5 \text{ type}} $$ While $1+2 =_{int} 3+5 \text{ type}$ looks right as a type, the context here doesn't make any sense, because it does not take the form of $x_1 : A_1,\dots, x_n : A_n$: It has the form $e_1 : A, e_2 : A_2$ where $e_1,e_2$ are expressions, not just variables. So a rule like the "Rule 2" above is nonsensical.

In short, you have to remember what a context is, which is just an assignment of free variables to types, and thus you can't just add arbitrary facts to a context.

$\endgroup$
1
$\begingroup$

An answer has already been accepted, but it is incorrect. In fact, the two forms of rule are both valid, and they are in fact interchangeable in a type theory with weakening and exchange. In a substructural type theory without weakening and exchange, (Rule 2) is more general than (Rule 1).

For instance, I explain in this answer how to convert between them, and it is a corollary of a much more general result (Proposition 6.4 of Arkor–Fiore's Algebraic models of simple type theories).

However, as Dan Doel points out in the comments below, although the rules are interchangeable, they have different proof theoretic properties, which favour Rule 1.


I should say a few words to explain why the other answer is incorrect.

The other answer mentions the definition of judgement given in the HoTT Book, but the HoTT Book describes a notion of judgement in the context of a specific type theory. There are many notions of type theory that do not fit within the description given in the book.

Secondly, the other answer suggests that one comes to a nonsensical conclusion given (Rule 2). However, they have made a mistake in the application of (Rule 2): one should instead substitute $(1 + 2)$ for $e_1$ and $(3 + 5)$ for $e_2$, which crucially should remove $e_1$ and $e_2$ from the context, producing: $$ \frac{}{\Gamma \vdash (1 + 2) =_{\text{int}} (3 + 5)\ \text{type}} $$ which is correct.

$\endgroup$
4
  • $\begingroup$ Thank you for pointing that out. After reading your linked answer, I realized that I don't understand what it means to 'apply' a type to something, and so I asked a separate question about that here. $\endgroup$
    – user837242
    Apr 17 at 18:39
  • 1
    $\begingroup$ This answer is also not really correct. The reason to use rules like Rule 1 is that they make substitution admissible, which is the more precise criterion that the other answer is trying to get at. And if one is designing a substructural theory, there are substructural analogues of Rule 1 and such that retain the desirable meta-theoretic properties that Rule 2 doesn't. $\endgroup$
    – Dan Doel
    Apr 17 at 19:26
  • $\begingroup$ @DanDoel: I agree that is a good proof-theoretic motivation for Rule 1, but I don't see that that makes my answer incorrect. The original question was about generality of the rules with respect to one another. I also don't see the indication of admissibility of substitution present in the other answer that you are referring to. $\endgroup$
    – varkor
    Apr 17 at 20:17
  • $\begingroup$ I do agree that my answer is not a full answer to the question, though; I primarily wanted to address the inaccuracies in the other answer. I think it would be helpful for you to post a full answer. $\endgroup$
    – varkor
    Apr 17 at 20:26

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .