Binary Tree Arithmetic with Generalized Constructors

arXiv:1301.0128v1 [cs.MS] 1 Jan 2013

Abstract
We describe arithmetic computations in terms of operations on
some well known free algebras (S1S, S2S and ordered rooted
binary trees) while emphasizing the common structure present in
all them when seen as isomorphic with the set of natural numbers.
Constructors and deconstructors seen through an initial algebra
semantics are generalized to recursively defined functions obeying
similar laws. Implementations using Scala’s apply and unapply
are discussed together with an application to a realistic arbitrary
size arithmetic package written in Scala, based on the free algebra
of rooted ordered binary trees, which also supports rational number
operations through an extension to signed rationals of the CalkinWilf bijection.
Categories and Subject Descriptors D.3.3 [PROGRAMMING
LANGUAGES]: Language Constructs and Features—Data types
and structures
General Terms Algorithms, Languages, Theory
Keywords arithmetic computations with free algebras, generalized constructors, declarative modeling of computational phenomena, bijective Gödel numberings and algebraic datatypes, CalkinWilf bijection between natural and rational numbers

1.

Introduction

Classical mathematics frequently uses functions defined on equivalence classes (e.g. modular arithmetic, factor objects in algebraic
structures) provided that it can prove that the choice of a representative in the class is irrelevant.
On the other hand, when working with proof assistants like
Coq [9], based on type theory and its computationally refined
extensions like the Calculus of Construction [4], one cannot avoid
noticing the prevalence of data types corresponding to free objects,
on top of which everything else is built in the form of canonical
representations.
Category-theory based descriptions of Peano arithmetic fit naturally in the general view that data types are initial algebras - in
this case the initial algebra generated by the successor function, as
a provider of the canonical representation of natural numbers. Of
course, a critical element in choosing such free algebras is computational efficiency of the operations one wants to perform on them,
in terms of low time and space complexity. For instance Coq formalizations of natural numbers typically use binary representations

Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
for profit or commercial advantage and that copies bear this notice and the full citation
on the first page. To copy otherwise, to republish, to post on servers or to redistribute
to lists, requires prior specific permission and/or a fee.
Copyright c ACM . . . $10.00

while keeping the Peano arithmetic view when more convenient in
proofs [9]. Note also that free algebras corresponding to one and
two successor arithmetic (S1S and S2S) have been used as a basis
for decidable weak arithmetic systems like [2] and [11]. It has been
shown recently in [16, 17] that the initial algebra of ordered rooted
binary trees corresponding to the language of Gödel’s System T
types [7] can be used as a the language of arithmetic representations, with hyper-exponential gains when handling numbers built
...2

from “towers of exponents” like 22 . Independently, this view is
confirmed by the suggestion to use λ-terms as a form of universal
data compression tool [8] and by deriving bijective encodings of
data types using a game-based mechanism [18].
These results suggest a free algebra based reconstruction of
fundamental data types that are relevant as building blocks for
finite mathematics and computer science. We will sketch in this
paper an (elementary, not involving category theory) foundation for
arithmetic computations with free algebras, in which construction
of sets, sequences, graphs, etc. can be further carried out along the
lines of [14, 15, 17].
The paper is organized as follows. We define in section 2 isomorphisms between the free algebras of signatures consisting of
one constant and respectively, of one successor (S), two successors
(O and I) and a free magma constructor (C).
To enable computations with the objects of the free algebras,
we discuss the use of generalized constructors / destructors derived
from these free algebras using the apply / unapply constructs available in Scala (section 3). As an application, a complete arbitrary
size rational arithmetic package using the Calkin-Wilf bijection between positive rationals and natural numbers is described in section
4. Sections 5 and 6 discuss related work and our conclusions.

2.

Free Algebras and Data Types

D EFINITION 1. Let σ be a signature consisting of an alphabet of
constants (called generators) and an alphabet of function symbols
(called constructors) with various arities. We define the free algebra
Aσ of signature σ inductively as the smallest set such that:
1. if c is a constant of σ then c ∈ Aσ
2. if f is an n-argument function symbol of σ, then ∀i, 0 ≤ i <
n, ti ∈ Aσ ⇒ f (t0 , . . . , ti , . . . , tn−1 ) ∈ Aσ .
We will write c/0 for constants and f/n for function symbols with
n arguments belonging to a given a signature.
More general definitions, e.g. as initial objects in the category of
algebraic structures, are also used in the literature and a close relation exists with term algebras distinguishing between function constructors (generating the Herbrand Universe) and predicate constructors (generating the Herbrand Base).
Recursive data types in programming languages like Haskell,
ML, Scala can be seen as a notation for free algebras. We refer to
[19] for a clear and convincing description of this connection.
For instance, the Haskell declarations

data AlgU = U | S AlgU
data AlgB = B | O AlgB | I AlgB
data AlgT = T | C AlgT AlgT

correspond, respectively to
• the free algebra AlgU with a single generator U and unary

constructor S (that can be seen as part of the language of Peano
or Robinson arithmetic, or the decidable (W)S1S system, [2])
• the free algebra AlgB with single generator B and two unary

constructors O and I (corresponding to the language of the
decidable system (W)S2S [11]), as well as “bijective base-2”
number notation [20]
• the free algebra AlgT with single generator T and one binary

constructor C (essentially the same thing as the free magma
generated by T ).
The set-theoretical construction corresponding to the “|” operation
is disjoint union and the data types correspond to infinite sets generated by applying the respective constructors repeatedly. The settheoretical interpretation of “self-reference” in such data type definitions can be seen as fixpoint operation on sets of natural numbers
as shown in the P ω construction used by Dana Scott in defining the
denotational semantics for various λ-calculus constructs [13].
We will next “instantiate” some general results to make the underlying mathematics as elementary and self-contained as possible.
While category theory is frequently used as the mathematical backing for data-types, we will provide here a simple set theory-based
formalism, along the lines of [1].
We will start with the elementary mathematics behind the AlgT
data type and follow with an outline for a similar treatment of AlgU
and AlgB.

Note that this property corresponds of the initial algebra [19]
view of the corresponding (ordered, rooted) binary tree data type.
D EFINITION 5. If u : X → Y , we denote M (u) : M (X) →
M (Y ) the unique morphism of magmas defined by the construction
in Proposition 1.
If v : Y → Z then the morphism M (v) ◦ M (u) extends v ◦ u :
X → Z and therefore M (v) ◦ M (u) = M (v ◦ u).
P ROPOSITION 2. If u : X → Y is respectively injective, surjective, bijective then so is M (u).
It follows that
P ROPOSITION 3. If X = {x} and Y = {y} and u : X → Y is
the bijection such that f (x) = y, then M (u) : M (X) → M (Y )
is a bijective morphism (i.e. an isomorphism) of free magmas.
Proof If X is empty so is M (X), hence u is injective. If u is injective, then ∃u0 : Y → X, u0 ◦ u = id M (X) where id M (X)
denotes the identity mapping of M (X). Then M (u0 ) ◦ M (u) =
M (u0 ◦ u) = id M (X) and hence M (u) is injective. If u is surjective, then ∃u0 : Y → X, u ◦ u0 = id M (Y ) . Then M (u) ◦ M (u0 ) =
M (u ◦ u0 ) = id M (Y ) and hence M (u) is surjective. If u is bijective, than it is injective and surjective and so is M (u).
We will identify the data type AlgT with the free magma generated by the set {T} and denote its binary operation x ∗ y as C x y.
It corresponds to the free algebra (that we will also denote AlgT)
defined by the signature {T/0, C/2}.
We can now instantiate the results described by the previous
propositions to AlgT:

D EFINITION 2. A set M with a (total) binary operation ∗ is called
a magma.

P ROPOSITION 4. Let X be an algebra defined by a constant t and
a binary operation c. Then there’s a unique morphism f : AlgT →
X that verifies
f (T ) = t
(1)

D EFINITION 3. A morphism between two magmas M and M 0 is a
function f : M → M 0 such that f (x ∗ y) = f (x) ∗ f (y).

f (C(x, y)) = c(f (x), f (y))
Moreover, if X is a free algebra then f is an isomorphism.

Let X be a set. We define the sets Mn (X) inductively as
follows: M1 (X) = X and for n > 1, Mn (X) is the disjoint union
of the sets Mk (X) × Mn−k (X) for 0 < k < n. Let M (X) be
the disjoint union of the family of sets Mn (X) for n > 0. We
identify each set Mn with its canonical image in M (X). Then for
w ∈ Mn (X), we call n the length of w and denote it l(w). Let
w, w0 ∈ M (X) and let p = l(w) and q = l(w0 ). The image of
(w, w0 ) ∈ Mp × Mq under the canonical injection in M (X) is
called the composition of w and w0 and is denoted w ∗ w0 .
When X = {T } where T is interpreted as the “empty” leaf
of ordered rooted binary trees, the elements of Mn can be seen as
ordered rooted binary trees with n leaves while the composition
operation “∗” represents joining two trees at their roots to form a
new tree.

Proof It follows from Proposition 2 and equation f (T ) = t, given
that f is a bijection between the singleton sets {T} and {t}.

2.1

The free magma of ordered rooted binary trees with
empty leaves

D EFINITION 4. The set M (X) with the composition operation
(w, w0 ) → w ∗ w0 is called the free magma generated by X.
P ROPOSITION 1. Let M be a magma. Then every mapping u :
X → M can be extended in a unique way to a morphism of M (X)
into M .
Proof We define inductively the mappings fn : Mm (X) → M
as follows: For n = 1, f1 = f . For n > 1, ∀p ∈ {1, .., n −
1}, fn (w ∗ w0 ) = fp (w) ∗ fn−p (w0 ). Let g : M (X) → M such
that ∀n > 0, ∀x ∈ Mn (X), g(x) = fn (x). Then g is the unique
morphism of M (X) into M which extends f.

2.2

(2)

The One Successor and Two Successors Free Algebras

The one successor free algebra (also known as unary natural numbers or Peano algebra, as well as the language of the monoid {0}∗
and the decidable systems WS1S and S1S) is defined by the signature {U/0, S/1}, where U is a constant (seen as zero) and S is
the unary successor function. We will denote AlgU this algebra and
identify it with its corresponding data type.
We state an analogue of Proposition 4 for the free algebra AlgU.
P ROPOSITION 5. Let X be an algebra defined by a constant u and
a unary operation s. Then there’s a unique morphism f : AlgU →
X that verifies
f (U ) = u
(3)
f (S(x)) = s(f (x))
Moreover, if X is a free algebra then f is an isomorphism.

(4)

Note that following the usual identification of data types and initial
algebras, AlgU corresponds to the initial algebra “1 + ” through
the operation g =<U,S> seen as a bijection g : 1 + N → N.
The two successor free algebra (also known as bijective base2 natural numbers or Peano algebra, as well as the language of
the monoid {0, 1}∗ and the decidable systems WS2S and S2S ) is

defined by the signature {B/0, O/1, I/1} where B is a constant
(seen as the empty sequence) and O, I are two unary successor
functions. We will denote AlgB this algebra and identify it with its
corresponding data type.
We can state an analogue of Proposition 4 for the free algebra
AlgB.
P ROPOSITION 6. Let X be an algebra defined by a constant b
and a two unary operations o, i. Then there’s a unique morphism
f : AlgB → X that verifies
f (B) = b

(5)

f (O(x)) = o(f (x))

(6)

f (I(x)) = i(f (x))
Moreover, if X is a free algebra then f is an isomorphism.

(7)

These observations suggest that for defining isomorphisms between AlgU, AlgB and AlgT that enable a complete set of equivalent arithmetic (and later set-theoretic) operations on each of them,
we will need a mechanism to prove such equivalences. To this end,
it will be enough to prove that such non-constructor operations also
form free algebras of matching signatures.
We will call terms the elements of our initial algebras.

3.

case C(T, T) ⇒ T
case C(T, y) ⇒ d(y)
case z
⇒ C(T, p(h(z)))
}

Note the predecessor function called p and our auxiliary functions
named d (which “doubles” its input, assumed different from T) and
h (which “halves” its input, assumed “even” and different from T).
def d(z: AlgT): AlgT = z match {
case C(x, y) ⇒ C(s(x), y)
}
def h(z: AlgT): AlgT = z match {
case C(x, y) ⇒ C(p(x), y)
}
}

We will define our generalized constructor/destructor S representing the successor function and predecessor function on
rooted ordered binary trees of type AlgT by providing apply and
unapply methods expressed in terms of our “real” constructors T
and C and the actual algorithms defined in the (shared) trait AlgT.
object S extends AlgT {
def apply(x: AlgT) = s(x)
def unapply(x: AlgT) = x match {
case C(_, _) ⇒ Some(p(x))
case T
⇒ None
}

Generalized Constructors

The iso-functors supporting the equivalence between actual constructors and their recursively defined function counterparts suggest exploring programming language constructs that treat them in
a similar way. For instance it makes sense to extend “constructoronly benefits” like pattern matching to their function counterparts.
Fortunately, constructors/deconstructors generalized to arbitrary functions are available in Scala through apply/unapply
methods and in Haskell through a special notation implementing views, under the implicit assumption that they define inverse
operations.
One can immediately notice that our free algebras provide sufficient conditions under which this assumption is enforced. This
suggests the possibility that such generalized constructor/deconstructor pairs could provide the combined benefits of pattern matching and data abstraction, with the implication that direct syntactic
support for such constructs can bring significant expressiveness to
functional programming languages.
3.1

Generalized Constructors with apply/unapply in Scala

Besides supporting case classes and case objects that are
used (among other things) to implement pattern matching, Scala’s
apply and unapply methods [5, 10] allow definition of customized constructors and destructors (called extractors in Scala).
We will next describe how arithmetic operations with our AlgT
terms, represented as ordered rooted binary trees, can benefit from
the use such “generalized constructors”.
Our AlgT free algebra will correspond in Scala to a case
object / case class definition, combined with a mechanism
to share actual code, encapsulated in the AlgT trait.
case object T extends AlgT
case class C(l: AlgT, r: AlgT) extends AlgT
trait AlgT {
def s(z: AlgT): AlgT = z match {
case T
⇒ C(T, T)
case C(T, y) ⇒ d(s(y))
case z
⇒ C(T, h(z))
}

}

The definition of the generalized constructor/destructor D representing double / half is similar. Note the use of the method d defined
in the trait AlgT.
object D extends AlgT {
def apply(x: AlgT) = d(x)
def unapply(x: AlgT) = x match {
case C(C(_, _), _) ⇒ Some(h(x))
case _
⇒ None
}
}

The definition of the generalized constructor/destructor O can be
seen as corresponding to λx.2x + 1 and its inverse.
object O extends AlgT {
def apply(x: AlgT) = C(T, x)
def unapply(x: AlgT) = x match {
case C(T, b) ⇒ Some(b)
case _
⇒ None
}
}

The definition of the generalized constructor/destructor O can be
seen as corresponding to λx.2x + 2 and its inverse. Note the use
of the generalized constructors S, D and O, both on the left and
right side of match statements, illustrating their usefulness both
as constructors and as extractors.
object I extends AlgT {
def apply(x: AlgT) = S(O(x))
def unapply(x: AlgT) = x match {
case D(a) ⇒ Some(p(a))
case _
⇒ None
}
}

def p(z: AlgT): AlgT = z match {

3.2

A Scala-based Natural Number Arithmetic Package
using AlgT Terms

We will now illustrate how the use of generalized constructors helps
writing a fairly complete set of arithmetic algorithms on therms
of AlgT seen as natural numbers. For comparison purposes, the
reader might want to look at the Haskell code in [17] where similar algorithms are expressed using a type class-based mechanism.
However, while the use of type classes comes with the benefits of
data abstraction it needs separate functions for constructing, deconstructing and recognizing terms to express the equivalent of the
generalized constructors used here.
We start with a comparison function returning LT, EQ, GT and
supporting a total order relation on AlgT, isomorphic to the one
on N. Note here the use of the generalized constructors O and I
providing a view of the terms of AlgT as terms of the free algebra
BinT.
trait Tcompute extends AlgT {
def cmp(u: AlgT, v: AlgT): Int = (u, v) match {
case (T, T)
⇒ EQ
case (T, _)
⇒ LT
case (_, T)
⇒ GT
case (O(x), O(y)) ⇒ cmp(x, y)
case (I(x), I(y)) ⇒ cmp(x, y)
case (O(x), I(y)) ⇒ strengthen(cmp(x, y), LT)
case (I(x), O(y)) ⇒ strengthen(cmp(x, y), GT)
}

}
}

Similarly, a constant time complexity definition is given here for
the exponent of 2 operation, by using the “real” constructor C.
def exp2(x: AlgT) = C(x, T)

The power operation pow takes advantage of the generalized constructors O and I on the left side of a case statement through the
AlgB view of AlgT.
def pow(u: AlgT, v: AlgT): AlgT = (u, v) match {
case (_, T)
⇒ C(T, T)
case (x, O(y)) ⇒ multiply(x, pow(multiply(x, x), y))
case (x, I(y)) ⇒ {
val xx = multiply(x, x)
multiply(xx, pow(xx, y))
}
}

Efficient division with remainder is a slightly more complex algorithm, where we take advantage of generalized constructors, direct
inheritance from trait AlgT as well as number of previously defined
functions:
def div_and_rem(x: AlgT, y: AlgT): (AlgT, AlgT) =
if (cmp(x, y) == LT) (T, x)
else if (T == y) null // division by zero
else {
def try_to_double(x:AlgT, y:AlgT, k:AlgT): AlgT =
if (cmp(x, y) == LT) p(k)
else try_to_double(x, D(y), S(k))

val LT = -1
val EQ = 0
val GT = 1
private def
rel match
case EQ
case _
}

def divstep(n: AlgT, m: AlgT): (AlgT, AlgT) = {
val q = try_to_double(n, m, T)
val p = multiply(exp2(q), m)
(q, sub(n, p))
}
val (qt, rm) = divstep(x, y)
val (z, r) = div_and_rem(rm, y)
val dv = add(exp2(qt), z)
(dv, r)

strengthen(rel: Int, from: Int) =
{
⇒ from
⇒ rel

Addition is expressed compactly in terms of the generalized constructors O, I and S.
def add(u: AlgT, v:
case (T, y)
case (x, T)
case (O(x), O(y))
case (O(x), I(y))
case (I(x), O(y))
case (I(x), I(y))
}

AlgT): AlgT = (u, v) match {
⇒ y
⇒ x
⇒ I(add(x, y))
⇒ O(S(add(x, y)))
⇒ O(S(add(x, y)))
⇒ I(S(add(x, y)))

The definition of subtraction is similar, except that the code of the
predecessor function p is conveniently inherited directly from the
trait AlgT, given that the trait Tcompute extends it.
def sub(u: AlgT, v:
case (x, T)
case (O(x), O(y))
case (O(x), I(y))
case (I(x), O(y))
case (I(x), I(y))
}

AlgT): AlgT = (u, v) match {
⇒ x
⇒ p(O(sub(x, y)))
⇒ p(p(O(sub(x, y))))
⇒ O(sub(x, y))
⇒ p(O(sub(x, y)))

The multiplication operation is similar to the Haskell code in section ??, except for the use of the generalized constructor O.
def multiply(u: AlgT, v: AlgT): AlgT = (u, v) match {
case (T, _) ⇒ T
case (_, T) ⇒ T
case (C(hx, tx), C(hy, ty)) ⇒ {
val v = add(tx, ty)
val z = p(O(multiply(tx, ty)))
C(add(hx, hy), add(v, z))

}

Division and reminder can be separated using Scala’s projection
functions:
def divide(x: AlgT, y: AlgT) = div_and_rem(x, y)._1
def reminder(x: AlgT, y: AlgT) = div_and_rem(x, y)._2

Finally, the greatest common divisor gcd and the least common
multiplier lcm are defined as follows:
def gcd(x: AlgT, y: AlgT): AlgT =
if (y == T) x else gcd(y, reminder(x, y))
def lcm(x: AlgT, y: AlgT): AlgT =
multiply(divide(x, gcd(x, y)), y)
}

The trait Tconvert implements efficiently conversion to/from
Scala’s BigInt arbitrary size integers using bit-level operations
corresponding to power of 2 and recognition of odd and even natural numbers. The function fromN builds an AlgT tree representation
equivalent to a BigInt.
trait Tconvert {
def fromN(i: BigInt): AlgT = {
def oddN(i: BigInt) =
i.testBit(0)
def evenN(i: BigInt) =
i != BigInt(0) && !i.testBit(0)

def hN(x: BigInt): BigInt =
if (oddN(x))
BigInt(0)
else
BigInt(1) + hN(x >> 1)
def tN(x: BigInt): BigInt =
if (oddN(x))
(x - BigInt(1)) >> 1
else
tN(x >> 1)
if (0 == i) T
else C(fromN(hN(i)), fromN(tN(i)))
}

The function toN converts an AlgT tree representation to a BigInt.
def toN(z: AlgT): BigInt = z match {
case T ⇒ 0
case C(x, y) ⇒
(BigInt(1) << toN(x).intValue()) ∗
(BigInt(2) ∗ toN(y) + 1)
}
}

Note that for both these conversions we have used, for efficiency
reasons, the “real constructors” T and C, although much simpler
(and slower) converters can be built using either the AlgB or AlgU
view of AlgT terms.
The use of Scala’s generalized constructors inspired by our free
algebra isomorphisms has shown the combined flexibility of inheritance as a mechanism for data abstraction and convenient pattern matching allowing the design of our algorithms in a functional
style. The implicit use of apply and unapply methods in combination with our simple free algebra semantics has facilitated the safe
use of fairly complex (mutually) recursive functions in the definition of the generalized constructors. The use of Scala’s traits has
facilitated flexible inheritance mechanisms supporting shared definitions without any additional syntactic clutter.

4.

An Application: Rational Arithmetic in Scala
with Calkin-Wilf Trees

We will extend our Scala code snippet described in subsection
3.1 to a realistic arbitrary size arithmetic package. It is somewhat
unconventional, as it is based on the Calkin-Wilf bijection [3, 6]
between N and the set of positive rational numbers Q+ , rather than
more typical representations like the arrays of long words used in
Java’s BigDecimal package, also adopted through a wrapper class
with the same name by Scala (which runs on top of the Java Virtual
Machine).
Among its advantages, division (with non-zero) always returns a
finitely represented rational and “no bit is lost” in the representation
as canonical rational numbers with co-prime numerator/denominator pairs are bijectively mapped to natural numbers. Our approach
emphasizes the fact that a mathematical concept defined traditionally through equivalence classes and quotients, can be expressed
entirely in terms of a free algebra-based mechanism.
The trait Q representing our rational number data type contains
distinct constructors for positive (P), negative numbers (M) and zero
(Z).
trait Q extends Qcode
case object Z extends Q
case class P(x: (AlgT, AlgT)) extends Q
case class M(x: (AlgT, AlgT)) extends Q

The actual code will be shared through the trait Qcode that also
mixes-in functionality from the natural number operations defined
in the traits Tcompute and Tconvert.
We start with a type definition for ordered pairs of natural numbers PQ represented as terms of AlgT and the conversion function
to a conventional fraction represented as an ordered pair of BigInt
objects. The conversion function toFraq uses the AlgT to BigInt
converter toN.
trait Qcode extends Tcompute with Tconvert {
type PQ = (AlgT, AlgT)
def toFraq(): (BigInt, BigInt) = this match {
case Z
⇒ (0, 1)
case M((a, b)) ⇒ (-(toN(a)), toN(b))
case P((a, b)) ⇒ (toN(a), toN(b))
}

The function t2pq splits its argument u seen as a natural number
into its corresponding Calkin-Wilf rational, represented as a pair of
positive natural numbers of type PQ. Note the use of our generalized
constructors O and I distinguishing between odd and even numbers.
The algorithm uses an encoding of the path in the Calkin-Wilf tree
as a member of AlgB, where O is interpreted as a command to take
the left branch and I is interpreted as a command to take the right
branch at a node of the Calkin-Wilf tree (shown in Fig. 1, for a few
small positive rationals, represented as conventional fractions).

Figure 1. The Calkin-Wilf Tree
def t2pq(u: AlgT): PQ = u match {
case T ⇒ (S(T), S(T))
case O(n) ⇒ {
val (x, y) = t2pq(n)
(x, add(x, y))
}
case I(n) ⇒ {
val (x, y) = t2pq(n)
(add(x, y), y)
}
}

The function pq2t fuses back into a “natural number” represented
as a term of AlgT, corresponding to the path in the Calkin-Wilf tree,
a pair of co-prime natural numbers representing the (numerator,
denominator) pair defining a positive rational number.
def pq2t(uv: PQ): AlgT = uv match {
case (O(T), O(T)) ⇒ T
case (a, b) ⇒
cmp(a, b) match {
case GT ⇒ I(pq2t(sub(a, b), b))
case LT ⇒ O(pq2t(a, sub(b, a)))
}
}

This brings us to the definition of the bijection between signed rationals and terms seen through the use of our generalized constructors O and I as terms of AlgB representing natural numbers.

def fromT(t: AlgT): Q = t match {
case T
⇒ Z // zero → zero
case O(x) ⇒ M(t2pq(x)) // odd → negative
case I(x) ⇒ P(t2pq(x)) // even → positive
}

val (u, v) = uv
cmp(multiply(x, v), multiply(y, u))
}

Multiplication, inverse and division on Q+ are defined as usual.
def pqmultiply(a: PQ, b: PQ) =
pqsimpl(multiply(a._1, b._1), multiply(a._2, b._2))

Its inverse from signed rationals to terms of AlgT, seen as natural
numbers, proceeds by case analysis on the Q data type. Note that
positive sign is encoded by mapping to even naturals and negative
sign is encoded by mapping to odd naturals.
def toT(q: Q):
case Z
⇒
case M(x) ⇒
case P(x) ⇒
}

AlgT = q match {
T // zero → zero
O(pq2t(x)) // negative → odd
I(pq2t(x)) // positive → even

def pqinverse(a: PQ) = (a._2, a._1)
def pqdivide(a: PQ, b: PQ) = pqmultiply(a, pqinverse(b))

We are ready to define arithmetic operations on the set of signed
rationals Q, by case analysis on their sign. We start with the opposite of a rational.

The bijection between Scala’s BigInt, seen as a natural number type and signed rationals, is defined as the pair of functions
rat2nat and nat2rat

def ropposite(x: Q) = x match {
case Z
⇒ Z
case M(a) ⇒ P(a)
case P(a) ⇒ M(a)

def nat2rat(n: BigInt): Q = fromT(fromN(n))
}
def rat2nat(q: Q): BigInt = toN(toT(q))

Next we define a simplifier of positive fractions represented as a
pair, to facilitate arithmetic operations on our rationals.

Addition is defined by case analysis on the sign and calls to the
appropriate operations on positive rationals.
def radd(a: Q, b: Q): Q = (a, b) match {
case (Z, y)
⇒ y
case (M(x), M(y)) ⇒ M(pqadd(x, y))
case (P(x), P(y)) ⇒ P(pqadd(x, y))
case (P(x), M(y)) ⇒ pqcmp(x, y) match {
case LT ⇒ M(pqsub(y, x))
case EQ ⇒ Z
case GT ⇒ P(pqsub(x, y))
}
case (M(x), P(y)) ⇒ ropposite(radd(P(x), M(y)))
}

def pqsimpl(xy: PQ) = {
val x = xy._1
val y = xy._2
val z = gcd(x, y)
(divide(x, z), divide(y, z))
}

We also use our simplifier to import and export non-canonically
represented rationals represented as BigInt pairs.
def fraq2pq(nd: (BigInt, BigInt)): PQ =
pqsimpl((fromN(nd._1), fromN(nd._2)))

Subtraction is defined similarly.

def pq2fraq(nd: PQ): (BigInt, BigInt) =
(toN(nd._1), toN(nd._2))

def rsub(a: Q, b: Q) = radd(a, ropposite(b))
def rmultiply(a: Q,
case (Z, _)
case (_, Z)
case (M(x), M(y))
case (M(x), P(y))
case (P(x), M(y))
case (P(x), P(y))
}

We are now ready for our arithmetic operations. The template function pqop, parameterized by a function f, will be shared between
addition and subtraction. Note that it also involves simplification,
to ensure that the results are in a canonical co-prime numerator/denominator form.
def pqop(f: (AlgT, AlgT) ⇒ AlgT, xy:PQ, uv:PQ):PQ = {
val (x, y) = xy
val (u, v) = uv
val z = gcd(y, v)
val y1 = divide(y, z)
val v1 = divide(v, z)
val num = f(multiply(x, v1), multiply(u, y1))
val den = multiply(z, multiply(y1, v1))
pqsimpl((num, den))
}

We can use it to define addition and subtraction of positive rationals
by simply instantiating our function parameter f to add and sub
operating on terms of AlgT.
def pqadd(a: PQ, b: PQ) = pqop(add, a, b)
def pqsub(a: PQ, b: PQ) = pqop(sub, a, b)

The comparison operation providing a total ordering of Q+ relies
on the function cmp comparing terms of AlgT seen as natural
numbers.
def pqcmp(xy: PQ, uv: PQ) = {
val (x, y) = xy

b:
⇒
⇒
⇒
⇒
⇒
⇒

Q): Q = (a, b) match {
Z
Z
P(pqmultiply(x, y))
M(pqmultiply(x, y))
M(pqmultiply(x, y))
P(pqmultiply(x, y))

Finally we define the inverse on non-zero rationals
def rinverse(a: Q) = a match {
case M(x) ⇒ M(pqinverse(x))
case P(x) ⇒ P(pqinverse(x))
}

and use it to derive from it a division operation on Q
def rdivide(a: Q, b: Q) =
rmultiply(a, rinverse(b))
}

These operations conclude the trait Qcode. While this complete
arithmetic package was built mostly as a proof of concept for the
expressiveness of our free algebra based approach on progressively
more interesting mathematical objects, future work is planned for
turning this package into a practical tool. A first observation toward
this end is that, like in the case of Java’s BigIntegers or the Cbased GMP package, one needs to use a hybrid approach, taking
advantage of actual machine words (64 bits at this point), to store
and operate on numbers that fit in a machine word.

5.

Related Work

Numeration systems on regular languages have been studied recently, e.g. in [12] and specific instances of them are also known as
bijective base-k numbers [20]. Arithmetic packages similar to AlgU
and AlgB are part of libraries of proof assistants like Coq [9] and
the corresponding regular languages have been used as a basis of
decidable arithmetic systems like (W)S1S [2] and (W)S2S [11].
Arithmetic computations based on more complex recursive data
types like the free magma of binary trees (essentially isomorphic
to the context-free language of balanced parentheses) are described
in [17] and [16], where they are seen as Gödel’s System T types,
as well as combinator application trees. In [15] a type class mechanism is used to express computations on hereditarily finite sets and
hereditarily finite functions. However, none of these papers provides proofs of the properties of the underlying free algebras or
uses mechanisms similar to the generalized constructors described
in this paper.
A very nice functional pearl [6] has explored in the past (using Haskell code) algorithms related to the Calkin-Wilf bijection
[3]. While using the same underlying mathematics, our Scala-based
package works on terms of the AlgT free algebra rather than conventional numbers, and provides a complete package of arbitrary
size rational arithmetic operations taking advantage of our generalized constructors.

6.

Conclusion

We have shown that free algebras corresponding to some basic
data types in programming languages can be used for arithmetic
computations isomorphic to the usual operations on N.
As a new theoretical contribution, we have worked-out details of
proofs, based only on elementary mathematics, of essential properties of the mutually recursive successor and predecessor functions,
on the free algebra AlgT of ordered rooted binary trees.
A concept of generalized constructor, for which we have found
simple implementations in Scala, has been introduced. By working in synergy with our free algebra isomorphisms we have described, using language constructs like Scala’s apply / unapply,
simple and safe means to combine data abstraction and pattern
matching in modern-day functional and object oriented languages.
As a new practical contribution, a complete arbitrary size signed
rational number package written in Scala has been derived working
with terms of the AlgT free algebra of rooted ordered binary trees
with empty leaves.
Future work is planned to investigate possible practical applications of our algorithms to symbolic and/or arbitrary length integer
arithmetic packages and to parallel execution of arithmetic computations on AlgT.
The code snippet showing the use of Scala’s apply and unapply
methods to support generalized constructors as well as the arithmetic on rationals is available as a separate file at http://######.

Acknowledgement
This research has been supported by NSF grant ######.

References
[1] Nicolas Bourbaki. Elements of Mathematics, Algebra I. Springer,
Berlin Heidelberg New York, 1989.
[2] J. R. Büchi. On a decision method in restricted second order arithmetic. International Congress on Logic, Method, and Philosophy of
Science, 141:1–12, 1962.
[3] N. Calkin and H. S. Wilf. Recounting the Rationals. American Math
Monthly,, 107:360–363, 2000.

[4] T. Coquand and G. Huet. The calculus of constructions. Information
and Computation, 76(2/3):95–120, 1988.
[5] Burak Emir, Martin Odersky, and John Williams. Matching objects
with patterns. In Erik Ernst, editor, ECOOP 2007 - Object-Oriented
Programming, volume 4609 of Lecture Notes in Computer Science,
pages 273–298. Springer Berlin / Heidelberg, 2007.
[6] Jeremy Gibbons, David Lester, and Richard Bird.
Enumerating the rationals.
Journal of Functional Programming, 16
(4), 2006. URL http://www.comlab.ox.ac.uk/oucl/work/
jeremy.gibbons/publications/rationals.pdf.
[7] K. Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten
Standpunktes. Dialectica, 12(280-287):12, 1958.
[8] Naoki Kobayashi, Kazutaka Matsuda, and Ayumi Shinohara. Functional Programs as Compressed Data. ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, January 2012.
ACM Press.
[9] The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. URL http://coq.inria.fr. Version
8.0.
[10] M. Odersky, L. Spoon, and B. Venners. Programming in Scala. Artima
Inc, 2008.
[11] Michael. O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical
Society, 141:1–35, 1969.
[12] Michel Rigo. Numeration systems on a regular language: arithmetic
operations, recognizability and formal power series. Theoretical Computer Science, 269(12):469 – 498, 2001. ISSN 0304-3975.
[13] Dana Scott. Data Types as Lattices. Siam J. Comput., 5(3):522–587,
1976.
[14] Paul Tarau. “Everything Is Everything” Revisited: Shapeshifting Data
Types with Isomorphisms and Hylomorphisms. Complex Systems,
(18):475–493, 2010.
[15] Paul Tarau. Declarative modeling of finite mathematics. In PPDP ’10:
Proceedings of the 12th international ACM SIGPLAN symposium on
Principles and practice of declarative programming, pages 131–142,
New York, NY, USA, 2010. ACM.
[16] Paul Tarau. Declarative Specification of Tree-based Symbolic Arithmetic Computations. In Claudio Russo and Neng-Fa Zhou, editors,
Proceedings of PADL’2012, Practical Aspects of Declarative Languages, pages 273–289, Philadelphia, PA, January 2012. Springer,
LNCS7149.
[17] Paul Tarau and David Haraburda. On Computing with Types. In
Proceedings of SAC’12, ACM Symposium on Applied Computing, PL
track, pages 1889–1896, Riva del Garda (Trento), Italy, March 2012.
[18] Dimitrios Vytiniotis and Andrew Kennedy. Functional Pearl: Every
Bit Counts. ICFP 2010 : The 15th ACM SIGPLAN International
Conference on Functional Programming, September 2010. ACM
Press.
[19] Philip Wadler.
Recursive Types for Free!
1990.
unpublished manuscript at http://homepages.inf.ed.ac.uk/wadler/
papers/free-rectypes/free-rectypes.txt.
[20] Wikipedia. Bijective numeration — wikipedia, the free encyclopedia,
2012. URL http://en.wikipedia.org/w/index.php?title=
Bijective_numeration&oldid=483462536. [Online; accessed 2June-2012].

