Spreads, Fans and Bars over Containers.

This post is an introduction to the container-oriented generalization of the core Brouwerian (co)data structures, inspired by Ghani, Hancock and Pattinson.1 I am not introducing anything novel; I’m merely taking their framework and showing how to round up the usual suspects of Brouwerian mathematics in their generalized, “family-friendly” setting. I am using Constable et al’s Computational Type Theory + Induction-Recursion as my metalanguage,2 but other variants of type theory may be used as well.

Generalized Neighborhoods: an inductive-recursive definition

Much of Brouwerian mathematics is based on three core notions concerning infinite trees of natural numbers: the choice sequence, the spread, and the bar. Brouwer’s spreads are predicates on finite prefixes of choice sequences (i.e. predicates on lists of natural numbers), subject to certain laws. Ghani et al generalize this over some family of sets \(\pi : {\mathbb{E}}\to{\mathbb{U}_{i}}\) by constructing a theory of neighborhoods (finite approximations \({{{\color{MidnightBlue}{u}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}}\)) of ideal points (i.e. choice sequences), inductive-recursively with their positions for refinement \({{{\color{MidnightBlue}{r}}}\in{{\color{MidnightBlue}{{\pi^\natural(u)}}}}}\):

\[ {\dfrac{\matrix{}}{{{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}\in{{\color{MidnightBlue}{{\mathbb{U}_{i}}}}}}}} \qquad {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}} }}{ {{{\color{MidnightBlue}{{\pi^\natural(u)}}}}\in{{\color{MidnightBlue}{{\mathbb{U}_{i}}}}}} }}\\[18pt] {\dfrac{\matrix{}}{{{{\color{MidnightBlue}{{\langle\rangle}}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}}}} \qquad {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}} & {{{\color{MidnightBlue}{r:{\pi^\natural(u)}}}}\gg {{{\color{MidnightBlue}{e}}}\in{{\color{MidnightBlue}{{\mathbb{E}}}}}}} }}{ {{{\color{MidnightBlue}{{u\frown r.e[r]}}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}} }} \]

The above rules are justified by the computational behavior of the non-canonical operator \({\pi^\natural(\cdot)}\):

\[ {\dfrac{\matrix{ }}{ {{{\color{MidnightBlue}{{\pi^\natural({\langle\rangle})}}}}\Rightarrow{{\color{Maroon}{{\mathsf{unit}}}}}} }} \qquad {\dfrac{\matrix{ {{{\color{MidnightBlue}{{\pi^\natural(u)}}}}\Rightarrow{{\color{Maroon}{R}}}} }}{ {{{\color{MidnightBlue}{{\pi^\natural({u\frown r.e[r]})}}}}\Rightarrow{{\color{Maroon}{{(\Sigma s\in R)\,\pi(e[s])}}}}} }} \]

The relation of one approximation being a prefix of another is easily defined:

\[ {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}} & {{{\color{MidnightBlue}{v}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}} }}{ {{{\color{MidnightBlue}{{u\preceq v}}}}\in{{\color{MidnightBlue}{{\mathbb{U}_{i}}}}}} }}\\[18pt] {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\Rightarrow{{\color{Maroon}{{\langle\rangle}}}}} }}{ {{{\color{MidnightBlue}{{u\preceq v}}}}\Rightarrow{{\color{Maroon}{{\mathsf{unit}}}}}} }} \qquad {\dfrac{\matrix{ {{{\color{MidnightBlue}{v}}}\Rightarrow{{\color{Maroon}{{w\frown r.e[r]}}}}} & {{{\color{MidnightBlue}{{u\preceq w}}}}\Rightarrow{{\color{Maroon}{P}}}} }}{ {{{\color{MidnightBlue}{{u\preceq v}}}}\Rightarrow{{\color{Maroon}{P}}}} }} \]

The view from the treetops: containers

What’s going on here? It will be helpful to specify in precisely what way Ghani et al generalized Brouwer’s menagerie of (co)data structures. Brouwer started off with the notion of a choice sequence as an infinite stream of natural numbers; a spread could be viewed as a collection of ideal points (i.e. choice sequences), and was given finitarily as a predicate on finite approximations of choice sequences (i.e. neighborhoods around the ideal points).

In our setting, we recognize how streams of naturals (or their finitary approximations, lists) arise as the greatest fixed points (resp. least fixed points) of the extension of a container \({n\in{\mathbb{N}}\triangleleft {\mathsf{unit}}}\), as developed in the theory of containers by Abbot, Ghani, McBride and others. To be precise, for a container \({{{\color{MidnightBlue}{C}}}\equiv{{\color{Maroon}{{e\in{\mathbb{E}}\triangleleft \pi(e)}}}}}\), its extension \({⟦C⟧(\cdot)}\) is defined as follows:

\[ {{{\color{MidnightBlue}{ {⟦C⟧(X)} }}}\equiv{{\color{Maroon}{ {(\Sigma e\in {\mathbb{E}})\,{\pi(e)\supset X}} }}}} \]

So, if we develop our theory in this very general setting, we shall recover Brouwer’s choice sequences and spreads in case \({{{\color{MidnightBlue}{C}}}\equiv{{\color{Maroon}{{n\in{\mathbb{N}}\triangleleft {\mathsf{unit}}}}}}}\), but in general, our choice sequences will be non-wellfounded trees, and our finite approximations will be well-founded trees. Streams and lists are the special cases of these where at each point, there is only one position for refinement.

The other sense in which this formulation is more general than Brouwer’s is that we do not restrict our nodes to be labelled by natural numbers; instead, each node is labelled with some \({{{\color{MidnightBlue}{e}}}\in{{\color{MidnightBlue}{{\mathbb{E}}}}}}\). In Brouwer’s parlance, this is a “dressed spread”; Brouwer starts with spreads of natural numbers, and then allows a spread of some other type in case there is a correlation law that allows it to be derived from an already-defined “naked spread” (i.e. a spread of natural numbers).

Generalized Spreads

Brouwer’s notion of a spread (law) may be reformulated so as to constrain predicates on neighborhoods \({{{\color{MidnightBlue}{u}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}}\). The core criteria are as follows:

  1. The spread shall leak upwards: in other words, if an approximation is in a spread, there must also be a refinement of that approximation in the spread.

  2. The spread shall be downward closed: if an approximation is in the spread, so should be its prefixes.

  3. The empty neighborhood shall be admitted. (Sambin strengthens this to say, “the spread shall be inhabited”,3 which in combination with downward closedness implies the admission of the empty neighborhood.)

Dummett4 and van Atten5 require in addition that the spread law be decidable; in his formal topology, Sambin does not require this, but notes it as an option.

Interpreted in our system, these requirements amount to the following constraint on neighborhood predicates: \[ {{{\color{MidnightBlue}{ {\mathsf{decidable}(\mathfrak{S})} }}}\equiv{{\color{Maroon}{ {(\Pi u\in {{\mathbb{E}}^\natural})\, \mathfrak{S}(u) + \lnot \mathfrak{S}(u) } }}}}\\ {{{\color{MidnightBlue}{ {\mathsf{leaksUpward}(\mathfrak{S})} }}}\equiv{{\color{Maroon}{ {(\Pi u\in {{\mathbb{E}}^\natural})\, {\mathfrak{S}(u)\supset {(\Sigma e\in {{\pi^\natural(u)}\supset {\mathbb{E}}})\, \mathfrak{S}({u\frown r.e(r)}) } } } }}}}\\ {{{\color{MidnightBlue}{ {\mathsf{downwardClosed}(\mathfrak{S})} }}}\equiv{{\color{Maroon}{ {(\Pi v\in {{\mathbb{E}}^\natural})\, {(\Pi u\in {\{u\in {{\mathbb{E}}^\natural}\mid {u\preceq v}\}})\, { \mathfrak{S}(v) \supset \mathfrak{S}(u) } } } }}}}\\ {{{\color{MidnightBlue}{ {\mathsf{isSpread}(\mathfrak{S})} }}}\equiv{{\color{Maroon}{ {\mathsf{decidable}(\mathfrak{S})} \times {\mathsf{leaksUpward}(\mathfrak{S})} \times {\mathsf{downwardClosed}(\mathfrak{S})} \times \mathfrak{S}({\langle\rangle}) }}}} \]

From these definitions, we can give the type of spreads as \[ {{{\color{MidnightBlue}{ {\mathsf{spread}}_i }}}\equiv{{\color{Maroon}{ {\{\mathfrak{S}\in {{{\mathbb{E}}^\natural}\supset {\mathbb{U}_{i}}} \mid {\mathsf{isSpread}(\mathfrak{S})}\}} }}}} \]

A spread may be thought of as generating a non-wellfounded tree, whose paths are choice sequences (infinite streams in Brouwer’s case) which are approximated (prefixed) by our neighborhoods (lists in Brouwer’s case).

Fans are finitary spreads

In general, the trees generated by spreads are both infinitely deep and (possibly) infinitely wide. For instance, if \({{{\color{MidnightBlue}{{\mathbb{E}}}}}\equiv{{\color{Maroon}{{\mathbb{N}}}}}}\), then for the universal spread given by the law \({\lambda(u. {\mathsf{unit}})}\), each node has \(\omega\) many children directly below it. A fan, then, is defined as a finitary spread, i.e. a spread where each node has only a finite number of children directly below it.

In Brouwer’s simple setting where we operate over the container signature \({n\in{\mathbb{N}}\triangleleft {\mathsf{unit}}}\) , it is easy to give a definition of fans, as Dummett does: \[ {{{\color{MidnightBlue}{ {\mathsf{isFan}(\mathfrak{S})} }}}\equiv{{\color{Maroon}{ {\mathsf{isSpread}(\mathfrak{S})} \times {(\Pi u\in {\{u\in {{\mathbb{E}}^\natural}\mid \mathfrak{S}(u)\}})\, {(\Sigma k\in {\mathbb{N}})\, {(\Pi m\in {\{m\in {\mathbb{N}}\mid m > k\}})\, \lnot \mathfrak{S}({u\frown r.m}) } } } }}}}\tag{*} \]

In other words, there’s a bound on the number of possible refinements to an approximation which do not escape the spread. This definition doesn’t quite work out for us in the generalized setting, however; in type theory, however, we have a more general way of expressing the finitude of set:

\[ {{{\color{MidnightBlue}{ {{\mathbb{N}}_{n}} }}}\equiv{{\color{Maroon}{ {\{m\in {\mathbb{N}}\mid m \leq n \}} }}}}\\ {{{\color{MidnightBlue}{ {\mathsf{surj}(A; B; f)} }}}\equiv{{\color{Maroon}{ {(\Pi b\in B)\, {(\Sigma a\in A)\, {f(a)=b\in B} } } }}}}\\ {{{\color{MidnightBlue}{ {\mathsf{isFinite}(A)} }}}\equiv{{\color{Maroon}{ {(\Sigma n\in {\mathbb{N}})\, {\{f\in {{{\mathbb{N}}_{n}}\supset A} \mid {\mathsf{surj}({{\mathbb{N}}_{n}}; A; f)} \}} } }}}} \]

A proper definition of fan-hood may now be given:

\[ {{{\color{MidnightBlue}{ {\mathsf{isFan}(\mathfrak{S})} }}}\equiv{{\color{Maroon}{ {\mathsf{isSpread}(\mathfrak{S})} \times {(\Pi u\in {{\mathbb{E}}^\natural})\, {\mathsf{isFinite}( {\{e\in {{\pi^\natural(u)}\supset {\mathbb{E}}} \mid \mathfrak{S}({u\frown r.e(r)}) \}} )} } }}}} \]

Generalized Choice Sequences

A choice sequence in this setting is going to be an infinite tree of refinements: the greatest fixed point of our container’s extension. Now, in CTT it is easy to define a type for the greatest fixed point of a functor: \[ {{{\color{MidnightBlue}{ {\nu(T. F[T])} }}}\equiv{{\color{Maroon}{ {(\cap n\in {\mathbb{N}})\, {\mathsf{primRec}(n; {\mathsf{Top}}; \_, T. F[T])} } }}}}\]

In the above definition, \({\mathsf{Top}}\) is the type of all closed terms in the computation system, identified using the trivial relation (i.e. we have \({\vert_{x,y}\;{{{{\color{MidnightBlue}{x}}}={{\color{MidnightBlue}{y}}}\in{{\color{MidnightBlue}{{\mathsf{Top}}}}}}\ \ ({{{\color{MidnightBlue}{x}}}\in{{\color{MidnightBlue}{{\mathsf{Top}}}}}}, {{{\color{MidnightBlue}{y}}}\in{{\color{MidnightBlue}{{\mathsf{Top}}}}}})}}\)). Intuitively, the definition works by saying that a member of \({\nu(T. F[T])}\) must uniformly (simultaneously) witness \(F^n[T]\) for all \({{{\color{MidnightBlue}{n}}}\in{{\color{MidnightBlue}{{\mathbb{N}}}}}}\).

Now it is possible to define choice sequences as the greatest fixed point of the extension of the container \({e\in{\mathbb{E}}\triangleleft \pi(e)}\): \[ {{{\color{MidnightBlue}{ {\mathsf{cseq}}}}}\equiv{{\color{Maroon}{ {\nu(R. {(\Sigma e\in {\mathbb{E}})\, {\pi(e)\supset R} } )} }}}} \]

We can also define the “head” of a choice sequence and its “tail”, by appealing to the fact that canonical members of this type will be infinitely-nested pairs:

\[ {{{\color{MidnightBlue}{{\mathsf{head}(\alpha)}}}}\equiv{{\color{Maroon}{{\mathsf{fst}(\alpha)}}}}}\\ {{{\color{MidnightBlue}{{\mathsf{tail}(\alpha)[r]}}}}\equiv{{\color{Maroon}{{\mathsf{snd}(\alpha)}(r)}}}}\\ \]

As noted earlier, a choice sequence should be viewed as an infinite path in a spread, or as a member of the spread’s extension as a collection of ideal points. This metaphor keeps coming up again and again, that of an “ideal point”; it is at the heart of the intuitionistic conception of the continuum and the real numbers. Recall that the real numbers are constructed as converging choice sequences of rationals; a classical set of real numbers, then, might be recast intuitionistically as a spread, whose paths are choice sequences which each represent some real number.

Choice Sequences & Their Neighborhoods

For a choice sequence \({{{\color{MidnightBlue}{\alpha}}}\in{{\color{MidnightBlue}{{\mathsf{cseq}}}}}}\), we would like to express the property that some approximation \({{{\color{MidnightBlue}{u}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}}\) is a neighborhood around \(\alpha\). Ghani et al show how to do this, by first defining an operator that gives the choice sequences that \({{{\color{MidnightBlue}{u}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}}\) is a neighborhood of, indexed by refinement positions \({\pi^\natural(u)}\):

\[ {\dfrac{\matrix{ {{{\color{MidnightBlue}{\alpha}}}\in{{\color{MidnightBlue}{{\mathsf{cseq}}}}}} & {{{\color{MidnightBlue}{u}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}} }}{ {{{\color{MidnightBlue}{{\alpha[u]}}}}\in{{\color{MidnightBlue}{{{\pi^\natural(u)}\supset {\mathsf{cseq}}}}}}} }} \]

We explain this operator by observing its computational behavior on neighborhoods:

\[ {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\Rightarrow{{\color{Maroon}{{\langle\rangle}}}}} }}{ {{{\color{MidnightBlue}{{\alpha[u]}}}}\Rightarrow{{\color{Maroon}{{\lambda(\_. \alpha)}}}}} }} \qquad {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\Rightarrow{{\color{Maroon}{{v\frown r.e[r]}}}}} }}{ {{{\color{MidnightBlue}{ {\alpha[u]} }}}\Rightarrow{{\color{Maroon}{ {\lambda({\langle p_1 , p_2\rangle}. {\mathsf{tail}({\alpha[v]}(p_1))[p_2]} )} }}}} }} \]

What’s happening here? \({\alpha[u]}\) takes a refinement position \({{{\color{MidnightBlue}{r}}}\in{{\color{MidnightBlue}{{\pi^\natural(u)}}}}}\) and gives the choice sequence that \(u\) refined by \(r\) approximates. Now, we can use this to express the property that \(u\) is a neighborhood around some arbitrary \({{{\color{MidnightBlue}{\alpha}}}\in{{\color{MidnightBlue}{{\mathsf{cseq}}}}}}\), namely \({u\prec\alpha}\):

\[ {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\Rightarrow{{\color{Maroon}{{\langle\rangle}}}}} }}{ {{{\color{MidnightBlue}{{u\prec\alpha}}}}\Rightarrow{{\color{Maroon}{{\mathsf{unit}}}}}} }} \\[18pt] {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\Rightarrow{{\color{Maroon}{{v\frown r.e[r]}}}}} }}{ {{{\color{MidnightBlue}{ {u\prec\alpha} }}}\Rightarrow{{\color{Maroon}{ {v\prec\alpha} \times ({\mathsf{head}(\cdot)}\circ {v[\alpha]} = {\lambda(r. e[r])} \in {{\pi^\natural(v)}\supset {\mathbb{E}}}) }}}} }} \]

From these computation rules, we may justify that this is indeed a sensible relation: \[ {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}} & {{{\color{MidnightBlue}{\alpha}}}\in{{\color{MidnightBlue}{{\mathsf{cseq}}}}}} }}{ {{{\color{MidnightBlue}{{u\prec\alpha}}}}\in{{\color{MidnightBlue}{{\mathbb{U}_{i}}}}}} }} \]

The type of neighborhoods of a choice sequence is now easily defined using CTT’s set types:

\[ {{{\color{MidnightBlue}{ {\alpha^\natural} }}}\equiv{{\color{Maroon}{ {\{u\in {{\mathbb{E}}^\natural}\mid {u\prec\alpha}\}} }}}} \]

Using this, we may finally express the property that a choice sequence is in a spread: if all neighborhoods of a choice sequence are in a spread, then the choice sequence is in the spread. For a spread law \(\mathfrak{S}\):

\[ {{{\color{MidnightBlue}{\mathfrak{S}(\alpha)}}}\equiv{{\color{Maroon}{ {(\Pi u\in {\alpha^\natural})\, \mathfrak{S}(u) } }}}} \]

Bars and the Bar Induction Principle

Following Dummett, we say that a predicate \(\mathbf{R}\) on neighborhoods is a bar in case every choice sequence has a neighborhood \({{{\color{MidnightBlue}{u}}}\in{{\color{MidnightBlue}{{{\mathbb{E}}^\natural}}}}}\) such that \(\mathbf{R}(u)\):

\[ {{{\color{MidnightBlue}{ {\mathsf{isBar}(\mathbf{R})} }}}\equiv{{\color{Maroon}{ {(\Pi \alpha\in {\mathsf{cseq}})\, {\{u\in {\alpha^\natural} \mid \mathbf{R}(u) \}} } }}}} \]

A few other auxiliary definitions will come in handy shortly: \[ {{{\color{MidnightBlue}{ {\mathbf{P}\sqsubseteq \mathbf{Q}} }}}\equiv{{\color{Maroon}{ {(\Pi u\in {{\mathbb{E}}^\natural})\, {\mathbf{P}(u)\supset \mathbf{Q}(u)} } }}}}\\ {{{\color{MidnightBlue}{ {\mathsf{isHereditary}(\mathbf{A})} }}}\equiv{{\color{Maroon}{ {(\Pi u\in {{\mathbb{E}}^\natural})\, { ({(\Pi e\in {{\pi^\natural(u)}\supset {{\mathbb{E}}^\natural}})\, \mathbf{A}({u\frown r.e(r)}) }) \supset \mathbf{A}(u) } } }}}} \]

At this time, we have enough defined in order to express the Bar Induction principle \({\mathbf{BI}_\mathsf{D}}\) (the subscript \(\mathsf{D}\) indicates that this is the variant of \(\mathbf{BI}\) which presumes the decidability of the bar):

\[ {{{\color{MidnightBlue}{ {\mathbf{BI}_\mathsf{D}}[\mathbf{R},\mathbf{A}] }}}\equiv{{\color{Maroon}{ { ({\mathsf{decidable}(\mathbf{R})} \times {\mathsf{isBar}(\mathbf{R})} \times {\mathsf{isHereditary}(\mathbf{A})} \times {\mathbf{R}\sqsubseteq \mathbf{A}}) \supset \mathbf{A}({\langle\rangle}) } }}}} \]

Now, in computational type theory, it is possible to write a program which should realize \({\mathbf{BI}_\mathsf{D}}\), but is is not possible to prove that it is in fact such a realizer: intuitively, it is believable that the algorithm terminates, but this is not evident in type theory without further axioms. In order to prove \({\mathbf{BI}_\mathsf{D}}\), a leap of faith must be taken, where you postulate the evidence of a weaker principle \({\mathbf{BI}_\mathsf{D}^\mathsf{wk}}\) which only allows you to specify a motive \(\mathbf{A}(\cdot)\) which is computationally irrelevant. Then, using \({\mathbf{BI}_\mathsf{D}^\mathsf{wk}}\), it is possible to prove that the realizer you wrote down is indeed the realizer of the full \({\mathbf{BI}_\mathsf{D}}\) which we described above.

Note that postulating a weak induction principle that only allows computationally irrelevant motives does not risk destroying the computational content or canonicity of type theory, and so the only thing that is actually at risk is consistency. However, the full bar induction principle (even without presupposing the decidability of the bar) is true in classical mathematics, so it ought be consistent with intuitionistic type theory.

Once we have used the weak induction principle to prove that our recursive program realizes the strong induction principle, we may say that \({\mathbf{BI}_\mathsf{D}}\) is evident, since we know that it has a realizer. To learn more about this construction, see Mark Bickfords slides for the talk, Adding Bar Induction to Nuprl. The version of bar induction that has been added to Nuprl is less general than the one here, but the result should transfer to our setting as well (I conjecture).

Parting Thoughts

I have been wondering what this construction look like if it were generalized from containers to indexed containers or indexed induction-recursion codes… Would it be useful? Contact me if you have any ideas.

  1. Neil Ghani, Peter Hancock and Dirk Pattinson, 2009. Continuous Functions on Final Coalgebras.

  2. I am assured by Peter Dybjer that are no serious obstacles to adding induction-recursion to CTT.

  3. Giovanni Sambin, 2012. Real and Ideal in Constructive Mathematics.

  4. Michael Dummett, 2000. Elements of Intuitionism.

  5. Mark van Atten, 2003. On Brouwer (Wadsworth Philosphers).