Strong Normalization and Equi-(co)inductive Types

Andreas Abel^{⋆}

Department of Computer Science, University of Munich Oettingenstr.67, D-80538 München, Germany

                           abel@tcs.ifi.lmu.de

Abstract. A type system for the lambda-calculus enriched with recursive and corecursive functions over equi-inductive and -coinductive types is presented in which all well-typed programs are strongly normalizing. The choice of equi-inductive types, instead of the more common isoinductive types, influences both reduction rules and the strong normalization proof. By embedding iso- into equi-types, the latter ones are recognized as more fundamental. A model based on orthogonality is constructed where a semantical type corresponds to a set of observations, and soundness of the type system is proven.

1 Introduction

Theorem provers based on the Curry-Howard-Isomorphism, such as Agda, Coq, Epigram, or LEGO are built on dependent types and use inductive and coinductive types to formalize data structures, object languages, logics, judgments, derivations, etc. Proofs by induction or coinduction are represented as recursive or corecursive programs, where only total programs represent valid proofs. As a consequence, only total programs, which are defined on all well-typed inputs, are accepted, and totality is checked by some static analysis (in case of Coq), or ensured by construction (in case of Epigram), or simply assumed (in case of LEGO and the current version of Agda).

Hughes, Pareto, and Sabry [16] have put forth a totality check based on sized types, such that each well-typed program is already total. Designed originally for embedded systems it has become attractive for theorem provers because of several advantages: First of all, its soundness can be proven by an interpretation of types as sets of total programs, as noted by Giménez [13]. Since soundness proofs for dependent types are delicate, the clarity that sized types offer should not be underestimated. Secondly, checking termination through types integrates the features of advanced type systems, most notably higher-order functions, higher-order types, polymorphism, and subtyping, into the termination check

⋆ Research supported by the coordination action TYPES (510996) and thematic network Applied Semantics II (IST-2001-38957) of the European Union and the project Cover of the Swedish Foundation of Strategic Research (SSF).

without extra effort. Some advanced examples of what one can do with typebased termination, but not with syntactical, “term-based” termination checks, are given in other works of the author [4, 3, 2]. And last, type-based termination is just (a) sized inductive and coinductive types with subtyping induced by the sizes plus (b) typing rules for recursive and corecursive functions which ensure well-foundedness by checking that sizes are decreased in recursive instances. Due to this conceptual simplicity it is planned to replace the current term-based termination check in Coq by a type-based one; in recent works, sized types have been integrated with dependent types [9, 10].

Dependently typed languages, such as the languages of the theorem provers listed above, need to compare terms for equality during type-checking. In the presence of recursion, this equality test is necessarily incomplete.^{1} A common heuristics is to normalize the terms and compare them for syntactic equality. In general, these terms are open, i. e., have free variables, and normalization takes place in all term positions, also under binders. This complicates matters considerably: Although a function is total in a semantical sense and terminates on all closed terms under lazy evaluation, it will probably diverge on open terms under full evaluation.^{2} Hence, unfolding recursion has to be sensibly restricted during normalization. In related work [13, 8], inductive types are given by constructors, and a recursive function is only unfolded if its “recursive” argument, i. e., the argument that gets smaller in recursive calls, is a constructor.

We take a more foundational approach and consider a language, F_{ω}, without constructors. Programs of F_{ω} are just λ-terms over constants fix_{n}^{μ} and fix_{n}^{ν} which introduce recursive and corecursive functions with n leading “parametric”, i. e., non-recursive arguments. A recursive function fix_{n}^{μ} s t_{1} … t_{n} v with body s, parametric arguments t_{i} and recursive argument v is unfolded if v is a value, i. e., a λ-abstraction or an under-applied, meaning not fully applied, (co)recursive function. A corecursive function fix_{n}^{ν} s t_{1} … t_{n} is unfolded if it is in evaluation position, e. g., applied to some term. In this article, we prove that this strategy is strongly normalizing for programs which are accepted by the sized type system.

For now, F_{ω} does not feature dependent types—they are not essential to studying the operational semantics, but cause considerable complications in the normalization proof. However, F_{ω} has arbitrary-rank polymorphism, thus, elementary data types like unit type, product type and disjoint sum can be defined by the usual Church-encodings. Inductive types are not given by constructors; instead we have least fixed-point types μ^{a}F which denote the ath iteration of type constructor F. Semantically μ^{0}F is empty, μ^{a+1}F = F (μ^{a}F), and for limit ordinals λ, μ^{λ}F denotes the union of all μ^{a}F for a < λ. It may help to think of the size index a as an strict upper bound for the height of the inhabitants of μ^{a}F, viewed as trees. Dually, we have sized coinductive types ν^{a}F, and a denotes

1 And one would not expect that this test succeeds for the equation f (fix (g ∘ f)) =

fix (f ∘ g) given arbitrary (well-typed programs) f and g. 2 Consider the recursive zero-function zero x = match x with 0 ↦ 0 | y + 1 ↦ zero y. If

applying zero to a variable triggers unfolding of recursion, normalization of zero will diverge.

the minimum number of elementary destructions one can safely perform on an element of ν^{a}F, which is, in case of streams, the minimum number of elements one can read off this stream.

With sum and product types, common inductive types can be expressed as μ^{a}F for a suitable F; their constructors are then simply λ-terms. However, there is a design choice: equi-inductive types have μ^{a+1}F = F (μ^{a}F) as a type equation in the system; iso-inductive types stipulate that μ^{a+1}F and F (μ^{a}F) are only isomorphic, witnessed by a folding operation in : F (μ^{a}F) → μ^{a+1}F and an unfolding operation out : μ^{a+1}F → F (μ^{a}F). The iso-approach has been taken in previous work by the author [3] and seems to be more common [12, 6, 19, 7], since it has a simpler theory. We go the foundational path and choose the “equi” flavor, which has consequences for the operational semantics and the normalization proof: since there are less syntactical “clutches” to hold on, more structure has to be built in the semantics.

Overview. In Section 2 we present System F_{ω} with typing rules which only accept strongly normalizing functions. In Section 3 we motivate the reduction rules of F_{ω} which are affected by equi-(co)inductive types. By embedding iso- into equiinductive types in Section 4, we justify that equi-types are more fundamental than iso-types. We then proceed to develop a semantical notion of type, based on strong normalization and orthogonality (Section 5). Finally, we sketch the soundness proof for F_{ω} in Section 6 and discuss some related work in Section 7.

2 System F_{ω}

Like in System F^{ω}, expressions of F_{ω} are separated into three levels: kinds, type constructors, and terms (objects). Figure 1 summarizes the first two levels. In contrast to the standard presentation, we have a second base kind, ord, whose inhabitants are syntactic ordinals. Canonical ordinals are either s^{n}ı = s (s … (s ı)) (notation: ı + n), the nth successor of an ordinal variable ι, or ∞, the closure ordinal of all inductive and coinductive types of F_{ω}. In spite of the economic syntax, expressions of kind ord, which we will refer to as size expressions, semantically denote ordinals up to the ωth uncountable (see Sect. 5.3). We use the metavariable a to range over size expressions and the metavariable ı to range over size variables. The metavariable X ranges over type constructor variables, which includes size variables.

Another feature of F_{ω} are polarized kinds [27, 5, 1]. Function kinds are labeled with a polarity p that classifies the inhabiting type constructors as covariant (p = +), contravariant (p = −), or non-variant (p = ∘), the last meaning mixed or unknown variance. Inductive types are introduced using the type constructor constant

μ_{κ} : ord →^{+} (κ →^{+} κ) →^{+} κ.

We write μ_{κ} a F usually as μ_{κ}^{a}F and drop index kind κ if clear from the context. The underlying type constructor F : κ →^{+} κ must be covariant—otherwise

Syntactic categories.

p  ::= + | − | ∘  polarity
κ  ::= ∗ | ord | pκ → κ′  kind
κ_{∗}  ::= ∗ | pκ_{∗} → κ′_{∗}  pure kind
a, b, A, B, F, G ::= C | X | λX:κ. F | F G  (type) constructor
C  ::= → | ∀_{κ} | μ_{κ_{∗}} | ν_{κ_{∗}} | s | ∞ constructor constant
Δ ::= ⋄ | Δ, X:pκ polarized context

The signature Σ assigns kinds to constants (κ →^{p} κ′ means pκ → κ′).

→ : ∗ →^{−} ∗ →^{+} ∗  function space
∀_{κ} : (κ →^{∘} ∗) →^{+} ∗  quantification
μ_{κ_{∗}} : ord →^{+} (κ_{∗} →^{+} κ_{∗}) →^{+} κ_{∗}  inductive constructors
ν_{κ_{∗}} : ord →^{−} (κ_{∗} →^{+} κ_{∗}) →^{+} κ_{∗}  coinductive constructors
s : ord →^{+} ord  successor of ordinal
∞ : ord  infinity ordinal

Notation.

∇ for μ or ν
∇^{a} for ∇a
∀X:κ. A for ∀_{κ}(λX:κ. A)
∀XA for ∀X:κ. A
λXF for λX:κ. F

Ordering and composition of polarities.

p ≤ p ∘ ≤ p +p = p −− = + ∘p = ∘ pp′ = p′p

Inverse application of a polarity to a context.

\begin{aligned}p^{−1}⋄ & = & ⋄ \\ +^{−1}Δ & = & Δ \\ −^{−1}(Δ, X:pκ) & = & (−^{−1}Δ), X:(−p)κ \end{aligned}  \begin{aligned}∘^{−1}(Δ, X:∘κ) & = & (∘^{−1}Δ), X:∘κ \\ ∘^{−1}(Δ, X:+κ) & = & ∘^{−1}Δ \\ ∘^{−1}(Δ, X:−κ) & = & ∘^{−1}Δ \end{aligned}

Kinding Δ ⊢ F : κ.

kind-c \frac{C:κ ∈ Σ}{Δ ⊢ C : κ}  kind-var \frac{X:pκ ∈ Δ  p ≤ +}{Δ ⊢ X : κ}
kind-abs \frac{Δ, X:pκ ⊢ F : κ′}{Δ ⊢ λX:κ. F : pκ → κ′}  kind-app \frac{Δ ⊢ F : pκ → κ′  p^{−1}Δ ⊢ G : κ}{Δ ⊢ F G : κ′}

Fig. 1. F_{ω}: Kinds and constructors.

divergence is possible even without recursion (Mendler [21])—and κ must be a pure kind, i. e., not mention ord. The last condition seems necessary to define a uniform closure ordinal for all inductive types, meaning an ordinal ∞ such that μ^{∞}F = F (μ^{∞}F). Inductive types are covariant in their size argument; the subtyping chain μ^{a}F ≤ μ^{a+1}F ≤ μ^{a+2}F ≤ ⋯ ≤ μ^{∞}F holds. Dually, coinductive types, which are introduced by the constant

ν_{κ} : ord →^{−} (κ →^{+} κ) →^{+} κ,

are contravariant, and we have the chain ν^{∞}F ≤ ⋯ ≤ ν^{a+2}F ≤ ν^{a+1}F ≤ ν^{a}F. Type constructors are identified modulo βη and the laws s ∞ = ∞ and ∇^{a+1}F = F (∇^{a}F), where ∇ is a placeholder for μ or ν, here and in the following. Type constructor equality is kinded and given by the judgement Δ ⊢ F = F′ : κ for a kinding context Δ. Exept β and η, we have the axioms Δ ⊢ s ∞ = ∞ : ord and Δ ⊢ ∇_{κ}^{sa}F = F (∇_{κ}^{a}F) : κ for wellkinded F and a : ord. Similarly, we have kinded higher-order subtyping Δ ⊢ F ≤ F′ : κ induced by Δ ⊢ a ≤ s a : ord and Δ ⊢ a ≤ ∞ : ord. Due to space restrictions, the rules have to be omitted, please find them in the author’s thesis [2, Sect. 2.2].

Figure 2 displays terms and typing rules of F_{ω}. Besides λ-terms, there are constants fix_{n}^{μ} to introduce functions that are recursive in the n + 1st argument, and constants fix_{n}^{ν} to introduce corecursive functions with n arguments. The type A(ı) of a recursive function introduced by fix_{n}^{μ} must be of the shape

∀X. A_{1} → ⋯ → A_{n} → μ^{ı}F^{0} G^{0} → ⋯ → μ^{ı}F^{m} G^{m} → C,

where the A_{i} are contravariant in the size index ı, C is covariant, and the F^{j} and G^{j} do not mention ı. This criterion is written as A fix_{n}^{μ}-adm. (More precisely, a function of this type is simultaneously recursive in the arguments n + 1 to n + m + 1, but we are only interested in the first recursive argument.) Note that if the variance conditions were ignored, non-terminating functions would be accepted [3]. The type of a corecursive function fix_{n}^{ν} s with n arguments has to be of the form

∀X. A_{1} → ⋯ → A_{n} → ν^{ı}F G

where the A_{i} are again contravariant in ı and F and G do not mention ı (criterion A fix_{n}^{ν}-adm).

Basic data types like unit, product, and sum can be added to the system, but we define them impredicatively (see Figure 2) since minimality of the system is a stronger concern in this work than efficiency. Some examples for sized types are:

Nat : ord →^{+} ∗
Nat := λı. μ^{ı}λX. 1 + X
List : ord →^{+} ∗ →^{+} ∗
List := λıλA. μ^{ı}λX. 1 + A × X

Tree : ord →^{+} ∗ →^{−} ∗ →^{+} ∗
Tree := λıλBλA. μ^{ı}λX. 1 + A × (B → X)
Stream : ord →^{−} ∗ →^{+} ∗
Stream := λıλA. ν^{ı}λX. A × X

A rich collection of examples is provided in the author’s thesis [2, Sect. 3.2].

Syntactic categories.

Var ∋ x  variable
Tm ∋ r, s, t ::= x | λxt | r s | fix_{n}^{μ} | fix_{n}^{ν}  term (n ∈ ℕ)
Val ∋ v ::= λxt | fix_{n}^{∇} | fix_{n}^{∇}s t (where |t| ≤ n) value (∇ ∈ {μ, ν})
Eframe ∋ e(_) ::= _s | fix_{n}^{μ} s t_{1..n} _evaluation frame
Ecxt ∋ E ::= Id | E ∘ e [Id(r) = r, (E ∘ e)(r) = E(e(r))] evaluation context
Cxt ∋ Γ ::= ⋄ | Γ, x:A | Γ, X:pκ  typing context

Well-formed typing contexts.

cxt-empty \overline{⋄ cxt} cxt-tyvar \frac{Γ cxt}{Γ, X:∘κ cxt} cxt-var \frac{Γ cxt  Γ ⊢ A : ∗}{Γ, x:A cxt}

Typing Γ ⊢ t : A.

ty-var \frac{(x:A) ∈ Γ  Γ cxt}{Γ ⊢ x : A}  ty-abs \frac{Γ, x:A ⊢ t : B}{Γ ⊢ λxt : A → B}
ty-app \frac{Γ ⊢ r : A → B  Γ ⊢ s : A}{Γ ⊢ r s : B}  ty-sub \frac{Γ ⊢ t : A  Γ ⊢ A ≤ B : ∗}{Γ ⊢ t : B}
ty-gen \frac{Γ, X:∘κ ⊢ t : F X}{Γ ⊢ t : ∀_{κ}F}  ty-inst \frac{Γ ⊢ t : ∀_{κ} F  Γ ⊢ G : κ}{Γ ⊢ t : F G}
ty-rec \frac{Γ ⊢ A : ord → ∗  A fix_{n}^{∇}-adm  Γ ⊢ a : ord}{Γ ⊢ fix_{n}^{∇} : (∀ı:ord. A ı → A (ı + 1)) → A a} ∇ ∈ \{μ, ν\}

Impredicative definition of unit, product, and sum type.

\begin{aligned}1 & := & ∀C. C → C & : & ∗ \\ × & := & λAλB∀C. (A → B → C) → C & : & ∗ →^{+} ∗ →^{+} ∗ \\ + & := & λAλB∀C. (A → C) → (B → C) → C & : & ∗ →^{+} ∗ →^{+} ∗ \end{aligned}

Reduction t ⟶ t′: Closure of the following axioms under all term constructors:

(λxt) s  ⟶ [s/x]t
fix_{n}^{μ}s t_{1..n} v ⟶ s (fix_{n}^{μ}s) t_{1..n} v  if v ≠ fix_{n′}^{ν}s′ t_{1..n′}
e (fix_{n}^{ν}s t_{1..n}) ⟶ e (s (fix_{n}^{ν}s) t_{1..n}) if e ≠ fix_{n′}^{μ}s′ t_{1..n′} _

Fig. 2. F_{ω}: Terms and type assignment.

3 Operational semantics

In this section, the reduction rules for recursive and corecursive functions are developed. It is clear that unrestricted unfolding of fixed points fix s ⟶ s (fix s) leads immediately to divergence. In the literature on type-based termination with iso-inductive types one finds the sound reduction rule fix_{n}^{μ}s t_{1..n} (in r) ⟶ s (fix_{n}^{μ}s) t_{1..n} (in r), which requires the recursive argument to be a canonical inhabitant of the inductive type. Since the canonical inhabitants for equi-inductive types can be of any shape, we liberalize this rule to

fix_{n}^{μ}s t_{1..n} v ⟶ s (fix_{n}^{μ}s) t_{1..n} v,  (1)

where v is a value; in our case a λ-abstraction, or an under-applied (co)recursive function.

Elements of a coinductive type should be delayed by default, they should only be evaluated when they are observed, or forced, i. e., when they are surrounded by a non-empty evaluation context e. A candidate for a reduction rule is

e (fix_{n}^{ν}s t_{1..n}) ⟶ e (s (fix_{n}^{ν}s) t_{1..n}).  (2)

It is easy to find well-typed diverging terms if less than n arguments t_{1..n} are required before the fixed-point can be unfolded.

Evaluation contexts e(_) are either applications _s or recursive functions fix_{n}^{μ} s t_{1..n} _. The second form is necessary because, before reduction (1) can be performed, the recursive argument has to be evaluated, hence, must be in evaluation position. However, we run into problems if a corecursive value is in a recursive evaluation context, e. g., fix_{0}^{μ} (λxx) (fix_{0}^{ν} (λzy)). Such a term can be well-typed^{3} if we use types like μλX. νλY. A. Depending on which fixedpoint we unfold we get completely different behavior: the recursion fix_{0}^{μ} can be unfolded ad infinitum, the term diverges. If we unfold the corecursion fix_{0}^{ν}, we arrive at fix_{0}^{μ} (λxx) y, which is blocked. Another bad example is fix_{0}^{μ}s (fix_{0}^{ν}s) with s = λzλxx. If we unfold recursion, we arrive at the normal form fix_{0}^{ν}s. Otherwise, if we first unfold corecursion, we obtain fix_{0}^{μ}s (λxx) which has normal form λxx; the calculus is not locally confluent.

In this article, we restore acceptable behavior in the following way: A corecursive value inside a recursive evaluation context should block reduction, terms like fix_{0}^{μ} s (fix_{0}^{ν} s′) should be considered neutral, like variables. The drawback of this decision is that types like ν^{ı}λX. List^{ȷ} X (non-wellfounded, but finitely branching trees) are not well-supported by the system: Applying the List-length function to such a tree, like fix_{0}^{ν}λx.singletonList(x), will not reduce. This seems to be a high price to pay for equi-(co)inductive types; in the iso-version, such problems do not arise. However, as we will see in the next section, even with these blocked terms, the equi-version is able to completely simulate reduction of the iso-version, so we have not lost anything in comparison with the iso-version, but we can gain something by improving the current reduction strategy in the equi-version.

3 Note that fix_{0}^{μ}λxx : (μ^{a}λXX) → C and fix_{0}^{ν}λxx : ν^{a}λXX.

4 Embedding Iso- into Equi-(co)inductive Types

Why are we so interested in equi-inductive types, if they cause us trouble? Because they are the more primitive notion. Strong normalization for iso-inductive types can be directly obtained from the result for equi-inductive types, since there exists a trivial type and reduction preserving embedding. Let Delay_{κ} be defined by recursion on the pure kind κ as follows:

Delay_{∗}  (A) := 1 → A
Delay_{pκ→κ′} (F) := λX:κ. Delay_{κ′}(F X)

Then we can define iso-inductive \overline{μ}_{κ} and iso-coinductive \overline{ν}_{κ} types in F_{ω} as follows:

\overline{∇}_{κ} := λıλF:κ. ∇_{κ}^{ı} Delay_{κ}(F)
in^{∇}(t) := λzt where z ∉ FV(t)

out^{∇}(r) := r ()

Now in^{μ}(t) is a non-corecursive value for each term t, and out^{ν}(_) is an applicative evaluation context, so we obtain in F_{ω} the reductions typical for iso-types:

fix_{n}^{μ}s t_{1..n} (in^{μ}(r)) ⟶ s (fix_{n}^{μ}s) t_{1..n} (in^{μ}(r))
out^{ν}(fix_{n}^{ν}s t_{1..n}) ⟶ out^{ν}(s (fix_{n}^{ν}s) t_{1..n}).

The reverse embedding, however, is not trivial. Since in the equi-system, folding and unfolding of inductive types can happen deep inside a type, equi-programs are not typable in the iso-system without major modifications. Only typing derivations of the equi-system can be translated into typing derivations of the isosystem. Thus, we consider equi-systems as more fundamental than iso-systems.

5 Semantical Types

A strongly normalizing term t ∈ SN is a term for which each reduction sequence ends in a value or a neutral term. A neutral term has either a variable in head position, or, in our case, a blocking fix^{μ}-fix^{ν} combination. We define SN inductively, extending previous works [15, 28, 17] by rules for (co)recursive terms (see Figure 3). Rule sn-roll is sound, but not strictly necessary; however, it simplifies the proof of extensionality (see lemma).

Safe reduction t ▷ t′ is a variant of weak head reduction which preserves strong normalization in both directions. In particular, SN is closed under safe expansion (rule sn-exp). This works because we require s ∈ SN in rule shr-β.

Lemma 1 (Properties of SN).

1. Extensionality: If r x ∈ SN then r ∈ SN.

2. Closure: If r ∈ SN and r ▷ r′ or r ◁ r′ then r′ ∈ SN.

3. Strong normalization: If r ∈ SN then there are no infinite reduction sequences r ⟶ r_{1} ⟶ r_{2} ⟶ . . ..

4. Weak head normalization: If r ∈ SN then r ▷ r′ and r′ ∈ SNe ∪ Val.

Strongly normalizing evaluation contexts E ∈ Scxt.

sc-id \overline{Id ∈ Scxt} sc-app \frac{E ∈ Scxt  s ∈ SN}{E ∘ (_s) ∈ Scxt} sc-rec \frac{E ∈ Scxt  s, t_{1..n} ∈ SN}{E ∘ (fix_{n}^{μ}s t_{1..n} _) ∈ Scxt}

Strongly normalizing neutral terms r ∈ SNe.

sne-var \frac{E ∈ Scxt}{E(x) ∈ SNe}  sne-fix^{μ}fix^{ν} \frac{E ∈ Scxt  s, t, s′, t′ ∈ SN}{E(fix_{n}^{μ}s t_{1..n} (fix_{n′}^{ν}s′ t′_{1..n′})) ∈ SNe}

Strongly normalizing terms t ∈ SN.

sn-sne \frac{r ∈ SNe}{r ∈ SN}  sn-abs \frac{t ∈ SN}{λxt ∈ SN}  sn-fix \frac{t ∈ SN}{fix_{n}^{∇}t ∈ SN} |t| ≤ n + 1
sn-exp \frac{r ▷ r′  r′ ∈ SN}{r ∈ SN}  sn-roll \frac{s (fix_{n}^{ν}s) t ∈ SN}{fix_{n}^{ν}s t ∈ SN} |t| ≤ n

Safe reduction t ▷ t′ (plus reflexivity and transitivity).

shr-β \frac{s ∈ SN}{E((λxt) s) ▷ E([s/x]t)}  shr-rec \frac{v ≠ fix_{n′}^{ν}s′ t′_{1..n′}}{E(fix_{n}^{μ}s t_{1..n} v) ▷ E(s (fix_{n}^{μ}s) t_{1..n} v)}
shr-corec \frac{e ≠ fix_{n′}^{μ}s′ t′_{1..n′} _}{E(e(fix_{n}^{ν}s t_{1..n})) ▷ E(e(s (fix_{n}^{ν}s) t_{1..n}))}

Fig. 3. Strongly normalizing terms.

Alternatively, one can take 3. as the defining property of SN and from this prove 1., 2., and the sn- and sne-rules in Figure 3. Property 4. holds then also, but only because there are no “junk terms” like 0 (λxx) in our language which block reduction but are neither neutral nor values.

In the remainder of this section, we prepare for the model construction for F_{ω} that will verify strong normalization. As usual, we interpret types as sets A of strongly normalizing terms, where A is closed under safe expansion. In the iso-case, we could interpret a coinductive type C := [[ν^{a+1}F]] as {r | out r ∈ [[F (ν^{a}F)]]}, or in words, as these terms r whose canonical observation out r is already well-behaved. A corecursive object, say fix_{0}^{ν}s can enter C by the safe expansion out (fix_{0}^{ν}s) ▷ out (s (fix_{0}^{ν}s)) provided that s (fix_{0}^{ν}s) ∈ C already. In the equi-case, however, a canonical observation is not available, we have no choice than to set the interpretation of C to the semantical type [[F (ν^{a}F)]]. How can now fix_{0}^{ν}s enter C? The solution is that each semantical type A is characterized by a set of evaluation contexts, E, such that t ∈ A iff E(t) ∈ SN for all E ∈ E. This characterization automatically ensures that A is closed under safe reduction and expansion. Now fix_{0}^{ν} s enters C through the safe expansion E(fix_{0}^{ν}s)▷E(s (fix_{0}^{ν}s)). Formally, this will be proven in Lemma 5. In the following, we give constructions and properties of semantical types. Due to lack of space, the presentation is rather dense, more details can be found in the author’s thesis [2].

5.1 Orthogonality

We say that term t is orthogonal to evaluation context E,

t ⊥ E :⟺ E(t) ∈ SN.

We could also say t behaves well in E. A semantical type A is the set of terms which behave well in all E ∈ E, where E is some set of strongly normalizing evaluation contexts. The space of semantical types is called SAT.

E^{⊥}  := {t | t ⊥ E for all E ∈ E}
A^{⊥}  := {E | t ⊥ E for all t ∈ A}
SAT  := {E^{⊥} | {Id} ⊆ E ⊆ Scxt}  saturated sets
N  := Scxt^{⊥} ⊃ SNe  neutral terms
S  := {Id}^{⊥}  s.n. terms
\overline{A}  := A^{⊥⊥}  closure
A → E^{⊥} := {Id, E ∘ (_s) | E ∈ E, s ∈ A}^{⊥}  function space
⋂ 𝔄  := ⋂ 𝔄 for 𝔄 ⊆ SAT  infimum
⋃ 𝔄  := \overline{⋃ 𝔄} for 𝔄 ⊆ SAT  supremum

The greatest semantical type is S = SN; the least semantical type N contains all terms which behave well in all good contexts, including the variables and even more, all safe expansions of strongly normalizing neutral terms. But due to rule sne-fix^{μ}fix^{ν}, also some corecursive values inhabit N, e. g., fix_{0}^{ν}λzy.

Lemma 2 (Properties of saturated sets).

1. Galois connection: A^{⊥} ⊇ E ⟺ A ⊆ E^{⊥}. This implies A ⊆ A^{⊥⊥}, A ⊆ B ⟹ A^{⊥} ⊇ B^{⊥}, and A^{⊥⊥⊥} = A^{⊥}, and the same laws for Es.

2. Biorthogonal closure: If A ⊆ S then {Id} ⊆ A^{⊥} ⊆ Scxt and A^{⊥⊥} ∈ SAT.

3. De Morgan 1: ⋂_{i∈I} E_{i}^{⊥} = (⋃_{i∈I} E_{i})^{⊥}.

4. De Morgan 2: ⋃_{i∈I} E_{i}^{⊥} ⊆ (⋂_{i∈I} E_{i})^{⊥}.

5. Reduction/expansion closure: If t ∈ E^{⊥} and t ▷ t′ or t ◁ t′ then t′ ∈ E^{⊥}.

6. Normalization: If t ∈ A ∈ SAT then either t ∈ N or t ▷ v.

7. Function space: If A ⊆ S and B ∈ SAT then A → B ∈ SAT.

8. Infimum and supremum: If 𝔄 ⊆ SAT then ⋂ 𝔄 ∈ SAT and ⋃ 𝔄 ∈ SAT.

In general, the inclusion in law De Morgan 2 is strict; thus, taking the orthogonal seems to be an intuitionistic rather than a classical negation.

Lemma 3 (Abstraction and application). Let B ∈ SAT.

1. If Var ⊆ A and r s, [s/x]t ∈ B for all s ∈ A, then r, λxt ∈ A → B.

2. If r ∈ A → B and s ∈ A then r s ∈ B.

The proof of 1. uses extensionality (Lemma 1) to show r ⊥ Id from r x ∈ B.

5.2 Recursion and corecursion, semantically

In this section, we characterize admissible types for recursion and corecursion in our semantics and prove semantical soundness of type-based termination. Let O denote some initial segment of the set-theoretic ordinals.

The semantic type family A ∈ O → SAT is admissible for recursion on the n + 1st argument if

adm-μ-shape there is an index set K and there are

B_{1}, …, B_{n}, I, C ∈ K × O → SAT such that for all α ∈ O,

A(α) = ⋂_{k∈K}(B_{1..n}(k, α) → I(k, α) → C(k, α)),

adm-μ-start I(k, 0) ⊆ N for all k ∈ K, and
adm-μ-limit  ⋂_{α<λ} A(α) ⊆ A(λ) for all limits λ ∈ O \ {0}.

In adm-μ-shape, the intersection ⋂ stands for a quantification over types, the B_{i} for non-recursive arguments, the I for the recursive argument of inductive type, and C for the result type.

Lemma 4 (Recursion is a function). Let A ∈ O → SAT be admissible for recursion on the n + 1st argument. If s ∈ A(α) → A(α + 1) for all α + 1 ∈ O, then fix_{n}^{μ}s ∈ A(β) for all β ∈ O.

Proof. By transfinite induction on β ∈ O [2, Lemma 3.32].

The soundness of corecursion makes crucial use of our definition of a semantical type by a set of evaluation contexts. It also requires that coinductive types denote the whole term universe S in the 0th iteration (adm-ν-start).

The semantic type family A ∈ O → SAT is admissible for corecursion with n arguments if

adm-ν-shape for some index set K and B_{1..n}, C ∈ K × O → SAT,

A(α) = ⋂_{k∈K}(B_{1..n}(k, α) → C(k, α)) for all α ∈ O,

adm-ν-start S ⊆ C(k, 0) for all k ∈ K, and
adm-ν-limit  ⋂_{α<λ} A(α) ⊆ A(λ) for all limits λ ∈ O \ {0}.

Lemma 5 (Corecursion is a function). Let A ∈ O → SAT be admissible for corecursion with n arguments. If s ∈ A(α) → A(α + 1) for all α + 1 ∈ O, then fix_{n}^{ν}s ∈ A(β) for all β ∈ O.

Proof. By transfinite induction on β ∈ O [2, Lemma 3.37].

5.3 Lattices and Iteration

The saturated sets form a complete lattice [[∗]] = SAT with least element ⊥^{∗} := N and greatest element ⊤^{∗} := S. It is ordered by inclusion ⊑^{∗} := ⊆ and has arbitrary infima inf^{∗} := ⋂ and suprema sup^{∗} := ⋃. Let [[ord]] := [0; ⊤^{ord}] be an initial segment of the set-theoretic ordinals which is closed under suprema, such that all (co)inductive types reach their fixpoint at ordinal ⊤^{ord}. An upper bound for the ⊤^{ord} is the ωth uncountable [3], although the true closure ordinal is probably much smaller, and it would be interesting to find out more about it. With the usual ordering on ordinals, [[ord]] constitutes a complete lattice as well. Function kinds [[∘κ → κ′]] := [[κ]] → [[κ′]] are interpreted as set-theoretic function spaces; a covariant function kind denotes just the monotonic functions and a contravariant kind the antitonic ones. For all function kinds, ordering is defined pointwise: F ⊑^{pκ→κ′} F′ :⟺ F(G) ⊑^{κ′} F′(G) for all G ∈ [[κ]]. Similarly, ⊥^{pκ→κ′}(G) := ⊥^{κ′} is defined pointwise, and so are ⊤^{pκ→κ′}, inf^{pκ→κ′}, and sup^{pκ→κ′}.

For monotone F ∈ [[κ]] →^{+} [[κ]] we define iteration from below and above as usual:

\begin{aligned}μ^{0}F & = & ⊥^{κ} \\ μ^{α+1}F & = & F(μ^{α}F) \\ μ^{λ}F & = & sup_{α<λ}^{κ} μ^{α}F \end{aligned}  \begin{aligned}ν^{0}F & = & ⊤^{κ} \\ ν^{α+1}F & = & F(ν^{α}F) \\ ν^{λ}F & = & inf_{α<λ}^{κ} ν^{α}F \end{aligned}

For fixed F, μ^{α}F is monotonic in α and ν^{α}F is antitonic in α.

6 Soundness

For a constructor constant C:κ, the semantics [[C]] ∈ [[κ]] is defined as follows:

[[→]](A, B ∈ [[∗]]) := A → B_{[[μ_{κ}]](α)(F ∈ [[κ]] →^{+} [[κ]]) := μ^{α}F}_{[[ν_{κ}]](α)(F ∈ [[κ]] →^{+} [[κ]]) := ν^{α}F}_{[[∀_{κ}]](F ∈ [[κ]] → [[∗]]) := ⋂_{G∈[[κ]]} F(G)} [[∞]]  := ⊤^{ord}

[[s]](⊤^{ord})  := ⊤^{ord}
[[s]](α < ⊤^{ord}) := α + 1

We extend this semantics to constructors F in the usual way.

Let θ be a partial mapping from constructor variables to sets. We say θ ∈ [[Δ]] if θ(X) ∈ [[κ]] for all (X : pκ) ∈ Δ. A partial order on valuations is defined by θ ⊑ θ′ ∈ [[Δ]] :⟺ θ(X) ⊑^{p} θ′(X) ∈ [[κ]] for all (X: pκ) ∈ Δ. Herein, we have used ⊑^{−} for ⊒, and ⊑^{∘} for =, and ⊑^{+} as synonym for ⊑.

Theorem 1 (Soundness of type-related judgements). Let θ, θ′ ∈ [[Δ]].

1. If Δ ⊢ F : κ then [[F]]_{θ} ∈ [[κ]].

2. If Δ ⊢ F = F′ : κ and θ ⊑ θ′ ∈ [[Δ]], then [[F]]_{θ} ⊑ [[F′]]_{θ′} ∈ [[κ]].

3. If Δ ⊢ F ≤ F′ : κ and θ ⊑ θ′ ∈ [[Δ]], then [[F]]_{θ} ⊑ [[F′]]_{θ′} ∈ [[κ]].

4. If Δ ⊢ A fix_{n}^{μ}-adm, then [[A]]_{θ} is admissible for recursion on the n + 1st arg.

5. If Δ ⊢ A fix_{n}^{ν}-adm, then [[A]]_{θ} is admissible for corecursion with n arguments.

We extend valuations θ to term variables and say θ ∈ [[Γ]] if θ(X) ∈ [[κ]] for all (X : pκ) ∈ Γ and θ(x) ∈ [[A]]_{θ} for all (x : A) ∈ Γ. Let ⦇t⦈_{θ} denote the capture-avoiding substitution of θ(x) for x in t, simultaneously for all x ∈ FV(t).

Theorem 2 (Soundness of F_{ω}). If Γ ⊢ t : A and θ ∈ [[Γ]] then ⦇t⦈_{θ} ∈ [[A]]_{θ}.

The theorem is proved by induction on the typing derivation [2, Thm. 3.49]. As a consequence, taking θ(x) = x for all (x: A) ∈ Γ and θ(X) = ⊤^{κ} for all (X:pκ) ∈ Γ, we get t = ⦇t⦈_{θ} ∈ [[A]]_{θ} ⊆ SN.

7 Conclusions

We have presented a type system for termination of recursive functions over equi-inductive and -coinductive types and shown its soundness by a model based on orthogonality. All reductions of the corresponding iso-system are simulated, hence, termination of the iso-system follows as a special case.

Parigot [24] already introduces equi-inductive types to model efficient recursion schemes in system AF_{2}, second order functional arithmetic. Raffalli [26] considers also equi-coinductive types. However, recursion is limited to Mendlerstyle (co)iteration [22], preventing a direct implementation of primitive recursive programs such as factorial. Iteration is but a special case of the recursion scheme of the present work, which generalizes course-of-value recursion.

Orthogonality has been introduced by Girard for the semantics of linear logic; it pops up again in Ludics [14]. Parigot has implicitly used orthogonality to prove strong normalization of second-order classical natural deduction [25]. His work has been extended by Matthes to positive fixed-point types [20]. Lindley and Stark [18] use orthogonality to show strong normalization of the monadic lambda-calculus and give credit to Pitts. Vouillon and Melliès [30] model recursive types with orthogonality, Vouillon [29] bases subtyping rules for union types on orthogonality.

Related works on type-based termination include: Hughes, Pareto, and Sabry [16], who treat first-order inductive and coinductive types that close at iteration ω. Their system is also equi in spirit [23, Ch. 3.10], however, they do not give reduction rules but construct a denotational model. Barthe et al. [8] prove strong normalization for recursive functions over sized inductive types of kind ∗. Although there are no explicit (un)folding operations in and out, the only way to generate inductive data is via constructors for labeled sums, which is crucially in the reduction rule for recursion. Thus, the system is iso in disguise, in is merged into the constructors, and out into case distinction. Blanqui [10] considers typebased termination for his Calculus of Algebraic Constructions—iso-inductive in spirit—which subsumes the Calculus of Inductive Constructions (CIC). Barthe, Gregoire, and Pastawski [9] have extended type-based termination to the CIC. Xi [31] bases termination on dependent types, albeit only dependencies on integer expressions, which gives him a great flexibility in termination measures. Since in his system a typing context can become unsatisfiable, he only shows call-by-value normalization of closed programs. Blanqui and Riba [11] manage to avoid unsatisfiable contexts, and thus, recover strong normalization.

In our treatment of equi-(co)inductive types, it is a bit unsatisfactory that terms like fix_{0}^{μ}s (fix_{0}^{ν} s′) are blocked. One could think of allowing both unfoldings, arriving at a non-confluent calculus. The techniques described in this paper are then no longer sufficient to prove strong normalization, but maybe methods used for normalization of classical logic could be employed.

Acknowledgments. Thanks to my supervisor, Martin Hofmann, and to Ralph Matthes for supporting my thesis work. Thanks to Lennart Beringer for proof reading and to the anonymous referees for their insightful and helpful comments.

Jérôme Vouillon’s excellent article on semantics of union types [29] inspired me to build a model based on orthogonality. Thanks to Frédéric Blanqui and Colin Riba for their invitation to LORIA in February 2007 and for discussions which deepened my understanding of orthogonality, strong normalization, and equiinductive types.

References

1. Abel, A.: Polarized subtyping for sized types. In: Grigoriev, D., Harrison, J., Hirsch, E. A., eds., Proc. of the 1st Int. Computer Science Symposium in Russia, CSR 2006, volume 3967 of Lect. Notes in Comput. Sci. Springer-Verlag (2006), 381–392

2. Abel, A.: A Polymorphic Lambda-Calculus with Sized Higher-Order Types. Ph.D. thesis, Ludwig-Maximilians-Universität München (2006)

3. Abel, A.: Semi-continuous sized types and termination. In: Ésik, Z., ed., Computer Science Logic, 20th Int. Workshop, CSL 2006, 15th Annual Conf. of the EACSL, volume 4207 of Lect. Notes in Comput. Sci. Springer-Verlag (2006), 72–88

4. Abel, A.: Towards generic programming with sized types. In: Uustalu, T., ed., Proc. of the 8th Int. Conf. on Mathematics of Program Construction, MPC ’06, volume 4014 of Lect. Notes in Comput. Sci. Springer-Verlag (2006), 10–28

5. Abel, A., Matthes, R.: Fixed points of type constructors and primitive recursion. In: Marcinkowski, J., Tarlecki, A., eds., Computer Science Logic, 18th Int. Workshop, CSL 2004, 13th Annual Conf. of the EACSL, volume 3210 of Lect. Notes in Comput. Sci. Springer-Verlag (2004), 190–204

6. Altenkirch, T.: Constructions, Inductive Types and Strong Normalization. Ph.D. thesis, University of Edinburgh (1993)

7. Altenkirch, T.: Logical relations and inductive/coinductive types. In: Gottlob, G., Grandjean, E., Seyr, K., eds., Computer Science Logic, 12th Int. Workshop, CSL ’99, 7th Annual Conf. of the EACSL. Lect. Notes in Comput. Sci., Springer-Verlag (1999), 343–354

8. Barthe, G., Frade, M. J., Giménez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Math. Struct. in Comput. Sci. 14 (2004) 1–45

9. Barthe, G., Grégoire, B., Pastawski, F.: CICˆ : Type-based termination of recursive definitions in the Calculus of Inductive Constructions. In: Hermann, M., Voronkov, A., eds., Proc. of the 13th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006, volume 4246 of Lect. Notes in Comput. Sci. Springer-Verlag (2006), 257–271

10. Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. In: van Oostrom, V., ed., Rewriting Techniques and Applications (RTA 2004), Aachen, Germany, volume 3091 of Lect. Notes in Comput. Sci. Springer-Verlag (2004), 24–39

11. Blanqui, F., Riba, C.: Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems. In: Hermann, M., Voronkov, A., eds., Proc. of the 13th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006, volume 4246 of Lect. Notes in Comput. Sci. Springer-Verlag (2006), 105–119

12. Geuvers, H.: Inductive and coinductive types with iteration and recursion. In: Nordström, B., Pettersson, K., Plotkin, G., eds., Types for Proofs and Programs (TYPES’92), Båstad, Sweden (1992), 193–217 13. Giménez, E.: Structural recursive definitions in type theory. In: Larsen, K. G.,

Skyum, S., Winskel, G., eds., Int. Colloquium on Automata, Languages and Programming (ICALP’98), Aalborg, Denmark, volume 1443 of Lect. Notes in Comput. Sci. Springer-Verlag (1998), 397–408

14. Girard, J.-Y.: Locus solum: From the rules of logic to the logic of rules. Math. Struct. in Comput. Sci. 11 (2001) 301–506

15. Goguen, H.: Typed operational semantics. In: Deziani-Ciancaglini, M., Plotkin, G. D., eds., Proc. of the 2nd Int. Conf. on Typed Lambda Calculi and Applications, TLCA ’95, volume 902 of Lect. Notes in Comput. Sci. Springer-Verlag (1995), 186– 200

16. Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Proc. of the 23rd ACM Symp. on Principles of Programming Languages, POPL’96 (1996), 410–423

17. Joachimski, F., Matthes, R.: Short proofs of normalization. Archive of Mathematical Logic 42 (2003) 59–87

18. Lindley, S., Stark, I.: Reducibility and ⊤⊤-lifting for computation types. In: Urzyczyn, P., ed., Proc. of the 7th Int. Conf. on Typed Lambda Calculi and Applications, TLCA 2005, volume 3461 of Lect. Notes in Comput. Sci. Springer-Verlag (2005)

19. Matthes, R.: Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Ph.D. thesis, Ludwig-Maximilians-University (1998)

20. Matthes, R.: Non-strictly positive fixed-points for classical natural deduction. Ann. Pure Appl. Logic 133 (2005) 205–230

21. Mendler, N. P.: Recursive types and type constraints in second-order lambda calculus. In: Proc. of the 2nd IEEE Symp. on Logic in Computer Science (LICS’87). IEEE Computer Soc. Press (1987), 30–36

22. Mendler, N. P.: Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic 51 (1991) 159–172

23. Pareto, L.: Types for Crash Prevention. Ph.D. thesis, Chalmers University of Technology (2000)

24. Parigot, M.: Recursive programming with proofs. Theor. Comput. Sci. 94 (1992) 335–356

25. Parigot, M.: Proofs of strong normalization for second order classical natural deduction. The Journal of Symbolic Logic 62 (1997) 1461–1479

26. Raffalli, C.: Data types, infinity and equality in system af_{2}. In: Börger, E., Gurevich, Y., Meinke, K., eds., Proc. of the 7th Wksh. on Computer Science Logic, CSL ’93, volume 832 of Lect. Notes in Comput. Sci. Springer-Verlag (1994), 280–294

27. Steffen, M.: Polarized Higher-Order Subtyping. Ph.D. thesis, Technische Fakultät, Universität Erlangen (1998)

28. van Raamsdonk, F., Severi, P., Sørensen, M. H., Xi, H.: Perpetual reductions in lambda calculus. Inf. Comput. 149 (1999) 173–225

29. Vouillon, J.: Subtyping union types. In: Marcinkowski, J., Tarlecki, A., eds., Computer Science Logic, 18th Int. Workshop, CSL 2004, 13th Annual Conf. of the EACSL, volume 3210 of Lect. Notes in Comput. Sci. Springer-Verlag (2004), 415– 429

30. Vouillon, J., Melliès, P.-A.: Semantic types: A fresh look at the ideal model for types. In: Jones, N. D., Leroy, X., eds., Proc. of the 31st ACM Symp. on Principles of Programming Languages, POPL 2004. ACM Press (2004), 52–63

31. Xi, H.: Dependent types for program termination verification. J. Higher-Order and Symb. Comput. 15 (2002) 91–131