This paper extends higher-order polynomial interpretations to impredicative polymorphism within System F-omega, enabling direct termination proofs for complex rewrite rules and inductive data types, demonstrated on a logic fragment.
Contribution
It introduces a novel termination method for impredicative polymorphic systems by interpreting terms in an extended System F-omega, broadening applicability.
Findings
01
Proves termination of a significant fragment of second-order propositional logic.
02
Enables direct interpretation of rewrite rules using impredicative polymorphism.
03
Facilitates encoding of inductive data types in termination proofs.
Abstract
We generalise the termination method of higher-order polynomial interpretations to a setting with impredicative polymorphism. Instead of using weakly monotonic functionals, we interpret terms in a suitable extension of System F-omega. This enables a direct interpretation of rewrite rules which make essential use of impredicative polymorphism. In addition, our generalisation eases the applicability of the method in the non-polymorphic setting by allowing for the encoding of inductive data types. As an illustration of the potential of our method, we prove termination of a substantial fragment of full intuitionistic second-order propositional logic with permutative conversions.
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Semantic Web and Ontologies
\CopyrightŁukasz Czajka and Cynthia Kop
\ccsdesc[500]Theory of computation Rewrite systems
\ccsdesc[500]Theory of computation Equational logic and rewriting
\ccsdesc[300]Theory of computation Type theory
We generalise the termination method of higher-order polynomial
interpretations to a setting with impredicative
polymorphism. Instead of using weakly monotonic functionals, we
interpret terms in a suitable extension of System Fω. This
enables a direct interpretation of rewrite rules which make
essential use of impredicative polymorphism. In addition, our
generalisation eases the applicability of the method in the
non-polymorphic setting by allowing for the encoding of inductive data
types. As an illustration of the potential of our method, we prove
termination of a substantial fragment of full intuitionistic
second-order propositional logic with permutative conversions.
Termination of higher-order term rewriting
systems [20, Chapter 11] has been an active area of
research for several decades.
One powerful method, introduced by v.d. Pol [22, 14],
interprets terms into weakly monotonic algebras. In later work
[5, 11], these algebra interpretations are specialised
into higher-order polynomial interpretations, a generalisation of
the popular – and highly automatable – technique of polynomial
interpretations for first-order term rewriting.
The methods of weakly monotonic algebras and polynomial
interpretation are both limited to monomorphic systems.
In this paper, we will further generalise polynomial
interpretations to a higher-order formalism with full impredicative
polymorphism.
This goes beyond shallow (rank-1, weak) polymorphism,
where type quantifiers are effectively allowed only at the top of a
type: it would be relatively easy to extend the methods to a system
with shallow polymorphism since shallowly polymorphic rules can be seen as defining an
infinite set of monomorphic rules.
While shallow polymorphism often suffices
in functional programming practice, there do exist interesting
examples of rewrite systems which require higher-rank impredicative
polymorphism.
For instance, in recent extensions of Haskell one may define a type of
heterogeneous lists.
[TABLE]
The above states that List is a type (∗), gives the types of its
two constructors nil and cons, and defines the corresponding
fold-left function foldl. Each element of a heterogeneous
list may have a different type. In practice, one would
constrain the type variable α with a type class to
guarantee the existence of some operations on list elements. The
function argument of foldl receives the element together
with its type. The ∀-quantifier binds type variables: a term
of type ∀α.τ takes a type ρ as an argument and
the result is a term of type τ[α:=ρ].
Impredicativity of polymorphism means that the type itself may be
substituted for its own type variable, e.g., if f:∀α.τ then f(∀α.τ):τ[α:=∀α.τ]. Negative occurrences of
impredicative type quantifiers prevent a translation
into an infinite set of simply typed rules by instantiating the type
variables. The above example is not directly reducible to shallow
polymorphism as used in the ML programming language.
Related work. The term rewriting literature
has various examples of higher-order term rewriting systems with some
forms of polymorphism. To start, there are several studies that
consider shallow polymorphic rewriting
(e.g., [8, 10, 24]), where (as in ML-like
languages) systems like foldl above cannot be handled.
Other works consider extensions of the λΠ-calculus
[2, 3] or the calculus of constructions
[1, 25] with rewriting rules; only the latter
includes full impredicative polymorphism. The termination techniques
presented for these systems are mostly syntactic (e.g., a recursive
path ordering [10, 25], or general schema
[1]), as opposed to our more semantic method based on
interpretations.
An exception is [3], which defines
interpretations into Π-algebras; this technique bears some
similarity to ours, although the methodologies are
quite different. A categorical definition for a general polymorphic
rewriting framework is presented in [4], but no
termination methods are considered for it.
Our approach.
The technique we develop in this paper operates on Polymorphic
Functional Systems (PFSs), a form of higher-order term rewriting systems
with full impredicative polymorphism (Section 3), that
various systems of interest can be encoded into (including the example
of heterogeneous fold above). Then, our methodology follows a standard
procedure:
we provide a general methodology to map each PFS term s to a
natural number [[s]], parameterised by a core interpretation
for each function symbol (Section 5);
•
we present a number of lemmas to make it easy to prove that
s≻t or s⪰t whenever s reduces to t
(Section 6).
Due to the additional complications of full polymorphism, we have
elected to only generalise higher-order polynomial interpretations,
and not v.d. Pol’s weakly monotonic algebras. That is, terms of base
type are always interpreted to natural numbers and all functions are
interpreted to combinations of addition and multiplication.
We will use the system of heterogeneous fold above as a running
example to demonstrate our method. However, termination of this
system can be shown in other ways (e.g., an encoding in
System F). Hence, we will also study a more complex example
in Section 7: termination of a substantial fragment
of IPC2, i.e., full intuitionistic second-order propositional logic
with permutative conversions. Permutative
conversions [21, Chapter 6] are used in
proof theory to obtain “good” normal forms of natural deduction
proofs, which satisfy e.g. the subformula property. Termination proofs
for systems with permutative conversions are notoriously tedious and
difficult, with some incorrect claims in the literature and no uniform
methodology. It is our goal to make such termination proofs
substantially easier in the future.
This is a pre-publication copy of a paper at FSCD 2019. In
particular, it contains an appendix with complete proofs for the results
in this paper.
2 Preliminaries
In this section we recall the definition of System Fω (see
e.g. [16, Section 11.7]), which will form a
basis both of our interpretations and of a general syntactic framework
for the investigated systems. In comparison to System F,
System Fω includes type constructors which results in a more
uniform treatment. We assume familiarity with core notions of lambda
calculi such as substitution and α-conversion.
Definition \thetheorem.
Kinds are defined inductively: ∗ is a kind, and if
κ1,κ2 are kinds then so is κ1⇒κ2. We assume an infinite set Vκ of type
constructor variables of each kind κ. Variables of
kind ∗ are type variables. We assume a fixed
set ΣκT of type constructor symbols paired with a
kind κ, denoted c:κ.
We define the set Tκ of type constructors of
kind κ by the following grammar.
Type constructors of kind ∗ are types.
[TABLE]
We use the standard notations ∀α.τ and λα.τ. When α is of kind κ then we use the
notation ∀α:κ.τ. If not indicated
otherwise, we assume α to be a type variable. We treat type
constructors up to α-conversion.
Example 2.1**.**
If Σ∗T={List} and Σ∗⇒∗⇒∗T={Pair}, types are for instance List and
∀α.PairαList. The expression
PairList is a type constructor, but not a type. If
Σ(∗⇒∗)⇒∗T={∃} and
σ∈T∗⇒∗, then both
∃(σ) and ∃(λα.σα) are
types.
The compatible closure of the rule (λα.φ)ψ→φ[α:=ψ] defines β-reduction on type
constructors. As type constructors are (essentially) simply-typed
lambda-terms, their β-reduction terminates
and is confluent; hence every type constructor τ has a unique
β-normal form nfβ(τ). A type atom is a type
in β-normal form which is neither an arrow τ1→τ2
nor a quantification ∀α.τ.
We define FTV(φ) – the set of free type constructor
variables of the type constructor φ – in an obvious way by
induction on φ. A type constructor φ is
closed if FTV(φ)=∅.
We assume a fixed type symbol χ∗∈Σ∗T. For κ=κ1⇒κ2 we define
χκ=λα:κ1.χκ2.
Definition 1**.**
We assume given an infinite set V of variables, each paired
with a type, denoted x:τ. We assume given a fixed set
Σ of function symbols, each paired with a closed type,
denoted f:τ. Every variable x and every function
symbol f occurs only with one type declaration.
The set of preterms consists of all expressions s such that
s:σ can be inferred for some type σ by the following
clauses:
•
x:σ for (x:σ)∈V.
•
f:σ for all
(f:σ)∈Σ.
•
λx:σ.s:σ→τ if
(x:σ)∈V and s:τ.
•
(Λα:κ.s):(∀α:κ.σ) if
s:σ and α does not occur free in the type of a
free variable of s.
•
s⋅t:τ if s:σ→τ and
t:σ
•
s∗τ:σ[α:=τ] if
s:∀α:κ.σ and τ is a type
constructor of kind κ,
•
s:τ if s:τ′ and τ=βτ′.
The set of free variables of a preterm t, denoted FV(t), is
defined in the expected way. Analogously, we define the
set FTV(t) of type constructor variables occurring free in t.
If α is a type then we use the notation Λα.t.
We denote an occurrence of a variable x of type τ
by xτ,
e.g. λx:τ→σ.xτ→σyτ. When clear or irrelevant, we omit
the type annotations, denoting the above term by λx.xy. Type substitution is defined in the expected way except that it
needs to change the types of variables. Formally, a type
substitution changes the types associated to variables in V. We
define the equivalence relation ≡ by: s≡t iff s
and t are identical modulo β-conversion in types.
Note that we present terms in orthodox Church-style, i.e.,
instead of using contexts each variable has a globally fixed type
associated to it.
Lemma 2.2**.**
If s:τ and s≡t then t:τ.
Proof 2.3**.**
Induction on s.
Definition 2**.**
The set of terms is the set of the equivalence classes
of ≡.
Because β-reduction on types is confluent and terminating, every
term has a canonical preterm representative – the one with all types
occurring in it β-normalised.
We define FTV(t)
as the value of FTV on the canonical representative of t.
We say that t is closed if both FTV(t)=∅
and FV(t)=∅.
Because typing and term formation operations (abstraction,
application, …) are invariant under ≡, we may denote terms
by their (canonical) representatives and informally treat them
interchangeably.
We will often abuse notation to omit ⋅ and ∗. Thus, st can
refer to both s⋅t and s∗t. This is not ambiguous
due to typing. When writing σ[α:=τ] we
implicitly assume that α and τ have the same
kind. Analogously with t[x:=s].
Lemma 2.4** (Substitution lemma).**
If s:τ and x:σ and t:σ then
s[x:=t]:τ.
2. 2.
If t:σ then
t[α:=τ]:σ[α:=τ].
Proof 2.5**.**
Induction on the typing derivation.
Lemma 2.6** (Generation lemma).**
If t:σ then there is a type σ′ such that
σ′=βσ and FTV(σ′)⊆FTV(t) and
one of the following holds.
•
t≡x is a variable with (x:σ′)∈V.
•
t≡f is a function symbol with
f:σ′ in Σ.
•
t≡λx:τ1.s and
σ′=τ1→τ2 and s:τ2.
•
t≡Λα:κ.s and
σ′=∀α:κ.τ and s:τ and
α does not occur free in the type of a free variable
of s.
•
t≡t1⋅t2 and t1:τ→σ′
and t2:τ and FTV(τ)⊆FTV(t).
•
t≡s∗τ and
σ′=ρ[α:=τ] and
s:∀(α:κ).ρ and τ is a type
constructor of kind κ.
Proof 2.7**.**
By analysing the derivation t:σ. To ensure
FTV(σ′)⊆FTV(t), note that if
α∈/FTV(t) is of kind κ and t:σ′, then
t:σ′[α:=χκ] by the substitution lemma
(thus we can eliminate α).
3 Polymorphic Functional Systems
In this section, we present a form of higher-order term rewriting
systems based on Fω: Polymorphic Functional Systems
(PFSs). Systems of interest, such as logic systems like ICP2 and
higher-order TRSs with shallow or full polymorphism can be encoded
into PFSs, and then proved terminating with the technique we will
develop in Sections 4–6.
Definition 3**.**
Kinds, type constructors and types are defined
like in Definition 2, parameterised by a fixed
set ΣT=⋃κΣκT of type constructor
symbols.
Let Σ be a set of function symbols such
that for f:σ∈Σ:
[TABLE]
We define PFS terms as in Definition 2 (based
on Definition 1), parameterised by Σ, with
the restriction that for any subterm s⋅u of a term t,
we have s=fρ1…ρnu1…um
where:
[TABLE]
This definition does not allow for a variable or
abstraction to occur at the head of an application, nor can we have
terms of the form s⋅t∗τ⋅q (although terms of the
form s⋅t∗τ, or x∗τ with x a variable,
are allowed to occur). To stress this restriction, we will
use the notation
fρ1,…,ρn(s1,…,sm) as an alternative
way to denote
fρ1…ρns1…sm when
f:∀(α1:κ1)…∀(αn:κn).σ1→…→σk→τ
is a function symbol in Σ with τ a type atom and m≤k.
This allows us to represent terms in a “functional” way, where
application does not explicitly occur (only implicitly in the
construction of fρ1,…,ρn(s1,…,sm)).
The following result follows easily by induction on term
structure:
Lemma 3.1**.**
If t,s are PFS terms then so is t[x:=s].
PFS terms will be rewritten through a reduction relation
⟶R based on a (usually infinite) set of rewrite rules. To
define this relation, we need two additional notions.
Definition 4**.**
A replacement is a function δ=γ∘ω
satisfying:
ω is a type constructor substitution,
2. 2.
γ is a term substitution such that
γ(ω(x)):ω(τ) for every
(x:τ)∈V.
For τ a type constructor, we use δ(τ) to denote
ω(τ). We use the notation
δ[x:=t]=γ[x:=t]∘ω. Note
that if t:τ then δ(t):δ(τ).
Definition 5**.**
A σ-contextCσ is a PFS term with a fresh function
symbol □σ∈/Σ of type σ occurring
exactly once. By Cσ[t] we denote a PFS term obtained
from Cσ by substituting t for □σ. We drop the
σ subscripts when clear or irrelevant.
Now, the rewrite rules are simply a set of term pairs, whose
monotonic closure generates the rewrite relation.
Definition 6**.**
A set R of term pairs (ℓ,r) is a set of rewrite
rules if: (a) FV(r)⊆FV(ℓ); (b) ℓ and r
have the same type; and (c) if (ℓ,r)∈R
then (δ(ℓ),δ(r))∈R for any
replacement δ. The reduction relation ⟶R
on PFS terms is defined by:
t⟶Rs iff t=C[ℓ] and s=C[r] for some (ℓ,r)∈R and
context C.
Definition 7**.**
A Polymorphic Functional System (PFS) is a triple
(ΣT,Σ,R) where ΣT is a set of type
constructor symbols, Σ a set of function symbols (restricted
as in Def. 3), and R is a set
of rules as in Definition 6. A term of a
PFS A is referred to as an A-term.
While PFS-terms are a restriction from the general terms
of system Fω, the reduction relation allows us to actually encode,
e.g., system F as a PFS: we can do so by including the symbol
@:∀α∀β.(α→β)→α→β in Σ and adding all rules of the form
@σ,τ(λx.s,t)⟶s[x:=t].
Similarly, β-reduction of type abstraction can be modelled
by including a symbol
A:∀α:∗⇒∗.∀β.(∀γ.αγ)→αβ and rules
Aλγ.σ,τ(Λγ.s)⟶s[γ:=τ].111The use of a type constructor variable α of kind
∗⇒∗ makes it possible to do type substitution as part of
a rule.
An application s∗τ with s:∀γ.σ is
encoded as Aλγ.σ,τ(s), so
α is substituted with λγ.τ.
This is well-typed because (λγ.σ)γ=βσ and (λγ.σ)τ=βσ[γ:=τ].
We can also use rules
(Λα.s)∗τ⟶s[α:=τ] without the extra
symbol, but to apply our method it may be
convenient
to use the extra symbol, as
it creates more liberty in choosing an interpretation.
Example 3.2** (Fold on heterogenous lists).**
The example from the introduction may be represented as a PFS with
one type symbol List:∗, the following function symbols:
[TABLE]
and the following rules (which formally represents an
infinite set of rules: one rule for each choice of types σ,τ and PFS terms s, t, etc.):
[TABLE]
4 A well-ordered set of interpretation terms
In polynomial interpretations of first-order term
rewriting [20, Chapter 6.2], each term s is mapped to a
natural number [[s]], such that [[s]]>[[t]]
whenever s⟶Rt. In higher-order rewriting, this is not
practical; instead, following [14], terms are mapped to weakly
monotonic functionals according to their type (i.e., terms with a [math]-order
type are mapped to natural numbers, terms with a 1-order type to weakly
monotonic functions over natural numbers, terms with a 2-order type to
weakly monotonic functionals taking weakly monotonic functions as
arguments, and so on). In this paper, to account for full polymorphism,
we will interpret PFS terms to a set I of interpretation terms
in a specific extension of System Fω. This set is defined in Section
4.1; we provide a well-founded partial ordering ≻ on
I in Section 4.2.
Although our world of interpretation terms is quite different
from the weakly monotonic functionals of [14], there are many
similarities. Most pertinently, every interpretation term λx.s
essentially defines a weakly monotonic function from I to
I. This, and the use of both addition and multiplication in
the definition of I, makes it possible to lift higher-order
polynomial interpretations [5] to our setting. We
prove weak monotonicity in Section 4.3.
4.1 Interpretation terms
Definition 8**.**
The set Y of interpretation types is the set of types
as in Definition 2 with ΣT={Nature:∗},
i.e., there is a single type constant Nature. Then χ∗=Nature.
The set I of interpretation terms is the set of terms
from Definition 2 (see also
Definition 1) where as types we take the
interpretation types and for the set Σ of function symbols we
take Σ={n:Nature∣n∈N}∪Σf, where
Σf={⊕:∀α.α→α→α,⊗:∀α.α→α→α,flatten:∀α.α→Nature,lift:∀α.Nature→α}.
For easier presentation, we write ⊕τ, ⊗τ, etc.,
instead of ⊕∗τ, ⊗∗τ, etc. We will
also use ⊕ and ⊗ in infix, left-associative
notation, and omit the type denotation where it is clear from
context. Thus, s⊕t⊕u should be read as
⊕σ(⊕σst)u if s has type
σ. Thus, our interpretation terms include natural
numbers with the operations of addition and multiplication. It would
not cause any fundamental problems to add more monotonic operations, e.g.,
exponentiation, but we refrain from doing so for the sake of
simplicity.
Normalising interpretation terms
The set I of interpretation terms can be reduced through
a relation ⇝, that we will define below. This relation will
be a powerful aid in defining the partial ordering ≻ in Section
4.2.
Definition 9**.**
We define the relation ⇝ on interpretation terms as the
smallest relation on I for which the following properties
are satisfied:
if s⇝t then both λx.s⇝λx.t and
Λα.s⇝Λα.t
2. 2.
if s⇝t then u⋅s⇝u⋅t
3. 3.
if s⇝t then both s⋅u⇝t⋅u and
s∗σ⇝t∗σ
4. 4.
(λx:σ.s)⋅t⇝s[x:=t]
and
(Λα.s)∗σ⇝s[α:=σ]
(β-reduction)
5. 5.
Recall Definition 2 and Definition 8 of
the set of interpretation terms I as the set of the
equivalence classes of ≡. So, for instance,
liftNature above denotes
the equivalence class of all preterms liftσ with
σ=βNature. Hence, the above rules are invariant
under ≡ (by confluence of β-reduction on types), and
they correctly define a relation on interpretation terms. We say
that s is a redex if s reduces by one of the rules 4–13.
A final interpretation term is an interpretation term s∈I such that (a) s is closed, and (b) s is in normal form
with respect to ⇝. We let If be the set of all final
interpretation terms. By Iτ (Iτf) we denote
the set of all (final) interpretation terms of interpretation
type τ.
An important difference with System Fω and related ones is that
the rules for ⊕τ, ⊗τ, flattenτ and
liftτ depend on the type τ. In particular, type
substitution in terms may create redexes. For instance, if α is
a type variable then ⊕αt1t2 is not a redex, but
⊕σ→τt1t2 is. This makes the question of
termination subtle. Indeed, System Fω is extremely sensitive to
modifications which are not of a logical nature. For instance, adding
a constant J:∀αβ.α→β
with a reduction rule
Jττ⇝λx:τ.x makes the system
non-terminating [7]. This rule breaks parametricity by
making it possible to compare two arbitrary types. Our rules do not allow such a
definition. Moreover, the natural number constants cannot be
distinguished “inside” the system. In other words, we could
replace all natural number constants with 0 and this would not
change the reduction behaviour of terms. So for the purposes of
termination, the type Nature is essentially a singleton. This
implies that, while we have polymorphic functions between an
arbitrary type α and Nature which are not constant when seen
“from outside” the system, they are constant for the purposes of
reduction “inside” the system (as they would have to be in a
parametric Fω-like system). Intuitively, these properties of
our system ensure that it stays “close enough” to Fω so
that the standard termination proof still generalises.
Now we state some properties of ⇝, including strong
normalisation. Because of space limitations, most (complete)
proofs are delegated to
Appendix A.1.
Lemma 4.1** (Subject reduction).**
If t:τ and t⇝t′ then t′:τ.
Proof 4.2**.**
By induction on the definition of t⇝t′, using
Lemmas 2.4 and 2.6.
Theorem 4.3**.**
If t:σ then t is terminating with respect to ⇝.
Proof 4.4**.**
By an adaptation of the Tait-Girard computability method. The proof
is an adaptation of chapters 6 and 14 from the
book [6], and chapters 10 and 11 from the
book [16].
Details are available in
Appendix A.1.
Lemma 4.5**.**
Every term s∈I has a unique normal form s↓. If s
is closed then so is s↓.
Proof 4.6**.**
One easily
checks that ⇝ is locally confluent. Since the
relation is
terminating by Theorem 4.3, it is confluent by Newman’s
lemma.
Lemma 4.7**.**
The only final interpretation terms of type Nature are the natural
numbers.
Example 4.8**.**
Let s∈INature→Nature and t∈INature. Then we can reduce
(s⊕liftNature→Nature(1))⋅t⇝(λx.sx⊕liftNature→Nature(1)x)⋅t⇝st⊕liftNature→Nature(1)t⇝st⊕(λy.liftNature(1))t⇝st⊕liftNature(1)⇝st⊕1. If s and t are variables, this term is in normal
form.
4.2 The ordering pair (⪰,≻)
With these ingredients, we are ready to define the well-founded
partial ordering ≻ on I. In fact, we will do more: rather
than a single partial ordering, we will define an ordering pair: a
pair of a quasi-ordering ⪰ and a compatible well-founded ordering
≻. The quasi-ordering ⪰ often makes it easier to prove
s≻t, since it suffices to show that s⪰s′≻t′⪰t for some interpretation terms s′,t′. Having ⪰ will
also allow us to use rule removal (Theorem 6.1).
Definition 10**.**
Let R∈{≻0,⪰0}. For closeds,t∈Iσ
and closed σ in β-normal form, the relation
sRσt is defined coinductively by the following rules.
[TABLE]
We define s≈σ0t if both s⪰σ0t and
t⪰σ0s. We drop the type subscripts when clear or
irrelevant.
Note that in the case for Nature the terms s↓, t↓ are natural
numbers by Lemma 4.7 (s↓,t↓ are closed and in
normal form, so they are final interpretation terms).
Intuitively, the above definition means that e.g. s≻0t iff
there exists a possibly infinite derivation tree using the above
rules. In such a derivation tree all leaves must witness s↓>t↓
in natural numbers. However, this also allows for infinite branches,
which solves the problem of repeating types due to impredicative
polymorphism. If e.g. s≻∀α.α0t then
s∗∀α.α≻∀α.α0t∗∀α.α, which forces an infinite branch in
the derivation tree. According to our definition, any infinite branch
may essentially be ignored.
Formally, the above coinductive definition of e.g. ≻σ0
may be interpreted as defining the largest relation such that if s≻σ0t then:
•
σ=Nature and s↓>t↓ in N, or
•
σ=τ1→τ2 and
s⋅q≻τ20t⋅q for all
q∈Iτ1f, or
•
σ=∀(α:κ).ρ and
s∗τ≻nfβ(ρ[α:=τ])0t∗τ for all closed τ∈Tκ.
For more background on coinduction see
e.g. [13, 15, 9]. In this
paper we use a few simple coinductive proofs to establish the basic
properties of ≻ and ⪰. Later, we just use these
properties and the details of the definition do not matter.
Definition 11**.**
A closureC=γ∘ω is a
replacement such that ω(α) is closed for each
type constructor variable α, and γ(x) is closed for
each term variable x.
For arbitrary types σ and arbitrary terms s,t∈I
we define s≻σt if for every closure C we can
obtain C(s)≻nfβ(C(σ))cC(t)
coinductively with the above rules. The relations ⪰σ
and ≈σ are defined analogously.
Note that for closed s,t and closed σ in β-normal form,
s≻σt iff s≻σ0t (and analogously
for ⪰,≈). In this case we shall often omit the
superscript [math].
The definition of ≻ and ⪰ may be reformulated as
follows.
Lemma 4.9**.**
t⪰s if and only if for every closure C and every
sequence u1,…,un of closed terms and closed type
constructors such that C(t)u1…un:Nature we have
(C(t)u1…un)↓≥(C(s)u1…un)↓ in
natural numbers. An analogous result holds with ≻ or ≈
instead of ⪰.
Proof 4.10**.**
The direction from left to right follows by induction on n; the
other by coinduction.
In what follows, all proofs by coinduction could be reformulated to
instead use the lemma above. However, this would arguably make the
proofs less perspicuous. Moreover, a coinductive definition is better
suited for a formalisation – the coinductive proofs here could be
written in Coq almost verbatim.
Our next task is to show that ⪰ and ≻ have the
desired properties of an ordering pair; e.g., transitivity and
compatibility. We first state a simple lemma that will be used
implicitly.
Lemma 4.11**.**
If τ∈Y is closed and β-normal, then
τ=Nature or τ=τ1→τ2 or
τ=∀ασ.
Lemma 4.12**.**
≻ is well-founded.
Proof 4.13**.**
It suffices to show this for closed terms and closed types in
β-normal form, because any infinite sequence t1≻τt2≻τt3≻τ… induces an infinite sequence
C(t1)≻nfβ(C(τ))C(t2)≻nfβ(C(τ))C(t3)≻nfβ(C(τ))… for any closure C. By induction on the size of a
β-normal type τ (with size measured as the number of
occurrences of ∀ and →) one proves that there does
not exist an infinite sequence t1≻τt2≻τt3≻τ… For instance, if α has kind κ and
t1≻∀ατt2≻∀ατt3≻∀ατ… then t1∗χκ≻τ′t2∗χκ≻τ′t3∗χκ≻τ′…, where
τ′=nfβ(τ[α:=χκ]). Because τ
is in β-normal form, all redexes in
τ[α:=χκ] are created by the substitution
and must have the form χκu. Hence, by the definition
of χκ (see Definition 2) the
type τ′ is smaller than τ. This
contradicts the inductive hypothesis.
Lemma 4.14**.**
Both ≻ and ⪰ are transitive.
Proof 4.15**.**
We show this for ≻, the proof for ⪰ being
analogous. Again, it suffices to prove this for closed
terms and closed types in β-normal form. We proceed by
coinduction.
If t1≻Naturet2≻Naturet3 then t1↓>t2↓>t3↓, so t1↓>t3↓. Thus t1≻Naturet3.
If t1≻σ→τt2≻σ→τt3
then t1⋅q≻τt2⋅q≻τt3⋅q
for q∈Iσf. Hence
t1⋅q≻τt3⋅q for q∈Iσf by
the coinductive hypothesis. Thus t1≻σ→τt3.
If t1≻∀(α:κ)σt2≻∀(α:κ)σt3
then
t1∗τ≻σ′t2∗τ≻σ′t3∗τ
for any closed τ of kind κ, where
σ′=nfβ(σ[α:=τ]). By the
coinductive hypothesis
t1∗τ≻σ′t3∗τ; thus
t1≻∀ασt3.
Lemma 4.16**.**
⪰ is reflexive.
Proof 4.17**.**
By coinduction one shows that ⪰σ is reflexive on
closed terms for closed β-normal σ. The case
of ⪰ is then immediate from definitions.
Lemma 4.18**.**
The relations ⪰ and ≻ are compatible, i.e., ≻⋅⪰⊆≻ and ⪰⋅≻⊆≻.
Proof 4.19**.**
By coinduction, analogous to the transitivity proof.
Lemma 4.20**.**
If t≻s then t⪰s.
Proof 4.21**.**
By coinduction.
Lemma 4.22**.**
If t⇝s then t≈s.
Proof 4.23**.**
Follows from Lemma 4.9, noting that t⇝s
implies C(t)⇝C(s) for all closures C.
Lemma 4.24**.**
Assume t≻s (resp. t⪰s). If t⇝t′ or
t′⇝t then t′≻s (resp. t′⪰s). If
s⇝s′ or s′⇝s then t≻s′
(resp. t⪰s′).
Proof 4.25**.**
Follows from Lemma 4.22, transitivity and
compatibility.
Corollary 4.26**.**
For R∈{≻,⪰,≈}: sRt if and only if
s↓Rt↓.
Example 4.27**.**
We can prove that x⊕liftNature→Nature(1)≻x: by
definition, this holds if s⊕liftNature→Nature(1)≻s for all closed s, so if (s⊕liftNature→Nature(1))u≻su for all closed s,u.
Following Example 4.8 and Lemma 4.24,
this holds if su⊕1≻su. By definition, this is the
case if (su⊕1)↓>(su)↓ in the natural numbers,
which clearly holds for any s,u.
4.3 Weak monotonicity
We will now show that s⪰s′ implies t[x:=s]⪰t[x:=s′] (weak monotonicity).
For this purpose, we prove a few lemmas, many of
which also apply to ≻, stating the preservation of ⪰
under term formation operations. We will need these results in the next section.
Lemma 4.28**.**
For R∈{⪰,≻}: if tRs then tuRsu with
u a term or type constructor.
Proof 4.29**.**
Follows from definitions.
Lemma 4.30**.**
For R∈{⪰,≻}: if nRm then
liftσnRliftσm for all types σ.
Proof 4.31**.**
Without loss of generality we may assume σ closed and in
β-normal form. By coinduction we show
lift(n)u1…uk⪰lift(m)u1…uk for closed
u1,…,uk. First note that
(liftt)u1…uk⇝∗lift(t) (with a different
type subscript in lift on the right side, omitted for
conciseness). If σ=Nature then
(lift(n)u1…uk)↓=n≥m=(lift(m)u1…uk)↓. If σ=τ1→τ2 then by the coinductive
hypothesis
lift(n)u1…ukq⪰τ2lift(m)u1…ukq for any q∈Iτ1f, so
lift(n)u1…uk⪰σlift(m)u1…uk
by definition. If σ=∀(α:κ)τ then by the
coinductive hypothesis
lift(n)u1…ukξ⪰σ′lift(m)u1…ukξ for any closed ξ∈Tκ, where
σ′=τ[α:=ξ]. Hence
lift(n)u1…uk⪰σlift(m)u1…uk
by definition.
Lemma 4.32**.**
For R∈{⪰,≻}: if tRσs then
flattenσtRNatureflattenσs for all types
σ.
Proof 4.33**.**
Without loss of generality we may assume σ is closed and in
β-normal form. Using Lemma 4.24, the lemma
follows by induction on σ.
Lemma 4.34**.**
For R∈{⪰,≻}: if tRs then
λx.tRλx.s and
Λα.tRΛα.s.
Proof 4.35**.**
Assume t⪰τs and x:σ. Let C
be a closure. We need to show
C(λx.t)⪰C(σ→τ)C(λx.s). Let u∈IC(σ)f. Then
C′=C[x:=u] is a closure and
C′(t)⪰C(τ)C′(s). Hence
C(t)[x:=u]⪰C(τ)C(s)[x:=u]. By
Lemma 4.24 this implies
C(λx.t)u⪰C(τ)C(λx.s)u. Therefore
C(λx.t)⪰C(σ→τ)C(λx.s). The proof for ≻ is analogous.
Lemma 4.36**.**
Let s,t,u be terms of type σ.
If s⪰t then s⊕σu⪰t⊕σu, u⊕σs⪰u⊕σt,
s⊗σu⪰t⊗σu, and u⊗σs⪰u⊗σt.
2. 2.
If s≻t then s⊕σu≻t⊕σu and u⊕σs≻u⊕σt. Moreover, if
additionally u⪰liftσ(1) then also s⊗σu≻t⊗σu and u⊗σs≻u⊗σt.
Proof 4.37**.**
It suffices to prove this for closed s,t,u and closed σ in
β-normal form. The proof is similar to the proof of
Lemma 4.30. For instance, we show by coinduction
that for closed w1,…,wn (denoted w): if
sw≻tw and uw⪰lift(1)w
then (s⊗u)w≻(t⊗u)w.
The following lemma depends on the lemmas above. The full proof may be
found in
Appendix A.2.
The proof is actually quite
complex, and uses a method similar to Girard’s method of candidates
for the termination proof.
Lemma 4.38** (Weak monotonicity).**
If s⪰s′ then t[x:=s]⪰t[x:=s′].
Corollary 4.39**.**
If s⪰s′ then ts⪰ts′.
5 A reduction pair for PFS terms
Recall that our goal is to prove termination of reduction in
a PFS. To
do so, in this section we will define a systematic way to generate
reduction pairs. We fix a PFS A, and define:
Definition 12**.**
A binary relation R on A-terms is monotonic if R(s,t)
implies R(C[s],C[t]) for every context C (we assume s,t have
the same type σ).
A reduction pair is a pair (⪰A,≻A) of a
quasi-order ⪰A on A-terms and a well-founded
ordering ≻A on A-terms such that:
(a)
⪰A and ≻A are compatible, i.e., ≻A⋅⪰A⊆≻A and ⪰A⋅≻A⊆≻A,
and (b)
⪰A and ≻A are both monotonic.
If we can generate such a pair with ℓ≻Ar for each
rule (ℓ,r)∈R, then we easily see that the PFS A is
terminating. (If we merely have ℓ≻Ar for some
rules and ℓ⪰Ar for the rest, we can still progress
with the termination proof, as we will discuss in Section
6.)
To generate this pair, we will define the notion of an
interpretation from the set of A-terms to the set I of
interpretation terms, and thus lift the ordering pair (⪰,≻)
to A.
In the next section, we will show how this reduction pair can be used
in practice to prove termination of PFSs.
One of the core ingredients of our interpretation function is a
mapping to translate types:
Definition 13**.**
A type constructor mapping is a function TM which
maps each type constructor symbol to a closed interpretation type
constructor of the same kind. A fixed type constructor mapping
TM is extended inductively to a function from type
constructors to closed interpretation type constructors in the
expected way. We denote the extended interpretation (type)
mapping by [[σ]]. Thus,
e.g. [[∀α.σ]]=∀α.[[σ]] and [[σ→τ]]=[[σ]]→[[τ]].
Lemma 5.1**.**
[[σ]][α:=[[τ]]]=[[σ[α:=τ]]]
Proof 5.2**.**
Induction on σ.
Similarly, we employ a symbol mapping as the key
ingredient to interpret PFS terms.
Definition 14**.**
Given a fixed type constructor mapping TM, a symbol
mapping is a function J which assigns to each function
symbol f:ρ a closed interpretation term
J(f) of type [[ρ]]. For a fixed
symbol mapping J, we define the interpretation
mapping[[s]] inductively:
[TABLE]
Note that [[σ]],[[τ]] above depend
on TM. Essentially, [[⋅]] substitutes
TM(c) for type constructor symbols c, and
J(f) for function symbols f, thus mapping
A-terms to interpretation terms. This translation preserves typing:
For all s,t,x,α,τ:
[[s]][α:=[[τ]]]=[[s[α:=τ]]]
and
[[s]][x:=[[t]]]=[[s[x:=t]]].
Proof 5.6**.**
Induction on s.
Definition 15**.**
For a fixed type constructor mapping TM and symbol mapping
J, the interpretation pair(⪰J,≻J) is defined as follows: s⪰Jt if [[s]]⪰[[t]], and s≻Jt if [[s]]≻[[t]].
Remark 5.7**.**
The polymorphic lambda-calculus has a much greater expressive power
than the simply-typed lambda-calculus. Inductive data types
may be encoded, along with their constructors and recursors with
appropriate derived reduction rules. This makes
our
interpretation method easier to apply, even in the non-polymorphic
setting, thanks to more
sophisticated “programming” in the interpretations.
The reader is advised to consult e.g. [6, Chapter 11]
for more background and explanations. We demonstrate the idea
by presenting an encoding for the recursive type List and its
fold-left function (see also
Ex. 5.15).
Example 5.8**.**
Towards a termination proof of Example 3.2,
we set TM(List)=∀β.(∀α.β→α→β)→β→β and
J(nil)=Λβ.λf:∀α.β→α→β.λx:β.x. If we additionally choose
J(foldl)=Λβ.λf.λx.λl.lβfx⊕liftβ(1), we have
[[foldlσ(f,s,nil)]]=(Λβ.λf.λx.λl.lβfx⊕liftβ(1))[[σ]]fs(Λβ.λf.λx.x)⇝∗s⊕lift[[σ]](1) by
β-reduction steps.
An extension of the proof from Example 4.27 shows that
this term ≻[[s]].
It is easy to see that ⪰J and
≻J have desirable properties such as transitivity,
reflexivity (for ⪰J) and well-foundedness (for
≻J). However, ≻J is not necessarily
monotonic. Using the interpretation from Example 5.8,
[[foldlσ(λx.s,t,nil)]]=[[foldσ(λx.w,t,nil)]] regardless of
s and w, so a reduction in s would not cause a decrease in
≻J. To obtain a reduction pair, we must impose certain
conditions on J; in particular, we will require that
J is safe.
Definition 16**.**
If s1≻s2 implies t[x:=s1]≻t[x:=s2], then the interpretation term t is safe
for x. A symbol mapping J is safe if for all
f:∀(α1:κ1)…∀(αn:κn).σ1→…→σk→τ
with τ a type atom we have: J(f)=Λα1…αn.λx1…xk.t with t
safe for each xi.
Lemma 5.9**.**
xu1…um is safe for x.
2. 2.
If t is safe for x then so are lift(t)
and flatten(t).
3. 3.
If s1 is safe for x or s2 is safe for x then s1⊕s2 is safe for x.
4. 4.
If either
(a)
s1 is safe for x and s2⪰lift(1), or
(b)
s2 is safe for x and s1⪰lift(1),
then s1⊗s2 is safe for x.
5. 5.
If t is safe for x then so is Λα.t
and λy.t (y=x).
Proof 5.10**.**
Each point follows from one of the lemmas proven before,
Lemma 4.20, Lemma 4.38,
Lemma 4.18 and the transitivity of ⪰. For
instance, for the first, assume s1≻s2 and let
uij=ui[x:=sj]. Then (xu1…um)[x:=s1]=s1u11…um1. By
Lemma 4.28 we have s1u11…um1≻s2u11…um1. By Lemma 4.20 and
Lemma 4.38 we have ui1⪰ui2. By
Corollary 4.39 and the transitivity of ⪰ we
obtain s2u11…um1⪰s2u12…um2. By
Lemma 4.18 finally (xu1…um)[x:=s1]=s1u11…um1≻s2u12…um2=(xu1…um)[x:=s2].
Lemma 5.11**.**
If J is safe then ≻J is monotonic.
Proof 5.12**.**
Assume s1≻Js2. By induction on
a context C we show C[s1]≻JC[s2]. If C=□ then
this is obvious. If C=λx.C′ or C=Λα.C′
then C′[s1]≻JC′[s2] by the inductive hypothesis,
and thus C[s1]≻JC[s2] follows from
Lemma 4.34 and definitions. If C=C′t then
C′[s1]≻JC′[s2] by the inductive hypothesis,
so C[s1]≻JC[s2] follows from definitions.
Finally, assume C=t⋅C′. Then t=fρ1…ρnt1…tm where
f:∀(α1:κ1)…∀(αn:κn).σ1→…→σk→τ
with τ a type atom, m<k, and J(f)=Λα1…αn.λx1…xk.u with u
safe for each xi. Without loss of generality assume m=k−1. Then
[[C[si]]]⇝u′[xk:=[[C′[si]]]]
where
u′=u[α1:=[[ρ1]]]…[αn:=[[ρn]]][x1:=[[t1]]]…[xk−1:=[[tk−1]]]. By
the inductive hypothesis [[C′[s1]]]≻[[C′[s2]]]. Hence u′[xk:=[[C′[s1]]]]≻u′[xk:=[[C′[s2]]]], because u is safe
for xk. Thus [[C[s1]]]≻[[C[s2]]] by
Lemma 4.24.
Theorem 5.13**.**
If J is safe then (⪰J,≻J) is a
reduction pair.
Proof 5.14**.**
By Lemmas 4.14 and 4.16,
⪰J is a
quasi-order. Lemmas 4.12
and 4.14 imply that ≻J is a
well-founded ordering. Compatibility follows from
Lemma 4.18. Monotonicity of ⪰J
follows from Lemma 4.38. Monotonicity
of ≻J follows from
Lemma 5.11.
Example 5.15**.**
The following is a safe interpretation for the PFS from
Example 3.2:
[TABLE]
Note that J(cons) is not required to be safe
for x, since x is not an argument of cons:
following its declaration, cons takes one type and two terms
as arguments. The variable x is only part of the interpretation.
Note also that the current interpretation is a mostly straightforward
extension of Example 5.8: we retain the same core
interpretations (which, intuitively, encode @ and
A as forms of application and encode a list as the function
that executes a fold over the list’s contents), but we add a clause
⊕lift(flatten(x)) for each argument x that the initial
interpretation is not safe for. The only further change is that, in
J(cons), the part between brackets has to be extended.
This was necessitated by the change to J(foldl), in
order for the rules to still be oriented (as we will do in
Example 6.7).
6 Proving termination with rule removal
A PFS A is certainly terminating if its reduction relation
⟶R is contained in a well-founded relation, which holds if
ℓ≻Jr for all its rules (ℓ,r). However,
sometimes it is cumbersome to find an interpretation that orients all
rules strictly. To illustrate, the interpretation of Example
5.15 gives ℓ≻Jr for two of
the rules and ℓ⪰Jr for the others (as we will see
in Example 6.7). In such cases, proof progress is still
achieved through rule removal.
Theorem 6.1**.**
Let R=R1∪R2, and suppose that
R1⊆≻R and
R2⊆⪰R for a reduction pair
(⪰R,≻R). Then ⟶R is terminating
if and only if ⟶R2 is
(so certainly if R2=∅).
Proof 6.2**.**
Monotonicity of ⪰R and ≻R implies that
⟶R1⊆≻R and
⟶R2⊆⪰R.
By well-foundedness of ≻R, compatibility
of ⪰R and ≻R, and transitivity
of ⪰R, every infinite ⟶R sequence can
contain only finitely many ⟶R1 steps.
The above theorem gives rise to the following rule removal
algorithm:
While R is non-empty:
(a)
Construct a reduction pair (⪰R,≻R)
such that all rules in R are oriented by ⪰R or
≻R, and at least one of them is oriented using
≻R.
2. (b)
Remove all rules ordered by ≻R from R.
If this algorithm succeeds, we have proven termination.
To use this algorithm with the pair (⪰J,≻J)
from Section 5, we should identify an
interpretation (TM,J)
such that (a) J is safe, (b) all rules can be oriented with
⪰J or ≻J, and (c) at least one rule is
oriented with ≻J.
The first requirement guarantees that
(⪰J,≻J) is a reduction pair (by
Theorem 5.13). Lemma 5.9 provides some
sufficient safety criteria. The second and third
requirements have to be verified for each individual rule.
Example 6.3**.**
We continue with our example of fold on heterogeneous lists. We prove
termination by rule removal, using the symbol mapping from
Example 5.15.
We will show:
[TABLE]
Consider the first inequality; by definition it holds if
\llbracket@σ,τ(λx:σ.s,t)]]⪰[[s[x:=t]]].
Since \llbracket@σ,τ(λx:σ.s,t)]]⇝∗[[s]][x:=[[t]]]⊕lift[[τ]](flatten[[σ]]([[t]])), and [[s]][x:=[[t]]]=[[s[x:=t]]] (by Lemma 5.5),
it suffices by Lemma 4.22 if
[[s[x:=t]]]⊕lift[[τ]](flatten[[σ]]([[t]]))⪰[[s[x:=t]]].
This is an instance of the general rule u⊕w⪰u that
we will obtain below.
To prove inequalities s≻t and s⪰t, we will often
use that ≻ and ⪰ are transitive and compatible with each
other (Lem. 4.14 and 4.18), that
⇝⊆≈ (Lem. 4.22),
that ⪰ is monotonic (Lem. 4.38),
that both ≻ and ⪰ are monotonic over lift and flatten
(Lem. 4.30 and 4.32) and that
interpretations respect substitution
(Lem. 5.5). We will also use
Lemma 4.36 which states (among other things)
that s≻t implies s⊕u≻t⊕u.
In addition, we can use the
calculation rules below. The proofs may be found in
Appendix A.3.
Lemma 6.4**.**
For all types σ and all terms s,t,u of type σ, we
have:
s⊕σt≈t⊕σs and s⊗σt≈t⊗σs;
2. 2.
s⊕σ(t⊕σu)≈(s⊕σt)⊕σu and s⊗σ(t⊗σu)≈(s⊗σt)⊗σu;
3. 3.
s⊗σ(t⊕σu)≈(s⊗σt)⊕σ(s⊗σu);
4. 4.
(liftσ0)⊕σs≈s and (liftσ1)⊗σs≈s.
Lemma 6.5**.**
liftσ(n+m)≈σ(liftσn)⊕σ(liftσm);
2. 2.
liftσ(nm)≈σ(liftσn)⊗σ(liftσm);
3. 3.
flattenσ(liftσ(n))≈n.
Lemma 6.6**.**
For all types σ, terms s,t of type σ and natural
numbers n>0:
s⊕σt⪰s and s⊕σt⪰t;
2. 2.
s⊕σ(liftσn)≻s and
(liftσn)⊕σt≻t.
Note that these calculation rules immediately give the
inequality x⊕liftnat→Nature(1)≻x from
Example 4.27, and also that liftσ(n)≻liftσ(m) whenever n>m. By
Lemmas 4.36 and 6.6 we
can use absolute positiveness: the property that
(a) s⪰t if we can write s≈s1⊕⋯⊕sn and t≈t1⊕⋯⊕tk with k≤n and
si⪰ti for all i≤k, and (b) if moreover s1≻t1 then s≻t. This property is typically very
useful to dispense the obligations obtained in a termination proof with
polynomial interpretations.
Example 6.7**.**
We now have the tools to finish the example of
heterogeneous lists (still using the interpretation from
Example 5.15). The proof obligation from Example
6.3, that
\llbracket@σ,τ(λx:σ.s,t)]]⪰[[s[x:=t]]], is completed by
Lemma 6.6(1).
We have [[Aλα.σ,τ(Λα.s)]]≈[[Λα.s]]∗[[τ]]≈[[s[α:=τ]]] by Lemma
5.5, and
[[foldlσ(f,s,nil)]]=[[nil]]∗[[σ]]⋅[[f]]⋅[[s]]⊕lift[[σ]](⟨something⟩⊕1)≈[[s]]⊕lift[[σ]](⟨something⟩⊕1)≻[[s]] by Lemmas
6.5(1) and
6.6(1).
For the last rule note that (using only Lemmas
4.22 and
6.5(1)):
[TABLE]
On the right-hand side of the inequality, noting that
liftσ→τ(u)⋅w⇝∗liftτ(u), we have:
[TABLE]
Now the right-hand side is the left-hand side ⊕lift(1).
Clearly, the rule is oriented with ≻. Thus, we may remove the
last two rules, and continue the rule removal algorithm with only the
first two, which together define β-reduction. This is trivial,
for instance with an interpretation
J(@)=Λα.Λβ.λf.λx.(f⋅x)⊕liftβ(flattenα(x)⊕1) and
J(A)=Λα.Λβ.λx.x∗β⊕liftαβ(1).
7 A larger example
System F is System Fω where no higher kinds are
allowed, i.e., there are no type constructors except types. By the
Curry-Howard isomorphism F corresponds to the
universal-implicational fragment of intuitionistic second-order
propositional logic, with the types corresponding to formulas and
terms to natural deduction proofs. The remaining connectives may be
encoded in F, but the permutative conversion rules do not
hold [6].
In this section we show
termination of the system IPC2
(see [17]) of intuitionistic second-order
propositional logic with all connectives and permutative conversions,
minus a few of the permutative conversion rules for the existential
quantifier. The paper [17] depends on
termination of IPC2, citing a proof from [26], which,
however, later turned out to be incorrect. Termination of
Curry-style IPC2 without ⊥ as primitive was shown
in [19]. To our knowledge, termination of the full
system IPC2 remains an open problem, strictly speaking.
Remark 7.1**.**
Our method builds on the work of van de Pol and Schwichtenberg, who used
higher-order polynomial interpretations to prove termination of a
fragment of intuitionistic first-order logic with permutative
conversions [23], in the hope of providing a
more perspicuous proof of this well-known result. Notably, they did
not treat disjunction, as we will do. More fundamentally, their method
cannot handle impredicative polymorphism necessary for second-order
logic.
The system IPC2 can be seen as a PFS with type constructors:
[TABLE]
We have the following function symbols:
[TABLE]
The types represent formulas in intuitionistic second-order
propositional logic, and the terms represent proofs. For example, a
term caseσ,τ,ρsuv is a proof term of
the formula ρ, built from a proof s of
orστ, a proof u that σ implies ρ
and a proof v that τ implies ρ. Proof terms can be
simplified using 28 reduction rules, including the following (the full
set of rules is available in
Appendix B):
[TABLE]
[TABLE]
To define an interpretation for IPC2, we will use the
standard encoding of
product and existential types (see [6, Chapter 11] for
more details).
[TABLE]
We do not currently have an algorithmic method to find a
suitable interpretation. Instead, we used the following manual process.
We start by noting the minimal requirements given by the first set of
rules (e.g., that prσ,τ1(pairσ,τ(s,t))⪰s); to orient these inequalities, it would be good to for
instance have [[pairσ,τ(s,t)]]⪰⟨[[s]],[[t]]⟩[[σ]],[[τ]] and [[prσ,τi(s)]]=π[[σ]],[[τ]]i([[s]]).
To make the interpretation safe, we additionally include clauses
lift(flatten(x)) for any unsafe arguments x; to make the rules
strictly oriented, we include clauses lift(1). Unfortunately, this approach does not suffice to orient the rules
where some terms are duplicated, such as the second- and third-last
rules. To handle these rules, we multiply the first argument
of several symbols with the second (and possibly third). Some further
tweaking gives the following safe interpretation, which orients most
of the rules:
[TABLE]
[TABLE]
[TABLE]
Above, ⊗ binds stronger than ⊕. The derivations to
orient rules with these interpretations are also given in
Appendix B.
The only rules that are not oriented with this interpretation – not
with ⪰ either – are the ones of the form
f(let(s,t),…)⟶let(s,f(t,…)), like
the rule marked (*) above. Nonetheless, this is already a significant
step towards a systematic, extensible methodology of termination proofs
for IPC2 and similar systems of higher-order logic. Verifying the
orientations is still tedious, but our method raises hope for at least
partial automation, as was done with polynomial interpretations for
non-polymorphic higher-order rewriting [5].
8 Conclusions and future work
We introduced a powerful and systematic methodology to prove
termination of higher-order rewriting with full impredicative
polymorphism. To use the method one just needs to invent safe
interpretations and verify the orientation of the rules with the
calculation rules.
As the method is tedious to apply manually for larger systems, a
natural direction for future work is to look into automation: both for
automatic verification that a given interpretation suffices and –
building on existing termination provers for first- and higher-order
term rewriting – for automatically finding a suitable interpretation.
In addition, it would be worth exploring improvements of the method
that would allow us to handle the remaining rules of IPC2, or
extending other techniques for higher-order termination such as
orderings (see, e.g., [10]) or dependency pairs
(e.g., [12, 18]).
Appendix A Complete proofs
A.1 Strong Normalisation of ⇝
By SN we denote the set of all interpretation terms terminating
w.r.t. ⇝. We will use \a.s for either
λa.s or Λa.s, depending on typing.
For t∈SN by ν(t) we denote the length of the longest
reduction starting at t. The following lemma is obvious, but worth
stating explicitly.
Lemma A.1**.**
If \a.s⇝∗t, then t=\a.t′
and s⇝∗t′. If s∈SN then both λx.s and
Λα.s are also in SN.
Proof A.2**.**
We observe that every reduct of \x.s has the form
\x.s′ with s⇝s′, and analogously for
Λα.s. Thus, the first statement follows by induction
on the length of the reduction \a.s⇝∗t,
and the second statement by induction on ν(s).
Lemma A.3**.**
If t1,t2∈SN then ∘Naturet1t2∈SN for ∘∈{⊕,⊗}.
Proof A.4**.**
By induction on ν(t1)+ν(t2). Assume t1,t2∈SN. To
prove ∘Naturet1t2∈SN it suffices to show s∈SN
for all s such that ∘Naturet1t2⇝s. If s=∘Naturet1′t2 or s=∘Naturet1t2′ with ti⇝ti′ then we complete by the induction hypothesis. Otherwise s∈N is obviously in SN.
In the rest of this section we adapt Tait-Girard’s method of candidates
to prove termination of ⇝. The proof is an adaptation of
chapters 6 and 14 from the book [6], and chapters 10
and 11 from the book [16].
Definition 17**.**
A term t is neutral if there does not exist a sequence of
terms and types u1,…,un with n≥1 such that tu1…un is a redex (by ⇝).
By induction on the kind κ of a type constructor τ we
define the set Cτ of all candidates of type
constructor τ.
First assume κ=∗, i.e., τ is a type. A set X of
interpretation terms of type τ is a candidate of
type τ when:
X⊆SN;
2. 2.
if t∈X and t⇝t′ then t′∈X;
3. 3.
if t is neutral and for every t′ with t⇝t′ we
have t′∈X, then t∈X;
4. 4.
if t1,t2∈X then ∘τt1t2∈X for
∘∈{⊕,⊗};
5. 5.
if t∈SN and t:Nature then liftτt∈X;
6. 6.
if t∈X then flattenτt∈SN.
Note that item 3 above implies:
•
if t is neutral and in normal form then t∈X.
Now assume κ=κ1⇒κ2. A function f:Tκ1×⋃ξ∈Tκ1Cξ→⋃ξ∈Tκ2Cξ is a candidate of type
constructor τ if for every closed type constructor σ
of kind κ1 and a candidate X∈Cσ we have
f(σ,X)∈Cτσ.
Note that the elements of a candidate of type τ are required to
have type τ.
Lemma A.5**.**
If σ=βσ′ then Cσ=Cσ′.
Proof A.6**.**
Induction on the kind of σ.
Definition 18**.**
Let ω be a mapping from type constructor variables to type
constructors (respecting kinds). The mapping ω extends in an
obvious way to a mapping from type constructors to type
constructors. A mapping ω is closed for σ if
ω(α) is closed for α∈FTV(σ) (then
ω(σ) is closed).
An ω-valuation is a mapping ξ from type
constructor variables to candidates such that ξ(α)∈Cω(α).
For each type constructor σ, each mapping ω closed
for σ, and each ω-valuation ξ, the set
[[σ]]ξω is defined by induction on σ:
•
[[α]]ξω=ξ(α) for a type
constructor variable α,
•
[[Nature]]ξω is the set of all terms t∈SN
such that t:Nature,
•
[[σ→τ]]ξω is the set of all
terms t such that t:ω(σ→τ) and for
every s∈[[σ]]ξω with s:ω(σ)
we have t⋅s∈[[τ]]ξω,
•
[[∀(α:κ)σ]]ξω is the set
of all terms t such that t:ω(∀ασ) and
for every closed type constructor φ of kind κ and
every X∈Cφ we have t∗φ∈[[σ]]ξ[α:=X]ω[α:=φ],
•
[[φψ]]ξω=[[φ]]ξω(ω(ψ),[[ψ]]ξω),
•
[[λ(α:κ)φ]]ξω(ψ,X)=[[φ]]ξ[α:=X]ω[α:=ψ]
for closed ψ∈Tκ and X∈Cψ.
In the above, if e.g. [[ψ]]ξω∈/Cω(ψ) then [[φψ]]ξω is
undefined.
If φ is closed then ω,ξ do not affect the value
of [[φ]]ξω, so then we simply
write [[φ]].
[[Nature]]⊆SN follows
directly from Definition 18.
2. 2.
Let t∈[[Nature]] and t⇝t′. Then t:Nature and t∈SN. Hence t′∈SN, and t′:Nature by the
subject reduction lemma. Thus t′∈[[Nature]].
3. 3.
Let t be neutral and t:Nature. Assume that for all t′
with t⇝t′ we have t′∈[[Nature]], so in
particular t′∈SN. But then t∈SN. Hence t∈[[Nature]].
4. 4.
Let t1,t2∈SN be such that ti:Nature. Obviously,
∘Naturet1t2:Nature. Also ∘Naturet1t2∈SN
follows by Lemma A.3. So ∘Naturet1t2∈[[Nature]].
5. 5.
Let t∈SN be such that t:Nature. Then liftNaturet:Nature. It remains to show liftNaturet∈SN. Any infinite
reduction from liftNaturet has the form liftNaturet⇝∗liftNaturet0⇝t1⇝t2⇝… or liftNaturet⇝liftNaturet0⇝liftNaturet1⇝liftNaturet2⇝…, where t⇝∗t0 and ti⇝ti+1. This contradicts t∈SN.
6. 6.
Let t∈SN be such that t:Nature. The proof of
flattenNaturet∈SN is analogous to the proof of liftNaturet∈SN above.
Lemma A.9**.**
[[χκ]]∈Cχκ.
Proof A.10**.**
Induction on κ. If κ=∗ then this follows from
Lemma A.7. If κ=κ1⇒κ2
then χκ=λα:κ1.χκ2. Let ψ be a closed type constructor of
kind κ1 and let X∈Cχκ1. We have
[[χκ]](ψ,X)=[[χκ2]] because
χκ2 is closed. By the inductive hypothesis
[[χκ]](ψ,X)=[[χκ2]]∈Cχκ2. This implies [[χκ]]∈Cχκ.
Lemma A.11**.**
Let σ,τ be types. Suppose [[τ]]ξ′ω′∈Cω′(τ) and [[σ]]ξ′ω′∈Cω′(σ) for all suitable ω′,ξ′. Then
•
λx.s∈[[τ→σ]]ξω if and
only if λx.s:ω(τ→σ) and s[x:=t]∈[[σ]]ξω for all t∈[[τ]]ξω;
•
Λα.s∈[[∀(α:κ).σ]]ξω if and only if
Λα.s:ω(∀(α:κ).σ) and
for every closed type constructor φ of kind κ and
all X∈Cφ we have s[α:=φ]∈[[σ]]ξ[α:=X]ω[α:=φ].
Proof A.12**.**
First suppose
λx:ω(τ).s∈[[τ→σ]]ξω. Then
λx:ω(τ).s:ω(τ→σ) and for all
t∈[[τ]]ξω we have
(λx:ω(τ).s)⋅t∈[[σ]]ξω.
As this set is a candidate, it is closed under ⇝, so also
s[x:=t]∈[[σ]]ξω. Similarly, if
Λα.s∈[[∀α.σ]]ξω,
then Λα.s:∀α.σ and
(Λα.s)∗φ∈[[σ]]ξ[α:=X]ω[α:=φ],
and we are done because
(Λα.s)∗τ⇝s[α:=φ] and
[[σ]]ξ[α:=X]ω[α:=φ]
is a candidate, so it is closed under ⇝.
Now suppose s[x:=t]∈[[σ]]ξω for all
t∈[[τ]]ξω. Let
t∈[[τ]]ξω. Then t∈SN because
[[τ]]ξω is a candidate. Also s∈SN because
every infinite reduction in s induces an infinite reduction in
s[x:=t] (⇝ is stable) and
[[σ]]ξω⊆SN is a candidate. For all
s′,t′ with s⇝∗s′ and t⇝∗t′, we show by
induction on ν(s′)+ν(t′) that
(λx.s′)⋅t′∈[[σ]]ξω. We have
(λx.s′)⋅t′:ω(σ) by definition and the
subject reduction theorem (note that t:ω(τ) because
[[τ]]ξω∈Cω(τ)). The set
[[σ]]ξω is a candidate, and
(λx.s′)⋅t′ is neutral, so in
[[σ]]ξω if all its reducts are. Thus assume
(λx.s′)⋅t′⇝u. If
u=(λx.s′)⋅t′′ with t′⇝t′′ or
u=(λx.s′′)⋅t′ with s′⇝s′′, then
u∈[[σ]]ξω by the inductive hypothesis. So
assume u=s′[x:=t′]. We have s[x:=t]⇝∗s′[x:=t′] by
monotonicity and stability of ⇝. Therefore
u=s′[x:=t′]∈[[σ]]ξω, because
s[x:=t]∈[[σ]]ξω and
[[σ]]ξω is a candidate and hence closed under
⇝.
A similar reasoning applies to s[α:=φ].
Lemma A.13**.**
If σ is a type constructor, ω is closed for σ,
and ξ is an ω-valuation, then [[σ]]ξω∈Cω(σ).
Proof A.14**.**
By induction on the structure of σ we show that
[[σ]]ξω∈Cω(σ) for all
suitable ω,ξ. First, if σ=α is a type
constructor variable α then [[σ]]ξω=ξ(α)∈Cω(σ) by definition. If σ=Nature then [[Nature]]ξω∈CNature by
Lemma A.7.
Assume σ=τ1→τ2. We check the conditions in
Definition 17.
Let t∈[[τ1→τ2]]ξω and assume
there is an infinite reduction t⇝t1⇝t2⇝t3⇝…. By the inductive hypothesis
[[τ1]]ξω and [[τ2]]ξω are
candidates. Let x be a fresh variable. Then xω(τ1):ω(τ1) and xω(τ1)∈[[τ1]]ξω because it is neutral and normal. Thus
tx∈[[τ2]]ξω⊆SN. But tx⇝t1x⇝t2x⇝t3x⇝…. Contradiction.
2. 2.
Let t∈[[τ1→τ2]]ξω and t⇝t′. Let u∈[[τ1]]ξω be such that
u:ω(τ1). Then tu∈[[τ2]]ξω. By
the inductive hypothesis [[τ2]]ξω is a
candidate, so t′u∈[[τ2]]ξω. Also note that
t′:ω(τ1→τ2) by the subject reduction
lemma. Hence t′∈[[τ1→τ2]]ξω.
3. 3.
Let t be neutral such that t:ω(τ1→τ2). Assume for every t′ with t⇝t′ we have t′∈[[τ1→τ2]]ξω. Let u∈[[τ1]]ξω be such that u:ω(τ1). By
the inductive hypothesis [[τ1]]ξω is a
candidate, so u∈SN. By induction on ν(u) we show that
tu∈[[τ2]]ξω. Assume tu⇝t′′. We
show t′′∈[[τ2]]ξω. Because t is neutral,
tu cannot be a redex. So there are two cases.
•
t′′=tu′ with u⇝u′. Then u′∈[[τ1]]ξω because [[τ1]]ξω
is a candidate, and u′:ω(τ1) by the subject
reduction lemma. So tu′∈[[τ2]]ξω by the
inductive hypothesis for u.
•
t′′=t′u with t⇝t′. Then t′∈[[τ1→τ2]]ξω by point 2 above. So
t′u∈[[τ2]]ξω.
We have thus shown that if tu⇝t′′ then t′′∈[[τ2]]ξω. By the (main) inductive hypothesis
[[τ2]]ξω is a candidate. Because tu
is neutral, the above implies tu∈[[τ2]]ξω. Since u∈[[τ1]]ξω was arbitrary with u:ω(τ1), we have shown t∈[[τ1→τ2]]ξω.
4. 4.
Assume t1,t2∈[[τ1→τ2]]ξω.
We have already shown that this implies t1,t2∈SN. Let s=∘ω(τ1→τ2)t1t2. We show s∈[[τ1→τ2]]ξω by induction on ν(t1)+ν(t2). Note that s:ω(τ1→τ2) because
ti:ω(τ1→τ2). Since s is neutral, we
have already seen in point 3 above that to prove s∈[[τ1→τ2]]ξω it suffices to show that
s′∈[[τ1→τ2]]ξω whenever s⇝s′. If s′=∘ω(τ1→τ2)t1′t2 with t1⇝t1′, then note that t1′∈[[τ1→τ2]]ξω because we have already
shown that [[τ1→τ2]]ξω is closed
under ⇝; thus, we can complete by the induction
hypothesis. If s′=∘ω(τ1→τ2)t1t2′, we complete in the same way. The only alternative is that
s′=λx:ω(τ1).∘ω(τ2)(t1x)(t2x).
Let u∈[[τ1]]ξω. Then u:ω(τ1)
because [[τ1]]ξω∈Cω(τ1) by
the inductive hypothesis. Since t1,t2∈[[τ1→τ2]]ξω, we have that t1u and
t2u are in [[τ2]]ξω by definition. Since
[[τ2]]ξω is a candidate, this means that
∘ω(τ2)(t1u)(t2u)=(∘ω(τ2)(t1x)(t2x))[x:=u] is in [[τ2]]ξω as well.
By Lemma A.11, we conclude that s′∈[[τ1→τ2]]ξω.
5. 5.
Let t∈SN satisfy t:Nature, and let s=liftω(τ1→τ2)(t). We show s∈[[τ1→τ2]]ξω by induction
on ν(t). We have s:ω(τ1→τ2) because t:Nature. Since s is neutral, we have already proved above in
point 3 that it suffices to show that s′∈[[τ1→τ2]]ξω whenever s⇝s′. If s′=liftω(τ1→τ2)(t′) with t⇝t′ then still t′∈SN and t′:Nature, so s′∈[[τ1→τ2]]ξω by the inductive
hypothesis. The only alternative is that s′=λx:ω(τ1).liftω(τ2)(t). Let u∈[[τ1]]ξω be such that u:ω(τ1). Because [[τ2]]ξω∈Cω(τ2) by the (main) inductive hypothesis
for σ, we have liftω(τ2)(t)∈[[τ2]]ξω. Since liftω(τ2)(t)=(liftω(τ2)x)[x:=t] we obtain s′∈[[τ1→τ2]]ξω by
Lemma A.11.
6. 6.
Let t∈[[τ1→τ2]]ξω. We show
s:=flattenω(τ1→τ2)t∈SN. We have
already shown t∈SN in point 1 above. Thus any infinite
reduction starting from s must have the form s⇝∗flattenω(τ1→τ2)t′⇝flattenω(τ2)(t′(liftω(τ1)0))⇝… with t⇝∗t′. We have already shown in point 2
above that [[τ1→τ2]]ξω is closed
under ⇝, so t′∈[[τ1→τ2]]ξω. By the inductive
hypothesis [[τ1]]ξω∈Cω(τ1), so
liftω(τ1)0∈[[τ1]]ξω by
property 5 of candidates. Hence t′(liftω(τ1)0)∈[[τ2]]ξω by definition. But by the inductive
hypothesis [[τ2]]ξω is a candidate, so
flattenω(τ2)(t′(liftω(τ1)0))∈SN. Contradiction.
Assume σ=∀(α:κ)τ. We check the
conditions in Definition 17.
Let t∈[[∀(α:κ)τ]]ξω
and assume there is an infinite reduction t⇝t1⇝t2⇝t3⇝…. Recall that χκ from
Definition 2 is a closed type constructor of
kind κ. By Lemma A.9 we have
[[χκ]]∈Cχκ. Then tχκ∈[[τ]]ξ[α:=[[χκ]]]ω[α:=χκ]. By
the inductive hypothesis
[[τ]]ξ[α:=[[χκ]]]ω[α:=χκ]
is a candidate, so tχκ∈SN. But tχκ⇝t1χκ⇝t2χκ⇝t3χκ⇝…. Contradiction.
2. 2.
Let t∈[[∀ατ]]ξω and t⇝t′. By the subject reduction lemma t′:ω(∀ατ). Let φ be a closed type
constructor of kind κ and X∈Cφ. Then tφ∈[[τ]]ξ[α:=X]ω[α:=φ]. By
the inductive hypothesis
[[τ]]ξ[α:=X]ω[α:=φ]
is a candidate, so t′φ∈[[τ]]ξ[α:=X]ω[α:=φ]. Therefore
t′∈[[∀ατ]]ξω.
3. 3.
Let t be neutral such that t:ω(∀ατ), and assume that for every t′ with
t⇝t′ we have t′∈[[∀ατ]]ξω. Let φ be a closed
type constructor of kind κ and X∈Cφ. Assume tφ⇝t′′. Then t′′=t′φ with t⇝t′, because t is neutral. Hence tφ⇝t′φ∈[[τ]]ξ[α:=X]ω[α:=φ]. By
the inductive
hypothesis [[τ]]ξ[α:=X]ω[α:=φ]
is a candidate. Also tφ is neutral, so tφ∈[[τ]]ξ[α:=X]ω[α:=φ]
because t′′ was arbitrary with tφ⇝t′′. This
implies that t∈[[∀ατ]]ξω.
4. 4.
Assume t1,t2∈[[∀ατ]]ξω. We have already shown
that this implies t1,t2∈SN. We prove
∘ω(∀ατ)t1t2∈[[∀ατ]]ξω by induction on ν(t1)+ν(t2). Since s:=∘ω(∀ατ)t1t2 is neutral, we have already proven that it suffices to show
that s′∈[[∀ατ]]ξω whenever s⇝s′. The cases when t1 or t2 are reduced are
immediate with the induction hypotheses. The only remaining case
is when s′=Λα.∘ω(τ)(t1α)(t2α). For all closed type constructors φ of
kind κ and all X∈Cφ we have both
t1φ and t2φ in
[[τ]]ξ[α:=X]ω[α:=φ]
(by definition of t1,t2∈[[∀ατ]]ξω). Let ω′=ω[α:=φ]. By bound variable renaming, we
may assume ω(α)=α and α does not occur
in t1,t2. Because
[[τ]]ξ[α:=X]ω[α:=φ]
is a candidate by the inductive hypothesis for σ, we have
Let t∈SN be such that t:Nature. By induction
on ν(t) we show s:=liftω(∀ατ)(t)∈[[∀ατ]]ξω. First note that s:ω(∀ατ). Since s is neutral, by the already
proven point 3 above, it suffices to show that s′∈[[∀ατ]]ξω whenever s⇝s′. The case when t is reduced is immediate by the inductive
hypothesis. The only remaining case is when s′=Λα.liftω(τ)(t) (without loss of
generality assuming ω(α)=α). Let φ be a
closed type constructor of kind κ and let X∈Cφ. Because
[[τ]]ξ[α:=X]ω[α:=φ]
is a candidate, we have
[TABLE]
This implies s′∈[[∀ατ]]ξω.
6. 6.
Let t∈[[∀ατ]]ξω. We show s:=flattenω(∀ατ)t∈SN. We have
already shown t∈SN in point 1 above. Thus any infinite
reduction starting from s must have the form s⇝∗flattenω(∀ατ)t′⇝flattenω(τ)[α:=χκ](t′χκ)⇝… with t⇝∗t′ (assuming
ω(α)=α without loss of generality). We have
already shown in point 2 above that
[[∀ατ]]ξω is closed
under ⇝, so t′∈[[∀ατ]]ξω. We have
[[χκ]]∈Cχκ by
Lemma A.9. Since χκ is also
closed, we have t′χκ∈[[τ]]ξ[α:=[[χκ]]]ω[α:=χκ]
by definition of [[∀ατ]]ξω. By the
inductive hypothesis
[[τ]]ξ[α:=[[χκ]]]ω[α:=χκ]∈Cω[α:=χκ](τ). Hence
flattenω[α:=χκ](τ)(t′χκ)∈SN. But
ω[α:=χκ](τ)=ω(τ)[α:=χκ] because χκ
is closed and ω(α)=α. Contradiction.
Assume σ=φψ, with ψ of kind κ1 and
φ of kind κ1⇒κ2. By the inductive
hypothesis [[ψ]]ξω∈Cω(ψ) and
[[φ]]ξω∈Cω(φ). Because
applying ω does not change kinds, we have
[[φψ]]ξω=[[φ]]ξω(ω(ψ),[[ψ]]ξω)∈Cω(φψ), by the definition of candidates of a
type constructor with kind κ1⇒κ2 (note that
ω(ψ) is closed, because ω is closed for σ).
Finally, assume σ=λ(α:κ)φ. Let ψ
be a closed type constructor of kind κ and X∈Cψ. By the inductive hypothesis
[[λ(α:κ)φ]]ξω(ψ,X)=[[φ]]ξ[α:=X]ω[α:=ψ]∈Cω[α:=ψ](φ). Because ψ is
closed we have ω[α:=ψ](φ)=ω(φ[α:=ψ])=βω((λα.φ)ψ)=ω(σψ)=ω(σ)ψ. By Lemma A.5 this implies
that [[σ]]ξω∈Cω(σ).
Lemma A.15**.**
∘∈[[∀α.α→α→α]] for ∘∈{⊕,⊗}.
Proof A.16**.**
Follows from definitions and property 4 of candidates.
Lemma A.17**.**
lift∈[[∀α.Nature→α]].
Proof A.18**.**
Follows from definitions and property 5 of candidates.
Lemma A.19**.**
flatten∈[[∀α.α→Nature]].
Proof A.20**.**
Follows from definitions and property 6 of candidates.
Lemma A.21**.**
For any type constructors σ,τ with α∈/FTV(τ), a mapping ω closed for σ and for τ,
and an ω-valuation ξ, we have:
[TABLE]
Proof A.22**.**
Let ω′=ω[α:=ω(τ)] and ξ′=ξ[α:=[[τ]]ξω]. First note
that ω is closed for σ[α:=τ]
and ω′ is closed for σ. We proceed by induction
on σ. If α∈/FTV(σ) then the claim is
obvious. If σ=α then
[[σ[α:=τ]]]ξω=[[τ]]ξω=[[σ]]ξ′ω′.
Assume σ=σ1→σ2. We show
[[σ[α:=τ]]]ξω⊆[[σ]]ξ′ω′. Let t∈[[σ[α:=τ]]]ξω. We have t:ω(σ[α:=τ]), so t:ω′(σ). Let
u∈[[σ1]]ξ′ω′. By the inductive hypothesis
u∈[[σ1[α:=τ]]]ξω. Hence tu∈[[σ2[α:=τ]]]ξω=[[σ2]]ξ′ω′, where the last equality follows from
the inductive hypothesis. Thus t∈[[σ]]ξ′ω′. The other direction is analogous. The
case σ=∀ασ′ is also analogous.
Assume σ=φψ. We have
[[σ[α:=τ]]]ξω=[[φ[α:=τ]]]ξω(ω(ψ[α:=τ]),[[ψ[α:=τ]]]ξω)=[[φ[α:=τ]]]ξω(ω′(ψ),[[ψ[α:=τ]]]ξω)=[[φ]]ξ′ω′(ω′(ψ),[[ψ]]ξ′ω′) where the last equality follows from the
inductive hypothesis.
Finally, assume σ=λ(β:κ)φ. Let ψ∈Tκ be closed and let X∈Cψ. We have
[[σ[α:=τ]]]ξω(ψ,X)=[[φ[α:=τ]]]ξ[β:=X]ω[β:=τ]=[[φ]]ξ′[β:=X]ω′[β:=τ]=[[σ]]ξ′ω′(ψ,X) where we use the inductive
hypothesis in the penultimate equality.
Lemma A.23**.**
Let τ be a type constructor of kind κ. Assume ω
is closed for ∀ασ and for τ. If t∈[[∀(α:κ)σ]]ξω then t(ω(τ))∈[[σ[α:=τ]]]ξω.
Proof A.24**.**
By Lemma A.13 we have [[τ]]ξω∈Cω(τ). So t(ω(τ))∈[[σ]]ξ[α:=[[τ]]ξω]ω[α:=ω(τ)]
by t∈[[∀(α:κ)σ]]ξω. Hence
t(ω(τ))∈[[σ[α:=τ]]]ξω by
Lemma A.21.
Lemma A.25**.**
If ω is closed for σ,σ′ and σ=βσ′ then [[σ]]ξω=[[σ′]]ξω.
Proof A.26**.**
It suffices to show the lemma for the case when σ is a
β-redex. Then the general case follows by induction
on σ and the length of reduction to a common reduct.
So assume (λατ)σ→βτ[α:=σ]. We have
[[(λατ)σ]]ξω=[[λατ]]ξω(ω(σ),[[σ]]ξω)=[[τ]]ξ[α:=[[σ]]ξω]ω[α:=ω(σ)]=[[τ[α:=σ]]]ξω where the last
equality follows from Lemma A.21.
A mapping ω on type constructors is extended in the obvious way
to a mapping on terms. Note that ω also acts on the type
annotations of variable occurrences, e.g. ω(λx:α.xα)=λx:ω(α).xω(α).
Lemma A.27**.**
If t:σ and ω is closed for σ and
FTV(ω(t))=∅ then ω(t)∈[[σ]]ξω.
Proof A.28**.**
We prove by induction on the structure of t that if t:σ
and ω is closed for σ and FTV(ω(t))=∅ and x1τ1,…,xnτn are all free
variable occurrences in the canonical representative of t (so
each τi is β-normal), then for all
u1∈[[τ1]]ξω,…,un∈[[τn]]ξω
we have ω(t)[x1:=u1,…,xn:=un]∈[[σ]]ξω. This suffices because
ω(xiτi)∈[[τi]]ξω. Note that
ω is closed for each τi because FTV(ω(t))=∅ and t is typed, so no type constructor variable
occurring free in τi can be bound in t by a Λ;
e.g. Λα.xα is not a valid typed term (we
assume τi to be in β-normal form). For brevity, we use
the notation ω∗(t)=ω(t)[x1:=u1,…,xn:=un]. Note that
ω∗(t):ω(σ).
By the generation lemma for t:σ there is a type σ′
such that σ′=βσ and FTV(σ′)⊆FTV(t) and one of the cases below holds. Note that ω is
closed for σ′ because it is closed for σ and
FTV(ω(t))=∅. By Lemma A.25 it
suffices to show ω∗(t)∈[[σ′]]ξω.
•
If t=x1σ′ then ω(t)[x1:=u1]=(x1ω(σ′))[x1:=u1]=u1∈[[σ′]]ξω by assumption.
•
If t=n is a natural number and σ′=Nature then t∈[[Nature]] by definition.
•
If t is a function symbol then the claim follows from
Lemma A.15, Lemma A.17 or
Lemma A.19.
•
If t=λx:σ1.s then
σ′=σ1→σ2 and s:σ2. Hence
ω is closed for σ2. Let
u∈[[σ1]]ξω. By the inductive hypothesis
ω∗(s)[x:=u]∈[[σ2]]ξω. Hence
ω∗(t)∈[[σ′]]ξω by
Lemma A.11.
•
If t=Λα:κ.s then σ′=∀ατ and s:τ. Let ψ be a closed type
constructor of kind κ and let X∈Cψ. Let
ω1=ω[α:=ψ] and
ξ1=ξ[α:=X]. Then ω1 is closed
for τ and FTV(ω1(s))=∅. By the inductive
hypothesis ω1∗(s)∈[[τ]]ξ1ω1. We
have ω1∗(s)=ω∗(s)[α:=ψ] (assuming
α chosen fresh such that ω(α)=α). Hence
ω∗(t)∈[[τ]]ξω by
Lemma A.11.
•
If t=t1t2 then t1:τ→σ′ and t2:τ and FTV(τ)⊆FTV(t). Hence ω is closed
for τ and for τ→σ′. By the inductive
hypothesis ω∗(t1)∈[[τ→σ′]]ξω and ω∗(t2)∈[[τ]]ξω. We have ω∗(t2):ω(τ). Then by definition ω∗(t)=(ω∗(t1))(ω∗(t2))∈[[σ′]]ξω.
•
If t=sψ then s:∀ατ and σ′=τ[α:=ψ]. By the inductive hypothesis
ω∗(s)∈[[∀ατ]]ξω. Because
FTV(ω(t))=∅, the mapping ω is closed
for ψ. So by Lemma A.23 we have ω∗(t)=ω∗(s)ω(ψ)∈[[τ[α:=ψ]]]ξω.
Theorem 4.3.
If t:σ then t∈SN.
Proof A.29**.**
For closed terms t and closed types σ this follows from
Lemma A.27, Lemma A.13
and property 1 of candidates (Definition 17). For
arbitrary terms and types, this follows by closing the terms with an
appropriate number of abstractions, and the types with corresponding
∀-quantifiers.
Lemma A.30**.**
The only final interpretation terms of type Nature are the natural
numbers.
Proof A.30**.**
We show by induction on t that if t is a final interpretation
term of type Nature then t is a natural number. Because t is
closed and in normal form, if it is not a natural number then it
must have the form fσt1…tn for a function
symbol f. For concreteness assume f=⊕. Then n≥2. Because t is closed, σ cannot be a
type variable. It also cannot be an arrow or a ∀-type,
because then t would contain a redex. So σ=Nature. Then
t1,t2 are final interpretation terms of type Nature, hence
natural numbers by the inductive hypothesis. But then t contains a
redex. Contradiction.
The case for f=⊗ is parallel. If
f∈{flatten,lift} and σ is closed, then
n≥1 and in all cases t is not in normal form.
A.2 Weak monotonicity proof
We want to show that if s⪰s′ then t[x:=s]⪰t[x:=s′]. A straightforward proof attempt runs into a problem
that, because of impredicativity of polymorphism, direct induction on
type structure is not possible. We adopt a method similar to Girard’s
method of candidates from the termination proof.
Definition 19**.**
By induction on the kind κ of a type constructor τ we
define the set Cτ of all candidates of type
constructor τ.
First assume κ=∗, i.e., τ is a type. A set X of terms
of type τ equipped with a binary relation ≥X is a
candidate of type τ if it satisfies the following
properties:
if t∈X and t′:τ and t′⇝t then t′∈X,
2. 2.
if t1,t2∈X then ∘τt1t2∈X for ∘∈{⊕,⊗},
3. 3.
if t:Nature then liftτt∈X.
and the relation ≥X satisfies the following properties:
⪰∩X×X⊆≥X,
2. 2.
if t1≥Xt2 and t1′⇝t1 (resp. t2′⇝t2) then t1′≥Xt2 (resp. t1≥Xt2′),
3. 3.
if t1≥Xt1′ and t2≥Xt2′ then ∘τt1t2≥X∘τt1′t2′ for ∘∈{⊕,⊗},
4. 4.
if t1⪰Naturet2 then liftτ(t1)≥Xliftτ(t2),
5. 5.
if t1≥Xt2 then flattenτ(t1)⪰Natureflattenτ(t2),
6. 6.
≥X is reflexive and transitive on X.
The relation ≥X is a comparison candidate for X,
and X is a candidate set.
Now assume κ=κ1⇒κ2. A function f:Tκ1×⋃ξ∈Tκ1Cξ→⋃ξ∈Tκ2Cξ is a candidate of type
constructor τ if for every closed type constructor σ
of kind κ1 and a candidate X∈Cσ we have
f(σ,X)∈Cτσ.
Lemma A.31**.**
If σ=βσ′ then Cσ=Cσ′.
Proof A.32**.**
Induction on the kind of σ.
Definition 20**.**
Let ω be a mapping from type constructor variables to type
constructors (respecting kinds). The mapping ω extends in an
obvious way to a mapping from type constructors to type
constructors. A mapping ω is closed for σ if
ω(α) is closed for α∈FTV(σ) (then
ω(σ) is closed).
An ω-valuation is a mapping ξ on type constructor
variables such that ξ(α)∈Cω(α).
For each type constructor σ, each mapping ω closed
for σ, and each ω-valuation ξ, we define
[[σ]]ξω by induction on σ:
•
[[α]]ξω=ξ(α) for a type
constructor variable α,
•
[[Nature]]ξω is the set of all terms t∈I such that t:Nature; equipped with the relation
≥Natureξ,ω=⪰Nature,
•
[[σ→τ]]ξω is the set of all
terms t such that t:ω(σ→τ) and:
–
for all s∈[[σ]]ξω we have
t⋅s∈[[τ]]ξω, and
–
if s1≥σξ,ωs2 then t⋅s1≥τξ,ωt⋅s2;
equipped with the
relation ≥σ→τξ,ω defined by:
–
t1≥σ→τξ,ωt2 iff
t1,t2∈[[σ→τ]]ξω and for
every s∈[[σ]]ξω we have t1s≥τξ,ωt2s,
•
[[∀(α:κ)[σ]]]ξω is the set
of all terms t such that t:ω(∀α[σ]) and:
–
for every closed type constructor φ of kind κ
and every X∈Cφ we have t∗φ∈[[σ]]ξ[α:=X]ω[α:=φ];
equipped with the
relation ≥∀α[σ]ξ,ω defined by:
–
t1≥∀(α:κ)[σ]ξ,ωt2
iff t1,t2∈[[∀(α:κ)[σ]]]ξω and for every
closed type constructor φ of kind κ and every X∈Cφ we have t1φ≥σξ[α:=X],ω[α:=φ]t2φ,
•
[[φψ]]ξω=[[φ]]ξω(ω(ψ),[[ψ]]ξω),
•
[[λ(α:κ)φ]]ξω(ψ,X)=[[φ]]ξ[α:=X]ω[α:=ψ]
for closed ψ∈Tκ and X∈Cψ.
In the above, if e.g. [[ψ]]ξω∈/Cω(ψ) then [[φψ]]ξω is
undefined.
Note that if t∈[[σ]]ξω then t:ω(σ), and if t1≥σξ,ωt2 then
t1,t2∈[[σ]]ξω. For brevity we
use [[σ]]ξω to denote both the pair
([[σ]]ξω,≥σξ,ω) and its
first element, depending on the context. For a type τ,
by ≥τξ,ω we always denote the second element of
the pair [[τ]]ξω. If τ is closed then ξ
and ω do not matter and we simply write ≥τ
and [[τ]].
Lemma A.33**.**
If σ is a type constructor, ω is closed for σ,
and ξ is an ω-valuation, then [[σ]]ξω∈Cω(σ).
Proof A.34**.**
Induction on σ. If σ=α then ξ(α)∈Cω(α) by definition. If σ=Nature then this
follows from definitions.
Assume σ=σ1→σ2. We check the properties of
a candidate set.
The first property follows from the inductive hypothesis and
property 2 of comparison candidates.
2. 2.
Let t1,t2∈[[σ]]ξω. We need to show
∘ω(σ)t1t2∈[[σ1→σ2]]ξω.
Let s∈[[σ1]]ξω. Then
∘ω(σ)t1t2s⇝∘ω(σ2)(t1s)(t2s). Because ti∈[[σ1→σ2]]ξω, we have tis∈[[σ2]]ξω. By the inductive
hypothesis [[σ2]]ξω∈Cω(σ2), so ∘ω(σ2)(t1s)(t2s)∈[[σ2]]ξω. Hence
∘ω(σ2)t1t2s∈[[σ2]]ξω by property 1 of candidate sets.
Let s1≥σ1ξ,ωs2. Then si∈[[σ1]]ξω. Because tj∈[[σ1→σ2]]ξω, we have tjsi∈[[σ2]]ξω and tjs1≥σ2ξ,ωtjs2. By the inductive
hypothesis ≥σ2ξ,ω is a comparison
candidate for [[σ2]]ξω. Thus
∘ω(σ2)(t1s1)(t2s1)≥σ2ξ,ω∘ω(σ2)(t1s2)(t2s2) by property 3 of comparison candidates. This suffices
by property 2 of comparison candidates.
3. 3.
Let t:Nature. Then liftω(σ)t:ω(σ).
Let s∈[[σ1]]ξω. Then
liftω(σ)ts⇝liftω(σ2)t. By the inductive hypothesis liftω(σ2)t∈[[σ2]]ξω. Hence liftω(σ)ts∈[[σ2]]ξω by property 1 of candidate sets.
Let s1,s2∈[[σ1]]ξω. By the inductive
hypothesis ≥σ2ξ,ω is a comparison
candidate for [[σ2]]ξω. We have
liftω(σ2)t≥σ2ξ,ωliftω(σ2)t by the reflexivity
of ≥σ2ξ,ω (property 6 of comparison
candidates). This suffices by property 2 of comparison candidates,
because liftω(σ)tsi⇝liftω(σ2)t.
Now we check the properties of a comparison candidate
for [[σ1→σ2]]ξω.
Suppose t1⪰t2 with t1,t2∈[[σ]]ξω. Let s∈[[σ1]]ξω. Then t1s⪰t2s by the
definition of ⪰. Hence t1s≥σ2ξ,ωt2s by the inductive hypothesis.
2. 2.
Follows from the inductive hypothesis and the already shown
property 1 of candidate sets
for [[σ1→σ2]]ξω.
3. 3.
Assume ti≥σξ,ωti′. Let s∈[[σ1]]ξω. We have ∘ω(σ)t1t2s⇝∘ω(σ2)(t1s)(t2s) and
∘ω(σ)t1′t2′s⇝∘ω(σ2)(t1′s)(t2′s). Since
ti,ti′∈[[σ]]ξω, we have tis≥σ2ξ,ωti′s and tis,ti′s∈[[σ2]]ξω. By the inductive hypothesis ∘(t1s)(t2s)≥σ2ξ,ω∘(t1′s)(t2′s), so ∘t1t2s≥σ2ξ,ω∘t1′t2′s by property 2 of comparison candidates. This implies
∘t1t2≥σξ,ω∘t1′t2′.
4. 4.
Follows from Lemma 4.30 and property 1 of
comparison candidates.
5. 5.
Assume t1≥σξ,ωt2. Then
flattenω(σ)ti⇝flattenω(σ2)(ti(liftω(σ1)0)). By
the inductive hypothesis and property 3 of candidate sets
liftω(σ1)0∈[[σ1]]ξω. Hence
ti(liftω(σ1)0)∈[[σ2]]ξω
and t1(liftω(σ1)0)≥σ2ξ,ωt2(liftω(σ1)0). Thus by the inductive hypothesis
flattenω(σ2)(t1(liftω(σ1)0))⪰Natureflattenω(σ2)(t2(liftω(σ1)0)). This implies
flattenω(σ)t1⪰Natureflattenω(σ)t2.
6. 6.
Follows directly from the inductive hypothesis.
If σ=∀ατ then the proof is analogous to the
case σ=σ1→σ2. If σ=φψ or
σ=λ(α:κ)φ then the claim follows from
the inductive hypothesis and Lemma A.31, like
in the proof of Lemma A.13.
Lemma A.35**.**
∘∈[[∀α.α→α→α]] for ∘∈{⊕,⊗}.
Proof A.36**.**
Let τ be a closed type and let X∈Cτ. Let
ω(α)=τ and ξ(α)=X.
Let t1,t2∈[[α]]ξω=X. Then ∘τt1t2∈[[α]]ξω by property 2 of candidate
sets.
Let t2′∈[[α]]ξω be such that t2≥αξ,ωt2′, i.e., t2≥Xt2′. By
properties 6 and 3 of comparison candidates we have we have
∘τt1t2≥αξ,ω∘τt1t2′. This shows ∘τt1∈[[α→α]]ξω.
Let t1′∈[[α]]ξω be such that t1≥αξ,ωt1′. Let u∈[[α]]ξω. By properties 6 and 3 of comparison
candidates we have ∘τt1u≥αξ,ω∘τt1′u. Hence ∘τt1≥α→αξ,ω∘τt1′. This
shows ∘τ∈[[α→α→α]]ξω.
Lemma A.37**.**
lift∈[[∀α.Nature→α]].
Proof A.38**.**
Let τ be a closed type and let X∈Cτ. Let
ω(α)=τ and ξ(α)=X. By property 4 of
comparison candidates we have liftτs1≥αξ,ωliftτs2 for all si:Nature
with s1⪰Natures2. It remains to show that liftτs∈[[α]]ξω=X for all s:Nature. This follows
from property 3 of candidate sets.
Lemma A.39**.**
flatten∈[[∀α.α→Nature]].
Proof A.40**.**
Follows from definitions and property 5 of comparison candidates.
Lemma A.41**.**
For any type constructors σ,τ with α∈/FTV(τ), a mapping ω closed for σ and for τ,
and an ω-valuation ξ, we have:
[TABLE]
Proof A.42**.**
Let ω′=ω[α:=ω(τ)] and ξ′=ξ[α:=[[τ]]ξω]. The proof by
induction on σ is analogous to the proof of
Lemma A.21. The main difference is that in the case
σ=σ1→σ2 we need to show that if e.g. t∈[[σ[α:=τ]]]ξω and s1≥σ1ξ′,ω′s2 then ts1≥σ2ξ′,ω′ts2. But then s1≥σ1[α:=τ]ξ,ωs2 by the
inductive hypothesis, so ts1≥σ2[α:=τ]ξ,ωts2 by
definition. Hence ts1≥σ2ξ′,ω′ts2 by
the inductive hypothesis.
Lemma A.43**.**
Let τ be a type constructor of kind κ. Assume ω
is closed for ∀α[σ] and for τ.
If t∈[[∀(α:κ)[σ]]]ξω
then t(ω(τ))∈[[σ[α:=τ]]]ξω.
2. 2.
If t1≥∀(α:κ)[σ]ξ,ωt2 then t1(ω(τ))≥σ[α:=τ]ξ,ωt2(ω(τ)).
Proof A.44**.**
Analogous to the proof of Lemma A.23, using
Lemma A.33 and Lemma A.41.
Lemma A.45**.**
If ω is closed for σ,σ′ and σ=βσ′ then [[σ]]ξω=[[σ′]]ξω and ≥σξ,ω=≥σ′ξ,ω.
Proof A.46**.**
Analogous to the proof of Lemma A.25, using
Lemma A.41.
For two replacements δ1=γ1∘ω and δ2=γ2∘ω (see Definition 11) and an
ω-valuation ξ we write δ1≥τξ,ωδ2 iff δ1(x)≥τξ,ωδ2(x) for
each x:τ.
Lemma A.47**.**
Assume t:σ and δ1=γ1∘ω,
δ2=γ2∘ω are replacements and ξ an
ω-valuation such that δ1≥ξ,ωδ2 and ω is closed for σ and FTV(ω(t))=∅ and for all xτ∈FTV(t) we have δi(x)∈[[τ]]ξω. Then δi(t)∈[[σ]]ξω and δ1(t)≥σξ,ωδ2(t).
Proof A.48**.**
Induction on the structure of t. By the generation lemma for t:σ there is a type σ′ such that σ′=βσ
and FTV(σ′)⊆FTV(t) and one of the cases below
holds. Note that ω is closed for σ′, because it is
closed for σ and FTV(ω(t))=∅. Hence by
Lemma A.45 it suffices to show δi(t)∈[[σ′]]ξω and δ1(t)≥σ′ξ,ωδ2(t).
•
If t=xσ′ then δi(t)∈[[σ′]]ξω by assumption. Also δ1(t)≥σ′ξ,ωδ2(t) by assumption.
•
If t=n is a natural number and σ′=Nature then
δi(t)=t and thus t∈[[Nature]] and δ1(t)≥Natureξ,ωδ2(t) by definition and the
reflexivity of ≥Natureξ,ω.
•
If t is a function symbol then the claim follows from
Lemma A.35, Lemma A.37 or
Lemma A.39, and the reflexivity
of ≥ξ,ω.
•
If t=λx:σ1.u then σ′=σ1→σ2 and u:σ2. Let s∈[[σ1]]ξω and
δi′=δi[x:=s]. This is well-defined because
s:ω(σ1) and ω(x) has
type ω(σ1). We have δ1′≥ξ,ωδ2′ by the reflexivity of ≥σ1ξ,ω
(Lemma A.33 and property 6 of comparison
candidates). Hence by the inductive hypothesis δi′(u)∈[[σ2]]ξω. We have δi(λx.u)s⇝δi′(u), so δi(λx.u)s∈[[σ2]]ξω by Lemma A.33
and property 1 of candidate sets.
Let s1,s2∈[[σ1]]ξω be such that s1≥σ1ξ,ωs2. Let
δi′=δi[x:=si]. We have δ1≥ξ,ωδ2. Hence by the inductive hypothesis
δ1′(u)≥σ2ξ,ωδ2′(u). We have
δi(λx.u)si⇝δi′(u). Thus
δ1(t)s1≥σ2ξ,ωδ2(t)s2 by
Lemma A.33 and property 2 of comparison
candidates.
Finally, we show δ1(t)≥σ1→σ2ξ,ωδ2(t). Let s∈[[σ1]]ξω and
δi′=δi[x:=s]. We have δ1′≥ξ,ωδ2′. By the inductive hypothesis
δ1′(u)≥σ2ξ,ωδ2′(u). We have
δi(λx.u)s⇝δi′(u). Thus δ1(t)s≥σ2ξ,ωδ2(t)s by
Lemma A.33 and property 2 of comparison
candidates.
•
If t=Λα:κ.u then σ′=∀α[τ] and u:τ. Let ψ be a closed type
constructor of kind κ and let X∈Cψ. Let
ω′=ω[α:=ψ] and
ξ′=ξ[α:=X]. Then ω′ is closed for τ
and FTV(ω′(u))=∅. Let
δi′=γi∘ω′. By the inductive hypothesis
δi′(u)∈[[τ]]ξ′ω′ and δ1′(u)≥τξ′,ω′δ2′(u). We have
δi(Λα.u)ψ⇝δi′(u). Hence
δi(Λα.u)ψ∈[[τ]]ξ′ω′ by
Lemma A.33 and property 1 of candidate
sets. Thus δi(Λα.u)∈[[∀α[τ]]]ξω. Also
δ1(Λα.u)ψ≥τξ′,ω′δ2(Λα.u)ψ by
Lemma A.33 and property 2 of comparison
candidates. Thus δ1(Λα.u)≥∀α[τ]ξ′,ω′δ2(Λα.u).
•
If t=t1t2 then t1:τ→σ′ and t2:τ and FTV(τ)⊆FTV(t). Hence ω is closed
for τ and for τ→σ′. By the inductive
hypothesis δi(t1)∈[[τ→σ′]]ξω and δi(t2)∈[[τ]]ξω and δ1(t1)≥τ→σ′ξ,ωδ2(t1) and
δ1(t2)≥τξ,ωδ2(t2). By the
definition of [[τ→σ′]]ξω we have
δi(t)=δi(t1)δi(t2)∈[[σ′]]ξω, and δ1(t1)δ1(t2)≥σ′ξ,ωδ1(t1)δ2(t2). By the
definition of ≥τ→σ′ξ,ω we have
δ1(t1)δ2(t2)≥σ′ξ,ωδ2(t1)δ2(t2). Hence
δ1(t)≥σ′ξ,ωδ2(t) by the
transitivity of ≥σ′ξ,ω.
•
If t=sψ then s:∀α[τ] and σ′=τ[α:=ψ]. By the inductive hypothesis
δi(s)∈[[∀α[τ]]]ξω and
δ1(s)≥∀α[τ]ξ,ωδ2(s). Because FTV(ω(t))=∅, the mapping
ω is closed for ψ. So by Lemma A.43 we
have δi(t)=δi(s)ω(ψ)∈[[τ[α:=ψ]]]ξω and δ1(t)≥τ[α:=ψ]ξ,ωδ2(t).
Corollary A.49**.**
If t is closed and t:σ then t∈[[σ]].
Lemma A.50**.**
If σ is a closed type and t1≥σt2 then
t1⪰σt2.
Proof A.51**.**
By coinduction. By Lemma A.45 we may assume
that σ is in β-normal form. The case σ=α is
impossible because σ is closed. If σ=Nature then
≥Nature=⪰Nature.
Assume σ=σ1→σ2. Let u:σ1 be
closed. By Corollary A.49 we have u∈[[σ1]]. Hence t1u≥σ2t2u. By the
coinductive hypothesis t1u⪰σ2t2u. This
implies t1⪰σt2.
Assume σ=∀(α:κ)τ. Let φ be a
closed type constructor of kind κ. By
Lemma A.33 we have [[φ]]∈Cφ. By the definition of ≥∀ατ and
Lemma A.41 we have t1φ≥τ[α:=φ]t2φ. Note that
τ[α:=φ] is still closed. Hence by the
coinductive hypothesis t1φ⪰τ[α:=φ]t2φ. This implies
t1⪰σt2.
Corollary A.52**.**
If σ is a closed type then ≥σ=⪰σ.
Proof A.53**.**
Follows from Lemma A.50,
Lemma A.33 and property 1 of comparison
candidates.
Lemma A.54** (Weak monotonicity).**
If s⪰σs′ then t[x:=s]⪰τt[x:=s′].
Proof A.54**.**
It suffices to show this when
s,s′,t[x:=s],t[x:=s′] and σ,τ are all
closed. Assume s⪰σs′. Then s≥σs′ by
Corollary A.52. Thus t[x:=s]≥τt[x:=s′] follows from
Lemma A.47. Hence t[x:=s]⪰τt[x:=s′] by Corollary A.52.
For all types σ, terms s,t of type σ and natural
numbers n>0:
s⊕σt⪰s and s⊕σt⪰t;
2. 2.
s⊕σ(liftσn)≻s and
(liftσn)⊕σt≻t.
Proof A.55**.**
It suffices to prove this for closed s,t and closed σ in
β-normal form.
By coinduction we show (s⊕t)u1…um⪰σsu1…um for closed u1,…,um. The
second case is similar.
First note that (s⊕t)u1…um⇝∗su1…um⊕tu1…um.
If σ=Nature then ((s⊕t)u1…um)↓=(su1…um)↓+(tu1…um)↓≥(su1…um)↓. Hence (s⊕t)u1…um)⪰Naturesu1…um.
If σ=τ1→τ2 then by the coinductive
hypothesis (s⊕t)u1…umq⪰τ2su1…umq for any q∈Iτ1f. Hence (s⊕t)u1…um⪰σsu1…um.
If σ=∀(α:κ)[τ] then by the coinductive
hypothesis (s⊕t)u1…umξ⪰σ′su1…umξ for any closed ξ∈Tκ, where
σ′=τ[α:=ξ]. Hence (s⊕t)u1…um⪰σsu1…um.
2. 2.
By coinduction we show (s⊕(liftn))u1…um⪰σsu1…um for closed u1,…,um. The
second case is similar.
Note that (s⊕(liftn))u1…um⇝∗su1…um⊕n. From this the case σ=Nature
follows. The other cases follow from the coinductive hypothesis,
like in the first point above.
Lemma A.56**.**
For all types σ and all terms s,t,u of type σ, we
have:
s⊕σt≈t⊕σs and s⊗σt≈t⊗σs;
2. 2.
s⊕σ(t⊕σu)≈(s⊕σt)⊕σu and s⊗σ(t⊗σu)≈(s⊗σt)⊗σu;
3. 3.
s⊗σ(t⊕σu)≈(s⊗σt)⊕σ(s⊗σu);
4. 4.
(liftσ0)⊕σs≈s and (liftσ1)⊗σs≈s.
Proof A.56**.**
The proof is again analogous to the proof of
Lemma 6.6. For instance, for closed s,t and closed
σ in β-normal form, we show by coinduction that (s⊕t)w1…wn⪰(t⊕s)w1…wn for
closed w1,…,wn (and then the same with ⪯).
Lemma A.57**.**
liftσ(n+m)≈σ(liftσn)⊕σ(liftσn).
2. 2.
liftσ(nm)≈σ(liftσn)⊗σ(liftσn).
3. 3.
flattenσ(liftσ(n))≈n.
Proof A.57**.**
It suffices to show this for closed σ in β-normal
form. For the first two points, one proves by induction on σ
that
(liftσ(n+m))↓=(liftσn⊕σliftσn)↓ (analogously for multiplication). This suffices by
Corollary 4.26 and the reflexivity of ≈.
For the third point, one proceeds by induction on σ. For
example, if σ=σ1→σ2 then
flattenσ(liftσ(n))⇝∗flattenσ2((λx.liftσ2n)(liftσ10))⇝flattenσ2(liftσ1n). Then the claim follows from the inductive hypothesis and
Lemma 4.24.
The system IPC2 can be seen as a PFS with the following type constructors:
[TABLE]
We also have the following function symbols:
[TABLE]
The following are the core rules (β-reductions):
[TABLE]
Then the next rules simplify proofs from contradiction:
[TABLE]
When a case occurs in a first argument, then it is shifted
to the root of the term.
[TABLE]
And the same happens for the let:
[TABLE]
It is this last group of rules that is not oriented by our method.
For all other rules ℓ⟶r we have [[ℓ]]≻[[r]], as demonstrated below.
We will use the fact that β-reduction provides the derived
reduction rules for πi and let.
Lemma B.1**.**
πi(⟨t1,t2⟩)⇝β∗ti and
let[τ,t]be[α,x]ins⇝β∗s[α:=τ][x:=t].
In the proofs below, we will often use that lift(n)⊗s⊕t⪰s if n≥1, which holds because lift(n)⊗s⊕t≈lift(1)⊗s⊕(lift(n−1)⊗s⊕t)≈s⊕(lift(n−1)⊗s⊕t)⪰s, using the calculation rules. Having this, the core rules and the
contradiction simplifications are all quite easy due to the choice of
J:
•
\llbracket@σ,τ(λx.s,t)]]≻[[s[x:=t]]]
We have
\llbracket@σ,τ(λx:σ.s,t)]]⇝β∗lift[[τ]](2)⊗((λx:[[σ]].[[s]])⋅[[t]])⊕lift[[τ]](⟨something⟩⊕1)⇝lift(2)⊗[[s]][x:=[[t]]]⊕lift(⟨something⟩⊕1)≻[[s]][x:=[[t]]], which equals [[s[x:=t]]]
by Lemma 5.5.
•
[[tappλα.σ,τ(Λα.s)]]≻[[s[α:=τ]]]
We have
[[tappλα.σ,τ(Λα.s)]]⇝β∗lift(λα.[[σ]])[[τ]](2)⊗((Λα.[[s]])∗β)⊕lift(λα.[[σ]])[[τ]](1)⇝lift(2)⊗[[s]][α:=[[τ]]]⊕lift(1)≻[[s]][α:=[[τ]]]=[[s[α:=τ]]], using Lemma
5.5.
•
[[prσ,τ1(pairσ,τ(s,t))]]≻[[s]]
We have
[[pairσ,τ(s,t)]]⇝β∗⟨[[s]],[[t]]⟩⊕lift[[σ]]×[[τ]](flatten[[σ]]([[s]])⊕flatten[[τ]]([[t]])) and therefore
[[prα,β1(pairα,β(s,t))]]⇝β∗lift[[σ]](2)⊗π1(⟨[[s]],[[t]]⟩⊕⟨something⟩)⊕lift[[σ]](1)⪰π1(⟨[[s]],[[t]]⟩)⊕lift[[σ]](1),
which ≻[[s]] by Lemma B.1.
•
[[prσ,τ2(pairσ,τ(s,t))]]≻[[t]]
Analogous to the inequality above.
•
[[caseσ,τ,ρ(inσ,τ1(u),λx.s,λy.t)]]≻[[s[x:=u]]]
Write A:=lift[[σ]]×[[τ]](flatten[[σ]]([[u]]));
then [[inσ,τ1(u)]]=⟨[[u]],lift[[τ]](1)⟩⊕A.
Let B:=flatten[[σ]]×[[τ]](⟨[[u]],lift[[τ]](1)⟩⊕A) and C:=[[λy.t]]⋅π2(⟨[[u]],lift[[τ]](1)⟩⊕A).
Then we can write:
[[caseσ,τ,ρ(inσ,τ1(u),λx.s,λy.t)]]=lift[[ρ]](2)⊕lift[[ρ]](3⊗B)⊕lift[[ρ]](B⊕1)⊗([[λx.s]]⋅π1(⟨[[u]],lift[[τ]](1)⟩⊕A)⊕C).
By splitting additive terms, distribution, neutrality of 1 and
absolute positiveness, this ≻[[λx.s]]⋅π1(⟨[[u]],liftτ(1)⟩)⇝∗[[λx.s]]⋅[[u]] (by
Lemma B.1), =(λx.[[s]])⋅[[u]]⇝β∗[[s]][x:=[[u]]]=[[s[x:=u]]] by Lemma 5.5.
We have
[[extφ,τ(s)]]⪰[[[τ]],[[s]]] by absolute positiveness.
Therefore, using monotonicity,
[[letφ,ρ(extφ,τ(s),Λα.λx:[[φ]]α.t)]]⪰lift[[ρ]](2)⊗(let[[ρ]][[[τ]],[[s]]]be[[α,x]]in[[Λα.λx:φα.t]]∗α⋅x)⊕⟨something⟩⊕lift[[ρ]](1).
Again by absolute positiveness, this ≻let[[ρ]][[[τ]],[[s]]]be[[α,x]]in[[Λα.λx:[[φ]]α.t]]∗α⋅x⇝let[[ρ]][[[τ]],[[s]]]be[[α,x]]in[[t]].
By Lemma B.1, this term
⪰[[t]][α:=[[τ]]][x:=[[s]]].
We complete by Lemma
5.5.
•
[[ϵτ(ϵ⊥(s))]]≻[[ϵτ(s)]].
We have [[ϵτ(ϵ⊥(s))]]=lift[[τ]](2⊗liftNature(2⊗[[s]]⊕1)⊕1)≈lift[[τ]](4⊗[[s]]⊕3)≻lift[[τ]](2⊗[[s]]⊕1)=[[ϵτ(s)]].
•
\llbracket@σ,τ(ϵσ→τ(s),t)]]≻[[ϵτ(s)]].
We have
\llbracket@σ,τ(ϵσ→τ(s),t)]]=lift[[τ]](2)⊗(lift[[σ]]→[[τ]](2⊗[[s]]⊕1)⋅[[t]])⊕lift[[τ]](⟨something⟩⊕1)≻lift[[σ]]→[[τ]](2⊗[[s]]⊕1)⋅[[t]]⇝lift[[τ]](2⊗[[s]]⊕1)=[[ϵτ(s)]].
•
[[tappφ,τ(ϵ∀α.φα(s))]]≻[[ϵφτ(s)]]
We have [[tappφ,τ(ϵ∀α.φα(s))]]=lift[[φ]][[τ]](2)⊗(lift∀α.[[φ]]α(2⊗[[s]]⊕1)∗[[τ]])⊕lift[[φ]][[τ]](1)≻lift∀α.[[φ]]α(2⊗[[s]]⊕1)∗[[τ]]=(Λα.lift[[φ]]α(2⊗[[s]]⊕1))∗[[τ]]⇝lift[[φ]][[τ]](2⊗[[s]]⊕1)=lift[[φτ]](2⊗[[s]]⊕1)=[[ϵφτ(s)]]
•
[[prσ,τ1(ϵandστ(s))]]≻[[ϵσ(s)]]
We have
[[prσ,τ1(ϵandστ(s))]]=lift[[σ]](2)⊗π1(lift[[σ]]×[[τ]](2⊗[[s]]⊕1))⊕lift[[σ]](1)≻π1(lift[[σ]]×[[τ]](2⊗[[s]]⊕1))=lift∀p.([[σ]]→[[τ]]→p)→p(2⊗[[s]]⊕1))∗[[σ]]⋅(λxy.x)=(Λp.λf.liftp(2⊗[[s]]⊕1))∗[[σ]]⋅(λxy.x)⇝∗lift[[σ]](2⊗[[s]]⊕1)=[[ϵσ(s)]].
We have [[caseσ,τ,ρ(ϵorστ(u),λx.s,λy.t)]]=lift[[ρ]](2)⊕lift[[ρ]](3⊗flatten[[σ]]×[[τ]](lift[[σ]]×[[τ]](2⊗[[u]]⊕1)))⊕⟨something⟩≻lift[[ρ]](3⊗flatten[[σ]]×[[τ]](lift[[σ]]×[[τ]](2⊗[[u]]⊕1)))⪰lift[[ρ]](flatten[[σ]]×[[τ]](lift[[σ]]×[[τ]](2⊗[[u]]⊕1)))≈lift[[ρ]](2⊗[[u]]⊕1)=[[ϵρ(u)]] because flattenσ(liftσ(n))≈n for all σ,n.
Unfortunately, the rules where case is shifted to the root
are rather more complicated, largely due to the variable
multiplication in J(case) – which we had to choose
because these rules may duplicate variables.
Taking into account that [[ρ]]×[[τ]] is just shorthand notation for
∀p.([[ρ]]→[[τ]]→p)→p, that π1(x)=x∗[[ρ]]⋅(λxy.x), and that liftσ→τ(x)⋅y≈liftτ(x), this term ≈
[TABLE]
On the right-hand side, we have:
[TABLE]
Following the definition of π1, we can pull the substitution
inside π1, and rewrite this term to:
[TABLE]
This is once more oriented by absolute positiveness.
Now, if we strike out equal terms in the left-hand side and the
right-hand side (after splitting additive terms where needed)
the following inequality remains:
[TABLE]
But now note that A⪰su and A⪰tu. Therefore, by
monotonicity, each term Li⪰ Ri below:
[TABLE]
[TABLE]
This merely leaves the following proof obligation:
[TABLE]
Since lift[[ξ]](3)⊗s≈s⊕s⊕s, we can eliminate all remaining terms (for
example: lift[[ξ]](3)⊗[[v]][z:=π1(A)]≈[[v]][z:=π1(A)]⊕[[v]][z:=π1(A)]⊕[[v]][z:=π1(A)]⪰vsu⊕vtu); thus, the
inequality holds.
In the following, let us denote vN:=[[v]]∗Nature⋅lift[[φ]]Nature(0)
and uf:=flatten[[σ]]×[[τ]]([[u]]). With these abbreviations, we have the
following on the left-hand side:
[TABLE]
[TABLE]
On the right-hand side, we have:
[TABLE]
[TABLE]
The last step follows because x occurs only in s, and y occurs
only in t. This term can now be reordered to:
[TABLE]
We conclude once more by absolute positiveness.
Bibliography26
The reference list from the paper itself. Each links out to its DOI / PubMed record.
1[1] F. Blanqui. Definitions by rewriting in the calculus of constructions. MSCS , 15(1):37–92, 2005.
2[2] D. Cousineau and G. Dowek. Embedding pure type systemsin the lambda-pi-calculus modulo. In TLCA , pages 102–117, 2017.
3[3] G. Dowek. Models and termination of proof reduction in the λ π 𝜆 𝜋 \lambda\pi -calculus modulo theory. In ICALP , pages 109:1–109:14, 2017.
4[4] M. Fiore and M. Hamana. Multiversal polymorphic algebraic theories: syntacs, semantics, translations and equational logic. In LICS , pages 520–520, 2013.
5[5] C. Fuhs and C. Kop. Polynomial interpretations for higher-order rewriting. In RTA , pages 176–192, 2012.
6[6] J.-V. Girard, P. Taylor, and Y. Lafont. Proofs and Types . Cambridge University Press, 1989.
7[7] J.-Y. Girard. Une extension de l’interpretation de Gödel a l’analyse, et son application a l’elimination des coupures dans l’analyse et la theorie des types. In SLS , pages 63 – 92. Elsevier, 1971.
8[8] M. Hamana. Polymorphic rewrite rules: Confluence, type inference, and instance validation. In FLOPS , pages 99–115, 2018.
