Termination and Productivity Checking with Continuous Types

Andreas Abel ^{⋆}

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

                     abel@informatik.uni-muenchen.de

Abstract. We analyze the interpretation of inductive and coinductive types as sets of strongly normalizing terms and isolate classes of types with certain continuity properties. Our result enables us to relax some side conditions on the shape of recursive definitions which are accepted by the type-based termination calculus of Barthe, Frade, Giménez, Pinto and Uustalu, thus enlarging its expressivity.

1 Introduction and Related Work

Interactive theorem provers like Coq [13], LEGO [20] and Twelf [18] support proofs by induction on finite-depth (inductive) structures (like natural numbers, lists, infinitely branching trees) and infinite-depth (coinductive) structures (like streams, processes, trees with infinite paths) in the form of recursive programs. However, these programs constitute valid proofs only if they denote total functions. In the last decade, considerable effort has been put on the development of means to define total functions in the type theories of the abovementioned theorem provers.

The first solution was to restrict programs to specific recursion schemes like iteration or primitive recursion (like natrec). Since these schemes come with complicated reduction behavior, they were inconvenient to use and so the search started how to incorporate the simpler general recursion (fix resp. letrec) known from functional programming. Programs using fix are in general not terminating (resp. productive, for the case of infinite structures), hence could denote partial or undefined functions. Thus, the use of fix has to be restricted in some manner.

Static analysis of the program. The first approach is to check the code of a recursive program to make sure some argument is decreasing in each recursive call (cf. Abel and Altenkirch [1, 4], Pientka [19], Lee, Jones and Ben-Amram [14]). For programs defining infinite objects like streams, the recursive calls need to be guarded. Guardedness checks have been devised e.g. by Coquand [8], Telford and Turner [22] and Giménez [9].

⋆ Research supported by the Graduiertenkolleg Logik in der Informatik (PhD Program Logic in Computer Science) of the Deutsche Forschungsgemeinschaft (DFG). The author thanks Martin Hofmann and Ralph Matthes for helpful discussions.

pivot : int → ∀Y ≈ int list . Y → Y × Y pivot a [ ]^{Y 1} = ([ ]^{Y 1}, [ ]^{Y 1} ) pivot a (x :: xs^{Y})^{Y 1} = let (l^{Y}, r^{Y}) = pivot a xs in

if a > x then ((x :: l)^{Y 1}, r^{Y ≤Y 1} ) else (l^{Y ≤Y 1}, (x :: r)^{Y 1} )

qsapp : ∀Y ≈ int list . Y → int list → int list

qsapp [ ]^{Y 1} ys = ys

qsapp (x :: xs^{Y})^{Y 1} ys = let (l^{Y}, r^{Y}) = pivot x xs in qsapp l^{Y} (x :: qsapp r^{Y} ys) quicksort : int list → int list quicksort l = qsapp l [ ]

Fig. 1. Example: Quick-sort.

For programs like quicksort (cf. Fig. 1, ignore type annotations for now), input arguments are transformed via another function (here: pivot), before fed into the recursive call. Hence, analyses need to infer the size relation between input and output of a function, or at least detect non-size increasing functions like pivot. Well-designed static analyses [19, 14, 15, 22] support some size checking for firstorder programs, but fail for higher-order programs. These analyses usually have some other drawbacks: they are quite sophisticated and thus hard to comprehend and to trust, and they are sensitive to little changes in the program code: a program which passed a termination check might not pass any longer if a redex is introduced (cf. discussion in Barthe et al. [7]). Furthermore, they all fail for non-strictly positive datatypes.

Type-based analysis tries to address these problems by assigning a specific type to a total program instead of analyzing the code: Types are preserved under reduction and scale to higher-order functions and non-strictly positive data. Type theory has a long tradition in the programming language and theorem proving community and people are trained to understand typing rules. So a type-based approach might be easier to comprehend and easier trusted.

The first type-based approach to termination is attributed to Mendler [16]. He used universally quantified type variables to restrict recursive calls. His ideas have been further developed by many [6, 21]; we will only consider approaches here which also detect non-size increasing functions.

Type-based termination in a nutshell. Inductive structures can be viewed as trees and thus classified by their height. First-order data structures like lists and binary trees have a finite height < ω which can be denoted by a natural number. Proof theory deals also with higher-order data structures like infinitely branching trees whose height can only be denoted by an infinite ordinal α ≥ ω below the least uncountable ordinal Ω. The dual concept to height is definedness or observability upto depth α and applies to coinductive structures.

In type-based termination, total functions are defined by induction on the height/definedness of structures. Let ∇Xσ define a inductive (∇ ≡ μ) or coinductive (∇ ≡ ν) datatype. Then ρ ≈ ∇Xσ denotes a subtype or approximation ρ of ∇Xσ which contains elements below a certain height/definedness α. Following Barthe et al. [7] we will refer to such elements as elements at stage α. Next, ρ^{n} denotes the type of elements at stage α + n. Types involving bounded quantification ∀Y ≈∇Xσ. τ(Y) can be instantiated at any approximation ρ ≈ ∇Xσ of a datatype to obtain the type τ(ρ). Recursive functions of result type τ involving ∇Xσ are introduced by the rule

{Y ≈∇Xσ, g:τ(Y) ⊢ M : τ(Y^{1}) \atop fix^{∇}g.M : ∀Y ≈∇Xσ. τ(Y)}.

The premise incarnates the step case of induction, taking the function from stage α to stage α+1. The base case α = 0 is handled by side conditions on the type τ which ensures that τ at stage 0 is interpreted as the whole universe of programs. This holds trivially for the class

\begin{aligned}τ(Y) & ≡ & Y → τ′(Y) & if ∇ = μ, \\ τ(Y) & ≡ & τ′(Y) → Y & if ∇ = ν. \end{aligned}

The fact that τ′ may depend on Y enables the type system to tract stage dependencies between input and output of a function like pivot : int → ∀Y ≈ int list. Y → Y × Y. The type of pivot guarantees that the length of both output lists is bounded by the length of the input list. This feature is very valuable for defining Euclidian division, merge sort, the stream of Fibonacci numbers (see below) etc.

For higher-order datatypes ∇Xσ we have to continue induction transfinitely and also handle the limit case α = λ. More precisely, we have to show that if the recursive program fix^{∇}g.M inhabits τ at stages β < λ then it inhabits τ also at the limit stage λ. For types in the special class above this is always the case if τ′(Y) is monotone in Y. But this is not a necessary condition and there are interesting types which do not fall into the above class. E.g., let Stream = νX. Nat×X denote streams of natural numbers, fold : ∀Y ≈Stream. Nat×Y → Y^{1} the injection into Stream and

sum : ∀Y ≈Stream. Y → Y → Y
sum (x :: xs) (y :: ys) = x + y :: sum xs ys
fib′ : ∀Y ≈Stream. Nat × Y
fib′ = (0, 1 :: sum (fold fib′) (snd fib′))

from which we can obtain the stream of Fibonacci numbers fib = fold fib′. In the type system of Barthe el al. [7], the type of fib′ is not accepted and it is not clear how to define the Fibonacci stream in a similarly elegant way. As we will see in Sect. 4, both definitions are perfectly legal in our system.

Approach  Flavor Polym. Norm. Datatypes Stages Arithmetic Continuity
Xi [23]  Church yes closed FO-μ  < ω Presb., ∗/  —
Hughes/Pareto+ [12, 11, 17] Curry yes closed FO-μν ≤ ω  Presb.  yes
Barthe/Giménez+ [7]  Curry no  SN  HO-μν < Ω +1 only  no
this  Curry no  SN  HO-μν < Ω +1 only  yes

Table 1. Recent work on type-based termination.

Contribution. This work addresses the question: Which types are legal as the result type τ of a recursive definition? We cannot give a final answer yet, but we have identified a class of types exceeding Barthe el al. [7] which follow a regular pattern. We analyzed the interpretation of types by sets of strongly normalizing terms and found that τ needs to be continuous for corecursive and something which we called paracontinuous for recursive definitions.

Hughes’ et al. [12] system accepts types τ which are ω-undershooting and pass a bottom-check, but he worked in a domain theoretic denotational semantics with only first-order datatypes and it is not clear yet whether all of his results carry over when considering strong normalization and higher-order datatypes.

Table 1 compares some recent approaches to type-based termination. Xi [23] aims at functional programming with a cbv-reduction semantics for closed terms and first-order inductive datatypes, hence its sufficient for him to consider only finite stages and he does not need to address the problem of limit stages and continuity. His stage expressions are most expressive and support full arithmetic, but this makes type-checking semi-decidable if multiplication of stages is involved. Hughes and Pareto aim at embedded functional programming with streams and processes, they have treated the problem of continuity for ω-instantiation. Barthe and Giménez aim at theorem proving and support higher-order datatypes needed for proof theory. They show strong normalization, but do not investigate continuity, and here this works steps in.

Our calculus λ^{fixμν} might serve as the core of a total functional programming language or an interactive proof assistant. Since it also handles non-strictly positive types, it could help to investigate programs with continuation types or algorithms extracted from classical proofs via double-negation translation.

This article is organized as follows. In Sect. 2 we will present the untyped term language with reduction semantics, and in Sect. 3 we will define types, subtyping and type interpretation. Sect. 4 is devoted to continuous types and Sect. 5 to co- and paracontinuous types. In Sect. 6 we will introduce the typing rules and prove soundness.

2 Untyped Calculus

Figure 2 presents terms, evaluation contexts and reduction relations of λ^{fixμν}, a core functional programming language with iso-recursive categorical datatypes, (fold, unfold), recursion (fix^{μ}) and corecursion (fix^{ν}). “fold” is the general constructor, sometimes called in; “unfold” the general destructor, also called out.

Terms M, N ∈ TM.

M, N ::=x | λx.M | M N | inl M | inr M | (case M of inl x_{1} ⇒ M_{1} | inr x_{2} ⇒ M_{2})
| (M_{1}, M_{2}) | fst M | snd M | fold M | unfold M | fix^{μ}g.M | fix^{ν}g.M

Evaluation contexts.

E[•] ::=• | E[•] M | unfold E[•] | (case E[•] of inl x_{1} ⇒ M_{1} | inr x_{2} ⇒ M_{2})
| fst E[•] | snd E[•] | (fix^{μ}g.M) E[•]

β-Reduction axioms: Lambda calculus with sums and products +

unfold (fold M) ⟶_{β} M
(fix^{μ}g.M) (fold N) ⟶_{β} ([fix^{μ}g.M/g]M)(fold N)
unfold E[fix^{ν}g.M] ⟶_{β} unfold E[[fix^{ν}g.M/g]M]

Reduction relations.

⟶_{β} β-reduction
⟶  one-step reduction: closure of ⟶_{β} under all term constructors
⟶^{+} transitive closure of ⟶
⟶^{∗}  reflexive-transitive closure of ⟶

Fig. 2. λ^{fixμν}: Terms, Evaluation Contexts and Reduction

Reduction axioms are standard, solely of interest are the rules for the fixedpoints: Recursive functions fix^{μ} are only unfolded when applied to an argument guarded by a fold and infinite objects fix^{ν} only under a unfold-destructor. These restrictions are essential for establishing strong normalization. The reduction relation ⟶, which results from closing ⟶_{β} under all term constructors, is confluent, which can be shown with the parallel-reduction method by Tait and Martin-Löf.

The set of strongly normalizing terms SN is defined as the wellfounded part of the set TM of terms wrt. the reduction relation ⟶. All variables x and all subterms of strongly normalizing terms are strongly normalizing. Furthermore, the set SN is closed under reduction.

Proofs of strong normalization typically involve some standardization argument. In our case we use weak head reduction; it is a reduction of the form E[M_{1}] ⟶ E[M_{2}] where M_{1} ⟶_{β} M_{2}. Terms of the form E[x] are called neutral. A set of terms P ⊆ TM is called saturated, written P ∈ SAT , if it contains only strongly normalizing terms, all strongly normalizing neutral terms, and if it is closed under weak head expansion. The saturation of a set P is defined as the closure under the following rules:

{M ∈ P \atop M ∈ P^{∗}}  {E[x] ∈ SN \atop E[x] ∈ P^{∗}}  {M ∈ SN  M ⟶_{β} M′  E[M′] ∈ P^{∗} \atop E[M] ∈ P^{∗}}

The set SN is saturated, and so is the function space P → Q := {M | M N ∈ Q for all N ∈ P }, provided P, Q ∈ SAT .

Types (∇ ∈ {μ, ν}, n ∈ ℕ).

ρ, σ, τ ::= X | σ → τ | σ + τ | σ × τ | ∇Xσ | Y^{n} | ∀Y ≈ ∇Xσ. τ

Contexts. Γ ::= · | Γ, x: τ | Γ, X | Γ, Y ≈ ∇Xσ

Judgments.

Γ cxt  Γ is a wellformed context.
Γ ⊢ X pos σ  Variable X appears positively in σ
Γ ⊢ X neg σ  Variable X appears negatively in σ
Γ ⊢ X only pos in σ All occurrences of X in σ are positive.
Γ ⊢ τ : type  τ is a wellformed type.
Γ ⊢ ρ ≈ ∇Xσ  ρ is an approximation of ∇Xσ.
Γ ⊢ ρ ≤ σ  ρ is a subtype of σ.

Approximations.

(Y ≈ ∇Xσ) ∈ Γ ; \overline{≈Y} ; Γ ⊢ Y^{n} ≈ ∇Xσ  \overline{≈∇} ; Γ ⊢ ∇Xσ ≈ ∇Xσ

Subtyping.

ρ ∈ \{μXσ, νXσ\} ; \overline{≤Base} ; Γ ⊢ ρ ≤ ρ  (Y ≈ μXσ) ∈ Γ ; \overline{≤Y_{1}^{μ}} ; Γ ⊢ Y^{n} ≤ μXσ  (Y ≈ μXσ) ∈ Γ  n ≤ m ; \overline{≤Y_{2}^{μ}} ; Γ ⊢ Y^{n} ≤ Y^{m}
(Y ≈ νXσ) ∈ Γ ; \overline{≤Y_{1}^{ν}} ; Γ ⊢ νXσ ≤ Y^{n}  (Y ≈ νXσ) ∈ Γ  n ≤ m ; \overline{≤Y_{2}^{ν}} ; Γ ⊢ Y^{m} ≤ Y^{n}
Γ ⊢ σ_{1} ≤ ρ_{1}  Γ ⊢ ρ_{2} ≤ σ_{2} ; \overline{≤→} ; Γ ⊢ ρ_{1} → ρ_{2} ≤ σ_{1} → σ_{2}  {Γ ⊢ ρ_{1} ≤ σ_{1}  Γ ⊢ ρ_{2} ≤ σ_{2}  ⋆ ∈ \{+, ×\} \atop Γ ⊢ ρ_{1} ⋆ ρ_{2} ≤ σ_{1} ⋆ σ_{2}}≤⋆
Γ ⊢ ρ ≈ ∇Xσ  Γ ⊢ [ρ/Y]τ ≤ τ′ ; \overline{≤∀L} ; Γ ⊢ (∀Y ≈ ∇Xσ. τ) ≤ τ′  Γ, Y ≈ ∇Xσ ⊢ ρ ≤ τ ; \overline{≤∀R} ; Γ ⊢ ρ ≤ ∀Y ≈ ∇Xσ. τ

Fig. 3. λ^{fixμν}: Types and Subtyping.

3 Types

Figure 3 presents types and type related judgments. Most of these are standard, like wellformedness of contexts and positive and negative occurrences of variables. A type τ is wellformed (Γ ⊢ τ : type) if it follows the grammar with the restriction that if τ ≡ ∇Xσ is a (co)inductive type, X may appear only positively in σ and σ may not contain quantifiers. Approximation types Y^{n} and bounded quantification ∀Y ≈ ∇Xσ. τ have been explained in the introduction already. Note that unit and empty type can be defined: 1 = νX.X, 0 = μX.X.

We regard all variables bound in a context as distinct. (Capture-avoiding) substitution for types is defined as usual and written [ρ/X]σ. Sometimes we exhibit a free variable in a type σ(X) and write σ(ρ) for the result of substitution. For approximations we define a special substitution given by the axioms [X^{m}/Y]Y^{n} = X^{n+m} and [∇Xσ/Y]Y^{n} = ∇Xσ plus congruence rules for all type constructors. The second axiom is justified by the fact that ∇Xσ denotes a fixed-point which is unaffected by n more iterations.

Subtyping is induced by approximation types. Since the semantics [[Y]] of some bounded type variable Y ≈ μXσ denotes some subset of [[μXσ]], we introduce the subtyping rule Y ≤ μXσ. Furthermore, since the approximations of an inductive type form an ascending chain bounded by the fixed-point of the approximation operator, we can safely add subtyping rules Y^{i} ≤ Y^{j} and Y^{i} ≤ μXσ for all indices i and j with i ≤ j. Note that two different type variables X ≠ Y are incomparable. Subtyping rules for approximations of coinductive types are obtained by dualization.

To increase expressivity of subtyping, we have incorporated a reflexivity rule for base types, congruence rules for sum, product and function types (contravariant on the left!) and rules for quantification. The subtyping relation ≤ is reflexive and transitive. Since most rules are syntax-directed, it is not hard to come up with a decision algorithm for subtyping. The only critical rules are the ones for quantification: rule ≤∀R always has to be applied before ≤∀L. When the rule ≤∀L fires, an approximation ρ has to be guessed. This can be implemented using existential variables and unification.

Type interpretation and soundness. In the following, we give an interpretation of types as sets of terms which we will later show to be saturated. Approximations will be interpreted as iterations Φ^{α} of monotonic operators Φ : P(TM) → P(TM). To distinguish between approximation from above and below, we define iterates as Φ^{∇,α} with a tag ∇ ∈ {μ, ν}.

\begin{aligned}Φ^{μ,0} & = & ∅^{∗} & Φ^{ν,0} & = & SN \\ Φ^{μ,α+1} & = & Φ(Φ^{μ,α}) & Φ^{ν,α+1} & = & Φ(Φ^{ν,α}) \\ Φ^{μ,λ} & = & ⋃_{α<λ} Φ^{μ,α} & Φ^{ν,λ} & = & ⋂_{α<λ} Φ^{ν,α} \end{aligned}

When clear from the context, we omit the tags μ, ν. To interpret context as sets of substitutions, let P, Q from here denote sets of terms. Raw substitutions are given by the grammar θ ::= · | θ, x ↦ M | θ, X ↦ P | θ, Y ↦ (Φ, ∇, α). Note that approximation variables Y are mapped to a triple consisting of a monotonic operator Φ, a flag ∇ ∈ {μ, ν} denoting whether Y approximates a least fixedpoint from below or a greatest fixed-point from above, plus an ordinal α denoting the current iteration. Γ -substitutions θ : Γ are those with dom(θ) = dom(Γ).

Let Γ ⊢ τ : type and θ : Γ. We define the type interpretation [[τ]]θ ⊆ TM by recursion on τ.

[[σ + τ]]θ = {inl M | M ∈ [[σ]]θ}^{∗} ∪ {inr M | M ∈ [[τ]]θ}^{∗}
[[σ × τ]]θ = {M | fst M ∈ [[σ]]θ, snd M ∈ [[τ]]θ}
[[σ → τ]]θ = [[σ]]θ → [[τ]]θ  [[X]]θ = θ(X)
[[μXσ]]θ = Φ_{μXσ,θ}^{Ω}  Φ_{μXσ,θ}(Q) = {fold M | M ∈ [[σ]](θ, X ↦Q)}^{∗}
[[νXσ]]θ = Φ_{νXσ,θ}^{Ω}  Φ_{νXσ,θ}(Q) = {M | unfold M ∈ [[σ]](θ, X ↦Q)}
[[Y^{n}]]θ = Φ^{α+n}  where θ(Y) = (Φ, ∇, α)
[[∀Y ≈∇Xσ. τ]]θ = ⋂_{α}[[τ]](θ, Y ↦(Φ_{∇Xσ,θ}, ∇, α))

The “introduction-based” semantics of + and μ has to be saturated explicitely (note the ^{∗}), which is not necessary for “elimination-based” constructions (→, ×, and ν). The semantics of (co)inductive types ∇Xσ are defined as iterates of operators at stage Ω, which is a (greatest) least fixed-point iff the semantics [[τ]] is monotonic for each substitution θ, i.e., monotonic in every variable that occurs positively and antitonic in every variable that occurs negatively. To make this observation precise, we define inclusion for substitutions. Let Γ ⊢ τ : type. Then Γ ⊢_{τ} θ_{1} ⊆ θ_{2} is defined to hold iff θ_{1} and θ_{2} are Γ -substitutions and

– θ_{1}(X) ⊆ θ_{2}(X) for all X with Γ ⊢ X pos τ,

– θ_{1}(X) ⊇ θ_{2}(X) for all X with Γ ⊢ X neg τ, and

– θ_{1}(Y) = θ_{2}(Y) for all (Y ≈∇Xσ) ∈ Γ.

Lemma 1 (Soundness of Subtyping). If Γ ⊢ ρ ≤ σ and Γ ⊢_{ρ} θ_{1} ⊆ θ_{2} then [[ρ]]θ_{1} ⊆ [[σ]]θ_{2}.

Proof. By induction on Γ ⊢ ρ ≤ σ.

By reflexivity of subtyping, this lemma entails monotonicity of all types which, again, entails soundness of our fixed-point construction. By simple induction proofs we also establish that substitution for types and approximations is sound. Finally, we show is that types are interpreted as saturated sets. To this end, we define the semantical version θ ∈ [[Γ]] of θ : Γ.

· ∈ [[·]]  {M ∈ [[τ]]θ  θ ∈ [[Γ]] \atop (θ, x↦M) ∈ [[Γ, x:τ]]}  {P ∈ SAT  θ ∈ [[Γ]] \atop (θ, X ↦P) ∈ [[Γ, X]]}

{α ordinal θ ∈ [[Γ]] \atop (θ, Y ↦(Φ_{∇Xσ,θ}, ∇, α)) ∈ [[Γ, Y ≈∇Xσ]]}

Lemma 2 (Saturatedness). If Γ cxt then for all θ ∈ [[Γ]] and all X the set θ(X) is saturated. If Γ ⊢ τ : type then for all θ ∈ [[Γ]] it holds that [[τ]]θ ∈ SAT .

4 Continuous Types

In this section, we will identify a set of legal result types τ(Y) for corecursion (see Sect. 1). The key requirement on τ is continuity. An operator Φ is continuous if for all families P^{α} (α ∈ I) of term sets it holds that

⋂_{α∈I} Φ(P^{α}) ⊆ Φ ( ⋂_{α∈I} P^{α}) .

In the following we will motivate why continuity is a necessary condition on τ. Consider the typing rule for corecursion specialized to streams.

Y ≈Stream, g:τ(Y) ⊢ M : τ(Y^{1})
fix^{ν}g.M : ∀Y ≈Stream. τ(Y)

Let S(Q) = {M ∈ TM | hd M ∈ [[Nat]] and tl M ∈ Q} be the semantical operator to construct the set of streams. Then [[Stream]] = ⋂_{α<ω} S^{α}. Hence, the corecursion rule for streams can be proven sound by transfinite induction upto ω. In the limit case ω, we can use the induction hypothesis for all smaller stages, i.e., we can assume

fix^{ν}g.M ∈ ⋂_{α<ω}[[τ]](S^{α}) to show fix^{ν}g.M ∈ [[τ]]( ⋂_{α<ω} S^{α}) = [[τ]]([[Stream]]).

Obviously, we require [[τ]] to be continuous.

A grammar for continuous types. We introduce a new judgment Γ ⊢ X cont τ, meaning that τ is continuous in the variables X.

Γ ⊢ X cont X_{i}

{X ∉ FV(τ) \atop Γ ⊢ X cont τ}

Γ ⊢ X only pos in σ Γ ⊢ X cont τ
Γ ⊢ X cont σ → τ
Γ ⊢ X cont σ, τ
Γ ⊢ X cont σ + τ

Γ ⊢ X cont σ, τ
Γ ⊢ X cont σ × τ

Γ, X ⊢ X, X cont σ
Γ ⊢ X cont ∇Xσ
(Y ≈∇Xσ) ∈ Γ Γ ⊢ X cont ∇Xσ
Γ ⊢ X cont Y^{n}

Γ, Y ≈∇Xσ ⊢ X cont τ
Γ ⊢ X cont ∀Y ≈∇Xσ. τ

For function types to be continuous, the domain just needs to be monotonic and the range continuous. Fixed-points are continuous if the respective operator is continuous and (of course) monotonic. Surprising is the fact that least fixedpoints are continuous, which requires that union preserves continuity. Let Φ be the operator of an inductive type. Then

⋂_{α} ⋃_{β<λ} Φ^{β}(P^{α}) ⊆ ⋃_{β<λ} Φ^{β} (⋂_{α} P^{α})

does not hold simply by set-theoretic means, even if Φ is continuous. In our semantics however, an intersection can be pulled into a union. Informally this may be explained as follows:

Consider polymorphic lists List(X) with operator L(A)(Q) = {nil} ∪ {a :: l | a ∈ A, l ∈ Q}. Note that for some fixed set A, L(A)^{n} denotes the nth approximant to [[List]](A). Recall that S was defined as the operator for streams. We say a stream s has goodness n if s ∈ S^{n}. Let M be some list of streams with the following property: At the same time, let M be a list of length m_{0} of streams of goodness 0, a list of length m_{1} of streams of goodness 1, … a list of length m_{n} of streams of goodness n, …. Formally, M ∈ L(S^{i})^{m_{i}} for all i. Since a list can only have one length, all m_{i} must be equal. Hence m_{i} = m_{0} for all i, and

⋂_{n}[[List]](S^{n}) = ⋂_{n}(⋃_{m}(L(S^{n}))^{m}) = ⋂_{n}(L(S^{n}))^{m_{0}}
⊆ (L(⋂_{n} S^{n}))^{m_{0}} = (L([[Stream]]))^{m_{0}} ⊆ [[List]]([[Stream]])

This example shows that List(A) is continuous in A. To generalize this result for all inductive types, we make the following general observation that new inductive data is only generated by successor iterates:

Lemma 3 (Successor Iterates are Sufficient). If fold M ∈ Φ_{μXσ,θ}^{α} then fold M ∈ Φ_{μXσ,θ}^{β+1} for some β < α.

Now we give a formulation of the above explained independence result for inductive types μY σ with a free variable X.

Lemma 4 (Independence). Let [[σ(X, Y)]] be continuous in the variables X and Y and Φ(P)(Q) = {fold M | M ∈ [[σ]](X ↦ P, Y ↦ Q)}^{∗}. Furthermore, let (β_{α}) a sequence of ordinals and P^{α} a sequence of sets of terms. Then

⋂_{α}(Φ(P^{α}))^{β_{α}} ⊆ Φ(⋂_{α} P^{α})^{β_{0}}

This lemma is proven by induction on β_{0} and can be generalized to continuous types σ(X, Y) by defining intersection on substitutions θ. It then yields soundness of syntactic continuity.

Theorem 1 (Soundness of cont). Let Γ ⊢ τ : type. If Γ ⊢ X cont τ, then [[τ]] is continuous in X.

As a side product of our considerations, we notice that all strictly positive coinductive types are continuous. Thus, their fixed-point is reached at iteration ω.

Types for infinite objects. Can all continuous types be used for fix^{ν}-definitions? Given our reduction semantics, the answer is no. Sums, inductive and coinductive types may be continuous, but they do not provide the necessary guardedness. For example, let

map_{0} = map (λx.0 :: x) : ∀Y ≈Stream.List(Y) → List(Y^{1})

Then M = fix^{ν}g. map_{0} g could be ascribed type ∀Y ≈Stream. List(Y). But unfolding of M diverges: unfold M ⟶_{β} unfold(map_{0} M) ⟶_{β} unfold(map_{0} (map_{0} M)) ⟶_{β} … Similar examples can be found for types with + and ν. What remains as legal types for fix^{ν}, are function space and product. By a judgment Y legal^{ν} τ, we give a grammar for these types.

Y legal^{ν} Y

Y only pos in σ Y legal^{ν} τ
Y legal^{ν} σ → τ

Y legal^{ν} σ Y legal^{ν} τ
Y legal^{ν} σ × τ

Examples for legal types τ according to this grammar which are not of the form τ(Y) → Y (τ monotone), like Y → Y → Y and Nat × Y, have been given in the introduction (Fibonacci streams).

5 Co- & Paracontinuous Types

As we have answered for fix^{ν}, we can ask for the recursive function constructor fix^{μ}: Which types τ(Y) would be legal in the rule

{Y ≈μXσ, g:τ(Y) ⊢ M : τ(Y) \atop fix^{μ}g.M : ∀Y ≈μXσ. τ(Y)}

This rule would be proven sound by transfinite induction on the approximations Φ^{α} of the inductive type μXσ. For limit steps λ, we may assume

fix^{μ}g.M ∈ ⋂_{α<λ}[[τ]](Φ^{α})  to show  fix^{μ}g.M ∈ [[τ]]( ⋃_{α<λ} Φ^{α}).

We call such types τ(Y), which permit this inference, paracontinuous. Obviously paracontinuous are types of the form Y → τ(Y) for Y only pos in τ. However, this does not include the most precise type for, e.g., the maximum function max : ∀Y ≈ Nat. Y → (Y → Y). Here Y occurs negatively in Y → Y, but the type is still paracontinuous. On our journey to identify paracontinuous types syntactically, we will first consider cocontinuity, the concept dual to continuity.

Cocontinuity. An operator Φ : P(TM) → P(TM) is called cocontinuous, if for all chains P (with P^{α} ⊆ P^{β} for α < β) it holds that

Φ(⋃_{α} P^{α}) ⊆ ⋃_{α} Φ(P^{α})

In the following we will identify the types τ for which the semantics [[τ]] is cocontinuous. Let us first consider products.

Lemma 5 (Products preserve Cocontinuity). Let Γ ⊢ σ(X), τ(X) : type. If [[σ]] and [[τ]] are cocontinuous and monotonic in X, so is [[σ × τ]].

Proof. Assume M ∈ [[σ × τ]](⋃_{α} P^{α}). Then by definition, fst M ∈ [[σ]](⋃_{α} P^{α}) and snd M ∈ [[τ]](⋃_{α} P^{α}). Since σ and τ are cocontinuous by assumption, there are ordinals α, β such that fst M ∈ [[σ]](P^{α}) and snd M ∈ [[τ]](P^{β}). Now let γ = max(α, β). Since P is a chain and [[σ]] and [[τ]] are monotonic, fst M ∈ [[σ]](P^{γ}) and snd M ∈ [[τ]](P^{γ}). We conclude M ∈ [[σ × τ]](P^{γ}).

Thus, products are cocontinuous because the binary maximum always exists. Since function types and coinductive types can be viewed as infinite products, they are not cocontinuous in general. For example, λx.x ∈ List → ⋃_{α<ω} L^{α}, but it does not inhabit List → L^{α} for any α < ω. We expect that the same holds for quantification. Sums and inductive types are trivially cocontinuous, provided they are monotonic. Hence, we can give a grammar for cocontinuous types via a judgment Γ ⊢ X cocont τ.

Γ ⊢ X cocont X_{i}

X ∉ FV(τ)
Γ ⊢ X cocont τ

Γ ⊢ X cocont σ, τ
Γ ⊢ X cocont σ + τ, σ × τ
Γ, X ⊢ X, X cocont σ
Γ ⊢ X cocont μXσ

(Y ≈μXσ) ∈ Γ Γ ⊢ X cocont μXσ
Γ ⊢ X cocont Y^{n}

Note that Γ ⊢ X cocont τ implies Γ ⊢ X only pos in τ. The grammar describes polynomial interleaved (nested) inductive types, which includes, e.g., natural numbers, lists and finitely branching trees, i.e., almost all inductive types used in practical programming. Furthermore all of these types are continuous and close at ω.

Lemma 6 (Soundness). If Γ ⊢ X cocont τ, then [[τ]] is cocontinuous and monotonic in X.

Proof. By induction on Γ ⊢ X cocont τ, using Lemma 5.

Paracontinuity. The considerations at the start of Sect. 5 suggested a definition of paracontinuity immediately. However, to make it work, we have to strengthen it a little.

An operator Φ is paracontinuous if for all chains P it holds that

for all α_{0} : ⋂_{α_{0}≤α} Φ(P^{α}) ⊆ Φ(⋃_{α} P^{α}).

Obviously all monotonic operators are paracontinuous. For function types, the domain has to be cocontinuous.

Lemma 7 (Paracontinuous Function Types). If [[τ]] is paracontinuous in X and [[σ]] is cocontinuous and monotonic in X, then [[σ → τ]] is paracontinuous in X.

Proof. Fix some α_{0} and assume M ∈ ⋂_{α_{0}≤α}[[σ → τ]](P^{α}) and N ∈ [[σ]](⋃_{α} P^{α}). Since σ is cocontinuous, N ∈ [[σ]](P^{β}) for some β. Let γ = max(α_{0}, β). Now, since P^{α} is a ascending chain, we can exploit the monotonicity of [[σ]] to infer N ∈ [[σ]](P^{α}) for all α ≥ γ. By assumption, M N ∈ [[τ]](P^{α}) for all α ≥ γ. Finally, since τ is paracontinuous, M N ∈ [[τ]](⋃_{α} P^{α}).

For types σ(X, Y) which are continuous in Y, fixed-point formation ∇Y σ preserves paracontinuity in X. The case of inductive types is especially interesting, since it makes again use of the Independence Lemma.

Lemma 8 (Paracontinuous Inductive Types). If [[σ(X, Y)]] is paracontinuous in X and continuous and monotonic in Y, then [[μYσ]] is paracontinuous in X.

Proof. By transfinite induction on the stages of [[μYσ]], using Lemma 4.

For coinductive types νY σ the proof is quite similar, but can be done without Lemma 4. The proven lemmata can be generalized to paracontinuity in several variables X.

We give a grammar for paracontinuous types by the judgment Γ ⊢ X para τ.

Γ ⊢ X para X_{i}

{X ∉ FV(τ) \atop Γ ⊢ X para τ} Γ ⊢ X cocont σ Γ ⊢ X para τ

Γ ⊢ X para σ → τ
Γ ⊢ X para σ, τ
Γ ⊢ X para σ + τ, σ × τ

Γ, X ⊢ X cont σ Γ, X ⊢ X, X para σ

Γ ⊢ X para ∇Xσ
(Y ≈∇Xσ) ∈ Γ Γ ⊢ X para ∇Xσ
Γ ⊢ X para Y^{n}

Γ, Y ≈∇Xσ ⊢ X para τ
Γ ⊢ X para ∀Y ≈∇Xσ.τ

Theorem 2 (Soundness). Let Γ ⊢ τ : type. If Γ ⊢ X para τ then [[τ]] is paracontinuous in X.

Proof. By induction on Γ ⊢ X para τ, using Lemmata 7 and 8.

Note that Γ ⊢ X cont τ implies Γ ⊢ X para τ. A non-paracontinuous type is τ(Y) = Stream(Y) → Bool (acknowledgment: John Hughes). A function “double” which checks whether a stream has duplicate elements would be total for streams of numbers bounded by some α < ω (returning always true) but not for streams of arbitrary natural numbers α = ω.

As for continuous types we raise the question: Are all paracontinuous types legal result types for the recursion constructor fix^{μ}? Again, the answer is no. Our reduction semantics only permits types Y → τ(Y) for Y para τ, which is still a great improvement over Y only pos in τ.

Typing (τ and all types in Γ closed):

Γ ⊢ M : τ

(Lambda-calculus with products and sums +) Folding.

{Γ ⊢ M : [∇Xσ/X]σ \atop Γ ⊢ fold M : ∇Xσ}  {(Y ≈ ∇Xσ) ∈ Γ  Γ ⊢ M : [Y^{n}/X]σ \atop Γ ⊢ fold M : Y^{n+1}}

Unfolding.

{Γ ⊢ M : ∇Xσ \atop Γ ⊢ unfold M : [∇Xσ/X]σ}  {(Y ≈ ∇Xσ) ∈ Γ  Γ ⊢ M : Y^{n+1} \atop Γ ⊢ unfold M : [Y^{n}/X]σ}

Fixed-Points.

{Γ, Y ≈ μXσ, g: Y → τ(Y) ⊢ M : Y^{1} → τ(Y^{1}) Γ ⊢ Y para τ(Y) \atop Γ ⊢ fix^{μ}g.M : ∀Y ≈ μXσ. Y → τ(Y)}

{Γ, Y ≈ νXσ, g: τ(Y) ⊢ M : τ(Y^{1}) Γ ⊢ Y legal^{ν} τ(Y) \atop Γ ⊢ fix^{ν}g.M : ∀Y ≈ νXσ. τ(Y)}

Subsumption.

{Γ ⊢ M : σ  Γ ⊢ σ ≤ τ \atop Γ ⊢ M : τ}  {Γ, Y ≈ ∇Xσ ⊢ M : τ \atop Γ ⊢ M : ∀Y ≈ ∇Xσ. τ}

Fig. 4. λ^{fixμν}: Typing rules.

6 Typing and Soundness

Figure 4 displays the typing rules of λ^{fixμν}. We excluded polymorphism, hence terms are only assigned closed types. By this we mean that τ contains no free type variables X, whereas approximations Y^{n} of fixed-point types are permitted.

The rules for lambda-calculus, sums and products are omitted since they are standard. For wrapping (fold) and unwrapping (unfold) (co)inductive types there are two rules each, one rule for the fixed-point and one dealing with approximations Y^{n+1}, keeping track of the stage. The rules for (co)recursion carry the side conditions developed in the previous sections. Furthermore, we have rules for subsumption (which includes ∀-instantiation) and ∀-introduction independent of a fix^{∇}.

Reduction is type preserving, I have shown this for a slightly simpler system [2]. The proof of soundness of typing (implying strong normalization) is similar to Barthe/Giménez [7], although I developed it independently following Abel/Altenkirch [3]. Due to lack of space I can only give a sketch.

Let the application Mθ of a substitution θ to a term M be defined as expected.

Lemma 9 (Soundness for fix^{μ}). Let Γ ⊢ Y para τ, θ ∈ [[Γ]] a substitution and Φ = Φ_{μXσ,θ}. Assume Mθ′ ∈ [[Y^{1} → τ(Y^{1})]]θ′ for all θ′ ∈ [[Γ, Y ≈ μXσ, g: Y → τ(Y)]]. Then

fix^{μ}g.Mθ ∈ ⋂_{α<Ω} Φ^{α} → [[τ]](θ, Y ↦(Φ, μ, α)).

Proof. By transfinite induction on α. The base case holds since Φ^{0} contains no canonical terms. The step case makes use of saturatedness, the ind. hyp. and the assumption on M. The limit case follows by paracontinuity.

The soundness of fix^{ν} requires a little more work. First we give a judgment E[•] ∈ [[τ ⊸ ρ]]θ that types some evaluation contexts.

• ∈ [[ρ ⊸ ρ]]θ  {E[•] ∈ [[τ ⊸ ρ]]θ  N ∈ [[σ]]θ \atop E[• N] ∈ [[(σ → τ) ⊸ ρ]]}

{E[•] ∈ [[τ_{1} ⊸ ρ]] \atop E[fst •] ∈ [[τ_{1} × τ_{2} ⊸ ρ]]}  {E[•] ∈ [[τ_{2} ⊸ ρ]] \atop E[snd •] ∈ [[τ_{1} × τ_{2} ⊸ ρ]]}

The linear arrow ⊸ is not a first-class type constructor, rather some notation. It is motivated by the fact that evaluation contexts E have exactly one hole •.

Lemma 10. Let Γ ⊢ Y legal^{ν} τ and some θ ∈ [[Γ]]. Assume that for all E[•] ∈ [[τ ⊸ Y]]θ, E[M] ∈ [[Y]]θ. Then M ∈ [[τ]]θ.

Proof. By induction on Γ ⊢ Y legal^{ν} τ.

Lemma 11 (Soundness of fix^{ν}). Let Γ ⊢ Y legal^{ν} τ, substitution θ ∈ [[Γ]] and Φ = Φ_{νXσ,θ}. Assume Mθ′ ∈ [[τ(Y^{1})]]θ′ for all θ′ ∈ [[Γ, Y ≈νXσ, g:τ(Y)]]. Then

fix^{ν}g.Mθ ∈ ⋂_{α<Ω}[[τ]](θ, Y ↦(Φ, ν, α))

Proof. By transfinite induction on α. Note that the assumption implies G ≡ fix^{ν}g.Mθ ∈ SN. The base case follows by Lemma 10 since Φ^{0} = SN, and the limit case is a consequence of continuity of [[τ(Y)]]. The step case makes crucial use of Lemma 10, since we consider unfold E[G] ⟶_{β} unfold E[Mθ′] for an appropriate extension θ′ of θ and all E[•] ∈ [[τ ⊸ Y]](θ, Y ↦Φ^{α+1}). The r.h.s. can be shown to be in the semantics by assumption, so the l.h.s. as well by saturation, which entails the goal. ⊓ ⊔ Theorem 3 (Soundness of Typing). Γ ⊢ M : τ, θ ∈ [[Γ]] imply Mθ ∈ [[τ]].

Soundness, proved by induction on Γ ⊢ M : τ, now directly entails strong normalization (choose some θ which keeps all term variables fixed).

References

1. Andreas Abel. Specification and verification of a formal system for structurally recursive functions. In TYPES ’99, vol. 1956 of LNCS, pages 1–20. Springer, 2000.

2. Andreas Abel. Termination checking with types. Technical Report 0201, Institut für Informatik, Ludwigs-Maximilians-Universität München, 2002.

3. A. Abel and T. Altenkirch. A predicative strong norm. proof for a λ-calculus with interleaving inductive types. In TYPES ’99, vol. 1956 of LNCS. Springer, 2000.

4. Andreas Abel and Thorsten Altenkirch. A predicative analysis of structural recursion. Journal of Functional Programming, 12(1):1–41, January 2002.

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

6. Roberto M. Amadio and Solange Coupet-Grimal. Analysis of a guard condition in type theory. In FoSSaCS ’98, volume 1378 of LNCS. Springer, 1998.

7. G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu. Type-based termination of recursive definitions. Math. Struct. in Comp. Sci., 2002. To appear.

8. Thierry Coquand. Infinite objects in type theory. In TYPES ’93, volume 806 of LNCS, pages 62–78. Springer, 1993.

9. Eduardo Giménez. Codifying guarded definitions with recursive schemes. In TYPES´ 94, volume 996 of LNCS, pages 39–59. Springer, 1995.

10. Martin Hofmann. Non strictly positive datatypes for breadth first search. TYPES mailing list, 1993.

11. John Hughes and Lars Pareto. Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In ICFP’99, pages 70–81, 1999.

12. John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In POPL’96, pages 410–423. ACM Press, 1996.

13. INRIA. The Coq Proof Assistant Reference Manual, version 7.0 edition, April 2001.

14. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In POPL’01. ACM Press, 2001.

15. David McAllester and Kostas Arkoudas. Walther Recursion. In CADE-13, volume 1104 of LNCS. Springer, 1996.

16. Nax Paul Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1–2):159–172, 1991.

17. Lars Pareto. Types for Crash Prevention. PhD thesis, Chalmers University of Technology, 2000.

18. Frank Pfenning and Carsten Schürmann. Twelf - a meta-logical framework for deductive systems. In CADE-16, volume 1632 of LNAI. Springer, 1999.

19. Brigitte Pientka. Termination and reduction checking for higher-order logic programs. In IJCAR 2001, volume 2083 of LNAI, pages 401–415. Springer, 2001.

20. Randy Pollack. The Theory of LEGO. PhD thesis, University of Edinburgh, 1994.

21. Christophe Raffalli. Data types, infinity and equality in System AF2. In CSL ’93, volume 832 of LNCS, pages 280–294. Springer, 1994.

22. Alastair J. Telford and David A. Turner. Ensuring streams flow. In AMAST ’97, volume 1349 of LNCS, pages 509–523. Springer, 1997.

23. Hongwei Xi. Dependent types for program termination verification. Journal of Higher-Order and Symbolic Computation, 15:91–131, 2002.