A Coalgebraic View of Bar Recursion and Bar Induction

Abstract

We reformulate the bar recursion and induction principles in terms of recursive and wellfounded coalgebras. Bar induction was originally proposed by Brouwer as an axiom to recover certain classically valid theorems in a constructive setting. It is a form of induction on non-wellfounded trees satisfying certain properties. Bar recursion, introduced later by Spector, is the corresponding function definition principle.

We give a generalization of these principles, by introducing the notion of barred coalgebra: a process with a branching behaviour given by a functor, such that all possible computations terminate.

Coalgebraic bar recursion is the statement that every barred coalgebra is recursive; a recursive coalgebra is one that allows definition of functions by a coalgebra-to-algebra morphism. It is a framework to characterize valid forms of recursion for terminating functional programs. One application of the principle is the tabulation of continuous functions: Ghani, Hancock and Pattinson defined a type of wellfounded trees that represent continuous functions on streams. Bar recursion allows us to prove that every stably continuous function can be tabulated to such a tree, where by stability we mean that the modulus of continuity is its own modulus. Coalgebraic bar induction states that every barred coalgebra is wellfounded; a wellfounded coalgebra is one that admits proof by induction.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Bar induction is a reasoning principle formulated by L. E. J. Brouwer [9, 23].

He argued that it is justified in a constructive view of mathematics. Some classical theorems that are not otherwise provable in intuitionistic mathematics, follow from bar induction.

Intuitively, it posits a link between termination and induction. It says that if processes of a certain class always terminate, then the class admits a form of wellfounded induction.

Specifically, here is the original formulation of bar induction. Assume:

• Q is a decidable predicate on lists of natural numbers and Q is a bar (for every stream $\sigma$ there exists a natural n such that the list of the first n elements of $\sigma$ satisfies Q);

• R is another predicate on lists of naturals, such that Q implies R (every list satisfying Q also satisfies R) and is inductive (for every list l, if every extension of l by one element satisfies R, then l also satisfies R);

Then the empty list satisfies R.

In this statement, streams must be interpreted as choice sequences, that is, infinite sequences of natural numbers not necessarily given by an effective rule. Kleene proved that bar induction implies that not all streams are computable [16]. Recently, Nakata, Bezem and one of us (Uustalu) [17] proved some interesting consequences of the principle on the relationships between some temporal operators (some of them mixed inductive/coinductive) on branching processes.

Later, Spector [19] formulated the principle of bar recursion that allows definition of higher-order functionals (see also [10] and Chap. 5 of [4]); he exploited the principle to give a proof of consistency of mathematical analysis. Berardi, Bezem and Coquand [5] reformulated Spector’s principle and results; their version was termed modified bar recursion by Berger and Oliva [6], who also gave an analysis of the relation between the different variations.

We offer a reformulation and generalization of the principle in terms of coalgebras. Coalgebras are useful to model branching computational processes and types of infinite data. In previous work [7, 8] we studied the notions of recursive and wellfounded coalgebras, useful to analyze recursive functions in total functional programming and induction proofs of their properties.

Now we formulate a new notion of barred coalgebra, which characterizes processes whose computations always terminate, or data structures whose paths are all finite. We then state two principles as modern versions of Brouwer’s.

Coalgebraic bar recursion states that every barred coalgebra is recursive. This allows us to define total recursive functions on a structure if we know that all its paths are finite. We give one application to continuous functions on streams. Ghani, Hancock and Pattinson [13] defined a type of inductive trees that represent continuous functions on streams by tabulating the outputs in their leaves. We restrict our attention to stably continuous functions, where stability means that the modulus of continuity is also continuous with itself as the modulus. We show that bar recursion implies that all stably continuous functions on streams can be tabulated.

Coalgebraic bar induction states that every barred coalgebra is wellfounded. This allows us to reason about the process by a form of induction. The original form of bar induction is an instantiation of this version.

We do not claim that the principles should be accepted always and in full generality. Instead, we view them as plausible assumptions encapsulating powerful function definition and reasoning devices that need to be justified depending on the exact setting where they are invoked.

The paper is organized as follows. In Sect. 2, we introduce coalgebraic bar recursion. In Sect. 3, we apply it to tabulation of stably continuous stream functions. Coalgebraic bar induction is introduced and compared to Brouwer’s principle in Sect. 4.

2 Bar Recursion

In previous work with Vene [7], we contributed to the study of recursive coalgebras, introduced by Osius [18] and further elaborated by Paul Taylor [20–22]. More recently, Adámek, Milius and colleagues [2, 3] have made additional significant contributions.

Definition 1

A coalgebra $(A, \alpha )$ of an endofunctor F on a category $\mathcal C$ is called recursive if for every algebra $(C, \gamma )$ there exists a unique map $f: A \rightarrow C$ (a coalgebra-to-algebra morphism) making the following diagram commute:

This is a useful notion in total functional programming: It guarantees that every structured recursive diagram (that is, a coalgebra-to-algebra morphism diagram) based on it is a definite description of a function.

In the definition, unique existence of a mediating morphism is demanded upfront. No “more intrinsic” property of the coalgebra is invoked to guarantee unique constructibility of the solution.

We are interested in coalgebras of functors that can be viewed as tree generators with a good notion of a path. A special class of set functors, called container functors [1] (they are closely related to polynomial functors [12]), give tree types that work for us.

Definition 2

A container is given by a set S of shapes and an S-indexed family of positions for every shape. It defines a set functor $\llbracket S,P\rrbracket$ by

$$ \llbracket S,P\rrbracket X = \varSigma s:S.\, P\,s\rightarrow X. $$

We use containers to describe “branching types” of trees. A container (S, P) says that there are S many “types” of branching nodes and that nodes of type s : S have $P\, s$ many children. The sets of wellfounded and non-wellfounded trees with branching type (S, P) are described as the inductive type $\mu X.\, \!\!\llbracket S,P\rrbracket \!\!\, X$ (the initial algebra) and the coinductive type $\nu X.\ \!\!\llbracket S,P\rrbracket \!\!\, X$ (the final coalgebra). For the first of these to have any elements at all, there must be at least one shape with no positions.

We demand that inhabitedness of $P\, s$ is decidable for all s : S.

A coalgebra $(A, \alpha )$ is a process with a set of states A and a transition function $\alpha : A\rightarrow \!\!\llbracket S,P\rrbracket \!\!\,A$ that generates a shape and new states in every position. Unfolding $\alpha$ takes a given initial state a : A to a non-wellfounded tree. This is the unique coalgebra morphism from $(A, \alpha )$ to the final coalgebra.

Recursiveness of the coalgebra is equivalent to this tree unfolding being actually wellfounded for every initial state a : A, which in other words is to say that the unique coalgebra morphism to the final coalgebra factors through the initial algebra. (This was observed by Adámek, Lücke and Milius [2], who also called this condition the halting property.)

We suggest a classically equivalent, but constructively weaker condition. This is that, for every initial state a : A, every path in the tree unfolding of $\alpha$ takes one from the root to a leaf in a finite number of steps.¹

We need first some additional definitions to formalize what we mean by paths of an element of the coalgebra.

For every state a, we define the set $\mathsf {Path}_\alpha \, a$ of paths starting from it. At each stage, the path chooses a position through which to proceed. Notation: We define types and families by rules; sets of rules written with a single rule line are inductive definitions, sets of rules written with a double rule line are coinductive definitions.

The first rule states that, if we reached a shape with no positions, then we are at a leaf of the tree and the path ends. The second rule states that we can construct a path by choosing a position in the present shape and continuing from the new state given by the transition in that position. This definition is coinductive, so the path may continue forever.

Alternatively, we could define paths as functions from $\mathbb {N}$; but this would exclude finite paths, which would have to be extended by iterating a distinguished element. The coinductive presentation is therefore more natural and avoids some coding. The status of general coinductive types in constructivism is unclear. However, paths and also tree unfoldings of coalgebras of containers can be coded with inductive and function types. So we are justified in using them.

Next we inductively define finiteness of a path. A path $\pi$ is considered finite ($\pi \downarrow$) if it reaches a positionless shape after a finite number of steps. The definition mirrors that of paths, but it is inductive.

$$ \frac{\alpha \,a = (s,h) \quad \lnot P\,s}{\mathsf {end} \downarrow } \qquad \frac{\alpha \,a = (s,h) \quad p:P\,s \quad \pi :\mathsf {Path}_\alpha \,(h\,p) \quad \pi \downarrow }{p \mathop {\prec }\pi \downarrow } $$

Definition 3

A barred coalgebra is a coalgebra $\alpha$ whose all paths are finite:

$$ \forall a:A.\, \forall \pi :\mathsf {Path}_\alpha \,a.\ \pi \downarrow . $$

Note that the simpler condition that the coalgebra has no infinite paths, although classically equivalent, is constructively weaker than finiteness of all paths. Adopting this condition instead would make coalgebraic bar induction too strong; it would not follow from Brouwer’s formulation anymore. Assuming decidability of inhabitation of $P\,s$, the difference of the two conditions is exactly Markov’s principle.

We are now ready to formulate a coalgebraic version of the principle of bar recursion. It says that finiteness of all paths of a coalgebra implies that we can define functions by recursion. Classically this is provable, but constructively it is just a plausible extra axiom.

Coalgebraic Bar Recursion: Every barred coalgebra is recursive.

$$ \alpha ~\mathrm{barred} \Rightarrow \alpha ~\mathrm{recursive} $$

The converse implication does not need to be assumed: it is provable.

Proposition 1

Every recursive coalgebra of a container functor is barred.

$$ \alpha ~{ recursive} \Rightarrow \alpha ~{ barred} $$

Proof

Assume that a coalgebra $\alpha : A \rightarrow \!\!\llbracket S,P\rrbracket \!\!\, A$ is recursive. Then we have the unique coalgebra-to-algebra morphism $f : A \rightarrow \mu X.\, \!\!\llbracket S,P\rrbracket \!\!\, X$. For an element a : A, finiteness of all paths from a is proved by structural induction on $f\, a$.    $\square$

We will not define Spector’s bar recursion here. (Instead we will discuss Brouwer’s bar induction in detail in Sect. 4.) But it corresponds to instances of coalgebraic bar recursion for $S = 1 + 1$ and $P\, (\mathsf {inl}\, *) = 0$, $P\, (\mathsf {inr}\, *) = A$, with A some fixed set. This means that $\llbracket S,P\rrbracket \, X \cong 1 + (A \rightarrow X)$. The typical case is $A = \mathbb {N}$, but Spector also considered general A. This allowed him to interpret the general axiom of countable choice.

3 Continuous Functions on Streams

We illustrate the coalgebraic bar recursion principle by applying it to continuous functions on streams.

A function on streams is continuous if it only uses a finite initial segment of its input stream to determine its result.

Ghani, Hancock and Pattinson [13] defined an inductive type of trees for representing continuous functions on streams. When applied to a stream, a function can either immediately return a result, or read the next element of the stream and continue the computation. In the tree representation, an immediate return is modelled by a leaf containing the output value, a reading operation is modelled by a node that branches according to the input value.

The statement that all continuous functions can be represented as trees in this manner is not provable constructively without additional assumptions. Ghani, Hancock and Pattinson give a proof of a negative version of this statement: If a function has no tree representation, then it cannot be continuous.

We will show that, assuming coalgebraic bar recursion, the positive statement of representability becomes provable for what we call stably continuous functions. Stability is a natural condition, requiring that the modulus of continuity is also continuous, with itself as its modulus.

Let $\mathbb {S}_A$ be the type of streams (infinite sequences) of elements of type A. The equivalence relation $\mathrel {=_{n}}$, for n a natural number, identifies streams that coincide on the first n elements:

$$ \sigma _1 \mathrel {=_{n}} \sigma _2 \quad \mathrm{if\,and\,only\,if}\quad \forall i<n.\, \sigma _1(i) = \sigma _2(i). $$

Definition 4

A function $f:\mathbb {S}_A\rightarrow B$ from streams of elements of type A to results of type B is continuous if

$$ \forall \sigma :\mathbb {S}_A.\ \exists n:\mathbb {N}.\ \forall \sigma ':\mathbb {S}_A.\ \sigma ' \mathrel {=_{n}} \sigma \rightarrow f\,\sigma ' = f\,\sigma . $$

So a function f is continuous on a stream $\sigma$ if the value of f only depends on the first n elements of $\sigma$, for some n. It is continuous globally if it is continuous on every stream.

This definition corresponds to $\mathbb {S}_A$ being assigned the prodiscrete and B the discrete topology. This is what is appropriate for our purposes here. It can feel limited. For $B=\mathbb {S}_A$, for instance, not even the identity function is continuous, but then with the trees considered here it cannot be tabulated either.²

For other purposes, other choices can be appropriate. Brouwer’s continuity principle states that all functions of type $\mathbb {S}_\mathbb {N}\rightarrow \mathbb {N}$ are continuous. It seems justified by a computational view of functions as programs: a terminating program computes its result in a finite number of steps; during the computation it can only read a finite number of entries from the stream. This principle can be generalized to functions $A \rightarrow B$ where A and B are assigned their “native” topologies (whereby stream types must get product topologies). However, Escardó recently discovered that the continuity principle is inconsistent in type theory [11], so the principle cannot be added safely to current type-theoretic foundations. The intuitive reason is that adding the principle adds new functions to the system and some of those are problematic. Various strands of research are investigating weaker and more refined versions of the principle that may be safe.

For our goals, it is important that a continuous function has an explicit modulus of continuity, the mapping that gives the length of the initial segment of the stream needed for the computation, and that this modulus is stable, that is, it makes consistent choices for streams that have the same initial segment.

Definition 5

A modulus of continuity for a function $f:\mathbb {S}_A\rightarrow B$ is a function $m_f: \mathbb {S}_A \rightarrow \mathbb {N}$ such that

$$ \forall \sigma , \sigma ':\mathbb {S}_A.\ \sigma ' \mathrel {=_{m_f\,\sigma }} \sigma \rightarrow f\,\sigma ' = f\,\sigma . $$

The modulus is stable if

$$ \forall \sigma , \sigma ':\mathbb {S}_A.\ \sigma ' \mathrel {=_{m_f\,\sigma }} \sigma \rightarrow m_f\,\sigma ' = m_f\,\sigma . $$

So a modulus of continuity is stable if and only if it is its own modulus of continuity. Stability is a reasonable assumption in the computational view of functions:

• If, to compute $f\,\sigma$, we only need to read the first $m_f\,\sigma$ elements of $\sigma$; and

• $\sigma '$ coincides with $\sigma$ on the first $m_f\,\sigma$ elements;

• then we only need the first $m_f\,\sigma$ elements of $\sigma '$ to compute $f\,\sigma '$ (which is equal to $f\,\sigma$);

• so it is reasonable to expect that $m_f\,\sigma ' = m_f\,\sigma$.

However, given a possibly non-stable modulus, it is not in general possible to construct another modulus which is stable. In the case that the original modulus is continuous, there is an algorithm to stabilize it.

Given a non-stable but continuous modulus m, we construct a new stable modulus $\bar{m}$ for the same function. We do it by truncating every stream at an appropriate point, dictated by m, and filling in the rest of it with a fixed stream. If A is inhabited, so we know an element, we can repeat that element in a constant stream $\sigma _0$. For every $\sigma$ and every index $i:\mathbb {N}$, let ${\sigma }|_{i}$ be its truncation at position i, that is, the list $[\sigma (0),\ldots ,\sigma (i-1)]$. Let $n_i = m\,({\sigma }|_{i} \mathop {+\!\!+}\sigma _0)$. (The notation $\mathop {+\!\!+}$ denotes prepending a list to a stream and also to a path.) We now define the result of the new modulus $\bar{m}$ on $\sigma$:

$$ \bar{m}\,\sigma = n_k \quad \mathrm{where }\,k = \min \{i \mid n_i \le i\}. $$

Continuity of m guarantees that $\bar{m}$ is well defined: k always exists. In fact we know that there is a j such that, if $\sigma ' \mathrel {=_{j}} \sigma$, then $m\,\sigma ' = m\,\sigma$. In particular, if we choose $\sigma ' = {\sigma }|_{i} \mathop {+\!\!+}\sigma _0$ where $i = \max (j,m\,\sigma )$, we have:

$$ n_i = m\,\sigma ' = m\,\sigma \le i. $$

So, since there is at least one i such that $n_i\le i$, there is a minimal one k.

In Ghani, Hancock and Pattinson’s work [13], a continuous function $f:\mathbb {S}_A\rightarrow B$ is represented by a wellfounded tree, an element of the inductive type $\mathsf {SF}_{{A},{B}}$ given by the rules

$$ \frac{b:B}{\mathsf {write}\,b : \mathsf {SF}_{{A},{B}}} \qquad \frac{g:A\rightarrow \mathsf {SF}_{{A},{B}}}{\mathsf {read}\,g : \mathsf {SF}_{{A},{B}}} $$

The idea is that an element of $\mathsf {SF}_{{A},{B}}$ is a tabulation of all the values of a function as leaves in a tree whose finite paths have to be matched against the input stream. The application of a tabulation gives us a continuous function:

$$ \begin{array}{l} \mathsf {apply}: \mathsf {SF}_{{A},{B}} \rightarrow \mathbb {S}_A \rightarrow B\\ \mathsf {apply}\,(\mathsf {write}\,b)\,s = b\\ \mathsf {apply}\,(\mathsf {read}\,g)\,(a\mathop {\prec }s) = \mathsf {apply}\,(g\,a)\,s \end{array} $$

The operator $\mathsf {apply}$ is defined by structural recursion on its tree argument.

Is there an inverse transformation, that is, a tabulation operator assigning a tree to every continuous function,

$$ \mathsf {tabulate}: (\mathbb {S}_A \rightarrow B) \rightarrow \mathsf {SF}_{{A},{B}}? $$

Classically, we can prove that this function exists, but the proof is not constructive. Intuitively, the algorithm to obtain the tabulation should be the following.

Let $f:\mathbb {S}_A \rightarrow B$ be continuous. Then we can define:

$$ \begin{array}{l@{\quad }l} \mathsf {tabulate}\,f = \mathsf {write}\,b &{} \mathrm{if}\,\,\,f\,{\text {``must be"}}\,\mathrm{constantly}\,b \\ \mathsf {tabulate}\,f = \mathsf {read}\,(\lambda a. \mathsf {tabulate}\, (\lambda \sigma . f\,(a\mathop {\prec }\sigma ))) &{} \mathrm{otherwise.} \end{array} $$

It is of course undecidable whether f is constant. But if the function is continuous constructively, we also have a modulus for it and can check whether the modulus is 0 on some fixed stream (we assume A to be inhabited, so we can construct one). This a sufficient condition for constancy.

However, it is not constructively provable that this algorithm generates a wellfounded tree. If the modulus is stable, we can prove that the paths of the recursive calls generated by the second equation for f are always finite. But this is not enough to conclude that the a priori non-wellfounded tabulation tree is wellfounded.

Ghani, Hancock and Pattinson proved a negative version of the statement: they did not construct a tabulation operator, but proved that, if a function cannot be tabulated, then it is not continuous.

With bar recursion, we can conclude the positive statement, using stable continuity. We provide two distinct proofs. The first proof is local: for every stably continuous function it constructs a barred coalgebra and uses it to generate the tabulation tree. The second proof is global: it constructs a single barred coalgebra on the set of all stably continuous functions and uses it to define a tabulation operation.

3.1 Individual Tabulations

First we show how to tabulate a single stably continuous function by associating an individual barred coalgebra to it. Let $f:\mathbb {S}_A\rightarrow B$ be a function with a stable modulus of continuity $m:\mathbb {S}_A\rightarrow \mathbb {N}$. We will assume that A is inhabited and has a distinguished element, which we can repeat in a stream $\sigma _0$.

We construct a coalgebra on the functor $F\,X = B + (A\rightarrow X)$ with carrier the set of lists of elements of A:

$$ \begin{array}{l} \alpha _f : \mathsf {List}_{A} \rightarrow B+(A\rightarrow \mathsf {List}_{A}) \\ \alpha _f\,l = \left\{ \begin{array}{l@{\quad }l} \mathsf {inl}\,(f\,(l\mathop {+\!\!+}\sigma _0)) &{} \mathrm{if}\,m\,(l\mathop {+\!\!+}\sigma _0) \le \mathsf {length}\,l\\ \mathsf {inr}\,(\lambda a.\, l\mathop {+\!\!+}[a]) &{} \mathrm{otherwise.} \end{array} \right. \end{array} $$

The coalgebra checks whether the list l is sufficient to determine the result given by f: if the modulus of continuity on a stream starting with l is at most the length of l, then we know that f will depend only on it. In this case, the coalgebra terminates with the value given by f. Else, it branches into new processes for all elements of A, lengthening the list by appending the element at the end.

Observe that the functor F is a container with shapes $B+\mathsf {1}$, a shape for each possible leaf in B, and a single shape for the continuation. The shapes in B have no positions: the coalgebra terminates. The single continuation shape has positions for all possible input elements, so the set of positions is A. The paths in $\mathsf {Path}_\alpha \,l$ are sequences of position choices, so in this case they are sequences of elements of A. Any such path $\pi$ can be padded out to a stream of elements of A by appending $\sigma _0$ to it: $\mathsf {pad}\, \mathsf {end}= \sigma _0$, $\mathsf {pad}\, (a \mathop {\prec }\pi )= a \mathop {\prec }\mathsf {pad}\, \pi$.

Lemma 1

$\alpha _f$ is a barred coalgebra.

Proof

Given $l: \mathsf {List}_{A}$ and $\pi :\mathsf {Path}_\alpha \,l$, we prove that $\pi \downarrow$ by induction on $m\, \sigma _{l,\pi } - \mathsf {length}\,l$ where $\sigma _{l,\pi } = l \mathop {+\!\!+}\mathsf {pad}\, \pi$.

• If $m\, \sigma _{l,\pi } - \mathsf {length}\,l = 0$, then $m\, \sigma _{l,\pi } \le \mathsf {length}\,l$, so $\sigma _{l,\pi } \mathrel {=_{m\,\sigma _{l,\pi }}} l\mathop {+\!\!+}\sigma _0$. By stability, $m\,(l\mathop {+\!\!+}\sigma _0) = m\,\sigma _{l,\pi } \le \mathsf {length}\,l$. Therefore $\alpha _f\,l = \mathsf {inl}\,(f\,(l\mathop {+\!\!+}\sigma _0))$ and $\pi = \mathsf {end}$. In this case obviously the path is finite.

• Otherwise, if $m\,\sigma _{l,\pi } - \mathsf {length}\,l > 0$, then $m\,\sigma _{l,\pi } > \mathsf {length}\,l$. It is impossible that $m\,(l\mathop {+\!\!+}\sigma _0)\le \mathsf {length}\,l$ because, if it were, then also $m\,\sigma _{l,\pi } = m\,(l\mathop {+\!\!+}\sigma _0) \le \mathsf {length}\,l$ by stability. So $\alpha _f\,l = \mathsf {inr}\,(\lambda a.\, l\mathop {+\!\!+}[a])$ and $\pi = a\mathop {\prec }\pi '$ for some a : A and $\pi ':\mathsf {Path}_\alpha \,(l\mathop {+\!\!+}[a])$. Note that $\sigma _{l\mathop {+\!\!+}[a],\pi '} = \sigma _{l,\pi }$, so $m\,\sigma _{l\mathop {+\!\!+}[a],\pi '} - \mathsf {length}\,(l\mathop {+\!\!+}[a]) = m\,\sigma _{\pi } - \mathsf {length}\,l - 1$. Therefore $\pi ' \downarrow$ by the induction hypothesis and so $\pi \downarrow$.      $\square$

We can now invoke bar induction on this coalgebra to tabulate f.

Theorem 1

The coalgebraic bar induction principle implies that there exists an element $\mathsf {tabulate}_f:\mathsf {SF}_{{A},{B}}$ such that $\mathsf {apply}\,(\mathsf {tabulate}_f)\,\sigma = f\,\sigma$ for every $\sigma :\mathbb {S}_A$.

Proof

If we apply the coalgebraic bar recursion principle to the statement of Lemma 1, we obtain that $\alpha _f$ is a recursive coalgebra.

Notice that $\mathsf {SF}_{{A},{B}}$ is the carrier of the initial algebra of the functor F:

$$ \mathsf {SF}_{{A},{B}} = \mu X.\, B+(A\rightarrow X). $$

The copair of the two constructors $[\mathsf {write},\mathsf {read}]$ is the actual algebra.

We can apply the defining property of recursive coalgebras to deduce that there exists a unique function $\mathsf {tab}$ making the following diagram commute.

We can now define the Ghani, Hancock and Pattinson representation of f by

$$ \begin{array}{l} \mathsf {tabulate}_f : \mathsf {SF}_{{A},{B}}\\ \mathsf {tabulate}_f = \mathsf {tab}\,[]. \end{array} $$

Its correctness can be checked simply by observing that, in general,

$$\begin{aligned} \mathsf {apply}\,(\mathsf {tab}\,l)\,\sigma = f\,(l\mathop {+\!\!+}\sigma ). \end{aligned}$$

   $\square$

3.2 Global Tabulation

The second way to use coalgebraic bar recursion for tabulation is to define a coalgebra on the set of all stably continuous functions:

$$ \mathcal{F}= \{(f,m) \mid m:\mathbb {S}_A \rightarrow \mathbb {N}\ ~\text {is a stable modulus of}~f:\mathbb {S}_A \rightarrow B \}. $$

We use the same functor as for the individual coalgebras of the previous section: $F\,X = B+(A\rightarrow X)$. The algebra simply tests whether a function must be constant: if it has to be, it returns its value, otherwise it branches. It does so by checking that the modulus is 0 for $\sigma _0$; it must be then be 0 for all streams by stability.

$$ \begin{array}{l} \alpha : \mathcal{F}\rightarrow B+(A\rightarrow \mathcal{F})\\ \alpha \, (f,m) = \left\{ \begin{array}{l@{\quad }l} \mathsf {inl}\,(f\,\sigma _0) &{} \text {if}~ m\,\sigma _0 = 0 \\ \mathsf {inr}\,(\lambda a.\, (f_a, m_a) &{} \text {otherwise} \end{array} \right. \end{array} $$

where

$$ f_a\,\sigma = f\,(a\mathop {\prec }\sigma ) \quad \text {and} \quad m_a\,\sigma = m\,(a\mathop {\prec }\sigma ) - 1. $$

In the branching case, the coalgebra reads an element of the input, a, and returns the function $f_a$ obtained by shifting f by a. The modulus $m_a$ of $f_a$ is one less than the modulus of f, as we do not count the prepended element a.

Lemma 2

The coalgebra $\alpha$ is barred.

Proof

Let $\pi :\mathsf {Path}_\alpha \, (f,m)$ be a path of the coalgebra. We prove that $\pi \downarrow$ by induction on $m\,\sigma _\pi$ where $\sigma _\pi = \mathsf {pad}\, \pi$.

• If $m\,\sigma _\pi =0$, then also $m\,\sigma _0 =0$ by stability. So $\alpha \, (f,m) = \mathsf {inl}\,(f\,\sigma _0)$ and $\pi = \mathsf {end}$.

• If $m\,\sigma _\pi > 0$, then also $m\,\sigma _0 > 0$ by stability. So $\alpha \, (f,m) = \mathsf {inr}\,(\lambda a.\, ( f_a, m_a))$. It must then be that $\pi = a\mathop {\prec }\pi '$ for some a : A and $\pi ':\mathsf {Path}_\alpha \, (f_a,m_a)$. If we then compute the modulus of the stream associated to the tail of the path, we obtain

  $$ m_a\,\sigma _{\pi '} = m\,(a\mathop {\prec }\sigma _{\pi '}) - 1 = m\,\sigma _\pi - 1. $$

  Therefore $\pi ' \downarrow$ by the induction hypothesis, so $\pi \downarrow$.   $\square$

We can now invoke bar induction on this coalgebra to construct a global tabulation operator.

Theorem 2

The coalgebraic bar induction principle implies that there exists a function $\mathsf {tabulate}: \mathcal{F}\rightarrow \mathsf {SF}_{{A},{B}}$ such that, for every continuous function with stable modulus $(f,m):\mathcal{F}$ and every stream $\sigma :\mathbb {S}_A$, we have

$$ \mathsf {apply}\,(\mathsf {tabulate}\, (f,m))\,\sigma = f\,\sigma . $$

Proof

Applying the coalgebraic bar induction principle to the result of Lemma 2, we obtain that $(\mathcal{F},\alpha )$ is a recursive coalgebra. In particular, the following diagram has a unique solution.

The operator $\mathsf {tabulate}$ maps every function to a correct tabulation tree for it. We prove this by induction on $m\,\sigma _0$:

• If $m\,\sigma _0 =0$, then, by commutativity of the diagram, definition of $\alpha$ and continuity,

  $$\begin{aligned} \mathsf {apply}\,(\mathsf {tabulate}\, (f,m))\,\sigma&= \mathsf {apply}\,([\mathsf {write},\mathsf {read}]\,(F\,\mathsf {tabulate}\,(\alpha \, (f,m))))\,\sigma \\&=\mathsf {apply}\,([\mathsf {write},\mathsf {read}]\,(\mathsf {inl}\,(f\,\sigma _0)))\,\sigma \\&=\mathsf {apply}\,(\mathsf {write}\,(f\,\sigma _0))\,\sigma \\&=f\,\sigma _0 = f\,\sigma .\\ \end{aligned}$$

• If $m\,\sigma _0 >0$, then, writing $\sigma = a\mathop {\prec }\sigma '$, by commutativity of the diagram, the definition of $\alpha$ and the induction hypothesis,

  $$\begin{aligned} \mathsf {apply}\,(\mathsf {tabulate}\, (f,m))\,\sigma&= \mathsf {apply}\,([\mathsf {write},\mathsf {read}]\,(F\,\mathsf {tabulate}\,(\alpha \, (f,m))))\,\sigma \\&= \mathsf {apply}\,([\mathsf {write},\mathsf {read}]\,(\mathsf {inr}\,(\lambda a.\, \mathsf {tabulate}\, (f_a, m_a))))\,\sigma \\&= \mathsf {apply}\,(\mathsf {read}\,(\lambda a.\, \mathsf {tabulate}\, (f_a, m_a)))\,(a\mathop {\prec }\sigma ') \\&= \mathsf {apply}\,(\mathsf {tabulate}\, (f_a, m_a)))\,\sigma ' \\&= f_a\,\sigma ' = f\,(a\mathop {\prec }\sigma ') = f\,\sigma . \end{aligned}$$

     $\square$

We finish this discussion of tabulation of continuous functions on streams by noting that we need bar recursion for tabulation because our notion of (stable) continuity of a function (which is the standard notion of continuity) is path-based. It considers one stream (choice sequence) at a time and requires that reaching an answer takes a finite number of steps. Alternatively, we could define continuity in a way that considers the entirety of possible evolutions of the choice process at once. This would result in a stronger notion of continuity and then a continuous function could be tabulated without assumptions like bar recursion.

Concretely, we could define continuity as a predicate on $\mathbb {S}_A \rightarrow B$ inductively as follows.

$$ \frac{\forall \sigma , \sigma ' : \mathbb {S}_A.\, f\, \sigma = f\, \sigma '}{f \mathrm {~continuous}} \qquad \frac{\forall a : A.\, (\lambda \sigma .\, f (a \mathop {\prec }\sigma )) \mathrm {~continuous}}{f \mathrm {~continuous}} $$

Tabulation would be immediate by structural recursion on the proof of continuity (and not exciting at all).

4 Bar Induction

We now want to give a coinductive account of the traditional formulation of bar induction. For this purpose, the notion of wellfounded coalgebra will be useful. Intuitively, it is a coalgebra that admits proofs of properties of its elements by induction. This notion was introduced by Taylor [20–22], who proved that, under weak reasonable assumptions, recursiveness and wellfoundedness of a coalgebra are equivalent. (In a previous article [8], we gave a review of the topic and extended it to the dual case or corecursive vs. antifounded algebras.)

Our formulation uses the next-time operator by Jacobs [15] on subobjects (subsets) of the carrier of a coalgebra. Let $(A, \alpha )$ be a coalgebra of a functor F that preserves pullbacks along monos on a category with pullbacks along monos. (These requirements are satisfied by container functors.)

Definition 6

Let $j:U \hookrightarrow A$ be a subobject of the carrier of the coalgebra. The next-time subobject, $\mathsf {nt}_\alpha \,j : \mathsf {nt}_\alpha \,U \hookrightarrow A$ is defined by the following pullback.

The idea of this definition is that, if U is a subset of A, then $\mathsf {nt}_\alpha \,U$ is the subset of A consisting of the elements that, after an $\alpha$ transition, fall into U.

In particular, suppose F is a container functor, $F = \!\!\llbracket S,P\rrbracket \!\!$. If a : A, then $\alpha \,a : F\,A$ has the form (s, h) with s : S and $h:P\,s\rightarrow A$. We have that $a\in \mathsf {nt}_\alpha \,U$ if, for all $p:P\,s$, $h\,p \in U$.

$$ \mathsf {nt}_\alpha \,U = \{ a:A \mid \forall p:P\,s.\ h\,p \in U\,\text {where}\, (s, h) = \alpha \, a \} $$

Definition 7

The coalgebra $(A,\alpha )$ is wellfounded if, for every subobject $j:U\hookrightarrow A$, if $\mathsf {nt}_\alpha \,U$ factors through U, then j is an isomorphism. In diagram form this says that

In simpler terms, the coalgebra is wellfounded, if $\mathsf {nt}_\alpha \,U \subseteq U$ implies $A \subseteq U$.

Intuitively, the defining property of wellfounded coalgebras is a generalization of the familiar induction principle associated to initial algebras. We want to prove that all elements of A are in the subset U. And we do this by showing that, if all “components” of an element a : A (given by $\alpha \,a$) are in U, so is a.

We introduce the following principle.

Coalgebraic Bar Induction: Every barred coalgebra is wellfounded.

$$ \alpha ~\mathrm{barred} \Rightarrow \alpha ~\mathrm{wellfounded} $$

This principle says that, if all paths of a coalgebra are finite, then we can prove its properties by induction.

The converse implication holds without extra assumptions.

Proposition 2

Every wellfounded coalgebra is barred.

$$ \alpha ~{wellfounded} \Rightarrow \alpha ~{barred} $$

Proof

Assume that $\alpha$ is wellfounded and take U to be the subset of those elements of A whose all paths are finite:

$$ U = \{a:A \mid \forall \pi :\mathsf {Path}_\alpha \,a.\ \pi \downarrow \}. $$

We then have that

$$ \mathsf {nt}_\alpha \,U = \{a:A \mid \forall p:P\,s.\ \forall \pi ':\mathsf {Path}_\alpha \,(h\,p).\, \pi ' \downarrow ~\text {where}~ (s, h) = \alpha \, a\}. $$

Suppose $a\in \mathsf {nt}_\alpha \,U$; we want to prove that $a\in U$. So assume $\pi :\mathsf {Path}_\alpha \,a$; we will show that this path is finite. Suppose $\alpha \, a = (s, h)$. If $\pi = \mathsf {end}$, as $\lnot P\, s$, then we conclude immediately that $\pi \downarrow$. If $\pi = p\mathop {\prec }\pi '$ for some $p:P\,s$ and $\pi ':\mathsf {Path}_\alpha \,(h\,p)$, then we know by assumption that $\pi ' \downarrow$ and consequently $\pi \downarrow$.

We proved that $\mathsf {nt}_\alpha \,U \subseteq U$; therefore, by wellfoundedness of $\alpha$, we have that $A \subseteq U$. So all paths are finite.    $\square$

The traditional formulation of bar induction from Brouwer is about predicates on lists of natural numbers.

Brouwer’s Bar Induction:

• Let Q be a decidable predicate on lists of natural numbers. Assume that Q is a bar: $\forall \sigma :\mathbb {S}_\mathbb {N}.\ \exists n:\mathbb {N}.\ Q\,({\sigma }|_{n})$.

• Let R be a predicate on lists of naturals. Assume that Q implies R and R is inductive: $\forall l:\mathsf {List}_{\mathbb {N}}.\, (\forall p:\mathbb {N}.\, R\,(l\mathop {+\!\!+}[p])) \rightarrow R\,l$.

• Then $R\,[]$ holds.

We can assume that Q and R are suffix closed: $\forall l:\mathsf {List}_{\mathbb {N}}.\, \forall p: \mathbb {N}.\, Q\,l \rightarrow Q\,(l\mathop {+\!\!+}[p])$ and similarly for R. Indeed, if they are not, we can use their suffix closures. We can define $\hat{Q}\, l$ to hold if $\exists n\le \mathsf {length}\,l.\, Q\,({l}|_{n})$ and similarly for $\hat{R}$. The new predicates $\hat{Q}$ and $\hat{R}$ still satisfy the assumptions of the principle and $\hat{R}\,[] \leftrightarrow R\,[]$. Also, since Q is decidable, Q being a bar implies that it is also a “tight” bar: $\forall \sigma :\mathbb {S}_\mathbb {N}.\ \exists n:\mathbb {N}.\ (\forall m: \mathbb {N}.\, m < n \rightarrow \lnot Q\,({\sigma }|_{m})) \wedge Q\,({\sigma }|_{n})$.

Instead of $\mathbb {N}$, one could consider other sets in Brouwer’s bar induction. The case of $\mathbb {B}$ is known as the fan “theorem” (Brouwer thought that fan theorem and bar induction were theorems, but both are just plausible axioms; the fan theorem is a positive version of weak König’s lemma). In principle one could replace $\mathbb {N}$ with any fixed set, but the question is how justified this is from the constructive point of view. $\mathbb {N}$ is special in that it is a set that can be traversed by an infinite process.

The traditional form of bar induction follows from the coalgebraic version.

Theorem 3

Coalgebraic bar induction implies Brouwer’s bar induction.

Proof

Given Q and R satisfying the assumptions of Brouwer’s bar induction, we define a coalgebra structure of the functor $F\,X = 1 + (\mathbb {N}\rightarrow X)$ on the set $\mathsf {List}_{\mathbb {N}}$.

$$ \begin{array}{l} \alpha : \mathsf {List}_{\mathbb {N}} \rightarrow 1 + (\mathbb {N}\rightarrow \mathsf {List}_{\mathbb {N}}) \\ \alpha \,l = \left\{ \begin{array}{l@{\quad }l} \mathsf {inl}\,*&{} \text {if}~Q\,l\\ \mathsf {inr}\,(\lambda p.\, l\mathop {+\!\!+}[p]) &{} \text {otherwise}. \end{array} \right. \end{array} $$

The function $\alpha$ is welldefined, since Q is decidable. From the assumption that Q is a bar, we conclude that $\alpha$ is barred. Indeed, let $\pi : \mathsf {Path}_\alpha \,l$ for some list l; we must prove that $\pi$ is finite. We consider the stream $\sigma = l \mathop {+\!\!+}\mathsf {pad}\, \pi$ (using, e.g., 0 as the distinguished element of $\mathbb {N}$ for padding). Since Q is decidable and a bar, $\sigma$ must have a shortest finite prefix ${\sigma }|_{n}$ satisfying Q. If $n < \mathsf {length}\, l$, then ${\sigma }|_{n}$ is a proper prefix of l. This forces that $\pi = \mathsf {end}$, since suffix-closedness of Q gives us that $Q\, l$. If $n \ge \mathsf {length}\, l$, then $l \mathop {+\!\!+}\pi = {\sigma }|_{n} \mathop {+\!\!+}\mathsf {end}$. Either way, $\pi$ is finite.

Thus we can apply coalgebraic bar induction and learn that $\alpha$ is wellfounded.

Let $U = \{l:\mathsf {List}_{\mathbb {N}} \mid R\,l\}$. (In type theory we can use the dependent pair type $\varSigma l:\mathsf {List}_{\mathbb {N}}.\ R\,l$.) We will prove that $\mathsf {nt}_\alpha \,U \subseteq U$ from where by wellfoundedness of $\alpha$ it will follow that $\mathsf {List}_{\mathbb {N}} \subseteq U$.

By definition

$$ \mathsf {nt}\,U =\{l:\mathsf {List}_{\mathbb {N}} \mid \alpha \,l \in 1+(\mathbb {N}\rightarrow U)\} $$

We prove that if $l\in \mathsf {nt}\,U$, then $l\in U$, by cases:

• If $Q\,l$ holds, then $\alpha \,l = \mathsf {inl}\,*$. Since Q implies R, we also have $R\,l$, that is, $l\in U$.

• If $Q\,l$ does not hold, then $\alpha \,l = \mathsf {inr}\,(\lambda p.\, l\mathop {+\!\!+}[p])$ with $l\mathop {+\!\!+}[p] \in U$ for every $p:\mathbb {N}$. By the assumption that R is inductive, we can derive that $l\in U$.

Therefore, since $\alpha$ is wellfounded, we can deduce that $\mathsf {List}_{\mathbb {N}} \subseteq U$, that is, $\forall l:\mathsf {List}_{\mathbb {N}}.\, R\,l$.

In particular, $R\,[]$, as desired.    $\square$

From Brouwer’s bar induction, coalgebraic bar induction follows for the functor $F\, X = 1 + (\mathbb {N}\rightarrow X)$.

Theorem 4

Brouwer’s bar induction implies coalgebraic bar induction for $F\, X = 1 + (\mathbb {N}\rightarrow X)$.

Proof

Given any set A with a barred coalgebra structure $\alpha : A \rightarrow 1 + (\mathbb {N}\rightarrow A)$ and a subset U of A satisfying the assumption $\mathsf {nt}_\alpha \, U \subseteq U$ of coalgebraic bar induction.

We define a function ${\searrow } : A \rightarrow \mathsf {List}_{\mathbb {N}} \rightarrow 1 + A$ by

$$ \begin{array}{l} a \searrow [] = \mathsf {inr}\,a \\ a \searrow (l \mathop {+\!\!+}[p]) = \left\{ \begin{array}{l@{\quad }l} \mathsf {inl}\, *&{} \mathrm {if~} a \searrow l = \mathsf {inl}\, *\\ \mathsf {inl}\, *&{} \mathrm {if~} a \searrow l = \mathsf {inr}\, a' \mathrm {~and~} \alpha \, a' = \mathsf {inl}\, *\\ \mathsf {inr}\, (f\, p) &{} \mathrm {if~} a \searrow l = \mathsf {inr}\, a' \mathrm {~and~} \alpha \, a' = \mathsf {inr}\, f \end{array} \right. \end{array} $$

For any a : A, we define $Q_a\, l$ to hold, if $a \searrow l = \mathsf {inl}\, *$, and $R_a\, l$ to hold, if $a \searrow l = \mathsf {inl}\, *$ or $a \searrow l = \mathsf {inr}\, a'$ and $a' \in U$.

It is immediate that, for any a : A, $Q_a$ is decidable and $\forall l: \mathsf {List}_{\mathbb {N}}.\, Q_a\, l \rightarrow R_a\, l$. Moreover, as $\alpha$ is barred, $Q_a$ is also a bar.

From $\mathsf {nt}_\alpha \, U \subseteq U$, it also follows that $R_a$ is inductive for all a : A.

Hence, for any given a : A, we can apply Brouwer’s bar induction, and conclude that $R_a\, []$. Since $a \searrow [] = \mathsf {inr}\, a$, this means that $a \in U$.   $\square$

Coalgebraic bar induction follows from Brouwer’s bar induction also for general container functors $\llbracket S,P\rrbracket$ for which $\varSigma s : S.\, P\, s$ is isomorphic to a decidable subset of $\mathbb {N}$. This is proved by “approximate” branchings of type $\llbracket S,P\rrbracket$ with branchings of type $F X = 1 + (\mathbb {N}\rightarrow X)$.

5 Conclusions

The explicit use of bar recursion and bar induction makes it possible to encapsulate non-constructive aspects of arguments about non-wellfounded trees and stream functions.

In this paper, we have defined coalgebraic versions of bar recursion and bar induction. We find that this perspective has at least two benefits. First, we can speak of the ingredients involved in bar recursion and bar induction using the terminology of modern theoretical computer science, especially coalgebra. Second, we can avoid unnecessary coding when we want to deal with types of trees with multiple types of branching nodes, with different numbers of children.

The notion of barred coalgebra neatly fills a useful position in the range of properties that a coalgebra may satisfy. In reasoning about the total correctness of programs, it is usual to give a proof of termination for all computations and then prove by induction that some invariant holds. This application of wellfounded induction is classically justified from termination, but is not constructively valid. Bar induction is the missing principle that provides the link. Since coalgebraic methods are becoming standard tools in programming and reasoning about correctness, we hope that the coalgebraic formulation of bar recursion will establish itself as a useful tool in functional programming and type theory.

Directly applying the traditional forms of bar induction and bar recursion in concrete cases often requires a lot of encoding, namely making all nodes to be of the same type with the same number of children, which also makes all paths infinite, all this artificially; termination is then characterized by a predicate with the bar property. Our formulation is more liberal and requires no encoding: nodes of different branching degrees are allowed and termination is simply modelled by leaves.