1 Introduction
The distinction of the semantic spaces of elements and types is common practice in practically all type systems. However, some systems deeply intertwine both concepts, e.g., in the Calculus of Constructions [Reference Coquand and Huet7] elements and types may be built using bindings over both elements and types. In this context our focus is on systems which do not make this distinction, i.e., the only semantic objects are functions (which we assume to include constants), typing is a binary relation between functions, and a function may play an element role as well as a type role in this relation. A dependent product is not needed as a distinct semantic entity as it becomes the type role of a function.
A major problem with such systems is that the type rule for dependent products and the type rule for lambda abstraction cannot both be accepted when trying to achieve uniqueness of types, e.g., [Reference Kamareddine15] introduces the single-binder based
$\flat $
-cube, a variant of the
$\beta $
-cube which does accepts both rules but does not keep unique types. Nevertheless, a few systems that reject the product formation rule and satisfy uniqueness of types have been proposed, dating back to early ones such as
$\Lambda $
[Reference de Bruijn, Geuvers, Nederpelt and Vrijer5, Reference Nederpelt18] and as well as more recent approaches [Reference de Groote10–Reference Guidi12, Reference Weber20]. However these systems have a severe restriction as the rejection of the formation rule for dependent products entails that their functions do not support polymorphism, in the sense that a typed lambda operator cannot be applied to functions with varying number of arguments. This may have prevented a more widespread interest.
In this paper we present for the first time a system using a partial order on functions to restore some of the expressive power lost by the rejection of the type rule for dependent products. More specifically, the idea is to proceed in two steps:
First, we introduce an infinite set of constants acting as top objects and a strict partial order which characterizes the set of functions strictly smaller than a given top object. The function set characterized by a given top object has the following properties: It contains all strictly smaller top objects and all functions built using strictly smaller top objects, and it contains all functions whose type is contained in the function set. In the second step, the reflexive closure of this strict partial order is then embedded into function structures to yield a partial order which is used to extend the type relation by an inclusionFootnote 1 rule introducing bounded polymorphism. One might wonder at this point if the strict ordering is really necessary. As it turns out an approach with a single partial ordering would lead to an inconsistent system (see remark in Section 2).
It turns out that, as a consequence of the desired properties, the defining rules of the three relations, i.e., the strict partial order w.r.t. top objects, the partial order on functions, and the typing relation itself, are interdependent and must always be considered together when arguing about their properties. As another consequence of this approach the top objects are predicative in the sense that a function using some top object cannot be smaller than this object. Furthermore this approach obviously precludes a notion of uniqueness of types w.r.t.
$\beta $
-conversion, e.g., [Reference Lungu, Luo, Ghilezan, Geuvers and Ivetić16].
It is well known that types can be interpreted as propositions and elements as proofs [Reference Howard, Seldin and Hindley13]. In our semantic setting this analogy is valid in the form of proof roles and propositions roles of functions, however due to the predicative nature of the top objects, there is no analogy to the impredicative type of propositions as used e.g., in the calculus of constructions [Reference Coquand and Huet7]. Instead such form of expressiveness is approximated by a hierarchy of function sets defined through top objects. Note that due to the two roles a function may play this simultaneously leads to a hierarchy of sets of propositions as well as a hierarchy of predicative type universes. Furthermore, in this approach one can extend the propositions-as-types analogy by viewing the partial order described above logically as implication.
By adaptation of existing arguments [Reference Weber20] the proposed system, referred to as
$\mathtt {d}_{\leq }$
, can be shown to satisfy confluence and subject reduction (Section 3). Furthermore one can show that the ordering is a partial order, every set of expressions has a maximal element, and there is a (unique) minimal, logically strongest, type among all types of an element (Section 4). The latter result implies an alternative notion of uniqueness of types. Strong normalisation is the deepest property and, inspired by proof techniques from Automath [Reference de Bruijn, Seldin and Hindley4, Reference van Daalen8], its proof is based on a well-founded relation defined over a subsystem of expressions without eliminators called norms. It can be summarized as follows: In Section 5 we introduce the subset of expressions without eliminators, i.e., expressions without function application, as functional norms which can be assigned to some expressions. Norm assignment is less strict than typing as it requires satisfaction of structural properties only. We then show that norms can be assigned to all typable expressions. In Section 6 we then define a well-founded ordering on norms, classify all typable expression by their norms and, based on that, show inductively that all typable expressions are strongly normalising. Due to space constraints, we do not provide the proofs in full detail leaving out some simple or even obvious steps. Significantly more detail can be found in [Reference Weber21] (Appendix D) which also studies the extension by further operators as introduced in [Reference Weber20].
Semantic abstraction of the objects involved in typing, i.e., to use functions in element as well as type roles in a relational setting, is the major contribution of function-based type systems. This work shows that dependent products are not necessary for defining type systems with bounded polymorphism, rather it presents a consistent system with bounded polymorphism and minimal types where typing is a relation between partially ordered functions. The focus of this paper is on a function-based type system itself. The categorical and domain theoretical study of such systems and possible extensions might be interesting further topics. The same holds for a practical evaluation, in particular of the use of elements and types as roles and of the strictly predicative approach.
2 Function-based typing with bounded polymorphism
Definition 1 (Expressions).
Let
$\mathcal {V}=\{x,y,z,\ldots \}$
be an infinite set of variables and
$\mathcal {C}=\{\tau _{0},\tau _{1},\ldots \}$
be an infinite set of primitive constants of level
$0$
,
$1$
,
$\ldots $
. The set of expressions
$\mathcal {E}$
is generated by the following rules
$:$
$$ \begin{align*} \mathcal{E}&\!::=\!\mathcal{C}\,\mid\,\mathcal{V}\,\mid\,[\mathcal{V}:\mathcal{E}]\mathcal{E}\,\mid\,(\mathcal{E}\,\mathcal{E}). \end{align*} $$
Expressions will be denoted by
$a,b,c,\ldots $
.
$[x:a]b$
is a universal abstraction.
$(a\,b)$
is an application.
At this point we would like to make a notational remark: Since a universal abstraction can be interpreted both as element and as type (or proposition), there is, in our view, a notational and naming dilemma. For example, one and the same entity would be written appropriately as lambda-abstraction
$\lambda x\!:\!a.b$
in its role as an element and universal quantification
$\forall x\!:\!a.b$
in its role as a proposition and neither notation would adequately cover both roles. Therefore we use a more neutral notation
$[x:a]b$
.
Definition 2 (Free variables, substitution).
Variables occurring in an expression which do not occur in the range of a binding occur free in the expression.
${{FV}}(a)$
which denotes the set of free variables of an expression a is defined as follows:
${{FV}}(\tau _{n})=\{\}$
,
${{FV}}(x)=\{x\}$
,
${{FV}}((a\,b))={{FV}}(a)\cup {{FV}}(b)$
, and
${{FV}}([x:a]b)={{FV}}(a)\cup ({{FV}}(b)\setminus \{x\})$
.
The substitution
$a\lbrack b/x\rbrack $
of all free occurrences of variable x in expression a by expression b is defined as follows:
$\tau _{n}\lbrack b/x\rbrack =\tau _{n}$
,
$y\lbrack b/x\rbrack =b$
if
$x=y$
and y otherwise,
$(a\,b)\lbrack c/x\rbrack =(a\lbrack c/x\rbrack \,b\lbrack c/x\rbrack )$
,
$([y:a]b)\lbrack c/x\rbrack =[y:a\lbrack c/x\rbrack ]b$
if
$x=y$
and
$[y:a\lbrack c/x\rbrack ]b\lbrack c/x\rbrack $
otherwise.
A substitution
$a\lbrack b/x\rbrack $
may lead to name clashes in case a variable y occurring free in the inserted expression b comes into the range of a binding of y in the original expression. These name clashes can be avoided by renaming of variables.
Definition 3 (Renaming).
Renaming on bound variables is usually called
$\alpha $
-conversion and induced by the following axiom
$(\mathit{using\ the\ notation} =_{\alpha })$
.
$$\begin{align*}\frac{y\notin{{FV}}(b)}{[x:a]b \;=_{\alpha}\; [y:a]b\lbrack y/x\rbrack}. \end{align*}$$
Remark (Implicit renaming, name-free representation).
To avoid clutter, we will write variables as strings but always assume appropriate renaming of bound variables in order to avoid name clashes. This assumption is justified because one could also use a less-readable but name-free presentation of expressions using e.g., de Bruijn indexes [Reference de Bruijn3] which would avoid the necessity of renaming all together.
In the following proofs we will informally refer to basic properties of substitution, e.g., that
$x\neq y$
and
$x\notin {{FV}}(c)$
imply
$a\lbrack b/x\rbrack \lbrack c/y\rbrack = a\lbrack c/y\rbrack \lbrack b\lbrack c/y\rbrack /x\rbrack $
.
Definition 4 (Single-step reduction, reduction, congruence).
Single-step reduction
$a\to b$
is the smallest relation satisfying the axiom
$\beta : ([x:a]b\:c)\;\to \;b\lbrack c/x\rbrack $
and the following four inference rules. (app
$_1$
):
$\textit{If}\ a_1\to b_1\ then\ (a_1\,a_2)\to (b_1\,a_2)$
. (app
$_2$
):
$\textit{If}\ a_2\to b_2\ then\ (a_1\,a_2)\to (a_1\,b_2)$
. (abs
$_1$
):
$\textit{If}\ a_1\to b_1\ then\ [x:a_1]a_2\to [x:b_1]a_2$
. (abs
$_2$
):
$\textit{If}\ a_2\to b_2\ then\ [x:a_1]a_2\to [x:a_1]b_2$
.
Reduction
$a\to ^* b$
is defined as the reflexive and transitive closure of single-step reduction
$a\to b$
. We use the notation
$a\to ^* b\to ^* c\ldots $
to indicate reduction sequences. Congruence of expressions, denoted by
$a=_{\lambda } b$
, is defined as the symmetric and transitive closure of reduction.
In the following proofs we will informally refer to basic properties of reduction and congruence, e.g., that
$[x:a]b\to ^* c$
implies
$c=[x:d]e$
where
$a\to ^* d$
and
$b\to ^* e$
.
Definition 5 (Context).
A context, denoted by
$\Gamma $
, is a sequence of declarations
$(x_1 :a_1,\ldots ,x_n :a_n)$
, where
$x_i$
are variables with
$x_i\neq x_j$
and
$a_i$
are expressions. The assumption about name-free representation of bound variables justifies the uniqueness assumption.
${{dom}}(\Gamma )=\{x_1,\ldots ,x_n\}$
and
${{ran}}(\Gamma )=\{a_1,\ldots ,a_n\}$
denote the domain and range of a context
$\Gamma $
.
$\Gamma ,x:a$
denotes the extension of
$\Gamma $
on the right by a binding
$x:a$
where x is an variable not yet declared in
$\Gamma $
.
$\Gamma _1,\Gamma _2$
denotes the concatenation of contexts declaring disjoint variables. The lookup of a variable in a context is defined by
$\Gamma (x_i)=a_i$
. Substitution is extended to contexts as usual. The empty context is written as
$()$
or simply omitted.
Definition 6 (Typing, inclusion, τ-inclusion, validity).
Typing
$\Gamma \!\vdash \! a:b$
, inclusion
$\Gamma \!\vdash \! a\leq b$
, and
$\tau _{}$
-inclusion
$\Gamma \!\vdash \! a<\tau _{n}$
are the smallest ternary relations on contexts and two expressions satisfying the inference rules of Table 1. The resulting system is referred to as
$\mathtt {d}_{\leq }$
.
Function-based typing with bounded polymorphism.
Validity
$\Gamma \!\vdash \! a$
of an expression a under a context
$\Gamma $
denotes that there is an expression b such that
$\Gamma \!\vdash \! a:b$
.
Note that the rules of the type relation, of inclusion, and of
$\tau _{}$
-inclusion are interdependent. Hence properties have to be established by simultaneous consideration of all three relations. Note that in the rules start and weak, which are introducing an identifier in their conclusion, in line with our assumption about renaming of identifiers, we assume that this identifier is indeed new, i.e., not used in any other expression in the rule.
Element roles and type roles can be illustrated by two simple examples: Let
$C=[x:\tau _{0}]\tau _{0}$
be the constant function delivering
$\tau _{0}$
, for any given argument of type
$\tau _{0}$
. In its role as a type, C corresponds to an implication (“
$\tau _{0}$
implies
$\tau _{0}$
”), and its proofs include the identity
$I=[x:\tau _{0}]x$
over
$\tau _{0}$
, i.e.,
$\vdash \! I:C$
using essentially the rules ax, start, and abs. In its role as an element, C corresponds to a constant function, and it will type to itself, i.e.,
$\vdash \! C:C$
using the rules ax and weak. I, which as element is obviously the identity function, in its role as a type corresponds to the proposition “everything of type
$\tau _{0}$
is true” which should not have any elements. This will be shown (Proposition 50) as a consequence of strong normalisation.
More generally, in the rule appl the type role of a universal abstraction (
$[x:b]c$
) can be intuitively understood as an infinite conjunction of instances
$c\lbrack b_1/x\rbrack \wedge c\lbrack b_2/x\rbrack \ldots $
where
$b_i:b$
for all i. Individual instances (
$c\lbrack b_i/x\rbrack $
) can be projected by means of the application operator. Intuitively, a proof of a universal abstraction (
$[x:a]c$
) must provide an infinite list of instances (
$b\lbrack a_1/x\rbrack ,b\lbrack a_2/x\rbrack ,\ldots $
where
$\kern1pt b\lbrack a_i/x\rbrack :c\lbrack a_i/x\rbrack $
for all i). Consequently, in the rule abs a universal abstraction (
$[x:a]b$
where
$x:a\!\vdash \! b:c$
) has the element role of being a proof of another universal abstraction (
$[x:a]c$
).
The reflexive axiom (ax) postulates that each constant is in the range of the typing relation. In a logical interpretation this means that all constants are true. The axiom might seem strange as the use of a reflexive axiom in combination with basic rules of PTS leads to paradoxes, e.g., [Reference Coquand6, Reference Hurkens14], see also [Reference Barendregt1](Section 5.5). However, as shown in [Reference Weber20] ax leads to a consistent non-polymorphic system and this result is extended here to bounded polymorphism. Intuitively consistency is not surprising due to the predicative character of the system, which does not even have an impredicative type for building propositions.
The six rules about inclusion and
$\tau _{}$
-inclusion pretty much directly formalize the desired properties mentioned in the introduction. Note that
$\vdash \!\tau _{n}:\tau _{n}$
does not imply that
$\Gamma \!\vdash \!\tau _{n}:a$
, for some a hence the preconditions of rule ord
$_<$
. Note that in a logical interpretation the three rules of inclusion are tautologies and, since all constants are true,
$\tau _{}$
-inclusion is also tautological.
Remark (Inconsistent extensions and variations).
Extensions by axioms such as
$\,\!\vdash \!\tau _{0}<\tau _{0}$
would lead to an obvious inconsistency: By abs
$_<$
we would have
$\,\!\vdash \! C<\tau _{0}$
and therefore by typ
$_<$
we obtain
$\,\!\vdash \! I<\tau _{0}$
. Therefore using emb
$_{\leq }$
and inc we could eventually type
$\,\!\vdash \! u:[x:I]x$
where
$u=[x:I](x\,x)$
. With a similar argument one could type the diverging element
$\,\!\vdash \!(u\,u):I$
.
Similarly for variations removing
$\tau _{}$
-inclusion and replacing its use in the rules typ
$_<$
and abs
$_<$
by inclusion. One would have
$\,\!\vdash \! C\leq \tau _{0}$
and
$\,\!\vdash \! I\leq \tau _{0}$
and hence could type
$\!\vdash \!(u\,u):I$
. Note this typing is independent on the rule ax in the sense that it only needs the property
$\,\!\vdash \!\tau _{0}$
.
For readability in this and all following examples we write
$[a\!\Rightarrow \! b]$
to denote
$[x:a]b$
if x is not free in b.
To illustrate bounded polymorphism let
$\Gamma =(N:\tau _{0},0:N)$
and let
$N_1=[N\!\Rightarrow \!\tau _{1}]$
be the functional space from N to
$\tau _{1}$
: For example
$[n:N]n$
is in this space since
$\Gamma \!\vdash \![n:N]n:[N\!\Rightarrow \! N]$
and
$\Gamma \!\vdash \![N\!\Rightarrow \! N]\leq N_1$
and therefore by inc
$\Gamma \!\vdash \![n:N]n:N_1$
.
$\Gamma \!\vdash \![N\!\Rightarrow \! N]\leq N_1$
follows from emb
$_{\leq }$
and abs
$_{\leq }$
since
$\Gamma ,n:N\!\vdash \! N<\tau _{1}$
where the latter statement can derived using typ
$_<$
. Similarly one can show that
$\Gamma \!\vdash \![n:N][m:N]n:N_1$
.
Consider now the polymorphic function
$f=[x:N_1](x\,0)$
instantiating the first argument of members of
$N_1$
by
$0$
. Obviously
$\Gamma \!\vdash \! f:[N_1\!\Rightarrow \!\tau _{1}]$
. Using abs and appl and the examples from the previous paragraph we obtain
$\Gamma \vdash \! (f\:[n:N]n):N$
and
$\Gamma \vdash \! (f\:[n:N][m:N]n):[N\!\Rightarrow \! N]$
with
$$\begin{align*}(f\:[n:N]n)\,=_{\lambda}\,0 \qquad (f\:[n:N][m:N]n)\,=_{\lambda}\,[m:N]0. \end{align*}$$
Compare this to the use of f in a type role, e.g., with
$\Gamma =(N:\tau _{0},0:N,r:f)$
we have
$\Gamma \!\vdash \! (r\,[n:N][m:N]n):(f\,[n:N][m:N]n)$
and
$(f\,[n:N][m:N]n)=_{\lambda }[m:N]0$
. Now the type hierarchy has been extended downward and
$N_1$
can be interpreted as a (very small) universe of types.
For an example of a polymorphic function over
$\tau _{2}$
let
$N_2=[N_1\!\Rightarrow \!\tau _{2}]$
be the functional space from
$N_1$
to
$\tau _{2}$
. Consider the function
$F=[P:N_2](P\;[n:N]n)$
instantiating functions from
$N_2$
by instantiating their argument by the identity function over N. Obviously
$\Gamma \!\vdash \! F:[N_2\!\Rightarrow \!\tau _{2}]$
and for example with
$g=[x:N_1][y:N_1](x\,0)$
we obtain
$$\begin{align*}(F\,f)\,=_{\lambda}\,(f\,[n:N]n)\,=_{\lambda}\,0 \qquad (F\,g)\,=_{\lambda}\,(g\,[n:N]n)\,=_{\lambda}\,[y:N_1]0. \end{align*}$$
Similar remarks as for the function f can be made about the use of F in a type role and the interpretation of
$N_2$
as a (somewhat larger) universe of types.
On a more general level, informally speaking, for
$n=0$
,
$1$
,
$\ldots $
the statement
$\vdash \! a:\tau _{n}$
characterizes an increasing level of polymorphism:
If
$\!\vdash \! a:\tau _{0}$
then
$\tau _{}$
-inclusion obviously becomes empty and hence the inclusion relation
$\Gamma \!\vdash \! a\leq b$
collapses to the identity
$\Gamma \!\vdash \! a\leq a$
leading to a system equivalent to the kernel of
$\mathtt {d}$
[Reference Weber20] which has no polymorphism when considering the element role of functions and no universes when considering the type role of functions.
If
$\!\vdash \! a:\tau _{1}$
then
$\tau _{}$
-inclusion introduces polymorphism for function whose type hierarchy is based on type
$\tau _{0}$
only and a universe of types whose type hierarchy is based on type
$\tau _{0}$
only. By the type hierarchy of a given expression a we refer to sequences a, b, c,
$\ldots $
, where
$\vdash \! a:b$
,
$\vdash \! b:c$
,
$\ldots $
. With rising n eventually all valid expressions will be covered (Proposition 16).
For intuition about the relationship between
$\mathtt {d}_{\leq }$
and the
$\lambda $
-cube (e.g., [Reference Barendregt1]), one may consider subsystems
$\mathtt {d}^{(n)}_{\leq }$
where the primitive constants
$\tau _{i}$
are permitted up to some maximal index n only. Note that each subsystem
$\mathtt {d}^{(n)}_{\leq }$
has parametrized objects that may have both element and type roles, so when comparing
$\mathtt {d}^{(n)}_{\leq }$
to the
$\lambda $
-cube the three axis of the cube collapse into one, however the set of elements as well as the number of type universes considered being restricted by
$\tau _{n}$
. These relationships are illustrated in Figure 1.
Relation between degree of polymorphism and levels of universes.
With growing index n, on the horizontal axis the expressiveness of the system successively approximates the calculus of constructions, and on the vertical axis it successively approximates the addition of predicative type universes (e.g., [Reference Luo17]). The formal investigation of these relationships is not in the scope of this work.
3 Basic properties
We begin with confluence of reduction. After that we show basic (decomposition) properties of typing, inclusion, and
$\tau _{}$
-inclusion, ending with subject reduction.
Proposition 1 (Confluence of reduction).
If
$a=_{\lambda } b$
then
$a\to ^* c$
and
$b\to ^* c$
for some c. As a consequence
$=_{\lambda }$
is transitive.
Proof. Confluence of reduction for the proposed system has already been argued several times, either directly [Reference de Groote10] or for an extended system [Reference Weber20].
Since transitivity of
$=_{\lambda }$
is frequently used, we sometimes omit the reference to Proposition 1. Furthermore we will informally use basic consequences of confluence, e.g., that
$a=_{\lambda } b$
implies
$c\lbrack a/x\rbrack =_{\lambda } c\lbrack b/x\rbrack $
as well as
$a\lbrack c/x\rbrack =_{\lambda } b\lbrack c/x\rbrack $
. We continue with a substitution lemma.
Proposition 2 (Substitution and typing).
Let
$\Gamma _a=(\Gamma _1,x:a,\Gamma _2)$
and
$\Gamma _b=(\Gamma _1, \Gamma _2\lbrack b/x\rbrack )$
where
$\Gamma _1\!\vdash \! b:a$
. For all c, d, n:
$\Gamma _a\!\vdash \! c:d$
implies
$\Gamma _b\!\vdash \! c\lbrack b/x\rbrack :d\lbrack b/x\rbrack $
,
$\Gamma _a\!\vdash \! c\leq d$
implies
$\Gamma _b\!\vdash \! c\lbrack b/x\rbrack \leq d\lbrack b/x\rbrack $
, and
$\Gamma _a\!\vdash \! c<\tau _{n}$
implies
$\Gamma _b\!\vdash \! c\lbrack b/x\rbrack <\tau _{n}$
.
Proof. Simultaneous induction on all three relations. It is a straightforward extension of the corresponding proof of the same property in
$\mathtt {d}$
in [Reference Weber20] (Lemma 4.35) to inclusion and
$\tau _{}$
-inclusion. For example in case of
$\tau _{}$
-inclusion and rule typ
$_<$
we have
$\Gamma _a\!\vdash \! c:c'$
for some
$c'$
where
$\Gamma _a\!\vdash \! c'<\tau _{n}$
. By inductive hypothesis
$\Gamma _b\!\vdash \! c\lbrack b/x\rbrack :c'\lbrack b/x\rbrack $
and
$\Gamma _b\!\vdash \! c'\lbrack b/x\rbrack <\tau _{n}$
hence by rule typ
$_<\ \Gamma _b\!\vdash \! c\lbrack b/x\rbrack <\tau _{n}$
.
As a direct consequence of the rules of inclusion and
$\tau _{}$
-inclusion we note that both are relations on valid expressions.
Proposition 3 (Inclusion and validity).
$\Gamma \!\vdash \! a<\tau _{n}$
implies
$\Gamma \!\vdash \! a$
,
$\Gamma \!\vdash \!\tau _{n}$
and
$\Gamma \!\vdash \! a\leq b$
implies
$\Gamma \!\vdash \! a$
,
$\Gamma \!\vdash \! b$
.
Proof. Obvious arguments on the definition of
$\tau _{}$
-inclusion and inclusion.
Based on this we can show a first closure property of validity.
Proposition 4 (Valid expressions have valid types).
If
$\Gamma \!\vdash \! a:b$
then
$\Gamma \!\vdash \! b$
.
Proof. Induction on the definition of
$\Gamma \!\vdash \! a:b$
. It is an extension of the corresponding proof in [Reference Weber20] using Proposition 2 for the case of application. Note that in case of rule inc we have
$\Gamma \!\vdash \! a:c$
and
$\Gamma \!\vdash \! c\leq b$
for some c and therefore by Proposition 3
$\Gamma \!\vdash \! b$
.
Validity statements can be decomposed.
Proposition 5 (Validity decomposition).
$(\Gamma _1,x:a,\Gamma _2)\vdash \! b$
implies
$\Gamma _1\!\vdash \! a$
. As a consequence
$\Gamma \!\vdash \![x:a]b$
implies
$\Gamma \!\vdash \! a$
and
$\Gamma ,x:a\!\vdash \! b$
.
Proof. Simple inductive argument for both the property and the consequence, see [Reference Weber20].
We note some decomposition properties implied by the definition of inclusion.
Proposition 6 (Basic decomposition properties of inclusion).
-
(i)
$\Gamma \!\vdash \!\tau _{n}\leq a$
implies
$a=\tau _{m}$
for some m where either
$m=n$
or
$\Gamma \!\vdash \!\tau _{n}<\tau _{m}$
. -
(ii) If
$\Gamma \!\vdash \! a\leq [x:b]c$
then
$a=[x:b]d$
for some d where
$\Gamma ,x:b\!\vdash \! d\leq c$
. -
(iii) If
$\Gamma \!\vdash \![x:b]c\leq a$
then either
$a=[x:b]d$
for some d where
$\Gamma ,x:b\!\vdash \! c\leq d$
or
$a=\tau _{m}$
for some m.
Proof. Obvious inductive arguments on the definition of inclusion.
To consider inclusions modulo congruence we introduce two additional relations.
Definition 7 (λ-inclusion, λ *-inclusion).
$\lambda $
-inclusion
$\Gamma \!\vdash \! a\leq _{\lambda } b$
means that
$\Gamma \!\vdash \! b$
and that there are
$a'$
,
$b'$
where
$a=_{\lambda } a'$
,
$\Gamma \!\vdash \! a'\leq b'$
, and
$b'=_{\lambda } b$
.
$\lambda ^*$
-inclusion
$\Gamma \!\vdash \! a\leq _{\lambda } b$
is defined as the transitive of closure of
$\Gamma \!\vdash \! a\leq _{\lambda } b$
.
Note the validity condition on b which ensures that in rule inc inclusion generalizes to
$\lambda $
-inclusion and
$\lambda ^*$
-inclusion (Proposition 8(v)). We will later show (Proposition 15) that
$\lambda $
-inclusion is transitive and that therefore
$\lambda ^*$
-inclusion is equivalent to
$\lambda $
-inclusion however this property requires to first show subject reduction (Proposition 11).
Next we show some basic properties of
$\lambda ^*$
-inclusion. Before that we need an auxiliary property about replacing congruent valid expressions in contexts.
Proposition 7 (Context equivalence and typing).
Let
$\Gamma _a=(\Gamma _1,x:a,\Gamma _2)$
and
$\Gamma _b=(\Gamma _1,x:b,\Gamma _2)$
where
$a=_{\lambda } b$
and
$\Gamma _1\!\vdash \! b$
: If
$\Gamma _a\!\vdash \! c<\tau _{n}$
then
$\Gamma _b\!\vdash \! c<\tau _{n}$
, if
$\Gamma _a\!\vdash \! c\leq d$
then
$\Gamma _b\!\vdash \! c\leq d$
, and if
$\Gamma _a\!\vdash \! c:d$
then
$\Gamma _b\!\vdash \! c:d$
. As a consequence
$\Gamma _a\!\vdash \! c\leq _{\lambda } d$
implies
$\Gamma _b\!\vdash \! c\leq _{\lambda } d$
and similar for
$\lambda ^*$
-inclusion.
Proof. Obvious inductive argument on all three relations. The consequences follow directly from the definition of
$\lambda $
-inclusion and a direct inductive argument on
$\lambda ^*$
-inclusion.
Proposition 8 (Basic properties of λ*-inclusion).
-
(i) If
$\Gamma \!\vdash \! a\leq _{\lambda ^*} b$
,
$a=_{\lambda } a'$
,
$b=_{\lambda } b'$
and
$\Gamma \!\vdash \! b'$
then
$\Gamma \!\vdash \! a'\leq _{\lambda ^*} b'$
. -
(ii) If
$\Gamma \!\vdash \! a\leq _{\lambda ^*} b$
where
$a=_{\lambda }\tau _{n}$
then
$b=_{\lambda }\tau _{m}$
for some m where
$\Gamma \!\vdash \!\tau _{n}\leq _{\lambda ^*}\tau _{m}$
. -
(iii) If
$\Gamma \!\vdash \! a\leq _{\lambda ^*}[x:b_1]b_2$
then
$a=_{\lambda }[x:b_1]a_2$
for some
$a_2$
where
$\Gamma \!\vdash \![x:b_1]a_2$
and
$\Gamma ,x:b_1\!\vdash \! a_2\leq _{\lambda ^*} b_2$
. -
(iv) If
$\Gamma \!\vdash \![x:a_1]a_2$
and
$\Gamma \!\vdash \! [x:a_1]a_2\leq _{\lambda ^*} b$
then either
$b=_{\lambda }[x:a_1]b_2$
for some
$b_2$
where
$\Gamma ,x:a_1\!\vdash \! a_2\leq _{\lambda ^*} b_2$
, or
$b=_{\lambda }\tau _{m}$
for some m where
$\Gamma \!\vdash \![x:a_1]a_2\leq _{\lambda ^*}\tau _{m}$
. -
(v) If
$\Gamma \!\vdash \! a:b$
and
$\Gamma \!\vdash \! b\leq _{\lambda ^*} c$
then
$\Gamma \!\vdash \! a:c$
.
Proof. We show first that each property is valid for
$\lambda $
-inclusion and then extend the argument to
$\lambda ^*$
-inclusion.
(i): For the case of
$\lambda $
-inclusion the property follows from Definition 7 and Proposition 1. The extension of this property to
$\Gamma \!\vdash \! a\leq _{\lambda ^*} b$
is straightforward.
(
$ii$
): For the case of
$\lambda $
-inclusion, if
$\Gamma \!\vdash \! a\leq _{\lambda } b$
where
$a=_{\lambda }\tau _{n}$
then by Definition 7
$a=_{\lambda } a'$
,
$\Gamma \!\vdash \! a'\leq b'$
, and
$b'=_{\lambda } b$
for some
$a'$
,
$b'$
. By definition of inclusion (Table 1) one of the following three cases must be true: (1)
$b'=a'$
, (2)
$b'=\tau _{m}$
for some m where
$\Gamma \!\vdash \! a'<\tau _{m}$
, or (3)
$b'$
is a universal abstraction. In case (1)
$\tau _{n}=_{\lambda } a=_{\lambda } a'=b'=_{\lambda }\tau _{m}$
and
$\Gamma \!\vdash \!\tau _{m}$
which by Proposition 1 implies
$n=m$
implying the property. In case (2) obviously
$\Gamma \!\vdash \! a'\leq \tau _{m}$
, and, since by Proposition 3
$\Gamma \!\vdash \!\tau _{m}$
by Definition 7 also
$\Gamma \!\vdash \! a'\leq _{\lambda }\tau _{m}$
, and therefore by (i)
$\Gamma \!\vdash \!\tau _{n}\leq _{\lambda }\tau _{m}$
. In case (3), if
$b'$
is a universal abstraction then by Proposition 6(
$ii$
)
$a'$
is a universal abstraction which is impossible since
$\tau _{n}=_{\lambda } a'$
. For the inductive extension to
$\lambda ^*$
-inclusion assume
$\Gamma \!\vdash \! a\leq _{\lambda ^*} d$
and
$\Gamma \!\vdash \! d\leq _{\lambda ^*} b$
for some d and
$a=_{\lambda }\tau _{n}$
. By inductive hypothesis of
$\Gamma \!\vdash \! a\leq _{\lambda ^*} d$
:
$d=_{\lambda }\tau _{k}$
for some k where
$\Gamma \!\vdash \!\tau _{n}\leq _{\lambda ^*}\tau _{k}$
. Hence by inductive hypothesis of
$\Gamma \!\vdash \! d\leq _{\lambda ^*} b$
:
$b=_{\lambda }\tau _{m}$
for some m where
$\Gamma \!\vdash \!\tau _{k}\leq _{\lambda ^*}\tau _{m}$
. By definition of
$\lambda ^*$
-inclusion
$\Gamma \!\vdash \!\tau _{n}\leq _{\lambda ^*}\tau _{m}$
which implies (
$ii$
).
(
$iii$
): For the case of
$\lambda $
-inclusion, if
$\Gamma \!\vdash \! a\leq _{\lambda }[x:b_1]b_2$
then
$\Gamma \!\vdash \![x:b_1]b_2$
,
$a=_{\lambda } a'$
,
$\Gamma \!\vdash \! a'\leq b'$
, and
$b'=_{\lambda }[x:b_1]b_2$
for some
$a'$
,
$b'$
. By definition of inclusion (Table 1) one of the following three cases must be true: (1)
$b'=a'$
, (2)
$b'=\tau _{m}$
for some m, or (3)
$a'{\kern-1pt}={\kern-1pt}[x:b_1']a_2$
and
$b'{\kern-1pt}={\kern-1pt}[x:b_1']b_2'$
for some
$b_1'$
,
$b_2'$
,
$a_2$
, where
$\Gamma ,x:b_1'\!\vdash \! a_2{\kern-1pt}\leq{\kern-1pt} b_2'$
. In case (1)
$a=_{\lambda } a'=b'=_{\lambda }[x:b_1]b_2$
and since
$\Gamma \!\vdash \![x:b_1]b_2$
by Proposition 5
$\Gamma ,x:b_1\!\vdash \! b_2$
and therefore
$\Gamma ,x:b_1\!\vdash \! b_2\leq _{\lambda } b_2$
which by Proposition 1 implies (
$iii$
) with
$a_2=b_2$
. Case (2) is impossible since obviously
$\tau _{m}\neq _{\lambda }[x:b_1]b_2$
. In case (3)
$[x:b_1]b_2=_{\lambda } b'=[x:b_1']b_2'$
hence by Proposition 1 and obvious properties of reduction
$b_1=_{\lambda } b_1'$
and
$b_2=_{\lambda } b_2'$
hence
$a=_{\lambda }[x:b_1]a_2$
. Since by Proposition 5
$\Gamma \!\vdash \! b_1$
and
$\Gamma ,x:b_1\!\vdash \! b_2$
, by Proposition 7
$\Gamma ,x:b_1\!\vdash \! a_2\leq b_2'$
and, using (i),
$\Gamma ,x:b_1\!\vdash \! a_2 \leq _{\lambda } b_2$
.
For the case of
$\lambda ^*$
-inclusion note that using (i) property (
$iii$
) can be reformulated equivalently as follows (
$iii'$
): For all b, if
$\Gamma \!\vdash \! a\leq _{\lambda ^*} b$
where
$b=_{\lambda }[x:b_1]b_2$
and
$\Gamma \!\vdash \![x:b_1]b_2$
for some
$b_1$
,
$b_2$
then
$\ldots $
(remainder of (
$iii$
)): On the one hand, assuming (
$iii'$
), (i) implies
$\Gamma \!\vdash \! a\leq _{\lambda ^*}[x:b_1]b_2$
, on the other hand, assuming (
$iii$
) one can set
$b=[x:b_1]b_2$
to obtain
$\Gamma \!\vdash \! a\leq _{\lambda ^*} b$
. The reformulated property is shown by induction on the definition of
$\Gamma \!\vdash \! a\leq _{\lambda ^*} b$
: If
$\Gamma \!\vdash \! a\leq _{\lambda } b$
,
$b=_{\lambda }[x:b_1]b_2$
, and
$\Gamma \!\vdash \![x:b_1]b_2$
for some
$b_1$
,
$b_2$
then by Proposition 1
$\Gamma \!\vdash \! a\leq _{\lambda }[x:b_1]b_2$
and we have the case of
$\lambda $
-inclusion from the previous paragraph. For the inductive step assume
$\Gamma \!\vdash \! a\leq _{\lambda ^*} d$
and
$\Gamma \!\vdash \! d\leq _{\lambda ^*} b$
for some d where
$b=_{\lambda }[x:b_1]b_2$
and
$\Gamma \!\vdash \![x:b_1]b_2$
. By inductive hypothesis of
$\Gamma \!\vdash \! d\leq _{\lambda ^*} b$
:
$d=_{\lambda }[x:b_1]d_2$
for some
$d_2$
where
$\Gamma \!\vdash \![x:b_1]d_2$
and
$\Gamma ,x:b_1\!\vdash \! d_2\leq _{\lambda ^*} b_2$
. By inductive hypothesis of
$\Gamma \!\vdash \! a\leq _{\lambda ^*} d$
:
$a=_{\lambda }[x:b_1]a_2$
for some
$a_2$
where
$\Gamma \!\vdash \![x:b_1]a_2$
and
$\Gamma ,x:b_1\!\vdash \! a_2\leq _{\lambda ^*} d_2$
. By definition of
$\lambda ^*$
-inclusion
$\Gamma ,x:b_1\!\vdash \! a_2\leq _{\lambda ^*} b_2$
.
(
$iv$
): Similar argument as for (
$iii$
) except that in the case of
$\lambda $
-inclusion case (1) requires the additional validity assumption
$\Gamma \!\vdash \![x:a_1]a_2$
and that case (2) immediately implies the property. Furthermore in the inductive step, if
$\Gamma \!\vdash \! a\leq _{\lambda ^*} d$
and
$\Gamma \!\vdash \! d\leq _{\lambda ^*} b$
then applying the inductive hypothesis to the first step may result in
$d=_{\lambda }\tau _{k}$
for some k and then (
$ii$
) is needed to show (
$iv$
).
(v): For the case of
$\lambda $
-inclusion,
$\Gamma \!\vdash \! b\leq _{\lambda } c$
by Definition 7 means that
$b=_{\lambda } b'$
,
$\Gamma \!\vdash \! b'\leq c'$
,
$c'=_{\lambda } c$
, and
$\Gamma \!\vdash \! c$
, for some
$b'$
and
$c'$
. By Proposition 3 we know that
$\Gamma \!\vdash \! b'$
and
$\Gamma \!\vdash \! c'$
hence from
$\Gamma \!\vdash \! a:b$
by conv and inc
$\Gamma \!\vdash \! a:c'$
and therefore by conv
$\Gamma \!\vdash \! a:c$
. The extension of this property to
$\Gamma \!\vdash \! b\leq _{\lambda ^*} c$
is straightforward.
We can now show decomposition properties of typing which will be used in many other proofs. Before that we show a generalization of the rule weak.
Proposition 9 (Context weakening).
If
$\Gamma _1\!\vdash \! c$
then
$(\Gamma _1,\Gamma _2)\!\vdash \! a:b$
implies
$(\Gamma _1,x:c,\Gamma _2)\!\vdash \! a:b$
. Similar for inclusion,
$\tau _{}$
-inclusion,
$\lambda $
-inclusion, and
$\lambda ^*$
-inclusion.
Proof. Simple consequence of rule weak.
Proposition 10 (Typing decomposition).
-
(i)
$\Gamma \!\vdash \!\tau _{n}:b$
implies
$b=_{\lambda }\tau _{m}$
for some m. -
(ii)
$\Gamma \!\vdash \! x:b$
implies
$x\in {{dom}}(\Gamma )$
and
$\Gamma \!\vdash \!\Gamma (x)\leq _{\lambda ^*} b$
. -
(iii)
$\Gamma \!\vdash \![x:a_1]a_2:b$
implies
$\Gamma ,x:a_1\!\vdash \! a_2:c$
for some c where
$\Gamma \!\vdash \![x:a_1]c\leq _{\lambda ^*} b$
. -
(iv)
$\Gamma \!\vdash \![x:a_1]a_2:[x:b_1]b_2$
implies
$a_1=_{\lambda } b_1$
and
$\Gamma ,x:a_1\!\vdash \! a_2:b_2$
. -
(v)
$\Gamma \!\vdash \! (a_1\,a_2):b$
implies
$\Gamma \!\vdash \! a_1:[y:c_1]c_2$
for some
$y\neq x$
,
$c_1$
,
$c_2$
where
$\Gamma \!\vdash \! a_2:c_1$
, and
$\Gamma \!\vdash \! c_2\lbrack a_2/y\rbrack \leq _{\lambda ^*} b$
.
Proof. In the following arguments we repeatedly make use of the fact that four of the seven typing rules of
$\mathtt {d}_{\leq }$
(Table 1) type a unique operator, i.e., a constant, a variable, a universal abstraction, or an application, and the remaining three rules weak, conv, and inc modify the type b or the context
$\Gamma $
of a given type statement
$\Gamma \!\vdash \! a:b$
only. Hence in an inductive argument about a statement
$\Gamma \!\vdash \! a:b$
where a is an concrete operator of
$\mathtt {d}_{\leq }$
, it is sufficient to consider the unique introduction rule of the operator followed by use of the rules weak, conv, and inc.
(i): We need to consider rule ax, followed by the use of rule weak, conv, and inc. Rule ax establishes
$b=_{\lambda }\tau _{m}$
for some m, rules weak and conv obviously preserve it. For rule inc the property is preserved thanks to Proposition 6(i). The proof of (
$ii$
) is similar to (i).
(
$iii$
): We need to consider rule abs, followed by use of rules weak, conv, and inc. Use of rule abs implies that
$\Gamma ,x:a_1\!\vdash \! a_2:c$
for some c. The property follows with
$b=[x:a_1]c$
since by Proposition 4 we know that
$\Gamma \!\vdash \! b$
which (Definition 7) implies
$\Gamma \!\vdash \! b\leq _{\lambda ^*} b$
. For the other rules the property follows from the inductive hypothesis and Proposition 9 in case of rule weak.
(
$iv$
): If
$\Gamma \!\vdash \![x:a_1]a_2:[x:b_1]b_2$
then by (
$iii$
)
$\Gamma ,x:a_1\!\vdash \! a_2:c$
and
$\Gamma \!\vdash \![x:a_1]c\leq _{\lambda ^*}[x:b_1]b_2$
for some c. By Proposition 8(
$iii$
)
$[x:a_1]c=_{\lambda }[x:b_1]d$
for some d where
$\Gamma ,x:b_1\!\vdash \! d\leq _{\lambda ^*} b_2$
. Since
$a_1=_{\lambda } b_1$
and by Proposition 5
$\Gamma \!\vdash \! a_1$
, by Proposition 7
$\Gamma ,x:a_1\!\vdash \! d\leq _{\lambda ^*} b_2$
. Since obviously
$c=_{\lambda } d$
by Proposition 8(i)
$\Gamma ,x:a_1\!\vdash \! c\leq _{\lambda ^*} b_2$
. By Proposition 8(v) we have
$\Gamma ,x:a_1\!\vdash \! a_2:b_2$
.
(v): For
$\Gamma \!\vdash \! (a_1\,a_2):b$
we need to consider rule appl followed by rules weak, conv, and inc. Use of rule appl implies
$b=c_2\lbrack a_2/y\rbrack $
for some
$y\neq x$
,
$c_2$
where
$\Gamma \!\vdash \! a_1:[y:c_1]c_2$
and
$\Gamma \!\vdash \! a_2:c_1$
for some
$c_1$
. By Proposition 4
$\Gamma \!\vdash \![y:c_1]c_2$
and therefore by (
$iii$
)
$\Gamma ,y:c_1\!\vdash \! c_2$
. By Proposition 2
$\Gamma \!\vdash \! b$
and therefore (Definition 7)
$\Gamma \!\vdash \! b\leq _{\lambda ^*} b$
. The other rules can be argued similar to (
$iii$
).
Based on the properties shown we can now turn to subject reduction which completes this section. Similarly to the substitution property (Proposition 2), this property is extended as follows:
Proposition 11 (Typing and inclusions under reduction).
Assume
$a\to ^* b$
:
$\Gamma \!\vdash \! a:c$
implies
$\Gamma \!\vdash \! b:c$
. As a consequence
$\Gamma \!\vdash \! c:a$
implies
$\Gamma \!\vdash \! c:b$
, and furthermore
$\Gamma \!\vdash \! a\leq c$
implies
$\Gamma \!\vdash \! b\leq c$
,
$\Gamma \!\vdash \! c\leq a$
implies
$\Gamma \!\vdash \! c\leq b$
, and
$\Gamma \!\vdash \! a<\tau _{n}$
implies
$\Gamma \!\vdash \! b<\tau _{n}$
for any n.
Proof. It is obviously sufficient to show all five properties for single-step reduction. Assume
$a\to b$
. We show that
$\Gamma \!\vdash \! a:c$
implies
$\Gamma \!\vdash \! b:c$
by induction on the definition of reduction (Definition 4):
For axiom
$\beta $
we have
$a=([x:a_1]a_2\;a_3)$
,
$b=a_2\lbrack a_3/x\rbrack $
, and
$\Gamma \!\vdash \!([x:a_1]a_2\;a_3):c$
. By Proposition 10(v)
$\Gamma \!\vdash \![x:a_1]a_2:[x:c_1]c_2$
,
$\Gamma \!\vdash \! a_3:c_1$
, and
$\Gamma \!\vdash \! c_2\lbrack a_3/x\rbrack \leq _{\lambda ^*} c$
for some
$c_1$
,
$c_2$
. By Proposition 10(
$iv$
)
$a_1=_{\lambda } c_1$
and
$\Gamma ,x:a_1\!\vdash \! a_2:c_2$
. By Proposition 5
$\Gamma \!\vdash \! a_1$
and therefore by rule conv it follows that
$\Gamma \!\vdash \! a_3:a_1$
and further by Proposition 2
$\Gamma \!\vdash \! a_2\lbrack a_3/x\rbrack :c_2\lbrack a_3/x\rbrack $
. By Proposition 8(v)
$\Gamma \!\vdash \! a_2\lbrack a_3/x\rbrack :c$
For rule abs
$_1$
we have
$a=[x:a_1]a_3$
,
$b=[x:a_2]a_3$
where
$a_1\to a_2$
, and
$\Gamma \!\vdash \![x:a_1]a_3:c$
. By Proposition 10(
$iii$
)
$\Gamma ,x:a_1\!\vdash \! a_3:c_2$
and
$\Gamma \!\vdash \![x:a_1]c_2\leq _{\lambda ^*} c$
for some
$c_2$
. By Proposition 5
$\Gamma \!\vdash \! a_1$
and therefore by inductive hypothesis
$\Gamma \!\vdash \! a_2$
. Therefore by Proposition 7
$\Gamma ,x:a_2\!\vdash \! a_3:c_2$
and hence by rule abs
$\Gamma \!\vdash \![x:a_2]a_3:[x:a_2]c_2$
. By Proposition 4
$\Gamma \!\vdash \! c$
,
$\Gamma \!\vdash \![x:a_2]c_2$
, and
$\Gamma \!\vdash \![x:a_1]c_2$
. Since
$[x:a_2]c_2=_{\lambda }[x:a_1]c_2$
, by Definition 7
$\Gamma \!\vdash \![x:a_2]c_2\leq _{\lambda ^*}[x:a_1]c_2$
and therefore
$\Gamma \!\vdash \![x:a_2]c_2\leq _{\lambda ^*} c$
. Hence by Proposition 8(v)
$\Gamma \!\vdash \! b:c$
. Rule abs
$_2$
can be argued in a similar way.
For rule app
$_1$
we have
$a=(a_1\,a_3)$
,
$b=(a_2\,a_3)$
where
$a_1\to a_2$
and
$\Gamma \!\vdash \!(a_1\,a_3):c$
. By Proposition 4
$\Gamma \!\vdash \! c$
. By Proposition 10(v)
$\Gamma \!\vdash \! a_1:[x:b_1]b_2$
,
$\Gamma \!\vdash \! a_3:b_1$
, and
$\Gamma \!\vdash \! b_2\lbrack a_3/x\rbrack \leq _{\lambda ^*} c$
for some x,
$b_1$
,
$b_2$
. By inductive hypothesis
$\Gamma \!\vdash \! a_2:[x:b_1]b_2$
and therefore by rule appl
$\Gamma \!\vdash \!(a_2\:a_3):b_2\lbrack a_3/x\rbrack $
. Hence by Proposition 8(v) we know that
$\Gamma \!\vdash \! b:c$
. Rule app
$_2$
can be argued in a similar way.
The first consequence, i.e., that
$\Gamma \!\vdash \! c:a$
implies
$\Gamma \!\vdash \! c:b$
follows from the rule conv. The other three consequences follows from simple inductive arguments on inclusion and
$\tau _{}$
-inclusion using elementary properties of reduction and Proposition 7.
As another simple consequence of Proposition 11 we extend and strengthen Proposition 10(i).
Proposition 12 (Typing of τ n ).
$\Gamma \!\vdash \!\tau _{n}:a$
as well as
$\Gamma \!\vdash \!\tau _{n}\leq a$
imply
$a=_{\lambda }\tau _{m}$
for some m where
$n\leq m$
, and
$\Gamma \!\vdash \!\tau _{n}<\tau _{k}$
implies
$n<k$
.
Proof. Inductive argument on all three relations. For example in case of
$\Gamma \!\vdash \!\tau _{n}:a$
and rule inc we have
$\Gamma \!\vdash \!\tau _{n}:b$
and
$\Gamma \!\vdash \! b\leq a$
for some b. By inductive hypothesis of
$\Gamma \!\vdash \!\tau _{n}:b$
we have
$b=_{\lambda }\tau _{k}$
for some k where
$n\leq k$
. Due to Proposition 1 it follows that
$b\to ^*\tau _{k}$
hence by Proposition 11
$\Gamma \!\vdash \!\tau _{n}:\tau _{k}$
and
$\Gamma \!\vdash \!\tau _{k}\leq a$
. So we have shown that
$\tau _{k}$
is a specific instance (of b in rule inc) for which we can apply the inductive hypothesis. Hence by inductive hypotheses of
$\Gamma \!\vdash \!\tau _{n}:\tau _{k}$
and
$\Gamma \!\vdash \!\tau _{k}\leq a$
we have
$n\leq k$
and
$a=_{\lambda }\tau _{m}$
for some m where
$k\leq m$
and hence
$n\leq m$
.
4 Ordering properties
In this section we show some basic ordering properties leading up to the definition of a unique type for valid expressions that is minimal with respect to inclusion. First we note that
$\tau _{}$
-inclusion is transitive.
Proposition 13 (Transitivity of τ-inclusion).
$\Gamma \!\vdash \! a<\tau _{m}$
and
$\Gamma \!\vdash \!\tau _{m}<\tau _{n}$
imply
$\Gamma \!\vdash \! a<\tau _{n}$
.
Proof. Induction on the definition of
$\Gamma \!\vdash \! a<\tau _{m}$
. Using Propositions 12 and 3 the case of rule ord
$_<$
is obvious. The case of rule abs
$_<$
is trivial. For rule typ
$_<$
we have
$\Gamma \!\vdash \! a:b$
and
$\Gamma \!\vdash \! b<\tau _{m}$
for some b. By inductive hypothesis
$\Gamma \!\vdash \! b<\tau _{n}$
. Hence by rule typ
$_<$
we know that
$\Gamma \!\vdash \! a<\tau _{n}$
.
In order to show transitivity of inclusion, we first need to show a restricted version.
Proposition 14 (Restricted transitivity of inclusion).
If
$\Gamma \!\vdash \! a\leq b$
and
$\Gamma \!\vdash \! b<\tau _{n}$
then
$\Gamma \!\vdash \! a<\tau _{n}$
.
Proof. By induction on the definition of
$\Gamma \!\vdash \! a\leq b$
we show that
$\Gamma \!\vdash \! a\leq b$
and
$\Gamma \!\vdash \! b<\tau _{n}$
imply
$\Gamma \!\vdash \! a<\tau _{n}$
. Rule refl
$_{\leq }$
is obvious. For rule emb
$_{\leq }$
we have
$b=\tau _{m}$
for some m where
$\Gamma \!\vdash \! a\leq \tau _{m}$
and
$\Gamma \!\vdash \!\tau _{m}<\tau _{n}$
. If
$a=\tau _{m}$
we are obviously done, otherwise
$\Gamma \!\vdash \! a<\tau _{m}$
and the property follows from Proposition 13.
For rule abs
$_{\leq }$
we have
$a=[x:a_1]a_2$
and
$b=[x:a_1]b_2$
where
$\Gamma ,x:a_1\!\vdash \! a_2\leq b_2$
. Since
$\Gamma \!\vdash \![x:a_1]b_2<\tau _{n}$
by definition of
$\tau $
-inclusion either
$\Gamma ,x:a_1\!\vdash \! b_2<\tau _{n}$
, and then by inductive hypothesis
$\Gamma ,x:a_1\!\vdash \! a_2<\tau _{n}$
and therefore by rule abs
$_<\ \Gamma \!\vdash \! a<\tau _{n}$
, or
$\Gamma \!\vdash \![x:a_1]b_2:c$
for some c where
$\Gamma \!\vdash \! c<\tau _{n}$
: In the latter case by Proposition 10(
$iii$
) we know that
$\Gamma ,x:a_1\!\vdash \! b_2:c_2$
for some
$c_2$
where
$\Gamma \!\vdash \![x:a_1]c_2\leq _{\lambda ^*} c$
. Since by Proposition 4
$\Gamma \!\vdash \![x:a_1]c_2$
we can apply Proposition 8(
$iv$
) and obtain cases (1)
$c=_{\lambda }[x:a_1]d$
for some d where
$\Gamma ,x:a_1\!\vdash \! c_2\leq _{\lambda ^*} d$
, or (2)
$c=_{\lambda }\tau _{m}$
for some m where
$\Gamma \!\vdash \![x:a_1]c_2\leq _{\lambda ^*}\tau _{m}$
.
-
(1) By Proposition 8(v)
$\Gamma ,x:a_1\!\vdash \! b_2:d$
and therefore
$\Gamma \!\vdash \![x:a_1]b_2:[x:a_1]d$
. By rule conv we have
$\Gamma \!\vdash \![x:a_1]b_2:c$
hence by rule typ
$_<\ \Gamma \!\vdash \![x:a_1]b_2<\tau _{n}$
. -
(2) Since
$\Gamma \!\vdash \![x:a_1]b_2:[x:a_1]c_2$
by Proposition 8(v) we know that
$\Gamma \!\vdash \![x:a_1]b_2:\tau _{m}$
. Obviously
$c\to ^*\tau _{m}$
hence since
$\Gamma \!\vdash \! c<\tau _{n}$
by Proposition 11 we know that
$\Gamma \!\vdash \! \tau _{m}<\tau _{n}$
. Hence by rule typ
$_<\ \Gamma \!\vdash \![x:a_1]b_2<\tau _{n}$
.
We can now show that in
$\mathtt {d}_{\leq }$
we are indeed dealing with partial orders.
Proposition 15. Inclusion and
$\lambda $
-inclusion are partial orders and as a consequence
$\lambda ^*$
-inclusion is equivalent to
$\lambda $
-inclusion.
Proof. Reflexivity of inclusion is obvious.
For transitivity, by induction on the definition of
$\Gamma \!\vdash \! a\leq b$
we show that
$\Gamma \!\vdash \! a\leq b$
and
$\Gamma \!\vdash \! b\leq c$
implies
$\Gamma \!\vdash \! a\leq c$
. Rule refl
$_{\leq }$
is obvious. For rule emb
$_{\leq }$
we have
$b=\tau _{n}$
and
$\Gamma \!\vdash \! a<\tau _{n}$
as well as
$\Gamma \!\vdash \!\tau _{n}\leq c$
. By definition of inclusion there are two cases: If
$c=\tau _{n}$
we are done, otherwise
$c=\tau _{m}$
for some m where
$\Gamma \!\vdash \!\tau _{n}<\tau _{m}$
and transitivity follows from Proposition 14. For rule abs
$_{\leq }$
we have
$a=[x:a_1]a_2$
and
$b=[x:a_1]b_2$
where
$\Gamma ,x:a_1\!\vdash \! a_2\leq b_2$
. From
$\Gamma \!\vdash \![x:a_1]b_2\leq c$
, by Proposition 6(
$iii$
) either (1)
$c=[x:a_1]c_2$
and
$\Gamma ,x:a_1\!\vdash \! b_2\leq c_2$
for some
$c_2$
, and then by inductive hypothesis
$\Gamma ,x:a_1\!\vdash \! a_2\leq c_2$
and therefore
$\Gamma \!\vdash \! a\leq c$
, or (2)
$c=\tau _{n}$
and then by Proposition 14
$\Gamma \!\vdash \![x:a_1]a_2<\tau _{n}$
and therefore
$\Gamma \!\vdash \! a\leq c$
.
For antisymmetry, by induction on the definition of
$\Gamma \!\vdash \! a\leq b$
we show that
$\Gamma \!\vdash \! a\leq b$
and
$\Gamma \!\vdash \! b\leq a$
implies
$a=b$
. The case of rule refl
$_{\leq }$
is obvious. For rule emb
$_{\leq }$
we have
$b=\tau _{n}$
, and
$\Gamma \!\vdash \! a<\tau _{n}$
as well as
$\Gamma \!\vdash \!\tau _{n}\leq a$
. From
$\Gamma \!\vdash \!\tau _{n}\leq a$
we know that either
$a=\tau _{n}$
or
$a=\tau _{m}$
for some m where
$\Gamma \!\vdash \!\tau _{n}<\tau _{m}$
. In the latter case, by Proposition 14
$\Gamma \!\vdash \!\tau _{m}<\tau _{m}$
which due to Proposition 12 is not possible. For rule abs
$_{\leq }$
we have
$a=[x:a_1]a_2$
and
$b=[x:a_1]b_2$
where
$\Gamma ,x:a_1\!\vdash \! a_2\leq b_2$
. From
$\Gamma \!\vdash \![x:a_1]b_2\leq a$
, by Proposition 6(
$ii$
) we know that
$\Gamma ,x:a_1\!\vdash \! b_2\leq a_2$
, and then by inductive hypothesis
$a_2=b_2$
which implies
$a=b$
.
The extension of these results to
$\lambda $
-inclusion is an easy consequence using Propositions 1 and 11. Transitivity of
$\lambda $
-inclusion obviously implies its equivalence to
$\lambda ^*$
-inclusion.
In order not to clutter the presentation, from now on we identify
$\lambda ^*$
-inclusions and
$\lambda $
-inclusions assuming implicit use of Proposition 15. The next property illustrates the role of the primitive constants.
Proposition 16 (Upper bounds).
All valid expressions are bounded by some
$\tau _{n}$
with respect to inclusion.
Proof. We first show that if
$\Gamma \!\vdash \! a:b$
then there is an n such that
$\Gamma \!\vdash \! b<\tau _{n}$
and
${{ran}}(\Gamma )<\tau _{n}$
.
${{ran}}(\Gamma )<\tau _{n}$
is an abbreviation for
$\Gamma \!\vdash \! c<\tau _{n}$
for all
$c\in {{ran}}(\Gamma )$
. The proof is by induction on the definition of
$\Gamma \!\vdash \! a:b$
.
In case of rule weak we have
$\Gamma ,x:c\!\vdash \! a:b$
where
$\Gamma \!\vdash \! a:b$
and
$\Gamma \!\vdash \! c:d$
. By inductive hypothesis
$\Gamma \!\vdash \! b<\tau _{n}$
and
${{ran}}(\Gamma )<\tau _{n}$
for some n. Hence by rule typ
$_<\ \Gamma \!\vdash \! a<\tau _{n}$
and by Proposition 9
$\Gamma ,x:c\!\vdash \! a<\tau _{n}$
. Similarly by inductive hypothesis
$\Gamma \!\vdash \! d<\tau _{m}$
and
${{ran}}(\Gamma )<\tau _{m}$
for some m. The property follows for the maximum of n and m using Proposition 13.
In case of rule appl we have
$a=(a_1\,a_2)$
,
$b=b_2\lbrack a_2/x\rbrack $
where
$\Gamma \!\vdash \!(a_1\,a_2):b_2\lbrack a_2/x\rbrack $
,
$\Gamma \!\vdash \! a_1:[x:b_1]b_2$
, and
$\Gamma \!\vdash \! a_2:b_1$
. By inductive hypothesis
$\Gamma \!\vdash \![x:b_1]b_2<\tau _{n}$
and
${{ran}}(\Gamma )<\tau _{n}$
for some n. Obviously
$\Gamma \!\vdash \! b_1<\tau _{n}$
and hence
${{ran}}(\Gamma ,x:b_1)<\tau _{n}$
and by rule typ
$_<\ \Gamma \!\vdash \! a_2<\tau _{n}$
. Obviously also
$\Gamma ,x:b_1\!\vdash \! b_2<\tau _{n}$
and hence the substitution property introduced in the next paragraph implies
$\Gamma \!\vdash \! b_2\lbrack a_2/x\rbrack <\tau _{n}$
.
Substitution property for
$\tau _{}$
-inclusion: Let
$\Gamma =(\Gamma _1,x:c_1,\Gamma _2)$
and
$\Gamma '=(\Gamma _1,\Gamma _2\lbrack c_2/x\rbrack )$
where
$\Gamma _1\!\vdash \! c_2:c_1$
. For all d, n: If
$\Gamma _1\!\vdash \! c_2<\tau _{n}$
,
$\Gamma \!\vdash \! d<\tau _{n}$
, and
${{ran}}(\Gamma )<\tau _{n}$
then
${{ran}}(\Gamma ')<\tau _{n}$
and
$\Gamma '\!\vdash \! d\lbrack c_2/x\rbrack <\tau _{n}$
. The obvious proof is by structural induction on the definition of
$\Gamma \!\vdash \! d<\tau _{n}$
using Proposition 2 for case typ
$_<$
.
As a consequence using rules typ
$_<$
and emb
$_{\leq }$
this implies that
$\Gamma \!\vdash \! a\leq \tau _{n}$
.
While there is no corresponding result on lower bounds we can show that the types of an expression have a minimal element.
Definition 8 (Minimal type).
If
$\Gamma \!\vdash \! a$
we define the minimal type
$M_{\Gamma }(a)$
recursively as follows:
$M_{\Gamma }(\tau _{n})=\tau _{n}$
,
$M_{\Gamma }(x)=\Gamma (x)$
,
$M_{\Gamma }([x:a]b)=[x:a]M_{\Gamma ,x:a}(b)$
, and
$M_{\Gamma }((a\:b))=d\lbrack b/x\rbrack $
where
$M_{\Gamma }(a)=[x:c]d$
.
Remark. The function is completely defined on its domain since
$\Gamma \!\vdash \!(a\:b)$
implies (Table 1)
$\Gamma \!\vdash \! a:[x:a_1]a_2$
for some
$a_1$
,
$a_2$
and hence
$M_{\Gamma }(a)=[x:a_1]a_3$
for some
$a_3$
.
We will show that minimal types are indeed minimal. Before that we need to generalize 2 to
$\lambda $
-inclusions.
Proposition 17 (λ-inclusion and substitution).
$\Gamma ,x:a\!\vdash \! b\leq _{\lambda } c$
and
$\Gamma \!\vdash \! d:a$
imply
$\Gamma \!\vdash \! b\lbrack d/x\rbrack \leq _{\lambda } c\lbrack d/x\rbrack $
.
Proof.
$\Gamma ,x:a\!\vdash \! b\leq _{\lambda } c$
implies
$b=_{\lambda } b'$
,
$\Gamma ,x:a\!\vdash \! b'\leq c'$
,
$c'=_{\lambda } c$
, and
$\Gamma \!\vdash \! c$
for some
$b'$
,
$c'$
. By 2
$\Gamma \!\vdash \! b'\lbrack d/x\rbrack \leq c'\lbrack d/x\rbrack $
and
$\Gamma \!\vdash \! c\lbrack d/x\rbrack $
. Since
$b\lbrack d/x\rbrack =_{\lambda } b'\lbrack d/x\rbrack $
and
$c\lbrack d/x\rbrack =_{\lambda } c'\lbrack d/x\rbrack $
we have
$\Gamma \!\vdash \! b\lbrack d/x\rbrack \leq _{\lambda } c\lbrack d/x\rbrack $
.
Proposition 18 (Minimal types are minimal).
$\Gamma \!\vdash \! a:b$
implies that
$\Gamma \!\vdash \! a:M_{\Gamma }(a)$
and
$\Gamma \!\vdash \!M_{\Gamma }(a)\leq _{\lambda } b$
.
Proof. Structural induction on a.
If
$a=\tau _{n}$
then by Proposition 12
$b=_{\lambda }\tau _{m}$
for some m where
$n\leq m$
. If
$n=m$
then by rule refl
$_{\leq }\ \Gamma \!\vdash \!\tau _{n}\leq \tau _{n}$
. If
$n<m$
then by rule ord
$_<$
, which is applicable since
$b\to ^*\tau _{m}$
, by Proposition 4
$\Gamma \!\vdash \! b$
, and therefore by Proposition 11
$\Gamma \!\vdash \!\tau _{m}$
, we obtain
$\Gamma \!\vdash \!\tau _{n}<\tau _{m}$
. In both cases this implies
$\Gamma \!\vdash \!M_{\Gamma }(a)=\tau _{n}\leq _{\lambda } b$
.
If
$a=x$
then by Proposition 10(
$ii$
)
$\Gamma \!\vdash \!\Gamma (x)\leq _{\lambda } b$
. Hence
$\Gamma \!\vdash \!M_{\Gamma }(a)\leq _{\lambda } b$
.
If
$a=[x:a_1]a_2$
then by Proposition 10(
$iii$
)
$\Gamma ,x:a_1\!\vdash \! a_2:c$
and
$\Gamma \!\vdash \![x:a_1]c\leq _{\lambda } b$
for some c. By inductive hypothesis
$\Gamma ,x:a_1\!\vdash \!M_{\Gamma ,x:a_1}(a_2)\leq _{\lambda } c$
hence obviously
$\Gamma \!\vdash \!M_{\Gamma }(a)\leq _{\lambda }[x:a_1]c$
and therefore by Proposition 15
$\Gamma \!\vdash \!M_{\Gamma }(a)\leq _{\lambda } b$
.
If
$a=(a_1\:a_2)$
then by Proposition 10(v)
$\Gamma \!\vdash \! a_1:[x:c_1]c_2$
for some x,
$c_1$
,
$c_2$
where
$\Gamma \!\vdash \! a_2:c_1$
and
$\Gamma \!\vdash \! c_2\lbrack a_2/x\rbrack \leq _{\lambda } b$
. By inductive hypothesis
$\Gamma \!\vdash \!M_{\Gamma }(a_1)\leq _{\lambda }[x:c_1]c_2$
. By Proposition 8(
$iii$
)
$M_{\Gamma }(a_1)=_{\lambda }[x:c_1]c_3$
for some
$c_3$
where
$\Gamma ,x:c_1\!\vdash \! c_3\leq _{\lambda } c_2$
. By Proposition 17
$\Gamma \!\vdash \! c_3\lbrack a_2/x\rbrack \leq _{\lambda } c_2\lbrack a_2/x\rbrack $
and therefore by definition of minimal type and Proposition 15
$\Gamma \!\vdash \!M_{\Gamma }(a)\leq _{\lambda } b$
.
5 Norms and norming
The idea for the proof of strong normalization of valid expressions in
$\mathtt {d}_{\leq }$
is to classify expressions according to structural properties in order to make an inductive argument work. For this purpose we use the expressions from
$\mathtt {d}_{\leq }$
without eliminators, i.e., without applications, as parametric structural skeletons called norms [Reference de Bruijn, Seldin and Hindley4, Reference van Daalen8]. Intuitively, norms can be seen as a reconstruction of bounded parametric types inside
$\mathtt {d}_{\leq }$
.
Definition 9 (norms).
The set of norms
$\bar {\mathcal {E}}$
is defined as follows
$:$
$$ \begin{align*} \bar{\mathcal{E}}&\!::=\!\mathcal{C}\,\mid\,\mathcal{V}\,\mid\,[\mathcal{V}:\bar{\mathcal{E}}]\bar{\mathcal{E.}} \end{align*} $$
We will use the notation
$\bar {a}$
,
$\bar {b}$
,
$\bar {c}$
,
$\ldots $
to denote norms.
Proposition 19 (Basic properties of norms).
Since norms are irreducible a lot of propositions can be simplified. For example on norms congruence
$\bar {a}=_{\lambda }\bar {b}$
is the same as equality
$\bar {a}=\bar {b}$
and
$\lambda $
-inclusion
$\Gamma \!\vdash \!\bar {a}\leq _{\lambda }\bar {b}$
is the same as inclusion
$\Gamma \!\vdash \!\bar {a}\leq \bar {b}$
. Furthermore all norms without free identifiers are valid and all types of norms are norms as well.
In order not to clutter the following presentations we assume implicit use of these properties.
The idea is to assign a unique norm to all expressions satisfying certain structural properties. Furthermore this assignment is intended have two key properties: Reduction of expression should not affect norm assignment (Proposition 21) and it should be possible to assign a norm to all valid expressions (Proposition 29).
The definition of norm assignment is complex since, as it turns out, when trying to achieve these properties, norming of applications cannot be defined in a compositional style. More precisely, when norming an application of a function to an argument the former cannot be normed in isolation but its norm also depends on its argument. To see this consider the exampleFootnote
2
$t=[x:[\tau _{0}\!\Rightarrow \!\tau _{1}]](x\,\tau _{0})$
. If we norm it to
$[[\tau _{0}\!\Rightarrow \!\tau _{1}]\!\Rightarrow \!\tau _{1}]$
independently of it use, then the application
$(t\,[\tau _{0}\!\Rightarrow \!\tau _{0}])$
would norm to
$\tau _{1}$
. However
$(t\,[\tau _{0}\!\Rightarrow \!\tau _{0}])\to ([\tau _{0}\!\Rightarrow \!\tau _{0}]\,\tau _{0})\to \tau _{0}$
which would violate the intended Proposition 21 (see also the first norming example below). As a consequence we have to include the argument context of a function when computing its norm. This is a major extension to the notion of norming as introduced in [Reference Weber20]. The machinery needed is provided by the following technical but straightforward definitions. In particular, we introduce an extension to contexts containing definitions in addition to declarations.
Definition 10. An extended context, denoted by
$\Lambda $
,
$\Lambda _1$
,
$\Lambda _2$
, etc. is a sequence
$(x_1\odot _1 a_1, \ldots , x_n\odot _n a_n)$
, where
$x_i$
are variables,
$x_i\neq x_j$
, and where each
$x_i\odot _i a_i$
stands for a declaration
$x_i:a_i$
or definition
$x_i\!:=\! a_i$
. For an extended context
$\Lambda $
,
${{dom}_:}(\Lambda )$
denotes the set of all variables which are declared,
${{dom}_{:=}}(\Lambda )$
denotes the set of all variables which are defined. The lookup
$\Lambda (x)$
of an variable x in an extended context is defined by
$\Lambda (x)=a_i$
if
$x=x_i$
.
$\Lambda ,x\!:=\! a$
denotes the extension of
$\Lambda $
on the right by a definition
$x\!:=\! a$
. Similar for
$\Lambda ,x:a$
.
$\Lambda _1,\Lambda _2$
denotes the concatenation of extended contexts. The empty extended context is written as
$()$
. Obviously, every context
$\Gamma $
is an extended context.
An extended context
$(x_1\odot _1\bar {a}_1$
,
$\ldots $
,
$x_n\odot _n\bar {a}_n)$
declaring or defining norms only, is called an extended norm context. Extended norm contexts are denoted by
$\bar {\Lambda }$
,
$\bar {\Lambda }_1$
,
$\bar {\Lambda }_2$
,
$\ldots $
.
Definition 11 (Norming).
Norming
$\,\parallel a \parallel _{\Lambda ,\Theta }$
of an expression a under an extended context
$\Lambda $
, and elimination list
$\Theta =(a_1,\ldots ,a_n)$
is a partial function defined in Table 2.
Definition of norming and generalized inclusion.
Furthermore, Table 2 defines generalized inclusion
$\Gamma \!\vdash \! a{{}\cdot \!{\!}\!\leq {}} b$
. Finally, Table 2 introduces extended context norming
$\,\parallel \Lambda _2 \parallel _{\Lambda _1}$
which is a partial function defined by
$\,\parallel () \parallel _{\Lambda _1}=()$
,
$\,\parallel (x:a,\Lambda _2) \parallel _{\Lambda _1}=(x:\,\parallel a \parallel _{\Lambda _1,()},\,\parallel \Lambda _2 \parallel _{\Lambda _1,x:a})$
, and
$\,\parallel (x\!:=\! a,\Lambda _2) \parallel _{\Lambda _1}=\,\parallel \Lambda _2 \parallel _{\Lambda _1,x:= a}$
. An expression a is normable under
$\Lambda $
and
$\Theta $
if
$\,\parallel a \parallel _{\Lambda ,\Theta }$
is defined. This is written as
$\Lambda ,\Theta \!\models \!\,a$
. Analogously for context norming where we write
$\Lambda _1\!\models \!\Lambda _2$
.
Note the use of elimination lists to manage the norm assignment of functions together with their arguments. For the motivation see the second norming example below. Note further that in the norm
$[x:\bar {c}]\bar {d}$
of the function a of an application
$(a\,b)$
the variable x does not have free occurrences in
$\bar {d}$
since it has already been substituted by means of the elimination list
$(b,\Theta )$
. Extended context norming is removing definitions since by construction a norm
$\,\parallel a \parallel _{\Lambda ,\Theta }$
obviously cannot have free variables
$x\in {dom}_{:=}(\Lambda )$
. As for empty contexts
$()$
we sometimes omit writing empty elimination lists and empty extended contexts. For example, we write
$\,\parallel a \parallel _{\Lambda }$
as abbreviation for
$\,\parallel a \parallel _{\Lambda ,()}$
and
$\,\parallel a \parallel _{}$
as abbreviation for
$\,\parallel a \parallel _{(),()}$
.
As a first example we show the use of elimination lists and the effect of function arguments on the result of norming: Let
$\Gamma =(x:[\tau _{0}\!\Rightarrow \!\tau _{0}],y:[\tau _{0}\!\Rightarrow \!\tau _{1}])$
and
$t=[z:[\tau _{0}\!\Rightarrow \!\tau _{1}]](z\,\tau _{0})$
. We have
$\,\parallel t \parallel _{\Gamma }=[[\tau _{0}\!\Rightarrow \!\tau _{1}]\!\Rightarrow \!\tau _{1}]$
. Now consider
$(t\;x)$
and
$(t\;y)$
.
-
•
$\,\parallel t \parallel _{\Gamma ,x}=[z:[\tau _{0}\!\Rightarrow \!\tau _{1}]]\,\parallel (z\,\tau _{0}) \parallel _{\Gamma ,z:= x}=[[\tau _{0}\!\Rightarrow \!\tau _{1}]\!\Rightarrow \!\tau _{0}]$
since
$\,\parallel z \parallel _{(\Gamma ,z:= x),\tau _{0}}=\,\parallel x \parallel _{(\Gamma ,z:= x),\tau _{0}}=\,\parallel [\tau _{0}\!\Rightarrow \!\tau _{0}] \parallel _{(\Gamma ,z:= x),\tau _{0}}=[\tau _{0}\!\Rightarrow \!\tau _{0}]$
. Hence
$\,\parallel (t\,x) \parallel _{\Gamma }=\tau _{0}$
. -
•
$\,\parallel t \parallel _{\Gamma ,y}=[z:[\tau _{0}\!\Rightarrow \!\tau _{1}]]\,\parallel (z\,\tau _{0}) \parallel _{\Gamma ,z:= y}=[[\tau _{0}\!\Rightarrow \!\tau _{1}]\!\Rightarrow \!\tau _{1}]$
since
$\,\parallel z \parallel _{(\Gamma ,z:= y),\tau _{0}}=\,\parallel y \parallel _{(\Gamma ,z:= y),\tau _{0}}=\,\parallel [\tau _{0}\!\Rightarrow \!\tau _{1}] \parallel _{(\Gamma ,z:= y),\tau _{0}}=[\tau _{0}\!\Rightarrow \!\tau _{1}]$
. Hence
$\,\parallel (t\,y) \parallel _{\Gamma }=\tau _{1}$
.
The generalized inclusion condition is needed in the following example: Let
$\Gamma =(x:\tau _{0},y:[z:\tau _{0}]z)$
. On the one hand, we have
$\Gamma \!\vdash \! (y\,x):x$
. On the other hand, since
$\,\parallel x \parallel _{\Gamma }=x$
,
$\,\parallel y \parallel _{\Gamma ,x}=\,\parallel [z:\tau _{0}]z \parallel _{\Gamma ,x}=[z:\tau _{0}]\,\parallel z \parallel _{\Gamma ,z:= x}=[z:\tau _{0}]x$
and
$\,\parallel \Gamma \parallel _{}=\Gamma \!\vdash \! x{{}\cdot \!{\!}\!\leq {}}\tau _{0}$
, we have
$\,\parallel (y\,x) \parallel _{\Gamma }=x$
. As a consequence when norming e.g.,
$([z:x]\tau _{0}\;(y\,x))$
we cannot use the type condition for the application but rather have to use inclusion.
To see that norming is a partial function let
$u=[x:[\tau _{1}\!\Rightarrow \!\tau _{0}]](x\,x)$
. When trying to norm
$(x\,x)$
with context
$x:[\tau _{1}\Rightarrow \tau _{0}]$
, first we obtain
$\,\parallel x \parallel _{x:[\tau _{1}\Rightarrow \tau _{0}],x}=\,\parallel [\tau _{1}\!\Rightarrow \!\tau _{0}] \parallel _{x:[\tau _{1}\Rightarrow \tau _{0}],x}=[\tau _{1}\!\Rightarrow \!\tau _{0}]$
as the norm of the function x in
$(x\,x)$
. However, since neither
$x:[\tau _{1}\!\Rightarrow \!\tau _{0}]\!\vdash \! x:\tau _{1}$
nor
$x:[\tau _{1}\!\Rightarrow \!\tau _{0}]\!\vdash \! x\leq \tau _{1}$
the argument x in
$(x\,x)$
does not satisfy the required generalized inclusion constraint. Hence
$\,\parallel (x\,x) \parallel _{x:[\tau _{1}\Rightarrow \tau _{0}]}$
and therefore also
$\,\parallel u \parallel _{}$
and
$\,\parallel (u\,u) \parallel _{}$
are undefined.
Substitution on an elimination list
$(a_1\ldots ,a_n)\lbrack a/x\rbrack $
is defined as an elimination list of substitutions
$(a_1\lbrack a/x\rbrack ,\ldots ,a_n\lbrack a/x\rbrack )$
. In order to show that norms are preserved by reduction we need the following substitution property.
Proposition 20 (Norm substitution property).
Let
$\Lambda =(\Lambda _1,x\!:=\! a,\Lambda _2)$
,
$\Lambda '$
=
$(\Lambda _1, \Lambda _2\lbrack a/x\rbrack )$
, and
$\Theta '=\Theta \lbrack a/x\rbrack $
. If
$\Lambda _1,x\!:=\! a\!\models \! \Lambda _2$
,
$\Lambda _1\!\models \!\Lambda _2\lbrack a/x\rbrack $
, and
$\,\parallel \Lambda \parallel _{}=\,\parallel \Lambda ' \parallel _{}$
then
$\Lambda ,\Theta \!\models \! b$
if and only if
$\Lambda ',\Theta '\!\models \! b\lbrack a/x\rbrack $
. Furthermore
$\,\parallel b \parallel _{\Lambda ,\Theta }=\,\parallel b\lbrack a/x\rbrack \parallel _{\Lambda ',\Theta '}$
.
Proof. The property can be seen by an inductive argument on
$\,\parallel b \parallel _{\Lambda ,\Theta }$
. If
$b=\tau _{n}$
then
$\,\parallel \tau _{n} \parallel _{\Lambda ,\Theta }=\tau _{n}=\,\parallel \tau _{n}\lbrack a/x\rbrack \parallel _{\Lambda ',\Theta '}$
. If
$b=x$
then
$x\in {{dom}_{:=}}(\Lambda )$
and
$\,\parallel x \parallel _{\Lambda ,\Theta }=\,\parallel a \parallel _{\Lambda ,\Theta }$
. Since obviously
${{FV}}(a)\cap {{dom}}(\Lambda _2)=\emptyset $
we have
$\,\parallel a \parallel _{\Lambda ,\Theta }=\,\parallel a \parallel _{\Lambda ',\Theta '}=\,\parallel x\lbrack a/x\rbrack \parallel _{\Lambda ',\Theta '}$
. If
$b=y$
where
$y\neq x$
then
$y\lbrack a/x\rbrack =y$
. If
$\Lambda ,\Theta \!\models \! y$
then by definition of norming there are two cases: If
$y\in {{dom}_:}(\Lambda )$
and
$\Theta =()$
then obviously
$\,\parallel y \parallel _{\Lambda }=y=\,\parallel y \parallel _{\Lambda '}$
. If
$y\in {{dom}_{:=}}(\Lambda )$
or if
$y\in {{dom}_:}(\Lambda )$
and
$\Theta \neq ()$
then
$\,\parallel y \parallel _{\Lambda ,\Theta }=\,\parallel \Lambda (y) \parallel _{\Lambda ,\Theta }$
. By inductive hypothesis
$\,\parallel \Lambda (y) \parallel _{\Lambda ,\Theta }=\,\parallel \Lambda (y)\lbrack a/x\rbrack \parallel _{\Lambda ',\Theta '}$
. Obviously
$\Lambda '(y)=\Lambda (y)\lbrack a/x\rbrack $
and therefore
$\,\parallel y \parallel _{\Lambda ,\Theta }=\,\parallel \Lambda '(y) \parallel _{\Lambda ',\Theta '}=\,\parallel y \parallel _{\Lambda ',\Theta '}$
. Conversely if
$\Lambda ',\Theta '\!\models \! y\lbrack a/x\rbrack $
a similar argument can be made with
$\Lambda '$
and
$\Theta '$
.
If
$b=[y:b_1]b_2$
where
$y\neq x$
then if
$\Lambda ,\Theta \!\models \! b$
there are two cases: If
$\Theta =()$
we can calculate as follows:
$$ \begin{align*} &\,\parallel [y:b_1]b_2 \parallel_{\Lambda}\\ =_{(\text{Definition}\;{11})}&\,[y:\,\parallel b_1 \parallel_{\Lambda}]\,\parallel b_2 \parallel_{\Lambda,y:b_1}\\ =_{(\text{Inductive hypothesis})}&\,[y:\,\parallel b_1\lbrack a/x\rbrack \parallel_{\Lambda'}]\,\parallel b_2\lbrack a/x\rbrack \parallel_{\Lambda',y:b_1\lbrack a/x\rbrack}\\ =_{(\text{Definitions}\;{2},\,{11})}&\,\parallel ([y:b_1]b_2)\lbrack a/x\rbrack \parallel_{\Lambda'}. \end{align*} $$
The use of the inductive hypothesis on
$\,\parallel b_2 \parallel _{\Lambda ,y:b_1}$
is justified since based on the inductive hypothesis on
$\,\parallel b_1 \parallel _{\Lambda }$
we know that
$\,\parallel \Lambda ,y:b_1 \parallel _{}=(\,\parallel \Lambda \parallel _{},y:\,\parallel b_1 \parallel _{\Lambda })= (\,\parallel \Lambda ' \parallel _{}, y:\,\parallel b_1\lbrack a/x\rbrack \parallel _{\Lambda '})=\,\parallel \Lambda ',y:b_1\lbrack a/x\rbrack \parallel _{}$
. If
$\Theta = (c,\Theta _1)$
then
$\Theta ' = (c\lbrack a/x\rbrack ,\Theta _1\lbrack a/x\rbrack )$
and
$$ \begin{align*} &\,\parallel [y:b_1]b_2 \parallel_{\Lambda,(c,\Theta_1)}\\ =_{(\text{Definition}\;{11})}&[y:\,\parallel b_1 \parallel_{\Lambda}]\,\parallel b_2 \parallel_{(\Lambda,y:= c),\Theta_1}\\ =_{(\text{Inductive hypothesis})}&\,[y:\,\parallel b_1\lbrack a/x\rbrack \parallel_{\Lambda'}]\,\parallel b_2\lbrack a/x\rbrack \parallel_{(\Lambda',y:= c\lbrack a/x\rbrack),\Theta_1\lbrack a/x\rbrack}\\ =_{(\text{Definitions}\;{2},\,{11})}&\,\parallel ([y:b_1]b_2)\lbrack a/x\rbrack \parallel_{\Lambda',\Theta'}. \end{align*} $$
The use of the inductive hypothesis on
$\,\parallel b_2 \parallel _{(\Lambda ,y:= c),\Theta _1}$
is justified since
$\,\parallel \Lambda ,y\!:=\! c \parallel _{}=\,\parallel \Lambda \parallel _{}=\,\parallel \Lambda ' \parallel _{}=\,\parallel \Lambda ',y\!:=\! c\lbrack a/x\rbrack \parallel _{}$
. Conversely if
$\Lambda ',\Theta '\!\models \! b\lbrack a/x\rbrack $
a similar argument can be made with
$\Theta '$
.
If
$b=(b_1\,b_2)$
then if
$\Lambda ,\Theta \!\models \! b$
we have
$\,\parallel (b_1\,b_2) \parallel _{\Lambda ,\Theta }=\bar {c}_2$
for some
$\bar {c}_2$
where
$\,\parallel b_1 \parallel _{\Lambda ,(b_2,\Theta )}=[y:\bar {c}_1]\bar {c}_2$
and
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b_2 \parallel _{\Lambda }{{}\cdot \!{\!}\!\leq {}}\bar {c}_1$
for some
$\bar {c}_1$
and y where we may assume
$y\neq x$
. From the inductive hypothesis
$\Lambda ',(b_2\lbrack a/x\rbrack ,\Theta ')\!\models \! b_1\lbrack a/x\rbrack $
,
$\,\parallel b_1 \parallel _{\Lambda ,(b_2,\Theta )}=\,\parallel b_1\lbrack a/x\rbrack \parallel _{\Lambda ',(b\lbrack a/x\rbrack ,\Theta ')}$
,
$\Lambda '\!\models \! b_2\lbrack a/x\rbrack $
, and
$\,\parallel b_2 \parallel _{\Lambda }=\,\parallel b_2\lbrack a/x\rbrack \parallel _{\Lambda '}$
. Hence
$\,\parallel b_1\lbrack a/x\rbrack \parallel _{\Lambda ',(b\lbrack a/x\rbrack ,\Theta ')}=[y:\bar {c}_1]\bar {c}_2$
. Note that this implies that
$x\notin {{FV}}([y:\bar {c}_1]\bar {c}_2)$
. We can calculate as follows:
$$ \begin{align*} &\,\parallel \Lambda \parallel_{}\vdash\,\,\parallel b_2 \parallel_{\Lambda}{{}\cdot\!{\!}\!\leq{}}\bar{c}_1\\ \Rightarrow_{(\text{Inductive hypothesis})}&\,\parallel \Lambda \parallel_{}\vdash\,\,\parallel b_2\lbrack a/x\rbrack \parallel_{\Lambda'}{{}\cdot\!{\!}\!\leq{}}\bar{c}_1\\ \Rightarrow_{(\parallel\Lambda\parallel_{}=\parallel\Lambda\parallel_{}')}&\,\parallel \Lambda' \parallel_{}\vdash\,\,\parallel b_2\lbrack a/x\rbrack \parallel_{\Lambda'}{{}\cdot\!{\!}\!\leq{}}\bar{c}_1. \end{align*} $$
Therefore by definition of norming
$\,\parallel (b_1\,b_2) \parallel _{\Lambda ,\Theta }=\bar {c}_2=\,\parallel (b_1\,b_2)\lbrack a/x\rbrack \parallel _{\Lambda ',\Theta '}$
. Conversely if
$\Lambda ',\Theta '\!\models \! b\lbrack a/x\rbrack $
an analogous argument applies.
As a consequence reduction is preserving norms.
Proposition 21 (Reduction preserves norms).
$\Gamma \!\models \! a$
and
$a\to ^* b$
imply
$\Gamma \!\models \! b$
and
$\,\parallel a \parallel _{\Gamma }=\,\parallel b \parallel _{\Gamma }$
.
Proof. It is obviously sufficient to show the property for single-step reduction (Definition 4) which we do here by induction on the definition of single-step reduction. The interesting case is the axiom
$\beta $
: We have
$a=([x:a_1]a_2\;a_3)$
,
$b=a_2\lbrack a_3/x\rbrack $
. By definition of norming
$\,\parallel ([x:a_1]a_2\:a_3) \parallel _{\Gamma }=\,\parallel a_2 \parallel _{\Gamma ,x:= a_3}$
since
$\,\parallel [x:a_1]a_2 \parallel _{\Gamma ,a_3}=[x:\,\parallel a_1 \parallel _{\Gamma }]\,\parallel a_2 \parallel _{\Gamma ,x:= a_3}$
. By Proposition 20 with
$\Lambda _1=\Gamma $
,
$\Lambda _2=()$
,
$\Theta =()$
,
$x=x$
,
$a=a_3$
, and
$b=a_2$
we obtain
$\,\parallel a_2 \parallel _{\Gamma ,x:= a_3}=\,\parallel a_2\lbrack a_3/x\rbrack \parallel _{\Gamma }$
. The structural cases are straightforward, where rule abs
$_1$
requires a lemma that expressions with identical norms can be exchanged in extended contexts.
We now come to the property that all valid expressions are normable which is an important step in our proof of strong normalisation. Unfortunately, the non-compositional definition style of norming precludes a direct inductive argument. Instead, we need to bridge the different definitional structures of typing and norming. This is achieved by assigning a set of pairs
$(\Lambda ,\Theta )$
, the instantiation set
$\mathbb {I}_{\Gamma \vdash \, a:b}$
(see Definition 13) to a typing
$\Gamma \!\vdash \! a:b$
and then prove two properties about this set:
-
• Proposition 25:
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \vdash \, a:b}$
implies
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel b \parallel _{\Lambda ,\Theta }$
. -
• Proposition 28:
$(\Lambda ,())\in \mathbb {I}_{\Gamma \vdash \, a:b}$
for all
$\Lambda :\Gamma $
.
Propositions 25 and 28 state that instantiation sets are correct and complete in the sense that they characterize generalized inclusions and that they contain empty elimination lists. As an easy consequence of these properties
$\Gamma \!\vdash \! a$
implies
$\Gamma \!\models \! a$
(Proposition 29). Proposition 28 introduces an extension of typing.
Definition 12. Context typing
$\Lambda :\Gamma $
is defined by
${{dom}}(\Lambda )={{dom}}(\Gamma )$
,
$\Lambda (x)=\Gamma (x)$
for all
$x\in {{dom}_:}(\Lambda )$
, and
$\Gamma \!\vdash \!\Lambda (x):\Gamma (x)$
for all
$x\in {{dom}_{:=}}(\Lambda )$
.
Context typing illustrates the rationale of instantiation sets, i.e., to take a typing
$\Gamma \!\vdash \! a:b$
and build extended contexts
$\Lambda $
which have definitions satisfying the declarations from
$\Gamma $
. When reading the following definition keep in mind that the only rules introducing declarations in a context are start and weak.
Definition 13 (Instantiation sets).
The functions
$\mathbb {I}_{\Gamma \vdash \, a:b}$
,
$\mathbb {I}_{\Gamma \vdash \, a\leq b}$
,
$\mathbb {I}_{\Gamma \vdash \, a<\tau _{n}}$
each assign a set of pairs
$(\Lambda ,\Theta )$
to a typing
$\Gamma \!\vdash \! a:b$
, an inclusion
$\Gamma \!\vdash \! a\leq b$
, and a
$\tau _{}$
-inclusion
$\Gamma \!\vdash \! a<\tau _{n}$
. The recursive definition of these functions is structured according to the rules in Table 1:
Definition of
$\mathbb {I}_{\Gamma \,\vdash \, a:b}:$
-
• ax:
$\mathbb {I}_{\,\vdash \,\tau _{n}:\tau _{n}}$
consists of all
$((),\Theta )$
. -
• start:
$\mathbb {I}_{\Gamma ,x:a\,\vdash \, x:a}$
consists of all
$((\Lambda ,x:a),\Theta )$
where
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \,\vdash \, a:b}$
and all
$((\Lambda ,x\!:=\! c),\Theta )$
where
$\Gamma \!\vdash \! c:a$
and
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \,\vdash \, c:a}$
. -
• weak:
$\mathbb {I}_{\Gamma ,x:c\,\vdash \, a:b}$
consists of all
$((\Lambda ,x:c),\Theta )$
where
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \,\vdash \, a:b}$
and of all
$((\Lambda ,x\!:=\! d),\Theta )$
where
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \,\vdash \, a:b}$
,
$\Gamma \!\vdash \! d:c$
, and
$(\Lambda ,())\in \mathbb {I}_{\Gamma \,\vdash \, d:c}$
. -
• conv:
$\mathbb {I}_{\Gamma \,\vdash \, a:c}$
consists of all
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \,\vdash \, a:b}$
where
$b=_{\lambda } c$
. -
• inc:
$\mathbb {I}_{\Gamma \,\vdash \, a:c}$
consists of all
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \,\vdash \, a:b}\cap \mathbb {I}_{\Gamma \,\vdash \, b\leq c}$
. -
• abs:
$\mathbb {I}_{\Gamma \,\vdash \,[x:a]b:[x:a]c}$
consists of all
$(\Lambda ,())$
where
$((\Lambda ,x:a),())\in \mathbb {I}_{\Gamma ,x:a\,\vdash \, b:c}$
and of all
$(\Lambda ,(d,\Theta ))$
where
$((\Lambda ,x\!:=\! d),\Theta )\in \mathbb {I}_{\Gamma ,x:a\,\vdash \, b:c}$
. -
• appl:
$\mathbb {I}_{\Gamma \,\vdash \,(a\,b):d\lbrack b/x\rbrack }$
consists of all
$(\Lambda ,\Theta )$
where
$(\Lambda ,(b,\Theta ))\in \mathbb {I}_{\Gamma \,\vdash \, a:[x:c]d}$
and
$(\Lambda ,())\in \mathbb {I}_{\Gamma \,\vdash \, b:c}$
.
Definition of
$\mathbb {I}_{\Gamma \,\vdash \, a\leq b}:$
-
• refl
$_{\leq }$
:
$\mathbb {I}_{\Gamma \,\vdash \, a\leq a}$
consists of all
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \,\vdash \, a:b}$
where
$\Gamma \!\vdash \! a:b$
. -
• emb
$_{\leq }$
:
$\mathbb {I}_{\Gamma \,\vdash \, a\leq \tau _{n}}$
consists of all
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \,\vdash \, a<\tau _{n}}$
. -
• abs
$_{\leq }: \mathbb {I}_{\Gamma \,\vdash \,[x:a]b\leq [x:a]c}$
consists of all
$(\Lambda ,())\in \mathbb {I}_{\Gamma ,x:a\,\vdash \, b\leq c}$
and of all
$(\Lambda ,(d,\Theta ))$
where
$((\Lambda ,x\!:=\! d),\Theta )\in \mathbb {I}_{\Gamma ,x:a\,\vdash \, b\leq c}$
.
Definition of
$\mathbb {I}_{\Gamma \,\vdash \, a<\tau _{n}}:$
-
• ord
$_<$
:
$\mathbb {I}_{\Gamma \,\vdash \,\tau _{m}<\tau _{n}}$
consists of all
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \vdash \,\tau _{m}:a}\cap \mathbb {I}_{\Gamma \vdash \,\tau _{n}:b}$
. -
• typ
$_<$
:
$\mathbb {I}_{\Gamma \,\vdash \, a<\tau _{n}}$
consists of all
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \,\vdash \, a:b}\cap \mathbb {I}_{\Gamma \,\vdash \, b<\tau _{n}}$
. -
• abs
$_<$
:
$\mathbb {I}_{\Gamma \,\vdash \,[x:a]b<\tau _{n}}$
consists of all
$(\Lambda ,())\in \mathbb {I}_{\Gamma ,x:a\,\vdash \, b<\tau _{n}}$
and of all
$(\Lambda ,(d,\Theta ))$
where
$((\Lambda ,x\!:=\! d),\Theta )\in \mathbb {I}_{\Gamma ,x:a\,\vdash \, b<\tau _{n}}$
.
The rules start and weak introduce recursive references to instantiation sets of typing statements which do not appear in the premises of the corresponding rule in Table 1. Since these references are always using the reduced context they do not lead to an infinite recursion. In order to show Proposition 25 we need some properties of generalized inclusion on norms (see Table 2). We begin with decomposition properties some of which strengthen existing properties for typing (Proposition 10) and inclusion (Proposition 6).
Proposition 22 (Decomposition of generalized inclusion on norms).
-
(i)
$\bar {\Gamma }\!\vdash \!\tau _{m}{{}\cdot \!{\!}\!\leq {}}\bar {b}$
for some m implies
$\bar {b}=\tau _{n}$
for some n. -
(ii)
$\bar {\Gamma }\!\vdash \! x{{}\cdot \!{\!}\!\leq {}}\bar {b}$
implies
$\bar {b}=x$
, or
$\bar {b}=\tau _{m}$
for some m, or
$\bar {\Gamma }\!\vdash \! x:\bar {b}$
. -
(iii) If
$\bar {\Gamma }\!\vdash \!\bar {a}{{}\cdot \!{\!}\!\leq {}}[x:\bar {b}_1]\bar {b}_2$
and
$\bar {a}\notin \mathcal {V}$
then
$\bar {a}=[x:\bar {b}_1]\bar {c}$
for some
$\bar {c}$
where
$\bar {\Gamma },x:\bar {b}_1\!\vdash \!\bar {c}{{}\cdot \!{\!}\!\leq {}}\bar {b}_2$
. -
(iv) If
$\bar {\Gamma }\!\vdash \![x:\bar {a}_1]\bar {a}_2{{}\cdot \!{\!}\!\leq {}}\bar {b}$
then either
$\bar {b}=\tau _{m}$
for some m or
$\bar {b}=[x:\bar {a}_1]\bar {c}$
for some
$\bar {c}$
where
$\bar {\Gamma },x:\bar {a}_1\!\vdash \!\bar {a}_2{{}\cdot \!{\!}\!\leq {}}\bar {c}$
.
Proof. For (i) the property follows from 12, for (
$ii$
)
$\bar {\Gamma }\!\vdash \! x\leq \bar {b}$
can only be introduced by rules refl
$_{\leq }$
and emb
$_{\leq }$
.
(
$iii$
): If
$\bar {\Gamma }\!\vdash \!\bar {a}\leq [x:\bar {b}_1]\bar {b}_2$
the property follows from Proposition 6(
$ii$
). If
$\bar {\Gamma }\!\vdash \!\bar {a}:[x:\bar {b}_1]\bar {b}_2$
then since
$\bar {a}\notin \mathcal {V}$
and (i) it can only be a universal abstraction and therefore by Proposition 10(
$iv$
) we know that
$\bar {a}=[x:\bar {b}_1]\bar {c}$
, for some
$\bar {c}$
where
$\bar {\Gamma },x:\bar {b}_1\!\vdash \!\bar {c}:\bar {b}_2$
which implies (
$iii$
).
(
$iv$
): If
$\bar {\Gamma }\!\vdash \![x:\bar {a}_1]\bar {a}_2\leq \bar {b}$
the property follows from Proposition 6(
$iii$
). Otherwise, if
$\bar {\Gamma }\!\vdash \![x:\bar {a}_1]\bar {a}_2:\bar {b}$
then by Proposition 10(
$iii$
)
$\bar {\Gamma },x:\bar {a}_1\!\vdash \!\bar {a}_2:\bar {d}$
for some
$\bar {d}$
where
$\bar {\Gamma }\!\vdash \![x:\bar {a}_1]\bar {d}\leq \bar {b}$
. By Proposition 6(
$iii$
)
$\bar {b}=\tau _{m}$
for some m or
$\bar {b}=[x:\bar {a}_1]\bar {c}$
for some
$\bar {c}$
where
$\bar {\Gamma },x:\bar {a}_1\!\vdash \!\bar {d}\leq \bar {c}$
. The first case is obvious, in the second case by rule inc
$\bar {\Gamma },x:\bar {a}_1\!\vdash \! \bar {a}_2:\bar {c}$
which implies (
$iv$
).
While typing and therefore generalized inclusion is not transitive, a restricted property is sufficient.
Proposition 23 (Extension of generalized inclusion on norms).
If
$\bar {\Gamma }\!\vdash \!\bar {a}{{}\cdot \!{\!}\!\leq {}}\bar {b}$
then
$\bar {\Gamma }\!\vdash \!\bar {b}\leq \bar {c}$
implies
$\bar {\Gamma }\!\vdash \!\bar {a}{{}\cdot \!{\!}\!\leq {}}\bar {c}$
, and
$\bar {\Gamma }\!\vdash \!\bar {b}<\tau _{n}$
implies
$\bar {\Gamma }\!\vdash \!\bar {a}<\tau _{n}$
.
Proof. If
$\bar {\Gamma }\!\vdash \!\bar {a}\leq \bar {b}$
the first property follows from Proposition 15 and the second one from Proposition 14. If
$\bar {\Gamma }\!\vdash \!\bar {a}:\bar {b}$
the first property follows follows from rule inc and the second one from rule typ
$_<$
.
Furthermore we need a simple operator to apply elimination lists to norms.
Definition 14. The partial elimination function
$\bar {a}[\Theta ]$
applies an elimination list to a norm. It is recursively defined by
$\tau _{n}[\Theta ]=\tau _{n}$
,
$([x:\bar {a}]\bar {b})[c,\Theta ]=\bar {b}[\Theta ]$
.
True prefixes of elimination lists do not eliminate to variables.
Proposition 24 (Basic elimination property).
Let
$\Theta =(\Theta _1,\Theta _2)$
for some
$\Theta _1$
and
$\Theta _2$
where
$\Theta _2\neq ()$
: If
$\Lambda ,\Theta \!\models \! a$
then
$\,\parallel a \parallel _{\Lambda ,\Theta }[\Theta _1]$
is defined and
$\,\parallel a \parallel _{\Lambda ,\Theta }[\Theta _1]\notin \mathcal {V}$
.
Proof. Induction on the definition of
$\,\parallel a \parallel _{\Lambda ,\Theta }$
. The interesting case is
$a=(a_1\;a_2)$
and therefore
$\,\parallel a \parallel _{\Lambda ,\Theta }=\bar {d}$
for some
$\bar {d}$
where
$\,\parallel a_1 \parallel _{\Lambda ,(a_2,\Theta )}=[x:\bar {c}]\bar {d}$
. By inductive hypothesis
$\,\parallel a_1 \parallel _{\Lambda ,(a_2,\Theta )}[a_2,\Theta _1]=\bar {d}[\Theta _1]\notin \mathcal {V}$
.
Now we can show that instantiation sets are correct in the sense that they describe generalized inclusions.
Proposition 25 (Instantiation sets and generalized inclusion).
If
$\Gamma \!\vdash \! a:b$
and
$(\Lambda ,\Theta ) \in \mathbb {I}_{\Gamma \vdash \, a:b}$
then
$\!\models \!\Lambda $
,
$(\Lambda ,\Theta )\!\models \! a$
,
$(\Lambda ,\Theta )\!\models \! b$
, and
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel b \parallel _{\Lambda ,\Theta }$
.
Proof. We show the following three properties: (i) if
$\Gamma \!\vdash \! a:b$
and
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \vdash \, a:b}$
then
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel b \parallel _{\Lambda ,\Theta }$
, (
$ii$
) if
$\Gamma \!\vdash \! a\leq b$
and
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \vdash \, a\leq b}$
then
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }\leq \,\parallel b \parallel _{\Lambda ,\Theta }$
, and (
$iii$
) if
$\Gamma \!\vdash \! a<\tau _{n}$
and
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \vdash \, a<\tau _{n}}$
then
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }<\tau _{n}$
. In each case we also show that all normings are defined. The properties are shown by simultaneous induction on the definition of instantiation sets for typing, inclusion, and
$\tau _{}$
-inclusion.
(i): For rule ax obviously for all n we have
$\,\parallel \tau _{n} \parallel _{\Theta }=\tau _{n}$
and
$\!\vdash \!\tau _{n}{{}\cdot \!{\!}\!\leq {}}\tau _{n}$
. The case of rule weak follows from the inductive hypothesis and a simple weakening argument.
Rule start: According to the definition of
$\mathbb {I}_{\Gamma ,x:a\,\vdash \, x:a}$
there are two cases: (1):
$\Lambda =(\Lambda ',x:a)$
where
$(\Lambda ',\Theta )\in \mathbb {I}_{\Gamma \vdash \, a:b}$
. By inductive hypothesis
$\!\models \!\Lambda '$
and
$(\Lambda ',\Theta )\!\models \! a$
and therefore obviously
$\!\models \!\Lambda $
. If
$\Theta =()$
then
$\,\parallel x \parallel _{\Lambda ,\Theta }=x$
. Obviously
$\,\parallel \Lambda \parallel _{}=(\,\parallel \Lambda ' \parallel _{},x:\,\parallel a \parallel _{\Lambda '})\vdash \, x:\,\parallel a \parallel _{\Lambda '}=\,\parallel a \parallel _{\Lambda }$
. If
$\Theta \neq ()$
then
$\,\parallel x \parallel _{\Lambda ,\Theta }=\,\parallel a \parallel _{\Lambda ,\Theta }$
. Either way, by definition of generalized inclusion
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel x \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel a \parallel _{\Lambda ,\Theta }$
. (2):
$\Lambda =(\Lambda ',x\!:=\! c)$
where
$\Gamma \!\vdash \! c:a$
and
$(\Lambda ',\Theta )\in \mathbb {I}_{\Gamma \vdash \, c:a}$
. By inductive hypothesis
$\!\models \!\Lambda '$
,
$(\Lambda ',\Theta )\!\models \! c$
,
$(\Lambda ',\Theta )\!\models \! a$
, and
$\,\parallel \Lambda ' \parallel _{}\vdash \,\,\parallel c \parallel _{\Lambda ',\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel a \parallel _{\Lambda ',\Theta }$
. Hence obviously
$\!\models \!\Lambda $
. Since
$\,\parallel \Lambda \parallel _{}=\,\parallel \Lambda ' \parallel _{}$
,
$\,\parallel x \parallel _{\Lambda ,\Theta }=\,\parallel c \parallel _{\Lambda ',\Theta }$
, and
$\,\parallel a \parallel _{\Lambda ,\Theta }=\,\parallel a \parallel _{\Lambda ',\Theta }$
we obtain
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel x \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel a \parallel _{\Lambda ,\Theta }$
.
Rule conv: Members of
$\mathbb {I}_{\Gamma \vdash \, a:c}$
are
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \vdash \, a:b}$
where
$b=_{\lambda } c$
. By inductive hypothesis
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel b \parallel _{\Lambda ,\Theta }$
where all three norms are defined. By Propositions 1 and 21
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel c \parallel _{\Lambda ,\Theta }$
.
Rule inc: Members of
$\mathbb {I}_{\Gamma \vdash \, a:c}$
are
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \vdash \, a:b}\cap \mathbb {I}_{\Gamma \vdash \, b\leq c}$
. By inductive hypothesis of (i) and (
$ii$
)
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel b \parallel _{\Lambda ,\Theta }$
and
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b \parallel _{\Lambda ,\Theta }\leq \,\parallel c \parallel _{\Lambda ,\Theta }$
where all norms are defined. By Proposition 23 it follows that
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel c \parallel _{\Lambda ,\Theta }$
.
Rule abs: This case can be shown by a case distinction in a style similar to rule start and not requiring any auxiliary propositions.
Rule appl: Members of
$\mathbb {I}_{\Gamma \vdash \,(a\,b):d\lbrack b/x\rbrack }$
are
$(\Lambda ,(b,\Theta ))\in \mathbb {I}_{\Gamma \vdash \, a:[x:c]d}$
and
$(\Lambda ,())\in \mathbb {I}_{\Gamma \,\vdash \, b:c}$
. We have to show that
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel (a\,b) \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel d\lbrack b/x\rbrack \parallel _{\Lambda ,\Theta }$
. By inductive hypothesis
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,(b,\Theta )}{{}\cdot \!{\!}\!\leq {}}\,\parallel [x:c]d \parallel _{\Lambda ,(b,\Theta )}=[x:\,\parallel c \parallel _{\Lambda }]\,\parallel d \parallel _{(\Lambda ,x:= b),\Theta } =_{\text {(Proposition }{20})} [ x:\,\parallel c \parallel _{\Lambda }]\,\parallel d\lbrack b/x\rbrack \parallel _{\Lambda ,\Theta }$
. Using Proposition 24 with
$\Theta _1=()$
and
$\Theta _2=(b,\Theta )$
we can apply Proposition 22(
$iii$
) to obtain
$\,\parallel a \parallel _{\Lambda ,(b,\Theta )}=[x:\,\parallel c \parallel _{\Lambda }]\bar {e}$
for some
$\bar {e}$
where
$\,\parallel \Lambda \parallel _{}\vdash \,\bar {e}{{}\cdot \!{\!}\!\leq {}}\,\parallel d\lbrack b/x\rbrack \parallel _{\Lambda ,\Theta }$
. Since by inductive hypothesis
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b \parallel _{\Lambda }{{}\cdot \!{\!}\!\leq {}}\,\parallel c \parallel _{\Lambda }$
, by definition of norming
$\,\parallel (a\,b) \parallel _{\Lambda ,\Theta }=\bar {e}$
. This implies
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel (a\,b) \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel d\lbrack b/x\rbrack \parallel _{\Lambda ,\Theta }$
.
(
$ii$
): For rules refl
$_{\leq }$
and emb
$_{\leq }$
the property follows from the inductive hypothesis. For rule abs
$_{\leq }$
the argument is similar to the rule start in (i).
(
$iii$
): For rule ord
$_<$
the property follows from the inductive hypothesis, for rule typ
$_<$
one additionally needs Proposition 23. For rule abs
$_<$
the argument is similar to the rule start in (i).
In order to show that instantiation sets are complete (Proposition 28) we need a property involving elimination and generalized inclusion
Proposition 26 (Elimination and generalized inclusion (1)).
If
$\bar {\Gamma }\vdash \,\bar {a}{{}\cdot \!{\!}\!\leq {}}\bar {b}$
and if
$\bar {a}[\Theta ]$
is defined then
$\bar {b}[\Theta ]$
is defined and
$\bar {\Gamma }\!\vdash \!\bar {a}[\Theta ]{{}\cdot \!{\!}\!\leq {}}\bar {b}[\Theta ]$
.
Proof. We show the following three properties: (i) If
$\bar {\Gamma }\!\vdash \!\bar {a}:\bar {b}$
and
$\bar {a}[\Theta ]$
is defined then
$\bar {b}[\Theta ]$
is defined and
$\bar {\Gamma }\!\vdash \!\bar {a}[\Theta ]:\bar {b}[\Theta ]$
, (
$ii$
) if
$\bar {\Gamma }\!\vdash \!\bar {a}\leq \bar {b}$
and
$\bar {a}[\Theta ]$
is defined then
$\bar {b}[\Theta ]$
is defined and
$\bar {\Gamma }\!\vdash \!\bar {a}[\Theta ]\leq \bar {b}[\Theta ]$
, and (
$iii$
) if
$\bar {\Gamma }\!\vdash \!\bar {a}<\tau _{n}$
and
$\bar {a}[\Theta ]$
is defined then
$\bar {\Gamma }\!\vdash \!\bar {a}[\Theta ]<\tau _{n}$
. The main property is a direct consequence of (i) and (
$ii$
). The proof is by an obvious simultaneous induction on the three relations not requiring further properties. For example consider
$(i)$
and rule abs: We have
$\bar {a}=[x:\bar {a}_1]\bar {a}_2$
and
$\bar {b}=[x:\bar {a}_1]\bar {b}_2$
where
$\bar {\Gamma },x:\bar {a}_1\!\vdash \!\bar {a}_2:\bar {b}_2$
. The nontrivial case is
$\Theta =(c,\Theta ')$
for some c,
$\Theta '$
. Obviously if
$\bar {a}[\Theta ]$
is defined then
$\bar {a}_2[\Theta ']$
is defined and by inductive hypothesis
$\bar {b}_2[\Theta ']$
is defined and
$\bar {\Gamma },x:\bar {a}_1\!\vdash \!\bar {a}_2[\Theta ']:\bar {b}_2[\Theta ']$
which obviously implies
$\bar {\Gamma }\!\vdash \!\bar {a}[\Theta ]:\bar {b}[\Theta ]$
.
Furthermore we need a property about extending instantiation sets.
Proposition 27 (Extension of instantiation sets).
Let
$S=\mathbb {I}_{\Gamma \vdash \, a:b}$
,
$S=\mathbb {I}_{\Gamma \vdash \, a\leq b}$
, or
$S=\mathbb {I}_{\Gamma \vdash \, a<\tau _{n}}$
, and assume
$\Lambda \!\models \! b_1$
: (
$C_1$
)Footnote
3
If
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }\![\Theta ]{{}\cdot \!{\!}\!\leq {}}[y:\bar {b}_1]\bar {b}_2$
where
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b_1 \parallel _{\Lambda }{{}\cdot \!{\!}\!\leq {}}\bar {b}_1$
and
$y\neq x$
, or (
$C_2$
) if
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }\![\Theta ]=\tau _{m}$
then
$(\Lambda ,(\Theta ,b_1))\in S$
.
Proof. The proof is by induction on the definition of instantiation sets. We begin with the case
$S=\mathbb {I}_{\Gamma \vdash \, a:b}$
.
ax: We have
$\Lambda =()$
and
$a=b=\tau _{n}$
. Obviously
$\,\parallel \tau _{n} \parallel _{\Theta }\![\Theta ]=\tau _{n}[\Theta ]=\tau _{n}$
and by definition of
$\mathbb {I}_{\Gamma \vdash \,\tau _{n}:\tau _{n}} ((),(\Theta ,b_1))\in S$
.
start: Assume that (
$C_1$
)
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma ,x:a\vdash \, x:a}$
and
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel x \parallel _{\Lambda ,\Theta }\![\Theta ]{{}\cdot \!{\!}\!\leq {}}[y:\bar {b}_1]\bar {b}_2$
where
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b_1 \parallel _{\Lambda }{{}\cdot \!{\!}\!\leq {}}\bar {b}_1$
where
$y\neq x$
or that (
$C_2$
)
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel x \parallel _{\Lambda ,\Theta }\![\Theta ]=\tau _{m}$
. In each case we show
$(\Lambda ,(\Theta ,b_1))\in \mathbb {I}_{\Gamma ,x:a\vdash \, x:a}$
. By definition of
$\mathbb {I}_{\Gamma ,x:a\vdash \, x:a}$
there are two cases:
-
•
$\Lambda =(\Lambda ',x:a)$
where
$(\Lambda ',\Theta )\in \mathbb {I}_{\Gamma \vdash \, a:b}$
. There are two subcases:If
$\Theta =()$
then by definition of norming and the elimination function
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel x \parallel _{\Lambda }\![()]=x:\,\parallel a \parallel _{\Lambda '}\![()]$
. Since
$x\neq \tau _{m}$
, (
$C_1$
) must be true. Since
$\,\parallel \Lambda \parallel _{}\vdash \, x\leq [y:\bar {b}_1]\bar {b}_2$
would contradict Proposition 6(
$ii$
) we have
$\,\parallel \Lambda \parallel _{}\vdash \, x:[y:\bar {b}_1]\bar {b}_2$
. By Proposition 10(
$ii$
) and since
$x\notin {{FV}}(a)\cup {{FV}}([y:\bar {b}_1]\bar {b}_2) \,\parallel \Lambda ' \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda '}\leq [y:\bar {b}_1]\bar {b}_2$
. Hence by inductive hypothesis
$(\Lambda ',b_1)\in \mathbb {I}_{\Gamma \vdash \, a:b}$
and therefore
$(\Lambda ,b_1)\in \mathbb {I}_{\Gamma ,x:a\vdash \, x:a}$
.If
$\Theta \neq ()$
then by definition of norming
$\,\parallel \Lambda ' \parallel _{}\vdash \,\,\parallel x \parallel _{\Lambda ',\Theta }\![\Theta ]=\,\parallel a \parallel _{\Lambda ',\Theta }\![\Theta ]$
. Hence we can apply the inductive hypothesis in case of both (
$C_1$
) and (
$C_2$
) to obtain
$(\Lambda ',(\Theta ,b_1))\in \mathbb {I}_{\Gamma \vdash \, a:b}$
and therefore
$(\Lambda ,(\Theta ,b_1))\in \mathbb {I}_{\Gamma ,x:a\vdash \, x:a}$
. -
•
$\Lambda =(\Lambda ',x\!:=\! c)$
where
$(\Lambda ',\Theta )\in \mathbb {I}_{\Gamma \vdash \, c:a}$
. By Proposition 25 we know that
$\,\parallel \Lambda ' \parallel _{}\vdash \,\,\parallel c \parallel _{\Lambda ',\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel a \parallel _{\Lambda ',\Theta }$
. By definition of norming
$\,\parallel \Lambda ' \parallel _{}\vdash \,\,\parallel x \parallel _{\Lambda ',\Theta }=\,\parallel c \parallel _{\Lambda ',\Theta }$
. Hence we can apply the inductive hypothesis in case of both (
$C_1$
) and (
$C_2$
) to obtain
$(\Lambda ',(\Theta ,b_1))\in \mathbb {I}_{\Gamma \vdash \, c:a}$
and therefore
$(\Lambda ,(\Theta ,b_1))\in \mathbb {I}_{\Gamma ,x:a\vdash \, x:a}$
.
weak, conv: Follows from the definition of norming, instantiation sets, and the inductive hypothesis not requiring further properties.
abs: Follows from the definition of norming, instantiation sets, the inductive hypothesis, and 22(
${iii}$
,
$iv$
).
inc:
$\mathbb {I}_{\Gamma \vdash \, a:c}$
consists of all
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \vdash \, a:b}\cap \mathbb {I}_{\Gamma \vdash \, b\leq c}$
. Assume that (
$C_1$
)
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }\![\Theta ]{{}\cdot \!{\!}\!\leq {}}[x:\bar {b}_1]\bar {b}_2$
where
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b_1 \parallel _{\Lambda }{{}\cdot \!{\!}\!\leq {}}\bar {b}_1$
or that (
$C_2$
)
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }\![\Theta ]=\tau _{m}$
. By inductive hypothesis for
$\mathbb {I}_{\Gamma \vdash \, a:b} (\Lambda ,(\Theta ,b_1))\in \mathbb {I}_{\Gamma \vdash \, a:b}$
. Since
$(\Lambda ,\Theta )\in \mathbb {I}_{\Gamma \vdash \, a:b}$
by Proposition 25
$\Lambda ,\Theta \!\models \! b$
and
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel b \parallel _{\Lambda ,\Theta }$
. By Proposition 26
$\,\parallel b \parallel _{\Lambda ,\Theta }\![\Theta ]$
is defined and
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }\![\Theta ]{{}\cdot \!{\!}\!\leq {}}\,\parallel b \parallel _{\Lambda ,\Theta }\![\Theta ]$
.
Next we show that one of the two preconditions (
$C_1$
) or (
$C_2$
) is always valid when adapted to
$\Gamma \!\vdash \! b\leq c$
so that the inductive hypothesis for
$\mathbb {I}_{\Gamma \vdash \, b\leq c}$
can be applied. For this we consider the two assumed preconditions (
$C_1$
) and (
$C_2$
) of
$\Gamma \!\vdash \! a:c$
. In case of (
$C_1$
) we make a case distinction:
-
• If
$\,\parallel a \parallel _{\Lambda ,\Theta }\![\Theta ]\in \mathcal {V}$
then by Proposition 22(
$ii$
)
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }\![\Theta ]:[x:\bar {b}_1]\bar {b}_2$
. Furthermore from
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel b \parallel _{\Lambda ,\Theta }$
by Proposition 22(
$iv$
) we know that either
$\,\parallel b \parallel _{\Lambda ,\Theta }\![\Theta ]=\tau _{k}$
for some k, and then the inductive hypothesis for
$\mathbb {I}_{\Gamma \vdash \, b\leq c}$
can obviously be applied, or that
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda ,\Theta }\![\Theta ]:\,\parallel b \parallel _{\Lambda ,\Theta }\![\Theta ]$
and then by Proposition 18 there is a
$\bar {b}'=M_{\Lambda }(\,\parallel a \parallel _{\Lambda ,\Theta }\![\Theta ])$
where
$\,\parallel \Lambda \parallel _{}\vdash \,\bar {b}'\leq [y:\bar {b}_1]\bar {b}_2$
and
$\,\parallel \Lambda \parallel _{}\vdash \,\bar {b}'\leq \,\parallel b \parallel _{\Lambda ,\Theta }\![\Theta ]$
. Using Proposition 6(
$ii$
) followed by Proposition 6(
$iii$
)
$\,\parallel b \parallel _{\Lambda ,\Theta }\![\Theta ]=[y:\bar {b}_1]\bar {b}_2'$
for some
$\bar {b}_2'$
or
$\,\parallel b \parallel _{\Lambda ,\Theta }\![\Theta ]=\tau _{k}$
for some k. Hence the inductive hypothesis for
$\mathbb {I}_{\Gamma \vdash \, b\leq c}$
can also be applied. -
• If
$\,\parallel a \parallel _{\Lambda ,\Theta }\![\Theta ]\notin \mathcal {V}$
by Proposition 22(
$iii$
)
$\,\parallel \Lambda \parallel _{}\vdash \,\!\,\parallel a \parallel _{\Lambda ,\Theta }\![\Theta ]=[x:\bar {b}_1]\bar {a}_2$
for some
$\bar {a}_2$
. By Proposition 22(
$iv$
) either
$\,\parallel \Lambda \parallel _{}\vdash \,\!\,\parallel b \parallel _{\Lambda ,\Theta }\![\Theta ] = \tau _{k}$
for some k, or
$\,\parallel \Lambda \parallel _{}\vdash \,\!\,\parallel b \parallel _{\Lambda ,\Theta }\![\Theta ]=[x:\bar {b}_1]\bar {b}_2'$
for some
$\bar {b}_2'$
in both cases of which the inductive hypothesis for
$\mathbb {I}_{\Gamma \vdash \, b\leq c}$
can be applied.
In case of (
$C_2$
) by Proposition 22(i)
$\,\parallel b \parallel _{\Lambda ,\Theta }=\tau _{k}$
for some k and hence
$\,\parallel b \parallel _{\Lambda ,\Theta }\![\Theta ]=\tau _{k}$
and therefore the inductive hypothesis for
$\mathbb {I}_{\Gamma \vdash \, b\leq c}$
can be applied. In summary, in all cases the inductive hypothesis for
$\mathbb {I}_{\Gamma \vdash \, b\leq c}$
can be applied which implies
$(\Lambda ,(\Theta ,b_1))\in \mathbb {I}_{\Gamma \vdash \, b\leq c}$
and therefore
$(\Lambda ,(\Theta ,b_1))\in \mathbb {I}_{\Gamma \vdash \, a:c}$
.
appl: Assume that (
$C_1$
)
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel (a\,b) \parallel _{\Lambda ,\Theta }\![\Theta ]{{}\cdot \!{\!}\!\leq {}}[x:\bar {b}_1]\bar {b}_2$
and
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b_1 \parallel _{\Lambda }{{}\cdot \!{\!}\!\leq {}}\bar {b}_1$
or that (
$C_2$
)
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel (a\,b) \parallel _{\Lambda ,\Theta }\![\Theta ]=\tau _{m}$
. Since
$\Lambda ,\Theta \!\models \! (a\,b)$
we know that
$\Lambda ,(b,\Theta )\!\models \! a$
and
$\,\parallel a \parallel _{\Lambda ,(b,\Theta )}=[x:\bar {a}_1]\,\parallel (a\,b) \parallel _{\Lambda ,\Theta }$
for some
$\bar {a}_1$
. Hence
$\,\parallel (a\,b) \parallel _{\Lambda }\![\Theta ]=\,\parallel a \parallel _{\Lambda }\![b,\Theta ]$
and therefore by inductive hypothesis for
$\mathbb {I}_{\Gamma \vdash \, a:[x:c]d}$
we obtain
$(\Lambda ,(b,\Theta ,b_1))\in \mathbb {I}_{\Gamma \vdash \, a:[x:c]d}$
. By definition of instantiation sets
$(\Lambda ,(\Theta ,b_1))\in \mathbb {I}_{\Gamma \vdash \,(a\,b):d\lbrack b/x\rbrack }$
.
The case
$S=\mathbb {I}_{\Gamma \vdash \, a\leq b}$
can be shown by obvious arguments using the definition of norming, instantiation sets, and Proposition 22(
$iii$
,
$iv$
). For the case
$S=\mathbb {I}_{\Gamma \vdash \, a<\tau _{n}}$
: For rule ord
$_<$
since
$\,\parallel \tau _{m} \parallel _{\Lambda ,\Theta }\![\Theta ]=\tau _{m}$
by inductive hypothesis we know that
$(\Lambda ,(\Theta ,d))\in \mathbb {I}_{\Gamma \vdash \,\tau _{m}:a}$
. A similar argument can be made about
$\mathbb {I}_{\Gamma \vdash \,\tau _{n}:a}$
Rules typ
$_<$
and abs
$_<$
can be argued similar to rules inc and abs.
We can now show that instantiation sets are complete in the sense that they contain empty elimination lists.
Proposition 28 (Instantiation sets contain empty elimination lists).
If
$\Lambda :\Gamma$
(see Definition 12) and
$\Gamma \vdash \, a:b$
then
$(\Lambda ,())\in \mathbb {I}_{\Gamma \vdash \, a:b}$
.
Proof. Assume
$\Lambda :\Gamma $
. We show that (i) if
$\Gamma \vdash \, a:b$
then
$(\Lambda ,())\in \mathbb {I}_{\Gamma \vdash \, a:b}$
, (
$ii$
) if
$\Gamma \vdash \, a\leq b$
then
$(\Lambda ,())\in \mathbb {I}_{\Gamma \vdash \, a\leq b}$
, and (
$iii$
) if
$\Gamma \vdash \, a<\tau _{n}$
then
$(\Lambda ,())\in \mathbb {I}_{\Gamma \vdash \, a<\tau _{n}}$
. All parts are shown simultaneously by induction on the definition of instantiation sets. For property (i) the cases of rules ax and abs are obvious by definition. The case of conv follows directly from the inductive hypothesis for (i) and the case of inc follows directly from the inductive hypotheses for (i) and (
$ii$
).
Rule start: Assume that
$\Lambda :(\Gamma , x:a)$
: Obviously
$\Lambda =(\Lambda ',x:a)$
or
$\Lambda =(\Lambda ', x\!:=\!\ \mathrm{for\ some}\ c)$
where
$\Lambda ':\Gamma $
and
$\Gamma \!\vdash \! c:a$
. Hence, according to the definition of
$\mathbb {I}_{\Gamma ,x:a\,\vdash \, x:a}$
there are two cases: In the first case
$((\Lambda ',x:a),())\in \mathbb {I}_{\Gamma ,x:a\,\vdash \, x:a}$
following from
$(\Lambda ',())\in \mathbb {I}_{\Gamma \vdash \, a:b}$
. which follows from the inductive hypothesis for
$\Gamma \!\vdash \! a:b$
. Similar for the second case
$\Lambda =(\Lambda ',x\!:=\! c)$
. The case of rule weak can be shown by a case distinction similar to rule start.
Rule appl: Members of
$\mathbb {I}_{\Gamma \vdash \,(a\,b):d\lbrack b/x\rbrack }$
are pairs
$(\Lambda ,\Theta )$
where
$(\Lambda ,(b,\Theta ))\in \mathbb {I}_{\Gamma \vdash \, a:[x:c]d}$
and
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b \parallel _{\Lambda }{{}\cdot \!{\!}\!\leq {}}\,\parallel c \parallel _{\Lambda }$
. We show that
$(\Lambda ,())\in \mathbb {I}_{\Gamma \vdash \,(a\,b):d\lbrack b/x\rbrack }$
which follows from
$(\Lambda ,b)\in \mathbb {I}_{\Gamma \vdash \, a:[x:c]d}$
. By inductive hypothesis
$(\Lambda ,())\in \mathbb {I}_{\Gamma \vdash \, a:[x:c]d}$
. By Proposition 25 we know that
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel a \parallel _{\Lambda }{{}\cdot \!{\!}\!\leq {}}\,\parallel [x:c]d \parallel _{\Lambda }=[x:\,\parallel c \parallel _{\Lambda }]\bar {d}$
for some
$\bar {d}$
. Since
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b \parallel _{\Lambda }{{}\cdot \!{\!}\!\leq {}}\,\parallel c \parallel _{\Lambda }$
, by Proposition 27 with
$\Theta =()$
,
$S=\mathbb {I}_{\Gamma \vdash \, a:[x:c]d}$
,
$b_1=b$
we know that
$(\Lambda ,b)\in \mathbb {I}_{\Gamma \vdash \, a:[x:c]d}$
.
For properties (
$ii$
) and (
$iii$
) all cases follow from the inductive hypothesis.
The previous results immediately imply that valid expression are normable.
Proposition 29 (Typing implies normability and norm inclusion).
For all
$\Gamma $
, a:
$\Gamma \!\vdash \! a$
implies
$\!\models \!\Gamma $
and
$\Gamma \!\models \! a$
.
6 Strong normalisation
We begin with a well-known strong normalization condition for applications.
Proposition 30 (Strong normalization condition).
Let
${\mathcal {S}_{}}\subseteq \mathcal {E}$
denote the set of expressions from which there is no infinite sequence of single-step reductions. If
$a,b\in {\mathcal {S}_{}}$
then
$(a\,b)\in {\mathcal {S}_{}}$
if
$a\to ^*[x:c_1]c_2$
implies
$c_2\lbrack b/x\rbrack \in {\mathcal {S}_{}}$
.
Proof. A simple analysis yields a proof by contradiction.
Inspired by this property, a common method to show strong normalisation is to define a notion of reducible expressions satisfying certain reducibility conditions suitable for inductive arguments both on type structure and on reduction length, to prove that all reducible expressions satisfy certain reducibility properties including strong normalisation, and then to prove that that all typable expressions are reducible [Reference Girard9, Reference Tait19]. As outlined in the introduction we will basically adopt this idea with some modifications for the system at hand inspired by the notions of norms and computable expressions as defined in language theoretical studies of Automath [Reference van Daalen8], see also [Reference van Benthem Jutting2]. First, in order to use inductive arguments based on norming we need to define a well-founded ordering on norms.
Definition 15 (Norm order).
The
$\tau _{n}$
-size
$\mathit {S}_{\bar {\Gamma }}^{(n)}(\bar {a})$
of a norm
$\bar {a}$
under norm context
$\bar {\Gamma }$
is defined recursively as follows:
$\mathit {S}_{\bar {\Gamma }}^{(n)}(\tau _{m})=1$
if
$n=m$
and
$0$
otherwise,
$\mathit {S}_{\bar {\Gamma }}^{(n)}(x)=\mathit {S}_{\bar {\Gamma }}^{(n)}(\bar {\Gamma }(x))$
if
$x\in {{dom}}(\bar {\Gamma })$
, and
$\mathit {S}_{\bar {\Gamma }}^{(n)}([x:\bar {a}]\bar {b})=\mathit {S}_{\bar {\Gamma }}^{(n)}(\bar {a})+\mathit {S}_{\bar {\Gamma },x:\bar {a}}^{(n)}(\bar {b})$
. The
$\tau _{}$
-size
$S_{\bar {\Gamma }}(\bar {a})$
of a norm
$\bar {a}$
under norm context
$\bar {\Gamma }$
is defined as the maximal number n with
$\mathit {S}_{\bar {\Gamma }}^{(n)}(\bar {a})>0$
. For norm context
$\bar {\Gamma }$
and norms
$\bar {a}$
,
$\bar {b}$
, norm order
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {b}$
is defined by the rules shown in Table 3.
Norm order and weak norm order.
The rules also introduce weak norm order
$\bar {\Gamma }\!\vdash \!\bar {a}\lesssim \bar {b}$
.
Note that abs
$_{\ll ,3}$
and abs
$_{\ll ,4}$
overlap, however they are consistent and in this formulation only two rules are needed. Furthermore either of the two rules obviously implies
$$\begin{align} \frac{\bar{\Gamma}\!\vdash\!\bar{a}\lesssim\bar{c}\quad\bar{\Gamma},x:\bar{a}\!\vdash\!\bar{b}\lesssim\bar{d}}{\bar{\Gamma}\!\vdash\![x:\bar{a}]\bar{b}\lesssim[x:\bar{c}]\bar{d}}. \end{align} $$
For readability we sometimes write
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {b}$
as
$\bar {\Gamma }\!\vdash \!\bar {b}\gg \bar {a}$
.
We begin with some basic relations between norm order and
$\tau _{}$
-size.
Proposition 31 (Norm order to τ-size).
If
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {b}$
then there is a k where
$\mathit {S}_{\bar {\Gamma }}^{(k)}(\bar {a})<\mathit {S}_{\bar {\Gamma }}^{(k)}(\bar {b})$
and
$\mathit {S}_{\bar {\Gamma }}^{(i)}(\bar {a})=\mathit {S}_{\bar {\Gamma }}^{(i)}(\bar {b})$
for all
$i>k$
. As a consequence
$S_{\bar {\Gamma }}(\bar {a})\leq S_{\bar {\Gamma }}(\bar {b})$
.
Proof. Induction on the definition of norm order. The index k which is obviously unique is called the discriminator. In case of rule start
$_{\ll }$
obviously
$k=n$
. For rule var
$_{\ll }\ k$
is the discriminator obtained from the inductive hypothesis. For rule abs
$_{\ll ,1}$
if
$\bar {a}=\bar {b}$
then obviously
$k=S_{\bar {\Gamma },x:\bar {a}}(\bar {c})$
otherwise obviously k is the maximum of the discriminator of
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {b}$
, which exists by inductive hypothesis, and
$S_{\bar {\Gamma },x:\bar {a}}(\bar {c})$
. Similar for rule abs
$_{\ll ,2}$
. For rule abs
$_{\ll ,3}$
by inductive hypothesis there is a discriminator l of
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {c}$
. If
$\bar {b}=\bar {d}$
then obviously
$k=l$
, otherwise, by inductive hypothesis there is a discriminator m for
$\bar {\Gamma },x:\bar {a}\!\vdash \!\bar {b}\ll \bar {d}$
and k is obviously the maximum of l and m. Similar for rule abs
$_{\ll ,4}$
. For the consequence obviously
$S_{\bar {\Gamma }}(\bar {a})<S_{\bar {\Gamma }}(\bar {b})$
if the discriminator equals the
$\tau _{}$
-size of
$\bar {b}$
and equality otherwise.
Proposition 32 (τ-Size to norm order).
If
$S_{\bar {\Gamma }}(\bar {a})<S_{\bar {\Gamma }}(\bar {b})$
then
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {b}$
.
Proof. Induction on the definition of
$S_{\bar {\Gamma }}(\bar {b})$
. The interesting case is
$\bar {b}=[x:\bar {b}_1]\bar {b}_1$
where
$S_{\bar {\Gamma }}(\bar {b})$
is the maximum of
$S_{\bar {\Gamma }}(\bar {b}_1)$
and
$S_{\bar {\Gamma },x:\bar {b}_1}(\bar {b}_2)$
. If
$S_{\bar {\Gamma }}(\bar {b})=S_{\bar {\Gamma }}(\bar {b}_1)$
then
$S_{\bar {\Gamma }}(\bar {a})<S_{\bar {\Gamma }}(\bar {b}_1)$
and hence by inductive hypothesis
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {b}_1$
. By rule abs
$_{\ll ,1}\ \bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {b}$
. Similar for
$S_{\bar {\Gamma }}(\bar {b})=S_{\bar {\Gamma },x:\bar {b}_1}(\bar {b}_2)$
.
Next we show that norm order is a proper basis for inductive arguments.
Proposition 33 (Norm order is well-founded).
Norm order is a well-founded relation, i.e., if
$\bar {\Gamma }\!\vdash \!\bar {a}$
then there is no infinite chain
$\bar {\Gamma }\!\vdash \!\bar {a}=\bar {a}_1\gg \bar {a}_2\gg \ldots $
.
Proof. The basic idea is to consider infinite norm order sequences starting from
$\bar {a}$
which satisfy a parametrized
$\tau _{}$
-size constraint
$C^{(n)}_{\bar {\Gamma }}(\bar {a})$
inspired by Proposition 31. Given an infinite chain
$\bar {\Gamma }\!\vdash \!\bar {a}=\bar {a}_1\gg \bar {a}_2\gg \ldots $
we define
$$\begin{align*}C^{(n)}_{\bar{\Gamma}}(\bar{a})\;\equiv\;\mathit{S}_{\bar{\Gamma}}^{(j)}(\bar{a})=\mathit{S}_{\bar{\Gamma}}^{(j)}(\bar{a}_i)\;\text{for all}\;i\geq 1\;\text{and all}\;j\;\text{where}\;n<j\leq S_{\bar{\Gamma}}(\bar{a}). \end{align*}$$
We show by induction on n that for all
$\bar {\Gamma }$
,
$\bar {a}$
with
$\bar {\Gamma }\!\vdash \!\bar {a}$
there is no infinite chain
$\bar {\Gamma }\!\vdash \!\bar {a}=\bar {a}_1\gg \bar {a}_2\gg \ldots $
for which
$C^{(n)}_{\bar {\Gamma }}(\bar {a})$
is valid. As a consequence this property holds for
$n=S_{\bar {\Gamma }}(\bar {a})$
, and since
$C^{(S_{\bar {\Gamma }}(\bar {a}))}_{\bar {\Gamma }}(\bar {a})$
is trivially true, there are no infinite chains at all.
The case
$n=0$
is obvious since otherwise
$\mathit {S}_{\bar {\Gamma }}^{(j)}(\bar {a})=\mathit {S}_{\bar {\Gamma }}^{(j)}(\bar {a}_2)$
for all
$j\leq S_{\bar {\Gamma }}(\bar {a})$
which violates Proposition 31. For the case
$n>0$
assume an infinite chain
$\bar {\Gamma }\!\vdash \!\bar {a}=\bar {a}_1\gg \bar {a}_2\gg \ldots $
with
$C^{(n)}_{\bar {\Gamma }}(\bar {a})$
, i.e.,
$\mathit {S}_{\bar {\Gamma }}^{(j)}(\bar {a})=\mathit {S}_{\bar {\Gamma }}^{(j)}(\bar {a}_i)$
for all
$i\geq 1$
and all j with
$n<j\leq S(\bar {a})$
. Obviously
$\mathit {S}_{\bar {\Gamma }}^{(n)}(\bar {a}_i)=\mathit {S}_{\bar {\Gamma }}^{(n)}(\bar {a})$
, for all
$i\geq 1$
is not possible since otherwise we would have an infinite sequence with
$\mathit {S}_{\bar {\Gamma }}^{(j)}(\bar {a})=\mathit {S}_{\bar {\Gamma }}^{(j)}(\bar {a}_i)$
for all
$i\geq 1$
and all j with
$n-1<j\leq S(a)$
, or in other words satisfying
$C^{(n-1)}_{\bar {\Gamma }}(\bar {a})$
, and therefore violating the inductive hypothesis. Hence there is an index
$i_0$
where
$\mathit {S}_{\bar {\Gamma }}^{(n)}(\bar {a})>\mathit {S}_{\bar {\Gamma }}^{(n)}(\bar {a}_{i_0})$
. By repeating this argument on the infinite sequence
${\bar {\Gamma }}\!\vdash \!\bar {a}_{i_0}\gg \bar {a}_{{i_0}+1}\gg \ldots $
we eventually reach an index
$i_h$
and infinite sequence
$\bar {\Gamma }\!\vdash \!\bar {a}_{i_h}\gg \bar {a}_{i_h+1}\gg \ldots $
where
$\mathit {S}_{\bar {\Gamma }}^{(n)}(\bar {a}_{i_h})=0$
. However this means that
$\mathit {S}_{\bar {\Gamma }}^{(n)}(\bar {a}_i)=0$
, for all
$i\geq i_h$
, or in other words satisfying
$C^{(n-1)}_{\bar {\Gamma }}(\bar {a}_{i_h})$
which violates the inductive hypothesis.
As a consequence, the following norm induction property is valid:
Proposition 34 (Norm induction).
If
$\Gamma \!\vdash \!\bar {a}_1$
then a property
$P_{\Gamma }(\bar {a}_1)$
is true if
$P_{\Gamma }(\bar {a}_2)$
for all
$\bar {a}_2$
with
$\,\parallel \Gamma \parallel _{}\vdash \,\bar {a}_1\gg \bar {a}_2$
implies
$P_{\Gamma }(\bar {a}_1)$
.
Proof. Note that the n-fold use of the inductive hypothesis implies a norm order sequence
$\bar {\Gamma }\!\vdash \!\bar {a}_1\gg \ldots \gg \bar {a}_n$
. By Proposition 33 the induction is well-founded.
In the following we note several basis properties involving (weak) norm order. They will be used for the single purpose to show that, under certain conditions, the set of computable expressions (Definition 16) exists (Proposition 44). They can be split into two parts: The first part is about norm order itself ending with Proposition 40, the second part is about norming and its relation to norm order, ending with Proposition 43. The proofs are a bit technical but essentially straightforward.
Proposition 35 (Weakening/Strengthening of (weak) norm order).
$\bar {\Gamma }\!\vdash \!\bar {b}\ll \bar {c}$
and
$\bar {\Gamma }\!\vdash \!\bar {a}$
imply
$\bar {\Gamma },x:\bar {a}\!\vdash \!\bar {b}\ll \bar {c}$
. If
$\bar {\Gamma },x:\bar {a}\!\vdash \!\bar {b}\ll \bar {c}$
and
$x\notin {FV}(\bar {b})$
then
$x\notin {FV}(\bar {c})$
and
$\bar {\Gamma }\!\vdash \!\bar {b}\ll \bar {c}$
. Similar for weak norm order.
Proof. Obvious inductive argument.
Proposition 36 (Left decomposition of weak norm order).
If
$\bar {\Gamma }\!\vdash \![x:\bar {a}]\bar {b}\lesssim \bar {c}$
then
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {c}$
and
$\bar {\Gamma },x:\bar {a}\!\vdash \!\bar {b}\ll \bar {c}$
.
Proof. If
$[x:\bar {a}]\bar {b}=\bar {c}$
,
$\bar {\Gamma }\!\vdash \!\bar {c}$
the property follows directly form rules abs
$_{\ll ,1}$
, abs
$_{\ll ,2}$
, and Proposition 35. The interesting case is
$\bar {\Gamma }\!\vdash \![x:\bar {a}]\bar {b}\ll \bar {c}$
which is shown by an obvious induction on the definition of
$\bar {\Gamma }\!\vdash \![x:\bar {a}]\bar {b}\ll \bar {c}$
.
Proposition 37 (Preservation of norm order).
If
$\bar {\Gamma }\!\vdash \!\bar {a}\lesssim \bar {b}$
and
$\bar {\Gamma },x:\bar {b}\!\vdash \!\bar {c}\ll \bar {d}$
then
$\bar {\Gamma },x:\bar {a}\!\vdash \!\bar {c}\ll \bar {d}$
. Furthermore under the same conditions
$\bar {\Gamma }\!\vdash \!\bar {c}\lbrack \bar {a}/x\rbrack \ll \bar {d}\lbrack \bar {a}/x\rbrack $
.
Proof. The property is obvious if
$\bar {a}=\bar {b}$
,
$\bar {\Gamma }\!\vdash \!\bar {a}$
. Otherwise we show the following more general property: Let
$\bar {\Gamma }_a=(\bar {\Gamma }_1,x:\bar {a},\bar {\Gamma }_2)$
and
$\bar {\Gamma }_b=(\bar {\Gamma }_1,x:\bar {b},\bar {\Gamma }_2)$
. If
$\bar {\Gamma }_1\!\vdash \!\bar {a}\ll \bar {b}$
and
$\bar {\Gamma }_b\!\vdash \!\bar {c}\ll \bar {d}$
then
$\bar {\Gamma }_a\!\vdash \!\bar {c}\ll \bar {d}$
. The proof is by induction on the definition of
$\bar {\Gamma }_b\!\vdash \!\bar {c}\ll \bar {d}$
: For rule start
$_{\ll }$
we have
$\bar {d}=\tau _{n}$
and obviously
$S_{\bar {\Gamma }_a}(\bar {c})\leq S_{\bar {\Gamma }_b}(\bar {c})<n$
. For rule var
$_{\ll }$
we have
$\bar {c}=y$
and
$\bar {\Gamma }_b\!\vdash \!\bar {\Gamma }_b(y)\lesssim \bar {d}$
. The case
$x=y$
is obvious, otherwise the property follows from the inductive hypothesis. For rule abs
$_{\ll ,1}$
we have
$\bar {d}=[y:\bar {d}_1]\bar {d}_2$
where
$y\neq x$
and
$\bar {\Gamma }_b\!\vdash \!\bar {c}\lesssim \bar {d}_1$
. If
$\bar {c}=\bar {d}_1$
then obviously
$\bar {\Gamma }_a\!\vdash \!\bar {c}\lesssim \bar {d}_1$
otherwise by inductive hypothesis
$\bar {\Gamma }_a\!\vdash \!\bar {c}\ll \bar {d}_1$
. In both cases by rule abs
$_{\ll ,1}\ \bar {\Gamma }_a\!\vdash \!\bar {c}\ll \bar {d}$
. Similar for rules abs
$_{\ll ,2}$
, abs
$_{\ll ,3}$
, and abs
$_{\ll ,4}$
. Under the same conditions, by an similar inductive argument we can show that
$\bar {\Gamma }_1,\bar {\Gamma }_2\lbrack a/x\rbrack \!\vdash \!\bar {c}\lbrack \bar {a}/x\rbrack \ll \bar {d}\lbrack \bar {a}/x\rbrack $
. With
$\bar {\Gamma }_1=\bar {\Gamma }$
,
$\bar {\Gamma }_2=()$
this implies
$\bar {\Gamma }\!\vdash \!\bar {c}\lbrack \bar {a}/x\rbrack \ll \bar {d}\lbrack \bar {a}/x\rbrack $
.
Proposition 38 (Transitivity of norm order).
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {b}$
and
$\bar {\Gamma }\!\vdash \!\bar {b}\ll \bar {c}$
imply
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {c}$
. As a consequence weak norm order is transitive as well.
Proof. First note that the consequence follows by an obvious case distinction. The main property is shown by induction on the definition of
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {b}$
. For rule start
$_{\ll }$
we have
$\bar {b}=\tau _{n}$
,
$S_{\bar {\Gamma }}(\bar {a})<n$
, and
$\bar {\Gamma }\!\vdash \!\tau _{n}\ll \bar {c}$
which by Proposition 31 implies
$n\leq S_{\bar {\Gamma }}(\bar {c})$
. From
$S_{\bar {\Gamma }}(\bar {a})<S_{\bar {\Gamma }}(\bar {c})$
by Proposition 32
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {c}$
. For rule var
$_{\ll }$
the property follows directly from the inductive hypothesis. For rule abs
$_{\ll ,1}$
we have
$\bar {b}=[x:\bar {b}_1]\bar {b}_2$
where
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {b}_1$
. From
$\bar {\Gamma }\!\vdash \![x:\bar {b}_1]\bar {b}_2\ll \bar {c}$
by Proposition 36
$\bar {\Gamma }\!\vdash \!\bar {b}_1\ll \bar {c}$
. By inductive hypothesis
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {c}$
. Rule abs
$_{\ll ,2}$
can be handled similar to rule abs
$_{\ll ,1}$
using also the weakening Proposition 35. For rule abs
$_{\ll ,3}$
(rule abs
$_{\ll ,4}$
is handled similarly) we have
$\bar {a}=[x:\bar {a}_1]\bar {a}_2$
,
$\bar {b}=[x:\bar {b}_1]\bar {b}_2$
where
$\bar {\Gamma }\!\vdash \!\bar {a}_1\ll \bar {b}_1$
,
$\bar {\Gamma },x:\bar {a}_1\!\vdash \!\bar {a}_2\lesssim \bar {b}_2$
, and
$\bar {\Gamma }\!\vdash \!\bar {b}\ll \bar {c}$
. Regarding the latter statement by definition of norm order (Table 3) there are five cases.
-
• start
$_{\ll }$
: This case is similar to the case start
$_{\ll }$
above. -
• abs
$_{\ll ,1}$
:
$\bar {c}=[x:\bar {c}_1]\bar {c}_2$
for some
$\bar {c}_1$
,
$\bar {c}_2$
where
$\bar {\Gamma }\!\vdash \!\bar {b}\lesssim \bar {c}_1$
. The inductive hypothesis obviously implies
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {c}_1$
hence by rule abs
$_{\ll ,1} \bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {c}$
. -
• abs
$_{\ll ,3}$
:
$\bar {c}=[x:\bar {c}_1]\bar {c}_2$
for some
$\bar {c}_1$
,
$\bar {c}_2$
where
$\bar {\Gamma }\!\vdash \!\bar {b}_1\ll \bar {c}_1$
,
$\bar {\Gamma },x:\bar {b}_1\!\vdash \!\bar {b}_2\lesssim \bar {c}_2$
. By a case distinction and Proposition 37 obviously
$\bar {\Gamma },x:\bar {a}_1\!\vdash \!\bar {b}_2\lesssim \bar {c}_2$
hence the inductive hypothesis obviously implies
$\bar {\Gamma },x:\bar {a}_1\!\vdash \!\bar {a}_2\lesssim \bar {c}_2$
. Furthermore by inductive hypothesis
$\bar {\Gamma }\!\vdash \!\bar {a}_1\ll \bar {c}_1$
and hence by rule abs
$_{\ll ,3}\ \bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {c}$
.
The cases abs
$_{\ll ,2}$
and abs
$_{\ll ,4}$
are argued similarly to cases abs
$_{\ll ,1}$
and abs
$_{\ll ,3}$
.
Proposition 39 (Decomposition of weak norm order).
If
$\bar {\Gamma }\!\vdash \![x:\bar {a}]\bar {b}\lesssim [x:\bar {a}]\bar {c}$
then
$\bar {\Gamma },x:\bar {a}\!\vdash \!\bar {b}\lesssim \bar {c}$
.
Proof. The interesting case is
$\bar {\Gamma }\!\vdash \![x:\bar {a}]\bar {b}\ll [x:\bar {a}]\bar {c}$
. By definition of norm order (Table 3) four rules are relevant. Rule abs
$_{\ll ,1}$
would imply
$\bar {\Gamma }\!\vdash \![x:\bar {a}]\bar {b}\ll \bar {a}$
. However, since obviously
$\bar {\Gamma }\!\vdash \!\bar {a}\ll [x:\bar {a}]\bar {b}$
, by Proposition 38
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \bar {a}$
which is impossible due to Proposition 31. Rule abs
$_{\ll ,2}$
implies
$\bar {\Gamma }\!\vdash \![x:\bar {a}]\bar {b}\lesssim \bar {c}$
. By Proposition 36 this implies
$\bar {\Gamma },x:\bar {a}\!\vdash \!\bar {b}\ll \bar {c}$
. Rules abs
$_{\ll ,3}$
and abs
$_{\ll ,4}$
directly establish the property.
We can now show that weak norm order (Table 3) is implied by generalized inclusion on norms.
Proposition 40 (Generalized inclusion includes weak norm order).
$\bar {\Gamma }\!\vdash \!\bar {a}{{}\cdot \!{\!}\!\leq {}}\bar {b}$
implies
$\bar {\Gamma }\!\vdash \!\bar {a}\lesssim \bar {b}$
.
Proof. We show three properties by simultaneous induction on the definition of typing, inclusion, and
$\tau _{}$
-inclusion: (i)
$\bar {\Gamma }\!\vdash \!\bar {a}:\bar {b}$
implies
$\bar {\Gamma }\!\vdash \!\bar {a}\lesssim \bar {b}$
, (
$ii$
)
$\bar {\Gamma }\!\vdash \!\bar {a}\leq \bar {b}$
implies
$\bar {\Gamma }\!\vdash \!\bar {a}\lesssim \bar {b}$
, and (
$iii$
)
$\bar {\Gamma }\!\vdash \!\bar {a}<\tau _{n}$
implies
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \tau _{n}$
. Note that due to Proposition 19 we can assume all auxiliary expressions in rule antecedents to be norms.
(i): Trivial for rule appl, obvious for rules ax and conv, and for rule start follows from rule var
$_{\ll }$
. For rule weak the property follows from the inductive hypothesis and from Proposition 35, for rule inc it follows from the inductive hypotheses of (i) and (
$ii$
) and from Proposition 38, and for rule abs it follows from the inductive hypothesis of (i), Proposition 3, and from rule abs
$_{\ll ,4}$
.
(
$ii$
): Obvious for rule refl
$_{\leq }$
, for rule emb
$_{\leq }$
follows from the inductive hypothesis of (
$iii$
), and for rule abs
$_{\leq }$
follows from the inductive hypothesis of (
$ii$
), Proposition 3, and rule abs
$_{\ll ,4}$
.
(
$iii$
): For rule ord
$_<$
the property follows from rule start
$_{\ll }$
and the definition of
$\tau _{}$
-size. For rule typ
$_<$
we have
$\bar {\Gamma }\!\vdash \!\bar {a}:\bar {c}$
and
$\bar {\Gamma }\!\vdash \!\bar {c}<\tau _{n}$
for some
$\bar {c}$
. By inductive hypotheses of (i) and (
$iii$
) we have
$\bar {\Gamma }\!\vdash \!\bar {a}\lesssim \bar {c}$
and
$\bar {\Gamma }\!\vdash \!\bar {c}\ll \tau _{n}$
and hence by Proposition 38
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \tau _{n}$
. For rule abs
$_<$
we have
$\bar {a}=[x:\bar {a}_1]\bar {a}_2$
for some
$\bar {a}_1$
,
$\bar {a}_2$
where
$\bar {\Gamma }\!\vdash \!\bar {a}_1<\tau _{n}$
and
$\bar {\Gamma },x:\bar {a}_1\!\vdash \!\bar {a}_2<\tau _{n}$
. By inductive hypothesis of (
$iii$
)
$\bar {\Gamma }\!\vdash \!\bar {a}_1\ll \tau _{n}$
and
$\bar {\Gamma },x:\bar {a}_1\!\vdash \!\bar {a}_2\ll \tau _{n}$
. By a very simple inspection of the norm order rules (Table 3) this implies
$S_{\bar {\Gamma }}(\bar {a}_1)<n$
and
$S_{\bar {\Gamma },x:\bar {a}_1}(\bar {a}_2)<n$
and therefore obviously
$S_{\bar {\Gamma }}(\bar {a})<n$
and by Proposition 32
$\bar {\Gamma }\!\vdash \!\bar {a}\ll \tau _{n}$
.
We now turn our attention to (regular) expressions and will eventually show a substitution property (Proposition 43) where we relate the norming of a substitution and the substitution on a norming w.r.t. weak norm order. Before that we need to show two auxiliary properties about norming.
Proposition 41 (Removal of elimination list).
For all
$\Lambda $
,
$\Theta $
, a: if
$\Lambda ,\Theta \!\models \! a$
and
$\Lambda \!\models \! a$
then
$\,\parallel a \parallel _{\Lambda ,\Theta }=[x:\bar {b}_1]\bar {b}_2$
for some
$\bar {b}_1$
,
$\bar {b}_2$
implies
$\,\parallel a \parallel _{\Lambda }=[x:\bar {b}_1]\bar {b}_2'$
for some
$\bar {b}_2'$
.
Proof. Induction on the definition of
$\,\parallel a \parallel _{\Lambda ,\Theta }$
. In order to make the induction work we show a more general property. For all
$\Lambda $
,
$\Theta _1$
,
$\Theta _2$
, and a let
$\Theta =(\Theta _1, \Theta _2)$
: If
$\Lambda ,\Theta \!\models \! a$
and
$\Lambda ,\Theta _1\!\models \! a$
then
$\,\parallel a \parallel _{\Lambda ,\Theta }[\Theta _1]=[x:\bar {b}_1]\bar {b}_2$
implies
$\,\parallel a \parallel _{\Lambda ,\Theta _1}[\Theta _1]= [x:\bar {b}_1]\bar {b}_2'$
for some
$\bar {b}_2'$
(see 14 for the definition of
$a[\Theta ]$
). The proof is simple and does not require further properties.
Based on this result we show a property somewhat similar to Proposition 26. In this property we use the notation
$(a\,\Theta )$
recursively defined by
$(a\,())=a$
,
$(a\,(b,\Theta ))=((a\,b)\,\Theta )$
. Note that
$\Lambda \!\models \!(a\,\Theta )$
obviously implies
$\Lambda ,\Theta \!\models \! a$
but not vice versa, e.g.,
$\tau _{0}\!\models \!\tau _{0}$
but not
$\!\models \!(\tau _{0}\,\tau _{0})$
.
Proposition 42 (Elimination and generalized inclusion (2)).
If
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b \parallel _{\Lambda }{{}\cdot \!{\!}\!\leq {}}\,\parallel a \parallel _{\Lambda }$
,
$\Lambda \!\models \!(b\,\Theta )$
, and
$\Lambda \!\models \!(a\,\Theta )$
then
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b \parallel _{\Lambda ,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel a \parallel _{\Lambda ,\Theta }$
.
Proof. Induction on
$\Theta $
.
$\Theta =()$
is obvious. Let
$\Theta =(c,\Theta ')$
, hence obviously
$\Lambda \!\models \!((b\,c)\,\Theta ')$
and
$\Lambda \!\models \!((a\,c)\,\Theta ')$
and by inductive hypothesis
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel (b\,c) \parallel _{\Lambda ,\Theta '}{{}\cdot \!{\!}\!\leq {}}\,\parallel (a\,c) \parallel _{\Lambda ,\Theta '}$
. Since
$\Lambda ,\Theta '\!\models \!(b\,c)$
we know that
$\,\parallel b \parallel _{\Lambda ,\Theta }=[x:\bar {b}_1]\,\parallel (b\,c) \parallel _{\Lambda ,\Theta '}$
for some x,
$\bar {b}_1$
. Similarly since
$\Lambda ,\Theta '\!\models \!(a\,c)$
we know that
$\,\parallel a \parallel _{\Lambda ,\Theta }=[x:\bar {a}_1]\,\parallel (a\,c) \parallel _{\Lambda ,\Theta '}$
for some
$\bar {a}_1$
. By Proposition 41 we have
$\,\parallel b \parallel _{\Lambda }=[x:\bar {b}_1]\bar {b}_2$
for some
$\bar {b}_2$
and similar for
$\,\parallel a \parallel _{\Lambda }$
. Hence since
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b \parallel _{\Lambda }{{}\cdot \!{\!}\!\leq {}}\,\parallel a \parallel _{\Lambda }$
by Proposition 22(
$iii$
)
$\bar {a}_1=\bar {b}_1$
. Hence obviously
$\,\parallel \Lambda \parallel _{}\vdash \,\,\parallel b \parallel _{\Lambda ,\Theta }=[x:\bar {b}_1]\,\parallel (b\,c) \parallel _{\Lambda ,\Theta '}{{}\cdot \!{\!}\!\leq {}}[x:\bar {a}_1]\,\parallel (a\,c) \parallel _{\Lambda ,\Theta '}=\,\parallel a \parallel _{\Lambda ,\Theta }$
.
We now come to the main substitution property involving norming and weak norm order.
Proposition 43 (Substitution property of weak norm order).
Assume that
$\!\models \!\Gamma $
,
$\Gamma \!\models \! a$
,
$\Gamma \!\models \! b$
,
$\Gamma ,x:a\!\models \! c$
, and
$\Gamma \!\models \! c\lbrack b/x\rbrack $
: If
$\,\parallel \Gamma \parallel _{}\vdash \,\,\parallel b \parallel _{\Gamma }\!{{}\cdot \!{\!}\!\leq {}}\,\parallel a \parallel _{\Gamma }$
then
$\,\parallel \Gamma \parallel _{}\vdash \,\,\parallel c\lbrack b/x\rbrack \parallel _{\Gamma }\lesssim \,\parallel c \parallel _{\Gamma ,x:a}\lbrack \,\parallel b \parallel _{\Gamma }/x\rbrack $
.
Proof. Under the given assumptions by Proposition 20 we obtain
$\Gamma ,x:= b\!\models \! c$
and
$\,\parallel c \parallel _{\Gamma ,x:= b}=\,\parallel c\lbrack b/x\rbrack \parallel _{\Gamma }$
. Therefore, we define
$\Lambda _a=(\Lambda _1,x:a,\Lambda _2)$
,
$\Lambda _b=(\Lambda _1,x:=b, \Lambda _2)$
and we show the more general property that
$\!\models \!\Lambda _b$
,
$\Lambda _1\!\models \! a$
,
$\Lambda _1\!\models \! b$
,
$\,\parallel \Lambda _1 \parallel _{}\vdash \,\,\parallel b \parallel _{\Lambda _1}{{}\cdot \!{\!}\!\leq {}}\,\parallel a \parallel _{\Lambda _1}$
,
$\Lambda _a\!\models \! (c\,\Theta )$
, and
$\Lambda _b\!\models \! (c\,\Theta )$
, imply
$\,\parallel \Lambda _b \parallel _{}\vdash \,\,\parallel c \parallel _{\Lambda _b,\Theta }\lesssim \,\parallel c \parallel _{\Lambda _a,\Theta }\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack $
. The original property is implied with
$\Lambda _1=\Gamma $
,
$\Lambda _2=()$
, and
$\Theta =()$
. The proof is by induction on the definition of
$\,\parallel c \parallel _{\Lambda _b,\Theta }$
.
The case
$c=\tau _{n}$
is obvious. If
$c=x$
then
$\,\parallel x \parallel _{\Lambda _b,\Theta }=\,\parallel b \parallel _{\Lambda _b,\Theta }$
. If
$\Theta =()$
then
$\,\parallel x \parallel _{\Lambda _a}\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack =\,\parallel b \parallel _{\Lambda _1}=\,\parallel b \parallel _{\Lambda _b,\Theta }$
. If
$\Theta \neq ()$
then
$\,\parallel x \parallel _{\Lambda _a,\Theta }\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack =\,\parallel a \parallel _{\Lambda _a,\Theta }\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack =\,\parallel a \parallel _{\Lambda _a,\Theta }$
and using Propositions 42 and 35 obviously
$\,\parallel \Lambda _b \parallel _{}\vdash \,\,\parallel b \parallel _{\Lambda _b,\Theta }{{}\cdot \!{\!}\!\leq {}}\,\parallel a \parallel _{\Lambda _a,\Theta }$
. Therefore by Proposition 40
$\,\parallel \Lambda _b \parallel _{}\vdash \,\,\parallel b \parallel _{\Lambda _b,\Theta }\lesssim \,\parallel a \parallel _{\Lambda _a,\Theta }$
. If
$c=y$
for some
$y\neq x$
then if
$y\in {{dom}}(\Lambda _1)$
two norms are equal, otherwise
$y\in {{dom}}(\Lambda _2)$
and the property follows from the inductive hypothesis.
If
$c=[y:c_1]c_2$
then if
$\Theta =()$
by definition of norming and substitution
$\,\parallel c \parallel _{\Lambda _b}=[y:\bar {c}_{1b}]\bar {c}_{2b}$
and
$\,\parallel c \parallel _{\Lambda _a}\lbrack \bar {c}_{1b}/x\rbrack =[y:\bar {c}_{1a}\lbrack \bar {c}_{1b}/x\rbrack ](\bar {c}_{2b}\lbrack \bar {c}_{1b}/x\rbrack )$
where
$\bar {c}_{1a}=\,\parallel c_1 \parallel _{\Lambda _a}$
,
$\bar {c}_{1b}=\,\parallel c_1 \parallel _{\Lambda _b}$
, and
$\bar {c}_{2b}=\,\parallel c_2 \parallel _{\Lambda _b,y:c_1}$
. By inductive hypothesis
$\,\parallel \Lambda _b \parallel _{}\vdash \,\bar {c}_{1b}\lesssim \bar {c}_{1a}\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack $
and
$\,\parallel \Lambda _b \parallel _{},y:\bar {c}_{1b}\vdash \,\bar {c}_{2b}\lesssim \bar {c}_{2a}\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack $
where
$\bar {c}_{2a}=\,\parallel c_2 \parallel _{\Lambda _a,y:c_1}$
. Hence by property abs
$_{\lesssim } \,\parallel \Lambda _b \parallel _{}\vdash \,\,\parallel c \parallel _{\Lambda _b}=[y:\,\parallel c_1 \parallel _{\Lambda _b}]\bar {c}_{2b} \lesssim [y:\bar {c}_{1a}\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack ]\bar {c}_{2a}\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack =\,\parallel c \parallel _{\Lambda _a}\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack $
. Otherwise if
$\Theta =(d,\Theta ')$
one can argue similarly with
$\bar {c}_{1a}$
,
$\bar {c}_{1b}$
as before and
$\bar {c}_{2a}=\,\parallel c_2 \parallel _{(\Lambda _a,y:= d),\Theta '}$
,
$\bar {c}_{2b}=\,\parallel c_2 \parallel _{(\Lambda _b,y:= d),\Theta '}$
. Note that the inductive hypothesis can be applied since from
$(c\,\Theta )=((c\,d)\,\Theta ')$
by Proposition 21
$\Lambda _b\!\models \!(c_2\lbrack d/y\rbrack \,\Theta ')$
and therefore by Proposition 20
$\Lambda _b,y:= d\!\models \!(c_2\,\Theta ')$
, and a similar argument can be made for
$\Lambda _a\!\models \!(c\,\Theta )$
.
If
$c=(c_1\,c_2)$
then by definition of norming
$\,\parallel c \parallel _{\Lambda _b,\Theta }=\bar {e}_b$
where
$\,\parallel c_1 \parallel _{\Lambda _b,(c_2,\Theta )}=[y:\bar {d}_b]\bar {e}_b$
for some
$y\neq x$
,
$\bar {d}_b$
,
$\bar {e}_b$
. Similarly
$\,\parallel c \parallel _{\Lambda _a,\Theta }\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack =\bar {e}_a\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack $
where
$\,\parallel c_1 \parallel _{\Lambda _a,(c_2,\Theta )}=[y:\bar {d}_a]\bar {e}_a$
for some
$\bar {d}_a$
,
$\bar {e}_a$
. By Proposition 41
$\,\parallel c_1 \parallel _{\Lambda _b}=[y:\bar {d}_b]\bar {e}$
and
$\,\parallel c_1 \parallel _{\Lambda _a}=[y:\bar {d}_a]\bar {e}'$
for some
$\bar {e}$
,
$\bar {e}'$
hence
$\bar {d}_b=\bar {d}_a$
. Since
$(c\,\Theta )=(c_1\,(c_2\,\Theta ))$
and similar for
$\Lambda _a$
, by inductive hypothesis, definition of substitution, and since
$x\notin {{FV}}(\bar {d}_b)$
we have
$\,\parallel \Lambda _b \parallel _{}\vdash \,[y:\bar {d}_b]\bar {e}_b\lesssim ([y:\bar {d}_b]\bar {e}_a)\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack =[y:\bar {d}_b](\bar {e}_a\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack )$
and therefore by Propositions 39 and 35
$\,\parallel \Lambda _b \parallel _{}\vdash \,\bar {e}_b\lesssim \bar {e}_a\lbrack \,\parallel b \parallel _{\Lambda _1}/x\rbrack $
.
Next we recursively define subsets of strongly normalisable valid expressions.
Definition 16. The set of computable expressions of norm
$\bar {a}$
under context
$\Gamma $
is denoted by
$\mathit {C}_{\Gamma }(\bar {a})$
.
$a\in \mathit {C}_{\Gamma }(\bar {a})$
iff
$a\in {\mathcal {S}_{}}$
,
$\Gamma \!\vdash \! a$
,
$\,\parallel \Gamma \parallel _{}\vdash \,\,\parallel a \parallel _{\Gamma }\!{{}\cdot \!{\!}\!\leq {}}\bar {a}$
, and the following computability condition is satisfied
$:$
For all x, b, c: If
$a\to ^*[x:b]c$
then
$c\lbrack d/x\rbrack \in \mathit {C}_{\Gamma }(\,\parallel c\lbrack d/x\rbrack \parallel _{\Gamma })$
for all
$d\in \mathit {C}_{\Gamma }(\,\parallel b \parallel _{\Gamma })$
with
$\Gamma \!\vdash \! d:b$
.
In the definition note that from
$\Gamma \!\vdash \! a$
by Proposition 29 we obtain both
$\!\models \!\Gamma $
and
$\Gamma \!\models \! a$
. Similarly Proposition 11 implies
$\Gamma \!\vdash \![x:b]c$
and then from
$\Gamma \!\vdash \! d:b$
by Propositions 5, 2, and 29
$\Gamma \!\models \! b$
and
$\Gamma \!\models \! c\lbrack d/x\rbrack $
. In order not to clutter the following argument about properties of computability we will not explicitly mention the use of these propositions.
Furthermore the recursion in the above definition eventually terminates which is a core argument of this proof of strong normalisation.
Proposition 44 (The definition of computable expressions terminates).
If
$\: \Gamma \!\vdash \!\bar {a}$
then the definition of
$\mathit {C}_{\Gamma }(\bar {a})$
terminates.
Proof. Norm induction (Proposition 34) on
$\bar {a}$
. Consider some
$a\in {\mathcal {S}_{}}$
where
$\Gamma \!\vdash \! a$
and
$\,\parallel \Gamma \parallel _{}\vdash \,\,\parallel a \parallel _{\Gamma }\!{{}\cdot \!{\!}\!\leq {}}\bar {a}$
. Let
$\bar {\Gamma }=\,\parallel \Gamma \parallel _{}$
,
$\bar {a}'=\,\parallel a \parallel _{\Gamma }$
, and assume
$a\to ^*[x:b]c$
for some x, b, c. By Proposition 21
$\bar {a}'=\,\parallel [x:b]c \parallel _{\Gamma }=[x:\,\parallel b \parallel _{\Gamma }]\,\parallel c \parallel _{\Gamma ,x:b}$
and by Proposition 40
$\bar {\Gamma }\!\vdash \!\bar {a}'\lesssim \bar {a}$
.
Let
$\bar {b}=\,\parallel b \parallel _{\Gamma }$
and
$\bar {c}=\,\parallel c \parallel _{\Gamma ,x:b}$
. Since obviously
$\bar {\Gamma },x:\bar {b}\!\vdash \!\bar {c}\lesssim \bar {c}$
by abs
$_{\ll ,2}\ \bar {\Gamma },x:\bar {b}\!\vdash \!\bar {c}\ll \bar {a}'$
and therefore by Propositions 38 and 35
$\bar {\Gamma },x:\bar {b}\!\vdash \!\bar {c}\ll \bar {a}$
. Assume some
$d\in \mathit {C}_{\Gamma }(\bar {b})$
where
$\Gamma \!\vdash \! d:b$
and let
$\bar {d}=\,\parallel d \parallel _{\Gamma }$
. Since
$\bar {\Gamma }\!\vdash \!\bar {d}\!{{}\cdot \!{\!}\!\leq {}}\bar {b}$
by Proposition 40
$\bar {\Gamma }\!\vdash \!\bar {d}\lesssim \bar {b}$
. Hence by Proposition 37
$\bar {\Gamma }\!\vdash \!\bar {c}\lbrack \bar {d}/x\rbrack \ll \bar {a}\lbrack \bar {d}/x\rbrack =\bar {a}$
and by Proposition 43
$\bar {\Gamma }\!\vdash \!\,\parallel c\lbrack d/x\rbrack \parallel _{\Gamma }\lesssim \bar {c}\lbrack \bar {d}/x\rbrack $
. Hence by Proposition 38
$\bar {\Gamma }\!\vdash \!\,\parallel c\lbrack d/x\rbrack \parallel _{\Gamma }\ll \bar {a}$
. By inductive hypothesis the definition of
$\mathit {C}_{\Gamma }(\,\parallel c\lbrack d/x\rbrack \parallel _{\Gamma })$
terminates and therefore the definition
$\mathit {C}_{\Gamma }(\bar {a})$
terminates as well.
Proposition 45 (Closure of computable expressions against reduction).
$\Gamma \!\models \! a_1$
,
$a_1\in \mathit {C}_{\Gamma }(\,\parallel a_1 \parallel _{\Gamma })$
, and
$a_1\to ^* a_2$
imply
$a_2\in \mathit {C}_{\Gamma }(\,\parallel a_1 \parallel _{\Gamma })$
.
Proof. Follows from Proposition 21 and since
$a_2\to ^*[x:b]c$
implies
$a_1\to ^*[x:b]c$
and therefore the computability condition for
$a_1$
implies the one for
$a_2$
.
Proposition 46 (Closure of computable expressions against application).
$\Gamma \!\vdash \!(a\,b)$
,
$a \in \mathit {C}_{\Gamma }(\,\parallel a \parallel _{\Gamma })$
, and
$b\in \mathit {C}_{\Gamma }(\,\parallel b \parallel _{\Gamma })$
imply
$(a\,b)\in \mathit {C}_{\Gamma }(\,\parallel (a\,b) \parallel _{\Gamma })$
.
Proof. Assume
$\Gamma \!\vdash \!(a\,b)$
,
$a\in \mathit {C}_{\Gamma }(\,\parallel a \parallel _{\Gamma })$
, and
$b\in \mathit {C}_{\Gamma }(\,\parallel b \parallel _{\Gamma })$
. By Proposition 29
$\Gamma \!\models \!(a\,b)$
which implies
$\,\parallel a \parallel _{\Gamma }=[x:\bar {a}_1]\bar {a}_2$
for some x,
$\bar {a}_1$
,
$\bar {a}_2$
where
$\,\parallel \Gamma \parallel _{}\vdash \,\,\parallel b \parallel _{\Gamma }\!{{}\cdot \!{\!}\!\leq {}}\bar {a}_1$
. Let
$a\to ^*[x:a_1]a_2$
for some
$a_1$
,
$a_2$
. From
$\Gamma \!\vdash \!(a\,b)$
by Proposition 11
$\Gamma \!\vdash \!([x:a_1]a_2\,b)$
. Hence by Proposition 10(v)
$\Gamma \!\vdash \! b:a_1$
and
$\Gamma \!\vdash \![x:a_1]a_2:[x:a_1]b_2$
for some
$b_2$
. Since by Propositions 4 and 5
$\Gamma \!\vdash \! a_1$
and
$\Gamma ,x:a_1\!\vdash \! a_2$
, by Propositions 29 and 21
$\,\parallel a_1 \parallel _{\Gamma }=\bar {a}_1$
and
$\,\parallel a_2 \parallel _{\Gamma ,x:a_1}=\bar {a}_2$
. Since
$b\in \mathit {C}_{\Gamma }(\,\parallel b \parallel _{\Gamma })$
, by definition of computable expressions
$b\in \mathit {C}_{\Gamma }(\bar {a}_1)$
. By computability condition of
$a\in \mathit {C}_{\Gamma }(\,\parallel a \parallel _{\Gamma })$
we obtain
$a_2\lbrack b/x\rbrack \in \mathit {C}_{\Gamma }(\,\parallel a_2\lbrack b/x\rbrack \parallel _{\Gamma })$
which implies
$a_2\lbrack b/x\rbrack \in {\mathcal {S}_{}}$
. Therefore by Proposition 30
$(a\,b)\in {\mathcal {S}_{}}$
.
It remains to show the computability condition for
$(a\,b)$
. Let
$(a\,b)\to ^*[y:a_3]a_4$
, for some
$y\neq x$
,
$a_3$
and
$a_4$
. By basic properties of reduction
$a\to ^*[x:a_1]a_2$
,
$b\to ^* b'$
, and
$a_2\lbrack b'/x\rbrack \to ^*[y:a_3]a_4$
for some
$a_1$
,
$a_2$
, and
$b'$
. Hence as argued in the previous paragraph
$\,\parallel a_1 \parallel _{\Gamma }=\bar {a}_1$
and
$\,\parallel a_2 \parallel _{\Gamma ,x:a_1}=\bar {a}_2$
. By Proposition 21
$\,\parallel (a\,b) \parallel _{\Gamma }=\,\parallel [y:a_3]a_4 \parallel _{\Gamma }$
. Furthermore, since
$b\to ^* b'$
by Proposition 45 and since
$\,\parallel \Gamma \parallel _{}\vdash \,\,\parallel b \parallel _{\Gamma }\!{{}\cdot \!{\!}\!\leq {}}\bar {a}_1$
we know that
$b'\in \mathit {C}_{\Gamma }(\bar {a}_1)$
. As in the previous paragraph we have
$\Gamma \!\vdash \! b:a_1$
and hence by Proposition 11
$\Gamma \!\vdash \! b':a_1$
. We now argue as follows:
$$ \begin{align*} &\ a\in\mathit{C}_{\Gamma}(\,\parallel [x:a_1]a_2 \parallel_{\Gamma})\\\Rightarrow&\ (a\ \text{is computable}, b'\in\mathit{C}_{\Gamma}(\bar{a}_1), \text{and}\ \Gamma\!\vdash\! b':a_1)\\&\ a_2\lbrack b'/x\rbrack\in\mathit{C}_{\Gamma}(\,\parallel a_2\lbrack b'/x\rbrack \parallel_{\Gamma})\\\Rightarrow&\ \text{(Proposition}\ {45}\ \text{since}\ a_2\lbrack b'/x\rbrack\to^*[y:a_3]a_4)\\&\ [y:a_3]a_4\in\mathit{C}_{\Gamma}(\,\parallel a_2\lbrack b'/x\rbrack \parallel_{\Gamma})\\\Rightarrow&\ \text{(By Proposition}\ {21} \,\parallel a_2\lbrack b'/x\rbrack \parallel_{\Gamma}=\,\parallel [y:a_3]a_4 \parallel_{\Gamma})\\&\ [y:a_3]a_4\in\mathit{C}_{\Gamma}(\,\parallel [y:a_3]a_4 \parallel_{\Gamma}). \end{align*} $$
From the computability condition of
$[y:a_3]a_4\in \mathit {C}_{\Gamma }(\,\parallel a \parallel _{\Gamma })$
we know that
$a_4\lbrack d/y\rbrack \in \mathit {C}_{\Gamma }(\,\parallel a_4\lbrack d/y\rbrack \parallel _{\Gamma })$
for all
$d\in \mathit {C}_{\Gamma }(\,\parallel a_3 \parallel _{\Gamma })$
where
$\Gamma \!\vdash \! d:a_3$
.
Note that computable expressions are not closed against universal abstraction. The missing part is made precise in the following property.
Proposition 47 (Abstraction closure for computable expressions).
Assume
$\: \Gamma \!\vdash \![x:a]b$
: If
$a\in \mathit {C}_{\Gamma }(\,\parallel a \parallel _{\Gamma })$
,
$b\in \mathit {C}_{\Gamma ,x:a}(\,\parallel b \parallel _{\Gamma ,x:a})$
, and if for all c with
$c\in \mathit {C}_{\Gamma }(\,\parallel a \parallel _{\Gamma })$
and
$\Gamma \!\vdash \! c:a$
we have
$b\lbrack c/x\rbrack \in \mathit {C}_{\Gamma }(\,\parallel b\lbrack c/x\rbrack \parallel _{\Gamma })$
then
$[x:a]b\in \mathit {C}_{\Gamma }(\,\parallel [x:a]b \parallel _{\Gamma })$
.
Proof. Assume
$\Gamma \!\vdash \![x:a]b$
and let
$\bar {a}=\,\parallel a \parallel _{\Gamma }$
and
$\bar {b}=\,\parallel b \parallel _{\Gamma ,x:a}$
. From
$a\in \mathit {C}_{\Gamma }(\bar {a})$
and
$b\in \mathit {C}_{\Gamma ,x:a}(\bar {b})$
, by definition of computable expressions
$a,b\in {\mathcal {S}_{}}$
. By an obvious argument this implies
$[x:a]b\in {\mathcal {S}_{}}$
. To show
$[x:a]b\in \mathit {C}_{\Gamma }([x:\bar {a}]\bar {b})$
, it remains to show the computability condition for
$[x:a]b$
: Assume
$[x:a]b\to ^*[x:c]d$
for some c and d. This obviously implies
$a\to ^* c$
and
$b\to ^* d$
. Assume
$e\in \mathit {C}_{\Gamma }(\bar {a})$
for some e where
$\Gamma \!\vdash \! e:a$
.
$b\lbrack e/x\rbrack \in \mathit {C}_{\Gamma }((\,\parallel b\lbrack e/x\rbrack \parallel _{\Gamma })$
follows from the assumption about substitution (by instantiating c to e). Since obviously
$b\lbrack e/x\rbrack \to ^* d\lbrack e/x\rbrack $
by Proposition 45
$d\lbrack e/x\rbrack \in \mathit {C}_{\Gamma }((\,\parallel d\lbrack e/x\rbrack \parallel _{\Gamma })$
.
Using Proposition 47 we will show computability of all normable expressions by showing the stronger property that normable expressions are computable under any substitution of their free variables to computable expressions matching their types. First we need to extend substitution:
Definition 17 (Substitution function, type matching substitution).
Given sequences of pairwise disjoint variables
$X=(x_1,\ldots ,x_n)$
and expressions
$B=(b_1,\ldots ,b_n)$
where
$n\geq 0$
, the substitution function
$\sigma _{X,B}$
is defined by
$\sigma _{X,B}(a)=a\lbrack b_1/x_1\rbrack \cdots \lbrack b_n/x_n\rbrack $
and on contexts by
$\sigma _{X,B}(())=()$
,
$\sigma _{X,B}(x:a,\Gamma )=(x:\sigma _{X,B}(a),\sigma _{X,B}(\Gamma ))$
if
$x\neq x_i$
, and
$\sigma _{X,B}(x:a,\Gamma )=\sigma _{X,B}(\Gamma )$
otherwise. If
$x\neq x_i$
we write
$\sigma _{X,B}\lbrack b/x\rbrack $
for
$\sigma _{(x_1,\ldots ,x_n,x),(b_1,\ldots ,b_n,b)}$
.
A substitution
$\sigma _{X,B}$
where
$X=(x_1,\ldots ,x_n)$
and
$B=(b_1,\ldots ,b_n)$
is type matching w.r.t.
$\Gamma $
iff
$\Gamma =(\Gamma _0,x_1:a_1,\Gamma _1\ldots x_n:a_n,\Gamma _n)$
, for some
$\Gamma _0$
and
$a_i$
,
$\Gamma _i$
and
$\Gamma \!\vdash \!\sigma _{X,B}(b_i):\sigma _{X,B}(a_i)$
where
$1\leq i\leq n$
.
We can now relate validity and computability under substitution.
Proposition 48 (Validity implies computability).
If
$\Gamma \!\vdash \! a$
then for any type-matching substitution function
$\sigma _{X,B}$
with
$\sigma _{X,B}(x_i)\in \mathit {C}_{\sigma _{X,B}(\Gamma )}(\,\parallel \sigma _{X,B}(b_i) \parallel _{\Gamma })$
, for
$1\leq i\leq n$
, we have
$\sigma _{X,B}(a)\in \mathit {C}_{\sigma _{X,B}(\Gamma )}(\,\parallel \sigma _{X,B}(a) \parallel _{\Gamma })$
.
Proof. Assume
$\Gamma \!\vdash \! a$
. The proof is by structural induction on a. We write
$\sigma $
for
$\sigma _{X,B}$
. The case
$a=\tau _{n}$
is obvious.
For the case
$a=x$
we have
$\Gamma \!\vdash \! x$
and
$\bar {a}=\,\parallel x \parallel _{\Gamma }=x$
. There are two sub cases: If
$x=x_i$
, for some i then obviously
$\sigma (x)=\sigma (b_i)$
and therefore, since
$\sigma (b_i)\in \mathit {C}_{\sigma (\Gamma )}(\,\parallel \sigma (b_i) \parallel _{\Gamma })$
we know that
$\sigma (x)\in \mathit {C}_{\sigma (\Gamma )}(\,\parallel \sigma (x) \parallel _{\Gamma })$
. If
$x\neq x_i$
, for all i then
$\sigma (x)=x$
and it is easy to see that
$x\in \mathit {C}_{\sigma (\Gamma )}(x)$
.
For the case
$a=[x:b]c$
: From
$\Gamma \!\vdash \![x:b]c$
by definition of validity
$\Gamma \!\vdash \! b$
and
$\Gamma ,x:b\!\vdash \! c$
. Applying the inductive hypothesis with
$\sigma $
we obtain
$\sigma (b)\in \mathit {C}_{\sigma (\Gamma )}(\,\parallel \sigma (b) \parallel _{\Gamma })$
and
$\sigma (c)\in \mathit {C}_{\sigma (\Gamma ,x:b)}(\,\parallel \sigma (c) \parallel _{\Gamma ,x:b})$
. Consider a d where
$d\in \mathit {C}_{\Gamma }(\,\parallel \sigma (b) \parallel _{\Gamma })$
and
$\Gamma \!\vdash \! d:b$
. If we define
$X'=(x_1,\ldots ,x_n,x)$
,
$B'=(b_1,\ldots ,b_n,d)$
, and
$\sigma '=\sigma \lbrack d/x\rbrack $
then
$\sigma '$
is obviously type matching and we can obviously apply the inductive hypothesis to it yielding
$\sigma '(c)=\sigma (c)\lbrack d/x\rbrack \in \mathit {C}_{\sigma '(\Gamma )}(\,\parallel \sigma (c)\lbrack d/x\rbrack \parallel _{\Gamma })$
. Hence by Proposition 47
$[x:\sigma (b)]\sigma (c)\in \mathit {C}_{\sigma '(\Gamma )}(\,\parallel [x:\sigma (b)]\sigma (c) \parallel _{\Gamma })$
which by definition of substitution and since obviously
$\sigma '(\Gamma )=\sigma (\Gamma )$
is equivalent to
$\sigma ([x:b]c)\in \mathit {C}_{\sigma (\Gamma )}(\,\parallel \sigma ([x:b]c) \parallel _{\Gamma })$
.
For the case
$a=(a_1\,a_2)$
by inductive hypothesis
$\sigma (a_1)\in \mathit {C}_{\sigma (\Gamma )}(\sigma (\,\parallel a_1 \parallel _{\Gamma })$
and
$\sigma (a_2)\in \mathit {C}_{\sigma (\Gamma )}(\sigma (\,\parallel a_2 \parallel _{\Gamma }))$
. Since
$\Gamma \!\vdash \! a$
and since
$\sigma $
is type-matching by an obvious induction using Proposition 2
$\sigma (\Gamma )\!\vdash \!(\sigma (a_1)\,\sigma (a_2))$
. Hence by Proposition 46 we obtain
$(\sigma (a_1)\,\sigma (a_2))\in \mathit {C}_{\sigma (\Gamma )}(\,\parallel (\sigma (a_1)\,\sigma (a_2)) \parallel _{\Gamma })$
which by definition of substitution is the same as
$\sigma ((a_1\,a_2))\in \mathit {C}_{\sigma (\Gamma )}(\,\parallel \sigma ((a_1\,a_2)) \parallel _{\Gamma })$
.
Strong normalisation of valid expressions is a direct consequence.
Proposition 49 (Strong normalization of valid expressions).
$\Gamma \!\vdash \! a$
implies
$a\in {\mathcal {S}_{}}$
.
Proof. Proposition 48 with
$\sigma _{(),()}$
implies
$a\in \mathit {C}_{\Gamma }(\,\parallel a \parallel _{\Gamma })$
. By definition of computable expressions this implies
$a\in {\mathcal {S}_{}}$
.
Strong normalisation and confluence (Proposition 1) imply the existence of a unique normal form for every valid expression. It is easy to see that such a normal form is either the constant
$\tau _{n}$
, for some n, or an expression
$[x_1:a_1]\ldots [x_k:a_k](\ldots ( x\,b_1) \ldots \, b_m)$
where
$k,m\geq 0$
and
$a_i$
,
$b_i$
are normal forms. The existence of unique normal forms for valid expressions is key for decision algorithms.
Remark (Decidability of typing).
The idea is to use minimal types (Definition 8). Given an expression a, to check if there is a b where
$\Gamma \!\vdash \! a:b$
one can use an obvious recursive algorithm based on the structure of a computing and comparing normal forms of minimal types. As usual there is a simultaneous recursion with the check of
$\Gamma \!\vdash \! c\leq d$
and
$\Gamma \!\vdash \! c<\tau _{n}$
, for some given c, d, and n.
Finally, strong normalisation leads to the following consistency property.
Proposition 50 (Consistency of d ≤).
There is no expression a such that
$\!\vdash \! a: [x:\tau _{n}]x$
.
Proof. Assume that there is an expression a with
$\vdash \! a:[x:\tau _{n}]x$
. By Proposition 49 (strong normalization), we know that there is a unique normal form b with
$a\to ^* b$
. By Proposition 11 (subject reduction) we know that
$\!\vdash \! b:[x:\tau _{n}]x$
. Note that due to Proposition 10(i) b cannot be a primitive constant. Hence, since b is valid, obviously
$b=[x_1:a_1]\ldots [x_k:a_k](\ldots ( y\,b_1) \ldots \, b_m)$
for some
$x_i$
,
$a_i$
, k where
$0\leq i\leq k$
and y,
$b_i$
, m where
$0\leq i\leq m$
and
$y=x_j$
for some j. Since
$k=0$
is obviously not possible, by Proposition 10(
$iv$
) we know that
$a_1=_{\lambda }\tau _{n}$
,
$x=x_1$
, and
$x:\tau _{n}\!\vdash \![x_2:a_2]\ldots [x_k:a_k](\ldots ( y\,b_1) \ldots \, b_m):x$
. If
$k=1$
then
$y=x$
and, since b is valid,
$m=0$
. Hence
$x:\tau _{n}\!\vdash \! x:x$
. By Propositions 10(
$ii$
) and 15 this implies
$x:\tau _{n}\!\vdash \!\tau _{n}\leq _{\lambda } x$
and hence, due to Proposition 11
$x:\tau _{n}\!\vdash \!\tau _{n}\leq x$
which contradicts Proposition 6(i). If
$k>1$
then by Proposition 10(
$iii$
) and 15
$x:\tau _{n},x_2:a_2\!\vdash \! [x_3:a_3]\ldots [x_k:a_k](\ldots ( y\,b_1) \ldots \, b_m):c$
for some c where
$x:\tau _{n}\!\vdash \! [x_2:a_2]c\leq _{\lambda } x$
. Due to Proposition 11 we may assume that
$[x_2:a_2]c$
is in normal form and hence
$x:\tau _{n}\!\vdash \! [x_2:a_2]c\leq x$
which contradicts Proposition 6(
$iii$
).
Acknowledgments
Thanks to an anonymous reviewer for pointing out a sloppiness in an important argument. More generally speaking, this work is in memoriam of my PhD supervisor Michel Sintzoff who passed away many years ago. He raised my interest in the simplicity of the type of systems studied here, but also pointed to challenges including polymorphism.
Funding
No financial support was required for this work.
