Electronic Notes in Theoretical Computer Science 265 (2010) 437–451

[Link]/locate/entcs

Cartesian Monoids

Rick Statman1,2
Department of Mathematical Sciences
Carnegie Mellon University
Pittsburgh, PA 15213, USA

Abstract
The Cartesian monoid of partial piecewise shift operators is developed as a model for programming systems
such as Backus’ FP. Special attention is paid to those elements which are equationally implicitly definable.

Keywords: Cartesian monoids, arithmetical hierarchy.

1 Introduction
By the time he wrote his famous letter to Dedekind in 1877, Cantor probably knew
that a set with more than one element is infinite if and only if it supports a surjective
pairing function.
Here are six simple steps any mathematician following his nose might take:
• Begin with a Cantor algebra; a set together a with surjective pairing function.
• Add a monoid of functions to the Cantor algebra.
• Write down the axioms of a Cartesian monoid and construct the free model.
• Contemplate the “op” of the free model; the piecewise shift operators.
• Allow an undefined element; partial piecewise shift operators.
• Consider the algebraic elements.
Where are we? The hyperarithmetic hierarchy. We will elaborate below.
We are principally interested in the fundamental relationship between infinity
and computability. In particular, we want to suggest that if we accept the notion
of a completed infinity then certain computational structures are forced on us. The
1 The author would like to thank referee 1 for several useful remarks and suggestions
2 Email: statman@[Link]

1571-0661/$ – see front matter © 2010 Elsevier B.V. All rights reserved.
doi:10.1016/[Link].2010.08.026
438 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451

inevitability of these structures is described by the 6 steps above. We pay attention

to these structures because they follow the functional programming trend.
Functional programming and equational specification have their roots in the
ideas of Herbrand, Gödel, Church, Curry and Kleene carried up to the present. The
standard was articulated by Backus in his 1978 Turing award lecture:
“. . . a small framework which accommodates a great variety of powerful features
entirely as changeable parts.”
Here is a very simple framework. We will see that it accommodates a great
variety of powerful features as changeable parts.

2 The notion of Cartesian monoid

The notion of Cartesian monoid axiomatizes the idea of a monoid of functions on
a set S supporting a surjective pairing function S × S → S lifted pointwise to
(S → S) × (S → S) → (S → S). So a Cartesian monoid
C = (M, ∗, I, L, R,  )
is a monoid (M, ∗, I) together with elements L, R ∈ M and a map   : M ×M → M
satisfying
L ∗ F, G = F (left projection)
R ∗ F, G = G (right projection)
L, R = I (surjectivity)
F, G ∗ H = F ∗ H, G ∗ H (pointwise lifting)
These axioms can be found among the first few of Backus’ axioms for FP, but they
have a much longer history. The author is not a historian and the reader would be
well served to consider [8] page 118. Generally speaking the axioms of Cartesian
monoids have been regarded as too weak to be of use in logical type theory. However,
they have an interesting connection to word problems.

3 Background
In 1937 Church used the lambda calculus formulated as a monoid to prove the
undecidability of the word problem for semigroups. This was pursued by Curry and
Feys in their 1952 book on combinatory logic with the study of the B, I monoid.
This monoid turns out to be the “positive part” of Thompson’s group F , and
to generate this group. The group F turns out to be a subgroup of another of
Thompson’s groups V “the group” of the free Cartesian monoid. The free Cartesian
monoid is particularly important here because it is simple and embeds in every non-
trivial Cartesian monoid. Indeed, in 1965 Richard Thompson discovered a family of
peculiar groups in connection to his theorem characterizing the groups with solvable
word problems. The group F was rediscovered by Peter Freyd and Alex Heller in
1993 in connection with homotopy retracts x ∗ x ∼ x which do not split y ∗ z ∼ I
 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451 439

and x ∼ z ∗ y. It is clear that both collections of authors knew the monoid of

piecewise shift operators. This monoid is isomorphic to the free Cartesian monoid.
Lambek and Scott first defined the notion of a Cartesian monoid in 1980. Actually,
they defined the notion of a Cartesian category leaving the Cartesian monoids as
the degenerate ones with a single object. Clearly, both were aware of the existence
of the free Cartesian monoid (on 0 generators). Since the axioms of a Cartesian
monoid are given by identities we say it is an algebraic structure, but it is not of the
familiar kind such as groups, rings and fields. The reader should consult [8] pp. 93-
97 for some elementary properties. The homomorphism/quotient theory of monoids
is very complicated and not like the case of groups. Nevertheless, Cartesian monoids
are ubiquitous and can be amalgamated. N → N is a universal monoid into which
every countable Cartesian monoid can be embedded by Cayley’s argument. Cayley’s
argument can be summarized as follows. The Cartesian monoid as an algebra can
be realized on a set S. The operation  ,  yields a surjective pairing function on
that set. The monoid lifts to the set of functions S → S under composition by
Cayley’s trick of x → left multiplication by x, and  ,  lifts pointwise.
Each element of the free Cartesian monoid on 0 generators is denoted by an
expression in I, L, R,  , ∗ and each expression can be uniquely re-written in a
normal form consisting of a binary tree whose nodes correspond to applications of
  with strings of L’s and R’s at its leaves (here I counts as the empty string) and
no subexpressions of the form L ∗ x, R ∗ x (this is all modulo associativity; see
[12]).

4 TOPS and POPS

The “op” class of Cartesian monoids comes from taking sums instead of (Cartesian)
products. These are the piecewise shift operators defined on (open subsets of)
Cantor Space. Here we construe Cantor space as the product of {0, 1}, endowed with
the discrete topology, along the natural numbers. The properties of Cantor space
are very well known; in particular, it is a totally disconnected compact Hausdorff
space. Basic open neighborhoods are represented by binary sequences u so that
f ∈ u ⇐⇒ there exists g s.t. f = uˆg. Here we add a point at infinity, denoted
@, to Cantor space to get projective Cantor space. A map F : projective Cantor
space → projective Cantor space is said to be a piecewise shift operator if whenever
f ∈ Cantor space and F (f ) = @ there exist u, v finite binary sequences and a g ∈
Cantor space such that for all h ∈ Cantor space
(i) f = uˆg
(ii) F (f ) = vˆg
(iii) F (uˆh) = vˆh
440 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451

and of course F (@) = @. The set of piecewise shift operators form a Cartesian
monoid by
I(f ) = f
L(f ) = 0ˆf (0 shift)
R(f ) = 1ˆf (1 shift)
F, G(0ˆf ) = F (f ) (definition by cases)
F, G(1ˆf ) = G(f ) (definition by cases)
F ∗ G(f ) = G(F (f )).
If F is a piecewise shift operator let
dom(F ) = {f ∈ Cantor space | F (f ) = @}.
This makes dom(F ) an open subset of Cantor space and F |dom(F ) an open continu-
ous mapping of dom(F ) into Cantor space. When dom(F ) = Cantor space we say
that F is total. So we have two Cartesian monoids.
• Total Operators of Piecewise Shift (TOPS)
• Partial Operators of Piecewise Shift (POPS)
Since Cantor Space is compact (König’s lemma) each member of TOPS is deter-
mined by a finite binary tree with binary sequences at its leaves; it follows that
Theorem 4.1 TOPS is isomorphic to the free Cartesian monoid on 0 generators.

5 POPS
Members of the POPS monoid can be thought of as infinite binary trees with finite
strings of L’s and R’s at their leaves (here the empty string is I). For example,
the operator constantly @, also denoted @, is the complete binary tree with no
leaves (dom(@) = ∅; @ corresponds to the totally undefined partial map Cantor
space → Cantor space). Among the piecewise shift operators are the members of
the Thompson/Freyd-Heller group F generated by the operators An defined by

nˆ0ˆ0ˆa → nˆ0ˆ0ˆ0ˆa
nˆ0ˆ1ˆa → nˆ0ˆ0ˆ1ˆa
nˆ1ˆ0ˆa → nˆ0ˆ1ˆa
nˆ1ˆ1ˆa → nˆ1ˆa,
where we have identified the number n with the sequence of n 1’s. These operators
satisfy the interesting identity
An ∗ Am = Am+1 ∗ An
when m > n. The members U of POPS for which there is a solution to U ∗ x = I
are the (left) units of POPS. They are all members of TOPS and form a monoid
 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451 441

(not Cartesian, since I, I is not a unit).

If C is a Cartesian monoid then the polynomial Cartesian monoid
C[x1 , . . . , xn ]
is defined in the obvious way. Similarly for products, sums and all the normal
universal algebraic constructions. Among the univariate polynomials are the linear
ones (without nested indeterminates).
(i) If F ∈ C then F is linear (constant).
(ii) If F, G ∈ C then F ∗ x ∗ G is linear.
(iii) If p(x) and q(x) are linear then so is p(x), q(x).
If D is an extension of C then the element F of D is said to be algebraic over C if
it is the unique solution to a Cartesian monoid polynomial equation
p(x) = q(x)
with parameters from C. If an element Fj of D is one coordinate of the unique
solution (F1 , . . . , Fn ) to a Cartesian monoid polynomial equation p(x1 , . . . , xn ) =
q(x1 , . . . , xn ) with parameters from C then, by pairing, Fj lies in the sub-Cartesian
monoid generated by an algebraic element. We loosely call Fj algebraic as well.
More generally, the definition of algebraic is equivalent to saying that there is a
triple of univariate polynomials p(y), q(y), r(y) such that p(y) = q(y) has a unique
solution G and F = r(G). Clearly multiple equations can be combined into one by
pairing.
For an example consider the system E:
x = y∗z
y = R, y ∗ L
z = z ∗ R, L.
This has a unique solution in POPS
y = R, R ∗ L, . . . R ∗ L ∗ ∗ L ∗ L, . . . . . .
where y is undefined on the sequence constantly 1,
z = . . . . . ., L ∗ R ∗ ∗ R ∗ R . . ., L ∗ R, L
where z is undefined on the sequence constantly 0, and
x = L, L ∗ R, . . . L ∗ R ∗ ∗ R ∗ R, . . . . . ..
where x is like y (hint to the reader; to read these complex expressions first pair
the explicit parentheses  , ). This x is also a solution to
x = L, x ∗ R
but not the unique such solution since I is also a solution. All three can be obtained
as projections of the unique solution to the fixed point equation
u = L ∗ R ∗ u ∗ R ∗ R ∗ u, R, L ∗ R ∗ u ∗ L, R ∗ R ∗ u ∗ R, L.
Below in Section 6 we will present a representation of the set of natural numbers
in TOPS. Members of POPS induce partial functions from numbers to numbers
442 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451

on this representation, and a member of POPS which is a projection of the unique

solution to a fixed point equation induces a partial recursive function. It will follow
from the construction in Section 6 that every partial recursive function can be
obtained in this way.
Now any polynomial equation p(x) = q(x) which does not imply L = R has
a model (Cartesian monoid) with a recursively enumerable inequality relation by
adding the constant F and defining r(F ) # s(F ) ⇐⇒ there exists t(x) such that
t(r(F )) = L and t(s(F )) = R. By Cayley’s argument, as in Section 3, this model can
be embedded into the universal monoid and the members of the model are recursive
in the halting problem. So we can compute with equations, with no particular
semantics, with the expected degree of complexity.
Let C be a Cartesian monoid, P a set of univariate polynomials (possibly with
parameters from C) and D a subset of C. We define a relation  depending on
C, D and P by F  G ⇐⇒ whenever p(x) ∈ P and p(F ) ∈ D then p(G) = p(F ). 
is always a quasi order. Define F ∼ G ⇐⇒ F  G and G  F . If P is all univariate
polynomials with parameters from C, and D is a Cartesian sub-monoid of C, then
∼ is a congruence relation and {F/∼ | F ∈ C} is a Cartesian monoid, with the
attending homomorphism F → F/∼.
For some examples:
(i) C = TOPS, P = all univariate polynomials, and D = {L, R}. Then by [12]
F ∼ G ⇐⇒ F = G.
(ii) C = POPS, P = all linear polynomials, and D = TOPS. Then F ∼ G ⇐⇒
F = G.
We call this latter condition shiftiness; namely, for P = all linear polynomials, and
D = TOPS, if for all F, G
F ∼ G ⇐⇒ F = G
C is said to be shifty.
The significance of POPS in this respect is just

Theorem 5.1 If the Cartesian monoid C has the same monoid of left units as
TOPS then there is a homomorphism from C into POPS. Indeed any polynomial
equation solvable in C is solvable in POPS. If C is shifty then the homomorphism
is an embedding.

Proof. To each member of C we assign an infinite binary tree with finite strings of
L’s and R’s at its leaves (here the empty string is I). This determines a map into
POPS. This map can only fail to be a Cartesian monoid homomorphism if there
exist F, G ∈ C and a string s of L’s and R’s such that s ∗ F is not a member of
TOPS but s ∗ F ∗ G is a string of L’s and R’s, say t. Now t is right invertible, by
say r, but then
(s ∗ F ) ∗ (G ∗ r) = I
so s ∗ F is a left unit in C − TOPS.
 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451 443

Homomorphisms preserve equations but as alluded to above the homomorphism

theory of Cartesian monoids is complicated. The homomorphisms of POPS above
depend on sub-Cartesian monoids D of POPS of which there are many. A subset
S of Cantor space is said to be closed under shift if whenever uˆf ∈ S we have also
vˆf ∈ S. Examples are
(a) All f ultimately constant.
(b) All f ultimately constantly 0.
(c) All f of Turing degree > halting problem.
If S is closed under shift then the set of all piecewise shift operators F such that
S ∪ dom(f ) = Cantor Space
forms a Cartesian monoid. (b) is essentially the total piecewise shift operators on
Baire Space. In the case of (c), the recursive piecewise shift operators are all total
by König’s lemma. Thus they are essentially all finite automata. Looking at such
sub-Cartesian monoids led us to find a homomorphic image of POPS with a solution
to our example E above with x = I. Of course, such a Cartesian monoid has a larger
monoid of units than TOPS. 2

6 HYPE
Each member of POPS is an infinite automaton whose computing power is the
computational complexity of its tree. The algebraic ones are the ones uniquely
specifiable by an equation. The hyperarithmetical functions were first introduced
by Kleene in the 1960’s (although the terminology is apparently due to Hartley
Rogers) as a generalization of the notion of recursive function which allows infinite
terminating searches.

Theorem 6.1 The algebraic elements of POPS are precisely the ones with hyper-
arithmetic trees.

To prove that the algebraic elements of POPS have hyperarithmetic trees is

a routine coding argument with a theorem of Spector ([16] corollary XLIV(d)
page 424).
We now know two quite distinct proofs of ⇒. The first uses a representation
of recursive functions and the above result of Spector, and the second requires
doing bar recursion inside POPS. Bar recursion is recursion over well founded trees,
and is a natural extension of general recursion. Since both require representing
general recursion we have chosen to outline the second proof. Each proof provides
an equational specification for each hyperarithmetic function and a demonstration
that the function meets the specification.
We begin with some notation:
• X := Y means X is by definition equal to Y .
Here are some definitions of data structures. Along with these definitions come
444 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451

some easily verified properties.

(1) Booleans.
T := L
F := R
Boole := {L, R}.
Then
Not(x) = x ∗ R, L
And(x, y) = x ∗ y ∗ I, R, R.
(2) Strings.
I is the empty string
L, R are atomic strings
if s is a string then so are s ∗ L and s ∗ R.
(3) Simplices (complete binary trees with all leaves labeled with I).
Sim(0) := I
Sim(n + 1) := Sim(n), Sim(n)
Simplex := {Sim(n) | n = 0, . . .}
Then
Next(x) := x ∗ I, I
Prev(x) := R ∗ x.
(4) Natural Numbers.
0 := L
n := L ∗ Rn
Nat := {L, L ∗ R, L ∗ R ∗ R, . . .}
Then
Succ(x) = x ∗ R
Pred(x) = x ∗ L, I.
(5) Wreath Product with Nat.
An element f ∈ POPS defines a function (with the same name) with do-
main = the natural numbers, in other words a sequence, by
Apply(f, n) = L ∗ Rn ∗ f .
We shall write f (n) for Apply(f, n).
Seq(f ) := L ∗ f, L ∗ R ∗ f, . . . L ∗ R ∗ f, . . . . . ..
We write [f (n) | n = 0, 1, . . .] for Seq(f ).

Im(f ) := {L ∗ Rn ∗ f | n = 0, 1, . . .}
Seq(f ) may or may not be equal to f . For example, Seq(I) ∈ POPS − TOPS.
If b : N k → N then f represents b if n1 ∗ . . . ∗ nk ∗ f = b(n1 , . . . , nk ) for all
n1 , . . . , nk ∈ Nat.
 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451 445

Prefix(f, g) := [f (n) ∗ g(n) | n = 0, 1, . . .].

(6) A functional F defined on a subset of POPS is said to be algebraic if there
exist multivariate polynomials p(s, y, z), q(x, y, z) such that for each x in the
domain of F there exists unique y, z such that
p(x, y, z) = q(x, y, z)
and z = F (x).
We now need to show that some of the above defined concepts have algebraic
definitions. We have 10 small propositions (i)–(x).
(i) x ∈ Boole ⇐⇒ x ∗ I, I = I and Prev(Next(x ∗ I, I, I)) = x ∗ I, I, I.
Proof. ⇐. If x ∗ I, I = I then x is right invertible thus belongs to TOPS.
Indeed x can be written as a complete binary tree of depth n with each of the
2n strings of L’s and R’s (in lexicographic order) followed by a random L or R
at its leaves. We need to see that these are all L’s or all R’s. It suffices to show
that x ∗ I, I, I is a simplex, but this follows from the second equation. 2
(ii) x = [C | n = 0, 1, . . .] ⇐⇒ x = C, x.
Proof. ⇐. x = C, x has no solution in TOPS. The only possibility is C = L
and x = R but this yields I = R. 2
(iii) x = [Sim(n) | n = 0, 1, . . .] ⇐⇒ x = I, Next(x).
Here and below we write additional variables unquantified on the r.h.s. if when
such objects exist they must be unique.

(iv) x ∈ Nat ⇐⇒
x ∗ [I | n = 0, 1, . . .] = I and x = L ∗ y and R ∗ y = y ∗ R and
y ∗ x ∗ [Sim(n) | n = 0, 1, . . .] = I.
Proof. ⇐. Again x is right invertible so x belongs to TOPS. Similarly for y.
Thus, by [8], y = Rn for some n and thus x is a natural number. 2
(v) x ∈ Simplex ⇐⇒ y ∈ Nat and x = y ∗ [Sim(n) | n = 0, 1, . . .].
(vi) x = [n | n = 0, 1, . . .] ⇐⇒
y = R, y ∗ L and z = z ∗ R, L and x = y ∗ z.
(vii) Seq(y) is linear in y.
x = Seq(y) ⇐⇒ x = [n | n = 0, 1, . . .] ∗ y

The next 3 constructions are essential for what follows.

(viii) x = [[n ∗ m | n = 0, 1, . . .] | m = 0, 1, . . .] ⇐⇒
x = [n | n = 0, 1, . . .] ∗ L, x ∗ R.
(ix) x = [[n ∗ m | m = 0, 1, . . .] | n − 0, 1, . . .] ⇐⇒
y = [n | n = 0, 1, . . .], [R ∗ m | m = 0, 1, . . .] ∗ y and
x = [[L ∗ m ∗ n | n = 0, 1, . . .] | n = 0, 1, . . .] ∗ y.
 446 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451

(x) x = [n ∗ n | n = 0, 1, . . .] ⇐⇒
y = L, [R ∗ n | n = 0, 1, . . .] ∗ y ∗ R and
x = [L ∗ n | n = 0, 1, . . .] ∗ y.

Now, the next two are definitions.

(xi) x = Pre(y) ⇐⇒ x = [n ∗ n | n = 0, 1, . . .] ∗ [y ∗ n | n = 0, 1, . . .].

(xii) x = Pre(y, z) ⇐⇒ x = Pre(Pre(y) ∗ z),
where we may want to substitute Seq(x) for x on r.h.s. below, to allow members
of TOPS.

Next are two small propositions.

(xiii) Im(x) ⊆ Nat ⇐⇒

Pre(y) ∗ x ∗ [Sim(n) | n = 0, 1, . . .] = [I | n = 0, 1, . . .] and
y ∗ R = [R ∗ n | n = 0, 1, . . .] ∗ y and
x = [L ∗ n | n = 0, 1, . . .] ∗ y.
Similarly for Im(Im(x)) ⊆ Nat

(xiv) Im(x) ⊆ Boole ⇐⇒

x ∗ [I, I | n = 0, 1, . . .] = [I | n = 0, 1, . . .] and
[R ∗ n | n = 0, 1, . . .] ∗ Next(x ∗ I, I, I) = x ∗ I, I, I.
Similarly for Im(Im(x)) ⊆ Boole.

Next we turn our attention to representing recursive functions.

(7) Arithmetical Closure Properties.

For n1 , . . . , nk ∈ Nat
(a) Transportation
n1 ∗ . . . ∗ nk ∗ Prek (x) = x ∗ n1 ∗ . . . ∗ nk .
(b) Thinning
n1 ∗ . . . ∗ nk ∗ Prek−1 ([I | n = 0, 1, . . .]) ∗ x = n2 ∗ . . . ∗ nk ∗ x.
(c) Permutation

n1 ∗ . . . ∗ ni ∗ ni+1 ∗ . . . ∗ nk ∗
Pren−i−2 ([[n ∗ m | m = 0, 1, . . .] | n = 0, 1, . . .]) ∗ x
= n1 ∗ . . . ∗ ni+1 ∗ ni ∗ . . . ∗ nk ∗ x.
(d) Contraction

n1 ∗ . . . ∗ ni ∗ . . . ∗ nk ∗ Prek−i−1 ([n ∗ n | n = 0, 1, . . .]) ∗ x

= n1 ∗ . . . ∗ ni ∗ ni ∗ . . . ∗ nk ∗ x.
(8) Composition.
 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451 447

There exists X0 , . . . , Xk such that for all n1 , . . . , nk ∈ Nat

n1 ∗ . . . ∗ nk ∗ X0 ∗ x1 ∗ X1 ∗ . . . ∗ xk ∗ Xk ∗ y
= n1 ∗ . . . ∗ nk ∗ (n1 ∗ . . . ∗ nk ∗ x1 ) ∗ . . . ∗ (n1 ∗ . . . ∗ nk ∗ xk ) ∗ y,
provided that n1 ∗ . . . ∗ nk ∗ xi ∈ Nat, i = 1 . . . k − 1. Set
Comp(x1 , . . . , xk , y) := X0 ∗ x1 ∗ X1 ∗ . . . ∗ xk ∗ Xk ∗ y.
(9) Primitive Recursion. Let
x = L, [n + 1 | n = 0, 1, . . .] ∗ y, L, I ∗ Comp(x, z)
provided for all n1 , . . . , nk , n, m ∈ Nat we have n1 ∗ . . . ∗ nk ∗ y ∈ Nat and
n1 ∗ . . . ∗ nk ∗ n ∗ m ∗ z ∈ Nat, then we have
n1 ∗ . . . ∗ nk ∗ 0 ∗ x = n1 ∗ . . . ∗ nk ∗ y,
n1 ∗ . . . ∗ nk ∗ (n + 1) ∗ x = n1 ∗ . . . ∗ nk ∗ n ∗ (n1 ∗ . . . ∗ nk ∗ n ∗ x) ∗ z.
We assume that finite sequences n1 , . . . , nk of natural numbers have been coded
as natural numbers
n1 , . . . , nk 
with the coding satisfying the following:
(a) The empty sequence   is coded by 0.
(b) The functions
suffix(n1 , . . . , nk , nk+1 ) = n1 , . . . , nk , nk+1 
prefix(n1 , . . . , nk , n0 ) = n0 , n1 , . . . , nk 
are both primitive recursive.
(c) Moreover, there is a primitive recursive function enum such that
enum(e, b1 , . . . , bk ) = 1
if the eth Turing machine halts in at most k steps when applied to e using
the Oracle with initial segment encoded by the bit string b1 . . . bk and never
querying any integer > k, and
enum(e, b1 , . . . , bk ) = 0
otherwise.
(10) Course of Values Recursion.
A definition:
y = Course(x) ⇐⇒ y = 0 ∗ x, R ∗ [n ∗ n ∗ x | n = 0, 1] ∗ Suffix ∗ y
(11) General Recursion (minimization).
Suppose that for all n1 , . . . , nk , n, m ∈ Nat,
n1 ∗ . . . ∗ nk ∗ m ∗ n ∗ u ∈ Nat.
Then by the above there is an algebraic definition D[u, v, y] such that D[u, v, y]
has a unique solution and for all n1 , . . . , nk , n, m,
⎧
⎪
⎪
⎨0 if there exists l < m + 1 such that
n1 ∗ . . . ∗ nk ∗ m ∗ n ∗ y = n1 ∗ . . . ∗ n k ∗ l ∗ n ∗ u = 0
⎪
⎪
⎩ m + 2 else.
448 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451

Now assume that for all n there exists m such that n1 ∗ . . . ∗ nk ∗ m ∗ n ∗ u = 0

then
x = min{m | n1 ∗ . . . ∗ nk ∗ m ∗ n ∗ u = 0}
⇐⇒ D[u, v, y] and
x = 0 ∗ [[n ∗ m | n = 0, 1, . . .] | m = 0, 1, . . .] ∗ z and
z = Pre(y, [[n ∗ m | n = 0, 1, . . .] | m = 0, 1, . . .]) ∗
[n ∗ L | n = 0, 1, . . .], [[n ∗ m | n = 0, 1, . . .] | m = 0, 1, . . .] ∗ z ∗ R

Proposition 6.2 Suppose that a, b : N k → N and f, g represent resp. a, b. If a

is general recursive in b then there exists an algebraic definition D[u, v, w] with a
unique solution when u = g and in this solution w = f .

Remark: It is clear that D[u, v, w] in the proposition does not depend on b but
only on the general recursive functional F such that F (b) = a.

To obtain all hyperarithmetic functions we need to be able to iterate the jump

operation along arbitrary recursive well orderings. The meaning of “iterate” will be
explained in more detail in (13). First, the arithmetical quantifier.
(12) Universal Quantifier.
Another definition
x = Uni(y)
⇐⇒ Im(x) ⊆ Boole and
Im(Im(y)) ∈ Boole and
x ∗ y, [[L | n = 0, 1, . . .] | n = 0, 1, . . .]
= [[L | n = 0, 1, . . .] | n = 0, 1 . . .] and
z = [[m ∗ y ∗ (n + 1) ∗ m ∗ z ∗ R, L | n = 0, 1, . . .] | m = 0, 1, . . .] and
Im([m ∗ x ∗ 0, 0 ∗ m ∗ z | m = 0, 1, . . .]) ⊆ Nat,
so n ∗ x = L ⇐⇒ for all m, m ∗ n ∗ y = L.
(13) Jump Operation.
Another definition
x = Jump(y)
⇐⇒ z = y ∗ 0, 1 and
.
x = Uni([[n ∗ m | n = 0, 1, . . .] | m = 0, 1 . . .] ∗ Course(z) ∗ enum)
∗ R, L

Proposition 6.3 Suppose that a, b : N k → N and f, g represent resp. a, b. If a is

arithmetical in b then there exists an algebraic definition D[u, v, w] with a unique
solution when u = g and in this solution w = f .
 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451 449

Remark: It is clear that D[u, v, w] in the proposition does not depend on b but
only on the arithmetical functional F such that F (b) = a.

(14) Bar Recursion.

A mapping T from finite sequences of natural numbers to Boolean values is
a well founded tree if
(i) T (n1 , . . . , nk ) = true ⇒ T (n2 , . . . , nk ) = true,
(ii) for all functions b : N → N there exists k such that T (b1 , . . . , bk ) = false.
If T is a well founded tree then the well founded tree T @ n1 , . . . , nk is
defined by T @ n1 , . . . , nk (s) = T (n1 , . . . , nk , s) for any sequence s of natural
numbers.
The iteration of the jump operation along the well founded tree T , here
denoted J(T ), is defined recursively by
• T (n1 , . . . , nk ) = false ⇒ J(T @ n1 , . . . , nk )) = { }.
• T (n1 , . . . , nk ) = true ⇒ J(T @ n1 , . . . , nk ) = the halting problem relative
to the set of all pairs (m, n) s.t. m ∈ T @ n1 , . . . , nk , n.
Suppose that f ∈ POPS represents a well founded tree; that is
(a) f is Boolean valued;
(b) n1 , . . . , nk  ∗ f = L ⇒ n2 , . . . , nk  ∗ f = L;
(c) n1 , . . . , nk  ∗ f = R ⇒ for all n0 ,
n0 , n1 , . . . , nk  ∗ f = R;
(d) for all functions b : N → N there exists k such that
b1 , . . . , bk  ∗ f = R.
With f = y then a solution x to
x = [n ∗ n | n = 0, 1, . . .] ∗ y ∗ [[L | n = 0, 1, . . .] | n = 0, 1, . . .], suffix ∗ x
and
suffix ∗ x = Jump(suffix ∗ suffix ∗ x)
represents the iteration of the jump operation over the well founded tree rep-
resented by f .

Proposition 6.4 Suppose that a, b : N k → N and f, g represent resp. a, b. If a

is hyperarithmetical in b then there exists an algebraic definition D[u, v, w] with a
unique solution when u = g and in this solution w = f .

It remains to show that we can pass from the coding of a tree as a number
theoretic function to the tree itself, but this is straightforward. This completes the
proof.

7 Future Developments
In the future we would like to develop new methods to prove that certain systems of
polynomial equations have unique solutions. The Banach fixed point theorem can
be useful if one can formulate the problem as a fixed point equation for a mapping
450 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451

contractive in a convenient complete metric space. For example, for F, G ∈ POPS

define d(F, G) = the smallest natural number n such that there is a string s of L’s
and R’s, strung by ∗, of length n such that s ∗ F or s ∗ G is such a string of L’s
and R’s and s ∗ F and s ∗ G are distinct. Under the usual tree topology POPS is a
complete metric space with distance measure
m(F, G) = 2−d(F,G) .
Here the mapping t(y) = R, y ∗ L is contractive with Lipschitz constant 1/2.
On the other hand it is not obvious how to do this with u below E above.
By the main theorem above and another theorem of Spector the problem of
determining whether a given Cartesian monoid polynomial equation has a unique
solution in POPS is equivalent to the problem of deciding whether a given Π11
sentence is true. So in the general case we cannot do better than recursive in
Kleene’s set of ordinal notations O.
In contrast to Klop’s famous counter-example to the Church-Rosser theorem
for lambda calculus with the vanilla reduction rules for surjective pairing, there
are recent positive Church-Rosser results for combinatory logic with several strong
forms of SP ([13,14]). These should carry over to a re-write version of the theory of
Cartesian monoids supplemented by a finite number of given (but not necessarily
unique) solutions to fixed point equations. It remains to see how much of the
reduction theory of combinatory logic carries over to this context.

8 Conclusion
After taking our 6 steps we conclude that the axioms of Cartesian monoids provide
us with a concise mathematical description of a model of computation; a description
which is useful for proving facts about the model. This model is oriented toward
a functional style of programming (variable free) and provides a useful algebra of
programs. It is of great interest to learn how to reason productively about these
structures. We remark here that, in addition, state transitions and storage can be
included through Backus’ AST approach. The objects in the free model and its
generalizations behave like finite automata which can write (we call these “literate
finite state machines”) adding further state transitions. These will be discussed at
a later date.

References
[1] Backus, Can programming be liberated from the von Neumann style?, Communications of A.C.M.,
21(8) (1978), 613–641.

[2] Belk, “Thompson’s Group F”, Cornell University, Department of Mathematics, Ph.D. thesis, 2004.

[3] Cannon, Floyd, and Parry, Introductory notes on Richard Thompson’s groups, L’Enseignement
Mathematique, 42 (1996), 215–256.

[4] Curien, “Categorical Combinators, Sequential Algorithms, and Functional Programming”, Pittman,
1986.
 R. Statman / Electronic Notes in Theoretical Computer Science 265 (2010) 437–451 451

[5] Freyd, Heller, Splitting homotopy idempotents II, Journal of Pure and Applied Algebra, 89 (1993),
93–195.

[6] Kleene, “Turing machine computable functionals of finite types I in Logic, Methodology, and the
Philosophy of Science”, Proceedings of the 1960 International Congress, Stanford University Press,
(1962), 38–45.

[7] Lambek, From lambda calculus to Cartesian closed categories, in Seldin and Hindley eds., To H.B.
Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Academic Press, 1980.

[8] Lambek and Scott, “Introduction to Higher Order Categorical Logic”, Cambridge University Press,
1986.

[9] Scott, Relating theories of the lambda calculus, in Seldin and Hindley eds., To H.B. Curry: Essays on
Combinatory Logic, Lambda Calculus, and Formalism, Academic Press, 1980.

[10] Statman, Combinators and the theory of partitions, CMU Department of Mathematics Research Report
88-31, 1988.

[11] ——— Simply typed lambda calculus with surjective pairing, CMU Department of Mathematics
Research Report 92-164, 1992.

[12] ——— On Cartesian monoids, CMU Department of Mathematics Research Report 96-188, 1996.
Appeared in Proceedings of CSL 1996. Springer Lecture Notes in Computer Sciences, 1258. Springer-
Verlag, 1996, pp 446–459.

[13] ——— Surjective pairing revisited in Klop, van Oostrom, and van Raamsdonk eds., Liber Amicorum
for Roel deVrijer, University of Amsterdam, 2009.

[14] Stovring, Extending the extensional lambda calculus with surjective pairing is conservative, LMCS, 2
(2006), 1–14.

[15] Thompson, Embeddings into finitely generated simple groups which preserve the word problem, in Adian,
Boone, and Higman eds., The Word Problem II, Studies in Logic and the Foundation of Mathematics,
North Holland, 95 (1980), 401–441.

[16] ——— Theory of Recursive Functions and Effective Computability, MIT Press, 1987.