INSTITUT FÜR INFORMATIK

DER LUDWIG-MAXIMILIANS-UNIVERSITÄT MÜNCHEN

Diplomarbeit

Eine semantische Analyse struktureller Rekursion

Bearbeiter: Andreas Abel Aufgabensteller: Prof. Dr. Peter Clote, Ph.D. Betreuer: Dr. Thorsten Altenkirch, Ph.D.

INSTITUT FÜR INFORMATIK

DER LUDWIG-MAXIMILIANS-UNIVERSITÄT MÜNCHEN

Diplomarbeit

Eine semantische Analyse struktureller Rekursion

Bearbeiter: Andreas Abel Aufgabensteller: Prof. Dr. Peter Clote, Ph.D. Betreuer: Dr. Thorsten Altenkirch, Ph.D. Abgabetermin: 26. Februar 1999 Hiermit versichere ich, dass ich die vorliegende Diplomarbeit selbständig verfasst und keine anderen als die angegebenen Quellen und Hilfsmittel verwendet habe.

München, den 26. Februar 1999

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

(Unterschrift des Kandidaten)

Danksagung

An erster Stelle danke ich Jesus Christus, der das Universum und den menschlichen Geist geformt hat und damit auch die Mathematik und Technik, die wir schaffen und zu unserem Wohl gebrauchen können. Auch hat er an einer kritischen Stelle im Laufe dieser Arbeit mein Gebet gehört und mir geholfen.

Sodann danke ich Thorsten Altenkirch, der in unkomplizierter Weise meine Arbeit betreut und sich viel Zeit für meine Fragen genommen hat. Ebenso Ralph Matthes, der die Arbeit gründlich gelesen hat und mich an seinem typentheoretischen Erfahrungsschatz teilhaben ließ, sofern es sein mit Doktorarbeit und Rigorosum gefüllter Terminkalender erlaubte. Und Rolf Backofen, der mir in einigen technischen Fragen geholfen hat.

Meinen Eltern danke ich für die wohlwollende Finanzierung meines Studiums und dafür, dass sie immer für mich da sind.

Und schließlich danke ich Julia, dass sie in meinem Leben aufgetaucht ist (obwohl sie mich eigentlich von meiner Arbeit nur abgelenkt hat).

A Semantic Analysis of Structural Recursion

Abstract

We consider a type theoretic language with lambda abstraction, disjoint unions, pairs and recursive terms and show that all structurally recursive functions terminate, i.e. functions, that contain recursive calls only with a structurally smaller argument. To this end, we define a semantics [[σ]] over all types and show that it is wellfounded w.r.t. the structural ordering on the values (normal forms of our terms). Then by wellfounded induction we can easily infer termination of a recursive function at all inputs in [[σ]] from termination at all smaller inputs. Later we extend our solution from strictly positive types to positive types and mutual recursive functions.

Contents

1 Introduction 7

2 The language 9 2.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

2.3.1 Natural numbers . . . . . . . . . . . . . . . . . . . . . 13 2.3.2 Ordinal numbers . . . . . . . . . . . . . . . . . . . . . 14

3 Operational semantics 15 3.1 Values and closures . . . . . . . . . . . . . . . . . . . . . . . . 15 3.2 Operational semantics . . . . . . . . . . . . . . . . . . . . . . 16 3.3 Correspondence of values and closures . . . . . . . . . . . . . 18 3.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

3.4.1 Numerals . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.4.2 Soundness of addition . . . . . . . . . . . . . . . . . . 21

4 Semantic values 23 4.1 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

5 Wellfoundedness of the structural ordering 29 5.1 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 6 Soundness of the termination criterium 35

7 Extensions 39 7.1 Positive types . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 7.2 Functions with multiple parameters . . . . . . . . . . . . . . . 44 7.3 Mutual recursion . . . . . . . . . . . . . . . . . . . . . . . . . 46

8 Conclusion 48

1 Introduction

By the seventh day God had finished the work he had been doing; so on the seventh day he rested from all his work. And God blessed the seventh day and made it holy, because on it he rested from all the work of creating that he had done.

The Bible, NIV, Genesis 2:2,3

In the research field of program verification termination is an important aspect. In general the negative solution of Hilbert’s halting problem showed that termination is undecidable. Nevertheless much work has been done on the question of termination, especially in the field of term rewriting systems [Der87, Ste95] – where several termination criteria have been developed – and more recently in the field of functional programming languages, e.g. [BG96, Gie97], to which our work contributes. We prove the following termination criterium:

All structurally recursive functions terminate.

We define a structurally recursive function as

a function f that terminates for all arguments v, if it does so under the condition that it terminates for all structurally smaller arguments v′.

Our termination criterium only (and then trivially) holds if the domain of f is wellfounded w.r.t. the structural ordering <, i.e. if there are no infinite descending chains v > v′ > . . ..

Functional programming languages like SML [Pau91] and Haskell [HPF97] and implementations of type theory like ALF [AGNvS94] and LEGO [LP92] allow definition of recursive functions/terms by pattern matching [Coq92]. A function is structurally recursive if

1. the pattern is total (i.e. no possible case is omitted) and

2. recursive calls use only structurally smaller arguments.

MuTTI (Munich Type Theory Implementation) is a functional language with dependent types. Pattern matching is done via case analysis of only one expression (no combined patterns), which rids us of a complicated totality check for condition 1.

For the simply typed sublanguage of MuTTI named foetus, we have developed a program which checks condition 2., where we obtain structurally smaller arguments only by case analysis, projection and function application. This restriction makes being structurally smaller a syntactic property that can easily be checked by foetus. For mutually recursive functions with multiple arguments, foetus constructs a call graph and tries to determine an permutation of the arguments with respect to which termination is verified using the lexicographic ordering (for detailed explanation see [Abe98]).

Our task now is to prove the soundness of our method, i.e. of our termination criterium. Therefore we consider a system with unit, sum, product, function and strictly positive recursive types that has the same expressivity as foetus, and we restrict to functions of one parameter without mutual recursion. After defining the types and terms of this system (section 2) we specify an operational semantics (section 3) and semantical values (section 4) on which we define a structural ordering. After having proven wellfoundedness of this ordering (section 5) we easily obtain the soundness of our termination criterium (section 6). We then extend our proof to systems with positive types (section 7.1), functions with multiple parameters (section 7.2) and mutual recursion (section 7.3) and we conclude by discussing further work (section 8).

A comment on our method for the reader familiar with normalization proofs. Our method of proving normalization for our system is a very intuitive one. Since we do not define a reduction relation as it is common for the lambda calculus in the literature, but treat it as a functional programming language with a fixed evaluation strategy, we neither have to consider terms of open types (i.e. types with free variables), nor show strong normalization, nor make use of sophisticated concepts like Girard’s candidates of reducibility or saturated sets [Gir72, Alt93]. Our proof is straight and simple.

2 The language

We need a language that is strong enough to form typical functional programs like functions on natural numbers, lists and user defined data types. On the other hand it has to be simple enough to enable reasoning about it.

2.1 Types

The type system we have chosen is constructed from the base type 1 (representing the set with one element), type variables X, Y, Z, … and the type constructors + (sum), × (product), → (function space) and Rec (recursive type). Within this system the set of natural numbers may be expressed as N := Rec X.1 + X and the set of lists over natural numbers as ListN := Rec X.1 + N × X. In the literature recursive types are often called μ-types.

To simplify the central proof of wellfoundedness (section 5) we restrict ourselves to strictly positive recursive types now. Later we will extend our system to positive recursive types (section 7.1).

Type variables. Assume a countably infinite set of type variables TyVars = {X, Y, Z, …}. A type variable X appears strictly positive within a type τ iff it appears never on the left side of some → (see rule (Arr) below).

Notation. For convenience we mix list, tuple and set notation: By X⃗ we mean a (possibly empty) list of type variables (X⃗ ⊂ TyVars) without duplicates (an ordered set) and by X⃗, X the appending of X to X⃗ assuming X ∉ X⃗.

Types. We inductively define the family of sets of types Ty(X⃗) indexed over a finite set of type variables X⃗ ⊂ TyVars appearing only strictly positive as follows:

(Unit) 1 ∈ Ty(∅)

(Var)

X⃗, X ⊂ TyVars
X ∈ Ty(X⃗, X)

(Weak)^{1} {σ ∈ Ty(X⃗) X ∉ X⃗ \atop σ ∈ Ty(X⃗, X)}

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

(Arr) {σ ∈ Ty(∅) τ ∈ Ty(X⃗) \atop σ → τ ∈ Ty(X⃗)}  (Rec) {σ ∈ Ty(X⃗, X) \atop Rec X.σ ∈ Ty(X⃗)}

We can restrict the free type variables to strictly positive ones because unlike Girards System F [Gir72], we have no polymorphic types and therefore need type variables only to construct recursive types.

Notation. In the following we write σ(X⃗) to express σ ∈ Ty(X⃗). Then σ and σ(X⃗) are synonyms. We also abbreviate the set of closed types Ty(∅) to Ty.

Renaming convention for types. Rec binds a type variable X in a type σ(X⃗, X), and we may replace all appearances of X in Rec X.σ(X⃗, X) by any new variable Y ∉ X⃗ without altering the actually denoted type. Thus we do not distinguish between Rec X.σ(X⃗, X) and Rec Y.σ(X⃗, Y).

Our style of variable introduction and binding (see rules (Var), (Weak) and (Rec) below) is very near to an implementation of variables by deBruijnindices (see [dB72]).^{2} This saves us a lot of work in defining substitution, but one must become familiar with the notation, e.g. that (Weak) is an explicit type (and later term) constructor. As compromise we have kept the variable names for better readability and thus formally need a renaming convention.

Substitution. Now we can define simultaneous substitution on types in the usual way. Provided a type σ(X⃗) with a list of free variables X⃗ and an equally long list of types ρ⃗ ∈ Ty(Y⃗) we define σ[X⃗ := ρ⃗] ∈ Ty(Y⃗) by recursion over σ as follows:

1Unlike all other type forming rules (Weak) does not alter the term describing the type in our representation. We have left out a constructor like WkX.σ for better readability.

Our implementation in LEGO, however, uses this explicit constructor.

2That means that one enumerates the variables and obtains rules like (Var) n ∈ Ty(n+ 1), (Weak) Ty(n) ⊂ Ty(n + 1) and (Rec) σ ∈ Ty(n + 1) ⇒ Rec n+1. σ ∈ Ty(n).

(Unit) 1[] := 1

(Var) X[X⃗ := ρ⃗, X := ρ] := ρ

(Weak)^{3} σ(X⃗, X)[X⃗, X := ρ⃗, ρ] := σ(X⃗)[X⃗ := ρ⃗]

(Sum) (σ(X⃗) + τ(X⃗)) [X⃗ := ρ⃗] := σ[X⃗ := ρ⃗] + τ[X⃗ := ρ⃗]

(Prod) (σ(X⃗) × τ(X⃗)) [X⃗ := ρ⃗] := σ[X⃗ := ρ⃗] × τ[X⃗ := ρ⃗]

(Arr) (σ(∅) → τ(X⃗)) [X⃗ := ρ⃗] := σ → (τ[X⃗ := ρ⃗])

(Rec) We can assume Z ∉ Y⃗ by the renaming convention, hence we can weaken all types ρ_{i}(Y⃗) by Z: (Rec Z.σ(X⃗, Z)) [X⃗ :=

ρ⃗] := Rec Z. (σ[X⃗ := ρ⃗(Y⃗ , Z), Z := Z])

Notation. We write σ(ρ⃗) for σ(X⃗)[X⃗ := ρ⃗] and define substitution of a single variable Y as σ(X⃗, Y, Z⃗)[Y := ρ] := σ[X⃗ := X⃗, Y := ρ, Z⃗ := Z⃗], which we further abbreviate to σ(X⃗, ρ, Z⃗).

2.2 Terms

Now we define the terms inhabiting the above defined types. The definitions are very similar to a typed lambda calculus enriched by sums and products, except for the recursive terms we allow. We have decided to type terms over contexts to easily define closures afterwards.

Term variables and contexts. Assume a countably infinite set of term variables TmVars = {g, x, y, z, …}. Provided the closed types σ_{1}, … σ_{n} we can form a context Γ = x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} ∈ Cxt as a list of pairwise distinct term variables together with their types. We write x^{σ} to express the variable is of type σ in a given context.

3Note that in the weakened type σ the newly introduced variable X does not appear.

Therefore the right side is well defined.

Terms. We define the set of terms Tm^{σ}[Γ] of a closed type σ over context Γ inductively as follows:

(unit) () ∈ Tm^{1}[]

(var)

Γ ∈ Cxt x ∉ Γ
x ∈ Tm^{σ}[Γ, x^{σ}]

(weak)

{t ∈ Tm^{σ}[Γ] x ∉ Γ \atop t ∈ Tm^{σ}[Γ, x^{τ}]}

(inl)

t ∈ Tm^{σ}[Γ] τ ∈ Ty
inl(t) ∈ Tm^{σ+τ}[Γ]

(inr)

t ∈ Tm^{τ}[Γ] σ ∈ Ty
inr(t) ∈ Tm^{σ+τ}[Γ]

(case)

t ∈ Tm^{σ+τ}[Γ] l ∈ Tm^{ρ}[Γ, x^{σ}] r ∈ Tm^{ρ}[Γ, y^{τ}]
case(t, x^{σ}.l, y^{τ}.r) ∈ Tm^{ρ}[Γ]

(pair)

s ∈ Tm^{σ}[Γ] t ∈ Tm^{τ}[Γ]
(s, t) ∈ Tm^{σ×τ}[Γ]

(fst) p ∈ Tm^{σ×τ}[Γ]

fst(p) ∈ Tm^{σ}[Γ]

(snd) p ∈ Tm^{σ×τ}[Γ]

snd(p) ∈ Tm^{τ}[Γ]

(lam)

{t ∈ Tm^{τ}[Γ, x^{σ}] \atop λx^{σ}.t ∈ Tm^{σ→τ}[Γ]}

(rec)

t ∈ Tm^{σ→τ}[Γ, g^{σ→τ}]
rec g^{σ→τ}.t ∈ Tm^{σ→τ}[Γ]

(app)

t ∈ Tm^{σ→τ}[Γ] s ∈ Tm^{σ}[Γ]
t s ∈ Tm^{τ}[Γ]

(fold)

t ∈ Tm^{σ(Rec X.σ(X))}[Γ]
fold(t) ∈ Tm^{Rec X.σ(X)}[Γ]

(unfold)

t ∈ Tm^{Rec X.σ(X)}[Γ]

unfold(t) ∈ Tm^{σ(Rec X.σ(X))}[Γ]

There are two main kinds of term forming rules: Rules for introducing types (the constructors (unit), (inl), (inr), (pair), (lam), (rec) and (fold)) and rules for eliminating types (the destructors (case), (fst), (snd), (app) and (unfold)). The remaining rules (var) and (weak) only work on the context and therefore do not fit in these categories.

Renaming convention for terms. In these rules case binds the variable x in the term l and y in r, λ binds x in t and rec binds g in t. Like we have done with types we do not distinguish between terms that are equal except that the names of their bound variables differ.

Notation. Similar to the type notation σ(X⃗) we write t^{σ} to express that t is of type σ, t[Γ] that t is a term over context Γ and t^{σ}[Γ] to express both, i.e. t ∈ Tm^{σ}[Γ]. We define the set of closed terms Tm^{σ} of type σ as the set of terms over an empty context Tm^{σ}[].

2.3 Examples

To strengthen the reader’s understanding of our language we will present a few examples. By the way we see that we can embed Gödel’s T and Kleene’s O into our system. Identifiers for defined expressions of our language are printed in bold font.

2.3.1 Natural numbers

We define the natural numbers as the recursive type

Nat ≡ Rec X.1 + X

and zero and successor as

O ≡ fold(inl())
S(v) ≡ fold(inr(v))

Addition on Nat could be defined as the following function add ∈ Tm^{Nat→Nat→Nat}:

add ≡ rec add^{Nat→Nat→Nat}. λx^{Nat}. λy^{Nat}. case(unfold(x),
1. y,
x^{′Nat}. S(add x′ y))

We use as variable name for a variable of type 1, since its content will always be () and thus we never have to refer to it.

We even can define the recursor R^{σ} over natural numbers for result type σ, that is a constant in Gödel’s T:

R^{σ} ≡ rec R^{σ→(Nat→σ→σ)→Nat→σ}. λf_{O}^{σ}. λf_{S}^{Nat→σ→σ}. λn^{Nat}.

case(unfold(n), 1. f_{O}, n^{′Nat}. f_{S} n′ (R f_{O} f_{S} n′)

2 THE LANGUAGE 14 2.3.2 Ordinal numbers In our system we can define ordinal numbers as follows, where we represent limes numbers as functions from Nat to Ord:

Ord ≡ Rec X.(1 + X) + (Nat → X)

As above we can define zero, successor, limes and addition:

O ≡ fold(inl(inl()))
S(v) ≡ fold(inl(inr(v)))
Lim(f) ≡ fold(inr(f))

addOrd ≡ rec addOrd^{Ord→Ord→Ord}. λx^{Ord}. λy^{Ord}. case(unfold(x),

n^{1+Ord}. case(n,
1. y,
x^{′Ord}. S(addOrd x′ y))
f^{Nat→Ord}. Lim(λz^{Nat}. addOrd (f z) y))

We will extend these examples in the next sections.

3 Operational semantics

We only assign a meaning to closed terms t ∈ Tm^{σ}: they evaluate to (syntactic) values of type σ. (We want to define semantic values as well, see section 4.) But during the process of evaluation defined by our operational semantics we will have to handle open terms, where their free variables are assigned values we store in an environment. Term and its corresponding environment form a closure which can be seen as completion of an open term.

3.1 Values and closures

In formulations of the lambda calculus in the literature (see for instance [Mat98] for an accurate formalization) often normal forms are defined as terms that cannot be reduced further.^{4} Since we do not want open terms as results of an evaluation, we follow a different approach: we define values from scratch and later show that they correspond to closed terms resp. closures (see section 3.3).

Values. We define Val^{σ} inductively as follows. Again we write v^{σ} to express v ∈ Val^{σ}. The set of environments Val(Γ) is defined simultaneously (see the definition below).

(vlam)

t ∈ Tm^{τ}[Γ, x^{σ}] e ∈ Val(Γ)
⟨λx^{σ}.t; e⟩ ∈ Val^{σ→τ}

(vunit)

() ∈ Val^{1}

(vrec)

t ∈ Tm^{σ→τ}[Γ, g^{σ→τ}] e ∈ Val(Γ)
⟨rec g^{σ→τ}.t; e⟩ ∈ Val^{σ→τ}

(vinl)

v ∈ Val^{σ} τ ∈ Ty
inl(v) ∈ Val^{σ+τ}

(vinr)

v ∈ Val^{τ} σ ∈ Ty
inr(v) ∈ Val^{σ+τ}

(vpair)

v ∈ Val^{σ} w ∈ Val^{τ}
(v, w) ∈ Val^{σ×τ}

(vfold)

v ∈ Val^{σ(Rec X.σ(X))}
fold(v) ∈ Val^{Rec X.σ(X)}

These rules correspond to the introduction rules for terms. Since values represent evaluated terms, we need only constructors, no destructors.

4Ralph Matthes first defines normal forms inductively and later proves that they are the irreducible terms.

Environments and Closures. We define the set of environments of the context Γ = x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} as

Val(Γ) := {x_{1} =v_{1}, …, x_{n} =v_{n} : v_{i} ∈ Val^{σ_{i}}}

We write e^{Γ} for an environment e ∈ Val(Γ) and “·” for the empty environment. The set of closures of type τ we define as

Cl^{τ} := {⟨t; e⟩ : Γ ∈ Cxt, t ∈ Tm^{τ}[Γ], e ∈ Val(Γ)}
∪ {f@u : f ∈ Val^{σ→τ}, u ∈ Val^{σ}}

Here @ is a syntactic function symbol Val^{σ→τ} × Val^{σ} → Cl^{τ}. Closures of the form f@u (value applied to values) are convenient to define the operational semantics without typecasting values back to terms, which in an implementation would be inefficient as well.

Renaming convention for closures. Since in a closure all variables of a term are bound, we consider two closures as equal that differ only in variable names.

3.2 Operational semantics

In the following we present a big step operational semantics “⇓” that defines how closures are evaluated to values. Our strategy is call-by-value (see rule (opapp)) and we do not evaluate under λ and rec (see rules (oplam) and (oprec). Furthermore it is deterministic, i.e. for every closure there is at most one computation tree.^{5}

Operational semantics. We inductively define a family of relations ⇓^{σ}⊆ Cl^{σ} × Val^{σ} indexed over Ty. As the type σ can be inferred from the type of the closure or the value, we generally leave it out. For reasons of readability we leave out type and context annotations wherever possible.

5For all closures except ⟨case(t, x.l, y.r); …⟩ there is only one computation rule. But also for closures with case analysis there will be only one computation tree, since ⟨t; …⟩ evaluates to either a left (inl) or a right (inr) injection of some value and thus only one of the rules (opcasel) or (opcaser) is applicable.

(opunit) ⟨(); ·⟩ ⇓ ()

(opvar) ⟨x; e, x = v⟩ ⇓ v  (opweak) {⟨t[Γ]; e⟩ ⇓ v \atop ⟨t[Γ, x]; e, x = w⟩ ⇓ v}

(opinl) {⟨t; e⟩ ⇓ v \atop ⟨inl(t); e⟩ ⇓ inl(v)}  (opinr) {⟨t; e⟩ ⇓ v \atop ⟨inr(t); e⟩ ⇓ inr(v)}

(opcasel) ⟨t^{σ+τ}[Γ]; e⟩ ⇓ inl(w^{σ}) ⟨l^{ρ}[Γ, x^{σ}]; e, x = w⟩ ⇓ v^{ρ}

⟨case(t, x.l, y.r); e⟩ ⇓ v

(opcaser) ⟨t^{σ+τ}[Γ]; e⟩ ⇓ inr(w^{τ}) ⟨r^{ρ}[Γ, y^{τ}]; e, x = w⟩ ⇓ v^{ρ}

⟨case(t, x.l, y.r); e⟩ ⇓ v

(oppair) {⟨s; e⟩ ⇓ v ⟨t; e⟩ ⇓ w \atop ⟨(s, t); e⟩ ⇓ (v, w)}

(opfst) {⟨p; e⟩ ⇓ (v, w) \atop ⟨fst(p); e⟩ ⇓ v}  (opsnd) {⟨p; e⟩ ⇓ (v, w) \atop ⟨snd(p); e⟩ ⇓ w}

(oplam) ⟨λx.t; e⟩ ⇓ ⟨λx.t; e⟩  (oprec) ⟨rec g.t; e⟩ ⇓ ⟨rec g.t; e⟩

(opapp) {⟨t; e⟩ ⇓ f ⟨s; e⟩ ⇓ u f@u ⇓ v \atop ⟨t s; e⟩ ⇓ v}

(opappvl) {⟨t; e, x = u⟩ ⇓ v \atop ⟨λx.t; e⟩@u ⇓ v}

(opappvr) {⟨t; e, g = rec g.t⟩ ⇓ f f@u ⇓ v \atop ⟨rec g.t; e⟩@u ⇓ v}

(opfold)

⟨t; e⟩ ⇓ v
⟨fold(t); e⟩ ⇓ fold(v)

(opunfold)

⟨t; e⟩ ⇓ fold(v)

⟨unfold(t); e⟩ ⇓ v

3.3 Correspondence of values and closures

For our operational semantics we want to show a consistency property: Values, converted back to closures, should evaluate to themselves. To prove this proposition we need some

Additional weakening rules. We specify two rules for terms that perform weakening by introduction of several variables at a time: By iterated application of (weak) we can weaken a term by a list of variables Δ:

(weakEnd)

t ∈ Tm^{σ}[Γ] Γ ∩ Δ = ∅
t ∈ Tm^{σ}[Γ, Δ]

We also need to be able to weaken a term by adding variables at the beginning of its context.

(weakBeg)

t ∈ Tm^{σ}[Γ] Γ ∩ Δ = ∅
t ∈ Tm^{σ}[Δ, Γ]

That rule we get by decomposing the term into its derivation tree, weakening the context at the leaves^{6} of this tree and then re-composing the term. In the same way we get evaluation rules for weakened closures:

(opweakEnd) {⟨t[Γ]; e^{Γ}⟩ ⇓ v \atop ⟨t[Γ, Δ]; e^{Γ}, d^{Δ}⟩ ⇓ v}

(opweakBeg) {⟨t[Γ]; e^{Γ}⟩ ⇓ v \atop ⟨t[Δ, Γ]; d^{Δ}, e^{Γ}⟩ ⇓ v}

Consistency. To prove that each value evaluates to itself, we must convert it back to its closure first. To this end, we define the canonical embedding

cl^{σ} : Val^{σ} ↪ Cl^{σ}

by recursion on values as follows:

6There are two kinds of leaves:

(var) Here we can weaken the context in the beginning, since we can introduce

a new variable with any context.

(unit) Since here the context is empty, we can insert the necessary weakening

step.

(vunit) cl() := ⟨(); ·⟩ (vlam) cl⟨λx.t; e⟩ := ⟨λx.t; e⟩ (vrec) cl⟨rec g.t; e⟩ := ⟨rec g.t; e⟩ (vinl) Let ⟨t; e⟩ := cl(v). Then cl(inl(v)) := ⟨inl(t); e⟩ (vinr) Let ⟨t; e⟩ := cl(v). Then cl(inr(v)) := ⟨inr(t); e⟩ (vpair) Let ⟨s[Δ]; d⟩ := cl(v), ⟨t[Γ]; e⟩ := cl(w). By the renaming

convention for closures we can assume that Γ ∩ Δ = ∅. We weaken s[Δ] to s[Δ, Γ] by weakEnd and t[Γ] to t[Δ, Γ] by weakBeg. Then cl(v, w) := ⟨(s, t)[Δ, Γ]; d, e⟩

(vfold) Let ⟨t; e⟩ := cl(v). Then cl(fold(v)) := ⟨fold(t); e⟩ Proposition 1 (Values evaluate to themselves)

∀σ ∈ Ty, v ∈ Val^{σ}. cl(v) ⇓ v

Proof by induction over v. The base cases (vunit), (vlam) and (vrec) are trivial by (opunit), (oplam) and (oprec).

(vinl) By induction hypothesis (IH) we have cl(v) =: ⟨t; e⟩ ⇓ v.

Using (opinl) we get cl(inl(v)) = ⟨inl(t); e⟩ ⇓ inl(v).

(vinr) analogously (vfold) analogously by (opfold) (vpair) By IH we have cl(v) =: ⟨s; d⟩ ⇓ v. Using (opweakEnd) we

get ⟨s; d, e⟩ ⇓ v. Also by IH we have cl(w) =: ⟨t; e⟩ ⇓ w, hence by (opweakBeg) ⟨t; d, e⟩ ⇓ w. (oppair) finishes the proof producing cl(v, w) = ⟨(s, t); d, e⟩ ⇓ (v, w) □

3.4 Examples

In the following we will show two properties of the type Nat defined in section 2.3.1.

3.4.1 Numerals

Recall the definition of Nat ≡ Rec X.1 + X, O and S in section 2.3.1. We can show that the numerals Val^{Nat} are isomorphic to the natural numbers ℕ.

Proposition 2

Val^{Nat} = {S^{n}(O) : n ∈ ℕ}

Proof. For “⊇” we show ∀n ∈ ℕ. S^{n}(O) ∈ Val^{Nat} by induction over n.

n = 0

\overline{vunit} ; () ∈ Val^{1}

\overline{vinl}

inl() ∈ Val^{1+Nat}

\overline{vfold}

O ≡ fold(inl()) ∈ Val^{Nat}

n → n+1

\overline{IH}

S^{n}(O) ∈ Val^{Nat}

\overline{vinr}

inr(S^{n}(O)) ∈ Val^{1+Nat}

\overline{vfold}

S^{n+1}(O) ≡ fold(inr(S^{n}(O))) ∈ Val^{Nat}

The other direction “⊆”: We show simultaneously

(i) v ∈ Val^{Nat} → v ∈ {S^{n}(O) : n ∈ ℕ}
(ii) v ∈ Val^{1+Nat} → v ∈ {inl(), inr(S^{n}(O)) : n ∈ ℕ}

by induction on generation of v. The only matching cases are:

(vinl) (ii) v ≡ inl() ∈ Val^{1+Nat}: Obviously v ∈ {inl(), inr(S^{n}(O)) :

n ∈ ℕ}.

(vinr) (ii) v ≡ inr(v′), v′ ∈ Val^{Nat}: By induction hypothesis (i) we have v′ ∈ {S^{n}(O) : n ∈ ℕ}, therefore we see immediately that v ∈ {inl(), inr(S^{n}(O)) : n ∈ ℕ}.

(vfold) (i) v ≡ fold(v′), v′ ∈ Val^{1+Nat}: By induction hypothesis (ii) either v′ = inl() or there is an n ∈ ℕ with v′ = inr(S^{n}(O)). In the first case v = O and in the second case v = S^{n+1}(O), thus in both cases v ∈ {S^{n}(O) : n ∈ ℕ}. □

For the following we introduce the abbreviation \overline{n} := S^{n}(O) for numerals.

3.4.2 Soundness of addition

In order to show that our function add really implements addition on numbers, we have to prove

∀n, m ∈ ℕ. ⟨add S^{n}(O) S^{m}(O); ·⟩ ⇓ S^{n+m}(O)

Here we want to show it for the values ⟨add; ·⟩ ∈ Val^{Nat→Nat→Nat}, \overline{n}, \overline{m} ∈ Val^{Nat}. (In the following we will write add also for its value ⟨add; ·⟩.) However, (add@\overline{n})@\overline{m} is not syntactically correct, because the application @ is a function symbol Val^{σ→τ} × Val^{σ} → Cl^{τ}. Therefore we need a function add\overline{n} ∈ Val^{Nat→Nat} for each numeral \overline{n} ∈ Val^{Nat}, which we define as the result of evaluating add@\overline{n}, i.e.

add\overline{n} = εv. add@\overline{n} ⇓ v

(Hilbert’s epsilon operator εx. P (x) picks an arbitrary element with the postulated property P; that implies P (εx. P (x)) is true.) We can compute add\overline{n} by our operational semantics:

\overline{oplam} ⟨λx …⟩ ⇓ ⟨λx …⟩

\overline{oplam} ; ⟨λy …⟩ ⇓ ⟨λy …⟩

\overline{opappvl}

⟨λx. λy …; add = add⟩@\overline{n} ⇓ ⟨λy …, x = \overline{n}⟩

\overline{opappvr}

⟨rec add.λx. λy. case(…); ·⟩@\overline{n} ⇓ ⟨λy. case(…); add = add, x = \overline{n}⟩

= def
add@\overline{n} ⇓ add\overline{n}

Now we can prove the correctness of add, i.e. we show

Proposition 3

∀n, m ∈ ℕ. add\overline{n}@\overline{m} ⇓ \overline{n + m}

Proof by induction over n. Case n = 0: We show add_{O}@\overline{m} ⇓ \overline{m}.

\overline{opvar}

⟨x; … x = O⟩ ⇓ O ≡ fold(inl())

\overline{opunfold}

⟨unfold(x); … x = O⟩ ⇓ inl()

\overline{opweak}

⟨unfold(x); … x = O, y = \overline{m}⟩ ⇓ inl()

\overline{opvar} ; ⟨y; … y = \overline{m}⟩ ⇓ \overline{m}

\overline{opweak}

⟨y; … y = \overline{m}, = ()⟩ ⇓ \overline{m}

\overline{opcasel}

⟨case(unfold(x), ^{1}.y, x^{′Nat}.S(add x′ y); add = add, x = O, y = \overline{m}⟩ ⇓ \overline{m}

\overline{opappvl}

⟨λy^{Nat}. case(…); add = add, x = O⟩@\overline{m} ⇓ \overline{m}

Case n → n+1: Given the induction hypothesis add\overline{n}@\overline{m} ⇓ \overline{n + m}. we show add_{S(\overline{n})}@\overline{m} ⇓ S(\overline{n + m}). For technical reasons we will split the proof tree 3 OPERATIONAL SEMANTICS 22 into three parts: (I) Derivation of ⟨add x′; … x′ = \overline{n}⟩ ⇓ add\overline{n}:

\begin{matrix}· \\ · \\ · \end{matrix} ⟨add; …⟩ ⇓ add \begin{matrix}· \\ · \\ · \end{matrix} ⟨x′; … x′ = \overline{n}⟩ ⇓ \overline{n} \begin{matrix}· \\ · \\ · \end{matrix} Def. of add\overline{n}

add@\overline{n} ⇓ add\overline{n}

\overline{opapp}

⟨add x′; … x′ = \overline{n}⟩ ⇓ add\overline{n}

(II) Derivation of ⟨S(add x′ y); … y = \overline{m}, x′ = \overline{n}⟩ ⇓ S(\overline{n + m}):

\begin{matrix}\begin{matrix}· \\ · \\ · \end{matrix} & (I) \\ ⟨add x′; … x′ = \overline{n}⟩ ⇓ add\overline{n} \end{matrix} \begin{matrix}· \\ · \\ · \end{matrix} ; ⟨y; …⟩ ⇓ \overline{m} \overline{IH} ; add\overline{n}@\overline{m} ⇓ \overline{n + m}

\overline{opapp}

⟨(add x′) y; … y = \overline{m}, x′ = \overline{n}⟩ ⇓ \overline{n + m}

\overline{opinr}

⟨inr(add x′ y); … y = \overline{m}, x′ = \overline{n}⟩ ⇓ inr(\overline{n + m})

\overline{opfold}

⟨S(add x′ y); … y = \overline{m}, x′ = \overline{n}⟩ ⇓ S(\overline{n + m})

(III) Derivation of add_{S(\overline{n})}@\overline{m} ⇓ S(\overline{n + m}):

\begin{matrix}· \\ · \\ · \end{matrix}

⟨unfold(x); ...x=S(\overline{n})...⟩ ⇓ inr(\overline{n})

\begin{matrix}· \\ · \\ · \end{matrix} (II) ⟨S(add x′ y); ...y=\overline{m}, x′=\overline{n}⟩ ⇓ S(\overline{n + m})

\overline{opcaser}

⟨case(unfold(x), ^{1}.y, x^{′Nat}.S(add x′ y)); … x = S(\overline{n}), y = \overline{m}⟩ ⇓ S(\overline{n + m})

\overline{opappvl}

⟨λy^{Nat}. case(…); add = add, x = S(\overline{n})⟩@\overline{m} ⇓ S(\overline{n + m})

= def

add_{S(\overline{n})}@\overline{m} ⇓ S(\overline{n + m})

□

4 Semantic values

Now that we have built a partial language by defining types, terms and an operational semantics, we are interested in a sublanguage that is total. Therefore we define a semantics [[·]] over the types, so that [[σ]] contains all “good” values of type σ, i.e. all values that guarantee termination.

Since recursive types Rec X.σ(X) are interpreted as the least fixed point of the operator represented by σ(X), we have to ensure monotonicity of our types. In a lemma we will show that all types are monotone since we have restricted ourselves to strictly positive types. But first some facts about the

Least fixed point. Let (U, ⊆) be a complete lattice^{7} of sets. By Tarski’s fixed-point theorem [Tar55] every monotone^{8} operator F : U → U has a least fixed point F := lfp F with the following two properties

(ispfp) F(F) ⊆ F
(ismpfp) ∀A ∈ U. F(A) ⊆ A → F ⊆ A

which characterize F as the least pre-fixed point of F. We can show that

F = inf {A ∈ U : F(A) ⊆ A}

We get “⊇” by (ispfp) since F ∈ A := {A ∈ U : F(A) ⊆ A} and “⊆” by (ismpfp) immediately.

For F to be the fixed point we need F ⊆ F(F). We obtain this as follows: Since F is monotone F(F(F)) ⊆ F(F) by (ispfp), hence F(F) ∈ A and therefore by (ismpfp) F ⊆ F(F).

Folding of value sets. For convenience we define a polymorphic bijective function fold that performs folding on all elements of a value set:

fold : P (Val^{σ(Rec X.σ(X))}) → P (Val^{Rec X.σ(X))})
W ↦ {fold(v) : v ∈ W }

From the rule (vfold) and its inversion we can derive that fold is monotone.

7i.e. to every collection A ⊆ U of sets there is an infimum inf A w.r.t. set inclusion “⊆”.

8F monotone :↔ ∀A ⊆ B. F(A) ⊆ F(B).

Semantic Values. The idea is that good values of →-type are the functions f that for every good input u produce a good output v. (This of course implies termination of f on all good inputs.) Good values of other types have no other restriction, except that they be derived from good values of the component types.

Let σ(X⃗) be a type over the free type variables X⃗ = X_{1}, …, X_{n}; τ⃗ = τ_{1}, …, τ_{n} a list of closed types and V⃗ = V_{1}, …, V_{n} ⊆ Valτ⃗ sets of (syntactic) values of type τ⃗ (i.e. V_{1} ⊆ Val^{τ_{1}}, …, V_{n} ⊆ Val^{τ_{n}}). The set of semantic values [[σ(X⃗)]]V⃗ ⊆ Val^{σ(τ⃗)} of type σ over the value sets V⃗ is a subset of the values of the type σ the variables of which are substituted by τ⃗. It is defined by recursion over σ as follows:

(Unit) [[1]] := {()}

(Var) [[X_{n}]]V⃗ := V_{n}

(Weak) [[σ(X⃗, Y)]]_{V⃗ ,W} := [[σ(X⃗)]]V⃗

(Sum) [[(σ + τ)(X⃗)]]V⃗ := {inl(v) : v ∈ [[σ(X⃗)]]V⃗ } ∪ {inr(v) : v ∈

[[τ(X⃗)]]V⃗ }

(Prod) [[(σ × τ)(X⃗)]]V⃗ := {(v, w) : v ∈ [[σ(X⃗)]]V⃗ , w ∈ [[τ(X⃗)]]V⃗ }

(Arr) [[σ → τ(X⃗)]]V⃗ := {f ∈ Val^{σ→τ(τ⃗)} : ∀u ∈ [[σ]]. ∃v ∈ [[τ(X⃗)]]V⃗ .

f@u ⇓ v}

(Rec) [[Rec Y.σ(X⃗, Y)]]V⃗ := lfp F, where we define F as

F : P (Val^{Rec Y.σ(τ⃗,Y)}) → P (Val^{Rec Y.σ(τ⃗,Y)})
W ↦ fold ([[σ(X⃗, Y)]]_{V⃗ ,W} )

For this definition to be valid the least fixed point in (Rec) must exist. This is only guaranteed if the operator F is monotone, which we show simultaneously to the definition. For reasons of clarity we have written it down separately in the following

Lemma 4 (Monotonicity of semantic values)

∀σ(X⃗, Y, Z⃗). A ⊆ B → [[σ(X⃗, Y, Z⃗)]]_{V⃗ ,A,W⃗} ⊆ [[σ(X⃗, Y, Z⃗)]]_{V⃗ ,B,W⃗}

Proof by induction on σ. Here the strict positivity of σ comes in decisively (see case (Arr)).

(Unit) Nothing to show.

(Var) [[X_{n}]]V⃗ = V_{n} ⊆ V_{n} = [[X_{n}]]V⃗ [[Y]]_{V⃗ ,A} = A ⊆ B = [[Y]]_{V⃗ ,A} [[Z_{n}]]_{V⃗ ,A,W⃗} = W_{n} ⊆ W_{n} = [[Z_{i}]]_{V⃗ ,A,W⃗}

(Weak) by Y: [[σ(X⃗, Y)]]_{V⃗ ,A} = [[σ(X⃗)]]V⃗ = [[σ(X⃗, Y)]]_{V⃗ ,B} by Z: [[σ(X⃗, Y, Z⃗, Z)]]_{V⃗ ,A,W⃗ ,W} = [[σ(X⃗, Y, Z⃗)]]_{V⃗ ,A,W⃗} ⊆ [[σ(X⃗, Y, Z⃗)]]_{V⃗ ,B,W⃗} = [[σ(X⃗, Y, Z⃗, Z)]]_{V⃗ ,B,W⃗ ,W} by IH.

Now for reasons of readability we leave out X⃗, Z⃗, V⃗ and W⃗.

(Sum) By IH we have [[σ(Y)]]_{A} ⊆ [[σ(Y)]]_{B} and [[τ(Y)]]_{A} ⊆

[[τ(Y)]]_{B}. Thus [[(σ + τ)(Y)]]_{A} = \underbrace{\{inl(v) : v ∈ [[σ(Y)]]_{A}\}}_{⊆\{inl(v):v∈[[σ(Y)]]_{B}\}} ∪

\underbrace{\{inr(v) : v ∈ [[τ(Y)]]_{A}\}}_{⊆\{inr(v):v∈[[τ(Y)]]_{B}\}} ⊆ [[(σ + τ)(Y)]]_{B} by monotonicity of

set union “∪”.

(Prod) [[σ(Y)]]_{A} ⊆ [[σ(Y)]]_{B} and [[τ(Y)]]_{A} ⊆ [[τ(Y)]]_{B} by IH. [[(σ × τ)(Y)]]_{A} = {(v, w) : v ∈ [[σ(Y)]]_{A}, w ∈ [[τ(Y)]]_{A}} ⊆ {(v, w) : v ∈ [[σ(Y)]]_{B}, w ∈ [[τ(Y)]]_{B}} = [[(σ ×τ)(Y)]]_{B} by monotonicity of “×”.

(Arr) Assume f ∈ [[σ → τ(Y)]]_{A} and u ∈ [[σ]]. By definition there is a v ∈ [[τ(Y)]]_{A} with f@u ⇓ v. By IH v ∈ [[τ(Y)]]_{B} and hence f ∈ [[σ → τ(Y)]]_{B}.

(Rec) [[Rec Z.σ(X⃗, Y, Z⃗, Z)]]_{V⃗ ,A,W⃗} ⊆ [[Rec Z.σ(X⃗, Y, Z⃗, Z)]]_{V⃗ ,B,W⃗} is what we have to show. We introduce the abbreviation F (W) := fold ([[σ(X⃗, Y, Z⃗, Z)]]_{V⃗ , ,W⃗ ,W} ) and thus or goal becomes lfp F_{A} ⊆ lfp F_{B}. By induction hypothesis we have [[σ(X⃗, Y, Z⃗, Z)]]_{V⃗ ,A,W⃗ ,W} ⊆ [[σ(X⃗, Y, Z⃗, Z)]]_{V⃗ ,B,W⃗ ,W} for all W and hence by monotonicity of fold F_{A}(lfp F_{B}) ⊆ F_{B}(lfp F_{B}) for W ≡ lfp F_{B}. By (ispfp) for F_{B} we obtain F_{A}(lfp F_{B}) ⊆ lfp F_{B}. Now we apply (ismpfp) for F_{A} and get lfp F_{A} ⊆ lfp F_{B}. □

Corollary 5

V⃗ ⊆ W⃗ → [[σ(X⃗)]]V⃗ ⊆ [[σ(X⃗)]]W⃗

Proof by iterated application of lemma 4.

For the desired monotonicity property [[σ(X⃗)]]V⃗ ⊆ [[σ(τ⃗)]] (V⃗ ⊆ [[τ⃗]]) we need the corollary of the following

Lemma 6 (Substitution in semantic values)

[[σ(X⃗, Y, Z⃗)]]_{V⃗ ,[[τ]],W⃗} = [[σ(X⃗, τ, Z⃗)]]_{V⃗ ,W⃗}

Proof by induction on σ. The case (Unit) is trivial, (Weak), (Sum), (Prod) and (Arr) are immediately shown by the induction hypothesis, so let us have a look at the remaining two:

(Var) [[Y]]_{V⃗ ,[[τ]],W⃗} = [[τ]] = [[Y [Y := τ]]]_{V⃗ ,W⃗}

(Rec) We introduce the abbreviations F(W) := [[σ(X⃗, Y, Z⃗, Z)]]_{V⃗ ,[[τ]],W⃗ ,W} and G(W) := [[σ(X⃗, τ, Z⃗, Z)]]_{V⃗ ,W⃗ ,W} and hence have to show lfp (fold ∘ F) = lfp (fold ∘ G). By IH we have ∀W.F(W) = G(W), thus F = G and also fold ∘ F = fold ∘ G. Since the operators are equal, the fixed points are equal as well, hence lfp (fold ∘ F) = lfp (fold ∘ G). □

Corollary 7

[[σ(X⃗)]]_{[[τ⃗]]} = [[σ(τ⃗)]]

Proof by iterated application of lemma 6.

Corollary 8 (Subset property of semantic values) For all V⃗ ⊆ [[τ⃗]] we have

[[σ(X⃗)]]V⃗ ⊆ [[σ(τ⃗)]]

Proof by corollary 5 and 7.

With the help of the above results we can show that the folding rule v ∈ Val^{σ(Rec X.σ(X))} → v ∈ Val^{Rec X.σ(X)} fo syntactic values is also valid for semantic values. Furthermore the opposite direction of this rule is valid as well.

Corollary 9 (Folding rule for semantic values)

fold ([[σ(Rec X.σ(X))]]) = [[Rec X.σ(X)]]

Proof. By corollary 7 [[σ(Rec X.σ(X))]] = [[σ(X)]]_{[[Rec X.σ(X)]]} and [[Rec X.σ(X)]] is the least fixed point of fold ∘ [[σ(X)]] .

Codomain and termination. We define the codomain of a function f ∈ [[σ → τ(X⃗)]]V⃗ as

CoDom(f) := {v ∈ [[τ(X⃗)]]V⃗ : ∃u ∈ [[σ]]. f@u ⇓ v}

We say a closure c ∈ Cl^{σ} terminates iff it evaluates to some value v ∈ [[σ]]:

c ⇓:↔ ∃v ∈ [[σ]]. c ⇓ v

4.1 Example

To clarify the semantics of a recursive type, we will consider [[Nat]] and show that it contains all numerals \overline{n} ∈ Val^{Nat}:

[[Nat]] = Val^{Nat}

Since Nat ≡ Rec X.1 + X we have to show that Val^{Nat} is least fixed point of

F : P (Val^{Nat}) → P (Val^{Nat})
F(W) := {fold(v) : v ∈ [[1 + X]]_{W} }
= {fold(inl()), fold(inr(v)) : v ∈ W }
= {O, S(v) : v ∈ W }

Since trivially F(Val^{Nat}) ⊆ Val^{Nat}, Val^{Nat} is pre-fixed point of F. We only have to show that there is no smaller pre-fixed point W. To this end, we show for all pre-fixed points W ⊆ Val^{Nat}

(i) ⋃_{n∈ℕ} F^{n}(∅) ⊆ W
(ii) Val^{Nat} ⊆ ⋃_{n∈ℕ} F^{n}(∅)

Proof. (i) We show ∀n ∈ ℕ. F^{n}(∅) ⊆ W by induction on n:

n = 0: F^{0}(∅) = ∅ ⊆ W

n → n+1: By induction hypothesis F^{n}(∅) ⊆ W, hence by monotonicity of F and (ispfp) for W we obtain F^{n+1}(∅) = F(F^{n}(∅)) ⊆

F(W) ⊆ W.

Hence it follows that ⋃_{n∈ℕ} F^{n}(∅) ⊆ W. (ii) We show ∀n ∈ ℕ. F^{n}(∅) = \{\overline{m} : m < n} by induction on n:

n = 0: F^{0}(∅) = ∅

n → n+1: By induction hypothesis F^{n}(∅) = \{\overline{m} : m < n\}, thus F^{n+1}(∅) = F(\{\overline{m} : m < n\}) = \{O, S(\overline{m}) : m < n\} = \{\overline{m} :

m < n + 1}.

Hence it follows that Val^{Nat} = ⋃_{n∈ℕ} \{\overline{m} : m < n\} ⊆ ⋃_{n∈ℕ} F^{n}(∅). □

5 Wellfoundedness of the structural ordering

We now define a transitive structural ordering < on the semantic values. The basic idea is that a value v is structurally smaller than a value w if the representing tree of v is a subtree of w.

In our approach the order of a value is only decreased (<) by case analysis, whereas projection and application keep it on the same level (≤). This has to be explained: Since we want to show that a function f ∈ Val^{σ→τ} terminates on an input v ∈ [[σ]] if it terminates on all w ∈ [[σ]] that are structurally smaller than v, i.e. w < v, we only want to be able to compare values of the same type σ. Since injection (inl, inr), pairing and building functions by λ enlarge the type and only folding shrinks the type, we need at least one folding step to obtain a greater value v of the same type σ out of a given value w. Therefore σ is a recursive type and has at least one “Rec” in its component. But since only recursive types over sums are both non-trivial and non-empty, these are the only types of interest for our work. Thus we can conclude that on the way of generating v out of w there is at least one injection, which then actually increases (<) the order. (See the example at the end of this section.)

Structural ordering. We define a pair of mutually dependent families of relations <_{σ,τ}, ≤_{σ,τ}⊆ [[σ]] × [[τ]] inductively as follows:

(lerefl) v ≤_{σ,σ} v  (lelt) {w <_{σ,τ} v \atop w ≤_{σ,τ} v}

(ltinl) {w ≤_{ρ,σ} v \atop w <_{ρ,σ+τ} inl(v)}  (ltinr) {w ≤_{ρ,τ} v \atop w <_{ρ,σ+τ} inr(v)}

(ltfst) {w <_{ρ,σ} v \atop w <_{ρ,σ×τ} (v, v′)}  (ltsnd) {w <_{ρ,τ} v′ \atop w <_{ρ,σ×τ} (v, v′)}

(lefst) {w ≤_{ρ,σ} v \atop w ≤_{ρ,σ×τ} (v, v′)}  (lesnd) {w ≤_{ρ,τ} v′ \atop w ≤_{ρ,σ×τ} (v, v′)}

(ltarr) {∃v ∈ CoDom(f).w <_{ρ,τ} v \atop w <_{ρ,σ→τ} f} (learr) {∃v ∈ CoDom(f).w ≤_{ρ,τ} v \atop w ≤_{ρ,σ→τ} f}

(ltfold)

w <_{σ,τ(Rec X.τ(X))} v
w <_{σ,Rec X.τ(X)} fold(v)

(lefold)

w ≤_{σ,τ(Rec X.τ(X))} v
w ≤_{σ,Rec X.τ(X)} fold(v)

By definition < and ≤ are transitive, < is irreflexive and ≤ reflexive.

Notation. Since the indexes σ and τ of <_{σ,τ} and ≤_{σ,τ} are determined in most expressions, we omit them for better readability.

We want to show that every set of semantic values is wellfounded which is given if every value is accessible. Therefore we first define the sets of accessible values w.r.t. < and then we show that each value is in the accessible set of its type.

Accessible sets. We define the family of accessible sets Acc^{σ} ⊆ [[σ]] w.r.t. < inductively as follows. (This is the usual definition.)

(acc) {∀τ, [[τ]] ∋ w < v. w ∈ Acc^{τ} \atop v ∈ Acc^{τ}}

Notation. For lists ρ⃗ of types we use the abbreviation Accρ⃗ := Acc^{ρ_{1}}, …, Acc^{ρ_{n}}.

Proposition 10 (Destructors for Acc) If a value is accessible, then smaller values are accessible as well:

(acc^{−1}) ∀v ∈ Acc^{σ}, [[τ]] ∋ w < v.w ∈ Acc^{τ}
(accfst) ∀(v, v′) ∈ Acc^{σ×τ}.v ∈ Acc^{σ}
(accsnd) ∀(v, v′) ∈ Acc^{σ×τ}.v′ ∈ Acc^{τ}
(accres) ∀f ∈ Acc^{σ→τ}.CoDom(f) ⊆ Acc^{τ}
(accunf) ∀ fold(v) ∈ Acc^{Rec X.σ(X)}.v ∈ Acc^{σ(Rec X.σ(X))}

Proof.

(acc^{−1}) We assume v ∈ Acc^{σ}. Since there is only one constructor (acc) for accessible sets, we can use it in the reverse direction and get [[τ]] ∋ w < v.w ∈ Acc^{τ}, what we had to show.

(accfst) To prove accessibility of v we have to show ∀[[ρ]] ∋ w < v.w ∈ Acc^{ρ}. Be now [[ρ]] ∋ w < v. By (ltfst) we get w < (v, v′), and since (v, v′) is accessible by assumption, w ∈ Acc^{ρ} by (acc^{−1}).

(accsnd) analogously (accres) We have to show v ∈ CoDom(f) → v ∈ Acc^{τ}. Assume [[ρ]] ∋

w < v ∈ CoDom(f). By (ltarr) we get w < f and again (acc^{−1}) proves w ∈ Acc^{ρ}, hence v ∈ Acc^{τ}.

(accunf) Again we have to show ∀[[ρ]] ∋ w < v.w ∈ Acc^{ρ}. Be now w < v. By (ltfold) we get w < fold(v), and since fold(v) is accessible by assumption, w ∈ Acc^{ρ} by (acc^{−1}). □

Proposition 11 (Accessibility of less-equal values) The values less than or equal to an accessible value are accessible themselves.

(accle) ∀v ∈ Acc^{τ}, [[σ]] ∋ w ≤ v.w ∈ Acc^{σ}

Proof by induction on generation of w ≤ v:

(lerefl) Pattern matches with σ ≡ τ, w ≡ v: v ≤ v ∈ Acc^{τ}.

(lelt) w < v: We get w ∈ Acc^{σ} by (acc^{−1}).

(lefst) Pattern matches with τ ≡ σ′ × τ′, v ≡ (v′, w′): We get v′ ∈ Acc^{σ′} by (accfst) and w ∈ Acc^{σ} by the induction hypothesis w ≤ v′ → w ∈ Acc^{σ}.

(lesnd) analogously

(learr) Pattern matches with τ ≡ σ′ → τ′: There is a v′ ∈ CoDom(v) with w ≤ v′. Since by (accres) v′ ∈ Acc^{τ′}, w ∈ Acc^{σ} by induction hypothesis.

(lefold) Pattern matches with τ ≡ Rec X.σ′(X), v ≡ fold(v′). Now v′ ∈ Acc^{σ(Rec X.σ′(X))} by (accunf) and thus w ∈ Acc^{σ} by induction hypothesis. □

Proposition 12 (Accessibility of successors) The successors of accessible values are accessible as well.

(accinl) ∀v ∈ Acc^{σ}. inl(v) ∈ Acc^{σ+τ}
(accinr) ∀v ∈ Acc^{τ}. inr(v) ∈ Acc^{σ+τ}
(accpair) ∀v ∈ Acc^{σ}, v′ ∈ Acc^{τ}. (v, v′) ∈ Acc^{σ×τ}
(accarr) ∀f ∈ [[σ → τ]]. (CoDom(f) ⊆ Acc^{τ}) → f ∈ Acc^{σ→τ}
(accfold) fold (Acc^{σ(Rec X.σ(X))}) ⊆ Acc^{Rec X.σ(X)}

Proof. We show all propositions by induction over the structural ordering.

(accinl) To prove inl(v) ∈ Acc^{σ+τ} we have to show ∀[[ρ]] ∋ w < inl(v).w ∈ Acc^{ρ} by induction over the generation of w < inl(v). Only case (ltinl) matches: w ≤ v. By (accle) we get w ∈ Acc^{ρ}.

(accinr) analogously

(accpair) We show ∀[[ρ]] ∋ w < (v, v′).w ∈ Acc^{ρ} by induction over the generation of w < (v, v′). The first matching case (ltfst) gives us w < v, and since v ∈ Acc^{σ} also w ∈ Acc^{ρ}. Case (ltsnd) analogous.

(accarr) Induction over [[ρ]] ∋ w < f gives us by (ltarr) a v ∈ CoDom(f) with w < v. Since by assumption v ∈ Acc^{τ}, we have w ∈ Acc^{ρ}. Hence f ∈ Acc^{σ→τ}.

(accfold) We must show ∀v ∈ Acc^{σ(Rec X.σ(X))}. fold(v) ∈ Acc^{Rec X.σ(X)}. Given an arbitrary value w, w < fold(v) is generated out of w < v by (ltfold). Again by assumption v ∈ Acc^{σ(Rec X.σ(X))}, thus w is accessible and hence fold(v) ∈ Acc^{Rec X.σ(X)}. □

Now we can show that all semantic values are accessible. It would be sufficient to know that all semantic values of closes types [[σ]] are accessible. But to prove it for recursive types we have to show the stronger proposition that also the semantic values of open types are accessible, where we insert sets of accessible values for the free type variables.

Lemma 13 (All semantic values are accessible)

∀σ(X⃗), ρ⃗. [[σ(X⃗)]]_{Acc}ρ⃗ ⊆ Acc^{σ(ρ⃗)}

Proof by induction over σ(X⃗).

(Unit) [[1]] = {()} ⊆ Acc^{1}. We have to show ∀[[ρ]] ∋ w < ().w ∈ Acc. This is trivially true because there is no matching rule for w < ().

(Var) [[X_{n}]]_{Acc}ρ⃗ = Acc^{ρ_{n}} = Acc^{X_{n}[X⃗:=ρ⃗]}

(Weak) [[σ(X⃗, X)]]_{Acc}_{ρ⃗,ρ} = [[σ(X⃗)]]_{Acc}ρ⃗ ⊆ Acc^{σ[X⃗:=ρ⃗]} = Acc^{σ[X⃗:=ρ⃗,X:=ρ]} by IH.

(Sum) Be v ∈ [[(σ + τ)(X⃗)]]_{Acc}ρ⃗. Case v = inl(v′), v′ ∈ [[σ(X⃗)]]_{Acc}ρ⃗: By IH we have v′ ∈ Acc^{σ(ρ⃗)}, hence by (accinl) v′ ∈ Acc^{(σ+τ)(ρ⃗)}. Case v = inr(v) analogous.

(Prod) Be (v, v′) ∈ [[(σ × τ)(X⃗)]]_{Acc}ρ⃗. Since v ∈ [[σ(X⃗)]]_{Acc}_{ρ⃗)} and v′ ∈ [[τ(X⃗)]]_{Acc}_{ρ⃗)}, by IH v ∈ Acc^{σ(ρ⃗)} and v′ ∈ Acc^{τ(ρ⃗)}, hence by (accpair) (v, v′) ∈ Acc^{(σ×τ)(ρ⃗)}.

(Arr) Be f ∈ [[σ → τ(X⃗)]]_{Acc}ρ⃗. By IH we have CoDom(f) ⊆ [[τ(X⃗)]]_{Acc}ρ⃗ ⊆ Acc^{τ(ρ⃗)}. By Corollary 8 we get f ∈ [[σ → τ(ρ⃗)]] and hence by (accarr) f ∈ Acc^{σ→τ(ρ⃗)}.

(Rec) We define F(W) := fold ([[σ(X⃗, Y)]]_{Accρ⃗,W} ), hence our

goal is [[Rec σ(X⃗, Y)]]_{Acc}ρ⃗ = lfp F ⊆ Acc^{Rec Y.σ(ρ⃗,Y)}. We instantiate the induction hypothesis [[σ(X⃗, Y)]]_{Accρ⃗,Acc^{ρ}} ⊆ Acc^{σ(ρ⃗,ρ)} for ρ ≡ Rec Y.σ(ρ⃗, Y) and get by monotonicity of fold F(Acc^{Rec Y.σ(ρ⃗,Y)}) ⊆ fold (Acc^{σ(ρ⃗,Rec Y.σ(ρ⃗,Y))}). Apply-

ing (accfold) yields F(Acc^{Rec Y.σ(ρ⃗,Y)}) ⊆ Acc^{Rec Y.σ(ρ⃗,Y)}, hence Acc^{Rec Y.σ(ρ⃗,Y)} is pre-fixed point of F. By (ismpfp) we know that lfp F ⊆ Acc^{Rec Y.σ(ρ⃗,Y)}. □

Corollary 14

∀σ(X⃗), ρ⃗. [[σ(X⃗)]]_{Acc}ρ⃗ = Acc^{σ(ρ⃗)}

Proof. “⊆” by lemma, “⊇”: Since for closed types ρ from the lemma we immediately get [[ρ]] = Acc^{ρ}, we have by corollary 7 Acc^{σ(ρ⃗)} = [[σ(ρ⃗)]] = [[σ(X⃗)]]_{[[ρ⃗]]} = [[σ(X⃗)]]_{Acc}ρ⃗.

5.1 Example

As an application of the results of this section we want to prove that the addition on ordinal numbers addOrd ∈ Tm^{Ord→Ord→Ord} defined in section 2.3.2 is structurally recursive. Therefore we must show that for each (semantic) input value recursive calls take place only with structurally smaller (semantic) values. In the following we will identify addOrd with its value ⟨addOrd; ·⟩ ∈ Val^{Ord→Ord→Ord}. There are three possible cases for the input v ∈ [[Ord]]:

v ≡ O: No recursive call.

v ≡ S(v′): v′ ∈ [[Ord]]. We have one recursive call with argument v′, which is structurally smaller than v:

\overline{lerefl} ; v′ ≤ v′ ; \overline{ltinr} ; v′ < inr(v′)

\overline{lelt}

v′ ≤ inr(v′)

\overline{ltinl}

v′ < inl(inr(v′))

\overline{ltfold}

v′ < S(v′) ≡ fold(inl(inr(v′)))

v ≡ Lim(f): f ∈ [[Nat → Ord]]. Here again we have one recursive call. The argument is (f z) which for z ∈ [[Nat]] evaluates to a w ∈ CoDom(f). Thus we can derive w < Lim(f) as follows:

\overline{lerefl} ; w ≤ w

∃I

∃v′ ∈ CoDom(f). w ≤ v′

\overline{learr}

w ≤ f

\overline{ltinr}

w < inr(f)

\overline{ltfold}

w < Lim(f) ≡ fold(inr(f))

□

6 Soundness of the termination criterium

We want to define a subset TM of good terms and prove normalization for all t ∈ TM. Since the recursive terms are candidates of nontermination, we have to restrict ourselves to structurally recursive terms for that we will prove termination easily by the wellfoundedness of the structural ordering. The normalization proof then can be done mechanically.

Structurally recursive terms. The subset of environments of semantic values over context Γ = x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} is of course

[[Γ]] = {x_{1} = v_{1}, …, x_{n} = v_{n} : v_{i} ∈ [[σ_{i}]]} ⊆ Val(Γ)

We will refer to an e ∈ [[Γ]] as a good environment. We define the set of structurally recursive terms SR^{σ→τ}[Γ] of type σ → τ over context Γ as the recursive terms that applied to any value v terminate in any good environment under the condition that they terminate for all structurally smaller values w < v:

SR^{σ→τ}[Γ] := {rec g.t ∈ Tm^{σ→τ}[Γ] : ∀e ∈ [[Γ]], v ∈ [[σ]].
(∀[[σ]] ∋ w < v.⟨rec g.t; e⟩@w ⇓) → ⟨rec g.t; e⟩@v ⇓}

We now want to prove that all structurally recursive terms supplied with any good environment are semantic values, i.e. terminate for every semantic value we apply. Since we have proved wellfoundedness of <, this can easily be done by

Wellfounded induction for families of predicates. We present a formulation of the wellfounded-part-induction principle for our definition of Acc^{σ} as family of accessible sets indexed by type σ. Let P^{σ} be a family of predicates over values of type σ.

(accind′) {∀v ∈ [[σ]]. (∀ρ, [[ρ]] ∋ w < v. P^{ρ}(w)) → P^{σ}(v) \atop ∀v ∈ Acc^{σ}. P^{σ}(v)}

For our purpose a specialization of this induction principle for a single predicate over a fixed type is sufficient. Given a type σ and a predicate P ⊆ [[σ]] we obtain

(accind) {∀v ∈ [[σ]]. (∀[[σ]] ∋ w < v. P (w)) → P (v) \atop ∀v ∈ Acc^{σ}. P (v)}

by defining a family of predicates P^{ρ} ⊆ [[ρ]] as

P^{ρ} := \{ \begin{matrix}P & if ρ = σ \\ [[ρ]] & else \end{matrix}

and applying (accind′). We see that the conditions ∀ρ, [[ρ]] ∋ w < v. P^{ρ}(w) and ∀[[σ]] ∋ w < v. P (w) are equivalent by definition of P^{ρ}.

Lemma 15 (Structurally recursive functions terminate)

∀rec g.t ∈ SR^{σ→τ}, e ∈ [[Γ]]. ⟨rec g.t; e⟩ ∈ [[σ → τ]]

Proof. Our goal is by definition equivalent to

∀rec g.t ∈ SR^{σ→τ}, e ∈ [[Γ]], v ∈ [[σ]]. ⟨rec g.t; e⟩@v ⇓

For a fixed environment e the assumption rec g.t ∈ SR^{σ→τ} expands to

∀v ∈ [[σ]]. (∀[[σ]] ∋ w < v. ⟨rec g.t; e⟩@w ⇓) → ⟨rec g.t; e⟩@v ⇓

By (accind) with P (v) ≡ ⟨rec g.t; e⟩@v ⇓ we get

∀v ∈ Acc^{σ}. ⟨rec g.t; e⟩@v ⇓

which is equivalent to our claim because of Acc^{σ} = [[σ]].

Good terms. We inductively define the set of good terms TM^{σ}[Γ] ⊂ Tm^{σ}[Γ] of type σ over context Γ, i.e. the terms that ensure termination. These rules are almost identical to the original term formation rules (see page 12), we only change Tm to TM and label the rule in CAPITAL letters, e.g.

(PAIR)

s ∈ TM^{σ}[Γ] t ∈ TM^{τ}[Γ]
(s, t) ∈ TM^{σ×τ}[Γ]

Only the rule (rec) is replaced by

(REC)

t ∈ TM^{σ→τ}[Γ, g^{σ→τ}] rec g.t ∈ SR^{σ→τ}[Γ]
rec g.t ∈ TM^{σ→τ}[Γ]

Note that in the second condition rec g.t ∈ SR^{σ→τ}[Γ] we use the natural embedding TM^{σ}[Γ] ↪ Tm^{σ}[Γ] that can be defined by recursion over TM simultanously to the inductive definition in the obvious way.

Good closures. Consequently the set of good closures CL^{τ} of type τ is defined as

Cl^{τ} := {⟨t; e⟩ : Γ ∈ Cxt, t ∈ TM^{τ}[Γ], e ∈ [[Γ]]}
∪ {f@u : f ∈ [[σ → τ]], u ∈ [[σ]]}

Again CL^{τ} ⊆ Cl^{τ}, hence we can use our operational semantics ⇓ on good closures as well. Now no obstacle is in our way to show

Theorem 16 (Normalization)

∀σ, Γ, t ∈ TM^{σ}[Γ], e ∈ [[Γ]]. ⟨t; e⟩ ⇓

Proof by induction on t ∈ TM^{σ}[Γ]. We overload the definition of e^{Γ} and now mean e ∈ [[Γ]].

(UNIT) By (opunit) ⟨(); ·⟩ ⇓ () ∈ [[1]].

(VAR) Since e^{Γ}, x^{σ} = v ∈ [[Γ, x^{σ}]] by (opvar) we prove ⟨x[Γ, x^{σ}]; e, x = v⟩ ⇓ v ∈ [[σ]].

(WEAK) By IH there is a v ∈ [[σ]] such that ⟨t^{σ}[Γ]; e⟩ ⇓ v, hence by (opweak) ⟨t[Γ, x]; e, x = w⟩ ⇓ v ∈ [[σ]].

(INL) By IH ⟨t^{σ}; e⟩ ⇓ v ∈ [[σ]], thus by (opinl) ⟨inl(t)^{σ+τ}; e⟩ ⇓ inl(v) ∈ [[σ + τ]].

(INR) analogously

(CASE) We must show ⟨case(t^{σ+τ}[Γ], x^{σ}.(l^{ρ}[Γ, x^{σ}]), y^{τ}.(r^{ρ}[Γ, y^{τ}])); e⟩ ⇓ v ∈ [[ρ]]. By IH we have ⟨t^{σ+τ}[Γ]; e⟩ ⇓ w′ ∈ [[σ + τ]]. Case w′ = inl(w^{σ}): By IH we get ⟨l^{ρ}[Γ, x^{σ}]; e, x = w⟩ ⇓ v ∈ [[ρ]], hence by (opcasel) we prove our claim. Case w′ = inr(w^{τ}) analogously by (opcaser).

(PAIR) Here we show ⟨(s^{σ}, t^{τ}); e⟩ ⇓. By IH we have ⟨s; e⟩ ⇓ v ∈ [[σ]] and ⟨t; e⟩ ⇓ w ∈ [[τ]] hence by (oppair) ⟨(s, t); e⟩ ⇓ (v, w) which is in [[σ × τ]] by definition.

(FST) By IH ⟨p^{σ×τ}; e⟩ ⇓ (v, w) ∈ [[σ × τ]], hence by (opfst) ⟨fst(p); e⟩ ⇓ v ∈ [[σ]].

(SND) analogously (LAM) By (oplam) ⟨λx^{σ}.t^{τ}; e^{Γ}⟩ ⇓ ⟨λx.t; e⟩. We have to show

⟨λx.t; e⟩ ∈ [[σ → τ]], i.e. ⟨λx.t; e⟩@u ⇓ for all u ∈ [[σ]]. Refinement by (opappvl) reduces our goal to ⟨t; e, x = u⟩ ⇓ which we get by the induction hypothesis.

(REC) Here by (oprec) we have to show ⟨rec g.t; e⟩ ∈ [[σ → τ]], which is true by lemma 15 since rec g.t ∈ SR^{σ→τ} by definition.

(APP) By IH we have ⟨t^{σ→τ}; e⟩ ⇓ f ∈ [[σ → τ]] and ⟨s; e⟩ ⇓ u ∈ [[σ]] therefore f@u ⇓ and by (opapp) ⟨t s; e⟩ ⇓ as well.

(FOLD) By IH ⟨t; e⟩ ⇓ v ∈ [[σ(Rec X.σ(X))]], hence by (opfold) ⟨fold(t); e⟩ ⇓ fold(v), which is in [[Rec X.σ(X)]] by the folding rule for semantic values (corollary 9).

(UNFOLD) By IH ⟨t; e⟩ ⇓ fold(v) ∈ [[Rec X.σ(X)]], hence by (opunfold) ⟨unfold(t); e⟩ ⇓ v, which is in [[σ(Rec X.σ(X))]] by corollary 9.

7 Extensions

In the following we want to extend our soundness proof to positive types, functions with multiple parameters and mutual recursion in order to cover the full functionality of the foetus termination checker.

7.1 Positive types

In the main part of our work we have restricted ourselves to a system with only strictly positive types. But we can without much effort expand the proof of wellfoundedness and therefore the termination criterium to systems with positive inductive types. In the following we will give the modifications to definitions and lemmata such that positive types can be handled as well.

Types. We now distinct between these type variables that appear positive and those that appear negative in types. Because again we do not support polymorphic types and thus need free type variables only for definition of positive recursive types, a type variable may appear either positive or negative (unlike the common definition in System F, where variables may be seen as both positive and negative or neither positive nor negative in some cases).

So we define the family of sets of types Ty(X⃗; Y⃗) over the finite sets of positively appearing variables X⃗ and negatively appearing variables Y⃗ inductively as follows:

(Unit)

1 ∈ Ty(∅; ∅)

(Var)^{9}

X⃗, X ⊂ TyVars
X ∈ Ty(X⃗, X; ∅)

(Weak^{+}) {σ ∈ Ty(X⃗; Y⃗) X ∉ X⃗, Y⃗ \atop σ ∈ Ty(X⃗, X; Y⃗)}

(Weak^{−}) {σ ∈ Ty(X⃗; Y⃗) Y ∉ X⃗, Y⃗ \atop σ ∈ Ty(X⃗; Y⃗ , Y)}

(Sum) {σ, τ ∈ Ty(X⃗; Y⃗) \atop σ + τ ∈ Ty(X⃗; Y⃗)} (Prod) {σ, τ ∈ Ty(X⃗; Y⃗) \atop σ × τ ∈ Ty(X⃗; Y⃗)}

9Note that there is no rule like (Var^{−}) since in the type σ ≡ X created by the rule (Var) the variable X appears positively.

(Arr)^{10} {σ ∈ Ty(Y⃗; X⃗) τ ∈ Ty(X⃗; Y⃗) \atop σ → τ ∈ Ty(X⃗; Y⃗)}
(Rec) {σ ∈ Ty(X⃗, X; Y⃗) \atop RecX.σ ∈ Ty(X⃗; Y⃗)}

Substitution. We now have to define substitution of the positive X⃗ and negative Y⃗ type variables in a type σ(X⃗, Y⃗) by lists of types ξ⃗ and η⃗ over the positive X⃗′ and negative Y⃗′ variables. For σ[X⃗ := ξ⃗; Y⃗ := η⃗] to be in Ty(X⃗′; Y⃗′), it is necessary that ξ⃗ ⊂ Ty(X⃗′; Y⃗′) and ξ⃗ ⊂ Ty(Y⃗′; X⃗′). The complete modified definition:

(Unit) 1[] := 1 (Var) X[X⃗ := ξ⃗, X := ξ; ] := ξ

(Weak^{+}) σ(X⃗, X; Y⃗)[X⃗, X := ρ⃗, ρ; Y⃗ := η⃗] := σ(X⃗)[X⃗ := ξ⃗; Y⃗ := η⃗] (Weak^{−}) σ(X⃗; Y⃗ , Y)[X⃗ := ρ⃗; Y⃗ , Y := η⃗, η] := σ(X⃗)[X⃗ := ξ⃗; Y⃗ := η⃗]

(Sum) (σ(X⃗; Y⃗) + τ(X⃗; Y⃗)) [X⃗ := ξ⃗; Y⃗ := η⃗] :=

σ[X⃗ := ξ⃗; Y⃗ := η⃗] + τ[X⃗ := ξ⃗; Y⃗ := η⃗]

(Prod) (σ(X⃗; Y⃗) × τ(X⃗; Y⃗)) [X⃗ := ξ⃗; Y⃗ := η⃗] :=

σ[X⃗ := ξ⃗; Y⃗ := η⃗] × τ[X⃗ := ξ⃗; Y⃗ := η⃗]

(Arr) (σ(Y⃗; X⃗) → τ(X⃗; Y⃗)) [X⃗ := ξ⃗; Y⃗ := η⃗] :=

σ[Y⃗ := η⃗; X⃗ := ξ⃗] → τ[X⃗ := ξ⃗; Y⃗ := η⃗]

(Rec) We can assume Z ∉ X⃗′, Y⃗′ by the renaming convention. (RecZ.σ(X⃗, Z; Y⃗)) [X⃗ := ξ⃗; Y⃗ := η⃗] :=

RecZ. (σ[X⃗ := ξ⃗(X⃗′, Z), Z := Z; Y⃗ := η⃗])

10The rule (Arr) implicitely defines positive and negative appearance: A variable is positive in a type σ → τ iff it is positive in τ and negative in σ and vice versa. All other rules preserve positivity and negativity.

Nothing changes for terms, syntactic values and the operational semantics, but we have to extend our definition of semantic values and our lemmata showing monotonicity, because we need the property

[[(σ → τ)(X⃗; Y⃗)]]_{V⃗;[[η⃗]]} ⊆ [[(σ → τ)(ξ⃗; η⃗)]]

for V⃗ ⊆ Valξ⃗ in order to show wellfoundedness.

Semantic Values. Be V⃗ ⊆ Valξ⃗, W⃗ ⊆ Valη⃗. We define the set of semantic values [[σ(X⃗; Y⃗)]]_{V⃗;W⃗} ⊆ Val^{σ(ξ⃗;η⃗)} by recursion over σ:

(Unit) [[1]] := {()}

(Var) [[X_{n}]]V⃗ := V_{n}

(Weak^{+}) [[σ(X⃗, X; Y⃗)]]_{V⃗ ,V;W⃗} := [[σ(X⃗; Y⃗)]]_{V⃗;W⃗}

(Weak^{−}) [[σ(X⃗; Y⃗ , Y)]]_{V⃗;W⃗ ,W} := [[σ(X⃗; Y⃗)]]_{V⃗;W⃗}

(Sum) [[(σ + τ)(X⃗; Y⃗)]]_{V⃗;W⃗} := {inl(v) : v ∈ [[σ(X⃗; Y⃗)]]_{V⃗;W⃗} } ∪ {inr(v) :

v ∈ [[τ(X⃗; Y⃗)]]_{V⃗;W⃗} }

(Prod) [[(σ × τ)(X⃗; Y⃗)]]_{V⃗;W⃗} := {(v, w) : v ∈ [[σ(X⃗; Y⃗)]]_{V⃗;W⃗} , w ∈

[[τ(X⃗; Y⃗)]]_{V⃗;W⃗} }

(Arr) [[(σ → τ)(X⃗; Y⃗)]]_{V⃗;W⃗} := {f ∈ Val^{(σ→τ)(ξ⃗;η⃗)} : ∀u ∈ [[σ(Y⃗;

X⃗)]]_{W⃗;V⃗} . ∃v ∈ [[τ(X⃗; Y⃗)]]_{V⃗;W⃗} . f@u ⇓ v}

(Rec) With the help of the abbreviation

F : P (Val^{Rec X.σ(ξ⃗,X;η⃗)}) → P (Val^{Rec X.σ(ξ⃗,X;η⃗)})
V ↦ fold ([[σ(X⃗, X; Y⃗)]]_{V⃗ ,V;W⃗} )
we define [[Rec X.σ(X⃗, X; Y⃗)]]_{V⃗;W⃗} := lfp F

We extend the lemma 4 by antitonicity for negative variables:

Lemma 17 (Monotonicity of semantic values)

(i) ∀σ ∈ Ty(X⃗, Z, X⃗′; Y⃗). A ⊆ B → [[σ]]_{V⃗ ,A,V⃗′;W⃗} ⊆ [[σ]]_{V⃗ ,B,V⃗′;W⃗}
(ii) ∀σ ∈ Ty(X⃗; Y⃗ , Z, Y⃗′). A ⊆ B → [[σ]]_{V⃗;W⃗ ,A,W⃗′} ⊇ [[σ]]_{V⃗;W⃗ ,B,W⃗′}

Proof simultaneously by induction over σ. Since most parts of this proof can be taken from proof of lemma 4 with small adjustments on the syntax, we only show the interesting cases (Arr) and (Rec)-(ii).

(Arr) (i) Assume an arbitrary f ∈ [[σ → τ]]_{V⃗ ,A,V⃗′;W⃗} (*) and a value u ∈ [[σ(Y⃗; X⃗, Z, X⃗′)]]_{W⃗;V⃗ ,B,V⃗′}. By induction hypothesis (ii) we see u ∈ [[σ]]_{W⃗;V⃗ ,A,V⃗′} and therefore since (*) exists v ∈ [[τ]]_{V⃗ ,A,V⃗′;W⃗} such that f@u ⇓ v. By induction hypothesis (i) we have v ∈ [[τ]]_{V⃗ ,B,V⃗′;W⃗} and hence f ∈ [[σ → τ]]_{V⃗ ,B,V⃗′;W⃗}. (ii) Here we assume f ∈ [[σ → τ]]_{V⃗;W⃗ ,B,W⃗′} and show f ∈ [[σ → τ]]_{V⃗;W⃗ ,A,W⃗′}. Proof analogous to (i).

(Rec) (i) Proof as in lemma 4. (ii) Analogous to (i). We define F′(W) := [[σ(X⃗; Y⃗ , Z, Y⃗′, Z′)]]_{V⃗;W⃗ , ,W⃗′,W} and F (W) := fold(F′(W)). Thus we have to show lfp F_{B} ⊆ lfp F_{A}. We instantiate the induction hypothesis (ii) ∀W.F′_{B}(W) ⊆ F′_{A}(W) for lfp F_{A} and get by monotonicity of fold and by (ispfp) F_{B}(lfp F_{A}) ⊆ F_{A}(lfp F_{A}) ⊆ lfp F_{A}. Further by (ismpfp) lfp F_{B} ⊆ lfp F_{A}. □

Lemma 6 can be expanded to negative variables as well:

Lemma 18 (Substitution in semantic values)

(i) [[σ(X⃗, Z, X⃗′; Y⃗)]]_{V⃗ ,[[ρ]],V⃗′;W⃗} = [[σ(X⃗, ρ, X⃗′; Y⃗)]]_{V⃗ ,V⃗′;W⃗}
(ii) [[σ(X⃗; Y⃗ , Z, Y⃗′)]]_{V⃗;W⃗ ,[[ρ]],W⃗′} = [[σ(X⃗; Y⃗ , ρ, Y⃗′)]]_{V⃗;W⃗ ,W⃗′}

Proof simultaneously by induction over σ. Again most cases are trivial or shown as in lemma 6. We show case (Arr) exemplarily:

(Arr) (i) f ∈ [[(σ → τ)(X⃗, Z, X⃗′; Y⃗)]]_{V⃗ ,[[ρ]],V⃗′;W⃗} iff for all u ∈ [[σ(Y⃗; X⃗, Z, X⃗′)]]_{W⃗;V⃗ ,[[ρ]],V⃗′} there is a v ∈ [[τ(X⃗, Z, X⃗′; Y⃗)]]_{V⃗ ,[[ρ]],V⃗′;W⃗} such that f@u ⇓ v. Applying both induction hypotheses shows that this condition is equivalent to ∀u ∈ [[σ(Y⃗; X⃗, ρ, X⃗′)]]_{W⃗;V⃗ ,V⃗′}∃v ∈ [[τ(X⃗, ρ, X⃗′; Y⃗)]]_{V⃗ ,V⃗′;W⃗} . f@u ⇓ v, which is the case iff f ∈ [[(σ → τ)(X⃗, ρ, X⃗′; Y⃗)]]_{V⃗ ,V⃗′;W⃗}. (ii) analogously □

By iterated application of these two lemmata we get Corollary 19 (Subset property of semantic values) For all σ, V⃗ ⊆ Valξ⃗ we have

[[σ(X⃗; Y⃗)]]_{V⃗;[[η]]} ⊆ [[σ(ξ⃗; η⃗)]]

In principle this corollary does hardly differ from the version for strictly positive type, since by lemma 18 it is equivalent to

∀σ, ξ⃗, η⃗, V⃗ ⊆ Valξ⃗. [[σ(X⃗; η⃗)]]V⃗ ⊆ [[σ(ξ⃗; η⃗)]],

which again can be formulated as

∀σ, ξ⃗, V⃗ ⊆ Valξ⃗. [[σ(X⃗; ∅)]]_{V⃗;∅} ⊆ [[σ(ξ⃗; ∅)]].

A slight modification has to be done on the definition of the

Codomain. For all functions f ∈ [[(σ → τ)(X⃗; Y⃗)]]_{V⃗;W⃗} we define

CoDom(f) := {v ∈ [[τ(X⃗; Y⃗)]]_{V⃗;W⃗} : ∃u ∈ [[σ(Y⃗; X⃗)]]_{W⃗;V⃗} . f@u ⇓ v}

Now since no change has to be done on the definition of the structural ordering and the accessibility propositions 10, 11 and 12, we can prove a reformulation of our central lemma 13. In fact as for corollary 19 the formulation will hardly differ from the original, since we can and need to show it only for types with no free negative variables. (We have to show it for types with free positive variables because of the recursive types.)

Lemma 20 (All semantic values are accessible)

∀σ(X⃗; ∅), ξ⃗. [[σ(X⃗; ∅)]]_{Accξ⃗;∅} ⊆ Acc^{σ(ξ⃗;∅)}

An equivalent formulation would be

∀σ(X⃗; Y⃗), ξ⃗, η⃗. [[σ(X⃗; Y⃗)]]_{Accξ⃗,[[η⃗]]} ⊆ Acc^{σ(ξ⃗;η⃗)}

Proof by induction over σ(X⃗; ∅). Case (Weak^{−}) is not applicable, and all other cases can be treated exactly the same as in the proof of the original lemma, even case (Arr):

(Arr) Be f ∈ [[(σ → τ)(X⃗; ∅)]]_{Acc}ξ⃗. By IH we have CoDom(f) ⊆ [[τ(X⃗; ∅)]]_{Accξ⃗;∅} ⊆ Acc^{τ(ξ⃗;∅)}. By Corollary 19 we get f ∈ [[(σ →

τ)(ξ⃗; ∅)]] and hence by (accarr) f ∈ Acc^{(σ→τ)(ξ⃗;∅)}.

In proving (Arr) we have no induction hypothesis for σ(∅; X⃗), but we actually do not need one, because the accessibility of f depends only on the accessibility of the codomain and not of the domain. □

7.2 Functions with multiple parameters

So far we have only considered functions that are structurally recursive by their first parameter. Now we want to extend our termination criterium to functions of multiple parameters. The termination checker foetus supports them already and calculates a permutation of the arguments such that the lexical ordering on them guarantees termination. In foetus the parameters have to be curried, but here we want to consider functions on tupels v⃗ of parameters because it fits easier in our formalization and formulation of strucural recursion. The proposition that structurally recursive function terminate is changed only slighty to

∀v⃗ ∈ [[σ]]. (∀[[σ]] ∋ w⃗ ≺ v⃗. ⟨rec g.t; e⟩@w⃗ ⇓) → ⟨rec g.t; e⟩@v⃗ ⇓
∀v⃗ ∈ [[σ]]. ⟨rec g.t; e⟩@v⃗ ⇓

Therefore all we have to do is do define the lexical ordering on products and prove that it is wellfounded.

Finite products. We define the nonempty finite product ∏_{i=1}^{n} σ_{i}, n ≥ 1 of types σ_{i} as abbreviation by

∏_{i=1}^{1} σ_{i} := σ_{1}

∏_{i=1}^{n+1} σ_{i} := σ_{n+1} × ∏_{i=1}^{n} σ_{i} (n ≥ 1)

Lexical ordering. Given the closed types σ_{1}, …, σ_{n} we inductively define ≺_{(σ_{n};...;σ_{1})}⊆ [[∏_{i=1}^{n} σ_{i}]] × [[∏_{i=1}^{n} σ_{i}]] as follows:

(lexin) {w <_{σ_{1},σ_{1}} v \atop w ≺_{(σ_{1})} v}

(lexlt) {w <_{σ_{n+1},σ_{n+1}} v w⃗, v⃗ ∈ [[∏_{i=1}^{n} σ_{i}]] \atop (w, w⃗) ≺_{(σ_{n+1};...;σ_{1})} (v, v⃗)}

(lexle) {w ≤_{σ_{n+1},σ_{n+1}} v w⃗ ≺_{(σ_{n};...;σ_{1})} v⃗ \atop (w, w⃗) ≺_{(σ_{n+1};...;σ_{1})} (v, v⃗)}

For simplicity, unlike foetus we do not allow permutation of the components.

The accessible set Acc_{≺}^{(σ_{n};...;σ_{1})} ⊆ [[∏_{i=1}^{n} σ_{i}]] of the lexical ordering ≺_{(σ_{n};...;σ_{1})} is defined inductively as usual (we omit the index of ≺ where it is not necessary):

(acclex) {∀[[∏_{i=1}^{n} σ_{i}]] ∋ w⃗ ≺ v⃗. w⃗ ∈ Acc_{≺}^{(σ_{n};...;σ_{1})} \atop v⃗ ∈ Acc_{≺}^{(σ_{n};...;σ_{1})}}

Now based on the wellfoundedness of the structural ordering < we can prove the

Lemma 21 (Wellfoundedness of the lexical ordering)

∀σ_{1}, …, σ_{n}. [[∏_{i=1}^{n} σ_{i}]] ⊆ Acc_{≺}^{(σ_{n};...;σ_{1})}

Proof by induction on n. It demonstrates the proper use of wellfounded induction.

n = 1 : We have to show [[σ_{1}]] ⊆ Acc_{≺}^{(σ_{1})}. Since by lemma 13 [[σ_{1}]] ⊆ Acc^{σ_{1}} our goal follows from the formally stronger claim ∀v ∈ Acc^{σ_{1}}.v ∈ Acc_{≺}^{(σ_{1})}. Using the wellfounded induction principle (accind) we get the hypothesis (H) ∀w < v.w ∈ Acc_{≺}^{(σ_{1})} and have to show v ∈ Acc_{≺}^{(σ_{1})} which by (acc) is equivalent to ∀w ≺ v. w ∈ Acc_{≺}^{(σ_{1})}. Now the only matching case for w ≺ v is (lexin), therefore w < v and we can finish this part of the proof by (H).

n → n+1 : Our goal is ∀v ∈ [[σ_{n+1}]], v⃗ ∈ [[∏_{i=1}^{n} σ_{i}]]. (v, v⃗) ∈ Acc_{≺}^{(σ_{n+1};...;σ_{1})} (in the following abbreviated to Acc_{≺}). Again, since [[σ_{n+1}]] ⊆ Acc^{σ_{n+1}}, we get the hypothesis (H1) ∀w < v, v⃗ ∈ [[∏_{i=1}^{n} σ_{i}]]. (w, v⃗) ∈ Acc_{≺} by (accind). Now in the same way, since by induction hypothesis [[∏_{i=1}^{n} σ_{i}]] ⊆ Acc_{≺}^{(σ_{n};...;σ_{1})}, we can apply the wellfounded induction principle for the lexical order and get a second hypothesis (H2) ∀w⃗ ≺ v⃗. (v, w⃗) ∈ Acc_{≺} to show the remaining goal (v, v⃗) ∈ Acc_{≺}. This follows from ∀(w, w⃗) ≺ (v, v⃗). (w, w⃗) ∈ Acc_{≺}. Now (w, w⃗) ≺ (v, v⃗) can be generated in two ways: Case (lexlt) w < v: We finish our proof by (H1). Case (lexle) w ≤ v, w⃗ ≺ v⃗: By (H2) we get (v, w⃗) ∈ Acc_{≺} and by the following small lemma also (w, w⃗) ∈ Acc_{≺}. □

Lemma 22

∀(v, v⃗) ∈ Acc_{≺}, v′ ≤ v. (v′, v⃗) ∈ Acc_{≺}

Proof. We have to prove ∀(w, w⃗) ≺ (v′, v⃗). (w, w⃗) ∈ Acc_{≺}. If we can show (w, w⃗) ≺ (v′, v⃗) → (w, w⃗) ≺ (v, v⃗), then the rest follows by (acclex^{−1}). Case analysis on (w, w⃗) ≺ (v′, v⃗):

(lexlt) w < v′: By transitivity of the structural ordering we get w < v and hence by (lexlt) (w, w⃗) ≺ (v, v⃗).

(lexlt) w ≤ v′, w⃗ ≺ v⃗: Again by transitivity of the structural ordering we get w ≤ v and hence by (lexle) (w, w⃗) ≺ (v, v⃗). □

Now having proven wellfoundedness of the lexical ordering we can redefine the set of structurally recursive terms to include the functions the termination of which is ensured by the lexical ordering (σ := ∏_{i=1}^{n} σ_{i}):

SR^{σ→τ}[Γ] := {rec g.t ∈ Tm^{σ→τ}[Γ] : ∀e ∈ [[Γ]], v⃗ ∈ [[σ]].
(∀w⃗ ≺_{(σ_{n};...;σ_{1})} v⃗.⟨rec g.t; e⟩@w⃗ ⇓) → ⟨rec g.t; e⟩@v⃗ ⇓}

By wellfounded induction for the lexical ordering we show that these structurally functions terminate on all inputs (as in lemma 15), and then by defining the good terms with the new definition of SR we can prove normalisation without further changes.

7.3 Mutual recursion

The termination checker foetus also supports mutual recursive functions. Our term syntax so far only allows to define one recursive function at a time, thus mutual recursion is not possible:

(rec)

t ∈ Tm^{σ→τ}[Γ, g^{σ→τ}]
rec g.t ∈ Tm^{σ→τ}[Γ]
(oprec) ⟨rec g.t; e⟩ ⇓ ⟨rec g.t; e⟩

(opappvr) {⟨t; e, g = rec g.t⟩ ⇓ f f@u ⇓ v \atop ⟨rec g.t; e⟩@u ⇓ v}

But these rules can easily be adopted for mutual recursion. We introduce the new term formers rec_{i}^{n} (1 ≤ i ≤ n) where rec_{i}^{n} denotes the ith of n simultaneous defined recursive functions. For each n we get the n introduction rules (written as one with n conclusions):

(rec^{n})

∀1 ≤ i ≤ n. t_{i} ∈ Tm^{σ_{i}→τ_{i}}[Γ, g^{σ_{1}→τ_{1}}, …, g^{σ_{n}→τ_{n}}]
∀1 ≤ i ≤ n. rec_{i}^{n}(g_{1} =t_{1}, …, g_{n} =t_{n}) ∈ Tm^{σ_{i}→τ_{i}}[Γ]

The operational sematics of course is extended by the following rules (we abbreviate g_{1} =t_{1}, …, g_{n} =t_{n} to g⃗ =t⃗):

(oprec_{i}^{n})

\overline{for all n, 1 ≤ i ≤ n.}
⟨rec_{i}^{n}(g⃗ =t⃗); e⟩ ⇓ ⟨rec_{i}^{n}(g⃗ =t⃗); e⟩

(opappvr_{i}^{n}) ⟨t_{i}; e, g_{1} = rec_{1}^{n}(g⃗ =t⃗), …, g_{n} = rec_{n}^{n}(g⃗ =t⃗)⟩ ⇓ f f@u ⇓ v

⟨rec_{i}^{n}(g⃗ =t⃗); e⟩@u ⇓ v
for all n, 1 ≤ i ≤ n.

Now a recursive function rec_{i}^{n}(g⃗ = t⃗) is structurally recursive only if all of the simultaneous defined functions that are called directly or indirectly are structurally recursive as well. In [Abe98]we explain an algorithm to decide structural recursiveness for mutual recursive functions with perhaps multiple parameters in detail.

For our soundness proof nothing changes since we assume structural recursiveness.

8 Conclusion

In this work we have shown the soundness of our method to ensure a recursive function terminates on all inputs. We have confirmed our assumption that from structural recursiveness we can infer totality. Of course it would be desirable to extend our system further to polymorphic and dependent types.

But what is still missing is the syntactical aspect: It remains to show that indeed structurally recursive functions are the semantics of structurally recursive terms, i.e. terms that contain recursive calls only with smaller arguments w.r.t. a structural ordering on terms. (In section 6 we have defined the set SR^{τ} of terms, but their property of structural recursiveness has been ensured by means of semantics.) This syntactical check now is implemented in foetus, and it would be worthwhile formulating it as a proof, from which we could again extract a termination checker. (From the proof in this work we can extract nothing, since wellfoundedness proofs have no computational content.)

During the production of this work I encountered an application of it. I formulated parts of my system in LEGO and did some of the accessibility proofs by pattern matching. But these proofs are only sound if the patterns are total and structurally recursive. Unfortunately, LEGO contains no checker like foetus so far, and thus I could not be sure if my proofs were correct.

I think that in the area of machine checked proofs the pattern-matching-style proofs will replace elimination-style proofs, since once one has adjusted oneself to this new way of thinking, one can prove more intuitively. (It is like programming: no practically minded person would prefer a programming language with only primitive recursion to a full-featured functional programming language like SML or Haskell.) And thus termination checkers for the theorem provers will be implemented as Thorsten Altenkirch and I have done, and for example Catarina Coquand is doing for ALF at the University of Göteborg.

References

[Abe98]  Andreas Abel.  foetus – termination checker for sim-

ple functional programs. http://www.informatik.unimuenchen.de/˜ abel/foetus/, 1998.

[AGNvS94] Thorsten Altenkirch, Veronica Gaspes, Bengt Nordström, and Björn von Sydow. A user’s guide to ALF. Department of Computing Science, University of Göteborg/Chalmers, http://www.cs.chalmers.se/Cs/Research/Logic/alf/guide.html, May 1994.

[Alt93] Thorsten Altenkirch. A formalization of the strong normalization proof for system F in LEGO. volume 664 of Lecture Notes in Computer Science, pages 13–28. Springer Verlag, 1993.

[BG96] Jürgen Brauburger and Jürgen Giesl. Termination analysis for partial functions. In Proceedings of the Third International Static Analysis Symposium (SAS’96), Aachen, Germany, Lecture Notes in Computer Science 1145, Springer-Verlag, 1996.

[Coq92] Thierry Coquand. Pattern matching with dependent types. (to be updated), 1992.

[dB72] N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34:381–392, 1972.

[Der87] N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69–115, 1987.

[Gie97] Jürgen Giesl. Termination of nested and mutually recursive algorithms. Journal of Automated Reasoning 19: 1–29, 1997.

[Gir72] Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur. Thèse de Doctorat d’État, Université de Paris VII, 1972.

[HPF97] Paul Hudak, John Peterson, and Joseph Fasel. A Gentle Introduction to Haskell, Version 1.4. Yale Haskell Project, http://www.haskell.org/tutorial/, March 1997.

[LP92] Zhaohui Luo and Robert Pollack. Lego proof development system: User’s manual. Lfcs, Computer Science Department, University of Edinburgh, The King’s Buildings, Edinburgh EH9 3JZ, Scotland, May 1992. Updated version. See http://www.dcs.ed.ac.uk/home/lego.

[Mat98] Ralph Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. PhD thesis, Ludwig-Maximilian-University, 1998.

[Pau91] Lawrence C. Paulson. ML for the Working Programmer. Cambridge University Press, 1991.

[Ste95] J. Steinbach. Simplification orderings: History of results. Fundamenta Informaticae, 24:47–87, 1995.

[Tar55] Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.