<figure><img src="image_1.png" /></figure>

HAL
open science

# Towards Corecursion Without Corecursion in Coq

Vlad Rusu, David Nowak

► To cite this version:

Vlad Rusu, David Nowak. Towards Corecursion Without Corecursion in Coq. 2022. hal-03689027v4

HAL Id: hal-03689027

https://inria.hal.science/hal-03689027v4

Preprint submitted on 15 Aug 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
# Towards Corecursion Without Corecursion in Coq

Vlad Rusu

Inria, Lille, France

Vlad.Rusu@inria.fr

David Nowak

CNRS, Lille, France

David.Nowak@univ-lille.fr

Coinduction is an important concept in functional programming. To formally prove properties of corecursive functions one can try to define them in a proof assistant such as Coq [1]. But there are limitations on the functions that can be defined in this proof assistant. In particular, corecursive calls must occur directly under a call to a constructor, without any calls to other recursive functions in between. In this paper we show how a partially ordered set with certain extensions - approximations and definedness measures - can be organised as Complete Partial Orders endowed with the same extensions. This makes it possible to define *total* corecursive functions without using Coq's corecursion, as unique solutions of fixpoint equations, thereby escaping Coq's builtin limitations.

## 1 Introduction

Coinduction is an important concept in functional programming. Coinductive types are the types of possibly infinite data structures such as the lists of Haskell, and corecursive functions compute values in coinductive types. An example is the Sieve of Eratosthenes that produces the infinite stream of primes.

To formally define corecursive functions one can try to use a proof assistant such as Coq. But then one quickly stumbles on the limitations of Coq on this matter. Indeed the language of this proof assistant is total, meaning that a function must be defined on all its domain (which is not requested for functional programming languages in general). Totality is ensured in Coq by a syntactical check of so-called guardedness. This criterion consists in checking that any corecursive call occurs directly under a call to a constructor of the coinductive type that constitutes the codomain (a.k.a. range) of the function under definition [6]. For example, Rose trees are coinductively defined as the constructor *tree* applied to a *forest*, which is an inductively-defined list of Rose trees. A *mirror* function would be corecursively defined by *mirror t = tree(map mirror(reverse(forest t)))*, but this is rejected by Coq because the corecursive call is not directly under the constructor *tree*, but under *map*, a recursive function defined on lists.

In a previous paper [9] we propose a method for defining such functions by replacing the syntactical guardedness criterion by a semantical proof obligation of productiveness: for each input, an arbitrarily close approximation of the corresponding output is eventually produced. When a functional (i.e., a higher-order function, which constitutes the “blueprint” of a corecursive function under definition) is monotonic and satisfies the productiveness requirement, a corecursive function can be defined as the unique fixpoint of the functional in question. This technique requires that the codomain of the function under definition be organized as a Omega-Complete Partial Order (ωCPO). For some coinductive types such as streams or possibly infinite lists, the ωCPO can be directly defined using Coq's builtin mechanisms, and particular corecursive functions, which do not admit a direct definition in Coq, can be indirectly defined as instances of limits of sequences of approximating functions in the ωCPO in question. But, being nonetheless based on Coq's builtin coinduction features, the ωCPO construction does not work for all coinductive types. In particular, for mixed inductive-coinductive types such as Rose trees the construction of *limits* in the corresponding ωCPO is rejected by Coq as unguarded. The solution we proposed in [9] is to replace the construction of ωCPOs of coinductive types by a completion mechanism,
by which inductive types are completed with equivalence classes of “ascending” sequences of elements
in inductive types, which are limits for the sequences in question and play the role of corecursive values.

However, the construction we ended up with in [9] imposes some not-so-practical conditions. The
order had to be weakly total, thus excluding the natural order induced by the constructors of the induc-
tive types. Although we were able to exhibit a weakly total order for the particular case of Rose tees,
the constructor tree is not monotonic w.r.t. this order. As a consequence, functionals that employ this
constructor are not monotonic either, which excludes them for being used in fixpoint equations for the
definition of corecursive functions. For example, the *mirror* function cannot be defined in the natural
manner, as a fixpoint of the functional *Mirror* = λf.λt.tree(map f (reverse(forest t))), but in an indirect
way that makes it harder to prove that the obtained function is indeed the intended one.

**Contributions.** In this paper we replace the weak totality condition on partial orders by a notion of approximation of a given precision meeting some quite natural conditions. These conditions are easier to satisfy than the (comparatively arbitrary) weak totality. We illustrate with the example of finite trees that the natural (i.e. structural) order on inductive types — quite importantly, this is the least constrained order under which constructors are monotonic — does satisfy the conditions on approximations whereas it did not satisfy weak totality. We then describe the construction of an $\omega$CPO under the said conditions. This construction is substantially more involved than that in [9], but has to be done only once and can then be instantiated on any inductive type with an adequate notion of approximation in order to generate coinductive types. For Rose trees, the effect of the new construction is that the *tree* constructor is now monotonic w.r.t. their natural *prefix* order. By further enriching the $\omega$CPOs with approximations with a measure of “definedness” (inherited from a definedness measure on partial orders with approximations) it becomes to define total corecursive functions (i.e., functions that return “total” values) in the most natural manner, as the unique solution of the fixpoint equation induced by a monotonic, productive functional of the function. We also give practical sufficient conditions ensuring the productiveness requirement.

**Outline.** Section 2 presents preliminary notions. These include the definition of $\omega$CPOs and a recapp of results from [9] that enable the definition of total corecursive functions as unique fixpoints of certain “productive” functionals involving $\omega$CPOs. We then introduce an abstract notion of approximations of a given precision and some assumptions over them. We show that the assumptions have a model - finite trees with their natural prefix order and a “cut” function. Some technical developments are also included.

Section 3 defines the completion operation that produces an $\omega$CPO from a partially ordered set with a least element. Completion is done in several steps: first, one completes an initial set of “finite” elements with new elements that are equivalence classes of ascending sequences of finite elements, thereby providing such sequences with “limits” (least upper bounds) required by $\omega$CPOs. Second, the order and approximations are extended to the new elements. Third, we show using a “diagonalization” technique that ascending sequences of both old and new elements have limits among the new elements, meaning that the construction of the $\omega$CPO does not require further completion steps.

In Section 4 we give practically usable sufficient conditions for proving the productiveness of functionals, which is required for defining total corecursive functions as unique fixpoints of those functionals. A special attention is given to *maximal* elements in the underlying $\omega$CPO. These are shown to coincide with total coinductive values - the values that a total corecursive function can return. Total values are characterized by having a “definedness” equal to infinity, according to a definedness measure, which we assume on the underlying partial order and its approximations and extend to the $\omega$CPO.

Section 5 applies completion to produce Rose trees from finite trees. The whole approach is in-
stantiated in Section 6 by defining the *mirror function* as the unique fixpoint of its functional, whose productiveness is proved by using the sufficient conditions in the previous section.

Section 7 concludes and presents related and future work. This paper will be formalized in Coq, but we keep it language-agnostic and use standard mathematics for better readability.

# 2 Preliminaries

## 2.1 Sequences and Complete Partial Orders

**Definition 1** Consider a set $C$ and a partial order $\leq$ on $C$. We denote by $<$ the relation defined by $t < t'$ iff $t \leq t'$ and $t \neq t'$. A sequence $(s_i)_{i \in \mathbb{N}}$ of elements of $C$ is

* increasing whenever for all $i \in \mathbb{N}$, $s_i \leq s_{i+1}$;

* strictly increasing, whenever for all $i \in \mathbb{N}$, $s_i < s_{i+1}$;

* stabilizing to $c \in C$ whenever there exist $m \in \mathbb{N}$ such that for all $i \geq m$, $s_i = c$, and stabilizing whenever it is stabilizing to some $c \in C$;

* ascending whenever it is increasing and non-stabilizing.

**Remark.** A sequence is ascending iff it is increasing and has a strictly increasing subsequence, and each increasing and stabilizing sequence is stabilizing to a unique value.

**Definition 2** An $\omega$-Complete Partial Order ($\omega$CPO) is a tuple $(C, \leq, \perp)$, where $\leq$ is a partial order on $C$, $\perp$ is the least element for $\leq$, and such that each increasing sequence $(s_n)_{n \in \mathbb{N}}$ over $C$ has a least upper bound.

Hereafter we call least upper bounds *limits* and denote the limit of a sequence $(s_n)_{n \in \mathbb{N}}$ by $\lim((s_n)_{n \in \mathbb{N}})$.

**Remark.** An important feature of $\omega$CPOs is that the order $\leq$ should be interpreted as a definition order. In this sense, $\perp$ is the *least defined* element, and elements that are maximal with respect to the order are interpreted as are “totally defined”. Intermediate, non-maximal elements are therefore “partially defined”. In this paper we are interested in defining *total* corecursive functions, which only return totally defined values. Such values play an important role in the rest of the paper.

We now recapp some results from [9] that enable the definition of total corecursive functions as unique fixpoints of “productive” functionals.

Assume an $\omega$CPO $(C, \leq, \perp)$. We extend $\leq$ to functions $D \to C$ by $f_1 \leq f_2$ iff $f_1 x \leq f_2 x$ for all $x \in D$.

**Definition 3** A functional $F : (D \to C) \to D \to C$ is increasing if for all $f_1, f_2 : D \to C$, $f_1 \leq f_2$ implies $Ff_1 \leq Ff_2$.

Consider a functional $F : (D \to C) \to D \to C$ as above. Let $\perp : D \to C$ be the constant function such that $\perp x = \perp$, for all $x \in D$, and let $F^n : (D \to C) \to D \to C$ be the functional inductively defined by $F^0 f = f$ and, for all $n \in \mathbb{N}$, $F^{n+1} f = F(F^n f)$.

**Definition 4** A functional $F : (D \to C) \to D \to C$ is productive whenever it is increasing and for all $x \in D$, the limit of the (increasing) sequence $(F^n \perp x)_{n \in \mathbb{N}}$ is maximal w.r.t. the order $\leq$.

**Remark.** The relationship between the productiveness of a functional and the informal notion of productiveness for corecursive functions is established in [9].

**Theorem 1 ([9])** If a functional $F$ is productive then $\lim((F^n \perp)_{n \in \mathbb{N}})$ is the unique fixpoint of $F$.

**Remark.** Hence, in order to define a total function one needs to (1) organize the codomain $C$ of the function as an $\omega$CPO; (2) prove that the functional of the function in question is productive.
## 2.2 Partially Ordered Sets with Least Elements and Quantified Approximations

**Assumption 1** In the sequel we assume:

1. a partially ordered set ($C^\circ, \leq^\circ$) with a least element $\perp$. Elements of $C^\circ$ are often called finite. It is required that no finite element be an upper bound for an ascending sequence of finite elements;

2. for each $N \in \mathbb{N}$, an approximation function $\|\cdot\|_N : C^\circ \to C^\circ$. For any $c \in C^\circ$, $\|c\|_N$ is called the approximation of $c$ having precision $N$, and satisfies the following properties:

(a) for all $c \in C^\circ$ and $N \in \mathbb{N}$, $\|c\|_N \leq^\circ c$;

(b) for all $c, c' \in C^\circ$ and $N \in \mathbb{N}$, $c \leq c'$ implies $\|c\|_N \leq^\circ \|c'\|_N$;

(c) for all $c \in C^\circ$ and $N, N' \in \mathbb{N}$, $N \leq N'$ implies $\|c\|_N \leq^\circ \|c'\|_N$;

(d) for all $c \in C^\circ$ there exists $N \in \mathbb{N}$ such that $\|c\|_N = c$;

(e) for all $c \in C^\circ$ and $N, N' \in \mathbb{N}$, $N \leq N'$ implies $\|\|c\|_N\|\|_N = \|c\|_N$;

3. for any $N \in \mathbb{N}$ and any ascending sequence $(s_n)_{n \in \mathbb{N}}$, $(\|s_n\|_N)_{n \in \mathbb{N}}$ is stabilizing.

**Remark.** The requirements in Assumption 1 are quite natural. Item 1 holds if finite elements have finitely many finite elements smaller than them, a property which may be expected from finite elements. Item 2.(a) says that approximations do approximate w.r.t. the precision, items 2.(b) and 2.(c) says that approximations are monotonic in both arguments; item 2.(d) says that for finite elements approximation can be exact, and item 2.(e) says that approximating first at some precision $N' \geq N$ and then approximating at precision $N$ amounts to approximating at precision $N$. Finally, item 3 says that mapping approximations to ascending sequences makes them stabilize - the sequence of approximations cannot grow forever.

**Example 1 (model for Assumption 1)** Let $C^\circ$ be the set of trees inductively defined by the rules $\perp \in C^\circ$ and for each list $l$ over $T$, tree$^\circ$ $l \in T$. Let $\leq^\circ$ be the prefix relation on $C^\circ$, inductively defined by $\perp \leq^\circ t$ for each $t \in C^\circ$, and, for every pair of lists $l, l'$ over $T$ having the same length, say, $m$, tree$^\circ$ $l \leq^\circ$ tree$^\circ$ $l'$ whenever $l[i] \leq^\circ l'[i]$ for each $i < m$ (where $l[i]$ denotes the $i$-th element of the list $l$). Let $\|\cdot\|_N$ ("cut at height $N$") denote the function $\lambda t$. If $N = 0 \lor t = \perp$ then $\perp$ else tree$^\circ$(map($\|\cdot\|_{N-1}$)(forest$^\circ$ $t$)) where forest$^\circ$(tree$^\circ$ $l$) $\triangleq$ $l$ and map is the mapping function on lists. We have proved in Coq that Assumption 1 holds for these definitions. The code is available at https://project.inria.fr/wpte2022/.

The $\leq^\circ$ order and the approximation $\|\cdot\|_N$ at precision $N \in \mathbb{N}$ can equivalently be defined by rewriting, which will be useful ahead in the paper. We thus recall some notions about rewriting. A position is a string over $\mathbb{N}$, with an associative concatenation operation $\cdot$ having the empty string $\epsilon$ as neutral element. The set of all positions is denoted $\mathbb{N}^*$. Given a tree $t$, the set $\pi t$ of positions of $t$ is inductively defined by $\pi \perp = \{\epsilon\}$ and $\pi(\text{tree}^\circ[t_0, \dots, t_{n-1}]) = \bigcup_{i=0}^{n-1}(\pi t_i) \cup \bigcup_{i=0}^{n-1} \bigcup_{p \in (\pi t_i)} \{i \cdot p\}$. For a tree and $p \in \pi t_i$, the subtree $t_{|p}$ of $t$ at position $p$ is defined by $t_{|\epsilon} := t$ and, for all $0 \leq i < n$ and $p \in (\pi t_i)$, $(\text{tree}^\circ[t_0, \dots, t_{n-1}])_{|(i \cdot p)} := (t_i)_{|p}$. A position $p \in \pi t$ is a $\perp$-position whenever $t_{|p} = \perp$. The substitution $t[t']_{|p}$ of a tree $t'$ at a position $p$ of a tree $t$ is inductively defined by $t[t']_{|\epsilon} = t'$ and, for all $0 \leq i < n$ and $p \in (\pi t_i)$, $(\text{tree}[t_0, \dots, t_i, \dots, t_{n-1}])t'_{|(i \cdot p)} = \text{tree}^\circ[t_1, \dots, t_i[t']_{|p}, \dots, t_{n-1}]$. The rewriting relation is defined as follows: two trees $t, t'$ are in the relation if there exists a $\perp$-position $p \in \pi t$ and a tree $t''$ such that $t' = t[t'']_{|p}$. Then, we prove that the $\leq^\circ$ order is the reflexive-transitive closure of the rewriting relation; and the approximation $\|\cdot\|_N$ can be defined as substituting $t_{|p}$ with $\perp$ at all positions of length $N$ in $t$.

Another observation that will be useful ahead in the paper is related to independent positions: two positions $p, p' \in \mathbb{N}^*$ are independent if none of them is a prefix of the other one. Given trees $t_1, t_2, t_3$ and two independent positions $p_1, p_2 \in \pi t$ the following equality holds: $(t_1[t_1]_{|p_1})[t_2]_{|p_2} = (t_2[t_2]_{|p_2})[t_1]_{|p_1}$, that is, the substitutions of $t_1, t_2$ in $t$ at the independent positions $p_1, p_2$ can be done in any order.
Refinements of trees as defined in Example 1 include, e.g., terms built over many-sorted first-order signatures and variations thereof [3], providing us with a rich set of examples satisfying the assumptions required for “completing” them to infinite terms and defining corecursive functions over them.

We now proceed with a some technical developments required for the completion operation. The presentation is independent of any model of Assumption 1, hence, it works for all such models.

**Remark.** Assumption 1 item 2.(b) implies that for increasing sequences $(s_n)_{n \in \mathbb{N}}$, the sequence $(\|s_n\|^N)_{n \in \mathbb{N}}$ is increasing. Hence, for ascending sequences $(s_n)_{n \in \mathbb{N}}$ the sequence $(\|s_n\|^N)_{n \in \mathbb{N}}$ is increasing and stabilizing (cf. Item 3 of the Assumption) and therefore has a limit: the value at which the sequence stabilizes.

**Lemma 1** Assume two increasing and stabilizing sequences $(s_n)_{n \in \mathbb{N}}$, $(s'_n)_{n \in \mathbb{N}}$ over $C^\circ$, such that for all $n \in \mathbb{N}$, $s_n \le \theta s'_n$. Then $\lim_{\|\cdot\| \le \theta} \lim_{\|\cdot\| \in \mathbb{N}} \|\cdot\| < \infty$.

*Proof.* Per the above observations, $\lim_{\|\cdot\| \in \mathbb{N}} \|\cdot\|$ is the value at which $(s_n)_{n \in \mathbb{N}}$ stabilizes, hence, there exists $i \in \mathbb{N}$ such that for all $j \ge i$, $s_j = \lim_{\|\cdot\| \in \mathbb{N}} \|\cdot\|$. Similarly, there exists $i' \in \mathbb{N}$ such that for all $j \ge i'$, $s'_j = \lim_{\|\cdot\| \in \mathbb{N}} \|\cdot\| = s_{i''}$; by hypothesis of the lemma $s_{i''} \le \theta s'_{i''}$ holds; and $s_{i''} = \lim_{\|\cdot\| \in \mathbb{N}} \|\cdot\|$. By transitivity, $\lim_{\|\cdot\| \in \mathbb{N}} \|\cdot\| \le \theta \lim_{\|\cdot\| \in \mathbb{N}} \|\cdot\|$, which proves the lemma.

Another consequence of Assumption 1 is the following lemma.

**Lemma 2** For all $c \in C^\circ$ there exists $N \in \mathbb{N}$ such that for all $N' \ge N$, $\|c\|^{N'} = c$.

*Proof.* $N$ such that $\|c\|^N = c$ exists by Assumption 1 item 2.(d). Consider any $N' \ge N$. We have $c = \|c\|^N$ by item 2.(d), hence, $c \le \theta \|c\|^{N'}$ using item 2.(c), and $\|c\|^{N'} \le \zeta c$ by item 2.(a). Using the antisymmetry of the $\le \theta$ relation we obtain that for the arbitrarily chosen $N' \ge N$, $\|c\|^{N'} = c$, which proves the lemma.

## 2.3 An Equivalence Relation on Sequences

Similar sequences eventually reach elements that are pairwise equal up to arbitrary close approximations:

**Definition 5** Two sequences $(s_n)_{n \in \mathbb{N}}$, $(s'_n)_{n \in \mathbb{N}}$ over $C^\circ$ are similar, written $(s_n)_{n \in \mathbb{N}} \sim (s'_n)_{n \in \mathbb{N}}$, whenever for all $N \in \mathbb{N}$ there exists $i \in \mathbb{N}$ such that for all $j \ge i$, $\|s_j\|^N = \|s'_j\|^N$.

**Lemma 3** The similarity relation $\sim$ is an equivalence relation on sequences over $C^\circ$.

*Proof.* Reflexivity and symmetry are immediate. For transitivity, assume $(s_n)_{n \in \mathbb{N}} \sim (s'_n)_{n \in \mathbb{N}}$ and $(s'_n)_{n \in \mathbb{N}} \sim (s''_n)_{n \in \mathbb{N}}$. Choose any $N \in \mathbb{N}$. From $(s_n)_{n \in \mathbb{N}} \sim (s'_n)_{n \in \mathbb{N}}$ we obtain $i \in \mathbb{N}$ such that for all $j \ge i$, $\|s_j\|^N = \|s'_j\|^N$, and from $(s'_n)_{n \in \mathbb{N}} \sim (s''_n)_{n \in \mathbb{N}}$ we obtain $i' \in \mathbb{N}$ such that for all $j \ge i'$, $\|s'_j\|^N = \|s''_j\|^N$. Setting $i'' := \max i i'$ we get: for all $j \ge i''$, $\|s_j\|^N = \|s'_j\|^N = \|s''_j\|^N$; which proves $(s_n)_{n \in \mathbb{N}} \sim (s'_n)_{n \in \mathbb{N}}$ and establishes transitivity.

**Lemma 4** For an increasing sequence $(s_n)_{n \in \mathbb{N}}$, let $s$ be the (unique) value at which $(\|s_n\|^N)_{n \in \mathbb{N}}$ stabilizes. If $(s_n)_{n \in \mathbb{N}} \sim (s'_n)_{n \in \mathbb{N}}$ then $(\|s'_n\|^N)_{n \in \mathbb{N}}$ also stabilizes at $s$.

*Proof.* From the stabilization hypothesis we obtain $i \in \mathbb{N}$ such that for all $j \ge i$, $\|s_j\|^N = s$. From $(s_n)_{n \in \mathbb{N}} \sim (s'_n)_{n \in \mathbb{N}}$ we obtain $i'$ such that for all $j \ge i'$, $\|s_j\|^N = \|s'_j\|^N$. Setting $i'' := \max i i'$ we obtain that for all $j \ge i''$, $\|s'_j\|^N = \|s_j\|^N = s$. Hence, $(\|s'_n\|^N)_{n \in \mathbb{N}}$ stabilizes at $s$; which proves the lemma.

Lemma 4 helps defining approximations of equivalence classes $\|[(s_n)_{n \in \mathbb{N}}]\|^N$ of ascending sequences:

**Definition 6** For any ascending sequence over $C^\circ$, $\|[(s_n)_{n \in \mathbb{N}}]\|^N = \lim_{\|\cdot\| \in \mathbb{N}} \|\cdot\|^N$.

Indeed, Lemma 4 says that the above definition is independent on the chosen representative in the class. This is essential in the rest of the paper. Unless otherwise stated, sequences are assumed to be over $C^\circ$.
**Lemma 5** For ascending sequences $(s_n)_{n \in \mathbb{N}}$ and $(s'_n)_{n \in \mathbb{N}}$ it holds that $(s_n)_{n \in \mathbb{N}} \sim (s'_n)_{n \in \mathbb{N}}$ if and only if for all $N \in \mathbb{N}$, $\llbracket (s_n)_{n \in \mathbb{N}} \rrbracket^N = \llbracket (s'_n)_{n \in \mathbb{N}} \rrbracket^N$.

*Proof.* (⇒): per the above remarks, $\llbracket (s_n)_{n \in \mathbb{N}} \rrbracket^N = \lim(\llbracket (\llbracket s_n \rrbracket^N)_{n \in \mathbb{N}} \rrbracket)$ and $\llbracket (s'_n)_{n \in \mathbb{N}} \rrbracket^N = \lim(\llbracket (\llbracket s'_n \rrbracket^N)_{n \in \mathbb{N}} \rrbracket)$. If $(s_n)_{n \in \mathbb{N}} \sim (s'_n)_{n \in \mathbb{N}}$ we know by Lemma 4 that the value $\lim(\llbracket (\llbracket s_n \rrbracket^N)_{n \in \mathbb{N}} \rrbracket)$ at which $(\llbracket s_n \rrbracket^N)_{n \in \mathbb{N}}$ stabilizes equals the value $\lim(\llbracket (\llbracket s'_n \rrbracket^N)_{n \in \mathbb{N}} \rrbracket)$ at which $(\llbracket s'_n \rrbracket^N)_{n \in \mathbb{N}}$ stabilizes. Hence, $\llbracket (s_n)_{n \in \mathbb{N}} \rrbracket^N = \llbracket (s'_n)_{n \in \mathbb{N}} \rrbracket^N$.

( ⇐ ): Choose an arbitrary $N \in \mathbb{N}$. Per the above remarks, from the hypothesis $\llbracket (s_n)_{n \in \mathbb{N}} \rrbracket^N = \llbracket (s'_n)_{n \in \mathbb{N}} \rrbracket^N$ we obtain that the value $\lim(\llbracket (\llbracket s_n \rrbracket^N)_{n \in \mathbb{N}} \rrbracket)$ at which $\llbracket (s_n)_{n \in \mathbb{N}} \rrbracket^N$ stabilizes equals the value $\lim(\llbracket (\llbracket s'_n \rrbracket^N)_{n \in \mathbb{N}} \rrbracket)$ at which $\llbracket (s'_n)_{n \in \mathbb{N}} \rrbracket^N$ stabilizes. Let $i$ be the least natural number such that for all $j \ge i$, $\llbracket s_j \rrbracket^N = \lim(\llbracket (\llbracket s_n \rrbracket^N)_{n \in \mathbb{N}} \rrbracket)$ and let $i'$ be the least natural number such that for all $j \ge i'$, $\llbracket s'_j \rrbracket^N = \lim(\llbracket (\llbracket s'_n \rrbracket^N)_{n \in \mathbb{N}} \rrbracket)$. Set $i'' := \max i i'$. Hence, for all $j \ge i''$, $\llbracket s'_j \rrbracket^N = \llbracket s'_j \rrbracket^N$ and since $N$ was chosen arbitrarily, by Definition 5, $(s_n)_{n \in \mathbb{N}} \sim (s'_n)_{n \in \mathbb{N}}$; which proves the ( ⇐ ) implication and the lemma.

## 2.4 An Order Relation on Equivalence Classes of Sequences

**Notation.** We denote by $K$ the set of equivalence classes of ascending sequences of elements in $C^\circ$.

**Definition 7** For $k, k' \in K$, $k \le k'$ whenever for all $N \in \mathbb{N}$, $\llbracket k \rrbracket^N \le \llbracket k' \rrbracket^N$.

**Lemma 6** The relation $\leq$ is a partial order on $K$.

*Proof.* Reflexivity and transitivity of $\leq$ easily result from the corresponding properties of $\leq^\circ$. For antisymmetry: let $k = [(s_n)_{n \in \mathbb{N}}]_\sim$ and $k' = [(s'_n)_{n \in \mathbb{N}}]_\sim$. Then, $k \le k'$ means that for all $N \in \mathbb{N}$, $\llbracket (s_n)_{n \in \mathbb{N}} \rrbracket^N \le \llbracket (s'_n)_{n \in \mathbb{N}} \rrbracket^N$, and $k' \le k$ means that for all $N \in \mathbb{N}$, $\llbracket (s'_n)_{n \in \mathbb{N}} \rrbracket^N \le \llbracket (s_n)_{n \in \mathbb{N}} \rrbracket^N$. As $\leq^\circ$ is antisymmetric, for all $N \in \mathbb{N}$, $\llbracket (s_n)_{n \in \mathbb{N}} \rrbracket^N = \llbracket (s'_n)_{n \in \mathbb{N}} \rrbracket^N$, and by Lemma 5, $(s_n)_{n \in \mathbb{N}} \sim (s'_n)_{n \in \mathbb{N}}$, i.e., $[(s_n)_{n \in \mathbb{N}}]_\sim = [(s'_n)_{n \in \mathbb{N}}]_\sim$: the lemma is proved.

We give an equivalent characterization of the order $\leq$, expressed as Lemma 8 below. To prove that lemma we need the monotonicity of approximations of equivalence classes:

**Lemma 7** If $k \in K$ and $N \le N'$ then $\llbracket k \rrbracket^N \le \llbracket k' \rrbracket^{N'}$.

*Proof.* Let $k = [(s_n)_{n \in \mathbb{N}}]_\sim$, thus, $\llbracket k \rrbracket^N = \lim(\llbracket (\llbracket s_n \rrbracket^N)_{n \in \mathbb{N}} \rrbracket)$ and $\llbracket k \rrbracket^{N'} = \lim(\llbracket (\llbracket s_n \rrbracket^{N'})_{n \in \mathbb{N}} \rrbracket)$. Using Assumption 1 item 2.(c), for all $n \in \mathbb{N}$, $\llbracket s_n \rrbracket^N \le \llbracket s_n \rrbracket^{N'}$. By Lemma 1 we obtain $\lim(\llbracket (\llbracket s_n \rrbracket^N)_{n \in \mathbb{N}} \rrbracket) \le \lim(\llbracket (\llbracket s_n \rrbracket^{N'})_{n \in \mathbb{N}} \rrbracket)$. Hence the conclusion $\llbracket k \rrbracket^N \le \llbracket k' \rrbracket^{N'}$.

**Lemma 8** $k \le k'$ if and only if for all $N \in \mathbb{N}$ there is $N' \in \mathbb{N}$ such that $\llbracket k \rrbracket^N \le \llbracket k' \rrbracket^{N'}$.

*Proof.* (⇒): this direction is trivial, as by Definition 7 $k \le k'$ means that for all $N \in \mathbb{N}$ there does exist $N' := N$ such that $\llbracket k \rrbracket^N \le \llbracket k' \rrbracket^{N'}$.

( ⇐ ): Choose an arbitrary $N \in \mathbb{N}$. For the corresponding $N' \in \mathbb{N}$ we have two cases:

* either $N' < N$, in which case by Lemma 7, $\llbracket k' \rrbracket^{N'} \le \llbracket k' \rrbracket^N$ and by transitivity using hypothesis $\llbracket k \rrbracket^N \le \llbracket k' \rrbracket^{N'}$ we obtain $\llbracket k \rrbracket^N \le \llbracket k' \rrbracket^N$;

* or $N \ge N'$, and from $\llbracket k \rrbracket^N \le \llbracket k' \rrbracket^{N'}$, using Assumption 1 item 2.(b) we obtain $\llbracket \llbracket k \rrbracket^N \rrbracket^N \le \llbracket \llbracket k' \rrbracket^{N'} \rrbracket^N$, which, by using item 2.(e), amounts to $\llbracket k \rrbracket^N \le \llbracket k' \rrbracket^N$.

Since $N \in \mathbb{N}$ has been arbitrarily chosen and in all cases $\llbracket k \rrbracket^N \le \llbracket k' \rrbracket^N$, by Definition 7 we obtain $k \le k'$, which proves the ( ⇐ ) implication and the lemma.
### 3 Completion

We show how a partially ordered set with a least element ($C^\circ, \leq^\circ, \perp$) satisfying Assumption 1 can be completed in order to obtain an $\omega$CPO ($C, \leq, \perp$). We have already noted that increasing and stabilizing sequences have limits. Hence, limits have to be constructed for the ascending sequences.

**Definition 8** Given a triple ($C^\circ, \leq^\circ, \perp$) satisfying Assumption 1, the completion operation consists in

1. extending the base set $C^\circ$ to a set $C = C^\circ \cup K$ where $K$ is the set of equivalence classes $[(s_n)_{n \in \mathbb{N}}]_\omega$ of ascending sequences over $C^\circ$;

2. defining the limits of each ascending sequence $(s_n)_{n \in \mathbb{N}}$ over $C^\circ$ to be the equivalence class of the sequence: $\lim_{n \to \infty} ((s_n)_{n \in \mathbb{N}}) \triangleq [(s_n)_{n \in \mathbb{N}}]$.

3. extending the order $\leq^\circ$ on $C^\circ$ to a relation $\leq$ on $C$ as follows:

(a) for $c, c' \in C^\circ$, $c \leq c$ whenever $c \leq^\circ c'$;

(b) for $c \in C$ and $k \in K$, $c \leq k$ whenever there exists $N \in \mathbb{N}$ such that $c \leq^\circ \lceil k \rceil^N$;

(c) for $k, k' \in K$, $k \leq k'$ whenever $k \leq^\circ k'$.

**Remark.** Definition 8 says nothing about limits of increasing sequences containing elements that are themselves limits (from $K$). Such sequences are dealt with ahead in the paper and shown to have limits among the new elements. Hence, the $\omega$CPO construction does not require further completion steps.

A key difference with the earlier completion operation in [9] is that equivalence classes there were all maximal with respect to the order; this was required in order to exclude limit elements (in $K$) from occurring in ascending sequences. In the new construction, limit elements are not excluded any more from ascending sequences, which enables us to have a nontrivial order on $K$, in which maximal elements are seen as “totally defined”, but in which “partially defined”, non-maximal limit elements also exist.

We now show that the relation $\leq$ is an order and that the constructed limits are least upper bounds of the respective sequences. This is then used in the next subsection in order to provide limits to sequences that include both finite elements and equivalence classes, and to prove that those limits are least upper bounds as well, thereby completing the organization of old and new elements and their order as an $\omega$CPO.

**Lemma 9** In the context of Definition 8, the relation $\leq$ is an order relation on $C$.

*Proof.* The reflexivity of $\leq$ follows from those of $\leq^\circ$ and of $\leq$. For antisymmetry: on $C^\circ$ it follows from the antisymmetry of $\leq^\circ$. On $K$, it follows from the antisymmetry of $\leq$. These are the only situations to consider, as for $c \in C^\circ$ and $k \in K$ having $k \leq c$ is impossible according to Definition 8.

There remains to prove that $\leq$ is transitive. There are only 4 possible cases:

1. $c, c', c'' \in C^\circ$ with $c \leq c'$, $c' \leq c''$: by Definition 8 of completion item 3.(a), here $\leq$ is $\leq^\circ$ and the required $c \leq c''$ results from the transitivity of $\leq^\circ$;

2. $c, c' \in C^\circ$ and $k \in K$ with $c \leq c'$ and $c' \leq k$: by Definition 8 item 3.(b), the latter means there exists $N \in \mathbb{N}$ such that $c' \leq^\circ \lceil k \rceil^N$, and since $c \leq c'$, the same $N$ ensures $c \leq^\circ \lceil k \rceil^N$ and thus $c \leq k$;

3. $c \in C^\circ$ and $k, k' \in K$ with $c \leq k$ and $k \leq k'$: by Definition 8 item 3.(b), there exists $N \in \mathbb{N}$ such that $c \leq^\circ \lceil k \rceil^N$, and by Definition 7 and item 3.(c), $\lceil k \rceil^N \leq^\circ \lceil k' \rceil^N$, thus, by transitivity, there exists $N \in \mathbb{N}$ such that $c \leq^\circ \lceil k' \rceil^N$, meaning that $c \leq k'$;

4. $k, k', k'' \in K$ with $k \leq k'$ and $k' \leq k''$: by Definition 8 item 3.(c), here $\leq$ is $\leq$ and the required $k \leq k''$ results from the transitivity of $\leq$. This concludes the proof of transitivity for $\leq$ and of the lemma as a whole.
**Lemma 10** In the context of Definition 8, the limit $\lim[(s_n)_{n \in \mathbb{N}}]$ of an ascending sequence $(s_n)_{n \in \mathbb{N}}$ over $C^\circ$ is a least upper bound for $(s_n)_{n \in \mathbb{N}}$.

*Proof.* By Definition 8, given an ascending sequence $(s_n)_{n \in \mathbb{N}}$, it follows that $\lim[(s_n)_{n \in \mathbb{N}}]$ is defined to be the equivalence class $[(s_n)_{n \in \mathbb{N}}]_{\sim}$ of the sequence.

We first prove that $[(s_n)_{n \in \mathbb{N}}]_{\sim}$ is an upper bound for the sequence $(s_n)_{n \in \mathbb{N}}$. That is, we must prove that for all $n \in \mathbb{N}$, $s_n \le [(s_n)_{n \in \mathbb{N}}]_{\sim}$. Choose an arbitrary $n \in \mathbb{N}$, and choose $N$ such that $\|s_n\|^N = s_n$. This is made possible by Assumption 1 item 2.(d). We then have $s_n = \|s_n\|^N \le \lim_{(\|s_n\|^N)_{n \in \mathbb{N}} \to \|s_n\|^N} \|(\|s_n\|^N)_{n \in \mathbb{N}}\| = \|(s_n)_{n \in \mathbb{N}}\|_{\sim}^N$. Hence, $s_n \le \|(s_n)_{n \in \mathbb{N}}\|_{\sim}^N$ and, by Definition 8 item 3.(b), $s_n \le [(s_n)_{n \in \mathbb{N}}]_{\sim}$. The upper-bound claim of $[(s_n)_{n \in \mathbb{N}}]_{\sim}$ with respect to $(s_n)_{n \in \mathbb{N}}$ is proved.

We now prove that $[(s_n)_{n \in \mathbb{N}}]_{\sim}$ is the least upper bound of $(s_n)_{n \in \mathbb{N}}$. Assume $b \in C$ such that for all $n \in \mathbb{N}$, $s_n \le b$. There are two cases to consider: $b \in C^\circ$ or $b \in K$. If $b \in C^\circ$ then for all $n \in \mathbb{N}$, $s_n \le b$. But this is impossible by Assumption 1 item 1 since $(s_n)_{n \in \mathbb{N}}$ is ascending.

If $b \in K$, then $b = [(s'_n)_{n \in \mathbb{N}}]_{\sim}$ for some ascending sequence $(s'_n)_{n \in \mathbb{N}}$. From the fact that for all $n \in \mathbb{N}$, $s_n \le [(s'_n)_{n \in \mathbb{N}}]_{\sim}$, using Assumption 1 item 2.(b) we obtain that for all $n \in \mathbb{N}$, there is $N' \in \mathbb{N}$ such that $s_n \le \|(s'_n)_{n \in \mathbb{N}}\|_{\sim}^N$. Choose an arbitrary $N \in \mathbb{N}$. Since for all $n \in \mathbb{N}$, $\|s_n\|^N \le s_n$ we further obtain that for all $n \in \mathbb{N}$ there exists $N' \in \mathbb{N}$ such that $\|s_n\|^N \le \|(s'_n)_{n \in \mathbb{N}}\|_{\sim}^N$. Now, the sequence $(\|s_n\|^N)_{n \in \mathbb{N}}$ is increasing and stabilizing, and $\lim_{(\|s_n\|^N)_{n \in \mathbb{N}} \to \|s_n\|^N} \|(\|s_n\|^N)_{n \in \mathbb{N}}\| = \|(s_n)_{n \in \mathbb{N}}\|_{\sim}^N$ is an element, say, $\|s_k\|^N$ of the sequence. We thus obtain that for the arbitrarily chosen $N \in \mathbb{N}$, there exists $N' \in \mathbb{N}$ such that $\lim_{(\|s_n\|^N)_{n \in \mathbb{N}} \to \|s_n\|^N} \|(\|s_n\|^N)_{n \in \mathbb{N}}\| = \|(s_n)_{n \in \mathbb{N}}\|_{\sim}^N$. Moreover, we know that $\lim_{(\|s_n\|^N)_{n \in \mathbb{N}} \to \|s_n\|^N} \|(\|s_n\|^N)_{n \in \mathbb{N}}\| = \|(s_n)_{n \in \mathbb{N}}\|_{\sim}^N$. We thus obtain that for all $N \in \mathbb{N}$, there exists $N' \in \mathbb{N}$ such that $\|s_n\|^N \le \|(s'_n)_{n \in \mathbb{N}}\|_{\sim}^N$. By Lemma 8 we obtain $[(s_n)_{n \in \mathbb{N}}]_{\sim} \le [(s'_n)_{n \in \mathbb{N}}]_{\sim}$. Then, by Definition 8 item 3.(c), $[(s_n)_{n \in \mathbb{N}}]_{\sim} \le [(s'_n)_{n \in \mathbb{N}}]_{\sim} = b$. Thus, in the only possible case ($b \in K$) we have obtained that $[(s_n)_{n \in \mathbb{N}}]_{\sim}$ is $\le$-ordered with $b$. This concludes the proof of the lemma.

## 3.1 Completion + Diagonalization = $\omega$CPO

In this section we show how to “finish” the completion operation in the previous section in order to obtain an $\omega$CPO. We add what is missing: limits for ascending sequences that include equivalence classes. The main idea is to use a diagonalization technique to extract an ascending sequence of finite elements from an ascending sequence that includes equivalence classes. We need a few technical lemmas. The first lemma adapts Assumption 1 items 2.(a)-(c), which hold for elements of $C^\circ$, to the elements of $K$.

**Lemma 11**

1. for all $k \in K$ and $N \in \mathbb{N}$, $\|k\|^N \le k$;

2. for all $k, k' \in K$ and $N \in \mathbb{N}$, $k \le k'$ implies $\|k\|^N \le \|k'\|^N$;

3. for all $k \in K$ and $N, N' \in \mathbb{N}$, $N \le N'$ implies $\|k\|^N \le \|k'\|^N$.

*Proof.*

1. The approximation $\|k\|^N$ is an element of $C^\circ$, hence, by Definition 8 item 3.(b), for $\|k\|^N \le k$ it is enough to show that there exists $N' \in \mathbb{N}$ such that $\|k\|^N \le \|k'\|^N$. Setting $N' := N$ ensures this;

2. By Definition 8 item 3.(c), $k \le k'$ is just $k \le k'$, which by Definition 7 is just the conclusion of this item - that for all $N \in \mathbb{N}$, $\|k\|^N \le \|k'\|^N$;

3. Both $\|k\|^N$ and $\|k'\|^N$ are elements of $C^\circ$, thus, $\le = \le^\circ$, and the conclusion follows by Lemma 7.

The next lemma establishes that ascending sequences are similar to any of their subsequences.
**Lemma 12** Consider an ascending sequence $(s_n)_{n \in \mathbb{N}}$ and a subsequence $(s_{(\varphi n)})_{n \in \mathbb{N}}$ of it, for some strictly increasing $\varphi : \mathbb{N} \to \mathbb{N}$. Then $(s_n)_{n \in \mathbb{N}} \sim (s_{(\varphi n)})_{n \in \mathbb{N}}$.

*Proof.* As a subsequence of an ascending sequence, $(s_{(\varphi n)})_{n \in \mathbb{N}}$ is ascending. Let $k = [(s_n)_{n \in \mathbb{N}}]_{\sim}$ and $k' = [(s_{(\varphi n)})_{n \in \mathbb{N}}]_{\sim}$. We observe that, by Lemma 8, showing $k = k'$ is equivalent to finding, for each $N \in \mathbb{N}$, some $N' \in \mathbb{N}$ such that $\lceil k \rceil^N = \lceil k' \rceil^{N'}$. Let $N' := N$. Using Definition 6, we have to show that $\lim_{j \to \infty} (\lceil s_n \rceil^N)_{n \in \mathbb{N}} = \lim_{j \to \infty} (\lceil s_{(\varphi n)} \rceil^N)_{n \in \mathbb{N}}$. Let $n_0$ be the least natural number such that $\lim_{j \to \infty} (\lceil s_n \rceil^N)_{n \in \mathbb{N}} = \lceil s_{n_0} \rceil^N$, and let $n_1 \in \mathbb{N}$ be such that $\lim_{j \to \infty} (\lceil s_{(\varphi n)} \rceil^N)_{n \in \mathbb{N}} = \lceil s_{n_1} \rceil^N$. $n_1 < n_0$ contradicts the minimality of $n_0$, hence, $n_1 \ge n_0$, which implies $\lim_{j \to \infty} (\lceil s_n \rceil^N)_{n \in \mathbb{N}} = \lceil s_{n_1} \rceil^N = \lim_{j \to \infty} (\lceil s_{(\varphi n)} \rceil^N)_{n \in \mathbb{N}}$ and proves the lemma.

We next introduce a notion of “diagonalization” for an equivalence class of ascending sequences.

**Definition 9** For $k \in K$, the sequence $(\lceil k \rceil^n)_{n \in \mathbb{N}}$ is called the *diagonal of k*.

The main interest of diagonalization is that it gives a “canonical” representative for the class.

**Lemma 13** For all $k \in K$, the sequence $(\lceil k \rceil^n)_{n \in \mathbb{N}}$ is ascending, and $\lim_{j \to \infty} (\lceil k \rceil^j)_{n \in \mathbb{N}} = k$.

*Proof.* We first prove the following technical result about ascending sequences: (†) if $(s_m)_{m \in \mathbb{N}}$ is an ascending sequence, then for all $j, n \in \mathbb{N}$ there exist $j' > n, n' > n$ such that $\lceil s_j \rceil^n < \lceil s_{j'} \rceil^{n'}$.

Proof of (†): there exists $j' > k$ such that $s_j < s_{j'}$. Moreover, for large enough $n'$ (in particular, $n' > Nn$) $\lceil s_{j'} \rceil^{n'} = s'_j$ (by Assumption 1, items 2(d)(c)(a)). Hence, $\lceil s_j \rceil^n \le \lceil s_j < s'_{j'} \rceil = \lceil s_{j'} \rceil^{n'}$, i.e., (†).

We now prove that $(\lceil k \rceil^n)_{n \in \mathbb{N}}$ is ascending. By Lemma 11 item 3 it is increasing. Choose an ascending sequence $(s_n)_{n \in \mathbb{N}} \in k$. Fix an arbitrary $n \in \mathbb{N}$. It holds that $\lceil k \rceil^n = \lim_{j \to \infty} (\lceil s_m \rceil^j)_{m \in \mathbb{N}}$. Now, $\lim_{j \to \infty} (\lceil s_m \rceil^j)_{m \in \mathbb{N}} = \lceil s_j \rceil^n$ for some $j \in \mathbb{N}$. Using (†) there exists $j' > j$ and $n' > n$ such that $\lceil s_j \rceil^n < \lceil s_{j'} \rceil^{n'}$. But $\lceil s_{j'} \rceil^{n'} \le \lim_{m \to \infty} (\lceil s_m \rceil^{n'})_{m \in \mathbb{N}}$. Overall, for the arbitrarily chosen $n \in \mathbb{N}$, there exists $n' > n$ such that $\lceil k \rceil^n = \lim_{j \to \infty} (\lceil s_m \rceil^j)_{m \in \mathbb{N}} < \lim_{j \to \infty} (\lceil s_m \rceil^{n'})_{m \in \mathbb{N}} = \lceil k \rceil^{n'}$, which proves that $(\lceil k \rceil^n)_{n \in \mathbb{N}}$ is ascending.

Finally, we prove that $\lim_{j \to \infty} (\lceil k \rceil^j)_{n \in \mathbb{N}} = k$, i.e., $k$ is the least upper bound of $(\lceil k \rceil^n)_{n \in \mathbb{N}}$. By Lemma 11 item 1, $k$ is an upper bound of $(\lceil k \rceil^n)_{n \in \mathbb{N}}$. We now prove it is the least upper bound. For, assuming an upper bound $k' \in C^\circ \cup K$, from Assumption 1 item 1 and the ascending property of $(\lceil k \rceil^n)_{n \in \mathbb{N}}$ we know that $k' \in C^\circ$ is impossible, hence, $k' \in K$. Now, since $k'$ is an upper bound, for all $n \in \mathbb{N}$, $\lceil k \rceil^n \le k'$. Choose an arbitrary $n \in \mathbb{N}$. Since $\lceil k \rceil^n \in C^\circ$ and $k' \in K$, by Definition 8 item 3 (b), there exists $n' \in \mathbb{N}$ such that $\lceil k \rceil^n \le \lceil k' \rceil^{n'}$. By Lemma 8 we obtain $k \le k'$, which shows $\lim_{j \to \infty} (\lceil k \rceil^j)_{n \in \mathbb{N}} = k$ and completes the proof.

**Notation.** For equivalence classes $k, k' \in K$ we write $k < k'$ for $k \le k'$ and $k \ne k'$. We denote by $C^\omega$ the set of sequences over a set $C$. We also call *diagonal* of $s \in (C^\circ \cup K)^\omega$ the sequence $(\lceil s_n \rceil^n)_{n \in \mathbb{N}} \in (C^\circ)^\omega$.

**Lemma 14** If $s \in (C^\circ \cup K)^\omega$ is increasing, the sequence $(\lceil s_n \rceil^n)_{n \in \mathbb{N}} \in (C^\circ)^\omega$ is increasing as well.

*Proof.* Any two consecutive elements $\lceil s_{i-1} \rceil^{i-1}$ and $\lceil s_i \rceil^i$ satisfy $\lceil s_{i-1} \rceil^{i-1} \le \lceil s_i \rceil^i$ by Lemma 11 items 2&3.

**Lemma 15** For all $k, k' \in K$, $k < k'$ implies that there exists $j \in \mathbb{N}$ such that for all $j' \ge j$, $\lceil k \rceil^{j'} < \lceil k' \rceil^{j'}$.

*Proof.* $k < k'$ implies in particular $k \le k'$. Assuming the negation of the conclusion, for each $j \in \mathbb{N}$ there exists $j' > j$ such that $\lceil k \rceil^{j'} < \lceil k' \rceil^{j'}$. But $k \le k'$ implies $\lceil k \rceil^{j'} \le \lceil k' \rceil^{j'}$, hence, for each $j \in \mathbb{N}$ there exists $j' > j$ such that $\lceil k \rceil^{j'} = \lceil k' \rceil^{j'}$, which means that there exists a strictly increasing function $\varphi : \mathbb{N} \to \mathbb{N}$ such that for all $j \in \mathbb{N}$, $\lceil k \rceil^{(\varphi j)} = \lceil k' \rceil^{(\varphi j)}$, i.e., $(\lceil k \rceil^{(\varphi j)})_{j \in \mathbb{N}} = (\lceil k' \rceil^{(\varphi j)})_{j \in \mathbb{N}}$. But $(\lceil k \rceil^{(\varphi j)})_{j \in \mathbb{N}}$
is a subsequence of the diagonal $(\llcorner k \rrcorner^j)_{j \in \mathbb{N}}$ of $k$, an ascending sequence according to Lemma 13, hence, by Lemma 12, $(\llcorner k \rrcorner^j)_{j \in \mathbb{N}} \sim (\llcorner k \rrcorner^{(\varphi^j)})_{j \in \mathbb{N}}$, and, again using Lemma 13, $k = \lim(\langle(\llcorner k \rrcorner^{(\varphi^j)})_{j \in \mathbb{N}}\rangle)$. Similarly, $k' = \lim(\langle(\llcorner k' \rrcorner^{(\varphi^j)})_{j \in \mathbb{N}}\rangle)$, i.e., $k = k'$, in contradiction with the hypothesis $k < k'$. The contradiction arises from negating the conclusion of the lemma, hence, the lemma is proved.

**Lemma 16** Consider a strictly increasing sequence $(k_n)_{n \in \mathbb{N}} \in K^\omega$. Then $(\llcorner k_n \rrcorner^n)_{n \in \mathbb{N}} \in (C^\circ)^\omega$ is ascending.

*Proof.* We build by induction a strictly increasing subsequence $(\llcorner k_i \rrcorner^{i_n})_{n \in \mathbb{N}}$ of $(\llcorner k_n \rrcorner^n)_{n \in \mathbb{N}}$. For the base case the subsequence is $\llcorner k_0 \rrcorner^0$. Assume now the subsequence of interest has been built up to a given length, hence, its last element is of the form $\llcorner k_{i_j} \rrcorner^{i_j}$. We have, by the strictly increasing nature of $(k_n)_{n \in \mathbb{N}}$, $k_{i_j} < k_{i_j+1}$, hence, using Lemma 11 item 1, $\llcorner k_{i_j} \rrcorner^{i_j} < k_{i_j+1}$. Using Lemma 15 and Assumption 1 items 2.(d) and 2.(c), we can find a $i' > i_j + 1$ which is large enough to ensure $\llcorner \llcorner k_{i_j} \rrcorner^{i_j} \rrcorner^{i'} = \llcorner k_{i_j} \rrcorner^{i_j}$, such that $\llcorner \llcorner k_{i_j} \rrcorner^{i_j} \rrcorner^{i'} < \llcorner k_{i_j+1} \rrcorner^{i'}$. Since $i' > i_j + 1$, by monotonicity of $(k_n)_{n \in \mathbb{N}}$, we obtain using Lemma 11 item 2, $\llcorner k_{i_j+1} \rrcorner^{i'} \le \llcorner k_{i'} \rrcorner^{i'}$, i.e., $\llcorner k_{i_j+1} \rrcorner^{i'} \le \llcorner k_{i'} \rrcorner^{i'}$ since the elements being compared are in $C^\circ$. Hence, we have obtained $i' > i_j$ such that $\llcorner k_{i_j} \rrcorner^{i_j} < \llcorner k_{i'} \rrcorner^{i'}$, and therefore have built the strictly increasing subsequence of interest up to length $j+1$. An infinite strictly increasing subsequence $(\llcorner k_{i_n} \rrcorner^{i_n})_{n \in \mathbb{N}}$ of $(\llcorner k_n \rrcorner^n)_{n \in \mathbb{N}}$ is (obviously) defined as soon as all its elements are defined. In order to define its $j$-th element, we build the finite strictly increasing subsequence by induction as above up to length $j$ and take its last element.

**Lemma 17** If $s \in (C^\circ \cup K)^\omega$ is ascending and there is $i \in \mathbb{N}$ such that $s_i \in K$, then $(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}$ is ascending.

*Proof.* By Lemma 14 the sequence $(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}$ is increasing. We only need to prove that it has a strictly ascending subsequence. Since $s$ is ascending it has a strictly increasing subsequence $(s_{i_n})_{n \in \mathbb{N}}$. Since $s_i \in K$, we obtain that for all $j \ge i$, $s_j \in K$. Consider the subsequence $(s_{i_n})_{n \in \mathbb{N}, i_n \ge i}$ of $(s_{i_n})_{n \in \mathbb{N}}$. As a subsequence of a strictly increasing subsequence, $(s_{i_n})_{n \in \mathbb{N}, i_n \ge i}$ is a strictly increasing sequence, and belongs to $K^\omega$. We apply Lemma 16 to it and get an ascending subsequence of $(s_{i_n})_{n \in \mathbb{N}, i_n \ge i}$, which by transitivity of the subsequence relation is also an ascending subsequence of the original sequence $s$ in the hypothesis.

The last lemma in this section provides limits to sequences $s \in (C^\circ \cup K)^\omega$ with at least one element in $K$.

**Lemma 18** If $s \in (C^\circ \cup K)^\omega$ is ascending and $s_i \in K$, then $[(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}]$ is the least upper bound for $s$.

*Proof.* We first prove that $[(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}]$ is an upper bound for $s$. Thus, we need to show that for all $j \in \mathbb{N}$, $s_j \le [(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}]$. Since $s$ is increasing, it is enough to show the above inequality for $j \ge i$, i.e., when $s_j \in K$. By Lemma 8 we only need to show (†): for all $N \in \mathbb{N}$, there exists $N' \in \mathbb{N}$ such that $\llcorner s_j \rrcorner^N \le \llcorner [(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}] \rrcorner^{N'}$. Choose an arbitrary $N \in \mathbb{N}$. Let $p = \max j N$. Thus, by Assumption 1 item 2.(b), $\llcorner s_j \rrcorner^N \le \llcorner s_p \rrcorner^N$. Using Assumption 1 item 2.(c), $\llcorner s_p \rrcorner^N \le \llcorner s_p \rrcorner^p$. By transitivity, $\llcorner s_j \rrcorner^N \le \llcorner s_p \rrcorner^p$. But since (by Lemma 17) $(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}$ is ascending, we know by Lemma 10 that $[(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}]$ is an upper bound for $(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}$. In particular, $\llcorner s_p \rrcorner^p \le \llcorner (\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}} \rrcorner$, and by transitivity, $\llcorner s_j \rrcorner^N \le \llcorner (\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}} \rrcorner$, which by Def. 8 item 3.(b) implies that there is $N' \in \mathbb{N}$ such that $\llcorner s_j \rrcorner^N \le \llcorner [(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}] \rrcorner^{N'}$, i.e., (†).

We now prove that $[(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}]$ is a least upper bound for $s$. Thus, assuming an upper bound $b \in C^\circ \cup K$ for $s$, we need to show that $[(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}] \le b$. Now, by Lemma 10, $[(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}]$ is the least upper bound for the ascending sequence $(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}$. Hence in order to show $[(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}] \le b$ one only has to show that $b$ is an upper bound for $(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}$. Choose an arbitrary $n \in \mathbb{N}$. We have, by Lemma 11 item 1, $\llcorner s_n \rrcorner^n \le s_n$ and since $b$ is an upper bound for $s$, $s_n \le b$. Hence, for an arbitrary $n \in \mathbb{N}$, $\llcorner s_n \rrcorner^n \le b$, which establishes that $b$ is an upper bound for $(\llcorner s_n \rrcorner^n)_{n \in \mathbb{N}}$, which completes the proof of the lemma.

This concludes the construction of the $\omega$CPO by completion.
# 4 Proving Productiveness

As already noted in Section 2 obtaining an $\omega$CPO is only the first step towards our main goal - defining total corecursive functions by unique fixpoints of their productive functionals by means of Theorem 1. The second step is to prove the productiveness requirement for given functionals. As visible in Definition 4, productiveness is concerned with certain sequences converging towards maximal elements.

## 4.1 Maximal vs. Totally Defined Elements

Maximality is easy to define, but it is not easy to prove in practice, especially for equivalence classes denoting infinite elements in an $\omega$CPO obtained by completion. In this section we provide an equivalent notion to maximality, called total definability, which is easier to use in practice because it is “computational” in nature. It is based on a “definedness” function which takes values in $\mathbb{N} \cup \{\infty\}$, a set in which one can perform computations: approximations, limits of sequences of numbers, etc. The definedness function is expected to satisfy some assumptions, stated below and justified after the statement.

**Assumption 2** We assume a definedness function $\delta: C^\circ \to \mathbb{N} \cup \{\infty\}$ satisfying the following properties:

1. for all $c, c' \in C^\circ$, $c \leq^\circ c'$ implies $\delta c \leq \delta c'$;

2. for all $c \in C^\circ$, if $\delta c = \infty$ then $c$ is maximal w.r.t. $\leq^\circ$;

3. for all $c \in C^\circ$ and $N \in \mathbb{N}$, if $\delta c \geq N$ then $\delta (\|c\|^N) = N$;

4. for all $c, c' \in C^\circ$ and $N \in \mathbb{N}$, if $c \leq^\circ c'$ and $\delta c > N$ then $\|c\|^N = \|c'\|^N$;

5. for all ascending sequences $(s_n)_{n \in \mathbb{N}} \in (C^\circ)^\omega$ and $N \in \mathbb{N}$ such that for all $n \in \mathbb{N}$, $\delta s_n \leq N$, there exists $i \in \mathbb{N}$ and an increasing sequence $(s'_j)_{j \geq i}$ such that for all $j \geq i$, $s_j \leq^\circ s'_j$ and $N < \delta s'_j$.

If $\delta c = n$ then we say that $c$ is defined up to $n$. If $c$ is defined up to $\infty$ we also say that $c$ is totally defined.

**A Model for Assumption 2** Like Assumption 1, Assumption 2 has a model in the set of tree defined in Example 1. Here, $\delta c$ is either: a natural number being the minimal length of a $\perp$-position in $c$, if $c$ has such positions; or, $c$ has no $\perp$-positions, $\delta c = \infty$. With the convention that the minimum of an empty list over $\mathbb{N} \cup \{\infty\}$ is $\infty$, i.e., $\min [] = \infty$, $\delta$ can be recursively defined as follows:

$$ \delta c = \text{if } c = \perp \text{ then } 0 \text{ else } 1 + \min(\text{map } \delta (\text{forest}^\circ c)). $$

We now justify the assumptions on the $\delta$ function.

1. for all $c, c' \in C^\circ$, $c \leq^\circ c'$ implies $\delta c \leq \delta c'$: This is monotonicity of $\delta$. If $c \leq^\circ c'$ then either $c = c'$, in which case $\delta c = \delta c'$, or $c'$ is obtained from $c'$ by rewriting some $\perp$ subtrees by non-$\perp$ ones. If $c$ and $c'$ still have at least one, common, minimal $\perp$ position then $\delta c' = \delta c$. Otherwise, due to rewriting, the $\perp$ positions of $c'$ (if any) are strictly longer than those of $c$, which implies $\delta c < \delta c'$.

2. for all $c \in C^\circ$, if $\delta c = \infty$ then $c$ is maximal w.r.t. $\leq^\circ$: $\delta c = \infty$ means that $c$ has no $\perp$-positions, i.e., it does not allow rewriting. If $c$ were non-maximal there would be $c'$ with $c <^\circ c'$, meaning rewriting would be possible from $c$. But we have just seen that it is not. Hence, $c$ is maximal.

3. for all $c \in C^\circ$ and $N \in \mathbb{N}$, if $\delta c \geq N$ then $\delta (\|c\|^N) = N$: $\delta c \geq N$ means that the are no $\perp$-positions of $c$ of length $< N$. Now, the approximation $\|c\|^N$ replaces all trees at positions of length $N$ in $c$ by $\perp$. These all the occureces of $\perp$ in $\|c\|^N$, and their positions all have length $N$, i.e., $\delta (\|c\|^N) = N$.
4. for all $c, c' \in C^\circ$ and $m \in \mathbb{N}$, if $c \le \circ c'$ and $\delta c > N$ then $\llcorner c \rrcorner^N = \llcorner c' \rrcorner^N$: here, all the $\perp$-positions of $c, c'$ are of length $> N$, and $c'$ is obtained from $c$ by rewriting in some (possiby, in zero) positions of length $> N$. Hence, this does not affect positions of length $\le N$. In particular, for all $p$ of length $\le N$, $p$ is a position of $c$ iff it is a position of $c'$, and if this is the case then $c_{lp} = c'_{lp}$. Now, the approximation of precision $N$ replaces all trees at positions of length $N$ by $\perp$. After performing the approximations, it is still the case that for all positions $p$ of length $\le N$, $p$ is a position of $\llcorner c \rrcorner^N$ iff it is a position of $\llcorner c' \rrcorner^N$, and if this is the case then $(\llcorner c \rrcorner^N)_{lp} = (\llcorner c' \rrcorner^N)_{lp}$; which implies $\llcorner c \rrcorner^N = \llcorner c' \rrcorner^N$.

5. for all ascending sequences $(s_n)_{n \in \mathbb{N}} \in (C^\circ)^\omega$ and $N \in \mathbb{N}$ such that for all $n \in \mathbb{N}$, $\delta s_n \le N$, there exists $i \in \mathbb{N}$ and an increasing sequence $(s'_j)_{j \ge i}$ such that for all $j \ge i$, $s_j \le \circ s'_j$ and $N < \delta s'_j$: we shall need to further elaborate on the definition of $\le \circ$ by rewriting: for $c, c' \in C^\circ$ and $l$ a list of positions, we inductively define the statement $c \le \circ_l c'$ by $c \le \circ_l c$ and $c \le \circ_{(p;l)} c'$ if there exist $c''$ s.t. $(c[c'']_p) \le \circ_l c'$, where "p; l" denotes adding the element $p$ at the head of the list $l$. We prove that $c \le \circ c'$ holds iff there exists a $l$ of $\perp$-positions of $c$ s.t. $c \le \circ_l c'$; and if the positions in $l$ are mutually independent from those in $l'$ and $c \le \circ_{l'} c'$ and $c \le \circ_{l''} c''$ then there exists $c'''$ such that $c' \le \circ_{l''} c'''$ and $c'' \le \circ_{l'} c'''$. Back to the statement of interest, since $(s_n)_{n \in \mathbb{N}} \in (C^\circ)^\omega$ is ascending and for all $n \in \mathbb{N}$, $\delta s_n \le N$, there must exist a first index, say, $i$, after which all rewritings that generate the subsequent elements of the sequence $(s_j)_{j \ge i}$ occur at non-minimal $\perp$-positions. Otherwise, the minimal $\perp$-positions are rewritten infinitely many times and eventually their length becomes strictly greater than $N$, in contradiction with the hypothesis for all $n \in \mathbb{N}$, $\delta s_n \le N$. We have the index $i$ and, by the manner in which it was obtained, for all $j \ge i$ $s_j \le \circ_{l_j} s_{j+1}$ for a list $l_j$ of non-minimal $\perp$-positions of $s_j$.
We now inductively build an increasing sequence $(s'_j)_{j \ge i}$ such that $N < \delta s'_j$ for all $j \ge i$ and (more than what the current statement requires) there is a list $l'$ of positions such that for all $j \ge i$, $s_j \le \circ_{l'} s'_j$. In the base case, let $l'$ be the list of all minimal $\perp$-positions of $s_i$. By replacing $\perp$ at all positions in $l'$ with sufficiently tall trees, we obtain $s_i < \circ_{l'} s'_i$ with $N < \delta s'_i$, which concludes this case.
Assume now the sequence $(s'_j)_{j \ge i}$ has been built up to some $j \ge i$. From the induction hypothesis, $s_j \le \circ_{l_j} s'_j$ and $N < \delta s'_j$. We have also obtained above that $s_j \le \circ_{l_j} s_{j+1}$ holds for a list $l_j$ of non-minimal positions of $s_j$. Hence, the positions in $l'$ and $l_j$ are mutually independent. Thus, there exists $s'_{j+1}$ with $s'_{j+1} \le \circ_{l_j} s'_{j+1}$ and $s_{j+1} \le \circ_{l'} s'_{j+1}$. Moreover, $N < \delta s'_{j+1}$ (which results from $N < \delta s'_j$ and monotononicity of $\delta$). This completes the induction step and the construction of $(s'_j)_{j \ge i}$ with the expected properties in the current statement. The model for Assumption 2 is also completed.

The remaining results in this section only rely on Assumption 1 and 2. They hold for any model of the assumption, including the trees from Example 1 and as well as terms over various kinds of signatures.

**Lemma 19** *For all $c \in C^\circ$, $c$ is totally defined if and only if $c$ is maximal w.r.t. $\le \circ$.*

*Proof.* (⇒): Suppose $\delta c = \infty$ but $c$ is not maximal, i.e., there exists $c' \in C^\circ$ such that $c < \circ c'$. Then, by the monotonicity of $\delta$ - item 1 in Assumption 2, $\delta c' = \infty$. Using Assumption 2 item 4, for all $N \in \mathbb{N}$, $\llcorner c \rrcorner^N = \llcorner c' \rrcorner^N$. By choosing $N$ large enough, using Lemma 2, we obtain $\llcorner c \rrcorner^N = c$ and $\llcorner c' \rrcorner^m = c'$, meaning that $c = c'$, in contradiction to $c < \circ c'$. The contradiction occurs due to the negation of the maximality of $c$; hence, the maximality holds. ( ⇐ ): this is just Assumption 2 item 2.

**Definition 10** *The definedness function $\delta$ from Assumption 2 is extended over $K$ by $\delta k = \lim(\| (\delta(\llcorner k \rrcorner^m)_{m \in \mathbb{N}}) \|)$. The notions of definedness up to some $n \in \mathbb{N} \cup \{\infty\}$ and total definedness are extended to $K$ as well.*

**Remark.** The limit (a.k.a. least upper bound) of a sequence of elements in $\mathbb{N} \cup \{\infty\}$ always exists, so referring to it it Definition 10 is legitimate.
**Lemma 20** For $k, k' \in K$, if $k \le k'$ then $\delta k \le \delta k'$.

*Proof.* From $k \le k'$ and Lemma 11 item 2, for all $n \in \mathbb{N}$, $\|k\|^n \le \|k'\|^n$, i.e., $\|k\|^n \le \|k'\|^n$, hence, by Assumption 2 item 1, for all $n \in \mathbb{N}$, $\delta (\|k\|^n) \le \delta (\|k'\|^n)$. Thus, $\lim(\|(\delta(\|k\|^n)_{n \in \mathbb{N}})\| \le \lim(\|(\delta(\|k'\|^n)_{n \in \mathbb{N}})\|)$, i.e., $\delta k \le \delta k'$.

**Lemma 21** For $k \in K$ and $n, m \in \mathbb{N}$, $n \ge m$ implies $\|k\|^m = \|\|k\|^n\|^m$.

*Proof.* Choose an arbitrary ascending sequence $(s_j)_{j \in \mathbb{N}} \in K$. Choose arbitrarily $n, m \in \mathbb{N}$ such that $n \ge m$. Then, by Definition 6, $\|k\|^m = \lim(\|(\|s_j\|^m)_{j \in \mathbb{N}}\|)$ and $\|k\|^n = \lim(\|(\|s_j\|^n)_{j \in \mathbb{N}}\|)$, hence, $\|\|k\|^n\|^m = \lim(\|(\|\|s_j\|^n)_{j \in \mathbb{N}}\|)^m = \lim(\|(\|\|s_j\|^n)_{j \in \mathbb{N}}\|)^m$. Using Assumption 1 item 2.(e), since $n \ge m$, $\|\|s_j\|^n\|^m = \|\|s_j\|^m\|$; hence, $\lim(\|(\|\|s_j\|^n)_{j \in \mathbb{N}}\|) = \lim(\|(\|\|s_j\|^m)_{j \in \mathbb{N}}\|) = \|k\|^m$. That is, we have obtained $\|\|k\|^n\|^m = \|k\|^m$ for arbitrarily chosen $n, m \in \mathbb{N}$ such that $n \ge m$, which proves the lemma.

**Lemma 22** For all $k \in K$, if $k \le k'$ and $\delta k = \infty$ then for all $m \in \mathbb{N}$, $\|k\|^m = \|k'\|^m$.

*Proof.* From $k \le k'$ and $\delta k = \infty$ we obtain using Lemma 20 that $\delta k' = \infty$. We note that in the diagonal $(\|k\|^n)_{n \in \mathbb{N}}$ of $k$ no element can be totally defined; otherwise by Lemma 19 that element would be maximal, in contradiction with the ascending nature of $(\|k\|^n)_{n \in \mathbb{N}}$ established in Lemma 13. The same reasoning holds for the diagonal of $k'$. Hence, for all $n \in \mathbb{N}$, $\delta(\|k\|)_n \in \mathbb{N}$ and $\delta(\|k'\|)_n \in \mathbb{N}$.

Fix an arbitrary $m \in \mathbb{N}$. Since $\delta k = \delta k' = \infty$, there exists $n$ such that $n \ge m$, $\delta (\|k\|)_n > m$. Let $c = \|k\|^n$ and $c' = \|k'\|^n$. Then, $c, c' \in C^\circ$, and $\delta c > m$. Moreover, from $k \le k'$ we obtain using Lemma 11 item 2, $\|k\|^n \le \|k'\|^n$, hence, $c \le c'$, i.e., $c \le c'$. Using Assumption 2 item 4 we obtain $\|c\|^m = \|c'\|^m$, thus, $\|\|k\|^n\|^m = \|\|k'\|^n\|^m$. Since $n \ge m$, using Lemma 21 we obtain $\|k\|^m = \|\|k\|^n\|^m$ and $\|k'\|^m = \|\|k'\|^n\|^m$, i.e., for the arbitrarily chosen $m \in \mathbb{N}$, $\|k\|^m = \|k'\|^m$, which proves the lemma.

**Lemma 23** For sequences $(s_n)_{n \in \mathbb{N}}$ and $(s'_n)_{n \in \mathbb{N}}$ in $(C^\circ)^\omega$, if $(s_n)_{n \in \mathbb{N}}$ is ascending, $(s'_n)_{n \in \mathbb{N}}$ is increasing, and for all $n \in \mathbb{N}$, $s_n \le s'_n$, then $(s'_n)_{n \in \mathbb{N}}$ is ascending and $[(s_n)_{n \in \mathbb{N}}] \le [(s'_n)_{n \in \mathbb{N}}]$.

*Proof.* Assume $(s'_n)_{n \in \mathbb{N}}$ is stabilizing to some value $c \in C^\circ$. Then for all $n \in \mathbb{N}$, $s_n \le s'_n \le c$, and since $(s_n)_{n \in \mathbb{N}}$ is ascending this contradicts Assumption 1 item 1. Hence, $(s'_n)_{n \in \mathbb{N}}$ is ascending. Let $k = [(s_n)_{n \in \mathbb{N}}] \sim$ and $k' = [(s'_n)_{n \in \mathbb{N}}] \sim$. We have to prove $k \le k'$, i.e., $k \le k'$ following Definition 8 item 3.(c). By Definition 7 this amounts to showing that for all $N \in \mathbb{N}$, $\|k_n\|^N \le \|k'_n\|^N$. Choose an arbitrary $N \in \mathbb{N}$. By Definition 6, $\|k_n\|^N \le \|k'_n\|^N$ amounts to proving $\lim(\|(\|s_n\|^N)_{n \in \mathbb{N}}\|) \le \lim(\|(\|s'_n\|^N)_{n \in \mathbb{N}}\|)$. Thanks to the hypothesis for all $n \in \mathbb{N}$, $s_n \le s'_n$, by using Assumption 1 item 2.(b) we obtain that for all $n \in \mathbb{N}$, $\|s_n\|^N \le \|s'_n\|^N$. Lemma 1 then establishes what was left to prove: $\lim(\|(\|s_n\|^N)_{n \in \mathbb{N}}\|) \le \lim(\|(\|s'_n\|^N)_{n \in \mathbb{N}}\|)$.

**Lemma 24** Consider two ascending sequences $(s_n)_{n \in \mathbb{N}}$ and $(s'_n)_{n \in \mathbb{N}}$ in $(C^\circ)^\omega$, and $N \in \mathbb{N}$ such that $[(s_n)_{n \in \mathbb{N}}] \sim [(s'_n)_{n \in \mathbb{N}}] \sim$ and for all $n \in \mathbb{N}$, $\delta s_n < N \le \delta s'_n$. Then $[(s_n)_{n \in \mathbb{N}}] \sim < [(s'_n)_{n \in \mathbb{N}}] \sim$.

*Proof.* Let $k = [(s_n)_{n \in \mathbb{N}}] \sim$ and $k' = [(s'_n)_{n \in \mathbb{N}}] \sim$. We have the hypothesis $k \le k'$, i.e., $k \le k'$ following Definition 8 item 3.(c), and have to show $k < k'$. For, assuming the contrary, $k = k'$, i.e., for all $M \in \mathbb{N}$, $\|k_n\|^M = \|k'_n\|^M$, and in particular $\|k_n\|^N = \|k'_n\|^N$. By Definition 6, the latter amounts to proving $\lim(\|(\|s_n\|^N)_{n \in \mathbb{N}}\|) = \lim(\|(\|s'_n\|^N)_{n \in \mathbb{N}}\|)$, which implies that for some sufficiently large $n \ge N$, $\|s_n\|^N = \|s'_n\|^N$. But by hypothesis, $\delta s_n < N$, hence, by the monotonicity of $\delta$ in Assumption 2, $\delta (\|s_n\|^N) < N$. Also by hypothesis, $\delta s'_n \ge N$, hence, by Assumption 2 item 3, $\delta (\|s'_n\|^M) = N$, leading to a contradiction. The origin of the contradiction is the assumption $k = k'$, hence, $k < k'$, which proves the lemma.

**Lemma 25** For all $k \in K$, $k$ is totally defined if and only if $k$ is maximal w.r.t. $\le$.
**Proof.** (⇒): Let $k' \in K$ such that $k \le k'$. From $\delta k = \infty$ and Lemma 20 it follows that $\delta k' = \infty$, and from Lemma 22 if follows that for all $m \in \mathbb{N}$, $\|k\|^m = \|k'\|^m$. By Definition 7, $k' \le k$, i.e., $k' \le k$ according to Definition 8 item 3.(c). Hence, $k$ is maximal w.r.t. $\le$.

(⇔): We show the contrapositive of this implication: assuming $\delta k \in \mathbb{N}$, we show that $k$ is not maximal. From $\delta k \in \mathbb{N}$, by Definition 10, $M := \max [\delta(\|k\|^m)_{m \in \mathbb{N}}] \in \mathbb{N}$, thus, for all $m \in \mathbb{N}$, $\delta(\|k\|^m) \le M$.

Consider now Assumption 2 item 5 where $(s_m)_{m \in \mathbb{N}} := (\|k\|^m)_{m \in \mathbb{N}}$ is an ascending sequence. We obtain $i \in \mathbb{N}$ and an increasing sequence $(s'_j)_{j \ge i}$ such that for all $j \ge i$, $\|k\|^j \le \alpha s'_j$ and $N < \delta s'_j$. For all $j < i$ we let $s'_j := (\|k\|^j)$. Hence, for all $j \in [\|k\|^j \le \alpha s'_j]$, Next, by Lemma 23, the increasing sequence $(s'_m)_{m \in \mathbb{N}}$ is ascending, and $k \le \lim(\|(s'_m)_{m \in \mathbb{N}}\|)$. Finally, by Lemma 24 instantiated with $N := M+1$, $k < \lim(\|(s'_m)_{m \in \mathbb{N}}\|)$. Hence, $k$ is not maximal; which concludes the proof of the contrapositive of $(⇔)$ and of the lemma.

## 4.2 Sufficient Conditions for Productiveness

We now use the results in the previous sections in order to give practical sufficient conditions for the productiveness of functionals and, by way of consequence, for defining total corecursive functions as unique fixpoints of the functionals in question. In this section we globally assume two partial orders with least elements ($D^\circ, \le_D^\circ, \perp_D$) and ($C^\circ, \le_C^\circ, \perp_C$). Let ($D, \le_D, \perp_D$) and ($C, \le_C, \perp_C$) be the respective $\omega$CPOs built by completion, with $K_D$ and $K_C$ the respective sets of equivalence classes, $\|\|_D$ and $\|\|_C$ their approximation functions, and $\delta_D, \delta_C$ their definedness functions.

**Notation.** $\tilde{D}$ denotes the set of maximal elements of $D$. A function $f^\circ : D^\circ \to C^\circ$ is strictly monotonic if for all $x, y \in D$, $x <_D^\circ y$ implies $f^\circ x <_C^\circ f^\circ y$. Note that a strictly monotonic function is also monotonic : $x \le_D^\circ y$ implies $f^\circ x \le_C^\circ f^\circ y$. The function $f^\circ$ preserves definedness if for all $x \in D$, $\delta_C(f^\circ x) \ge \delta_D x$.

**Lemma 26** Assume $f^\circ : D^\circ \to C^\circ$ is strictly monotonic and definedness preserving, and the functional $F : (\tilde{D} \to C) \to \tilde{D} \to C$ is monotonic and $\forall n \in \mathbb{N}, \forall x \in \tilde{D}, F^n \perp x = f^\circ(\|x\|_D^n)$. Then $F$ is productive.

**Proof.** Since $F$ is monotonic, there remains to show the rest of the productiveness requirement: for all $x \in \tilde{D}$, $\lim(\|(F^n \perp x)_{n \in \mathbb{N}}\|)$ is maximal in $C$. Thanks to the hypothesis $\forall n \in \mathbb{N}, \forall x \in \tilde{D}, (F^n \perp x) = f^\circ(\|x\|_D^n)$, what we have to show is that for all $x \in \tilde{D}$, $\lim(\|(f^\circ(\|x\|_D^n))_{n \in \mathbb{N}}\|)$ is maximal in $C$. There are two cases:

* if $x \in D^\circ \cap \tilde{D}$ then $(\|x\|_D^n)_{n \in \mathbb{N}}$ is increasing and stabilizes at its limit $x$. By monotonocity of $f^\circ$, $(f^\circ(\|x\|_D^n))_{n \in \mathbb{N}}$ is also increasing and stabilizes at its limit $f^\circ x$. Since $x$ is maximal, by Lemma 19 $\delta_D x = \infty$ and by hypothesis, $\delta_C (f^\circ x) \ge \delta_D x = \infty$, hence, again by Lemma 19, $f^\circ x$ is maximal in $C$ and since $f^\circ x = \lim(\|(f^\circ(\|x\|_D^n))_{n \in \mathbb{N}}\|)$ we obtain the maximality of $\lim(\|(f^\circ(\|x\|_D^n))_{n \in \mathbb{N}}\|)$;

* $x \in K_D \cap \tilde{D}$: by Lemma 13, $(\|x\|_D^n)_{n \in \mathbb{N}}$ is ascending and its limit is $x$. Now, none of the elements in the sequence is maximal, otherwise the sequence would by stabilizing; hence, by Lemma 25, for all $n \in \mathbb{N}$, $\delta_D (\|x\|_D^n) < \infty$. By (strict) monotonocity of $f^\circ$, $(f^\circ(\|x\|_D^n))_{n \in \mathbb{N}}$ is also ascending. Since $x$ is maximal, by Lemma 13 $\delta_D x = \infty$, which, by Definition 10, means $\lim(\|(\delta_D (\|x\|_D^n))_{n \in \mathbb{N}}\|) = \infty$. Again, none of the elements in the sequence $(f^\circ(\|x\|_D^n))_{n \in \mathbb{N}}$ is maximal, otherwise the sequence would by stabilizing, Hence, by Lemma 25, for all $n \in \mathbb{N}$, $\delta_C (f^\circ(\|x\|_D^n)) < \infty$. By hypothesis, $\delta_C (f^\circ(\|x\|_D^n)) \ge \delta_D \|x\|_D^n$ and therefore $\delta_C(\lim(\|(f^\circ(\|x\|_D^n))_{n \in \mathbb{N}}\|)) \ge \delta_D(\lim(\|(\|x\|_D^n)_{n \in \mathbb{N}}\|)) = \delta_D x = \infty$, which, using Lemma 13, implies that $\lim(\|(f^\circ(\|x\|_D^n))_{n \in \mathbb{N}}\|)$ is maximal in $C$. The proof is done.

Lemma 26 is used in conjunction with Theorem 1 for defining total corecursive functions as unique fixpoints of their functionals. We next illustrate how everything comes together on Rose trees.
# 5 Rose Trees as an $\omega$CPO and the *mirror* function as a unique fixpoint

In this section we define Rose trees using the finite trees in Example 1 and the $\omega$CPO construction in Section 3. We also define the *mirror* function, a total corecursive function between Rose trees, as a unique fixpoint of its functional, proved to be productive using the techniques shown in Section 4.

Remember from Example 1 that finite trees $C^\circ$ have constructors $\perp$ and $\mathit{tree}^\circ l$ for finite lists $l$ of finite trees. The prefix order $\leq^\circ$ is such that for all $t \in C^\circ$, $\perp \leq^\circ t$, and for all lists $l, l'$ of trees having the same length $m$, $\mathit{tree}^\circ l \leq^\circ \mathit{tree}^\circ l'$ if and only if for all $i < m$, $l[i] \leq^\circ l'[i]$. The $\mathit{forest}^\circ$ accessor is defined from non-$\perp$ trees - i.e., trees of the form $\mathit{tree}^\circ l$ for $l$ a list of finite trees, by $\mathit{forest}^\circ(\mathit{tree}^\circ l) = l$.

We have seen in the previous sections that, together with their approximations $\llcorner \rrcorner$) and definedness function $\delta$, finite trees satisfy Assumptions 1 and 2 therefore constitute an $\omega$CPO ($C^\circ \cup K, \leq, \perp$) where $K$ is the set of equivalence classes of ascending sequences of finite trees, some of which are maximal - or, equivalently, totally defined. Ascending sequences require trees having at least one branch that grows “forever”, and their limits (in $K$) have at least one infinite branch. Overall, the set $K$ together with the set $C^\circ$ of finite trees constitute the set $C^\circ \cup K$ of Rose trees, of finite breadth and possibly infinite depth.

## 5.1 Extending the $\mathit{tree}^\circ$ Constructor and $\mathit{forest}^\circ$ Accessor from Finite Trees to Rose Trees

The $\omega$CPO of Rose trees is not yet fully functional (for the purpose of defining total corecursive func- tions) until we extend the $\mathit{tree}^\circ$ constructor and $\mathit{forest}^\circ$ accessor from finite trees to Rose trees. Indeed, functionals for corecursive functions under definition use the extended constructors and accessors. Such is the functional $\mathit{Mirror} = \lambda f.\lambda t.\mathit{tree} (\mathit{map} f (\mathit{reverse} (\mathit{forest} t)))$ for the *mirror* function that shall we define.

We first extend the notion of diagonal, defined for equivalence classes in $K$ (Def. 9), to $C^\circ \cup K$.

**Definition 11** For all $c \in C^\circ \cup K$, we define the *diagonal* of $c$ to be the sequence $(\llcorner c \rrcorner^n)_{n \in \mathbb{N}}$.

**Lemma 27** For all $c \in C^\circ \cup K$, the *diagonal* of $c$ is an increasing sequence and its limit is $c$.

*Proof.* For $c \in K$ we the result follows from Lemma 13. For $c \in C^\circ$, the sequence is increasing due to Assumption 1 item 2.(c). By Lemma 2, for large enough $n \in \mathbb{N}$, $\llcorner c \rrcorner^n = c$, meaning that $(\llcorner c \rrcorner^n)_{n \in \mathbb{N}}$ is increasing and stabilizes at $c$, hence its limit is $c$.

Consider a list $l = [t_0, \dots, t_{m-1}]$ of elements in $C = C^\circ \cup K$. By Lemma 27, each $t_i$ is the limit of its diagonal: $t_i = \lim(\llcorner(t_i) \rrcorner^n)_{n \in \mathbb{N}})$. Let us consider the sequence of lists $(\llcorner t_0 \rrcorner^n, \dots, \llcorner t_{m-1} \rrcorner^n])_{n \in \mathbb{N}}$. This sequence is pointwise increasing: for all $n \in \mathbb{N}$ and $i < m$, $\llcorner t_i \rrcorner^n \le \llcorner t_i \rrcorner^{n+1}$. Thanks to the monotonicity of the $\leq^\circ$ order, the sequence $(\mathit{tree}^\circ[\llcorner t_0 \rrcorner^n, \dots, \llcorner t_{m-1} \rrcorner^n]))_{n \in \mathbb{N}}$ is increasing as well. This justifies the following definition:

**Definition 12** $\mathit{tree} [t_0, \dots, t_{m-1}] \triangleq \lim(\llcorner(\mathit{tree}^\circ[\llcorner t_0 \rrcorner^n, \dots, \llcorner t_{m-1} \rrcorner^n]))_{n \in \mathbb{N}})$.

We now give equivalent conditions under which $\mathit{tree} [t_0, \dots, t_{m-1}] \in C^\circ$ and $\mathit{tree} [t_0, \dots, t_{m-1}] \in K$.

**Lemma 28** $\mathit{tree} [t_0, \dots, t_{m-1}] \in C^\circ$ if and only if for all $i < m$, $t_i \in C^\circ$. If this is the case then $\mathit{tree} [t_0, \dots, t_{m-1}] = \mathit{tree}^\circ [t_0, \dots, t_{m-1}]$.

*Proof.*

(⇒): if $\mathit{tree} [t_0, \dots, t_{m-1}] \in C^\circ$ then the increasing sequence $(\mathit{tree}^\circ[\llcorner t_0 \rrcorner^n, \dots, \llcorner t_{m-1} \rrcorner^n])_{n \in \mathbb{N}}$ cannot be ascending; otherwise, its limit (and in particular upper bound) $\lim(\llcorner(\mathit{tree}^\circ[\llcorner t_0 \rrcorner^n, \dots, \llcorner t_{m-1} \rrcorner^n])_{n \in \mathbb{N}})$, which by Definition 12 satisfies $\lim(\llcorner(\mathit{tree}^\circ[\llcorner t_0 \rrcorner^n, \dots, \llcorner t_{m-1} \rrcorner^n])_{n \in \mathbb{N}}) = \mathit{tree} [t_0, \dots, t_{m-1}]$, is in $C^\circ$, and this contradicts Assumption 1 item 1. Hence, the sequence $(\mathit{tree}^\circ[\llcorner t_0 \rrcorner^n, \dots, \llcorner t_{m-1} \rrcorner^n])_{n \in \mathbb{N}}$ is stabilizing.
This implies that for all $i < m$, the increasing sequence $(\lceil t_i \rceil^n)_{n \in \mathbb{N}}$ is stabilizing (the contrary would imply that $(\text{tree}^o[\lceil t_0 \rceil^n, \dots, \lceil t_{m-1} \rceil^n])_{n \in \mathbb{N}}$ is non-stabilizing as well). The value at which $(\lceil t_i \rceil^n)_{n \in \mathbb{N}}$ is stabilizing is its limit $t_i$, hence, the latter is in $C^o$. This implies that $(\text{tree}^o[\lceil t_0 \rceil^n, \dots, \lceil t_m - 1 \rceil^n])_{n \in \mathbb{N}}$ stabilizes at $\text{tree}^o[t_0, \dots, t_{m-1}]$, meaning that $\lim(\langle(\text{tree}^o[\lceil t_0 \rceil^n, \dots, \lceil t_{m-1} \rceil^n])\rangle_{n \in \mathbb{N}}) = \text{tree}^o[t_0, \dots, t_{m-1}]$ and using Definition 12, $\text{tree}^o[t_0, \dots, t_{m-1}] = \text{tree}[t_0, \dots, t_{m-1}]$.

(=$\Leftarrow$): if for all $i < m$, $t_i \in C^o$, then for all $i < m$, $(\lceil t_i \rceil^n)_{n \in \mathbb{N}}$ is stabilizing at its limit $t_i$. It follows that $(\text{tree}^o[\lceil t_0 \rceil^n, \dots, \lceil t_{m-1} \rceil^n])_{n \in \mathbb{N}}$ is stabilizing and its limit equals $\text{tree}^o[t_0, \dots, t_{m-1}] \in C^o$. On the other hand, by Definition 12, $\lim(\langle(\text{tree}^o[\lceil t_0 \rceil^n, \dots, \lceil t_{m-1} \rceil^n])\rangle_{n \in \mathbb{N}}) = \text{tree}[t_0, \dots, t_{m-1}]$. It follows that $\text{tree}[t_0, \dots, t_{m-1}] \in C^o$ and $\text{tree}[t_0, \dots, t_{m-1}] = \text{tree}^o[t_0, \dots, t_{m-1}]$.

**Lemma 29** *tree* [*t*₀,...,*t*<sub>*m*−1</sub>] ∈ *K* if and only if there exists *i* < *m* such that *t*ᵢ ∈ *K*. If this is the case then

$$ \text{tree}[t_0, \dots, t_{m-1}] = [(\text{tree}^o[\lceil t_0 \rceil^n, \dots, \lceil t_{m-1} \rceil^n])_{n \in \mathbb{N}}] \sim $$

*Proof.* tree [*t*₀,...,*t*<sub>*m*−1</sub>] ∈ *K* is equivalent to tree [*t*₀,...,*t*<sub>*m*−1</sub>] ∉ C°, which by Lemma 28 is equivalent to the existence of some *i* < *m* such that *t*ᵢ ∈ *K*. The statement tree [*t*₀,...,*t*<sub>*m*−1</sub>] = [(tree°[∫∫*t*₀∫∫ⁿ, ∫∫*t*<sub>*m*−1</sub>∫∫ⁿ])ₙ∈N]~ follows from Definition 12 and Definition 8 item 2 of limits of ascending sequences over C°.

The next result holds in general (i.e., not only for sequences of trees) but was not needed until now.

**Lemma 30** For any increasing sequence $(s_n)_{n \in \mathbb{N}} \in (C^o)^\omega$, $\lceil \lim(\langle(s_n)_{n \in \mathbb{N}}\rangle) \rceil^N = \lim(\langle(\lceil s_n \rceil^N)_{n \in \mathbb{N}}\rangle)$.

*Proof.* If the sequence is ascending then the lemma follows from Definition 6 and Definition 8 item 2. If the sequence is stabilizing to some $c \in C^o$ then $\lceil \lim(\langle(s_n)_{n \in \mathbb{N}}\rangle) \rceil^N = \lceil c \rceil^N = \lim(\langle(\lceil s_n \rceil^N)_{n \in \mathbb{N}}\rangle)$.

The following lemma states that the function tree from Definition 12 is continuous in the sense of Scott:

**Lemma 31** For all $m \in \mathbb{N}$, if for all $i < m$, the sequences $(s_n^i)_{n \in \mathbb{N}}$ are increasing, then it holds that
$$ \lim(\langle(\text{tree}^o[s_n^0, \dots, s_n^{m-1}]\rangle)_{n \in \mathbb{N}}) = \text{tree}[(\lim(\langle(s_n^0)_{n \in \mathbb{N}}\rangle), \dots, (\lim(\langle(s_n^{m-1})_{n \in \mathbb{N}}\rangle))]. $$

*Proof.* We first note that $\lim(\langle(\text{tree}^o[s_n^0, \dots, s_n^{m-1}]\rangle)_{n \in \mathbb{N}})$ exists due to monotonicity of the tree° constructor. We first prove the lemma for the stabilizing case - all sequences $(s_n^i)_{n \in \mathbb{N}}$ stabilize. They stabilize to their limits $\lim(\langle(s_n^i)_{n \in \mathbb{N}}\rangle)$, thus, $(\text{tree}^o[s_n^0, \dots, s_n^{m-1}]_{n \in \mathbb{N}})$ stabilizes to $\text{tree}^o[(\lim(\langle(s_n^0)_{n \in \mathbb{N}}\rangle), \dots, (\lim(\langle(s_n^{m-1})_{n \in \mathbb{N}}\rangle))]$ which by Lemma 28 equals $\text{tree}[(\lim(\langle(s_n^0)_{n \in \mathbb{N}}\rangle), \dots, (\lim(\langle(s_n^{m-1})_{n \in \mathbb{N}}\rangle))];$ which proves the stabilizing case.

We now focus on the general case. Let $t^i = \lim(\langle(s_n^i)_{n \in \mathbb{N}}\rangle)$ for $i < m$. By Def. 12, $\text{tree}[t^0, \dots, t^{m-1}] = \lim(\langle(\text{tree}^o[\lceil t^0 \rceil^n, \dots, \lceil t^{m-1} \rceil^n])\rangle_{n \in \mathbb{N}})$. But using Lemma 30, for all $i < m$ and $n \in \mathbb{N}$, $\lceil t^i \rceil^n \triangleq \lceil \lim(\langle(s_j^i)_{j \in \mathbb{N}}\rangle) \rceil^n = \lim(\langle(\lceil s_j^i \rceil^n)_{j \in \mathbb{N}}\rangle)$, thus, $\text{tree}^o[\lceil t^0 \rceil^n, \dots, \lceil t^{m-1} \rceil^n] = \text{tree}^o[(\lim(\langle(\lceil s_j^0 \rceil^n)_{j \in \mathbb{N}}\rangle), \dots, (\lim(\langle(\lceil s_j^{m-1} \rceil^n)_{j \in \mathbb{N}}\rangle))]$ for all $n \in \mathbb{N}$. Hence, ($\dagger$): $\text{tree}[t^0, \dots, t^{m-1}] = \lim(\langle(\text{tree}^o[(\lim(\langle(\lceil s_j^0 \rceil^n)_{j \in \mathbb{N}}\rangle), \dots, (\lim(\langle(\lceil s_j^{m-1} \rceil^n)_{j \in \mathbb{N}}\rangle))\rangle)_{n \in \mathbb{N}})$.

In the right-hand side of the ($\dagger$) equality, all sequences $(\lceil s_j^0 \rceil^n)_{j \in \mathbb{N}}, \dots, (\lceil s_j^{m-1} \rceil^n)_{j \in \mathbb{N}}$ stabilize. Using the stabilizing case established above we obtain $\text{tree}^o[(\lim(\langle(\lceil s_j^0 \rceil^n)_{j \in \mathbb{N}}\rangle), \dots, (\lim(\langle(\lceil s_j^{m-1} \rceil^n)_{j \in \mathbb{N}}\rangle))] = \lim(\langle(\text{tree}^o[(\lceil s_j^0 \rceil^n), \dots, (\lceil s_j^{m-1} \rceil^n)]\rangle)_{j \in \mathbb{N}})$, for all $n \in \mathbb{N}$. By rewriting the latter equality in ($\dagger$) we obtain ($\ddagger$): $\text{tree}[t^0, \dots, t^{m-1}] = \lim(\langle(\lim(\langle(\text{tree}^o[(\lceil s_j^0 \rceil^n), \dots, (\lceil s_j^{m-1} \rceil^n)]\rangle)_{j \in \mathbb{N}})\rangle)_{n \in \mathbb{N}})$. Using properties of the $\lceil \cdot \rceil$ function, for all $n, j \in \mathbb{N}$, $\text{tree}^o[(\lceil s_j^0 \rceil^n), \dots, (\lceil s_j^{m-1} \rceil^n)] = \lceil \text{tree}^o[s_j^0, \dots, s_j^{m-1}] \rceil^{n+1}$. Rewriting this equality in ($\ddagger$) gives ($\#$): $\text{tree}[t^0, \dots, t^{m-1}] = \lim(\langle(\lim(\langle(\text{tree}^o[s_j^0, \dots, s_j^{m-1}]\rangle^{n+1})_{j \in \mathbb{N}})\rangle)_{n \in \mathbb{N}})$. But the sequence $(\lceil \lim(\langle(\text{tree}^o[s_j^0, \dots, s_j^{m-1}]\rangle)\rangle)_{j \in \mathbb{N}} \rceil^{n+1})_{n \in \mathbb{N}}$ is just $(\lceil \lim(\langle(\text{tree}^o[s_j^0, \dots, s_j^{m-1}]\rangle)\rangle)_{j \in \mathbb{N}} \rceil^n)_{n \in \mathbb{N}}$ without its first element, hence, $\lim(\langle(\lceil \lim(\langle(\text{tree}^o[s_j^0, \dots, s_j^{m-1}]\rangle)\rangle)_{j \in \mathbb{N}} \rceil^{n+1})\rangle)_{n \in \mathbb{N}} = \lim(\langle(\lceil \lim(\langle(\text{tree}^o[s_j^0, \dots, s_j^{m-1}]\rangle)\rangle)_{j \in \mathbb{N}} \rceil^n)\rangle)_{n \in \mathbb{N}}$, which together ($\#$) gives by transitivity (b): $\text{tree}[t^0, \dots, t^{m-1}] = \lim(\langle(\lim(\langle(\text{tree}^o[s_j^0, \dots, s_j^{m-1}]\rangle^n)_{j \in \mathbb{N}})\rangle)_{n \in \mathbb{N}})$. Using Lemma 30, $\lim(\langle(\lceil \lim(\langle(\text{tree}^o[s_j^0, \dots, s_j^{m-1}]\rangle^n)\rangle)_{j \in \mathbb{N}} \rceil^n)\rangle)_{j \in \mathbb{N}} = \lceil \lim(\langle(\text{tree}^o[s_j^0, \dots, s_j^{m-1}]\rangle)\rangle)_{j \in \mathbb{N}} \rceil^n$ for all $n \in \mathbb{N}$. By rewriting the latter equality in (b) we get ($\#$): $\text{tree}[t^0, \dots, t^{m-1}] = \lim(\langle(\lceil \lim(\langle(\text{tree}^o[s_j^0, \dots, s_j^{m-1}]\rangle)\rangle)_{j \in \mathbb{N}} \rceil^n)\rangle)_{n \in \mathbb{N}}$.
By Lemma 27, $\lim(\|\lim((tree^o[s_j^0, \dots, s_j^{m-1}])\|)_{j \in \mathbb{N}}^N)_{n \in \mathbb{N}} = \lim((tree^o[s_0^0, \dots, s_j^{m-1}])\|)_{j \in \mathbb{N}}$, and by transitivity: (●): $tree[t^0, \dots, t^{m-1}] = \lim((tree^o[s_j^0, \dots, s_j^{m-1}])\|)_{j \in \mathbb{N}}$. Finally, $tree[\lim\|(s_n^0)_{n \in \mathbb{N}}\|, \dots, \lim\|(s_n^{m-1})_{n \in \mathbb{N}}\|]$, which is by definition $tree[t^0, \dots, t^{m-1}]$, was proved by (●) equal to $\lim((tree^o[s_j^0, \dots, s_j^{m-1}])\|)_{j \in \mathbb{N}}$: qed.

There remains to prove that *tree* satisfies the following properties of its restriction to finite trees:

* approximations: $\llcorner tree l \rrcorner^0 = \perp$ and $\llcorner tree l \rrcorner^{N+1} = tree(map(\llcorner \cdot \rrcorner^N)) l$;

* monotonicity: $tree l \le tree l'$ iff for some $m \in \mathbb{N}$, $length l = length l' = m$ and for all $i < m$, $l[i] \le l'[i]$;

* surjectiveness for infinite trees: for all $k \in K$ there exists $l$ such that $k = tree l$;

* injectiveness: for all lists of Rose trees $l, l'$, $tree l = tree l'$ implies $l = l'$.

In particular, the last two properties will enable us to define the forest accessor for nonempty trees.

**Lemma 32** For any list $l$ over $C^\circ \cup K$, $\llcorner tree l \rrcorner^0 = \perp$ and for all $N \in \mathbb{N}$, $\llcorner tree l \rrcorner^{N+1} = tree((map(\llcorner \cdot \rrcorner^N)) l)$.

*Proof.* If all elements of $l$ are in $C^\circ$ then the statements follows from the definition of $\llcorner \cdot \rrcorner$ for finite trees. Assume now there is at least one element of $l$ which is in $K$, and let $l = [t_0, \dots, t_{m-1}]$. Then, $tree[t_0, \dots, t_{m-1}] \in K$ by Lemma 29, and by Def 12, $tree[t_0, \dots, t_{m-1}] = \lim(\|tree^o[\llcorner t_0 \rrcorner^N, \dots, \llcorner t_{m-1} \rrcorner^N]\|)_{n \in \mathbb{N}}$. Then, by Lemma 30, for all $M \in \mathbb{N}$, ($\dagger$): $\llcorner tree [t_0, \dots, t_{m-1}] \rrcorner^M = \lim(\|\llcorner tree^o[\llcorner t_0 \rrcorner^N, \dots, \llcorner t_{m-1} \rrcorner^N]\|)_{n \in \mathbb{N}}$.

* if $M = 0$ then ($\dagger$) reduces to $\llcorner tree l \rrcorner^0$ being the limit of a sequence of $\perp$, which proves the first part of the lemma: $\llcorner tree l \rrcorner^0 = \perp$;

* if $M > 0$, i.e., $M = N + 1$, the right-hand side of ($\dagger$) becomes (by definition of $\llcorner \cdot \rrcorner$ for finite trees) $\lim(\|\|tree^o[\llcorner t_0^N \rrcorner^N, \dots, \llcorner t_{m-1}^N \rrcorner^N]\|)\|)_{n \in \mathbb{N}})\|)$. For $n \ge N$, by Assumption 1 item 5 it holds that for all $i < m$, $\llcorner \llcorner t_i \rrcorner^N \rrcorner^N = \llcorner t_i \rrcorner^N$. Hence, the increasing sequence $(tree^o[\llcorner t_0 \rrcorner^N, \dots, \llcorner t_{m-1} \rrcorner^N]\|)_{n \in \mathbb{N}}$ stabilizes to $tree^o[\llcorner t_0 \rrcorner^N, \dots, \llcorner t_{m-1} \rrcorner^N]$. Since for all $i < m$, $\llcorner t_i \rrcorner^N \in C^\circ$ we have, by Lemma 28, $tree^o[\llcorner t_0 \rrcorner^N, \dots, \llcorner t_{m-1} \rrcorner^N] = tree[\llcorner t_0 \rrcorner^N, \dots, \llcorner t_{m-1} \rrcorner^N]$. Remembering that $l = [t_0, \dots, t_{m-1}]$ and $M = N + 1$, ($\dagger$) proves the second statement of the lemma: $\llcorner tree l \rrcorner^{N+1} = tree((map(\llcorner \cdot \rrcorner^N)) l)$.

**Lemma 33** $tree l \le tree l'$ iff for some $m \in \mathbb{N}$, $length l = length l' = m$ and for all $i = 1, \dots, m$, $l[i] \le l'[i]$.

*Proof.*

($\Rightarrow$): if both $l$ and $l'$ consist of finite trees then the statement follows from the definition of $\leq^\circ$. Otherwise, $tree l \le tree l'$ holds in two possible cases:

* $tree l \in C^\circ$ and $tree l' \in K$. Let $m = length l$. Using Lemma 28, for all $i < m$, $l[i] \in C^\circ$ and $tree l = tree^o l$. By Definition 8 item 3.(b), $tree^o l \le tree l$ implies there exists $M \in \mathbb{N}$ such that $tree^o l \le \llcorner tree l \rrcorner^M$. Now, $M = 0$ is impossible since, by Lemma 32, this would imply the impossible inequality $tree^o l \le \perp$. Hence, $M = N + 1$ and then, using Lemma 32, we obtain $tree^o l \le tree(map(\llcorner \cdot \rrcorner^M)l')$. Now, all the elements of $map(\llcorner \cdot \rrcorner^M)l'$ are finite trees, thus, using Lemma 28, we obtain $tree^o l \le tree^o(map(\llcorner \cdot \rrcorner^N)l')$. Using the properties of the constructor $tree^o$, we obtain $length(map(\llcorner \cdot \rrcorner^M)l') = length l = m$ and then $length l' = m$ using the property that $map$ preserves list length. Moreover, we obtain that for all $i < m$, $l[i] \le \llcorner l'[i] \rrcorner^N$, which, by Definition 8 item 3.(b) (if $l'[i] \in K$) resp. Assumption 1 item 2.(a) (if $l'[i] \in C^\circ$) implies that for all $i < m$, $l[i] \le l'[i]$, which settles this case.

* $tree l \in K$ and $tree l' \in K$. Then, using Definition 8 item 3.(c), for all $N \in \mathbb{N}$, $\llcorner tree l \rrcorner^{N+1} \le \llcorner tree l' \rrcorner^{N+1}$. Fix an arbitrary $N \in \mathbb{N}$. Using Lemma 32, $tree(map(\llcorner \cdot \rrcorner^N)l) \le tree(map(\llcorner \cdot \rrcorner^N)l)$, which, using Lemma 28 and Lemma 8 item 3.(a), becomes $tree^o(map(\llcorner \cdot \rrcorner^N)l) \le \circled{=} tree^o(map(\llcorner \cdot \rrcorner^N)l)$. Next, using properties of the $\leq^\circ$ order, $length(map(\llcorner \cdot \rrcorner^N)l) = length(map(\llcorner \cdot \rrcorner^N)l)$ which implies
length $l = length l'$ and let $m$ denote the common value of the lengths. We obtain that for all $i < m$, $\llcorner l[i] \rrcorner^N \le \llcorner l'[i] \rrcorner^N$, and since $N \in \mathbb{N}$ has been chosen arbitrarily, by Definition 8 item 3.(b) (if $l'[i] \in K$) resp. Lemma 2 (if $l'[i] \in C^\circ$) using Definition 8 item 3.(c), implies that for all $i < m$ it holds that $l[i] \le l'[i]$, which settles this case as well.

(=$\Leftarrow$): again, if both $l$ and $l'$ consist of finite trees then the statement follows from the definition of $\leq^\circ$. The case where $l$ contains an element of $K$, say, at position $i$, why $l'$ contains only elements of $C^\circ$ is impossible, since (by Definition 8 item 3), $l[i] \in K$ cannot be in $\leq$ order with $l'[i] \in C^\circ$. The two remaining cases are:

* $l$ only consists of elements in $C^\circ$ and $l'$ contains at least one element in $K$: let $0 \le i_1, i_2, \dots, i_n < m$ be the positions where $l'[i_j] \in K$ for $j = 1, \dots, n$. For any such index $i_j$ there is $N_j$ such that $l[i_j] \le \llcorner l'[i_j] \rrcorner^{N_j}$. Let $N'$ be the maximum of $\{N_j | j = 1, \dots, n\}$. For the positions in the list other than $i_1, i_2, \dots, i_n$, the elements at those positions are in $C^\circ$. Using Lemma 2, there exists $N''$ such that for all $i_p \in \{0, \dots, m-1\} \setminus \{i_1, \dots, i_n\}$, $\llcorner l'[i_p] \rrcorner^{N''} = l'[i_p]$. Take now $N = \max N' N''$. Then, using Assumption 1 item 2.(c), Lemma 2 and the hypothesis of the implication, we obtain (†): for all $i < m$, $l[i] \le \llcorner l'[i] \rrcorner^N$. Next, since $l$ contains only elements in $C^\circ$, by Lemma 28, tree $l = \text{tree}^\circ l \in C^\circ$. We now show (‡): $\text{tree}^\circ l \le \llcorner \text{tree}^\circ l' \rrcorner^{N+1}$, which by Definition 8 item 3.(b) implies the desired conclusion $\text{tree}^\circ l \le \text{tree}^\circ l'$. Now, (‡) amounts to $\text{tree}^\circ l \le \llcorner \text{tree}(\llcorner \cdot \rrcorner^N) l' \rrcorner^{N+1}$, which (since $\text{length}^\circ l = \text{length}^\circ l'$ implies $\text{length}^\circ l = \text{length}(\text{map}(\llcorner \cdot \rrcorner^N)l'))$ reduces to (†): this case is proved.

* both $l$ and $l'$ contain at least one element of $K$. Then, by Lemma 29, $\text{tree}^\circ l \in K$ and $\text{tree}^\circ l' \in K$. In order to prove $\text{tree}^\circ l \le \text{tree}^\circ l'$, by Definition 8 item 3.(b), we need to prove $\text{tree}^\circ l \le \text{tree}^\circ l'$, which by Lemma 8 amounts to proving (†): for all $M \in \mathbb{N}$ there exists $M' \in \mathbb{N}$ such that $\llcorner (\text{tree}^\circ l) \rrcorner^M \le \llcorner (\text{tree}^\circ l') \rrcorner^M$. For $M=0$ any $M' \in \mathbb{N}$ will do. Now consider an arbitrary $M > 0$, i.e., $M = N+1$. Using Lemma 32 and the properties of $\leq^\circ$, (†) reduces to proving (‡): for all $N \in \mathbb{N}$ and $i < m$, there exists $N' \in \mathbb{N}$ such that $\llcorner l[i] \rrcorner^N \le \llcorner l'[i] \rrcorner^{N'}$. Let $0 \le i_1, i_2, \dots, i_n < m$ the positions at which $l'[i_j] \in K$ for $j = 1, \dots, n$. For any such index $i_j$ there is $N_j$ such that $l[i_j] \le \llcorner l'[i_j] \rrcorner^{N_j}$. We choose $N \in \mathbb{N}$ and let $N'$ be the maximum of $\{N\} \cup \{N_j | j = 1, \dots, n\}$. We show (‡) for the arbitrary $N, i$ and chosen $N'$:

- if $l[i] \in C^\circ$ and $l'[i] \in C^\circ$, $\llcorner l[i] \rrcorner^N \le \llcorner l'[i] \rrcorner^{N'}$ results from $l[i] \le \llcorner l'[i] \rrcorner^{\circ}$ (obtained from the hypothesis $l[i] \le \llcorner l'[i] \rrcorner^{\circ}$ and Definition 8 item 3.(a)), $N \le N'$, and Assumption 1 items 2.(b), 2.(c);

- if $l[i] \in C^\circ$ and $l[i] \in K$, we have $\llcorner l[i] \rrcorner^N \le \llcorner l[i] \rrcorner^\circ$ by Assumption 1 item 2.(a), hence, by Definition 8 item 3.(a), $\llcorner l[i] \rrcorner^N \le l[i]$. Moreover, $l[i] \le \llcorner l'[i] \rrcorner^{N'}$, from the definition of $N'$ and Assumption 1 item 2.(c), and then $l[i] \le \llcorner l'[i] \rrcorner^{N'}$ by Definition 8 item 3.(a). By transitivity, we obtain the desired $\llcorner l[i] \rrcorner^N \le \llcorner l'[i] \rrcorner^{N'}$;

- if $l[i] \in K$ and $l[i] \in K$, $\llcorner l[i] \rrcorner^N \le \llcorner l'[i] \rrcorner^{N'}$ results from the hypothesis $l[i] \le l'[i]$, $N \le N'$, and Lemma 11 items 2 and 3. This completes the proof of the current subcase and of the lemma.

**Lemma 34** For all $k \in K$ there exists a list $l$ of Rose trees such that $k = \text{tree}^\circ l$.

*Proof.* Consider the diagonal $(\llcorner k \rrcorner^n)_{n \in \mathbb{N}}$. By Lemma 13 it is an ascending sequence and its limit is $k$. Hence, there exists $M \in \mathbb{N}$ such that for all $j \ge M$, $\llcorner k \rrcorner^j \ne \perp$. We choose $M$ minimal with the above property, hence, and for all $j < M$, $\llcorner k \rrcorner^j = \perp$. Thus, for all $j \ge M$, $\llcorner k \rrcorner^j = \text{tree}^\circ l^j$ for some list $l^j$ of finite trees. Due to the increasing nature of $(\llcorner k \rrcorner^n)_{n \in \mathbb{N}}$, all the lists $l^j$ have the same length, say, $m$. Moreover, $m > 0$, because if $m = 0$ the sentence would be stabilizing. Thus (†): for all $j \ge M$, $\llcorner k \rrcorner^j = \text{tree}^\circ [t_0^j, \dots, t_{m-1}^j]$ with $m > 0$. For any arbitrarily chosen $i < m$, consider the sequence $(t_i^{n+M})_{n \in \mathbb{N}}$. Thanks to properties of $\leq^\circ$ the sequence is increasing, and let $t_i$ be its limit. There remains to prove
that $k = \text{tree } [t_0, \dots, t_{m-1}]$. By Lemma 31, $\text{tree } [t_0, \dots, t_{m-1}] = \lim(\|(\text{tree}^\circ[t_0^{n+M}, \dots, t_{m-1}^{n+M}])_{n \in \mathbb{N}}\|)$. Using $(\dagger)$, $\lim(\|(\text{tree}^\circ[t_0^{n+M}, \dots, t_{m-1}^{n+M}])_{n \in \mathbb{N}}\|) = \lim(\|(\|k\|^{n+M})_{n \in \mathbb{N}}\|)$. But $(\|k\|^{n+M})_{n \in \mathbb{N}}$ is a subsequence of $(\|k\|^n)_{n \in \mathbb{N}}$, hence, using Lemma 12 the latter two sequences are similar and have the same limit $k$. This proves $\text{tree } [t^0, \dots, t^{m-1}] = k$ and the lemma.

**Lemma 35** For all lists of Rose trees $l, l'$, $\text{tree } l = \text{tree } l'$ implies $l = l'$.

*Proof.* $\text{tree } l = \text{tree } l'$ implies $\text{tree } l \le \text{tree } l'$ and $\text{tree } l' \le \text{tree } l$. The former implies $\text{length } l = \text{length } l' = m$ for some $m \in \mathbb{N}$ and for all $i < m$, $l[i] \le l'[i]$. Symmetrically, for all $i < m$, $l'[i] \le l[i]$. It follows that $\text{length } l = \text{length } l' = m$ for some $m \in \mathbb{N}$ and for all $i < m$, $l[i] = l'[i]$, i.e., the equality of the two lists.

We can now define the forest function as an extension of the forest$^\circ$ accessor:

**Definition 13** Given $t \in (C^\circ \setminus \{\perp\}) \cup K$, we define forest $t$ as follows:

* if $t \in C^\circ \setminus \{\perp\}$ then forest $t = \text{forest}^\circ t$;

* if $t \in K$ then we let forest $t = l$, where $l$ is the unique list of trees such that $t = \text{tree } l$. (The existence and uniqueness of $l$ is ensured by Lemmas 34 and 35.)

The tree and forest functions satisfy the expected equations which they inherit from tree$^\circ$ and forest$^\circ$:

**Lemma 36** For all $t \in (C^\circ \setminus \{\perp\}) \cup K$, $\text{tree}(\text{forest } t) = t$, and for all lists $l$ of Rose trees, forest ($\text{tree } l$) = $l$.

*Proof.* We prove the first statement in the lemma. Let $t \in (C^\circ \setminus \{\perp\}) \cup K$. If $t \in (C^\circ \setminus \{\perp\})$ the statement holds due to properties of the tree$^\circ$ constructor and forest$^\circ$ accessor. If $t \in K$ then, by Definition 13, forest $t$ is the unique list of trees $l$ such that $t = \text{tree } l$, i.e., $t = \text{tree}(\text{forest } t)$.

We focus on the second statement. If $l$ is a list of finite trees then by Lemma 28 $\text{tree } l = \text{tree}^\circ l \in C^\circ$ and then forest ($\text{tree } l$) = forest$^\circ(\text{tree}^\circ l)$, and the statement follows from forest$^\circ(\text{tree}^\circ l) = l$. If $l$ contains at least one infinite tree then by Lemma 29, $\text{tree } l \in K$. The statement forest ($\text{tree } l$) = $l$ follows from Definition 13.

We now have all the ingredients for writing functionals involving Rose trees and for defining functions over Rose trees as unique fixpoints of the functionals in question.

# 6 Defining a Total Mirror Function Between Rose Trees

The *mirror* function for totally defined (equivalently, maximal) Rose trees, which we shall define via its fixpoint equation, has the functional defined by $\text{Mirror } f \hat{t} = \text{tree}(\text{map } f (\text{reverse } (\text{forest } \hat{t})))$, for all functions $f: \widetilde{\text{Tree}} \to \text{Tree}$ and $\hat{t}: \widetilde{\text{Tree}}$, where $\widetilde{\text{Tree}}$ denotes maximal elements in the $\omega$CPO of Rose trees. For defining the *mirror* function via the equation $\text{mirror} = \text{Mirror mirror}$ we use Theorem 1, which requires us to prove that the functional *Mirror* is productive. The productiveness is established via Lemma 26. For this, we first prove that $F$ it is monotonic, then inductively define a mirror function for finite trees $t^\circ$, mirror$^\circ t^\circ = \text{if } t^\circ = \perp \text{ then } \perp \text{ else tree}^\circ(\text{map mirror}^\circ(\text{reverse } (\text{forest } t^\circ)))$. Next, we show that mirror$^\circ$ is strictly increasing and preserves definedness, which are routine' proofs by induction on finite trees. Finally we prove the last (and nontrivial) part of the sufficient condition in a separate lemma:

**Lemma 37** For all $n \in \mathbb{N}$ and $\hat{t} \in \widetilde{\text{Tree}}$, $\text{Mirror}^n \perp \hat{t} = \text{mirror}^\circ (\|\hat{t}\|^n)$

*Proof.* By induction on $n$. The base case is trivial as it reduces to $\perp = \perp$. For the inductive step: assume that for all $\hat{t} \in \widetilde{\text{Tree}}$, $\text{Mirror}^n \perp \hat{t} = \text{mirror}^\circ (\|\hat{t}\|^n)$. Fix an arbitrary $\hat{t} \in \widetilde{\text{Tree}}$. We have the equality chain:

$$ \text{Mirror}^{n+1} \perp \hat{t} = (\text{by definition of iteration of a functional}) $$
Mirror(Mirror$^{n}$⊥) $\hat{t}$ = (by induction hypothesis and properties of function composition ○)

Mirror (mirror$^{○}$ ○ (⊤ · ⊤$^{n}$)) $\hat{t}$ = (using $\hat{t}$ = tree (forest $\hat{t}$) that holds by Lemma 36)

Mirror (mirror$^{○}$ ○ (⊤ · ⊤$^{n}$)) (tree (forest $\hat{t}$)) = (by definition of *Mirror*)

tree (map (mirror$^{○}$ ○ (⊤ · ⊤$^{n}$))(reverse(forest $\hat{t}$))) = (by Lemma 28)

tree$^{○}$(map (mirror$^{○}$ ○ (⊤ · ⊤$^{n}$))(reverse(forest $\hat{t}$))) = (by properties of map vs. ○)

tree$^{○}$(map mirror$^{○}$(map(⊤ · ⊤$^{n}$)(reverse(forest $\hat{t}$)))) = (by properties of map vs. reverse)

tree$^{○}$(map mirror$^{○}$(reverse(map(⊤ · ⊤$^{n}$) forest $\hat{t}$))) = (by definition of mirror$^{○}$)

mirror$^{○}$(tree$^{○}$(map(⊤ · ⊤$^{n}$) forest $\hat{t}$)) = (by Lemma 28)

mirror$^{○}$(tree (map(⊤ · ⊤$^{n}$) forest $\hat{t}$)) = (by Lemma 32)

mirror$^{○}$(⊤ tree (forest $\hat{t}$) ⊤$^{n+1}$) = (using $\hat{t}$ = tree (forest $\hat{t}$) that holds by Lemma 36)

mirror$^{○}$(⊤ $\hat{t}$) ⊤$^{n+1}$)

which concludes the proof of the induction step and of the lemma.

Then, Lemma 26 ensures that *Mirror* is productive and Theorem 1 says that there is a unique function *mirror* : *Tree* → *Tree* such that *mirror* = *Mirror mirror*, i.e., for all maximal (a.k.a. totally defined) Rose trees $\hat{t}$, *mirror* $\hat{t}$ = *map mirror* (*reverse* (forest $\hat{t}$)); which was our original goal.

# 7 Conclusion, Related Work and Future Work

We have shown a way to build an $\omega$CPO from a partially ordered set satisfying certain assumptions regarding approximations and definedness measures. The assumptions have a model as finite trees, and more generally, as terms built over various classes of signatures. The $\omega$CPO resulting by completion inherits the approximation and definedness measures and enables, in combination with earlier results [9], to define total corecursive functions as unique fixpoints of their productive functionals. The approximation and definedness measures are employed in the design of practically usable, liberal sufficient conditions for productiveness. We illustrate the resulting approach for defining the *mirror* function on Rose trees as the unique fixpoint of its functional. The approach will be implemented in Coq as it is mainly designed to increase the (currently very limited) expressiveness of corecursive functions definable in Coq.

**Related Work.** Our completion operation has similarities with the classical construction of real numbers based on completing rationals with equivalence classes of Cauchy sequences of rationals. However, Cauchy sequences require metric spaces, with a distance function satisfying certain properties, and it does not seem possible tree-like datatypes such as Rose trees and their natural prefix order as a metric space. We have investigated this and found the reason: the distance requires a “weak totality” property that the prefix order does not satisfy. Defining corecursive functions based on Cauchy sequences is mentioned in [7]. Using Banach’s fixpoint theorem, corecursive functions are defined as unique fixpoints of eventually contracting functionals. However, their work is not concerned with extending the class of definable total corecursive functions beyond the guarded ones, whereas for us that is the major goal.

We now compare our work with some textbook results from elementary domain theory [2](Chapter 1). The fixpoint theorem that we are using is a specialized version of Kleene's theorem, stating that continuous functionals over CPOs (a generalization of $\omega$CPOs) have a least fixpoint. Kleene's theorem can be used for defining partial functions, and does not guarantee in any way that the resulting function is total. For totality one needs productiveness, and our version of the theorem specifically uses productiveness for defining total functions. Another textbook result is completion by ideals that transforms partial orders into CPOs and monotonic functions between partial orders into continuous functions between CPOs. Moreover, completion by ideals is a free construction, in a categorical sense; it satisfies the fewest
possible properties in order to be a completion to a CPO. However, in order to define total corecursive
functions with our approach one needs an extension of a restriction of CPOs, namely, ω CPOs extended
with specific approximation and definedness measures. Hence, completion by ideals as such is not useful
for our approach. However, a refinement of it that would transform partial orders + approximation and
definedness measures to CPOs inheriting those measures could be useful, especially if it were a free con-
struction. In that case, some tedious results that users need to prove "by hand" for each datatype (namely,
the extension of constructors and accessors of inductive types to the completed types, and their properties
- in our case, all of Section 5.1) are mere consequences of the (for now, hypothetical completion) being
free. We are planning to investigate this idea in future work.

Corecursion is present in several major proof assistants. In Coq, corecursive function definitions have to satisfy a guardedness-by-constructors criterion. In some cases, a function that is not guarded can be transformed into an equivalent, guarded function [4]. Their idea is to use an ad-hoc predicate stating that the definition under study is, in some sense, productive. However, they do not handle the case where corecursive calls are guarded by non-constructor functions, such as our mirror function for Rose trees.

Agda [11] is a proof assistant with an underlying type theory close to that of Coq. It also offers
support for corecursive function definition. In the core tool there is a guardedness checker similar to that
of Coq, but somewhat more liberal. Extensions of Agda include sized types [10] that provide users with a
uniform, automatic way of handling termination and productiveness. The implementation of sized types
is currently unsound (cf. https://github.com/agda/agda/issues/3026).

Isabelle/HOL [12] is also major proof assistant which supports corecursive functions. It accept func-
tion that go beyond guarded corecursion [5], provided the functions are *friendly* (a friendly function
needs to destruct at most one constructor of input to produce one constructor of output). Unguarded
corecursive calls are also accepted, provided they eventually produce a constructor of output. Like in our
case, the user needs to prove the conditions ensuring the well-formedness of corecursive functions.

**Future Work.** We have already mentioned the idea of presenting our approach as a free construction. This is theoretical work but has practical benefits since it eases the burden users have to go through with the current completion operation for each datatype on which they wish to define total corecursive functions. Another more practical line of work is to find applications where productive but unguarded corecursive functions are necessary. We found one in the semantics of synchronous reactive languages. Specifically, synchronous languages allowing the writing of nondeterministic programs have executions that are Rose trees, and the functions involved in their semantics are total, productive but unguarded - an interesting test-bed for our approach. Finally, the approach is targeting Coq but it is general enough to be implemented in other proof assistants. An interesting candidate is Lean [8], a proof assistant from the same family as Coq, which to our best knowledge does not have include coinductive types nor corecursive functions, but does have quotient types, which our approach would definitely benefit from.

References

[1] : *The Coq Proof Assistant*. https://coq.inria.fr/.

[2] Roberto M. Amadio & Pierre-Louis Curien (1998): *Domains and lambda-calculi*. Cambridge tracts in theoretical computer science 46, Cambridge University Press.

[3] Franz Baader & Tobias Nipkow (1998): *Term Rewriting and All That*. Cambridge University Press, doi:10.1017/CBO9781139172752.
[4] Y. Bertot & E. Komendantskaya (2008): *Inductive and Coinductive Components of Corecursive Functions in Coq*. In: Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, CMCS 2008, Budapest, Hungary, April 4-6, 2008, Electronic Notes in Theoretical Computer Science 203, pp. 25-47.

[5] J. C. Blanchette, A. Bouzy, A. Lochbihler, A. Popescu & D. Traytel: *Defining Nonprimitively (Co)recursive Functions in Isabelle/HOL*. https://isabelle.in.tum.de/dist/Isabelle2021/doc/corec.pdf.

[6] E. Giménez (1994): *Codifying Guarded Definitions with Recursive Schemes*. In: Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers, Lecture Notes in Computer Science 996, Springer, pp. 39-59.

[7] D. Kozen & N. Ruozzi (2009): *Applications of Metric Coinduction*. Log. Methods Comput. Sci. 5(3).

[8] : *The Lean Proof Assistant*. https://leanprover.github.io/.

[9] Vlad Rusu & David Nowak (2022): *Defining Corecursive Functions in Coq Using Approximations*. In: ECOOP, Berlin, Germany. Available at https://hal.inria.fr/hal-03671876.

[10] N. Veltri & N. van der Weide (2019): *Guarded Recursion in Agda via Sized Types*. In: 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, LIPIcs 131, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 32:1-32:19.

[11] : *The Agda Proof Assistant*. https://agda.readthedocs.io.

[12] : *The Isabelle/HOL Proof Assistant*. https://isabelle.in.tum.de/.