Conatural numbers

In computer science, a conatural number is either a natural number or infinity. The set of conatural numbers is denoted by ${\overline {\mathbb {N} }}$ ^[1].

Taking the predecessor is a canonical partial operation on the conatural numbers. Using the convention that the natural numbers are the positive integers, the predecessor of 1 is undefined, the predecessor of n is n - 1 for n = 2, 3, ... and the predecessor of ∞ is defined as ∞ itself. In particular, every conatural number except 1 has a predecessor. Taking the predecessor of a conatural number is canonical in the sense that this partial operation is the terminal partial operation on a set. In more detail, suppose that partial operation g : S ⇸ S on elements of a set S, i.e. a partial function from S to itself, is given. Then there exists a unique total function $f:S\to {\overline {\mathbb {N} }}$ such that (i)f(g(s)) is the predecessor of f(s) whenever g is defined on some element s in S; and (ii) f(s) does not have a predecessor whenever g is undefined on some element s in S. Indeed $f(s):=\inf\{n\in \mathbb {N} :\,g^{n}(s){\text{ is undefined}}\}$ , where $g^{n}(s)=(g\circ g\circ \cdots \circ g)(s)$ is the n-th iterate of g.

The canonicity of the predecessor partial operation can be formalised as saying that the set of conatural numbers is the carrier of the terminal coalgebra of the endofunctor $S\mapsto S\sqcup \{()\}:\mathbf {Set} \to \mathbf {Set}$ that sends a set S to its disjoint union with the singleton set ^[2]. As a carrier of this endofunctor, the conatural numbers is equipped with two destructors, a nullary ${\mathsf {isOne}}$ destructor and an unary destructor that sends a conatural number to its predecessor. Explicitly, the nullary ${\mathsf {isOne}}$ destructor is defined only on 1 and sends it to the empty tuple (). In particular, the domain of definition the unary predecessor destructor is the complement of the nullary ${\mathsf {isOne}}$ destructor.

Notes[edit]

↑ Gordon (2017, p. 15) writes that "the Peano coalgebra. . . [has] carrier set ${\overline {\mathbb {N} }}=\mathbb {N} \cup \{\infty \}$ ".
↑ On (2017, p.32), Gordon writes that "The conatural numbers are characterised as being the unique terminal $\mathbb {F} _{\mathbb {N} }$ -coalgebra." And earlier, on p. 29, he defined $\mathbb {F} _{\mathbb {N} }(X)=1+X$ , where 1 denotes the terminal set, i.e a singleton set, here chosen as {()}, and + denotes disjoint union written here as the more traditional $\sqcup$ .

References[edit]

Gordon, Mike. "Corecursion and coinduction: what they are and how they relate to recursion and induction", University of Cambridge Computer Laboratory website, first complete draft on 03 February 2017. Retrieved on 15 November 2018.

Conatural numbers

Contents

See also[edit]

Notes[edit]

References[edit]

Further reading and external links[edit]