SEMI-CONTINUOUS SIZED TYPES AND TERMINATION

ANDREAS ABEL

Institut für Informatik, Ludwig-Maximilians-Universität München e-mail address: abel@tcs.ifi.lmu.de

Abstract. A type-based approach to termination uses sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is visible in the type system that recursive calls occur just at a smaller size. This approach is only sound if the type of the recursive function is admissible, i.e., depends on the size index in a certain way. To explore the space of admissible functions in the presence of higher-kinded data types and impredicative polymorphism, a semantics is developed where sized types are interpreted as functions from ordinals into sets of strongly normalizing terms. It is shown that upper semi-continuity of such functions is a sufficient semantic criterion for admissibility. To provide a syntactical criterion, a calculus for semicontinuous functions is developed.

1. Introduction

Termination of computer programs has received continuous interest in the history of computer science, and classical applications are total correctness and termination of partial evaluation. In languages with a notion of computation on the type-level, such as dependently-typed languages or rich typed intermediate languages in compilers [CW99], termination of expressions that compute a type is required for type checking and type soundness. Further, theorem provers that are based on the Curry-Howard Isomorphism and offer a functional programming language to write down proofs usually reject non-terminating programs to ensure consistency. Since the pioneering work of Mendler [Men87], termination analysis has been combined with typing, with much success for strongly-typed languages [HPS96, ACG98, Gim98, Xi01, BFG^{+}04, Bla04]. The resulting technique, type-based termination checking, has several advantages over a purely syntactical termination analysis: (1) It is robust w. r. t. small changes of the analyzed program, since it is working on an abstraction of the program: its type. So if the reformulation of a program (e.g., by introducing a redex) still can be assigned the same sized type, it automatically passes the termination check. (2)

2000 ACM Subject Classification: 68N15, 68N18, 68Q42. Key words and phrases: Type-based termination, sized types, inductive types, semi-continuity, strong

normalization.

A shorter version of this article has appeared in the proceedings of Computer Science Logic 2006 [Abe06c]. Research supported by the coordination action TYPES (510996) and thematic network Applied Se-

mantics II (IST-2001-38957) of the European Union and the project Cover of the Swedish Foundation of Strategic Research (SSF).

LOGICAL METHODS IN COMPUTER SCIENCE  DOI:10.2168/LMCS-???  \begin{matrix}c \\ ◯ \end{matrix} Andreas Abel Creative Commons

In design and justification, type-based termination rests on a technology extensively studied for several decades: types. (3) Type-based termination is essentially a refinement of the typing rules for recursion and for introduction and elimination of data. This is orthogonal to other language constructs, like variants, records, and modules. Thus, a language can be easily enriched by such constructs without change to the termination checker. This is not true if termination checking is a separate static analysis. Orthogonality has an especially pleasing effect: (4) Type-based termination scales to higher-order functions and polymorphism. (5) Last but not least, it effortlessly creates a termination certificate, which is just the typing derivation.

Type-based termination especially plays its strength when combined with higher-order datatypes and higher-rank polymorphism, i. e., occurrence of ∀ to the left of an arrow. Let us see an example. We consider the type of generalized rose trees GRose F A parameterized by an element type A and the branching type F. It is given by two constructors:

leaf : GRose F A
node : A → F (GRose F A) → GRose F A

Generalized rose trees are either a leaf or a node a fr of a label a of type A and a collection of subtrees fr of type F (GRose F A). Instances of generalized rose trees are binary trees (F A = A × A), finitely branching trees (F A = List A), or infinitely branching trees (F A = Nat → A). Programming a generic equality function for generalized rose trees that is polymorphic in F and A, we will end up with the following equations:

Eq A = A → A → Bool

eqGRose : (∀A. Eq A → Eq (F A)) → ∀A. Eq A → Eq (GRose F A)

eqGRose eqF eqA leaf leaf = true

eqGRose eqF eqA (node a fr) (node a′ fr′) = (eqA a a′) ∧ (eqF (eqGRose eqF eqA) fr fr′)

eqGRose eqF eqA = false The generic equality eqGRose takes two parametric arguments, eqF and eqA. The second one is a placeholder for an equality test for type A, the first one lifts an equality test for an arbitrary type A to an equality test for the type F A. The equality test for generalized rose trees, eqGRose eqF eqA, is then defined by recursion on the next two arguments. In the case of two nodes we would expect a recursive call, but instead, the function itself is passed as an argument to eqF , one of its own arguments! Nevertheless, eqGRose is a total function, provided its arguments are total and well-typed. However, with traditional methods, which only take the computational behavior into account, it will be hard to verify termination of eqGRose. This is due to the fact that the polymorphic nature of eqF plays a crucial role. It is easy to find an instance of eqF of the wrong type which makes the program loop. Take, for instance:

eqF : Eq (GRose F Nat) → Eq (F (GRose F Nat)) eqF eq fr fr′ = eq (node 0 fr) (node 0 fr′)

A type-based termination criterion however passes eqGRose with ease: Consider the indexed type GRose^{ı} F A of generalized rose trees whose height is smaller than ı. The types of the constructors are refined as follows:

leaf : ∀F ∀A∀ı. GRose^{ı+1} F A
node : ∀F ∀A∀ı. A → GRose^{ı} F A → GRose^{ı+1} F A

When defining eqGRose for trees of height < ı + 1, we may use eqGRose on trees of height < ı. Hence, in the clause for two nodes, term eqGRose eqF eqA has type Eq (GRose^{ı} F A), and eqF (eqGRose eqF eqA) gets type Eq (F (GRose^{ı} F A)), by instantiation of the polymorphic type of eqF . Now it is safe to apply the last expression to fr and fr′ which are in F (GRose^{ı} F A), since node a fr and node a′ fr′ were assumed to be in GRose^{ı+1} F A.

In essence, type-based termination is a stricter typing of the fixed-point combinator fix which introduces recursion. The unrestricted use, via the typing rule (1), is replaced by a rule with a stronger hypothesis (2):

(1) \frac{f : A → A}{fix f : A}  (2) \frac{f : ∀ı. A(ı) → A(ı + 1)}{fix f : ∀n. A(n)}

Soundness of rule (2) can be shown by induction on n. To get started, we need to show fix f : A(0) which requires A(ı) to be of a special shape, for instance A(ı) = GRose^{ı} F B → C (this corresponds to Hughes, Pareto, and Sabry’s bottom check [HPS96]). Then A(0) denotes functions which have to behave well for all arguments in GRose^{0} F B, i. e., for no arguments, since GRose^{0} F B is empty. Trivially, any program fulfills this condition. In the step case, we need to show fix f : A(n + 1), but this follows from the equation fix f = f (fix f) since f : A(n) → A(n + 1), and fix f : A(n) by induction hypothesis.

In general, the index ı in A(ı) will be an ordinal number. Ordinals are useful when we want to speak of objects of unbounded size, e. g., generalized rose trees of height < ω that inhabit the type GRose^{ω} F A. Even more, ordinals are required to denote the height of infinitely branching trees: take generalized rose trees with F A = Nat → A. Other examples of infinite branching, which come from the area of type-theoretic theorem provers, are the W -type, Brouwer ordinals and the accessibility predicate [PM92].

In the presence of ordinal indices, rule (2) has to be proven sound by transfinite induction. In the case of a limit ordinal λ, we have to infer fix f : A(λ) from the induction hypothesis fix f : ∀α < λ. A(α). This imposes extra conditions on the shape of a so-called admissible type A, which are the object of this article. Of course, a monotone A is trivially admissible, but many interesting types for recursive functions are not monotone, like A(α) = Nat^{α} → Nat^{α} → Nat^{α} (where Nat^{α} contains the natural numbers < α). We will show that all those types A(α) are admissible that are upper semi-continuous in α, meaning lim sup_{α→λ} A(α) ⊆ A(λ) for limit ordinals λ. Function types C(α) = A(α) → B(α) will be admissible if A is lower semi-continuous (A(λ) ⊆ lim inf_{α→λ} A(α)) and B is upper semi-continuous. Similar laws will be developed for the other type constructors and put into the form of a kinding system for semi-continuous types.

Before we dive into the mathematics, let us make sure that semi-continuity is relevant for termination. A type which is not upper semi-continuous is A(ı) = (Nat^{ω} → Nat^{ı}) → Nat^{ω} (see Sect. 5). Assuming we can nevertheless use this type for a recursive function, we can construct a loop. First, define successor succ : ∀ı. Nat^{ı} → Nat^{ı+1} and predecessor pred : ∀ı. Nat^{ı+1} → Nat^{ı}. Note that the size index is an upper bound and ω is the biggest such bound for the case of natural numbers, thus, we have the subtyping relations Nat^{ı} ≤ Nat^{ı+1} ≤ ⋯ ≤ Nat^{ω} ≤ Nat^{ω+1} ≤ Nat^{ω}.

We make the following definitions:

A(ı) := (Nat^{ω} → Nat^{ı}) → Nat^{ω}
shift : ∀ı. (Nat^{ω} → Nat^{ı+1})
→ Nat^{ω} → Nat^{ı}
shift := λgλn. pred (g (succ n))

f  : ∀ı. A(ı) → A(ı + 1)
f  := λloopλg. loop (shift g)
loop : ∀ı. A(ı)
loop := fix f

Since Nat^{ω} → Nat^{0} is empty, A passes the bottom check. Still, instantiating types to succ : Nat^{ω} → Nat^{ω} and loop : (Nat^{ω} → Nat^{ω}) → Nat^{ω} we convince ourselves that the execution of loop succ indeed runs forever.

1.1. Related Work and Contribution. Ensuring termination through typing is quite an old idea, just think of type systems for the λ-calculus like simple types, System F, System F^{ω}, or the Calculus of Constructions, which all have the normalization property. These systems have been extended by special recursion operators, like primitive recursion in Gödel’s T, or the recursors generated for inductive definitions in Type Theory (e. g., in Coq). These recursion operators preserve normalization but limit the definition of recursive functions to special patterns, namely instantiations of the recursion scheme dictated by the recursion operator. Taming general recursion fix f through typing, however, which allows the definition of recursive functions in the intuitive way known from functional programming, is not yet fully explored. Mendler [Men87] pioneered this field; he used a certain polymorphic typing of the functional f to obtain primitive (co)recursive functions over arbitrary datatypes. Amadio and Coupet-Grimal [ACG98] and Giménez [Gim98] developed Mendler’s approach further, until a presentation using ordinal-indexed (co)inductive types was found and proven sound by Barthe et al. [BFG^{+}04]. The system λ presented in loc. cit. restricts types A(ı) of recursive functions to the shape μ^{ı}F → C(ı) where the domain must be an inductive type μ^{ı}F indexed by ı and the codomain a type C(ı) that is monotonic in ı. This criterion, which has also been described by the author [Abe04], allows for a simple soundness proof in the limit case of the transfinite induction, but excludes interesting types like the considered

Eq (GRose^{ı} F A) = GRose^{ı} F A → GRose^{ı} F A → Bool

which has an antitonic codomain C(ı) = GRose^{ı} F A → Bool. The author has in previous work widened the criterion, but only for a type system without polymorphism [Abe03]. Other recent works on type-based termination [Bla04, Bla05, BGP05] stick to the restriction of λ . Xi [Xi01] uses dependent types and lexicographic measures to ensure termination of recursive programs in a call-by-value language, but his indices are natural numbers instead of ordinals; this excludes infinite objects we are interested in.

Closest to the present work is the sized type system of Hughes, Pareto, and Sabry [HPS96], Synchronous Haskell [Par00], which admits ordinal indices up to ω. Index quantifiers as in ∀ı. A(ı) range over natural numbers, but can be instantiated to ω if A(ı) is ω-undershooting. Sound semantic criteria for ω-undershooting types are already present, but in a somewhat ad-hoc manner. We cast these criteria in the established mathematical framework of semi-continuous functions and provide a syntactical implementation in form of a derivation system. Furthermore, we allow ordinals beyond ω and infinitely branching inductive types that invalidate some criteria for the only finitely branching tree types in Synchronous Haskell. Finally, we allow polymorphic recursion, impredicative polymorphism and higher-kinded inductive and coinductive types such as GRose. This article summarizes the main results of the author’s dissertation [Abe06b]. A shorter version has appeared in the CSL’06 proceedings [Abe06c].

1.2. Contents. In Section 2 we introduce the syntax of F_{ω}, our λ-calculus with higherkinded polymorphism, recursion over higher-kinded inductive types and corecursion into higher-kinded coinductive types. Static semantics (i. e., typing rules) and dynamic semantics (i. e., reduction rules) are presented there, and we formally express the eqGRose-example from the introduction in F_{ω}. In Section 3 we model the types of F_{ω} as saturated sets of strongly normalizing terms in order to show termination of well-typed programs. After these two technical sections we come to the main part of this article: In Section 4 we identify compositional criteria for semi-continuous types and in Section 5 we justify the absence of certain composition schemes by giving counterexamples. These results are put in the form of a calculus for semi-continuous types in Section 6, culminating in syntactic rules for admissible (co)recursion types. We close by giving some practical examples for admissible types.

1.3. Preliminaries. We assume that the reader is to some extent acquainted with the higher-order polymorphic lambda-calculus, System F^{ω} (see Pierce’s text book [Pie02]) and has some knowledge of ordinals, inductive types, and strong normalization.

2. Overview of System F_{ω}

In this section we introduce F_{ω}, an a posteriori strongly normalizing extension of System F^{ω} with higher-kinded inductive and coinductive types and (co)recursion combinators. Figure 1 summarizes the syntactic entities.

2.1. Type constructors. We seek to model sized types like GRose^{ı}F A whose first parameter F is a type constructor of kind ∗ → ∗, meaning that it maps types to types. It is therefore suggestive to take F^{ω} as basis, which formalizes type constructors of arbitrary kind and, e. g., lays the foundation for the purely functional language Haskell. In the introduction, we have presented GRoses as built from two (data) constructors leaf and node; however, for a theoretic analysis it is more convenient to consider GRose F A as the least fixed-point of the type constructor λX. 1 + (A × F X). For this we write

GRose F A := μλX. 1 + (A × F X).

Herein, 1 is the unit type and + the disjoint sum. Taking the empty tuple ⟨⟩ : 1 to be the inhabitant of the unit type and inl : A → (A + B) and inr : B → (A + B) the two injections into the disjoint sum lets us define the original data constructors:

leaf : GRose F A
leaf := in (inl ⟨⟩)
node : A → F (GRose F A) → GRose F A
node := λaλfr. in (inr ⟨a, fr⟩)

(The tag in introduces a inductive type, see below.)

Polarities, kinds, constructors, kinding contexts.

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

Constructor constants and their kinds (κ →^{p} κ′ means pκ → κ′).

1 : ∗  unit type
+ : ∗ →^{+} ∗ →^{+} ∗  disjoint sum
× : ∗ →^{+} ∗ →^{+} ∗  cartesian product
→ : ∗ →^{−} ∗ →^{+} ∗  function space
∀_{κ} : (κ →^{∘} ∗) →^{+} ∗  quantification
μ_{κ_{∗}} : ord →^{+} (κ_{∗} →^{+} κ_{∗}) →^{+} κ_{∗}  inductive constructors
ν_{κ_{∗}} : ord →^{−} (κ_{∗} →^{+} κ_{∗}) →^{+} κ_{∗}  coinductive constructors
s : ord →^{+} ord successor of ordinal
∞ : ord  infinity ordinal

Objects (terms), values, evaluation frames, typing contexts.

r, s, t ::= c | x | λxt | r s  term
c  ::= ⟨⟩ | pair | fst | snd | inl | inr | case | in | out | fix_{n}^{μ} | fix_{n}^{ν} constant (n ∈ ℕ)
v  ::= λxt | pair t_{1} t_{2} | inl t | inr t | in t | c | pair t | fix_{n}^{∇}s t_{1..m} value (m ≤ n)
e( ) ::= s | fst | snd | case | out | fix_{n}^{μ} s t_{1..n}  evaluation frame
E( ) ::= e_{1}(… e_{n}( ) …)  evaluation context (n ≥ 0)
Γ ::= ⋄ | Γ, x:A | Γ, X:pκ typing context

Reduction t ⟶ t′.

(λxt) s  ⟶ [s/x]t
fst ⟨r, s⟩  ⟶ r
snd ⟨r, s⟩ ⟶ s
case (inl r) ⟶ λxλy. x r (∗)
case (inr r) ⟶ λxλy. y r (∗)

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

+ closure under all term constructs

(*) x, y ∉ FV(r).

Figure 1: F_{ω}: Syntax and operational semantics.

2.2. Polarized kinds. Negative recursive types such as μλX. X → 1 allow the coding of Y and other fixed-point combinators as pure λ-terms, so one can write recursive programs without special syntax for recursion [Men87]. For our purposes, this is counter-productive— type systems for termination need to identify all uses of recursion. Therefore, we restrict to positive recursive types μH where H is monotone. In the case of GRose, the underlying constructor H X = 1 + (A × F X) must be monotone, which is the case if F is monotone. So GRose F A is only well-formed for monotone F. To distinguish type constructors by their monotonicity behavior, also called variance, we equip function kinds with polarities p [Ste98], which are written before the domain or on top of the arrow. Polarity + denotes covariant constructors, − contravariant constructors and ∘ mixed-variant constructors [DC99]. For instance:

λX. X → 1  : ∗ →^{−} ∗
λX. X → X  : ∗ →^{∘} ∗
λX. Int → (1 + X) : ∗ →^{+} ∗
GRose  : (∗ →^{+} ∗) →^{+} ∗ →^{+} ∗

Abel [Abe06a] and Matthes [AM04] provide more explanation on polarities.

2.3. Sized inductive types. We refine inductive types μF to sized inductive types μ^{a}F. The first argument, a, to μ, which we usually write as superscript, denotes the upper bound for the height of data represented by terms of the inductive type. The index a is a constructor of kind ord and denotes an ordinal; the relevant ordinal expressions are given by the grammar

a ::= ı | s a | ∞

with ı an ordinal variable.^{1} If a actually denotes a finite ordinal (a natural number), then the height is simply the number of data constructors on the longest path in the tree structure of any element of μ^{a}F. Since a is only an upper bound, μ^{a}F is a subtype of μ^{b}F, written μ^{a}F ≤ μ^{b}F for a ≤ b, meaning that μ is covariant in the index argument. Finally, F ≤ F′ implies μ^{a}F ≤ μ^{a}F′, so we get the kinding

μ : ord →^{+} (∗ →^{+} ∗) →^{+} ∗

for the least fixed-point constructor. For the closure ordinal ∞, we have

μ^{∞}F = μ^{∞+1}F,

where ∞ + 1 is a shorthand for s∞, s : ord →^{+} ord being the successor on ordinals.

Because ∞ denotes the closure ordinal, the axiom s ∞ = ∞ is justified. Equality on type constructors is defined as the least congruent equivalence relation closed under this equation and βη.

At this point, let us stress that the syntax of ordinals is extremely simple, hence, equality of types and subtyping is decidable. The user can think of ordinals as of natural numbers with infinity, although they will be interpreted as real ordinals up to a fairly large closure ordinal in Section 3.

1One could add a constant for the ordinal 0, but for our purposes it is enough that each concrete data structure inhabits μ^{∞}F. For checking termination relative sizes are sufficient, which can be expressed using ordinal variables and successor.

Example 2.1 (Some sized types).

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

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

2.4. Sized coinductive types. Dually to inductive or least fixed-point types μF we have coinductive or greatest fixed-point types νF to model infinite structures. For instance StreamA = νX. A × X contains the infinite sequences over A. The dual to the height of an inductive data structure is the depth of a coinductive one, i.e., how often one can unwind the structure. So the size a of a sized coinductive type ν^{a}F is a lower bound on the depth of its inhabitants. Since it is a lower bound, coinductive types are contravariant in their size index:

ν : ord →^{−} (∗ →^{+} ∗) →^{+} ∗.

As for inductive types, the equation ν^{∞}F = ν^{∞+1}F holds.

Example 2.2 (Sized streams). On a stream in Stream^{a}A one can safely read off the first a elements.

Stream : ord →^{−} ∗ →^{+} ∗
Stream := λıλA. ν^{ı}λX. A × X

2.5. Heterogeneous datatypes. If we consider not only fixed-point types, but also fixedpoint constructors, we can treat programs involving so-called nested or heterogeneous types. A simple example of a heterogeneous type is the type of powerlists PList A which contains lists of As whose length is a power of two [Hin00a]. The type constructor PList : ∗ →^{+} ∗ can be modeled as μλXλA. A + X (A × A) which is the least fixed-point of a type constructor

of kind (∗ →^{+} ∗) →^{+} (∗ →^{+} ∗).

Sized heterogeneous types are obtained by simply generalizing μ and ν to

\begin{aligned}μ_{κ} & : & ord →^{+} (κ →^{+} κ) →^{+} κ \\ ν_{κ} & : & ord →^{−} (κ →^{+} κ) →^{+} κ. \end{aligned}

The kind κ is required to be pure, i. e., a kind not mentioning ord, for reasons explained in Section 3.4. All our examples work for pure κ.

Example 2.3 (Sized heterogeneous types).

PList : ord →^{+} ∗ →^{+} ∗
PList := λı. μ^{ı}λXλA. A + X (A × A)
Bush : ord →^{+} ∗ →^{+} ∗
Bush := λı. μ^{ı}λXλA. 1 + A × X (X A)
Lam : ord →^{+} ∗ →^{+} ∗
Lam := λı. μ^{ı}λXλA. A + X A × X A + X (1 + A)

The second type, Bush^{a} A, bushy lists, models finite maps from unlabeled binary trees of height < a into A [Alt01, Hin00b]. The third type, Lam^{a} A, is inhabited by de Bruijn representations of untyped lambda terms of height < a with free variables in A [BP99, AR99].

2.6. Programs. The term language of F_{ω} is the λ-calculus plus the standard constants to introduce and eliminate unit (1), sum (+), and product (×) types. We write ⟨t_{1}, t_{2}⟩ for pair t_{1} t_{2}. Further, there is folding, in, and unfolding, out, of (co)inductive types. The complete listing of the typing rules can be found in Figure 6 in the appendix, here we discuss the most important ones. Let κ = p⃗κ⃗ → ∗ a pure kind, F : +κ → κ, G_{i} : κ_{i} for 1 ≤ i ≤ |κ⃗|, a : ord, and ∇ ∈ {μ, ν}, then we have the following (un)folding rules:

ty-fold \frac{Γ ⊢ t : F (∇_{κ}^{a} F) G⃗}{Γ ⊢ in t : ∇_{κ}^{a+1}F G⃗}  ty-unfold \frac{Γ ⊢ r : ∇_{κ}^{a+1}F G⃗}{Γ ⊢ out r : F (∇_{κ}^{a} F) G⃗}

Finally, there are fixed-point combinators fix_{n}^{μ} and fix_{n}^{ν} for each n ∈ ℕ on the term level. The term fix_{n}^{μ} s denotes a recursive function with n leading non-recursive arguments; the n + 1st argument must be of an inductive type. Similarly, fix_{n}^{ν} s is a corecursive function which takes n arguments and produces an inhabitant of a coinductive type. We abbreviate f t_{1} … t_{n} by f t_{1..n} or f t⃗.

One-step reduction t ⟶ t′ is defined by the β-reduction axioms given in Figure 1 plus congruence rules. Its transitive closure is denoted by ⟶^{+}, and ⟶^{∗} is the reflexivetransitive closure. Interesting are the reduction rules for recursion and corecursion:

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

A recursive function is only unfolded if its recursive argument is a value, i. e., of the form in t. This condition is required to ensure strong normalization; it is present in the work of Mendler [Men87], Giménez [Gim98], Barthe et al. [BFG^{+}04], and the author [Abe04]. Dually, corecursive functions are only unfolded on demand, i. e., in an evaluation context, the matching one being out .

p ≤ p′  polarity ordering
Δ ⊢ F : κ  kinding
Δ ⊢ F = F′ : κ constructor equality
Δ ⊢ F ≤ F′ : κ higher-order subtyping
t ⟶ t′  reduction
Γ ⊢ t : A  typing
Γ ⊢ A fix_{n}^{∇}-adm admissible recursion type

Figure 2: F_{ω}: Judgements.

Figure 2 lists the basic judgements of F_{ω}, their rules can be found in the appendix. As pointed out in the introduction, recursion is introduced by the rule

ty-rec \frac{Γ ⊢ A fix_{n}^{∇}-adm Γ ⊢ a : ord}{Γ ⊢ fix_{n}^{∇} : (∀ı:ord. A ı → A (ı + 1)) → A a}.

Herein, ∇ stands for μ or ν, and the judgement A fix_{n}^{∇}-adm (see Def. 6.3) ensures that type A is admissible for (co)recursion, as discussed in the introduction. In this article, we will find out which types are admissible.

Example 2.4. Now we can code the example from the introduction in F_{ω}, with a suitable coding of true, false and ∧.

eqGRose : (∀A. Eq A → Eq (F A)) → ∀A. Eq A → ∀ı. Eq (GRose^{ı}F A)
eqGRose := λeqF λeqA.
fix_{0}^{μ}λeqλt_{1}λt_{2}. case (out t_{1})
(λ . case (out t_{2}) (λ . true) (λn_{2}. false))
(λn_{1}. case (out t_{2}) (λ . false)
(λn_{2}. (eqA (fst n_{1}) (fst n_{2})) ∧ (eqF eq (snd n_{1}) (snd n_{2}))))

Typing succeeds, by the following assignment of types to variables:

eqF : ∀A. Eq A → Eq (F A)
eqA : Eq A
eq : Eq (GRose^{ı}F A)

t_{1}, t_{2} : GRose^{ı+1}F A
: 1
n_{1}, n_{2} : A × F (GRose^{ı}F A)

More examples, including programs over heterogeneous types, can be found in the author’s thesis [Abe06b].

3. Semantics

Hughes, Pareto, and Sabry [HPS96] give a domain-theoretic semantics of sized types. We, however, follow Barthe et al. [BFG^{+}04] and interpret types as sets of terminating open expressions and show that any reduction sequence starting with a well-typed expression converges to a normal form. This is more than showing termination of programs (closed expressions); our results can be applied to partial evaluation and testing term equality in type-theoretic proof assistants.

The material in this section is quite technical, but provides the necessary basis for our considerations in the following sections. The reader may browse it, take a closer look at the interpretation of types (Sec. 3.5) and then continue with Section 4, coming back when necessary.

Let S denote the set of strongly normalizing terms. We interpret a type A as a semantic type ⟦A⟧ ⊆ S, and the function space is defined extensionally:

⟦A → B⟧ = {r | r s ∈ ⟦B⟧ for all s ∈ ⟦A⟧}.

As main theorem, we show that given a well-typed term x_{1} : A_{1}, … x_{n} : A_{n} ⊢ t : C and replacements s_{i} ∈ ⟦A_{i}⟧ for each occurring variable x_{i}, the substitution [s⃗/x⃗]t inhabits ⟦C⟧. The proof proceeds by induction on the typing derivation, and in the λ-case (here simplified)

\frac{x : A ⊢ t : B}{⊢ λxt : A → B}

it suffices to show (λxt) s ∈ ⟦B⟧ for any s ∈ ⟦A⟧. However, by induction hypothesis we know only [s/x]t ∈ ⟦B⟧. We therefore require semantic types to be closed under weak head expansion to make this case go through.

Since we are interested in normalization of open terms, we need to set aforementioned replacements s_{i} to variables x_{i}. This is possible if each semantic type contains all variables, which has to be generalized to all neutral terms, i.e. terms E[x] with a variable in evaluation position. These observations motivate our definition of semantic types.

3.1. Semantic types. We define safe (weak head) reduction ▷ by the following axioms. The idea is that semantic types are closed under ▷-expansion.

(λxt) s  ▷ [s/x]t if s ∈ S
fst (pair r s) ▷ r  if s ∈ S
snd (pair r s) ▷ s  if r ∈ S
out (in r) ▷ r

case (inl r)  ▷ λxλy. x r  (∗)
case (inr r)  ▷ λxλy. y r  (∗)
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})

Side condition (*): x, y ∉ FV(r). Additionally, we close safe reduction under evaluation contexts and transitivity:

\begin{matrix}E(t) & ▷ & E(t′) & if t ▷ t′ \\ t_{1} & ▷ & t_{3} & if t_{1} ▷ t_{2} and t_{2} ▷ t_{3} \end{matrix}

One-step safe reduction is deterministic, hence, if r ▷ s and r ▷ t then either s = t or s ▷ t or t ▷ s.

V := {v, E(x) | v value, E evaluation context}

is the set of ▷-normal forms, not counting junk terms like fst (λxt).

The relation is defined such that S is closed under ▷-expansion, meaning t ▷ t′ ∈ S implies t ∈ S. In other words, ▷ used in the expansion direction does not introduce diverging terms. Let ^{▷}A denote the closure of term set A under ▷-expansion. In general, the closure of term set A is defined as

\overline{A} = ^{▷}(A ∪ \{E(x) | x variable, E(x) ∈ S\}).

Closure preserves strong normalization: If A ⊆ S then \overline{A} ⊆ S. A term set is closed if \overline{A} = A. The least closed set is the set of neutral terms N := \overline{∅} ≠ ∅. Intuitively, a neutral term never reduces to a value, it necessarily has a free variable, and it can be substituted into any term without creating a new redex. A term set A is saturated if A is closed and N ⊆ A ⊆ S (this makes sure that A contains all variables). A saturated set is called a semantic type.

3.2. Interpretation of kinds. When types are interpreted as sets of terms, the easiest interpretation of type constructors are set-theoretical operators on term sets, or as we go higher-order, on operators.

The saturated sets form a complete lattice ⟦∗⟧ with least element ⊥^{∗} := N and greatest element ⊤^{∗} := S. It is ordered by inclusion ⊑^{∗} := ⊆ and has set-theoretic infimum inf^{∗} := ⋂ and supremum sup^{∗} := ⋃. Let ⟦ord⟧ := O where O = [0; ⊤^{ord}] is an initial segment of the set-theoretic ordinals. With the usual ordering on ordinals, O constitutes a complete lattice as well. For lattices 𝔏 and 𝔏′, let 𝔏 →^{+} 𝔏′ denote the space of monotone functions from 𝔏 to 𝔏′ and 𝔏 →^{−} 𝔏′ the space of antitone ones. The mixed-variant function kind ⟦∘κ → κ′⟧ is interpreted as set-theoretic function space ⟦κ⟧ → ⟦κ′⟧; the covariant function kind +κ → κ′ denotes the monotonic function space ⟦κ⟧ →^{+} ⟦κ′⟧ and the contravariant kind −κ → κ′ the antitonic space ⟦κ⟧ →^{−} ⟦κ′⟧. 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κ→κ′}.

3.3. Limits and iteration. Inductive types ⟦μ^{a}F ⟧ are constructed by iterating the operator ⟦F ⟧ ⟦a⟧-times, starting with the least semantic type ⊥. At limit ordinals, we take the supremum. If ⟦a⟧ is big enough, latest if ⟦a⟧ = ⊤^{ord}, the least fixed-point is reached, but our type system also provides notation for the approximation stages below the fixed-point. For coinductive types, we start with the biggest semantic type ⊤ and take the infimum at limits. It is possible to unify these two forms of iteration, by taking the lim sup instead of infimum or supremum at the limits. The notion of lim sup and iteration can be defined for arbitrary lattices:

In the following λ ∈ O will denote a limit ordinal. (We will only consider proper limits, i. e., λ ≠ 0.) For 𝔏 a complete lattice and f ∈ O → 𝔏 we define:

lim inf_{α→λ} f(α) := sup_{α_{0}<λ} inf_{α_{0}≤α<λ} f(α)
lim sup_{α→λ} f(α) := inf_{α_{0}<λ} sup_{α_{0}≤α<λ} f(α)

Using inf_{λ} f as shorthand for inf_{α<λ} f(α), and analogous shorthands for sup, lim inf, and lim sup, we have inf_{λ} f ⊑ lim inf_{λ} f ⊑ lim sup_{λ} f ⊑ sup_{λ} f. If f is monotone, then even lim inf_{λ} f = sup_{λ} f, and if f is antitone, then inf_{λ} f = lim sup_{λ} f.

If f ∈ 𝔏 → 𝔏 and g ∈ 𝔏, we define transfinite iteration f^{α}(g) by recursion on α as follows:

\begin{aligned}f^{0} & (g) & := & g \\ f^{α+1} & (g) & := & f(f^{α}(g)) \\ f^{λ} & (g) & := & lim sup_{α→λ} f^{α}(g) \end{aligned}

This definition of iteration works for any f, not just monotone ones. For monotone f, we obtain the usual approximants of least and greatest fixed-points as μ^{α}f = f^{α}(⊥) and ν^{α}f = f^{α}(⊤): It is easy to check that μ^{λ}f = sup_{α<λ} μ^{α}f and ν^{λ}f = inf_{α<λ} ν^{α}f, so our definition coincides with the usual one.

3.4. Closure ordinal. We can calculate an upper bound for the ordinal ⊤^{ord} at which all fixed-points are reached as follows: Let ℶ_{n} be a sequence of cardinals defined by ℶ_{0} = |ℕ| and ℶ_{n+1} = |P(ℶ_{n})|. For a pure kind κ, let |κ| be the number of ∗s in κ. Since ⟦∗⟧ consists of countable sets, |⟦∗⟧| ≤ |P(ℕ)| = ℶ_{1}, and by induction on κ, |⟦κ⟧| ≤ ℶ_{|κ|+1}. Since an (ascending or descending) chain in ⟦κ⟧ is shorter than |⟦κ⟧|, each fixed point is reached latest at the |⟦κ⟧|th iteration. Hence, the closure ordinal for all (co)inductive types can be approximated from above by ⊤^{ord} = ℶ_{ω}.

This calculation does not work if we allow fixed-points of constructors involving ord. Then the closure ordinal of such a fixed-point would depend on which ordinals are in the semantics of ord, which in turn would depend on what the closure ordinal for all fixed-points was—a vicious cycle. However, I do not see a practical example where one want to construct the fixed point of a sized-type transformer F : (ord →^{∘} κ) →^{+} (ord →^{∘} κ). Note that this does not exclude fixed-points inside fixed-points, such as

BTree^{ı,ȷ} A = μ^{ı}λX. 1 + X × (μ^{ȷ}λY. 1 + A × X × Y),

“B-trees” of height < ı with each node containing < ȷ keys of type A.

Example 3.1 (Number classes). Here we show that higher-kinded inductive types may require strictly higher closure ordinals than inductive types of kind ∗. Following Hancock [Han02], we can define the number classes as inductive types as follows:

NC_{0} := μ^{∞}λX. 1  ≅ 1
NC_{1} := μ^{∞}λX. 1 + (NC_{0} → X)  ≅ Nat^{∞}
NC_{2} := μ^{∞}λX. 1 + (NC_{0} → X) + (NC_{1} → X) ≅ μ^{∞}λX. 1 + X + (Nat^{∞} → X)
NC_{3} := μ^{∞}λX. 1 + (NC_{0} → X) + (NC_{1} → X) + (NC_{2} → X)
⋮

The second number class NC_{2} is also known as Brouwer ordinals. The law behind this scheme is: NC_{n} = μF_{n}, where F_{0} X = 1 and F_{n+1} X = F_{n} X + (μF_{n} → X). Each number class requires a higher closure ordinal, and their limit is the closure ordinal of all inductive types of kind ∗. Now let

NumClTree : ord →^{+} (∗ →^{+} ∗) →^{∘} ∗
NumClTree := λı. μ^{ı}λY λF. 1 + (μ^{∞}F → Y (λX. F X + (μ^{∞}F → X))).

Then NumClTree^{∞} (λX. 1) is the type of trees branching over the nth number class at the nth level.

3.5. Interpretation of types. For r a term, e an evaluation frame, and A a term set, let r · A = {r s | s ∈ A} and e^{−1}A = {r | e(r) ∈ A}. If e is strongly normalizing and A saturated, then e^{−1}A is again saturated. For saturated sets A, B ∈ ⟦∗⟧ we define the following saturated sets:

A + B := \overline{inl · A} ∪ \overline{inr · B}
A × B := (fst )^{−1}A ∩ (snd )^{−1}B
A → B := ⋂_{s∈A} ( s)^{−1}B

1 := \overline{\{⟨⟩\}}_{A^{μ} := \overline{in · A}}_{A^{ν} := (out )^{−1}A}

The last two notations are lifted pointwise to operators F ∈ ⟦pκ → κ′⟧ by setting F^{∇}(G) = (F(G))^{∇}, where ∇ ∈ {μ, ν}.

Remark 3.2. Our definition of product and function space (inspired by Vouillon [Vou04]) makes it immediate that × and → operate on saturated sets. But it is just a reformulation of the usual A × B = {r | fst r ∈ A and snd r ∈ B} and A → B = {r | r s ∈ B for all s ∈ A}.

Notice that the finitary or (in the logical sense) positive connectives 1, +, and μ are defined via introductions, while the infinitary or negative connectives → and ν are defined via eliminations. (The product fits in either category.)

For a constructor constant C:κ, the semantics ⟦C⟧ ∈ ⟦κ⟧ is defined as follows:

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

This semantics is extended to arbitrary constructors in the usual way. Let U = ⋃_{κ}⟦κ⟧. For a valuation θ which partially maps constructor variables X to their interpretation G ∈ U, we define the partial map ⟦−⟧_{θ} from constructors F to their interpretation in U by recursion on F.

⟦C⟧_{θ}  := ⟦C⟧
⟦X⟧_{θ}  := θ(X)
⟦F G⟧_{θ}  := ⟦F ⟧_{θ}(⟦G⟧_{θ})
⟦λX:κ. F ⟧_{θ} := \{ \begin{matrix}F & if F ∈ ⟦κ⟧ → ⟦κ′⟧ for some κ′ \\ undef. & else \end{matrix}
where F(G ∈ ⟦κ⟧) := ⟦F ⟧_{θ[X↦G]}

In the last clause, F is a partial function from ⟦κ⟧ to U.

The interpretation ⟦F ⟧_{θ} is well-defined for well-kinded F, and these are the only constructors we are interested in, but we chose to give a (possibly undefined) meaning to all constructors. If one restricts the interpretation to well-kinded constructors, one has to define it by recursion on kinding derivation and show coherence: If a constructor has two kinding derivations ending in the same kind, then the two interpretations coincide. This alternative requires a bit more work than our choice.

Lemma 3.3 (Basic properties of interpretation).

(1) Relevance: If θ(X) = θ′(X) for all X ∈ FV(F), then ⟦F ⟧_{θ} = ⟦F ⟧_{θ′}.

(2) Substitution: ⟦[G/X]F ⟧_{θ} = ⟦F ⟧_{θ[X↦⟦G⟧_{θ}]}.

Proof. Each by induction on F. For (2), consider case F = λY :κ. F′. W. l. o. g., Y ∉ FV(G). By induction hypothesis,

F(H) := ⟦[G/X]F ⟧_{θ[Y ↦H]} = ⟦F ⟧_{θ[Y ↦H][X↦⟦G⟧_{θ[Y ↦H]}]} = ⟦F ⟧_{θ[X↦⟦G⟧_{θ}][Y ↦H]},

using (1) on G. Hence, ⟦[G/X](λY :κ. F)⟧_{θ} = ⟦λY :κ. F ⟧_{θ[X↦⟦G⟧_{θ}]}.

Although the substitution property holds even for ill-kinded constructors, we only have for well-kinded constructors that ⟦(λX : κ. F) G⟧_{θ} = ⟦[G/X]F ⟧_{θ}. In general, the left hand side is less defined than the right hand side, e. g., ⟦(λX : ∗. 1) ∞⟧_{θ} is undefined, whereas the interpretation ⟦1⟧_{θ} of its β-reduct is well-defined. In the following we show that for well-kinded constructors the interpretation is well-defined and invariant under β.

Theorem 3.4 (Soundness of kinding, equality, and subtyping for constructors). Let θ ⊑ θ′ ∈ ⟦Δ⟧, meaning that for all (X : pκ′) ∈ Δ it holds that G := θ(X) ∈ ⟦κ′⟧ and G′ := θ′(X) ∈ ⟦κ′⟧, and G = G′ if p = ∘, G ⊑ G′ if p = +, and G′ ⊑ G if p = −.

(1) If Δ ⊢ F : κ then ⟦F ⟧_{θ} ⊑ ⟦F ⟧_{θ′} ∈ ⟦κ⟧.

(2) If Δ ⊢ F = F′ : κ then ⟦F ⟧_{θ} = ⟦F′⟧_{θ′} ∈ ⟦κ⟧.

(3) If Δ ⊢ F ≤ F′ : κ then ⟦F ⟧_{θ} ⊑ ⟦F′⟧_{θ′} ∈ ⟦κ⟧.

Proof. Simultaneously by induction on the derivation.

Now we can compute the semantics of types, e. g., ⟦Nat^{ı}⟧_{(ı↦α)} = Nat^{α} = μ^{α}(X ↦ (1 + X)^{μ}). Similarly, the semantic versions of List, Stream, etc. are denoted by List, Stream, etc.

3.6. Semantic admissibility and strong normalization. For the main theorem to follow, we assume semantic soundness of our yet to be defined syntactical criterion of admissibility (Def. 6.3).

Assumption 3.5 (Semantic admissibility). If Γ ⊢ A fix_{n}^{∇}-adm and θ(X) ∈ ⟦κ⟧ for all (X:κ) ∈ ⟦Γ⟧ then A := ⟦A⟧_{θ} ∈ ⟦ord⟧ → ⟦∗⟧ has the following properties:

(1) Shape: A(α) = ⋂_{k∈K} B_{1}(k, α) → … → B_{n}(k, α) → B(k, α) for some K and some

B_{1}, …, B_{n}, B ∈ K × ⟦ord⟧ → ⟦∗⟧. In case ∇ = μ, B(k, α) = I(k, α)^{μ} → C(k, α) for

some I, C. Otherwise, B(k, α) = C(k, α)^{ν} for some C.

(2) Bottom-check: I(k, 0)^{μ} = ⊥^{∗} in case ∇ = μ and C(k, 0)^{ν} = ⊤^{∗} in case ∇ = ν.

(3) Limit-check: inf_{α<λ} A(α) ⊆ A(λ) for all limit ordinals λ ∈ ⟦ord⟧ \ {0}.

In case of recursion (∇ = μ), the condition (1) ensures that fix_{n}^{μ}s really produces a function whose n+1st argument is of something that looks like an inductive type (I(k, α)^{μ}). The function can be polymorphic, therefore the intersection ⋂_{k∈K} over an index set K. Condition (2) requires I to exhibit at least for α = 0 the behavior of an inductive type: I(k, 0)^{μ} = ⊥^{∗}, which is equivalent to I(k, 0) = ∅. The technical condition (3) is used in the following theorem and will occupy our attention for the remainder of this article. In case of corecursion (∇ = ν), condition (1) ensures that fix_{n}^{ν}s maps n arguments into something like a coinductive type (C(k, α)^{ν}), which needs to cover the whole universe ⊤^{∗} of terms for α = 0.

Now we show soundness of our typing rules, which entails strong normalization. Let tθ denote the simultaneous substitution of θ(x) for each x ∈ FV(t) in t.

Theorem 3.6 (Soundness of typing). Assume that the judgement Γ ⊢ A fix_{n}^{∇}-adm is sound, as stated above. Let θ(X) ∈ ⟦κ⟧ for all (X: κ) ∈ Γ and θ(x) ∈ ⟦A⟧_{θ} for all (x: A) ∈ Γ. If Γ ⊢ t : B then tθ ∈ ⟦B⟧_{θ}.

Proof. By induction on the typing derivation. We consider the recursion rule (ty-rec for ∇ = μ).

ty-rec \frac{Γ ⊢ A fix_{n}^{μ}-adm  Γ ⊢ a : ord}{Γ ⊢ fix_{n}^{μ} : (∀ı:ord. A ı → A (ı + 1)) → A a}

By hypothesis, A := ⟦A⟧_{θ} ∈ ⟦ord⟧ → ⟦∗⟧ is admissible, and α := ⟦a⟧_{θ} ∈ ⟦ord⟧. Assume an s ∈ ⟦∀ı: ord. A ı → A (ı + 1)⟧_{θ} ⊆ ⋂_{β<⊤^{ord}} A(β) → A(β + 1). We show fix_{n}^{μ} s ∈ A(α) by transfinite induction on α.

In the base case α = 0, A(0) = ⋂_{k∈K} B_{1..n}(k, 0) → ⊥^{∗} → C(k, 0). We assume k ∈ K, t_{i} ∈ B_{i}(k, 0), then e(r) := fix_{n}^{μ} s t_{1..n} r is a strongly normalizing evaluation frame. Since each r ∈ ⊥^{∗} = N is neutral, we have e(r) ∈ N ⊆ C(k, 0).

In the step case, A(α + 1) = ⋂_{k∈K} B_{1..n}(k, α + 1) → I(k, α + 1)^{μ} → C(k, α + 1). We assume k ∈ K, t_{i} ∈ B_{i}(k, α + 1), and r ∈ I(k, α + 1)^{μ}, which means that either r is neutral—then we continue as in the previous case—or r▷in r′. Now fix_{n}^{μ} s t⃗r▷fix_{n}^{μ} s t⃗(in r′)▷ s (fix_{n}^{μ} s) t⃗(in r′). The last term inhabits C(k, α + 1), since fix_{n}^{μ} s ∈ A(α) by induction hypothesis and therefore s (fix_{n}^{μ} s) ∈ A(α + 1).

Finally, in the limit case, fix_{n}^{μ} s ∈ A(α) for all α < λ by induction hypothesis. Since ⋂_{α<λ} A(α) = inf_{α<λ} A(α) ⊆ A(λ), we are done.

Corollary 3.7 (Strong normalization). If Γ ⊢ t : B then t is strongly normalizing.

Proof. From soundness of typing, taking a valuation θ with θ(x) = x for all term variables x and θ(X) = ⊤^{κ} for all (X:pκ) ∈ Γ.

4. Semi-Continuity

As motivated in the introduction, only types C ∈ ⟦ord⟧ → ⟦∗⟧ which satisfy the limitcheck inf_{λ} C ⊑ C(λ) can be admissible for recursion. In this section we develop a compositional criterion for admissible types. The limit-check itself is not compositional since it does not sensibly distribute over function spaces: To show inf_{α<λ}(A(α) → B(α)) ⊑ A(λ) → B(λ) from inf_{λ} B ⊑ B(λ) requires A(λ) ⊑ inf_{λ} A, which is not even true for A(α) = Nat^{α} at limit ω. However, the criterion lim sup_{λ} C ⊑ C(λ) entails the limit-check, and it distributes reasonably over the function space:

Proposition 4.1. If A(λ) ⊑ lim inf_{λ} A and lim sup_{λ} B ⊑ B(λ) then lim sup_{λ}(A(α) →

B(α)) ⊑ A(λ) → B(λ).

This proposition will reappear (and proven) as Cor. 4.8. Note that Nat^{ω} = lim inf_{ω} Nat, hence, A(α) = Nat^{α} can now serve as the domain of an admissible function space, which is the least we expect.

The conditions on A and B in the lemma are established mathematical terms: They are subconcepts of continuity. In this article, we consider only functions f ∈ O → 𝔏 from ordinals into some lattice 𝔏. For such f, the question whether f is continuous in point α only makes sense if α is a limit ordinal, because only then there are infinite nonstationary sequences which converge to α; and since every strictly decreasing sequence is finite on ordinals (well-foundedness!), it only makes sense to look at ascending sequences, i. e., approaching the limit from the left. Hence, function f is upper semi-continuous in λ, if lim sup_{λ} f ⊑ f(λ), and lower semi-continuous, if f(λ) ⊑ lim inf_{λ} f. If f is both upper and lower semi-continuous in λ, then it is continuous in λ (then upper and lower limit coincide with f(λ)).

In the following we identify sufficient criteria for sum, product, function, inductive, and coinductive types to be semi-continuous.

4.1. Semi-continuity from monotonicity.

Obviously, any monotone function is upper semi-continuous, and any antitone function is lower semi-continuous. Now consider a monotone f with f(λ) = sup_{λ} f, as it is the case for an inductive type f(α) = μ^{α}F (where F does not depend on α). Since for monotone f, sup_{λ} f = lim inf_{λ} f, f is lower semi-continuous. This criterion can be used with Prop. 4.1 to show upper semi-continuity of function types with inductive domain, such as Eq(GRose^{ı} F A) (see introduction) and, e. g.,

C(α) = Nat^{α} → List^{α}(A) → C′(α)

where C′(α) is any monotonic type-valued function, for instance, List^{α}(Nat^{α}), and A is some constant type: The domain types, Nat^{α} and List^{α}(A), are lower semi-continuous according the just established criterion and the monotonic codomain C′(α) is upper semi-continuous, hence, Prop. 4.1 proves upper semi-continuity of C. Note that this criterion fails us if we replace the domain List^{α}(A) by List^{α}(Nat^{α}), or even μ^{α}(F(Nat^{α})) for some monotone F, since it is not immediately obvious that

μ^{ω}(F(Nat^{ω})) = sup_{α<ω} μ^{α}(F(sup_{β<ω} Nat^{β})) =^{?} sup_{γ<ω} μ^{γ}(F(Nat^{γ})).

However, domain types where one indexed inductive type is inside another inductive type are useful in practice, see Example 6.6. Before we consider lower semi-continuity of such types, let us consider the dual case.

For f(α) = ν^{α}F, F not dependent on α, f is antitone and f(λ) := lim sup_{λ} f = inf_{λ} f, hence, f is continuous in all limits. This establishes upper semi-continuity of a type involved in stream-zipping,

Stream^{α}(A) → Stream^{α}(B) → Stream^{α}(C).

However, types like Stream^{α}(Nat^{α}) are not yet covered, but now we will develop concepts that allow us to look inside (co)inductive types.

4.2. Simple semi-continuous types. First we will investigate how disjoint sum, product, and function space operate on semi-continuous types.

Definition 4.2. Let f ∈ 𝔏 → 𝔏′. We say lim sup pushes through f, or f is lim sup-pushable, if for all g ∈ O → 𝔏,

lim sup_{α→λ} f(g(α)) ⊑ f(lim sup_{λ} g).

Analogously, f is lim inf-pullable, or lim inf can be pulled out of f, if for all g,

f(lim inf_{λ} g) ⊑ lim inf_{α→λ} f(g(α)).

These notions extend straightforwardly to fs with several arguments.

Lemma 4.3 (Facts about limits).

(1) sup_{i∈I} lim inf_{α→λ} h(α, i) ⊑ lim inf_{α→λ} sup_{i∈I} h(α, i).

(2) lim sup_{α→λ} inf_{i∈I} h(α, i) ⊑ inf_{i∈I} lim sup_{α→λ} h(α, i).

(3) lim sup_{α→λ} inf_{i∈I(α)} h(α, i) ⊑ inf_{i∈lim inf_{λ} I} lim sup_{α→λ} h(α, i).

Fact (2) states that lim sup pushes through infimum, setting 𝔏 = K → 𝔏′ for some set K ⊇ I, f(g′) = inf_{i∈I} g′(i), and g(α)(i) = h(α, i) in the above definition. Thus, universal quantification is lim sup-pushable, which justifies rule cont-∀ in Figure 3 (see Sect. 6). The dual fact (1) expresses that lim inf can be pulled out of a supremum.

Fact (3) is a generalization of (2) which we will need to show semi-continuity properties of the function space.

Proof. In the following proof of (3), let all ordinals range below λ. First we derive

h(α, i) ⊑ sup_{α≥α_{0}} h(α, i)  for α ≥ α_{0}
inf_{i∈I(α)} h(α, i) ⊑ inf_{i∈⋂_{α≥α_{0}} I(α)} sup_{α≥α_{0}} h(α, i) for α ≥ α_{0}
sup_{α≥α_{0}} inf_{i∈I(α)} h(α, i) ⊑ inf_{i∈inf_{α≥α_{0}} I(α)} sup_{α≥α_{0}} h(α, i).

(I(α) is a set, so intersection = infimum.) Secondly, note that

inf_{α_{0}} inf_{i∈J(α_{0})} g(α_{0}, i) = inf_{α_{0},i∈J(α_{0})} inf_{α_{0}} g(α_{0}, i) = inf_{i∈sup_{α_{0}} J(α_{0})} inf_{α_{0}} g(α_{0}, i).

With g(α_{0}, i) := sup_{α≥α_{0}} h(α, i) and J(α_{0}) := inf_{α≥α_{0}} I(α) we finally derive

lim sup_{α→λ} inf_{i∈I(α)} h(α, i) =
inf_{α_{0}} sup_{α≥α_{0}} inf_{i∈I(α)} h(α, i) ⊑ inf_{α_{0}} inf_{i∈inf_{α≥α_{0}} I(α)} sup_{α≥α_{0}} h(α, i)
= inf_{i∈sup_{α_{0}} inf_{α≥α_{0}} I(α)} inf_{α_{0}} sup_{α≥α_{0}} h(α, i)
= inf_{i∈lim inf_{λ} I} lim sup_{α→λ} h(α, i).

Lemma 4.4 (lim inf can be pulled out of the building blocks of saturated sets).

(1) r · lim inf_{λ} A  ⊆ lim inf_{α→λ}(r · A(α)).
(2) e^{−1}(lim inf_{λ} A)  ⊆ lim inf_{α→λ} e^{−1}(A(α)).
(3) lim inf_{λ} A ∩ lim inf_{λ} B ⊆ lim inf_{α→λ}(A(α) ∩ B(α)).
(4) ^{▷}( lim inf_{λ} A)  ⊆ lim inf_{α→λ} ^{▷}(A(α)).

Proof. All propositions have easy proofs. Let all introduced ordinals range below λ. For proposition (3), assume r ∈ lim inf_{λ} A ∩ lim inf_{λ} B, which means that there are α_{0}, β_{0} such that r ∈ A(α) for all α with α_{0} ≤ α and r ∈ B(β) for all β with β_{0} ≤ β. We have to show that there exists γ_{0} such that r ∈ A(γ) ∩ B(γ) for all γ with γ_{0} ≤ γ. Choose γ_{0} := max(α_{0}, β_{0}). Notice that even lim inf_{λ} A ∩ lim inf_{λ} B = lim inf_{α→λ}(A(α) ∩ B(α)), since the reverse direction is follows immediately from A(α) ∩ B(α) ⊆ A(α), B(α).

For proposition (4), assume r▷r′ ∈ lim inf_{λ} A. There exists α_{0} such that for all α ≥ α_{0}, we have r′ ∈ A(α), and thus, r ∈ ^{▷}(A(α)). It follows that r ∈ lim inf_{α→λ} ^{▷}(A(α)).

The last lemma can be dualized to lim sup:

Lemma 4.5 (lim sup pushes through the building blocks of saturated sets).

(1) lim sup_{α→λ}(r · A(α))  ⊆ r · lim sup_{λ} A.
(2) lim sup_{α→λ} e^{−1}(A(α)) ⊆ e^{−1}(lim sup_{λ} A).
(3) lim sup_{α→λ}(A(α) ∪ B(α)) ⊆ lim sup_{λ} A ∪ lim sup_{λ} B. (only classically!)
(4) lim sup_{α→λ} ^{▷}(A(α))  ⊆ ^{▷}( lim sup_{λ} A) if A(α) ⊆ V for all α < λ.

Proof. The first three propositions follow trivially since the infimum and supremum considered are set-theoretic intersection and union. Note that proposition (3) is valid in classical logics but not in intuitionistic logics: An r which inhabits infinitely many unions A(α) ∪ B(α), must classically inhabit infinitely many A(α) or infinitely many B(α). But we cannot tell which of these alternatives holds, so the proposition has no intuitionistic proof. However, we will not need this proposition for the results to follow.

For the last proposition, assume r ∈ lim sup_{α→λ} ^{▷}(A(α)). If we require all following ordinals < λ, this means that for arbitrary α_{0} there exist α ≥ α_{0} and r′ ∈ A(α) such that r ▷ r′. Since each r′ ∈ V and safe reduction into V is deterministic, there is in fact a unique r′ ∈ ⋃_{α≥α_{0}} A(α) with r ▷ r′ for all α, hence, r ∈ ^{▷}( lim sup_{λ} A).

Proposition (4) of Lemma 4.5 fails if we drop the condition A(α) ⊆ V: Let t_{i} = out^{i+1}(fix_{0}^{ν} out) and observe that t_{i} ▷ t_{i+1}. Setting A(n) := {t_{i} | i ≥ n} we have t_{0} ∈ inf_{n<ω} ^{▷}(A(n)) ⊆ lim sup_{n→ω} ^{▷}(A(n)), but lim sup_{ω} A = inf_{ω} A = ∅, thus, t_{0} ∉ ^{▷}( lim sup_{ω} A). It did not help that the A(n) were closed unter ▷-reduction.

Lemma 4.6. Binary sums + and products × and the operations (−)^{μ} and (−)^{ν} are lim suppushable and lim inf-pullable.

Proof. Directly by the last lemmata. For instance,

(lim inf_{λ} A) × (lim inf_{λ} B) = (fst^{−1} lim inf_{λ} A) ∩ (snd^{−1} lim inf_{λ} B)
⊆ (lim inf_{α→λ} fst^{−1}A(α)) ∩ (lim inf_{β→λ} snd^{−1}B(β))
⊆ lim inf_{γ→λ}(fst^{−1}A(γ) ∩ snd^{−1}B(γ))
= lim inf_{γ→λ}(A(γ) × B(γ)).

Because we wish to avoid classical reasoning (Lemma 4.5 (3)) as much as possible, pushing lim sup through disjoint sums requires a closer look: Assume r ∈ lim sup_{γ→λ}(A(γ) + B(γ)), hence, for some γ, either r ▷ inl r′ for some r′ ∈ A(γ), or r ▷ inr r′ for some r′ ∈ B(γ), or r ∈ N. Since safe reduction ▷ is deterministic, and N does not contain values, one of these three alternatives must hold whenever r ∈ A(γ) + B(γ) for some γ. So either r ∈ ▷(inl · (lim sup_{λ} A)), or r ∈ ^{▷}(inr · (lim sup_{λ} B)), or r ∈ N, which means r ∈ (lim sup_{λ} A) + (lim sup_{λ} B).

Analogously, we show that lim sup pushes through (·)^{μ}.

Using monotonicity of the product constructor, the lemma entails that A(α) × B(α) is upper/lower semi-continuous if A(α) and B(α) are. This applies also for +.

Theorem 4.7 (Pushing lim sup through function space). lim sup_{α→λ} (A(α) → B(α)) ⊆ (lim inf_{λ} A) → lim sup_{λ} B.

Proof. We use Lemma 4.3 (3).

lim sup_{α→λ} (A(α) → B(α)) = lim sup_{α→λ} ⋂_{s∈A(α)}( s)^{−1}B(α)
⊆ ⋂_{s∈lim inf_{λ} A} lim sup_{α→λ}( s)^{−1}B(α)
⊆ ⋂_{s∈lim inf_{λ} A}( s)^{−1}(lim sup_{λ} B)
= (lim inf_{λ} A) → lim sup_{λ} B.

Corollary 4.8. If A(λ) ⊑ lim inf_{λ} A and lim sup_{λ} B ⊑ B(λ) then lim sup_{λ}(A(α) →

B(α)) ⊑ A(λ) → B(λ).

4.3. Coinductive types preserve upper semi-continuity. We have already seen that Stream^{α}(Nat^{ω}) is upper semi-continuous. In this section, we establish means to show that also a type like Stream^{α}(Nat^{α}) is upper semi-continuous (which is, by the way, isomorphic

to Nat^{α} → Nat^{α}).

Definition 4.9. A family F_{α} ∈ 𝔏 → 𝔏′ (α ∈ O) is called lim sup-pushable if for any G_{(−)} ∈ O → 𝔏,

lim sup_{α→λ} F_{γ}(G_{α}) ⊑ F_{γ}(lim sup_{α→λ} G_{α})  for all γ ∈ O,
lim sup_{α→λ} F_{α}(G_{α}) ⊑ F_{λ}(lim sup_{α→λ} G_{α})  for all limits λ > 0.

The first property is easier to prove, but not entailed by the second property. Usually we will confine in showing the second.

Lemma 4.10. Let F_{α} ∈ 𝔏⃗ → 𝔏 →^{+} 𝔏 be a family which is lim sup-pushable in all arguments.. Then for all β the family

\begin{matrix}H_{α} ∈ 𝔏⃗ → 𝔏 \\ H_{α}(G⃗) = ν^{β}(F_{α}(G⃗)) \end{matrix}

is lim sup-pushable. Proof. By transfinite induction on β we prove for all G_{i} ∈ O → 𝔏_{i} that

lim sup_{α→λ} ν^{β}(F_{α}(G⃗_{α})) ⊑ ν^{β}F_{λ}(lim sup_{λ} G⃗).

In case β = 0, both sides become the maximum element of 𝔏. In the successor case we have

lim sup_{α→λ} ν^{β+1}(F_{α}(G⃗_{α})) = lim sup_{α→λ} F_{α}(G⃗_{α})(ν^{β}(F_{α}(G⃗_{α})))
⊑ F_{λ}(lim sup_{λ} G⃗)(lim sup_{α→λ} ν^{β}(F_{α}(G⃗_{α}))) F_{α} pushable
⊑ F_{λ}(lim sup_{λ} G⃗)(ν^{β}(F_{λ}(lim sup_{λ} G⃗)))  F_{α} monotone, i.h.
= ν^{β+1}(F_{λ}(lim sup_{λ} G⃗)).

In the remaining case β = λ we exploit that lim sup pushes through infima (Lemma 4.3.2).

In the remainder of this part we will show that lim sup_{α<λ} ν^{ϕ(α)}F_{α} ⊑ ν^{lim inf_{λ} ϕ}F_{λ}. This will enable us to show that types like Stream^{α}(Nat^{α}) are lim sup-pushable.

In the following, we will need additional properties of lim sup. For the value of lim inf_{λ} f and lim sup_{λ} f, only the behavior of f on a final segment of [0; λ[ is relevant: Lemma 4.11 (Limit starting later). Let all ordinal range below λ.

(1) inf_{β_{0}≥α_{0}} sup_{β≥β_{0}} f(β) = inf_{γ_{0}≥0} sup_{γ≥γ_{0}} f(γ).
(2) sup_{β_{0}≥α_{0}} inf_{β≥β_{0}} f(β) = sup_{γ_{0}≥0} inf_{γ≥γ_{0}} f(γ).

Proof. We show (1), the proof of (2) is analogous. Direction ⊒ follows by monotonicity of inf. For ⊑, we have to show that for all γ_{0} there exists a β_{0} ≥ α_{0} such that

sup_{β≥β_{0}} f(β) ⊑ sup_{γ≥γ_{0}} f(γ).

Take β_{0} = max(γ_{0}, α_{0}). Lemma 4.12 (Splitting limits).

(1) lim sup_{β→λ} h(β, β) ⊑ lim sup_{α→λ} lim sup_{β→λ} h(α, β) for h ∈ O →^{−} O → 𝔏,
(2) lim inf_{α→λ} lim inf_{β→λ} h(α, β) ⊑ lim inf_{β→λ} h(β, β) for h ∈ O →^{+} O → 𝔏.

Proof. Again, we show just (1). Because of antitonicity, we have for all α,

h(β, β)  ⊑ h(α, β)  for all β ≥ α
sup_{β≥β_{0}} h(β, β)  ⊑ sup_{β≥β_{0}} h(α, β)  for all β_{0} ≥ α
inf_{β_{0}≥α} sup_{β≥β_{0}} h(β, β) ⊑ inf_{β_{0}≥α} sup_{β≥β_{0}} h(α, β)
lim sup_{β→λ} h(β, β) ⊑ lim sup_{β→λ} h(α, β) by Lemma 4.11.

The goal follows by taking lim sup on the r.h.s.

Next, we show how to push a lim sup into ν^{(−)}.

Lemma 4.13. Let ϕ ∈ O → O and I ⊆ O. Then (1) sup_{α∈I} ν^{ϕ(α)} ⊑ ν^{inf_{I} ϕ},

(2) sup_{α∈I} ν^{ϕ(α)} ⊒ ν^{inf_{I} ϕ},

(3) inf_{α∈I} ν^{ϕ(α)} ⊒ ν^{sup_{I} ϕ}, and

(4) inf_{α∈I} ν^{ϕ(α)} ⊑ ν^{sup_{I} ϕ}.

Proof. (1) and (3) follow directly from antitonicity. For (2), remember that each set of ordinals is left-closed, hence inf_{I} ϕ = ϕ(α) for some α ∈ I. The remaining proposition (4) is proven by cases on sup_{I} ϕ. If sup_{I} ϕ is not a limit ordinal then sup_{I} ϕ = ϕ(α) for some α ∈ I. For this α, clearly ν^{ϕ(α)} ⊑ ν^{sup_{I} ϕ}, which entails the lemma. Otherwise, if sup_{I} ϕ is a limit ordinal, then by definition of ν at limits we have to show inf_{α∈I} ν^{ϕ(α)} ⊑ ν^{β} for all β < sup_{I} ϕ. By definition of the supremum, β < ϕ(α) for some α. Since ν is antitone, ν^{ϕ(α)} ⊑ ν^{β} from which we infer our subgoal by forming the infimum on the left hand side.

Corollary 4.14. lim sup_{α→λ} ν^{ϕ(α)} = ν^{lim inf_{λ} ϕ}.

Now we have the tools in hand to prove that coinductive types preserve upper semicontinuity. In the second part of the following theorem, we make use of the fact that our coinductive types close at ordinal ω.

Theorem 4.15 (Upper semi-continuity of coinductive types). Let F_{α} ∈ 𝔏⃗ → 𝔏 →^{+} 𝔏 be a family which is lim sup-pushable in all arguments and ϕ ∈ O →^{+} O. Then

lim sup_{α→λ} ν^{ϕ(α)}(F_{α}(G⃗_{α})) ⊑ ν^{(lim inf_{λ} ϕ)}(F_{λ}(lim sup_{λ} G⃗)).

If ϕ is constant or affine, then even

lim sup_{α→λ} ν^{ϕ(α)}(F_{α}(G⃗_{α})) ⊑ ν^{ϕ(λ)}(F_{λ}(lim sup_{λ} G⃗)).

Proof. Direct. Note that ν^{ϕ(−)} is antitone, so we can split the lim sup.

lim sup_{α→λ} ν^{ϕ(α)}(F_{α}(G⃗_{α})) ⊑ lim sup_{α→λ} lim sup_{γ→λ} ν^{ϕ(α)}(F_{γ}(G⃗_{γ})) Lemma 4.12
⊑ lim sup_{α→λ} ν^{ϕ(α)}(F_{λ}(lim sup_{λ} G⃗))  Lemma 4.10
⊑ ν^{lim inf_{α→λ} ϕ(α)}(F_{λ}(lim sup_{λ} G⃗))  Cor. 4.14.

Now if ϕ is constant, then lim inf_{λ} ϕ = ϕ(λ). If ϕ is affine, then surely ϕ(λ) ≥ ω, and also lim inf_{λ} ϕ ≥ ω. We only need to show that in our case the greatest fixed-point is reached already at iteration ω. Observe that H(X) := F_{λ}(lim sup_{λ} G⃗)(X) is lim sup-pushable, since the family F is. It suffices to show that ν^{ω}H ⊑ ν^{ω+1}H.

ν^{ω}H = lim sup_{β→ω} ν^{β}H  = lim sup_{β→ω} ν^{β+1}H = lim sup_{β→ω} H(ν^{β}H)
⊑ H(lim sup_{β→ω} ν^{β}H) = ν^{ω+1}H.

Thus, ν^{ω+1}H = ν^{ω}H, which means that ν^{β}H = ν^{ω}H for all β ≥ ω; the fixed-point is reached.

For example, since F_{α}(X) = (Nat^{α} × X)^{ν} is lim sup-pushable, we have can infer upper semi-continuity of Stream^{α}(Nat^{α}) = ν^{α}F_{α}.

4.4. Inductive types preserve lower semi-continuity. We can dualize the results of the last section and prove that inductive types preserve lower semi-continuity and lim suppushability.

Definition 4.16. A family F_{α} ∈ 𝔏 → 𝔏′ (α ∈ O) is called lim inf-pullable if for all G_{(−)} ∈ O → 𝔏,

F_{γ}(lim inf_{α→λ} G_{α}) ⊑ lim inf_{α→λ} F_{γ}(G_{α})  for all γ ∈ O,
F_{λ}(lim inf_{α→λ} G_{α}) ⊑ lim inf_{α→λ} F_{α}(G_{α})  for all limits λ > 0.

Lemma 4.17. Let F_{α} ∈ 𝔏⃗ → 𝔏 →^{+} 𝔏 be a family which is lim inf-pullable in all arguments. Then,

(1) μ^{β}(F_{(−)}(−)) is a lim inf-pullable family,

(2) μ^{(lim inf_{λ} ϕ)} = lim inf_{α→λ} μ^{ϕ(α)}.

Theorem 4.18 (Lower semi-continuity of inductive types). Let F_{α} ∈ 𝔏⃗ → 𝔏 →^{+} 𝔏 be a family which is lim inf-pullable in all arguments and ϕ ∈ O →^{+} O. Then

μ^{(lim inf_{λ} ϕ)}(F_{λ}(lim inf_{λ} G⃗)) ⊑ lim inf_{α→λ} μ^{ϕ(α)}(F_{α}(G⃗_{α})).

If ϕ is lower semi-continuous, then even

μ^{ϕ(λ)}(F_{λ}(lim inf_{λ} G⃗)) ⊑ lim inf_{α→λ} μ^{ϕ(α)}(F_{α}(G⃗_{α})).

Putting together the conditions ϕ is required to be monotone and continuous in the second statement of the theorem. Since ϕ is coming from a size expression in our case, such a ϕ will either be the identity or a constant function. (The successor function is not continuous!)

Using Thm. 4.18, we can establish lower semi-continuity of List^{α}(Nat^{α}).

5. Non Semi-Continuous Types

This section is devoted to show that our list of criteria for semi-continuity is somewhat complete. Concretely, we demonstrate that there is no compositional scheme to establish lower semi-continuity of function types or upper semi-continuity of inductive types.

5.1. Function space and lower semi-continuity. One may wonder whether Cor. 4.8 can be dualized, i. e., does upper semi-continuity of A and lower semi-continuity of B entail lower semi-continuity of C(α) = A(α) → B(α)? The answer is no, e. g., consider C(α) = Nat^{ω} → Nat^{α}. Although A(α) = Nat^{ω} is trivially upper semi-continuous, and B(α) = Nat^{α} is lower semi-continuous, C is not lower semi-continuous: For instance, the identity function is in C(ω) but in no C(α) for α < ω, hence, also not in lim inf_{ω} C. And indeed, if this C was lower semi-continuous, then our criterion would be unsound, because then by Cor. 4.8 the type (Nat^{ω} → Nat^{α}) → Nat^{ω}, which admits a looping function (see introduction), would be upper semi-continuous.

Nevertheless, there are some lower semi-continuous function spaces, for instance, if the domain is a finite type. For example, Bool → Nat^{α} is lower semi-continuous in α, which

22

implies that (Bool → Nat^{α}) → Nat^{α} could be admissible. This is the type of a maximum function taking its two inputs in form of a function over booleans (Bool → Nat^{α} ≅ Nat^{α} × Nat^{α}). However, this example is somewhat contrived; it is not clear whether such cases appear in practice, so we will not pursue this further here.

5.2. Inductive types and upper semi-continuity. Pareto [Par00] proves that inductive types are (in our terminology) lim sup-pushable. His inductive types denote only finitely branching trees, but we also consider infinite branching, arising from function space embedded in inductive types. Such an infinitely branching type is the type of hungry functions (which consumes one argument after the other):

Hungry : ord →^{+} ∗ →^{−} ∗
Hungry := λıλA. μ^{ı}λX. A → X.

We are interested in the special case of Hungry^{ı}(Nat^{ı}). In the following we show that accepting such a type as the result of recursion will lead to accepting a non-terminating program. As a consequence, infinitely branching inductive data types, such as μ^{ı}λX. Nat^{ı} → X, do not inherit upper semi-continuity from their defining body, here, Nat^{ı} → X (recall that Nat^{ı} is lower semi-continuous, hence Nat^{ı} → X is upper semi-continuous). But remember that inductive types can still be upper semi-continuous, e. g., Hungry^{ı}(Nat^{∞}) = μ^{ı}λX. Nat^{∞} → X, which is covariant in its size index.

Semantically, we set H^{α} = μ^{α}F_{α}, where F_{α}(X) = (Nat^{α} → X)^{μ}. Since

lim sup_{α→λ} F_{α}(G(α)) ⊑ ((lim inf_{α→λ} Nat^{α}) → (lim sup_{λ} G))^{μ}
= F_{λ}(lim sup_{λ} G),

the family F_{α} is lim sup pushable. If we had a result like

lim sup_{α→λ} μ^{ϕ(α)}F_{α} ⊑ μ^{lim sup_{λ} ϕ} lim sup_{λ} F,

then H would be upper semi-continuous, and it would be legal to write the following recursive function:

h : ∀ı. Nat^{ı} → Hungry^{ı}(Nat^{ı})
h := fix_{0}^{μ}λhλ . in (s ∘ h ∘ pred)
h (in ) ⟶^{+} in (s ∘ h ∘ pred)

We will show that the existence of h destroys normalization. In the body of h we refer to an auxiliary function s. As well as its inverse, p, it can be defined by induction on ı:

s : ∀ı∀ȷ. Hungry^{ı}(Nat^{ȷ}) → Hungry^{ı}(Nat^{ȷ+1})
s := fix_{0}^{μ}λsλh. in (s ∘ (out h) ∘ pred)
s (in f) ⟶^{+} in (s ∘ f ∘ pred)
p : ∀ı∀ȷ. Hungry^{ı}(Nat^{ȷ+1}) → Hungry^{ı}(Nat^{ȷ})
p := fix_{0}^{μ}λpλh. in (p ∘ (out h) ∘ succ)
p (in f) ⟶^{+} in (p ∘ f ∘ succ)

(Note that these definitions are perfectly acceptable and not to blame.) Another innocent function is the following. Its type looks funny, since it produces something in the empty type, but let us mind that Hungry, being an inductive type “with nothing to start induction,” is also empty.

tr : ∀ı. Hungry^{ı}(Nat^{∞}) → ∀A.A
tr := fix_{0}^{μ}λtrλh. tr ((p ∘ (out h) ∘ succ) zero)
tr (in f) ⟶^{+} tr ((p ∘ f ∘ succ) zero)

Some calculation now shows that tr (h zero), the application of tr to the “bad guy” h, diverges:

tr (h zero)  ⟶^{+} tr (in (s ∘ h ∘ pred))
⟶^{+} tr ((p ∘ s ∘ h ∘ pred ∘ succ) zero)  ⟶^{+}
tr (p (s (h zero))) ⟶^{+} tr (p (s (in (s ∘ h ∘ pred)))))
⟶^{+} tr (p (in (s^{2} ∘ h ∘ pred^{2})))
⟶^{+} tr (in (p ∘ s^{2} ∘ h ∘ pred^{2} ∘ succ))
⟶^{+} tr ((p^{2} ∘ s^{2} ∘ h ∘ pred^{2} ∘ succ^{2}) zero) ⟶^{+}
tr (p^{2} (s^{2} (h zero))) ⟶^{+} …

6. A Kinding System for Semi-Continuity

We turn the results of Section 4 into a calculus and define a judgement Δ; Π ⊢^{ıq} F : κ, where ı is an ordinal variable with (ı : pord) ∈ Δ for some p, the bit q ∈ {⊖, ⊕} states whether the constructor F under consideration is lower (⊖) or upper (⊕) semi-continuous, and Π is a context of strictly positive constructor variables X:+κ′. We will prove (Thm. 6.2) that the family F (ı) is lim sup-pushable in all X ∈ Π if q = ⊕ and lim inf-pullable if q = ⊖.

The complete listing of rules can be found in Figure 3; in the following, we discuss a few.

cont-co \frac{Δ, ı:+ord ⊢ F : κ  p ∈ \{+, ∘\}}{Δ, ı:pord; Π ⊢^{ı⊕} F : κ}

If ı appears only positively in F, then F is trivially upper semi-continuous. However, monotonicity does not imply lim sup-pushability, so no variables from Π may occur in F. In the conclusion we may choose to set p = ∘, meaning that we forget that F is monotone in ı. Rule cont-contra is analogous and rule cont-in states that a constant F is (trivially) continuous.

cont-var \frac{X:pκ ∈ Δ, Π  p ≤ +}{Δ; Π ⊢^{ıq} X : κ}

Rule cont-var can be used also for X = ι. It states that the identity is continuous and both lim sup-pushable and lim inf-pullable.

Using the four rules discussed so far, we can derive semi-continuity properties of ordinal expressions. Expressions like ∞ and s^{n}ȷ (with ȷ ≠ ı) which are constant in ι are trivially continuous; so is the identity ι. Expressions of the form s^{n}ı with n ≥ 1 are only upper semi-continuous (rule cont-co), but not lower semi-continuous.

Now we discuss some rules to construct semi-continuous types and type constructors.

cont-arr \frac{−Δ; ⋄ ⊢^{ı⊖} A : ∗  Δ; Π ⊢^{ı⊕} B : ∗}{Δ; Π ⊢^{ı⊕} A → B : ∗}

Strictly positive contexts.

Π ::= ⋄ | Π, X:+κ_{∗}

Semi-continuity Δ; Π ⊢^{ıq} F : κ for q ∈ {⊕, ⊖}.

cont-co \frac{Δ, ı:+ord ⊢ F : κ  p ≤ +}{Δ, ı:pord; Π ⊢^{ı⊕} F : κ}  cont-contra \frac{Δ, ı:−ord ⊢ F : κ  p ≤ −}{Δ, ı:pord; Π ⊢^{ı⊖} F : κ}

cont-in \frac{Δ ⊢ F : κ}{Δ, ı:pord; Π ⊢^{ıq} F : κ}  cont-var \frac{X:pκ ∈ Δ, Π  p ≤ +}{Δ; Π ⊢^{ıq} X : κ}

cont-abs \frac{Δ, X:pκ; Π ⊢^{ıq} F : κ′}{Δ; Π ⊢^{ıq} λX:κ. F : pκ → κ′} X ≠ ı

cont-app \frac{Δ, ı:p′ord; Π ⊢^{ıq} F : pκ → κ′  p^{−1}Δ ⊢ G : κ}{Δ, ı:p′ord; Π ⊢^{ıq} F G : κ′}

cont-sum \frac{Δ; Π ⊢^{ıq} A : ∗  Δ; Π ⊢^{ıq} B : ∗}{Δ; Π ⊢^{ıq} A + B : ∗}

cont-prod \frac{Δ; Π ⊢^{ıq} A : ∗  Δ; Π ⊢^{ıq} B : ∗}{Δ; Π ⊢^{ıq} A × B : ∗}

cont-arr \frac{−Δ; ⋄ ⊢^{ı⊖} A : ∗  Δ; Π ⊢^{ı⊕} B : ∗}{Δ; Π ⊢^{ı⊕} A → B : ∗}  cont-∀ \frac{Δ; Π ⊢^{ı⊕} F : ∘κ → ∗}{Δ; Π ⊢^{ı⊕} ∀_{κ}F : ∗}

cont-mu \frac{Δ; Π, X:+κ_{∗} ⊢^{ı⊖} F : κ_{∗} Δ ⊢ a : ord}{Δ; Π ⊢^{ı⊖} μ^{a}(λX:κ_{∗}. F) : κ_{∗}} a = ı or ı ∉ FV(a)

cont-nu \frac{Δ; Π, X:+κ_{∗} ⊢^{ı⊕} F : κ_{∗}  Δ ⊢ a ord}{Δ; Π ⊢^{ı⊕} ν^{a}(λX:κ_{∗}. F) : κ_{∗}}

Pure ordinal expressions Δ ⊢ a ord.

ord-∞ \overline{Δ ⊢ ∞ ord} ord-var \frac{(ı:pord) ∈ Δ  p ≤ +}{Δ ⊢ ı ord} ord-s \frac{Δ ⊢ a ord}{Δ ⊢ s a ord}

Figure 3: F_{ω}: Semi-continuous constructors and recursion types.

This rule incarnates Thm. 4.7. Note that, because A is to the left of the arrow, the polarity of all ordinary variables in A is reversed, and A may not contain strictly positive variables.

cont-nu \frac{Δ; Π, X:+κ_{∗} ⊢^{ı⊕} F : κ_{∗}  Δ ⊢ a ord}{Δ; Π ⊢^{ı⊕} ν^{a}(λX:κ_{∗}. F) : κ_{∗}}

Rule cont-nu states that strictly positive coinductive types are upper semi-continuous. The ordinal a must be ∞ or s^{n}ȷ for some ȷ:ord ∈ Δ (which may also be identical to ı).

Lemma 6.1. Assume Δ ⊢ a ord and let θ ∈ ⟦Δ⟧, ı an ordinal variables, and

ϕ := (α ↦ ⟦a⟧_{θ[ı↦α]}) ∈ ⟦ord⟧ → ⟦ord⟧.

Then for all limit ordinals λ ≥ ω, either lim inf_{λ} ϕ = ϕ(λ), or both sides are ≥ ω.

Proof. ϕ is either constant or affine (ϕ(α) = min α + n, ⊤^{ord} for some n ∈ ℕ), and such ϕ have the required property.

Theorem 6.2 (Soundness of Continuity Derivations). Assume Δ; X⃗: +κ⃗ ⊢^{ıq} F : κ. Let θ a valuation of the variables in Δ and set F_{α}(G⃗) = ⟦F ⟧_{θ[ı↦α][X⃗↦G⃗]}.

(1) If q = ⊖ then the family F is lim inf-pullable.

(2) If q = ⊕ then the family F is lim sup-pushable.

Proof. By induction on the continuity derivation. Some cases:

cont-nu \frac{Δ; X⃗:κ⃗, X:+κ_{∗} ⊢^{ı⊕} F : κ_{∗}  Δ ⊢ a ord}{Δ; X⃗:κ⃗ ⊢^{ı⊕} ν^{a}(λX:κ_{∗}. F) : κ_{∗}}

Let F_{α}(G⃗)(H) = ⟦F ⟧_{θ[ı↦α][X⃗↦G⃗][X↦H]} and ϕ(α) = ⟦a⟧_{θ[ı↦α]}. By Lemma 6.1, ϕ is either constant or affine, and by induction hypothesis, F is lim sup-pushable. Thus, we can apply Thm. 4.15 to infer the goal.

cont-mu \frac{Δ; Π, X:+κ_{∗} ⊢^{ı⊖} F : κ_{∗} Δ ⊢ a : ord}{Δ; Π ⊢^{ı⊖} μ^{a}(λX:κ_{∗}. F) : κ_{∗}} a = ı or ı ∉ FV(a)

ϕ(α) := ⟦a⟧_{θ[ı↦α]} is either constant or the identity, hence, it is monotone and continuous. The goal follows from Thm. 4.18.

Now we are able to formulate the syntactical admissibility criterion for types of (co)recursive functions.

Definition 6.3 (Syntactic admissibility).

Γ ⊢ A fix_{n}^{μ}-adm iff Γ, ı:∘ord ⊢ A ı = ∀X⃗:κ⃗.B_{1} → ⋯ → B_{n} → μ^{ı}F H⃗ → C : ∗
and Γ, ı:∘ord; ⋄ ⊢^{ı⊕} ∀X⃗:κ⃗. B_{1..n} → μ^{ı}F H⃗ → C : ∗
Γ ⊢ A fix_{n}^{ν}-adm iff Γ, ı:∘ord ⊢ A ı = ∀X⃗:κ⃗.B_{1} → ⋯ → B_{n} → ν^{ı}F H⃗ : ∗
and Γ, ı:∘ord; ⋄ ⊢^{ı⊕} ∀X⃗:κ⃗. B_{1..n} → ν^{ı}F H⃗ : ∗

It is easy to check that admissible types fulfill the semantic criteria given at the end of Section 3. We prove Assumption 3.5, restated as the following theorem.

Theorem 6.4 (Soundness of admissibility). If Γ ⊢ A fix_{n}^{∇}-adm and θ(X) ∈ ⟦κ⟧ for all (X:κ) ∈ ⟦Γ⟧ then A := ⟦A⟧_{θ} ∈ ⟦ord⟧ → ⟦∗⟧ has the following properties:

(1) Shape: A(α) = ⋂_{k∈K} B_{1}(k, α) → … → B_{n}(k, α) → B(k, α) for some K and some

B_{1}, …, B_{n}, B ∈ K × ⟦ord⟧ → ⟦∗⟧. In case ∇ = μ, B(k, α) = I(k, α)^{μ} → C(k, α) for

some I, C. Otherwise, B(k, α) = C(k, α)^{ν} for some C.

(2) Bottom-check: I(k, 0)^{μ} = ⊥^{∗} in case ∇ = μ and C(k, 0)^{ν} = ⊤^{∗} in case ∇ = ν.

(3) Limit-check: inf_{α<λ} A(α) ⊆ A(λ) for all limit ordinals λ ∈ ⟦ord⟧ \ {0}.

Proof. Set K := ⟦κ_{1}⟧ × … ⟦κ_{m}⟧ with m := |κ⃗| and B_{i}(k, α) := ⟦B_{i}⟧_{θ[X⃗↦k][ı↦α]} for i = 1..n. Further, let F(k)(α) := ⟦F ⟧_{θ[X⃗↦k][ı↦α]} and H_{j}(k)(α) := ⟦H_{j}⟧_{θ[X⃗↦k][ı↦α]}.

In case ∇ = μ, first let C(k, α) = ⟦C⟧_{θ[X⃗↦k][ı↦α]}. Define ∅^{p⃗κ⃗→∗}(G⃗) = ∅ and observe that

for any f ∈ ⟦κ⟧ →^{+} ⟦κ⟧, μ^{α}f^{μ} = (f^{μ})^{α}(⊥^{κ}) = ((f ∘ (−)^{μ})^{α}(∅^{κ}))^{μ}. (Induction on α, using ∅^{μ} = ⊥ and sup-continuity of (−)^{μ}.) Thus, we can set

I(k, α) = (((F(k)(α) ∘ (−)^{μ})^{α}(∅))(H⃗)

and have I(k, α)^{μ} = ⟦μ^{ı}F H⃗⟧_{θ[X⃗↦k][ı↦α]}. Properties (1) and (2) are hence satisfied. By Thm. 6.2, the type A is upper semi-continuous which implies (3).

For case ∇ = ν, define (out · ⊤^{p⃗κ⃗→∗})(G⃗) = out · ⊤^{∗}. Then (out · ⊤)^{ν} = ⊤. Observe that ν^{α}f^{ν} = (f^{ν})^{α}(⊤) = ((f ∘ (−)^{ν})^{α}(out · ⊤))^{ν} and set

C(k, α) = (((F(k)(α) ∘ (−)^{ν})^{α}(out · ⊤))(H⃗).

Then C(k, α)^{ν} = ⟦ν^{ı}F H⃗⟧_{θ[X⃗↦k][ı↦α]}. Using Thm. 6.2, all three properties hold.

Example 6.5 (Inductive type inside coinductive type). Rule cont-nu allows the type system to accept the following definition, which assigns an informative type to the stream nats of all natural numbers in ascending order:

nats  : ∀ı. Stream^{ı} Nat^{ı}
nats  := fix_{0}^{ν}λnats. ⟨zero, mapStream succ nats⟩
mapStream : ∀A∀B. (A → B) → ∀ı. Stream^{ı}A → Stream^{ı}B
mapStream := λffix_{1}^{ν}λmapsλs. in⟨f (fst (out s)), maps (snd (out s))⟩

The type of nats expresses that if you read the first n elements of the stream, these are numbers < n. In particular, the ith element of nats is at most i − 1. This is the most information a type of nats can carry in our type system.

Example 6.6 (Inductive type inside inductive type). In the following, we describe breadthfirst traversal of rose (finitely branching) trees whose termination is recognized by F_{ω}.

Rose : ord →^{+} ∗ →^{+} ∗
Rose := λıλA. GRose^{ı} List^{∞} A = λıλA. μ_{∗}^{ı}λX. A × List^{∞}X

The step function, defined by induction on ȷ, traverses a list of rose trees of height < ı + 1 and produces a list of the roots and a list of the branches (height < ı).

step : ∀ȷ∀A∀ı. List^{ȷ}(Rose^{ı+1} A) → List^{ȷ} A × List^{∞}(Rose^{ı} A)
step := fix_{0}^{μ}λstepλl. match l with

nil ↦ ⟨nil, nil⟩

cons ⟨a, rs′⟩ rs ↦ match step rs with ⟨as, rs′′⟩ ↦ ⟨cons a as, append rs′ rs′′⟩

Now, bf iterates step on a non-empty forest, which is represented by a single rose tree r and a possibly empty list of rose trees rs. It is defined by induction on ı, the strict upper bound of the tree heights.

bf : ∀ı∀A. Rose^{ı} A → List^{∞}(Rose^{ı} A) → List^{∞}A
bf := fix_{0}^{μ}λbf λrλrs. match step (cons r rs) with
⟨as, nil⟩  ↦ as
⟨as, cons r′ rs′⟩ ↦ append as (bf r′ rs′)

Function bf terminates because the recursive-call trees in forest cons r′ rs′ are smaller than the input trees in forest cons r rs. This information is available to the type system through the type of step. The type of bf is admissible for recursion since List^{∞} (Rose^{ı} A) is lower semi-continuous in ı—thanks to Thm. 4.18 and rule cont-mu.

It is clear that admissibility is no way complete. One can find trivial examples of terminating programs which are refused by the type system because they fail the admissibility check. For instance, take the recursive identity function of type ∀ı. Nat^{ı} → Nat^{ı} and add an unused argument of type Nat^{∞} → Nat^{ı}:

loopnot : ∀ı. Nat^{ı} → (Nat^{∞} → Nat^{ı}) → Nat^{ı}

loopnot 0  g = 0
loopnot (n + 1) g = 1 + loopnot n (shift g)

Its type is not upper semi-continuous, but of course loopnot is terminating.

7. Conclusions

We have motivated the importance of semi-continuity for the soundness of type-based termination checking, explored the realm of semi-continuous functions from ordinals to semantic types, and developed a calculus for semi-continuous types. We have seen a few interesting examples involving semi-continuous types, many more can be found in the author’s thesis [Abe06b, Ch. 6]. These examples cannot be handled by type-based termination à la Barthe et al. [BFG^{+}04, BGP05], but our developments could be directly incorporated into their calculus.

In previous work [Abe03], I have already presented a calculus for admissible recursion types. But the language had neither polymorphism, higher-kinded types, nor semicontinuous types inside each other (Stream^{ı} Nat^{ı}). Hughes, Pareto, and Sabry [HPS96] have also given criteria for admissible types similar to ours, but rather ad-hoc ones, not based on the mathematical concept of semi-continuity. Also, a crucial difference is that we also treat infinitely branching data structures. To be fair, I should say that their work has been a major source of inspiration for me.

As a further direction of research, I propose to develop a kinding system where semicontinuity is first class, i. e., one can abstract over semi-continuous constructors, and kind arrows can carry the corresponding polarities ⊖ or ⊕. First attempts suggest that such a calculus is not straightforward, and a more fine-grained polarity system will be necessary. Important is also the study of semi-continuity properties of dependent types, in order to apply these results to type-based termination in type-theoretic proof assistants.

7.1. Acknowledgments. I would like to thank my supervisor, Martin Hofmann, for discussions on F_{ω}. Thanks to John Hughes for lending his ear in difficult phases of this work, for instance, when I was trying to prove upper semi-continuity of inductive types but then found the Hungry counterexample. Thanks to the anonymous referees of previous versions of this paper who gave insightful and helpful comments.

References

[Abe03] Andreas Abel. Termination and guardedness checking with continuous types. In M. Hofmann, editor, Typed Lambda Calculi and Applications (TLCA 2003), Valencia, Spain, volume 2701 of Lecture Notes in Computer Science, pages 1–15. Springer-Verlag, June 2003.

[Abe04] Andreas Abel. Termination checking with types. RAIRO – Theoretical Informatics and Applications, 38(4):277–319, 2004. Special Issue: Fixed Points in Computer Science (FICS’03).

[Abe06a] Andreas Abel. Polarized subtyping for sized types. In Dima Grigoriev, John Harrison, and Edward A. Hirsch, editors, Computer Science - Theory and Applications, First International Computer Science Symposium in Russia, CSR 2006, St. Petersburg, Russia, June 8-12, 2006, Proceedings, volume 3967 of Lecture Notes in Computer Science, pages 381–392. Springer-Verlag, 2006.

[Abe06b] Andreas Abel. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Ludwig-Maximilians-Universität München, 2006.

[Abe06c] Andreas Abel. Semi-continuous sized types and termination. In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 21-24, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 72–88. Springer-Verlag, 2006.

[ACG98] Roberto M. Amadio and Solange Coupet-Grimal. Analysis of a guard condition in type theory (extended abstract). In Maurice Nivat, editor, Foundations of Software Science and Computation Structure, First International Conference, FoSSaCS’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, volume 1378 of Lecture Notes in Computer Science, pages 48–62. Springer-Verlag, 1998.

[Alt01] Thorsten Altenkirch. Representations of first order function types as terminal coalgebras. In Typed Lambda Calculi and Applications, TLCA 2001, number 2044 in Lecture Notes in Computer Science, pages 8 – 21. Springer-Verlag, 2001.

[AM04] Andreas Abel and Ralph Matthes. Fixed points of type constructors and primitive recursion. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 190–204. Springer-Verlag, 2004.

[AR99] Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Jörg Flum and Mario Rodríguez-Artalejo, editors, Computer Science Logic, 13th International Workshop, CSL ’99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings, volume 1683 of Lecture Notes in Computer Science, pages 453–468. Springer-Verlag, 1999.

[BFG^{+}04] Gilles Barthe, Maria J. Frade, Eduardo Giménez, Luis Pinto, and Tarmo Uustalu. Type-based termination of recursive definitions. Mathematical Structures in Computer Science, 14(1):1–45, 2004.

[BGP05] Gilles Barthe, Benjamin Grégoire, and Fernando Pastawski. Practical inference for type-based termination in a polymorphic setting. In Pawel Urzyczyn, editor, Typed Lambda Calculi and Applications (TLCA 2005), Nara, Japan, volume 3461 of Lecture Notes in Computer Science, pages 71–85. Springer-Verlag, 2005.

[Bla04] Frédéric Blanqui. A type-based termination criterion for dependently-typed higher-order rewrite systems. In Vincent van Oostrom, editor, Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Germany, June 3 – 5, 2004, Proceedings, volume 3091 of Lecture Notes in Computer Science, pages 24–39. Springer-Verlag, 2004.

[Bla05] Frédéric Blanqui. Decidability of type-checking in the Calculus of Algebraic Constructions with size annotations. In C.-H. Luke Ong, editor, Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, volume 3634 of Lecture Notes in Computer Science, pages 135–150. Springer-Verlag, 2005.

[BP99] Richard S. Bird and Ross Paterson. De Bruijn notation as a nested datatype. Journal of Functional Programming, 9(1):77–91, 1999.

[CW99] Karl Crary and Stephanie Weirich. Flexible type analysis. In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), Paris, France, volume 34 of SIGPLAN Notices, pages 233–248. ACM Press, 1999.

[DC99] Dominic Duggan and Adriana Compagnoni. Subtyping for object type constructors, January 1999. Presented at FOOL 6.

[Gim98] Eduardo Giménez. Structural recursive definitions in type theory. In K. G. Larsen, S. Skyum, and G. Winskel, editors, Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, volume 1443 of Lecture Notes in Computer Science, pages 397–408. Springer-Verlag, 1998.

[Han02] Peter Hancock. The step to the next number class. http://www.dcs.ed.ac.uk/home/pgh/numberclasses.html, 2002.

[Hin00a] Ralf Hinze. Efficient generalized folds. In Johan Jeuring, editor, Proceedings of the Second Workshop on Generic Programming, WGP 2000, Ponte de Lima, Portugal, July 2000.

[Hin00b] Ralf Hinze. Generalizing generalized tries. Journal of Functional Programming, 10(4):327–351, July 2000.

[HPS96] John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’96, pages 410–423, 1996.

[Men87] Nax P. Mendler. Recursive types and type constraints in second-order lambda calculus. In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, N.Y., pages 30–36. IEEE Computer Society Press, 1987.

[Par00] Lars Pareto. Types for Crash Prevention. PhD thesis, Chalmers University of Technology, 2000.

[Pie02] Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.

[PM92] Christine Paulin-Mohring. Inductive definitions in the system Coq—rules and properties. Technical report, Laboratoire de l’Informatique du Parallélisme, December 1992.

[Ste98] Martin Steffen. Polarized Higher-Order Subtyping. PhD thesis, Technische Fakultät, Universität Erlangen, 1998.

[Vou04] Jérôme Vouillon. Subtyping union types. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 415–429. Springer-Verlag, 2004.

[Xi01] Hongwei Xi. Dependent types for program termination verification. In Proceedings of 16th IEEE Symposium on Logic in Computer Science, Boston, USA, June 2001.

Appendix A. Complete Specification of F_{ω}

The following figures display all constructs and rules of F_{ω}.

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  ::= 1 | + | × | → | ∀_{κ} | μ_{κ_{∗}} | ν_{κ_{∗}} | s | ∞ constructor constant
Δ ::= ⋄ | Δ, X:pκ polarized context

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

1 : ∗  unit type
+ : ∗ →^{+} ∗ →^{+} ∗  disjoint sum
× : ∗ →^{+} ∗ →^{+} ∗  cartesian product
→ : ∗ →^{−} ∗ →^{+} ∗  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
A + B for + A B  A × B for × A B  A → B for → A B

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 : κ′}

Figure 4: F_{ω}: Kinds and constructors.

Constructor equality Δ ⊢ F = F′ : κ.

eq-∞ \overline{Δ ⊢ s ∞ = ∞ : ord}
eq-β \frac{Δ, X:pκ ⊢ F : κ′  p^{−1}Δ ⊢ G : κ}{Δ ⊢ (λX:κ. F) G = [G/X]F : κ′}  eq-η \frac{Δ ⊢ F : pκ → κ′}{Δ ⊢ (λX:κ. F X) = F : pκ → κ′}
eq-var \frac{X:pκ ∈ Δ  p ≤ +}{Δ ⊢ X = X : κ}  eq-λ \frac{Δ, X:pκ ⊢ F = F′ : κ′}{Δ ⊢ λX:κ. F = λX:κ. F′ : pκ → κ′}
eq-c \frac{C:κ ∈ Σ}{Δ ⊢ C = C : κ}  eq-app \frac{Δ ⊢ F = F′ : pκ → κ′  p^{−1}Δ ⊢ G = G′ : κ}{Δ ⊢ F G = F′ G′ : κ′}
eq-sym \frac{Δ ⊢ F = F′ : κ}{Δ ⊢ F′ = F : κ}  eq-trans \frac{Δ ⊢ F_{1} = F_{2} : κ  Δ ⊢ F_{2} = F_{3} : κ}{Δ ⊢ F_{1} = F_{3} : κ}

Constructor subtyping Δ ⊢ F ≤ F′ : κ.

leq-s-r \frac{Δ ⊢ a : ord}{Δ ⊢ a ≤ s a : ord}  leq-∞ \frac{Δ ⊢ a : ord}{Δ ⊢ a ≤ ∞ : ord}
leq-λ \frac{Δ, X:pκ ⊢ F ≤ F′ : κ′}{Δ ⊢ λX:κ. F ≤ λX:κ. F′ : pκ → κ′}
leq-app \frac{Δ ⊢ F ≤ F′ : pκ → κ′  p^{−1}Δ ⊢ G : κ}{Δ ⊢ F G ≤ F′ G : κ′}
leq-app+ \frac{Δ ⊢ F : +κ → κ′  Δ ⊢ G ≤ G′ : κ}{Δ ⊢ F G ≤ F G′ : κ′}
leq-app− \frac{Δ ⊢ F : −κ → κ′  −^{−1}Δ ⊢ G′ ≤ G : κ}{Δ ⊢ F G ≤ F G′ : κ′}
leq-refl \frac{Δ ⊢ F = F′ : κ}{Δ ⊢ F ≤ F′ : κ} leq-trans \frac{Δ ⊢ F_{1} ≤ F_{2} : κ Δ ⊢ F_{2} ≤ F_{3} : κ}{Δ ⊢ F_{1} ≤ F_{3} : κ}
leq-antisym \frac{Δ ⊢ F ≤ F′ : κ  Δ ⊢ F′ ≤ F : κ}{Δ ⊢ F = F′ : κ}

Figure 5: F_{ω}: Constructor equality and subtyping.

Syntactic categories.

r, s, t ::= c | x | λxt | r s  term
c ::= ⟨⟩ | pair | fst | snd | inl | inr | case | in | out | fix_{n}^{μ} | fix_{n}^{ν} constant (n ∈ ℕ)
v  ::= λxt | ⟨⟩ | pair t_{1} t_{2} | inl t | inr t | in t | c | pair t | fix_{n}^{∇}s t_{1..m} value (m < n)
e( ) ::= s | fst | snd | case | out | fix_{n}^{μ} s t_{1..n}  evaluation frame
E( ) ::= e_{1}(… e_{n}( ) …)  eval. cxt.(n ≥ 0)
Γ ::= ⋄ | Γ, x:A | Γ, X:pκ typing context

Notation:

⟨r, s⟩ for pair r s t_{1..n} for t_{1} t_{2} … t_{n}.

Reduction t ⟶ t′.

(λxt) s  ⟶ [s/x]t
fst ⟨r, s⟩  ⟶ r
snd ⟨r, s⟩ ⟶ s
case (inl r) ⟶ λxλy. x r
case (inr r) ⟶ λxλy. y r

out (in r)  ⟶ r
fix_{n}^{μ} s t_{1..n} (in t) ⟶ s (fix_{n}^{μ} s) t_{1..n} (in t)
out (fix_{n}^{ν} s t_{1..n}) ⟶ out (s (fix_{n}^{ν} s) t_{1..n})
[s/x]t  ⟶ [s′/x]t if s ⟶ s′

The signature Σ contains types for some constants:

pair : ∀A∀B. A → B → A × B
fst : ∀A∀B. A × B → A
snd : ∀A∀B. A × B → B

⟨⟩ : 1_{inl : ∀A∀B. A → A + B}_{inr : ∀A∀B. B → A + B}

case : ∀A∀B∀C. A + B → (A → C) → (B → C) → C
in : ∀F:κ →^{+} κ. ∀G^{1} :κ_{∗}^{1} … ∀G^{n}:κ_{∗}^{n}. ∀ı:ord. F (∇_{κ}^{ı}F) G⃗ → ∇_{κ}^{ı+1}F G⃗
out : ∀F:κ →^{+} κ. ∀G^{1} :κ_{∗}^{1} … ∀G^{n}:κ_{∗}^{n}. ∀ı:ord. ∇_{κ}^{ı+1}F G⃗ → F (∇_{κ}^{ı}F) G⃗

(∇ ∈ {μ, ν}, κ = κ⃗_{∗} →^{p⃗} ∗)

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-c \frac{(c:A) ∈ Σ}{Γ ⊢ c : 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 fix_{n}^{∇}-adm  Γ ⊢ a : ord}{Γ ⊢ fix_{n}^{∇} : (∀ı:ord. A ı → A (ı + 1)) → A a}

Figure 6: F_{ω}: Terms, reduction and typing.