A Predicative Strong Normalisation Proof for a λ-calculus with Interleaving Inductive Types

Andreas Abel^{1} and Thorsten Altenkirch^{2}

1 Department of Computer Science, University of Munich

               abel@informatik.uni-muenchen.de

2 School of Computer Science & Information Technology, University of Nottingham

                      txa@cs.nott.ac.uk

Abstract. We present a new strong normalisation proof for a λ-calculus with interleaving strictly positive inductive types λ^{μ} which avoids the use of impredicative reasoning, i.e., the theorem of Knaster-Tarski. Instead it only uses predicative, i.e., strictly positive inductive definitions on the metalevel. To achieve this we show that every strictly positive operator on types gives rise to an operator on saturated sets which is not only monotone but also (deterministically) set based – a concept introduced by Peter Aczel in the context of intuitionistic set theory. We also extend this to coinductive types using greatest fixpoints of strictly monotone operators on the metalevel.

1 Introduction

We shall investigate a λ-calculus with strictly positive^{1} inductive types. I.e., given a type σ(X) where X appears only strictly positive we may construct a new type μX.σ which is generated by the constructor c : σ(μX.σ) → μX.σ. Examples are the natural numbers Nat = μX.1 + X, lists over a given type τ: List^{τ} = μX.1 + τ × X or trees branching over τ: Tree^{τ} = μX.1 + (τ → X). We also allow interleaving inductive types, as an example consider arbitrarily but finitely branching trees which can be defined by

Fin = μX.List^{X} = μX.μY.1 + X × Y

We call Fin interleaving because the inductive definition goes through another inductive type – List. A type like Tree^{Nat} is nested but not interleaved. ^{2}

1 The occurrence of a type variable is positive iff it occurs within an even number of left hand sides of →-types, it is strictly positive iff it never occurs on the left hand side of a →-type. We will only use strictly positive occurrences in this paper because positive inductive types cannot be understood predicatively in general.

2 The use of the term interleaving for this situation is due to Ralph Matthes, e.g., see [Mat98]. An alternative would be mutually.

Positivity is essential for normalisation, i.e., we do not allow recursive domain equations like X = X → X which may be represented by the type μX.X → X. The difference between positive and strictly positive is more subtle, i.e., μX.(X → Bool) → Bool is an example of a positive but not strictly positive type. This example has been used by Reynolds to show that there are no settheoretical models of System F [Rey84].

We consider λ^{μ} as a simply typed programming language corresponding to a subset of Martin-Löf’s Type Theory (MLTT) [Mar84]. For our system we show the important property of strong normalisation, following the idea of Tait [Tai67]. To show strong normalisation of the simply typed λ-calculus, he defined a set-valued interpreting function [[−]] on the types. For each type σ the set [[σ]] contains the computable terms of type σ. Later Girard extended this idea to the impredicative System F under the name candidates of reducibility [Gir72]. Our construction is based on a technical alternative to candidates called saturated sets - this technique has been used by Luo [Luo90] and by the second author [Alt93]. Since in our system a type σ may contain free variables, the interpretation [[σ]] is no longer just a saturated set but a monotone operator on saturated sets.

Now we could just adopt the normalisation proof for System F and use Knaster’s and Tarski’s theorem, stating that every monotone operator on a complete lattice has a least fixed point, to define the interpretation for μ-types. But this construction would require impredicative reasoning and the full prooftheoretical strength of System F. It could not be carried out in a predicative meta theory like MLTT. Should it not be possible to reason about a predicative system like λ^{μ} in a predicative^{3} meta theory, as for instance, MLTT?

Predicative theories allow only strictly positive inductive definitions. That means they must be given by an operator Φ(P) where P only occurs strictly positive, i.e., never on the left hand side of an arrow. Φ defines a set μ which is characterized as the smallest set closed under Φ:

\overline{(intro)} ; Φ(μ) ⊆ μ  Φ(Q) ⊆ Q ; \overline{(elim)} ; μ ⊆ Q

Strictly positive inductive definitions can be understood as defined by well founded derivation trees which may be infinitely branching. Hence, when building a derivation, we only refer to subderivations which are smaller in an intuitive sense. In this way the consistency of predicative theories can be justified, whereas the consistency of impredicative theories is only empiric. Furthermore there are more options to extend a weaker, i.e., predicative theory without getting into inconsistencies.

In this paper we show that indeed the strong normalisation of λ^{μ} can be proven by predicative means. We manage to define the interpretation [[−]] of the types without Knaster-Tarski, just by strictly positive inductive definitions, using the concept of (deterministically) set based operators introduced by Peter

3 We are using the term predicative in the sense of avoiding circular definitions — this usage has been popularized by Per Martin-Löf. In the terminology of proof theory our system would be called impredicative since its ordinal is greater than Γ_{0}.

Aczel in the context of intuitionistic set theory [Acz97]. Intuitively, a set based operator can be understood as a monotone operator Φ which comes with a urelement relation U. We require that if y ∈ Φ(P) and x U y (read x is an urelement of y) then x ∈ P. We also require that the urelements can be used to reconstruct the whole, i.e., y ∈ Φ({x | x U y}) for reasonable y ∈ Φ(True). For any monotone operator Φ which satisfies the conditions given above the predicate x ∈ Φ(P) can be replaced by the conditions x ∈ Φ(True) and ∀y U x → y ∈ P which is strictly positive in P (see proposition 1). We have used this technique in [AA99] to construct a value semantics for the types of the foetus system predicatively.

As an example consider Φ_{List} which can be defined inductively (writing [] for the empty list and :: for cons):

[] ∈ Φ_{List}(P)

a ∈ P l ∈ Φ_{List}(P)
a :: l ∈ Φ_{List}(P)

The appropriate relation U_{List} can be defined inductively as well:

a U_{List} a :: l  a U_{List} l ; a U_{List} b :: l

It is now straightforward to verify that Φ_{List} is set based by rule induction.

We show that every strictly positive type can be interpreted by a set based operator and that fixpoints of set based operators can be constructed by strictly positive inductive definitions on the meta level. Unsurprisingly, we need additional power on the metalevel which is given by one level of reflection corresponding to the introduction of a Martin-Löf universe. Specifically, this is required when defining the interpretation of types [[σ]].

We also extend the construction to coinductive or lazy types (like the type of Streams over τ which is given by Stream^{τ} = νX.τ × X). To do so we consider strictly positive definitions of greatest fixpoints as predicatively acceptable. This assumption is based on the work on coinductive types in Type Theory [Coq94]. Intuitively, greatest fixpoints correspond to arbitrary trees, i.e., not necessarily well founded ones.

To be precise: We assume that given a propositional expression Φ(P) s.t. P appears strictly positive, it is possible to construct the greatest fixpoint ν of Φ, s.t.

\overline{(co-intro)} ; ν ⊆ Φ(ν)  Q ⊆ Φ(Q) ; \overline{(co-elim)} ; Q ⊆ ν

1.1 Related work

Lambda calculi with inductive types have been considered by a number of authors, e.g., see [Hag87,Men88,Dyb91,CM89,Geu92,Loa97,Alt98]. Loader notes that strong normalisation can be shown by using the techniques from System F. This is carried out for monotone inductive types with primitive recursion by Ralph Matthes [Mat98], using an impredicative meta theory. Benl presents a predicative strong normalisation proof for non-interleaving inductive types [Ben98], but this has not been extended to interleaving inductive types or coinductive types.

Jouannaud and Okada [JO97], later with Blanqui [BJO99], also do not treat interleaving inductive types, which they call mutually inductive. Furthermore their normalisation proof is not predicative from our perspective, since they use the theorem of Knaster and Tarski to construct the computability predicates. This requires quantification over all such predicates, which can only be carried out in an impredicative meta theory.

The system we are investigating here is closely related to the proof-theoretical system ID_{<ω}^{i}. However, we differ in allowing interleaving inductive definitions which correspond to simultaneously defined sets. It is not clear in the moment whether Buchholz’ reduction from ID_{α}^{c} to ID_{α}^{i} [Buc81], which also justifies positive inductive definitions, can be extended to our system.

1.2 Acknowledgments

Thierry Coquand has pointed out to us that one should use set based operators to prove normalisation predicatively. We would also like to acknowledge discussions with Peter Aczel on set based operators. Helmut Schwichtenberg allowed us to present this work to his group, where we got interesting feedback from him and his colleagues. Ralph Matthes gave a lot of very helpful comments on the draft. We would also like to thank the anonymous referees who invested a lot of time and effort to write reports which helped us to improve the paper.

1.3 Notational conventions

We are using a vector notation to simplify our notation. If we have a family of expressions e_{1}, e_{2}, …, e_{n} we write e for the whole sequence. We denote the length n of the sequence by |e|. Given a fixed e we write ee for e_{1}e, e_{2}e, …, e_{n}e. Given a sequence of sets S where |S| = n we write ΠS for S_{1} × S_{2} × ⋯ × S_{n}.

We use set notation to define predicates, i.e., we write x ∈ P for P (x) and we define new predicates by the notation for set comprehension. However, sets are not first order citizens in our meta theory, i.e., we do not quantify over sets and we do not use power sets. We write relations infix, i.e., we write x R y for (x, y) ∈ R. We write projections as partial applications, i.e., R(y) = {x | x R y}.

We will annotate term families by types but to increase readability we will often omit these annotations. We use the convention that all arrow symbols associate to the right. We consider types and terms upto alpha-equivalence and use ≡ to denote this.

2 The Calculus λ^{μ}

We already presented this calculus in [Alt98] also allowing positive inductive types. We shall simplify the presentation here by exploiting the fact that we are only interested in strictly positive types, following [Loa97,Abe99]. The choice of type formers presented here is quite canonical and corresponds to bicartesian closed categories which have also initial algebras for all definable endofunctors.

We assume a set of type variables X, we denote elements of X by X, Y, Z and finite sequences of type variables by X, Y , Z. The extension of X by Y is denoted by X, Y. We define the set of types in which the variables X occur at most strictly positive Ty(X) inductively by the following rules:

\overline{(Const)} ; 0, 1 ∈ Ty(X) \overline{(Var)} ; X_{i} ∈ Ty(X) σ ∈ Ty() τ ∈ Ty(X) \overline{(Arr)}

σ → τ ∈ Ty(X)

σ, τ ∈ Ty(X)
\overline{(Sum),(Prod)}
σ + τ, σ × τ ∈ Ty(X)

σ ∈ Ty(X, Y) ; \overline{(Mu)} ; μY.σ ∈ Ty(X)

Closed types are denoted by Ty = Ty(). If σ ∈ Ty(X) and τ_{i} ∈ Ty for 1 ≤ i ≤ |X| we write σ(τ) ∈ Ty for the result of substituting X_{i} in σ by τ_{i} in a capture avoiding way.

Different to System F, we can restrict the typing rules to closed types because we have no term forming rules which introduce new type variables (like Λ in the case of System F). A type context Γ is a finite sequence of assumptions of the form x : σ where x ∈ V is a term variable and σ ∈ Ty. We require that all the variables in a context are different. We introduce the judgment Γ ⊢ t : σ meaning that t has the type σ in context Γ, where σ ∈ Ty. Γ ⊢ t : σ is given by the usual rules for simply typed λ calculus:

\overline{var} ; Γ, x : σ, Δ ⊢ x : σ Γ, x : σ ⊢ t : τ ; \overline{lam} ; Γ ⊢ λx^{σ}.t : σ → τ {Γ ⊢ t : σ → τ Γ ⊢ u : σ \atop Γ ⊢ tu : τ}app

Additionally we assume a set of constants C and a signature given by Σ ⊆ C ×Ty which is decidable. We introduce the rule

c : σ ∈ Σ ; \overline{const} ; Γ ⊢ c : σ

For λ^{μ} we consider the following signature Σ^{μ}

unit : 1
pair^{σ_{1},σ_{2}} : σ_{1} → σ_{2} → (σ_{1} × σ_{2})
π_{i}^{σ_{1},σ_{2}} : (σ_{1} × σ_{2}) → σ_{i}  i ∈ {1, 2}
case_{0}^{σ} : 0 → σ
in_{i}^{σ_{1},σ_{2}} : σ_{i} → (σ_{1} + σ_{2})  i ∈ {1, 2}
case^{σ_{1},σ_{2},ρ} : (σ_{1} → ρ) → (σ_{2} → ρ) → (σ_{1} + σ_{2}) → ρ
c^{X.τ} : τ(μX.τ) → μX.τ
It^{X.τ,σ} : (τ(σ) → σ) → (μX.τ) → σ

where σ, σ_{i}, ρ ∈ Ty and τ ∈ Ty(X). We will often omit type annotations when they are clear from the context.

We write Tm^{σ} for the set of terms of type σ:

Tm^{σ} = {t|∃Γ.Γ ⊢ t : σ}

Since we only allow strictly positive occurrences of type variables every type gives rise to a functor in the sense of category theory. We exploit this by defining the functorial strength of a type ρ ∈ Ty(X): Given f_{i} ∈ σ_{i} → τ_{i} for 1 ≤ i ≤ n, where n = |X| we define

ρ(f) : ρ(σ) → ρ(τ)

by induction over the structure of ρ: ^{4}

C(f) = λx^{C}.x  C ∈ {0, 1}
X_{i}(f) = f_{i}  1 ≤ i ≤ n
(ρ_{1} → ρ_{2})(f) = λg^{ρ_{1}→ρ_{2}(σ)}.λx^{ρ_{1}}.ρ_{2}(f)(gx)
(ρ_{1} × ρ_{2})(f) = λp^{ρ_{1}(σ)×ρ_{2}(σ)}. pair^{ρ_{1}(τ)×ρ_{2}(τ)}(ρ_{1}(f)(π_{1}p))(ρ_{2}(f)(π_{2}p))
(ρ_{1} + ρ_{2})(f) = case^{ρ_{1}(σ),ρ_{2}(σ),ρ_{1}(τ)+ρ_{2}(τ)}

(λx^{ρ_{1}(σ)}. in_{1}(ρ_{1}(f)x))(λy^{ρ_{2}(σ)}. in_{2}(ρ_{2}(f)y))

(μX.ρ)(f) = It^{X.ρ(σ,X),μα}(λx^{ρ(σ,μα)}. c^{α}(ρ(f, λy^{μα}.y)x))

where α abbreviates X.ρ(τ , X)

This operation is motivated by the fact that each ρ gives rise to a (strong) functor. We allow a partial instantiation of ρ which can be defined by instantiating all other places with the identity function λx^{σ}.x. The strength is needed in the definition of the β-rule for μ types, which, read as an equation, corresponds to weak initiality of the appropriate ρ(−)-algebra.

We are now ready to define the reduction relation ⊳_{1} ⊆ Tm × Tm. We first define top level β-reduction by the following axioms

(λx.t)u ⊳_{β} u[x := t]
π_{i}(pair t_{1}t_{2}) ⊳_{β} t_{i}  i ∈ {1, 2}
case t_{1}t_{2}(in_{i} u) ⊳_{β} t_{i}u  i ∈ {1, 2}
It^{X.ρ} t(c u) ⊳_{β} t(ρ(It^{X.ρ} t)u)

and then define ⊳_{1} ⊆ Tm × Tm as the congruence closure:

{t ⊳_{β} u \atop t ⊳_{1} u} {t ⊳_{1} t′ \atop tu ⊳_{1} t′u} {u ⊳_{1} u′ \atop tu ⊳_{1} tu′} {t ⊳_{1} t′ \atop λx.t ⊳_{1} λx.t′}

We define the set of strongly normalizing terms SN^{σ} of type σ inductively by the rule:

t ∈ Tm^{σ} ∀t′ ∈ Tm^{σ}.(t ⊳_{1} t′) ⟹ t′ ∈ SN^{σ}
t ∈ SN^{σ}

Our goal is to give a predicative proof of the strong normalization theorem:

4 The case for → works only because ρ_{1} is closed by definition.

Theorem 1. {t ∈ Tm^{σ} \atop t ∈ SN^{σ}}

3 Proving Strong Normalisation using Saturated Sets

Even for the simply typed lambda calculus strong normalisation cannot be proven by a mere induction over the term structure, since an application (λx.t) s can beta-reduce to a term t[x := s] that neither is a subterm of t nor of s. To strengthen the induction hypothesis, Tait [Tai67] introduced the set of computable terms [[σ]] ⊆ SN^{σ} of type σ. E.g., given P ⊆ SN^{σ}, Q ⊆ SN^{τ} we define

P ⇒ Q := {t ∈ SN^{σ→τ} | ∀u ∈ P. t u ∈ Q}
[[σ → τ]] := [[σ]] ⇒ [[τ]]

The new obligation Tm^{σ} ⊆ [[σ]] can be proven by induction over the terms (cf. Prop. 11) and the application case now is trivial.

But how does one extend this to other types, like the type of natural numbers? In [GLT89] it is suggested to interpret Nat by all strongly normalizing terms of this type. However, one has to pay a high price for this when showing the soundness of the eliminator and it is not clear how this technique can be extended to systems like the one presented here. Here we follow a different way and construct the interpretation of all other types introduction based, i.e.,

0 ∈ [[Nat]]  {t ∈ [[Nat]] \atop S t ∈ [[Nat]]}

However, there are a lot of strongly normalizing terms which are not included in this definition. The basic idea is that the computable terms are the ones such that all computation paths end up in [[Nat]], i.e., we may want to add the following rule

t ∈ Tm^{Nat} ∀u.t ⊳_{1} u ⟹ u ∈ [[Nat]]
\overline{(comp)}
t ∈ [[Nat]]

But this is just the definition of SN^{Nat}! The key technical insight we use is to restrict attention to (strongly normalizing) terms whose canonical computation, which we call weak head reduction (⊳_{whd}), ends up in [[Nat]] or which are canonically irreducible, such terms we call void (Void). Sets of strongly normalizing terms which are closed under canonical computations and which include all void terms we call saturated (SAT). In the example we would replace the rule (comp) by the two rules

t ∈ Void^{Nat} ; \overline{(sat1)} ; t ∈ [[Nat]]

t ∈ SN^{Nat} t ⊳_{whd} t′ t′ ∈ [[Nat]]
\overline{(sat2)}
t ∈ [[Nat]]

We are now going to define the notions Void and ⊳_{whd} for our calculus.^{5} We define evaluation contexts as eliminator terms with a hole in the key position

E[X] ::= X t_{1} | π_{j} X | case t_{1} t_{2} X | It t_{1} X

Weak head reduction ⊳_{whd} ⊆ ⊳_{1} is defined as the least relation closed under the β-axioms and under evaluation contexts.

{t ⊳_{β} u \atop t ⊳_{1} u}  {t ⊳_{whd} u \atop E[t] ⊳_{whd} E[u]}

Note that ⊳_{whd} is deterministic. Furthermore we define the set Void as the least set which includes variables and which is closed under evaluation contexts:

{x ∈ V \atop x ∈ Void}

t ∈ Void E[x] ∈ SN
E[t] ∈ Void

We write Void^{σ} for Void ∩ Tm^{σ}. We verify the syntactic properties which are needed in the proof and which motivate the definition of ⊳_{whd}:

Lemma 1.

1. {t ⊳_{whd} u  t ⊳ t′ \atop u ≡ t′ ∨ ∃u′.t′ ⊳_{whd} u′ ∧ u ⊳^{∗} u′}

2. t ∈ Void E[x] ∈ SN

E[t] ∈ SN

3. {t ⊳_{whd} t′  E[t′] ∈ SN \atop E[t] ∈ SN}

4. {E[t] ⊳_{whd} t′  t, t′, E[x] ∈ SN \atop E[t] ∈ SN}

We omit the proof here. Note that the first property is a weak form of standardisation, expressing that weak head reduction can only be postponed but not avoided. This property is needed to show some of the other properties, which in general can be verified by rule induction over the definition of SN. A simple corollary of 2. is that Void ⊆ SN.

Given a set of strongly normalizing terms P ⊆ SN^{σ} we define its saturation P^{∗} ⊆ SN^{σ} as the least set closed under

t ∈ P ; \overline{(emb)} ; t ∈ P^{∗} t ∈ Void^{σ} ; \overline{(sat1)} ; t ∈ P^{∗} t ∈ SN^{σ} t ⊳_{whd} t′ t′ ∈ P^{∗}

\overline{(sat2)}
t ∈ P^{∗}

We say that a set P ⊆ SN^{σ} is saturated iff P^{∗} ⊆ P and write P ∈ SAT^{σ}. Obviously, P^{∗} ∈ SAT^{σ}.

4 A Predicative Interpretation of Types

Following Tait, the interpretations [[σ]] of all closed types σ ∈ Ty will be saturated sets. But how about the types with free type variables? We use Girard’s

5 Note that the type Nat can be represented as μX.1 + X, then define 0 = c^{X.1+X}(in_{1} unit) : Nat, S = λx^{Nat}.c^{X.1+X}(in_{2} x) : Nat → Nat

approach, who extended Tait’s method to System F [Gir72]: Open types are operators on saturated sets (Girard actually used his candidate sets, which are more restrictive than saturated sets). Transferred to our notation and terminology, he defined the semantics of second-order quantified types as

[[ΠY.σ(X)]](P) := ⋂_{Q∈SAT} [[σ(X, Y)]](P , Q)

making splendid use of impredicativity: He quantifies over all saturated sets while defining one. Since we do not quantify over types but use open types only to define recursive types, we can give the interpretation by inductive definitions (i.e., predicatively). Technically, this requires the “urelement” relation U to be defined simultaneously with the interpretations. Given σ ∈ Ty(X) and closed types τ_{i} ∈ Ty for 1 ≤ i ≤ n = |X|, we will define

[[σ]](P) ⊆ SN^{σ(τ)}  P_{i} ⊆ SN^{τ_{i}} for 1 ≤ i ≤ n
U_{i}^{σ} ⊆ Tm^{τ_{i}} × Tm^{σ(τ)} 1 ≤ i ≤ n

such that the following properties hold:

Saturated If all P_{i} ∈ SAT^{τ_{i}} then [[σ]](P) ∈ SAT^{σ(τ)} Monotone [[σ]] is monotone in all arguments, i.e.,

∀1 ≤ i ≤ n. P_{i} ⊆ Q_{i}
\overline{(mon)}
[[σ]](P) ⊆ [[σ]](Q)

Set based [[σ]] is set based by U^{σ}. For all 1 ≤ i ≤ n, t ∈ SN^{σ(τ)} and u ∈ SN^{τ_{i}} the interpretation [[σ]] satisfies

t ∈ [[σ]](P)  u U_{i}^{σ} t ; \overline{(sb1)} ; u ∈ P_{i}  t ∈ [[σ]](SN^{τ}) ; \overline{(sb2)} ; t ∈ [[σ]](U^{σ}(t))

Note that (sb1) can be read as t ∈ [[σ]](P) ⟹ U_{i}^{σ}(t) ⊆ P_{i}. Informally, this states that the ith component urelements of t must be in the original set of urelements P_{i}. Likewise, (sb2) states that t must be reconstructible out of the urelements extracted from t.

We require the operators to be set based for the following reason: The interpretation M := [[μX.σ]](P) of an inductive type is defined by

t ∈ [[σ]](P , M)
\overline{(cons′)}
c t ∈ M

However, this cannot be a rule of an inductive definition since M, which we want to define, does not appear strictly positive in the premise. Although X appears strictly positive in the type σ, M cannot be said to appear strictly positive, since it is argument of [[σ]], not of σ, and we do not know “what the operator is doing with M”. Monotonicity is not strong enough for our purposes, and this is where set-basedness comes in:

Proposition 1. Every [[σ]](P) is equivalent to a predicate which is strictly positive in P - that is for t ∈ SN^{σ(τ)}:

t ∈ [[σ]](P) ⟺ t ∈ [[σ]](SN^{τ}) ∧ ∀i. U_{i}^{σ}(t) ⊆ P_{i}

Proof.

⇒ Assuming t ∈ [[σ]](P), we obtain t ∈ [[σ]](SN^{τ}) by (mon) and U_{i}^{σ}(t) ⊆ P_{i} for

all i by (sb1). ⇐ Using (sb2), t ∈ [[σ]](SN^{τ}) entails

t ∈ [[σ]](U^{σ}(t))

Since by assumption U^{σ}(t) ⊆ P (component wise), we can derive t ∈ [[σ]](P) by (mon). ⊓ ⊔

In the following we give definitions for [[σ]] and U^{σ}.

(Const),(Var),(Arr) Let σ ∈ Ty and X_{i}, τ ∈ Ty(X)

[[0]](P) = {}^{∗}  u U_{i}^{0} t ⟺ False
[[1]](P) = {unit}^{∗}  u U_{i}^{1} t ⟺ False
[[X_{i}]](P) = P_{i}  u U_{j}^{X_{i}} t ⟺ i = j ∧ u ≡ t
[[σ → τ]](P) = [[σ]] ⇒ ([[τ]](P)) u U_{i}^{σ→τ} t ⟺ ∃t′ ∈ [[σ]]. u U_{i}^{τ} t t′

The following lemma is standard, e.g. see [Alt93] for a proof:

Lemma 2. Given P ⊆ SN^{σ} and Q ∈ SAT^{τ} we have that P ⇒ Q ∈ SAT^{σ→τ}.

Proposition 2. The interpretations [[0]], [[1]], [[X_{i}]], [[σ → τ]] are saturated, monotone and set based.

Proof. We verify here the (only interesting) case that [[σ → τ]] is set based:

(sb1) Given t ∈ [[σ → τ]](P) and u U_{i}^{σ→τ} t we know that there is a t′ ∈ [[σ]] s.t.

u U_{i}^{σ→τ} tt′. Since tt′ ∈ [[τ]](P) we can use (sb1) for τ to conclude u ∈ P_{i}. (sb2) Given t ∈ [[σ → τ]](SN^{τ}) we have to show that t ∈ [[σ → τ]](U^{σ→τ} (t)):

Assume u ∈ [[σ]] we can use the hypothesis to show that tu ∈ SN and hence by (sb2) for τ tu ∈ [[τ]](U^{τ} (tu)). Clearly U_{i}^{τ} (tu) ⊆ U_{i}^{σ→τ} t and hence using mon of [[τ]] we have tu ∈ [[τ]](U^{σ→τ} (t)) as required. ⊓ ⊔

(Prod) Given σ_{1}, σ_{2} ∈ Ty(X) we define

[[σ_{1} × σ_{2}]](P) = {pair t_{1}t_{2} | ∀j ∈ {1, 2}. t_{j} ∈ [[σ_{j}]](P)}^{∗}  (1)

We define U_{i}^{σ_{1}×σ_{2}} inductively by the following rules

j ∈ {1, 2} u U_{i}^{σ_{j}} t_{j}
\overline{(pair)}
u U_{i}^{σ_{1}×σ_{2}} pair t_{1}t_{2}

t ∈ SN t ⊳_{whd} t′ u U_{i}^{σ_{1}×σ_{2}} t′
\overline{(clos^{×})}
u U_{i}^{σ_{1}×σ_{2}} t

Proposition 3. The interpretation [[σ_{1} × σ_{2}]] of the product is monotone and set based.

Proof. Since (mon) is obvious in this and all subsequent cases we concentrate on set based:

(sb1) Given t ∈ [[σ_{1} × σ_{2}]](P) to show

u U_{i}^{σ_{1}×σ_{2}} t ⟹ u ∈ P_{i}

we exploit that the closure (1) is defined inductively and analyze the cases: (emb) t ≡ pair t_{1} t_{2} where t_{j} ∈ [[σ_{j}]](P). Hence u U_{i}^{σ_{1}×σ_{2}} t can only have

been derived from u U_{i}^{σ_{j}} t_{j}. Then (sb1) for σ_{j} implies u ∈ P_{i}. (sat1) For t ∈ Void the precondition u U_{i}^{σ_{1}×σ_{2}} t is never derivable. (sat2) We have t ∈ SN and t ⊳_{whd} t′ and assume u U_{i}^{σ_{1}×σ_{2}} t to show u ∈ P_{i}. Since t has a weak head reduct, it cannot be of the form pair t_{1}t_{2}. Thus u U_{i}^{σ_{1}×σ_{2}} t can only have been derived by (clos^{×}) and since ⊳_{whd} is deterministic we have u U_{i}^{σ_{1}×σ_{2}} t′. Now, the ind.hyp. for t′ entails u ∈ P_{i}.

(sb2) Given t ∈ [[σ_{1} × σ_{2}]](SN) we show

t ∈ [[σ_{1} × σ_{2}]](U^{σ_{1}×σ_{2}}(t))

by induction over the closure rules:

(emb) t ≡ pair t_{1} t_{2} where t_{j} ∈ [[σ_{j}]](SN). We apply the ind.hyp. to derive t_{j} ∈ [[σ_{j}]](U^{σ_{j}}(t_{j})). Since U_{i}^{σ_{j}}(t_{j}) ⊆ U_{i}^{σ_{1}×σ_{2}}(pair t_{1} t_{2}) by (pair) we use (mon) to derive t_{j} ∈ [[σ_{j}]](U^{σ_{1}×σ_{2}}(pair t_{1}t_{2})) and hence t ∈

[[σ_{1} × σ_{2}]](U^{σ_{1}×σ_{2}}(t)).

(sat1) Since [[σ_{1} × σ_{2}]] is defined as a closure it contains all t ∈ Void.

(sat2) We have t ∈ SN, t⊳_{whd}t′, and the ind.hyp. t′ ∈ [[σ_{1} × σ_{2}]](U^{σ_{1}×σ_{2}}(t′)). (clos^{×}) implies that U^{σ_{1}×σ_{2}}(t′) ⊆ U^{σ_{1}×σ_{2}}(t) and hence using (mon) we know t′ ∈ [[σ_{1} × σ_{2}]](U^{σ_{1}×σ_{2}}(t)). We use the premises again and apply

(sat2) for [[σ_{1} × σ_{2}]] to derive t ∈ [[σ_{1} × σ_{2}]](U^{σ_{1}×σ_{2}}(t))
⊓ ⊔

Since we have not used ×-specific properties in the case that the last step was (clos^{×}) we can transfer these parts of the proof to sum and inductive types.

(Sum) Given σ_{1}, σ_{2} ∈ Ty(X) we define

[[σ_{1} + σ_{2}]](P) = {in_{j} t | j ∈ {1, 2} ∧ t ∈ [[σ_{j}]](P)}^{∗}

We define U_{i}^{σ_{1}+σ_{2}} inductively by the following rules (j ∈ {1, 2})

u U_{i}^{σ_{j}} t ; \overline{(in_{j})} ; u U_{i}^{σ_{1}+σ_{2}} in_{j} t t ∈ SN t ⊳_{whd} t′ u U_{i}^{σ_{1}+σ_{2}} t′

\overline{(clos^{+})}
u U_{i}^{σ_{1}+σ_{2}} t

Proposition 4. The interpretation [[σ_{1} + σ_{2}]] of the disjoint union is monotone and set based.

Proof.

(sb1) By induction on t ∈ [[σ_{1} + σ_{2}]](P):

(emb) t ≡ in_{j} s and s ∈ [[σ_{j}]](P). Since u U_{i}^{σ_{1}+σ_{2}} t must have been derived

from u U_{i}^{σ_{j}} s, we may apply the ind.hyp. to conclude u ∈ P_{i}.

(sat1),(sat2) As before for ×. (sb2) By induction on t ∈ [[σ_{1} + σ_{2}]](SN):

(emb) t ≡ in_{j} s and s ∈ [[σ_{j}]](SN). By ind.hyp. we have s ∈ [[σ_{j}]](U^{σ_{j}}(s)). Since U_{i}^{σ_{j}}(s) ⊆ U_{i}^{σ_{1}+σ_{2}}(in_{j} s) we can show s ∈ [[σ_{j}]](U^{σ_{1}+σ_{2}}(in_{j} s)) using

(mon) and hence t ∈ [[σ_{1} + σ_{2}]](U^{σ_{1}+σ_{2}}(t)).

(sat1),(sat2) As before for ×. ⊓ ⊔

(Mu) Given σ ∈ Ty(X, X) where n = |X| we define [[μX.σ]](P) inductively by (sat1), (sat2) and:

t ∈ [[σ]](P , SN^{μX.σ}) ∀u. u U_{n+1}^{σ} t ⟹ u ∈ [[μX.σ]](P)
\overline{(cons)}
c t ∈ [[μX.σ]](P)

We could not have used the saturation operator ^{∗} here instead of (sat1) and (sat2), since saturation and (cons) may have to be interleaved.

Note that [[μX.σ]] appears only strictly positively in the premises! By Prop. 1 (cons) is equivalent to the rule (cons’) given on page 9. We could not have used cons’ for the definition because [[μX.σ]] appears non-positively as an argument to [[σ]].

We also define U_{i}^{μX.σ} inductively:

1 ≤ i ≤ n u U_{i}^{σ} t ; \overline{(non-rec)} ; u U_{i}^{μX.σ} c t  u U_{i}^{μX.σ} t′ t′ U_{n+1}^{σ} t ; \overline{(rec)} ; u U_{i}^{μX.σ} c t

t ∈ SN t ⊳_{whd} t′ u U_{i}^{μX.σ} t′
\overline{(clos^{μ})}
u U_{i}^{μX.σ} t

Proposition 5. The interpretation [[μX.σ]] of inductive types is monotone and set based.

Proof. We omit (mon) since this follows from the fact that least fixpoints preserve monotonicity:

(sb1) We define a family of relations R by

u R_{i} t ⟺ (t ∈ [[μX.σ]](P) ⟹ u ∈ P_{i})

and show that R_{i} is closed under the rules defining U_{i}^{μX.σ}

(non-rec) Given u U_{i}^{σ} t and c t ∈ [[μX.σ]](P) we show u ∈ P_{i}. Since from the second assumption we can infer t ∈ [[σ]](P , [[μX.σ]](P)), our goal follows by (sb1) for σ, using the first assumption.

(rec) As before we have t ∈ [[σ]](P , [[μX.σ]](P)). Hence, using (sb1) for σ, the premise t′ U_{n+1}^{σ} t implies t′ ∈ [[μX.σ]](P). Now we use the ind.hyp.

u R_{i} t′ to conclude u ∈ P_{i}.

(clos^{μ}) Assuming t ∈ SN and t ⊳_{whd} t′ we exploit (sat2) for [[μX.σ]](P).

(sb2) We show that the set

Q = {t | t ∈ [[μX.σ]](U^{μX.σ}(t))}

is closed under the rules defining [[μX.σ]](SN^{τ}).

(cons) We assume

t ∈ [[σ]](SN^{τ} , Q)  (2)

which by using (sb2) for σ (and Q ⊆ SN) entails

t ∈ [[σ]](U^{σ}(t))  (3)

Using (cons’), to show that c t ∈ Q it suffices to show

t ∈ [[σ]](U^{μX.σ}(c t), [[μX.σ]](U^{μX.σ}(c t)))

We derive this from 3 using (mon), which leaves us two subgoals

1. For 1 ≤ i ≤ n prove that U_{i}^{σ}(t) ⊆ U_{i}^{μX.σ}(c t), which is an immediate consequence from (non-rec).

2. To show U_{n+1}^{σ}(t) ⊆ [[μX.σ]](U^{μX.σ}(c t)) assume

t′ U_{n+1}^{σ} t  (4)

Under this assumption we have that U_{i}^{μX.σ}(t′) ⊆ U_{i}^{μX.σ}(c t) by (rec). Using (sb1) for σ on 2 and 4 we have that t′ ∈ Q, i.e.,

t′ ∈ [[μX.σ]](U^{μX.σ}(t′))

and hence using (mon) t′ ∈ [[μX.σ]](U^{μX.σ}(c t)). (sat1),(sat2) As for ×. ⊓ ⊔

Having defined the interpretation for all types we show that the interpretation is compatible with substitution:

Proposition 6. Given τ ∈ Ty(X) and σ_{i} ∈ Ty for 1 ≤ i ≤ |X| we have

[[τ]]([[σ]]) = [[τ(σ)]]

Proof. Straightforward induction on τ ∈ Ty(X). ⊓ ⊔

5 Strong Normalisation

We have to show that all constructions are sound wrt. our semantics. The verification for simple types is standard (see [Alt93]) and summarized by the following proposition:

Proposition 7. Given σ, τ ∈ Ty the following implications hold

t ∈ [[σ → τ]]  u ∈ [[σ]] ; \overline{(sem-app)} ; tu ∈ [[τ]]  ∀u ∈ [[σ]].t[x := u] ∈ [[τ]] ; \overline{(sem-lam)} ; λx.t ∈ [[σ → τ]]

The difficult case is (sem-lam), since ⇒ is defined elimination based. In contrast, the semantics for all other type constructors introduced so far is constructor based, hence the soundness of constructors is trivial:

Proposition 8.

unit ∈ [[1]]
pair^{σ_{1},σ_{2}} ∈ [[σ_{1} → σ_{2} → (σ_{1} × σ_{2})]]
in_{i}^{σ_{1},σ_{2}} ∈ [[σ_{i} → (σ_{1} + σ_{2})]]  i ∈ {1, 2}
c^{X.τ} ∈ [[τ(μX.τ) → μX.τ]]

To show the soundness of eliminators we have to exploit the saturatedness. We postpone the case for It since its soundness has to be shown mutually with the soundness of strength.

Proposition 9.

π_{i}^{σ_{1},σ_{2}} ∈ [[(σ_{1} × σ_{2}) → σ_{i}]]  i ∈ {1, 2}
case_{0}^{σ} ∈ [[0 → σ]]
case^{σ_{1},σ_{2},ρ} ∈ [[(σ_{1} → ρ) → (σ_{2} → ρ) → (σ_{1} + σ_{2}) → ρ]]

Proof. We show soundness for the binary case to illustrate the idea: Given t_{i} ∈ [[σ_{i} → ρ]] and

u ∈ [[σ_{1} + σ_{2}]]  (5)

we prove t ≡ case t_{1}t_{2}u ∈ [[ρ]] by induction over the rules used to derive (5):

(sat1) If u ∈ Void then case t_{1}t_{2}u ∈ Void ⊆ [[ρ]], using (sat1) for ρ. (sat2) Given u ∈ SN, u ⊳_{whd} u′ with u′ ∈ [[σ_{1} + σ_{2}]]. Now by ind.hyp. we have

that case t_{1}t_{2}u′ ∈ [[ρ]] and we observe that t⊳_{whd} case t_{1}t_{2}u′. Using Lemma 1 we can show t ∈ SN and hence by (sat2) t ∈ [[ρ]].

(emb) u ≡ in_{i} u′ with u′ ∈ [[σ_{i}]]. Using Lemma 1 we derive that t ∈ SN. We have t ⊳_{whd} t_{i}u′ and from the premises we know t_{i}u′ ∈ [[ρ]]. Hence by (sat2) t ∈ [[ρ]]. ⊓ ⊔

We are now ready to establish the soundness of It and strength:

Proposition 10. Given ρ ∈ Ty(X), let n = |X|:

1. Assume σ_{i}, τ_{i} ∈ Ty, P_{i} ∈ SAT^{σ_{i}}, Q_{i} ∈ SAT^{τ_{i}} and f_{i} ∈ P_{i} ⇒ Q_{i} for 1 ≤ i ≤ n,

we have that

ρ(f) ∈ [[ρ]](P) ⇒ [[ρ]](Q)

2. If n > 1 assume τ_{i} ∈ Ty and P_{i} ∈ SAT^{τ_{i}} for 1 ≤ i < n. Let σ ∈ Ty and Q ∈ SAT^{σ}, it holds that

It^{X.ρ(τ ,X),σ} ∈ ([[ρ]](P , Q) ⇒ Q) ⇒ [[μX.ρ]](P) ⇒ Q

Proof. We show both properties by mutual induction on ρ ∈ Ty(X):

1. For all cases but (Mu) the property follows from the ind.hyp. 1. and Prop. 7, 8 and 9. For (Mu) we also have to use the 2nd part of the ind.hyp.

2. Assume f ∈ [[ρ]](P , Q) ⇒ Q we define

S = {t | It ft ∈ Q}

Note that It f ∈ S ⇒ Q by definition. We show that S is closed under the rules defining [[μX.ρ]]: (sat1) If t ∈ Void then It ft ∈ Void ⊆ Q using (sat1) for Q. (sat2) We have t ∈ SN, t ⊳_{whd} t′ and t′ ∈ S, i.e., It ft′ ∈ Q. From these

assumptions we infer It ft⊳_{whd} It ft′. Using Lemma 1 we can show It ft ∈ SN and hence, exploiting the saturatedness of Q, by (sat2) It ft ∈ Q, that is t ∈ S. As a byproduct we have shown S ∈ SAT.

(cons) For this rule from the assumption t ∈ [[ρ]](P , S) we have to show c t ∈ S, or, by definition of S, It f(c t) ∈ Q. Using the first part of the ind.hyp. and the saturatedness of S shown above, we establish^{6}

ρ(τ , It f) ∈ [[ρ]](P , S) ⇒ [[ρ]](P , Q)

Now using our assumptions we can further establish

f(ρ(It f) t) ∈ Q

We observe that It f(c t) ⊳_{whd} f(ρ(It f) t) and using Lemma 1 we can show It f(c t) ∈ SN. Hence by (sat2) It f(c t) ∈ Q.

By minimality of [[μX.ρ]] we have that [[μX.ρ]](P) ⊆ S and hence

It f ∈ [[μX.ρ]](P) ⇒ Q
⊓ ⊔

Proposition 11 (Soundness). Given Γ = x_{1} : σ_{1}, …, x_{n} : σ_{n} and u_{i} ∈ [[σ_{i}]] for 1 ≤ i ≤ n it follows that

Γ ⊢ t : τ ⟹ t[x := u] ∈ [[τ]]

Proof. By induction over the derivation of Γ ⊢ t : τ using Prop. 7–10. ⊓ ⊔

Theorem 1 is now a simple corollary:

Proof. Given Γ ⊢ t : τ by (sat1) we know x_{i} ∈ [[σ_{n}]] and hence by Prop. 11 t[x = x] ∈ [[τ]] ⊆ SN^{τ}. ⊓ ⊔

6 ρ(It f) is an abbreviation of ρ(λx^{τ}.x, It f), cf. the definition of strength in Sect. 2.

6 Coinductive Types

We shall sketch in this section how to extend our construction to coinductive types, i.e., introduce a type constructor ν to introduce terminal coalgebras. We will use greatest fixpoints of strictly positive operators.

6.1 Extending the Calculus

The calculus λ^{μν} is given by the following extensions of λ^{μ}:

Type constructor: ρ ∈ Ty(X, Y) ; \overline{(Nu)} ; νY.ρ ∈ Ty(X)

Constants:  d^{X.ρ} : (νX.ρ) → ρ(νX.ρ)
Co^{X.ρ,σ} : (σ → ρ(σ)) → σ → νX.ρ
Strength:  (νX.ρ)(f) = Co^{X.ρ(τ ,X),να}(λx^{να}. ρ(f, λy^{να}.y)(d^{α} x))

where α stands for X.ρ(σ, X)

β axiom:  d(Co^{X.ρ,σ} ft) ⊳ ρ(Co f)(ft)
Evaluation context: E[X] ::= ⋯ | dX

We interpret ⊳_{whd} and Void wrt. to the extended definition of E[X]. We note that Lemma 1 remains true under this extension and we now understand Theorem 1 wrt. the extended calculus.

6.2 Extending the Interpretation

Given ρ ∈ Ty(X, X) where n = |X| we define [[νX.ρ]](P) (predicatively) as the greatest fixpoint of the following rules:

t ∈ [[νX.ρ]](P)
\overline{(destr1)}
dt ∈ [[ρ]](P , SN^{νX.ρ})

t ∈ [[νX.ρ]](P) u U_{n+1}^{ρ} dt ; \overline{(destr2)} ; u ∈ [[νX.ρ]](P)

Note that, dually to the inductive case, the rules are supposed to match the (co-ind) scheme, i.e., we define the greatest fixpoint of the operator

Φ(Q) = {t | dt ∈ [[ρ]](P , SN^{νX.ρ}) ∧ ∀u.(u U_{n+1}^{ρ} dt) → u ∈ Q}

Using Prop. 1 we can show that (destr1) and (destr2) are equivalent to

t ∈ [[νX.ρ]](P)
\overline{(destr′)}
dt ∈ [[ρ]](P , [[νX.ρ]](P))

We define U_{i}^{νX.ρ} inductively (!), i.e., as a least not a greatest fixpoint:

1 ≤ i ≤ n u U_{i}^{ρ} dt ; \overline{(non-rec)} ; u U_{i}^{μX.ρ} t  {u U_{i}^{νX.ρ} t′ t′ U_{n+1}^{ρ} dt \atop u U_{i}^{νX.ρ} t}(rec)

Note that different to the μ types we have not explicitely closed the interpretation under (sat1) and (sat2). However, we can show:

Proposition 12. The interpretation [[νX.ρ]] of coinductive types is saturated.

Proof. We show that

[[νX.ρ]](P)^{∗} ⊆ [[νX.ρ]](P)

by verifying that [[νX.ρ]](P)^{∗} is closed under (destr’) (and hence equivalently under (destr1) and (destr2)) by induction over t ∈ [[νX.ρ]](P)^{∗}:

(sat1) If t ∈ Void then dt ∈ Void ⊆ [[ρ]](P , [[νX.ρ]](P)^{∗}) by (sat1) for ρ. (sat2) Given t ∈ SN, t ⊳_{whd} t′, by ind.hyp we assume that

dt′ ∈ [[ρ]](P , [[νX.ρ]](P)^{∗}).

Since dt ∈ SN by Lemma 1 and dt ⊳_{whd} dt′ we can use (sat2) for ρ. (emb) Given t ∈ [[νX.ρ]](P) we know that

dt ∈[[ρ]](P , [[νX.ρ]](P))
⊆[[ρ]](P , [[νX.ρ]](P)^{∗})

using (mon) and [[νX.ρ]](P) ⊆ [[νX.ρ]](P)^{∗}

To show (sb2) we need an auxiliary relation ≤ ⊆ Tm^{(νX.ρ)(τ)} × Tm^{(νX.ρ)(τ)} which is inductively defined by

t ∈ [[νX.ρ]](SN^{τ}) ; \overline{(refl)} ; t ≤ t  t′′ ≤ t′  t′ U_{n+1}^{ρ} dt ; \overline{(trans)} ; t′′ ≤ t

Intuitively, ≤ is a generalization of the prefix relation on streams.

Lemma 3. {t′ ≤ t \atop t′ ∈ [[νX.ρ]](U^{νX.ρ}(t))}

Proof. Given a fixed t ∈ [[νX.ρ]](SN^{τ}) we show that the set ≤(t) is closed under (destr’) for [[νX.ρ]](U^{νX.ρ}(t)) and hence by (co-elim)^{7} the rule holds.

We have to show s ≤ t (i.e., s ∈ ≤(t)) implies

ds ∈ [[ρ]](U^{νX.ρ}(t), ≤(t))

We show this by induction over s ≤ t:

(refl) We have to show

dt ∈ [[ρ]](U^{νX.ρ}(t), ≤(t))

By (sb2) for ρ we know dt ∈ [[ρ]](U^{ρ}(dt)). For 1 ≤ i ≤ n (non-rec) implies that U_{i}^{ρ}(dt) ⊆ U_{i}^{νX.ρ}(t), and using (trans) and (refl) it is easy to see that U_{n+1}^{ρ}(dt) ⊆ ≤(t). Hence by (mon) for [[ρ]] we have dt ∈ [[ρ]](U^{νX.ρ}(t), ≤(t)).

7 See introduction, page 3.

(trans) Given

t′ U_{n+1}^{ρ} dt  (6)

and as ind.hyp. dt′′ ∈ [[ρ]](U^{νX.ρ}(t′), ≤(t′)) we have to show

dt′′ ∈ [[ρ]](U^{νX.ρ}(t), ≤(t))

Using (rec) and (6) we know that U_{i}^{νX.ρ}(t′) ⊆ U_{i}^{νX.ρ}(t). Using (trans) and (6) we know ≤(t′) ⊆ ≤(t) and hence by applying (mon) for [[ρ]] for the ind.hyp. we have dt′′ ∈ [[ρ]](U^{νX.ρ}(t), ≤(t)).

Proposition 13. [[νX.ρ]] is monotone and set based.

Proof.

(sb1) We show that

u R_{i} t : ⟺ t ∈ [[νX.ρ]](P) ⟹ u ∈ P_{i}

is closed under the rules defining U_{i}^{νX.ρ}

(non-rec) We have dt ∈ [[ρ]](P , [[μX.ρ]](P)) and hence by (sb1) for ρ the

premise u U_{i}^{ρ} t implies u ∈ P_{i}. (rec) As before we have dt ∈ [[ρ]](P , [[νX.ρ]](P)). Hence, using (sb1) for ρ, the first premise t′ U_{n+1}^{ρ} dt implies t′ ∈ [[νX.ρ]](P). Now we use the

second premise t′ R_{i} u to conclude u ∈ P_{i}.

(sb2) Follows from Lemma 3 for t ≤ t.

6.3 Extending Soundness

The soundness of d follows directly from the definition of ν:

Proposition 14.

d^{X.ρ} ∈ [[(νX.ρ) → ρ(νX.ρ)]]

We have to extend Prop. 10 by a case for Co:

Proposition 15. Prop. 10 extended by:

3. If n > 1 assume τ_{i} ∈ Ty and P_{i} ∈ SAT^{τ_{i}} for 1 ≤ i < n. Let σ ∈ Ty and Q ∈ SAT^{σ}; it holds that

Co^{X.ρ(τ ,X),σ} ∈ (Q ⇒ [[ρ]](P , Q)) ⇒ Q ⇒ [[νX.ρ]](P)

Proof. We have to extend 1. by the case for ν but the reasoning is the same as for μ. Let us consider 3.: Assuming f ∈ Q ⇒ [[ρ]](P , Q) we show that

S = {Co^{X.ρ(τ ,X)} ft | t ∈ Q}

is closed under (destr’).

This entails S ⊆ [[νX.ρ]](P), since [[νX.ρ]](P) is defined as the greatest fixpoint of the rule (destr’), and thus our claim follows.

The definition of S implies that Co f ∈ Q ⇒ S (writing Co for Co^{X.ρ(τ ,X)}). Assuming t ∈ Q we have to show that d(Co ft) ∈ [[ρ]](P , Q). We use (sat2) since d(Co ft) ⊳_{whd} ρ(Co f)(ft). By ind.hyp. we know that ρ(Co f) ∈ ρ(P , Q) ⇒ ρ(P , S), which suffices to show that the reduct is in ρ(P , S). We finish by observing that an application of Lemma 1 shows that d(Co ft) ∈ SN. ⊓ ⊔

Prop. 11 can be extended to the new cases using Prop. 14 and 15 and hence Theorem 1 can be extended to λ^{μν}.

7 Conclusions and Further Work

It is straightforward to extend the construction presented here to primitive recursion

Re^{X.τ,σ} : (τ((μX.τ) × σ) → σ) → (μX.τ) → σ

and corecursion

CR^{X.τ,σ} : (σ → τ((νX.τ) + σ)) → σ → νX.τ,

which we have to omit here due to lack of space.

It may be argued that a syntactic approach to strong normalisation a la Benl [Ben98] may also be extended to a system as general as ours. However, we believe that the semantic approach using set based operators will allow further generalizations such as a functorial calculus (e.g., see [JBM98]) and heterogenous datatypes as discussed in [AR99].

References

[AA99] Andreas Abel and Thorsten Altenkirch. A predicative analysis of structural recursion. Submitted to the Journal of Functional Programming, December 1999.

[Abe99] Andreas Abel. A semantic analysis of structural recursion. Master’s thesis, Ludwig-Maximilians-University Munich, 1999. http://www.informatik.unimuenchen.de/˜ abel/publications/.

[Acz97] Peter Aczel. Notes on constructive set theory. Available from the WWW, 1997.

[Alt93] Thorsten Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, November 1993.

[Alt98] Thorsten Altenkirch. Logical relations and inductive/coinductive types. 1998.

[AR99] Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Computer Science Logic 99, 1999.

[Ben98] Holger Benl. Starke Normalisierung für die Heyting-Arithmetik mit induktiven Typen. Master’s thesis, Ludwig-Maximillians-Universität, München, 1998.

[BJO99] Frédéric Blanqui, Jean-Pierre Jouannaud, and Mitsuhiro Okada. Inductive data type systems. To appear in Theoretical Computer Science, 1999.

[Buc81] Wilfried Buchholz. The ω_{μ+1}-rule. In Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, volume 897 of Lecture Notes in Mathematics, pages 188–233. 1981.

[CM89] Thierry Coquand and Christine Mohring. Inductively defined types. In P. Löf and G. Mints, editors, LNCS 389, volume 417 of Lecture Notes in Computer Science, pages 50–66. Springer-Verlag, 1989.

[Coq94] Infinite objects in type theory. LNCS, pages 62–78, Berlin, 1994. Springer-Verlag.

[Dyb91] Peter Dybjer. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. Technical Report Report 62, Programming Methodology Group, Chalmers University, 1991.

[Geu92] Herman Geuvers. Inductive and coinductive types with iteration and recursion. In Workshop on Types for Proofs and Programs, Båstad, pages 193–217, 1992.

[Gir72] J. Y. Girard. Interprétation fonctionelle et élimination des coupures dans l’arithétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972.

[GLT89] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.

[Hag87] Tatsuya Hagino. A Categorical Programming Language. PhD thesis, University of Edinburgh, September 1987.

[JBM98] C.B. Jay, G. Bellè, and E. Moggi. Functorial ML. Journal of Functional Programming, 8(6):573–619, 1998.

[JO97] J. P. Jouannaud and M. Okada. Abstract data type systems. Theoretical Computer Science, 173, 1997.

[Loa97] Ralph Loader. Equational theories for inductive types. Annals of Pure and Applied Logic, 84:175–217, 1997.

[Luo90] Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990.

[Mar84] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

[Mat98] Ralph Matthes. Extensions of System F by Iteration And Primitive Recursion on Monotone Inductive Types. PhD thesis, University of Munich, 1998.

[Men88] Nax P. Mendler. Inductive Definition in Type Theory. PhD thesis, Cornell University, 1988.

[Rey84] John C. Reynolds. Polymorphism is not set-theoretic. In Gilles Kahn, David B. MacQueen, and Gordon D. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 145–156, Berlin, 1984. Springer-Verlag.

[Tai67] W. W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2):198–212, June 1967.