1 Introduction
In the simply typed lambdacalculus, to assign a type to a term, we first need to assign a type to its free variables. For instance, if we assign the type to the variable and the type nat to the variable , then we can assign the type to the term .
Whether a type is assigned to before or after one is assigned to is immaterial, so the context does not need to be ordered.
1.1 Wellformed Contexts
In systems, such as the Calculus of constructions, where atomic types are variables of a special type , contexts are ordered and, for instance, the term is assigned the type in the context but not in the context , that is not wellformed.
In a wellformed context, the declarations are ordered in such a way that the type of a variable only contains variables declared to its left. For instance, the context is wellformed, but the context is not. Moreover, in such a wellformed context, each type is itself welltyped in the context formed with the variable declarations to its left. For instance, the context is not wellformed. So, a context is said to be wellformed if, for each , is derivable for some sort in .
The original formulation of the Calculus of constructions of Coquand and Huet [5] has two forms of judgements: one expressing that a context is wellformed and another expressing that a term has a type in a context . Two rules define when a context is wellformed
and one enables the assignment of a type to a variable, in a wellformed context
These three rules together with five others—(sort), (prod), (abs), (app), and (conv)—form a eightrule presentation of the Calculus of constructions, and more generally of Pure type systems. Because the rule (var) requires the context to be wellformed, a variable can only be assigned a type in a wellformed context and this property extends to all terms, as it is an invariant of the typing rules.
This system was simplified by Geuvers and Nederhof [8] and Barendregt [2], who use a single form of judgement expressing that a term has a type in a context . First, they drop the context in the rule (var) simplifying it to
and add a weakening rule
to extend the judgement to . Then, they exploit the fact that the conclusion of the rule (decl) is now identical to the premise of the rule (var), to coin a derived rule
Now that the variables can be typed without using a judgement of the form , such judgements can be dropped, together with the rules (empty), (decl), and (var). So the two rules (start) and (weak), together with the five other rules form an equivalent sevenrule formulation of the Calculus of constructions, and more generally of Pure type systems.
1.2 Interacting Safely with an Unsafe Environment
When a judgement of the form is derived, the welltypedness of the term needs to be checked. But it can be checked either when the variable is added to the context or when it is used in the derivation of the judgement . In the system with the rules (decl) and (var), it is checked in the rule (decl), that is when the variable is added to the context. When the rule (var) is replaced with the rule (start), it is checked when the variable is used. These two systems illustrate two approaches to safety: the first is to build a safe environment, the second is to interact safely with a possibly unsafe environment.
In the formulation of Geuvers and Nederhof and Barendregt, it is still possible to define a notion of wellformed context: the context is wellformed if for each , is derivable. With such a definition, it is possible to prove that if the judgement is derivable, then is wellformed. In this proof, the second premise of the rule (weak), , is instrumental, as its only purpose is to preserve the wellformedness of the context.
We can go further with the idea of interacting safely with an unsafe environment and drop this second premise, leading to the weakening rule
Then, in the judgement , nothing prevents the context from being non wellformed, but the term is still welltyped because the rule (start), unlike the rule (var), has a premise . In such a system, the judgement is derivable, although the term is not welltyped, but the judgement is not because this term is not welltyped.
Yet, with the rule (start) and this strong weakening rule, the judgement is not derivable, because the judgement is not derivable. Thus, to make this judgement derivable, we should not use a weakening rule that erases all the declarations to the right of the declaration of nil and the rule (start). But we should instead use a rule that keeps the full context to type the term . Yet, like the rule (start), this rule should not check that the context is wellformed, but that the type of the variable is a welltyped term
This leads to the sixrule system described in Figure 1.
As the order of declarations in a context is now immaterial, contexts can indifferently be defined as sequences or as sets of declarations.
1.3 Previous Work
There are several reasons for using arbitrary contexts. One of them is that, as already noticed by Sacerdoti Coen [4], when we have two contexts and , for instance developed by different teams in different places, and we want to merge them, we should not have to make a choice between , and . We should just be able to consider the unordered context , provided it is a context, that is if is declared in and is declared in then .
Another is that, when we extend Pure type systems with computation rules, like in the logical framework Dedukti, we additionally want to declare constants in a signature and then add computation rules. For instance, we want to be able to declare constants in a signature and then computation rules , . Because, unlike in [6], the term is not welltyped without the computation rules, we cannot check the that the signature is wellformed before we declare the rules. But, because the rules use the constants declared in , we cannot declare the rules before the signature, in particular the rules do not make sense in the part of the signature to the left of the declaration of , that is in , where the constant is missing. And, because we sometimes want to consider rules where and are not welltyped terms [3], we cannot interleave constant declarations and computation rules. Note that in Blanqui’s Calculus of algebraic constructions [3], the contexts are required to be wellformed, but the signatures are not.
Another source of inspiration is the presentation of Pure type systems without explicit contexts [7], where Geuvers, Krebbers, McKinna, and Wiedijk completely drop contexts in the presentation of Pure type systems. In particular, Theorem 3.1 below is similar to their Theorem 19. The presentation of Figure 1 is however milder than their Pure type systems without explicit contexts, as it does not change the syntax of terms, avoiding, for instance, the question of the convertibility of and . In particular, if is derivable in the usual formulation of Pure type systems, it is also derivable in the system of Figure 1.
We show, in this note, that the system presented in Figure 1 indeed allows to interact safely with an unsafe environment, in the sense that if a judgement is derivable in this system, then there exists , such that and is derivable with the usual Pure type system rules. The intuition is that, because of the rule (var’), the structure of a derivation tree induces a dependency between the used variables of that is a partial order, and as already noticed by Sacerdoti Coen [4], a topological sorting of the used variables yields a linear context . Topological sorting is the key of Lemma 3.4.
So this paper build upon the work of Coquand and Huet [5], Geuvers and Nederhof [8], Barendregt [2], Blanqui [3], Sacerdoti Coen [4], and Geuvers, Krebbers, McKinna, and Wiedijk [7]. Its main contribution is to show that Pure type systems can be defined with six rules only, without a primitive notion of wellformed context, and without changing the syntax of terms.
2 Pure Type Systems
Let us first recall a usual definition of (functional) Pure type systems [8, 2]. To define the syntax of terms, we consider a set of sorts and a family of of infinite and disjoint sets of variables of sort . The syntax is then
A context is a sequence of pairs formed with a variable and a term, such that the variables are distinct. So, when we write the context , we implicitly assume that is not already declared in .
A context is said to be included into a context () if every in is also in .
Two contexts and are said to be compatible if each time is in and is in , then .
To define the typing rule, we consider a set of axioms, that are pairs of sorts and a set of rules, that are triple of sorts. As we restrict to functional Pure type systems, we assume that the relations and are functional.
Definition 2.1 (The type system )
Example. Consider two sorts and and an axiom . The judgement is derivable in . But the judgements is not because is declared before nat and the judgement is not because is not welltyped.
Definition 2.2 (Wellformed)
Wellformed contexts are inductively defined with the rules

the empty context is wellformed,

if is wellformed and is derivable in , then is wellformed.
Lemma 2.1
If is derivable, then is wellformed. Conversely, if is wellformed, then there exist two terms and , such that is derivable.
Proof. We prove that is wellformed, by induction on the derivation of . Conversely, if is wellformed and and are two sorts, such that then is derivable with the rules (sort) and (weak).
We will use the two following lemmas. The first is Lemma 18 in [8] and 5.2.12 in [2] and the second Lemma 26 in [8] and 5.2.17 in [2].
Lemma 2.2 (Thinning)
If is derivable, , and is wellformed, then is derivable.
Lemma 2.3 (Strengthening)
If is derivable and does not occur in , , and , then is derivable.
Lemma 2.4 (Strengthening contexts)
If is wellformed and does not occur in then is wellformed.
Proof. By induction on the structure of . If is empty, then is wellformed. Otherwise, . By induction hypothesis, is wellformed. As is wellformed, is derivable. By Lemma 2.3, is derivable. Thus, is wellformed.
If and are two wellformed contexts with no variables in common, then the concatenation also is wellformed. This remark extend to the case where and have variables in common, but are compatible.
Lemma 2.5 (Merging)
If and are two wellformed compatible contexts, then there exists a wellformed context , such that , , and .
Proof. By induction on of .

If is empty, we take . The context is wellformed, , , and .

If , then is wellformed and, by induction hypothesis, there exists a wellformed context , such that , , and .

If , then we take . The context is wellformed, , , and .

Otherwise, as and are compatible, contains no other declaration of . We take . We have , , . By Lemma 2.2, as , and , and is wellformed, is derivable , thus is wellformed.

Example. Consider two sorts and and an axiom . If and , the context is .
3 Arbitrary Contexts
Definition 3.1 (The type system )
The system is formed with the rules of Figure 1. With respect to the system , the rule (sort) is replaced with the rule (sort’), the rule (start) is replaced with the rule (var’), and the rule (weak) is dropped.
Example. Consider two sorts and and an axiom . The judgement is derivable in . So are the judgements and .
Lemma 3.1 (Thinning)
If and are two contexts, such that and is derivable in , then is derivable in .
Proof. By induction on the derivation of in .
Lemma 3.2 (Key lemma)
If is wellformed and is derivable in , then is derivable in .
Proof. By induction on the derivation of in .

If the derivation ends with the rule (sort’), then , , and . As is wellformed, is derivable in with the rules (sort) and (weak).

If the derivation ends with the rule (var’), then is a variable , , and is derivable in the system . As is wellformed, is derivable in . Thus, is derivable in with the rule (start). And, as is wellformed, is derivable with the rule (weak).

If the derivation ends with the rule (prod), then , , is derivable in , is derivable in , and . Then, as is wellformed, by induction hypothesis, is derivable in . Thus, is wellformed and, by induction hypothesis again, is derivable in . So, is derivable in with the rule (prod).

If the derivation ends with the rule (abs), then , , is derivable in , is derivable in , is derivable in , and . By induction hypothesis, is derivable in . Thus, is wellformed and, by induction hypothesis again, is derivable in and is derivable in . So, is derivable in with the rule (abs).

If the derivation ends with the rule (app), then , , is derivable in and is derivable in . By induction hypothesis is derivable in and is derivable in . Hence is derivable in , with the rule (app).

If the derivation ends with the rule (conv), then is derivable in , is derivable in , and . By induction hypothesis, is derivable in and is derivable in . Thus, is derivable in , with the rule (conv).
Lemma 3.3 (Reordering)
Let be a context, a variable that does not occur in , and a wellformed context, such that and is derivable in . Then, there exists a wellformed context , such that is derivable in .
Proof. If is in , then we have , and as , does not occur in . We take . By Lemma 2.4, is wellformed and, by Lemma 3.1, is derivable in .
Otherwise, we take . This context is wellformed and, by Lemma 3.1, is derivable in .
Lemma 3.4 (Context curation)
If is derivable in , then there exists a wellformed context , such that and is derivable in .
Proof. By induction on the derivation of .

If the derivation ends with the rule (sort’), then and , such that . We take the empty context for , , is wellformed, and is derivable in , with the rule (sort’).

If the derivation ends with the rule (var’), then is a variable , is an element of and is derivable in . By induction hypothesis, there exists a wellformed context , such that and is derivable in .
If is an element of , we take . We have and is wellformed. Moreover is derivable in and contains , thus is derivable in , with the rule (var’).

If the derivation ends with the rule (prod) then , , the contexts and are derivable in , and . Modulo equivalence, we can assume that does not occur in . By induction hypothesis, there exist two wellformed contexts and , such that , , and the judgements and are derivable in .
By Lemma 3.3, there exists a wellformed context such that is derivable in . As and contain no declaration of , by Lemma 2.5, there exists a wellformed context , such that , , and contains no declaration of . We have and . Thus, by Lemma 3.1, and are derivable in . Thus, is derivable in , with the rule (prod).

If the derivation ends with the rule (abs), then , , the judgements , , and are derivable in , and . Modulo equivalence, we can assume that does not occur in . By induction hypothesis, there exist three wellformed contexts , , and , such that , , , and the judgements , , and are derivable in .
By Lemma 3.3, there exists wellformed contexts and , such that the judgements and are derivable in . As , , and contain no declaration of , using Lemma 2.5 twice, there exists a wellformed context , such that , , , and contains no declaration of . We have , , and . Thus, by Lemma 3.1, the judgements , , and are derivable in . Thus, is derivable in , with the rule (abs).

If the derivation ends with the rule (app) then , , and the judgements and are derivable in . By induction hypothesis, there exists two wellformed contexts and , such that , , and the judgements and are derivable in .

If the derivation ends with the rule (conv) then the judgements and are derivable in , and . By induction hypothesis, there exists two wellformed contexts and , such that , , and the judgements and are derivable in .
Theorem 3.1
If is derivable in , then there exists , such that and is derivable in .
Proof. By Lemma 3.4, there exists a wellformed context , such that and is derivable in . By Lemma 3.2, is derivable in .
Example. Consider two sorts and and an axiom . From the derivation of the judgement, , we extract the context .
And from the derivation of , we also extract the context .
Acknowledgements
The author wants to thank Frédéric Blanqui, Herman Geuvers, and Claudio Sacerdoti Coen for useful and lively discussions about the various presentations of type theory.
References
 [1]
 [2] H. Barendregt (1992): Lambda calculi with types. In S. Abramsky, D.M. Gabbay & T.S.E. Maibaum, editors: Handbook of Logic in Computer Science, 2, Oxford University Press, pp. 117–309.
 [3] F. Blanqui (2001): Definitions by Rewriting in the Calculus of Constructions. In: Logic in Computer Science, IEEE Computer Society, pp. 9–18, doi:10.1109/LICS.2001.932478.
 [4] C. Sacerdoti Coen (2004): Mathematical Libraries as Proof Assistant Environments. In A. Asperti, G. Bancerek & A. Trybulec, editors: Mathematical Knowledge Management, Lecture Notes in Computer Science 3119, Springer, pp. 332–346, doi:10.1007/9783540278184_24.
 [5] T. Coquand & G. Huet (1988): The Calculus of Constructions. Information and Computation 76(2/3), pp. 95–120, doi:10.1016/08905401(88)900053.
 [6] D. Cousineau & G. Dowek (2007): Embedding Pure Type Systems in the LambdaPiCalculus Modulo. In S. Ronchi Della Rocca, editor: Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 4583, Springer, pp. 102–117, doi:10.1007/9783540732280_9.
 [7] H. Geuvers, R. Krebbers, J. McKinna & F. Wiedijk (2010): Pure Type Systems without Explicit Contexts. In K. Crary & M. Miculan, editors: Logical Frameworks and Metalanguages: Theory and Practice, Electronic Proceedings in Theoretical Computer Science 34, Open Publishing Association, pp. 53–67, doi:10.4204/EPTCS.34.6.
 [8] H. Geuvers & M.J. Nederhof (1991): Modular proof of strong normalization for the calculus of constructions. Journal of Functional Programming 1(2), pp. 155–189, doi:10.1017/S0956796800020037.
Comments
There are no comments yet.