Distributive Computability
Sebastiano Vigna
Tesi di Dottorato di Ricerca in Informatica (VII ciclo)
Università degli Studi di Milano e di Torino

2

Contents
1

Introduction

2

Distributive computability
2.1 An elementary definition . . . . . . . . .
2.1.1 Some notation . . . . . . . . . .
2.1.2 The normal form theorem . . . .
2.2 Recursive functions . . . . . . . . . . . .
2.2.1 Encodings . . . . . . . . . . . . .
2.2.2 Equivalence theorems . . . . . .
2.3 Partial functions . . . . . . . . . . . . . .
2.4 Computability in an ordered ring . . . . .
2.4.1 The finite dimensional BSS model
2.4.2 The basic functions . . . . . . . .
2.4.3 Encodings . . . . . . . . . . . . .
2.4.4 Equivalence theorems . . . . . .
2.4.5 An application . . . . . . . . . .

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

9
9
11
11
14
15
15
19
19
20
21
21
23
26

Automata
3.1 Basic definitions . . . . . . . . . . . . .
3.1.1 Pseudofunctions . . . . . . . .
3.2 Morphisms . . . . . . . . . . . . . . .
3.2.1 Refinement . . . . . . . . . . .
3.2.2 Pseudofunctions and refinement
3.2.3 Examples . . . . . . . . . . . .
3.2.4 Abstraction . . . . . . . . . . .
3.2.5 Input/Output . . . . . . . . . .
3.3 Partial specification . . . . . . . . . . .
3.4 A Categorical Note . . . . . . . . . . .

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

29
29
30
30
31
33
33
34
35
35
38

The general theory
4.1 Distributive categories . . . . . . . . . . . . . . . . . . . .
4.1.1 Data types . . . . . . . . . . . . . . . . . . . . . . .
4.1.2 The free distributive category on a distributive graph
4.1.3 The language IMP(G) . . . . . . . . . . . . . . . .
4.2 Extensive categories . . . . . . . . . . . . . . . . . . . . . .
4.2.1 Functions and functional processors . . . . . . . . .
4.2.2 The semantics of IMP(G) programs . . . . . . . . .
4.2.3 Technical lemmata . . . . . . . . . . . . . . . . . .

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.

39
39
39
40
45
45
47
50
50

3

4

5

3

.
.
.
.
.
.
.
.
.
.

CONTENTS

4

4.3
4.4
5

6

4.2.4 The control function theorem . . . . . . . . . . . . . . . . . . . . . . . . . .
Refinement in lextensive categories . . . . . . . . . . . . . . . . . . . . . . . . . . .
Some consideration on partiality . . . . . . . . . . . . . . . . . . . . . . . . . . . .

52
54
57

A new coding for IMP(G)
5.1 A new efficient coding for IMP(G) data . . . . .
5.1.1 The old coding . . . . . . . . . . . . . .
5.1.2 The new coding . . . . . . . . . . . . . .
5.1.3 Normalization and associativity . . . . .
5.2 Coding IMP(G) programs . . . . . . . . . . . .
5.2.1 Coding simple functions . . . . . . . . .
5.2.2 Coding derived functions . . . . . . . . .
5.3 A type-checking algorithm for IMP(G) programs
5.4 Some remarks on implementation . . . . . . . .

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

59
59
59
60
61
62
62
63
63
66

A literate IMP(G) implementation
6.1 Identifiers . . . . . . . . . . .
6.2 Objects . . . . . . . . . . . .
6.3 Arrows . . . . . . . . . . . .
6.4 Support . . . . . . . . . . . .
6.5 DomCod . . . . . . . . . . . .
6.6 Data . . . . . . . . . . . . . .
6.7 Errors . . . . . . . . . . . . .
6.8 IMP-syntax . . . . . . . . . .
6.9 IMP-compile . . . . . . . . .
6.10 IMP-typecheck . . . . . . . .
6.11 IMP-exec . . . . . . . . . . .
6.12 IMP-Nat . . . . . . . . . . . .
6.13 IMP . . . . . . . . . . . . . .

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

67
68
69
70
71
75
79
79
80
81
89
92
94
95

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.

Chapter 1

Introduction
This thesis presents a series of theoretical results and practical realisations about the theory of computation in distributive categories. Distributive categories have been proposed as a foundational tool
for Computer Science in the last years, starting from the papers of R.F.C. Walters [Walters:1989a,
Walters:1992a, Walters:1992b]. We shall focus on two major topics: distributive computability, i.e.,
a generalized theory of computability based on distributive categories, and the IMP(G) language,
which is a language based on the syntax of distributive categories. The link between the former and
the latter is that the functions computed by IMP(G) programs are exactly the distributively computable functions.
In order to put into a historical perspective the definitions we shall use, we would like to quote
part of a letter of D.E. Knuth written in 1966 to the editor of the Communications of the ACM
[Knuth:1966]:
The preceding letter by Dr. Huber defines “algorithm” in terms of programming languages. I would like to take a slightly different point of view, in which algorithms are
concepts which have existence apart from any programming language. [. . . ] I will try
to explain how the notion of “algorithm” can be mathematically formulated along these
lines. Let us say that a computational method comprises a set Q (finite or infinite) of
“states”, containing a subset X of “inputs” and a subset Y of “outputs”; and a function
F from Q into itself. (These quantities are usually also restrictely to be finitely definable, in some sense that corresponds to what human beings can comprehend.) Such a
computational method defines a computation for each x in X as follows: Let q 0 = x,
and for m ≥ 0 when qm has been defined let qm+1 = F(qm ) if qm 6∈ Y ; if qm ∈ Y ,
we say that the computational method terminates after m steps, producing the output q m .
Clearly any program (i.e., a sentence in a programming language) is an example of a
computational method in this sense. An algorithm is now defined to be a computational
method that terminates in finitely many steps for each input x. Finally we can define the
notion of a program representing a computational method: let the computational method
C be (Q, X, Y, F) and let the program P be (Q 0 , X 0 , Y 0 , F 0 ); P represents C if there is
a function σ from Q into Q 0 , taking X into X 0 , and a function τ from Y 0 into Y , such
that (i) if x ∈ X defines defines the computational sequence x = q 0 , q1 , . . . in C, then
σ (q0 ), σ (q1 ), . . . is a subsequence of the computational sequence x 0 = σ (x) = q00 , . . .
in P; and (ii) if C produces output y from x, P produces the output y 0 from x 0 where
τ (y 0 ) = y.
The notion of pseudofunction (Chapter 3), introduced by Walters in the context of distributive categories [Walters:1992b], corresponds exactly to that of an algorithm in the sense of Knuth (prefunc5

6

CHAPTER 1. INTRODUCTION

tional processors [Khalil], on the other hand, correspond to computational methods). And we shall
show that the notion of representation can be led to that of a functor. Thus, the study of computation
in distributive categories can be viewed as a new, wide generalization of some basic ideas about computation and iteration which have been known for a long time. The scientific program carried out in
this thesis deals in particular with the computational power of computation in distributive categories,
and with the relations between iteration and refinement (implementation/representation).
Such a generalization has obviously to be compared with the existing general formalisms for
the description of iteration. In particular, we would like to mention Heller’s recursion categories
[Heller:1990] and Elgot’s iteration theories [Elgot:1975]. Heller’s framework is rather different from
ours, because he is interested in generalizing recursion theory rather than computation theory. For
instance, all the objects of a recursion category are isomorphic, which is not true, for instance, as
soon as the natural numbers are replaced by a generic ring R, as in Section 2.4, where the BSS model
of computation will be compared with distributive categories. On the other hand, Heller proved that
the Turing completion of certain subcategories of a (locally connected) iteration category are always
recursion categories, in the sense that it is always possible to prove the existence of universal functions
[Heller:1990].
The feedback operator of iteration theories, on the contrary, is very similar to the call[ − ] operator
introduced in Chapter 2. In particular, the normal form theorem exhibits some properties of call[ − ]
which are true also for the feedback operator [Bloom & Esik:1993]. However, iteration theories
are restricted to consider sum of objects (an iteration theory is an N-category, i.e., it is a category
whose objects are the natural numbers), whereas in distributive categories both sums and products
are allowed, thus allowing to describe data types (for instance, the “parallel product” of two functions
is not expressible in an iteration theory, as it is not the related part of the normal form theorem).
Chapter 2 introduces in an elementary manner the definition of distributive computability, and
gives the basic results which motivate further developments: first of all, the distributively computable
functions over the successor and predecessor functions are exactly the recursive functions; second, the
distributively computable functions over the operation of an ordered ring R are exactly the functions
computable in the BSS model (this result provides one of the few known equivalent formulations of
the BSS computable functions).
Chapter 3 is devoted to the study of morphisms of automata. The main result proved here is
a refinement theorem which says that an automaton on a free monoid implements (represents) the
functions it computes, in the sense of Knuth’s letter.
Chapter 4 dives deeply into category theory, in order to describe distributive computability in
the greatest generality. The technical definition justifying the elementary treatment of Chapter 2 are
given here, together with a series of theoretical results about distributive and extensive categories
which allow to prove a theorem about the computational irrelevance of iteration (in a very general
sense) under a simple syntactical assumption which corresponds to the absence of tests. Finally, the
refinement theorem is lifted to the extensive categorical setting.
The last two chapters present the implementation of a series of tools (type-checker, compiler and
interpreter) for programming in IMP(G). The tools are based on a new representation of distributive
data and programs (the first such representation was given in [Khalil & Walters:1993]) which allows
to implement efficiently an interpreter.
Most of the material in this thesis is original. The equivalence theorems of Chapter 2 have been
published in [Sabadini, Vigna & Walters:1996] and in [Vigna:1996] (the equivalence theorem for recursive functions appears here in a slightly stronger version). The basic ideas of Chapter 3 were introduced in [Sabadini, Vigna & Walters:1993a] and in [Sabadini, Vigna & Walters:1993b]; the presentation given here extends the results contained in the aforementioned references to generic monoids,
and introduces some new counterexamples and theorems (in particular, Section 3.3).
The constructions given in Section 4.1.2 appear here for the first time, and starting from Section 4.2.1 the rest of Chapter 4 is original. The first definition of function computed by iteration

7
was given by Khalil and Walters in terms of colimits; the definition was then simplified and restated
in terms of sums in [Wagner, Khalil & Walters:1995] and [Sabadini, Vigna & Walters:1996]. In this
thesis we use a new formulation, which is equivalent to the previous ones.
Finally, the material of the last two chapters has been entirely developed by the author, and partially presented in [Vigna:1995].
I would like to thank several people, without whom the making of this thesis would have been
much harder, if not impossible. Paolo Boldi introduced me to the BSS model by means of his excellent survey, and commented the drafts. The material of Chapter 4 and of Chapter 6 has been heavily
discussed with Steve Lack and Eelco Visser, respectively. In particular, the electronic communications with Steve have always been a useful source of inspiration about distributive and extensive
categories, while Eelco answered all my (often stupid) questions about ASF+SDF 1 and suggested
several improvements. The feedback received at the ASF+SDF95 workshop from the people of the
University of Amsterdam was also a precious source of information. Danilo Bruschi and Gaetano
Lanzarone kindly made the computing resources on which to run ASF+SDF available.
But the biggest “thanks” goes without any doubt to the people of the “Sala Dottorandi & Paolo
Boldi” (Ph.D. room) of the University of Milan. For three years they have been not only brilliant researchers with whom interaction is always scientifically fruitful, but also friends whose relationships
are warm and intense; the time spent together has been some of the best time of my life.

1 The system ASF+SDF was used in order to realize the implementation described in the last two chapters.

8

CHAPTER 1. INTRODUCTION

Chapter 2

Distributive computability
In this chapter we shall introduce the concept of distributive computability. The definition we shall
give of function computable by iteration is in the same spirit of Kleene’s definition of recursive
function [Kleene:1936], but it will be given in the environment of a countably extensive category,
thus giving a wide and natural generalization of the concept of computable function.
Kleene’s definitions builds inductively a set of functions from the powers of N to N; starting from
the zero function, the successor function and the projections, and closing by substitution, primitive
recursion and minimization, we obtain a class of function which we call (partial) recursive.
In the definition which we shall give the domain and codomain of the functions will be obtained by
using also the sum operator (disjoint union, in the category of sets). This fact will allow the definition
of an operator of iteration which essentially incorporates both primitive recursion and minimization.
Moreover, the rôle of the zero, successor and projection functions will be taken by an arbitrary set of
basic functions; thus, the notion of distributive computability will be parametric, and will depend on
the given basic set.
Recently, Blum, Shub and Smale proposed a generalization of the definition of computable function [Blum, Shub & Smale:1989] which is valid in an arbitrary ordered ring, rather than in the natural
numbers. We will show how also this class of functions is generated by a particular instantiation of
the model of distributive computability.

2.1 An elementary definition
In order to make this thesis accessible to the widest audience, we will first give a definition of distributively computable function in a special case, i.e., in the familiar category of sets. In other words,
Set is now the “computational universe” (the rôle played by the category E in Chapter 4).
For any pair of sets X , Y , the sum X + Y is the disjoint union of X and Y , i.e., the set X × {0} ∪
Y × {1}. The canonical injections inj1 : X → X + Y , inj2 : Y → X + Y are defined by
inj1 (x)

=

hx, 0i

inj2 (y)

=

hy, 1i.

The product X × Y is the cartesian product of X and Y , i.e., the set {hx, yi | x ∈ X ∧ y ∈ Y }.
The canonical projections proj1 : X × Y → X , proj2 : X × Y → Y are defined by
proj1 (hx, yi)

=

x

proj2 (hx, yi)

=

y.

9

CHAPTER 2. DISTRIBUTIVE COMPUTABILITY

10

Should ambiguities arise, we shall write inj1X,Y and so on.
The empty set ∅ and the singleton I = {∗} are the units of + and × (up to isomorphism, i.e., up
to bijections of sets; we shall not insist in making such isomorphisms explicit). For any set X , there
are unique functions
!X
¡X

:
:

∅→X
X → I,

called the initial and terminal maps1 .
We have also corresponding constructions on functions: for any pair of functions f : X → Z and
g : Y → Z , ( f | g) : X + Y → Z is defined by

f (x) if z = hx, 0i
( f | g)(z) =
g(y) if z = hy, 1i
and for any pair of functions f : Z → X and g : Z → Y , ( f, g) : Z → X × Y is defined by
( f, g)(x) = h f (x), g(x)i.
We shall denote by g ◦ f the composition of the functions f : X → Y and g : Y → Z .
Sums and products of sets are related by the distributivity isomorphism
∼
=

δ : X ×Y + X × Z −
→ X × (Y + Z ),
which maps hhx, wi, ki to hx, hw, kii, with k = 0 or 1, and w an element of Y or Z , respectively.
Moreover, any set X has an associated identity function 1 X : X → X .
We can now introduce some entities derived from the previous ones:
• 1 X = (1 X , 1 X ) : X → X × X ;
• ∇ X = (1 X | 1 X ) : X + X → X ;
• for each pair of functions f : X → X 0 and g : Y → Y 0 , we have
f × g = ( f ◦ proj1 , g ◦ proj2 ) : X × Y → X 0 × Y 0
and
f + g = (inj1 ◦ f | inj2 ◦g) : X + Y → X 0 + Y 0 .
Note that ( f | g) = ∇ ◦ ( f + g) and ( f, g) = ( f × g) ◦ 1, so whatever we build using (−, −) and
(− | −) can also be built using ×, +, 1 and ∇; for instance, the canonical function δ : X × Y + X ×
Z → X × (Y + Z ) we described previously is exactly
δ = (1 X × inj1 | 1 X × inj2 ),
and the isomorphisms of commutativity of sum and product, both denoted twist with an abuse of
notation, can be expressed as
(proj2 ,proj1 )

twist : X × Y −−−−−−−→ Y × X
and

(inj2 | inj1 )

twist : X + Y −−−−−−→ Y + X.
1 In [Sabadini, Vigna & Walters:1996], initial and terminal maps are erroneously missing from the elementary definition.

2.1. AN ELEMENTARY DEFINITION

11

Now, if we have a family of sets (the basic sets), consider all the sets that can be obtained from
them and ∅, I by repeated application of sums and products (these are the derived sets). Given a
family of basic functions between derived sets, any function obtained by repeated use of (− | −),
(−, −) and composition on the basic functions, injections, projections, identities, initial maps, terminal maps and δ −1 is again a function between derived sets: all functions defined in this way are called
derived functions.
Finally, for each triple of sets X , U , Y , and any derived function
f : X +U →U +Y
such that for each x ∈ X there is an n x such that2 f n x (x) ∈ Y (i.e., the function terminates for
each input) we define the function which f computes by iteration, denoted by call[ X, U, Y, f ] (or
call[ f ], if X , U and Y are clear from the context), as
call[ X, U, Y, f ](x) = f n x (x).
Note that if such an n x exists, it is unique, because we cannot iterate f over an element of Y .
Definition 1 The class of distributively computable functions (over the given family of basic functions) is exactly the class of functions of the form call[ f ], with f a derived function.

2.1.1

Some notation

We would like to establish some notation which will be useful throughout this thesis. A +/×-algebra
is an algebra having two constants 0, 1 and two binary operators + and ×. A term of the free
+/×-algebra on A is called a distributive expression on A.
The sets ∅ and I are the structural sets. A simple set is either a basic set or a structural set. When
the operations of sum and product and the constants 0 and 1 are interpreted in the category of sets, a
distributive expression on the basic sets gives rise to a derived set. We shall frequently confuse the
former and the latter.
A structural function is one of the injections, projections, identities, initial maps, terminal maps
and inverse distributivity isomorphisms. A simple function is either a basic function or a structural
function. Thus, derived functions are obtained by applying (− | −), (−, −) and composition to
simple functions.
Given a function f : X + Y → Z , we shall denote with f |X the restriction of f to X .
Of course, analogous definitions can be given in an arbitrary distributive category by replacing
“set” with “object” and “function” with “arrow”. Algebraically speaking, structural entities corresponds to constants and operators of a distributive category, while basic entities are generators.
Retrictions are obtained by composition with an injection.

2.1.2

The normal form theorem

The theorem we are going to introduce, appeared for the first time in [Walters:1992b] 3 , is the distributive counterpart of Kleene’s normal form theorem, which says that in the construction of a recursive
function it is possible to use the minimization operator just one time.
Theorem 1 The following properties are true for call[ − ] (we assume that call[ − ] is defined whenever we mention it):
2 We shall omit the natural number tagging the element of a sum whenever no confusion is possible, thus writing just x
instead of hx, ki.
3 Part (iv) of the theorem appeared for the first time in [Sabadini & Walters:1993].

CHAPTER 2. DISTRIBUTIVE COMPUTABILITY

12
(i). For each function f : X → Y ,

f = call[ (inj2 ◦( f | !Y ) : X + ∅ → ∅ + Y ];
(ii). If f : X + U → U + Y and g : Y + V → V + Z , then
call[ f ] ◦ call[ g ] = call[ X, U + Y + V, Z , f + g ].
(iii). If f : X + U → U + Y and g : X 0 + U 0 → U 0 + Y 0 , then
call[ f ] + call[ g ] = call[ a ◦ ( f + g) ◦ b ],
where a is the commutativity isomorphism
∼
=

X + X0 + U + U0 −
→ X + U + X 0 + U 0,
and b is the commutativity isomorphism
∼
=

→ U + U 0 + Y + Y 0;
U + Y + U0 + Y0 −
moreover,
call[ f ] × call[ g ] =
0

0

,Y
| injU,Y
×g|U 0 ) ],
call[ d ◦ ( f |X × g|X 0 | f |U × g|U 0 | f |U × injU
2
2

where d is the isomorphism
∼
=

(U + Y ) × (U 0 + Y 0 ) −
→ UU 0 + U Y 0 + Y U 0 + Y Y 0
induced by distributivity.
(iv). If f : X + V + U → U + V + Y , then
call[ X, V, Y, call[ X + V, U, V + Y, f ] ] = call[ X, U + V, Y, i ◦ f ] : X → Y,
where i is the commutativity isomorphism
∼
=

U +V +Y −
→ V + U + Y.
Note that since ( f | g) = ∇ ◦ ( f + g) and ( f, g) = ( f × g) ◦ 1, also (call[ f ] | call[ g ]) and
(call[ f ], call[ g ]) can be expressed with a single use of call[ − ]. We remark that the properties of
call[ − ] which do not involve products are the properties of the feedback operator of iteration theories
[Bloom & Esik:1993].
The immediate consequence of the normal form theorem is that the functions computed by iteration, when added to the family of basic functions, do not modify its computational power. Formally,
Theorem 2 The class of distributively computable functions is the class of functions obtained by
applying inductively (− | −), (−, −), composition and call[ − ] to simple functions.

2.1. AN ELEMENTARY DEFINITION

13

Proof. We just have to show that, given a function f defined using repeatedly call[ − ], it is also
possible to define it by applying call[ − ] to a suitable derived function. But the normal form theorem
show that any derived function used in the definition of f is of the form call[ g ], and that each time
an operator is applied, call[ − ] can be “extracted” in such a way to arrive to a definition of the form
call[ call[ · · · call[ g ] · · · ] ], with g a derived function; now, part (iv) of the normal form theorem
reduces all the applications of call[ − ] to just one.
A completely analogous analysis (as briefly discussed in Section 2.3) can be done on the pcall[ − ]
operator, which allows to iterate any f : X + U → U + Y , producing possibly a partial function.
This fact in turn yields immediately that the class of total distributively computable partial functions
coincides with the class of distributively computable functions.
In order to prove the theorems of this chapter, it is now necessary to introduce some technical
lemmata which show how it is possible to avoid the usage of initial maps in the definition of noninitial
derived functions.
Definition 2 Let X be a derived set. The reduced form of X , named ρ(X ), is obtained inductively
from X as follows:
(i). ρ(X ) = X for simple sets;
(ii). ρ(X × ∅) = ρ(∅ × X ) = ∅;
(iii). ρ(X + ∅) = ρ(∅ + X ) = ρ(X ).
Clearly, X ∼
= ρ(X ), and we can fix this isomorphism (which we will call ν X ) on the basis of the
proj2
inductive definition (X × ∅ −−→ ∅, and so on). Note that X ∼
= ∅ iff ρ(X ) = ∅.
Theorem 3 Let f : X → Y be a derived function, with X 6 ∼
= ∅. Then f = νY−1 ◦ f 0 ◦ ν X , where
0
f : ρ(X ) → ρ(Y ) is a derived function which is defined without using initial maps.
Proof. The claim is obvious for simple functions. Let us examine inductively the following cases:
• f = (g | h) : X + X 0 → Y . If (without loss of generality) h 0 is an initial map, f 0 = g 0 ◦ inj1X,∅
and f = νY−1 ◦ f 0 ◦ ν X . If instead neither g 0 nor h 0 are initial maps, f 0 = (g 0 | h 0 ) and
f = νY−1 ◦ f 0 ◦ ν X +X 0 .
• f = (g, h) : X → Y × Y 0 . In this case, the claim is obvious with f 0 = (g 0 , h 0 ), because neither
g nor h can be initial.
• f = h ◦ g. Again, the claim is obvious with f 0 = h 0 ◦ g 0 (recall that f is initial iff g is initial,
and that if h is initial then g is initial).

Corollary 1 The class of functions obtained applying call[ − ] to functions (between reduced derived
sets) defined without using initial maps is equal to the class of distributively computable functions
without initial maps.
At this point we can restrict our attention to functions defined without using initial maps. Indeed,
the iteration of a function f for which f 0 is initial produces necessarily an initial map (if X + U ∼
= ∅,
then X ∼
= ∅). Since initial maps do not compute anything (they have empty domain), in the
=U ∼
proof of equivalence theorems we can forget them4 .
4 Note that these considerations are true also at the categorical level, i.e., in the extensive categorical setting of Chapter 4.

CHAPTER 2. DISTRIBUTIVE COMPUTABILITY

14

2.2 Recursive functions
We now recall Kleene’s definition of recursive function [Kleene:1936].
Definition 3 The set of recursive functions from N k to N is the smallest set of functions containing
the 0 constant function, the successor function succ : N → N, the projections π j : N k → N and
closed under the following constructions:
(i). (substitution) given f : N k → N and gi : N j → N (1 ≤ i ≤ k), form f (g1 , g2 , . . . , gk ) :
N j → N;
(ii). (primitive recursion) given g : N k → N, h : N k+2 → N, form f : N k+1 → N by setting
f (m, 0) = g(m)
and
f (m, n + 1) = h(m, n, f (m, n));
(iii). (minimization) given a function f : N k+1 → N such that for all m there is an n m such that
f (m, n m ) = 0, form g : N k → N by setting
g(m) = µn f (m, n) = min{n ∈ N | f (m, n) = 0}.
If we drop the condition of existence of a solution in n for f (m, n) = 0, we have the definition of
partial recursive function.
Definition 4 The set of partial recursive functions from N k to N is the smallest set of partial functions containing the 0 constant function, the successor function succ : N → N, the projections
π j : N k → N, and closed under substitution, primitive recursion, and under the following construction (partial minimization): given f : N k+1 → N, form g : N k → N by setting
g(m) = µn f (m, n) = min{n ∈ N | f (m, n) = 0 and f (m, i) is defined for all i < n};
g(m) is undefined when the aforementioned set is empty.
It is a well-known but non trivial fact that the class of recursive functions coincide with the class
of total partial recursive functions. We shall give in the sequel a very simple proof of this fact using
Theorem 2.
Now we instantiate the definition of distributive computability using as basic functions the following generalizations of the precedessor and successor functions:
p:N

→

I+N

n
0

7→
7→

n−1
∗

s:I+N

→

N

(= {∗} + N)
if n > 0

∗ 7→ 0
n 7→ n + 1.
Note that with these definitions s and p are inverse, and that the predecessor function allows to
check if a number is equal to zero: indeed, by composing p with a function of the form f + g, the
computation will continue with f or g depending of the input of p being equal to zero. We will
denote with D N the set of function distributively computable on s and p.

2.2. RECURSIVE FUNCTIONS

2.2.1

15

Encodings

Now we would like to prove that the set D N and the set of recursive function do coincide. Strictly
speaking, this is impossible, because the domains and codomains of the first class of functions are
taken from a much larger set.
However, we will exploit the fact that any derived set built starting from N and I can be mapped
injectively in N, and that N can be mapped surjectively on any such derived set using standard
arithmetic operations based upon primitive recursion only (see, for instance, [Manin:1977]); once we
code the domain and codomain of the functions in D N using this maps, we shall obtain exactly the
class of recursive functions.
Definition 5 The (bijective) encodings σ+ : N + N → N and σ× : N × N → N are defined
by σ+ (hn, ki) = 2n + k and by the standard pairing function (for this latter and its inverse, see
[Manin:1977]). Let 0 : I → N the constant zero function, and ¡ N : N → I the terminal map
associated to N. For each derived set X we define the encodings σ X : X → N and σ X0 : N → X :
• if X = I , then σ X = 0 and σ X0 = ¡ N ;
• if X = N, then σ N = σ N0 = 1 N ;
• if X = Y + Z , then σ X = σ+ ◦ (σY + σ Z ) and σ X0 = (σY0 + σ Z0 ) ◦ σ+−1 ;
• if X = Y × Z , then σ X = σ× ◦ (σY × σ Z ) and σ X0 = (σY0 × σ Z0 ) ◦ σ×−1 .
Note that the encodings σ and σ 0 are related by the following property:
Proposition 1 σ X0 ◦ σ X = 1 X .
Proof. A simple structural induction shows that
σ X0 ◦ σ X = (σY0 + σ Z0 ) ◦ σ+−1 ◦ σ+ ◦ (σY + σ Z ) =
(σY0 + σ Z0 ) ◦ (σY + σ Z ) = σY0 ◦ σY + σ Z0 ◦ σ Z = 1 X .
Analogously for the product.
In what follows, given a function f : X → Y we will denote with b
f the function σY ◦ f ◦ σ X0 .
The previous proposition shows that
Corollary 2 b
g◦ b
f = g[
◦ f.

2.2.2

Equivalence theorems

Using the encodings we just defined, we can finally state the equivalence theorem:
Theorem 4 Let F = { f : N → N | f is recursive} the set of recursive functions, and let G =
{b
f | f : X → Y ∈ D N } be the set of distributively computable functions whose domains and
codomains have been coded in N. Then F = G.
Note that we considered only recursive functions having N as domain: it is immediate to see that
this restriction can be made without loss of generality.

Proof. We begin by showing that F ⊆ G, i.e., the recursive functions N → N are a subset of the
distributively computable ones.

CHAPTER 2. DISTRIBUTIVE COMPUTABILITY

16

First of all note that the basic functions mentioned in the definition of recursive function are
distributively computable (succ = s◦inj2 , and 0 = s◦inj1 ). Substitution can be obtained using (−, −)
and composition, so that the only things left to prove are primitive recursion and minimization.
Primitive recursion. Given functions g : N k → N and h : N k+2 → N which define by primitive
recursion a function f : N k+1 → N, we want to build a function
α : N k × N + (N k × N × N × (I + N)) → (N k × N × N × (I + N)) + N
such that call[ α ] = f .
Intuitively, the “middle part” of the state space is given by
input×last output×recursion index×counter
(the recursion index is n in Definition 3; the counter is necessary because it has to run backwards
with respect to n).
We shall describe α by breaking it into the two component which acts on the summands of its
domain; we shall understand the obvious injections in the codomain. The first part moves the data
out of the initial state, decrements the counter, initialize the recursion index to 0 and applies at the
same time the “initial data” function g:
(1,g)×0× p
Nk × N ∼
= N k × I × N −−−−−−→ N k × N × N × (I + N).

Note that
N k × N × N × (I + N) ∼
= (N k × N × N) + (N k × N × N × N),
so we can define the second part of α separately on the two summands. Clearly,
proj2

N k × N × N −−→ N
projects the result on the final state. Indeed, when the counter arrives in the first part of (I + N) we
iterated the loop exactly the number of times required.
The following function defines the action on the second summand:
Nk × N × N × N

−−−−−−−−−−−−→

1×1×1×1

Nk × Nk × N × N × N × N

1×1×twist ×1×1

Nk × Nk × N × N × N × N

−−−−−−−−−−−−→
1×h×1×1

−−−−−−−−−−−−→
1×1×(s◦inj2 )× p

−−−−−−−−−−−−→

Nk × N × N × N
N k × N × N × (I + N).

In order to show that call[ α ] = f , we shall compute explicitly the orbit induced by α. For an
input (m, n) we have
(m, n) 7→ (m, g(m), 0, n − 1).
If n = 0, the next iteration will be
(m, g(m), 0) 7→ g(m) = f (m, 0),
which computes correctly f . If n > 0,
(m, g(m), 0, n − 1)

7→

(m, m, g(m), 0, 0, n − 1)

7→ (m, m, 0, g(m), 0, n − 1)
7→ (m, h(m, 0, g(m)), 0, n − 1) = (m, f (m, 1), 0, n − 1)
7→

(m, f (m, 1), 1, n − 2)

2.2. RECURSIVE FUNCTIONS

17

and, by induction, when α computes f (m, k) the counter is decremented to n − k − 1, thus moving
the state to the final summand.
Minimization. The function
β : N k + (N k × N) → (N k × N) + N
which we shall use in order to emulate the minimization operator is defined on N k by N k ∼
= Nk ×
1×0

I −−→ N k × N, while on N k × N it acts as follows:
Nk × N

1

−−−−−−−−−−−−→

Nk × N × Nk × N

1×1× f

Nk × N × N

1×1× p

N k × N × (I + N)

−−−−−−−−−−−−→
−−−−−−−−−−−−→
δ −1

−−−−−−−−−−−−→

(N k × N) + (N k × N × N)

−−−−−−−−−−−−→

proj2 +(proj1 ,proj2 )

N + (N k × N)

−−−−−−−−−−−−→

twist

(N k × N) + N

(1×(s◦inj2 ))+1

(N k × N) + N.

−−−−−−−−−−−−→

Thus, if the result of f is 0, the function lands in N, returning the number of iterations; otherwise, it
remains in N k × N, incrementing the iteration counter (the second factor of the product).
In more detail, for a given input m the first application of β gives
m 7→ (m, 0),
and then we have
(m, 0)

7→ (m, 0, m, 0)
7→ (m, 0, f (m, 0))
7→

(m, 0, f (m, 0) − 1).

Now, if f (m, 0) = 0, we have simply
(m, 0, ∗) 7→ 0,
otherwise
(m, 0, f (m, 0) − 1) 7→ (m, 0) 7→ (m, 1),
so that β keeps incrementing the loop counter until f is evaluated to 0. Clearly, call[ β ] = µ n f (m, n).
Let now f : X → Y be a distributively computable function. This function has been obtained
by iterating a suitable derived function g : X + U → U + Y . We shall denote with h the loop
(g | inj2 )

X + U + Y → X + U + Y induced by g (and defined formally by h : X + U + Y −−−−−→
inj2

U + Y −−→ X + (U + Y )). Clearly, f is the function obtained by applying h to an element of X until
the generated orbit intersects Y (all elements of Y are fixed points of h).
Since by Corollary 2 we have hbk = b
h k , if we shall be able to prove that for any loop h : X + U +
Y → X + U + Y the function b
h is recursive, we shall be able to use (as it happens typically when
proving the computability of recursive functions using an imperative language) primitive recursion
in order to compute b
h k , and minimization in order to find out the number of iterations which are

CHAPTER 2. DISTRIBUTIVE COMPUTABILITY

18

necessary to arrive in Y . At this point, primitive recursion will again enable us to actually iterate b
h as
much as it is necessary.
Thus, given a loop h : (X + U ) + Y → (X + U ) + Y (the grouping is chosen without loss of
generality), consider the following recursion scheme:

a(n, 0) = n − (n mod 4)
a(n, k + 1) = (b
h ◦ a)(n, k).
Clearly, if n is a multiple of four we have that a(n, k) = b
h k (n). Since the encoding σ(X +U )+Y sends
the elements of Y into odd numbers, µk (1 − (a(n, k) mod 2)) is the least number of iterations after
which b
h “lands in Y ” on input n, and
b(n) = a(n, µk (1 − (a(n, k) mod 2)))

iterates b
h exactly that number of times. Note that at the first iteration we ensure that n is a multiple
of four, and thus that it represents an element of X , making the application of µ possible (we do not
have any guarantee of termination on U ).
At this point we just have to precompose b with multiplication by four (which corresponds to the
inclusion of X in (X + U ) + Y ) and postcompose it with integer division by two (which corresponds
to the extraction of Y from (X + U ) + Y ). The resulting recursive function is exactly b
f.
In order to complete the proof, we shall show by structural induction that all functions b
f , where
f is a derived function, are recursive. The following claims are immediately verified:
• the function b
s sends even number in zero and odd numbers in (n + 1)/2;
• the function b
p sends zero in zero and the other numbers in 2n − 1;
di = proji ◦σ×−1 (i = 1, 2);
• proj

ci (n) = 2n + i − 1 (i = 1, 2);
• inj

• 1c
X = 1N ;
¡ X = 0;
•b

−1 (n) = 2σ ((proj ◦σ −1 )(n), b(proj ◦σ −1 )(n)/2c) + ((proj ◦σ −1 )(n) mod 2).
• δd
×
1
2
2
×
×
×

If f = h ◦ g, then by Corollary 2 we have b
f =b
h ◦b
g . If f = (g, h), b
f is obtained by substituting b
g
b
b
and h into the pairing function σ× . If f = (g | h), f (n) = f 0 (n, n mod 2), where f 0 is obtained by
primitive recursion as follows:
 0
f (n, 0) = b
g (bn/2c)
f 0 (n, k + 1) = b
h(bn/2c).

What we just proved, and the considerations made at the beginning of this chapter, allows us to
say that
Lemma 1 The encodings σ X , σ X0 are distributively computable for each X .
The operation of encoding derived sets in N can be reversed: instead of restricting the distributively computable functions to the class G (the previous lemma implies G ⊆ D N ), we can enlarge F
by composing its functions with the encodings. It is easy to show that
b = {σ 0 ◦ f ◦ σ X | f : R n X → R n Y ∈ F}. Then F
b = DN .
Theorem 5 Let F
Y

2.3. PARTIAL FUNCTIONS

19

Note that this is the claim proved originally in [Sabadini, Vigna & Walters:1996].
b is also trivially in D N (use lemma 1, the fact F = G ⊆ D R , and the closure
Proof. Any function in F
of D N with respect to composition). On the other hand, if f : X → Y ∈ D N then b
f ∈ G = F. But
then
b 3 σ0 ◦ b
F
f ◦ σ X = σY0 ◦ σY ◦ f ◦ σ X0 ◦ σ X = f.
Y

2.3 Partial functions
We shall now briefly outline the (single) modification necessary to handle partiality, and state the
equivalence theorem between recursive and total partial recursive functions, which admits a very
simple proof in this context.
Definition 6 For each function f : X + U → U + Y we define the partial function
pcall[ f ] : X → Y =



f n x (x)
⊥ (undefined)

if there is an integer n x such that f n x (x) ∈ Y
otherwise.

Substituting pcall[ − ] for call[ − ] in the proof of Theorem 4 (the operators on sets and functions
should be redefined accordingly, in a standard manner) yields immediately a result analogous to
Theorem 4 for partial functions. This fact, coupled with the normal form theorem, yields a simple
proof of the well-known but non trivial
Theorem 6 The class of total partial recursive functions coincides with the class of recursive functions.
Proof. Obvious, because the use of call[ − ] or pcall[ − ] in the definition of a recursive function can
be reduced by Theorem 2 to a single, outermost application.

2.4 Computability in an ordered ring
In [Blum, Shub & Smale:1989], Blum, Shub and Smale have defined a model of machine working
on an arbitrary commutative ordered ring (or field) R. Their definition has given rise to a whole
new theory of computability and computational complexity. In the BSS model, a machine has a finite
control, given by a finite graph, and an unlimited number of registers, each capable of holding an
element of R. The computational steps consist in computing polynomials, and possibly deciding the
next step by comparing the result of an evaluation with 0. A pair of integer registers can be used as
pointers in order to retrieve and set any register.
In this section we want to prove an equivalence result between the functions R l → R m (with l, m
finite) computable in the BSS model, and the functions distributively computable in the category of
sets when the basic functions are the constants, sum, multiplication (possibly also inversion) and test
for nonnegativity (note that we do not force a finiteness condition on the state space of BSS machines;
this is unnecessary, as explained below). We remark that an extension of this result to the case of BSS
machines with infinite input/output state space is possible by describing all spaces involved in the
computation via suitable unbounded data types like stacks.

CHAPTER 2. DISTRIBUTIVE COMPUTABILITY

20

2.4.1

The finite dimensional BSS model

In [Blum, Shub & Smale:1989] two kinds of machine are defined: finite dimensional and infinite
dimensional ones, the difference lying in the presence, in the second case, of an infinite number of
registers in the input, output and state space, and of some machinery which is necessary in order
to address such registers. We shall introduce the finite dimensional model, for a reason which will
become clear below.
Recall that an ordered ring is a ring R with a specified subset P ⊆ R \ {0} such that:
1. if α, β ∈ P then α + β, αβ ∈ P;
2. for all α ∈ R \ {0}, either α ∈ P or −α ∈ P, but not both.
In an ordered ring, the notation α > β stands for α − β ∈ P.
In the rest of this section, the word “ring” will always mean “ordered commutative ring”. We
shall frequently use the term “polynomial function” for functions R i → R j : this means that each
of the j components of the function is (induced by) a polynomial in i variables. It will be always
understood that if R is a field such functions can also be rational functions. The elements of R will
be denoted by α, β, . . ., while the vectors of R n will be denoted by α = hα1 , α2 , . . . , αn i, β, . . ..
Definition 7 A finite dimensional machine M over R consists of three spaces: the input space I¯ =
R l , the output space Ō = R m and the state space S̄ = R n , together with a finite directed connected
graph with node set N̄ = {1, 2, . . . , N } (N > 1) divided in four subsets: input, computation, branch
and output nodes.
Node 1 is the only input node, having fan-in 0 and fan-out5 1; node N is the only output node,
having fan-out 0. They have associated linear functions (named I (−) and O(−)), mapping respectively the input space to the state space and the state space to the output space. Any other node
k ∈ {2, 3, . . . , N − 1} can be of the following types:
(i). a branching node; in this case, k has fan-out 2 and its two (distinguished) successors are β − (k)
and β + (k); there is a polynomial function h k : S̄ → R associated to k, and for a given state
α ∈ S̄, branching on − or + will depend upon whether or not h k (α) < 0;
(ii). a computation node; in this case, k has fan-out 1 and there is a polynomial function g k : S̄ → S̄
associated with it.
We can view M as a discrete dynamical system over the full state space N̄ × S̄. M induces a
computing endomorphism on the full state space:
h1, αi 7→ hβ(1), αi
hN , αi 7→ hN , αi
hk, αi

7→

hk, αi

7→

hβ(k), gk (α)i if k is a computation node
(
hβ − (k), αi if h k (α) < 0
if k is a branching node.
hβ + (k), αi if h k (α) ≥ 0

The computation of M under input α is the orbit generated in the full state space by the computing
endomorphism starting from h1, I (α)i. If the orbit reaches a fixed point of the form hN , βi for some
β ∈ S̄ we say that the machine halted, and that its output is O(β). The association α 7→ O(β)
defines a partial function ϕ M , which is called the partial function computed by the machine M. In
5 If k is a node with fan-out 1, then β(k) denotes the “next” node in the graph after k.

2.4. COMPUTABILITY IN AN ORDERED RING

21

what follows, we shall consider only machines computing total functions; the obvious extension to
the partial case can be made by substituting the pcall[ − ] operator to the call[ − ] operator.
When defining the infinite dimensional model, the state space—and possibly the input and output spaces—becomes R ∞ (i.e., the space of infinite sequences of elements of R in which only a
finite number of components is nonzero) and nodes of fifth type are added, which allow to access any
register of the state space. However, as suggested in [Blum, Shub & Smale:1989] (and proved in a
different, particularly enlightening way in [Michaux:1989]), if the input and output space of an infinite dimensional machine M are finite, then the function ϕ M is computed also by a finite dimensional
machine. Thus, since in this paper we are discussing the class of computable functions R l → R m
with l, m finite, we can restrict our attention to finite dimensional machines without loss of generality.

2.4.2

The basic functions

For a given ring R, we shall now list the basic functions which will be used to generate the distributively computable functions (categorically speaking, we are defining the base distributive graph). The
list includes the following functions:
R×R
R×R
I
R

∗

−
→
+

−
→
pαq

−→
≥

−
→

R
R
R (for all α ∈ R)
I + I.

If R is a field, we include also a function
(−)−1

R −−−→ R,
the intended semantics being: product and sum of two elements of the ring, constants, test for nonnegativity and inversion. Analytically,
hα, βi
hα, βi

∗

7→
+

7→
pαq

∗

7→

α

7→

α

≥

(−)−1

7→

αβ
α+β
α
(

h∗, 0i
h∗, 1i

α −1

if α < 0
if α ≥ 0

(α 6= 0)

Intuitively, we are claiming that we can multiply and sum (and possibly invert 6 ) the elements
of R, that we can generate any constant, and that we can compute the characteristic function of the
positives7 . We shall denote with D R the class of functions distributively computable starting from
the functions above.
6 In the BSS model it is assumed that a rational function will never be evaluated when the denominator is zero. Thus, we
do not care too much about the definition of 0−1 . It can be taken to be 0, for instance.
7 We mention, without developing the theory, that the function ≥ can be replaced by a test for equality with zero, which
allows to extend the equivalence theorem to unordered rings such as C.

CHAPTER 2. DISTRIBUTIVE COMPUTABILITY

22

2.4.3

Encodings

As in the case of recursive functions, we must now establish an encoding for the derived sets built
from R and I . The solution previously proposed is no longer applicable, because it relied on the
existence of a computable isomorphism N → N × N, which is not in general available for an
arbitrary ring R. Here we shall be contented of encoding sums into products.
Definition 8 The encodings σ (i, j) : R i + R j → R × R i × R j and σ 0 (i, j) : R × R i × R j → R i + R j
are defined by
(
(
σ (i, j) h−1, α, 0i if k = 0
σ 0 (i, j) hβ, 0i if α < 0
hα, ki 7→
hα, β, γ i 7→
h0, 0, αi
if k = 1
hγ , 1i otherwise.
For any derived set X we define inductively σ X : X → R n X and σ X0 : R n X → X as follows:
• if X = I , then n I = 1, σ I = 0 and σ I0 = ∗;
• if X = R, then n R = 1 and σ R = σ R0 = 1 R ;
• if X = Y + Z , then n X = n Y + n Z + 1, σ X = σ (n Y , n Z ) ◦ (σY + σ Z ) and σ X0 = (σY0 + σ Z0 ) ◦
σ 0 (n Y , n Z );
• if X = Y × Z then n X = n Y + n Z , σ X = σY × σ Z and σ X0 = σY0 × σ Z0 .
The encodings σ X and σ X0 are related by the following fundamental property:
Proposition 2 σ X0 ◦ σ X = 1 X .
Proof. We prove the claim by structural induction. The base case is obvious. If X = Y + Z , then we
have that
σ X0 ◦ σ X = (σY0 + σ Z0 ) ◦ σ 0 (n Y , n Z ) ◦ σ (n Y , n Z ) ◦ (σY + σ Z )
= (σY0 + σ Z0 ) ◦ (σY + σ Z ) = σY0 ◦ σY + σ Z0 ◦ σ Z = 1 X .
Finally, if X = Y × Z then
σ X0 ◦ σ X = (σY0 × σ Z0 ) ◦ (σY × σ Z ) = σY0 ◦ σY × σ Z0 ◦ σ Z = 1 X .
In what follows, given a function f : X → Y we shall denote with b
f the function σY ◦ f ◦ σ X0 .
Using the previous proposition, it is easy to prove the following
Corollary 3 Let f : X → Y , g : X 0 → Y 0 . Then
• if Y = X 0 then b
g◦ b
f = g[
◦ f;
• (b
f ,b
g ) = (\
f, g);

• (b
f |b
g ) = (\
f | g) ◦ σ (n X , n X 0 );

f | g).
• (b
f |b
g ) ◦ σ 0 (n X , n X 0 ) = (\

2.4. COMPUTABILITY IN AN ORDERED RING

2.4.4

23

Equivalence theorems

We firstly need a couple of technical lemmata:

Lemma 2 The derived functions of the form f : R l → R m contain the polynomial functions. If R
is a field, they contain the rational functions.

Proof. We just have to show that the thesis holds for the functions R l → R associated to polynomials;
the general case can be obtained by applying the (−, −) operator.
We work by structural induction on a polynomial p: if p is a variable or a constant α, the correpαq

sponding function is an identity or the function I −→ R, respectively, precomposed with a suitable
projection or terminal map. If p = p 0 p 00 , then by applying the operator (−, −) to the functions
associated to p 0 and p 00 and composing with ∗ : R 2 → R we obtain the function associated to p.
An analogous consideration can be made if p = p 0 + p 00 . If R is a field any rational function can be
easily obtained by inverting the denominator using (−)−1 .

Lemma 3 The derived functions contain the encodings.

Proof. Trivial, by structural induction. The base case is covered by identities, constant maps and
projections. The maps σ (i, j) and σ 0 (i, j) can be easily shown to be derived functions, and the
operations used in the inductive construction of σ X and σ X0 are those allowed when building derived
functions.
We can now state and prove our main theorem. Since the domains and codomains of the functions
computed in the BSS model are restricted to the powers of R, we have (as for recursive functions)
to encode the derived sets appearing in the domains and codomains of functions in D R using the
techniques developed in Section 2.4.3.

Theorem 7 Let F = {ϕ M : R l → R m | M is a BSS machine } be the set of functions computed by
machines over R in the BSS model, and G = { b
f | f : P → Q ∈ D R } be the set of distributively
computable functions whose domains and codomains have been encoded into powers of R. Then
F = G.

Proof. Let us prove that F ⊆ G, by building a derived function f : R l + N · R n → N · R n + R m
which8 emulates the behaviour of a given machine M with node set N̄ . By Lemma 2 we know that
we can freely use polynomial functions while building such a function.
8 Note that by distributivity N̄ × R n ∼ N · R n = R n + R n + · · · + R n (N times); we correspondingly use N -ary injections:
=
they can be easily defined in terms of binary ones.

CHAPTER 2. DISTRIBUTIVE COMPUTABILITY

24

We define f “piecewise” as follows (the sequence of arrows denotes functional composition):
inj1 ◦I (−)

f 0 : R l −−−−−−−−−−−−→ N · R n
injβ(1)

f 1 : R n −−−−−−−−−−−−→ N · R n
injβ(k) ◦gk

f k : R n −−−−−−−−−−−−→ N · R n

if k is a computation node

1 Rn

f k : R n −−−−−−−−−−−−→ R n × R n
h k ×1 R n

−−−−−−−−−−−−→ R × R n
≥×1 R n

−−−−−−−−−−−−→ (I + I ) × R n
δ −1

−−−−−−−−−−−−→ I × R n + I × R n
∼
=

−−−−−−−−−−−−→ R n + R n
(injβ − (k) | injβ + (k) )

−−−−−−−−−−−−→ N · R n

if k is a branching node

O(−)

f N : R n −−−−−−−−−−−−→ R m
and then f = ( f 0 | f 1 | · · · | f N ), understanding composition with the obvious injections into
N · R n + R m . A routine check shows that f acts on N · R exactly as the computing endomorphism
of M. Thus, since σ Rl = 1 Rl and σ R m = 1 R m , we have call[ f ]=ϕ M , so F ⊆ G.
Let now f : X → Y be a function of D R . As in the proof of Theorem 4, such a function has been
obtained by iterating a suitable derived function g : X + U → U + Y (i.e., f = call[ g ]). We shall
denote by h the loop X + U + Y → X + U + Y induced by g. It is clear that f is exactly the function
obtained applying h to an element of X until the generated orbit intersects Y .
By Corollary 3, we have that hbk = b
h k . Thus, if we can show that for any loop h : X + U + Y →
X + U + Y there is a machine computing b
h, we can build a new machine M with input space R n X ,
n
n
X
+U
+Y
Y
. The input map of M immerges the element of X encoded
output space R and state space R
in R n X into the encoding of the same element in R n X +U +Y ; the output map extracts the encoding of
an element of Y from its encoding in R n X +U +Y (such maps are obviously linear). The machine M
applies b
h to its state space, and then checks for the element represented in R n X +U +Y being in Y (recall
that such a check can be made simply by checking the nonnegativity of certain components of the
vector encoding the element). If it is not, M applies again b
h; otherwise, it moves to the output node.
Clearly, ϕ M = b
f.
In order to make complete the argument, we shall now show by structural induction that, for all
derived functions f : X → Y , b
f can be computed by a suitable finite dimensional machine. We shall
describe the machines informally; the details would just be cumbersome. Unless otherwise specified,
the input will be represented by a vector α (or a scalar α).
It is not difficult to check that the base case is covered by the following machines (we shall not
mention encodings when they are just the identity):
• the machines computing ∗ : R 2 → R and + : R 2 → R just output α1 α2 and α1 + α2 ,
respectively;
• the machine computing a constant pαq ◦ σ I0 : R → R outputs that constant;
• the machine computing σ I +I ◦ ≥: R → R 3 outputs h−1, 0, 0i if α < 0, and h0, 0, 0i if α ≥ 0;

2.4. COMPUTABILITY IN AN ORDERED RING

25

• the machine computing a first (second) projection just outputs the variables corresponding to
the first (second) component;
• the machine computing a first (second) injection outputs h−1, α, 0i (h0, 0, αi);
• the machine computing an identity outputs its input;
• the machine computing a terminal map outputs 0;
• the machine computing the inverse distributivity isomorphism on input hhα, β, γ i, δi outputs
hα, hβ, δi, hγ , δii.
If f = h ◦ g, then by Corollary 3 h[
◦g = b
h ◦b
g , so by connecting in series the machines
corresponding to b
g and b
h we obtain a machine which computes b
f.
0
00
0
If f = (g, h), with g : X → Y , h : X → Y (so Y = Y × Y 00 ), then we take a machine which
duplicates its input, runs b
g on the first copy and b
h on the second one, and finally outputs the two
results juxtaposed. Again by Corollary 3, this machine computes b
f.
If f = (g | h), with g : X 0 → Y , h : X 00 → Y (so X = X 0 + X 00 ), then we take a machine which
on input hα, β, γ i ∈ R × R n X 0 × R n X 00 checks if α < 0: in this case, it outputs b
g (β); otherwise, it
outputs b
h(γ ). One more time, Corollary 3 guarantees that the computed function is b
f . This completes
the proof.
As in the case of recursive functions, instead of restricting the class of distributively computable
functions we could enlarge F using the encodings. However, we can again prove that

b = {σ 0 ◦ f ◦ σ X | f : R n X → R n Y ∈ F}. Then F
b = DR .
Theorem 8 Let F
Y
b is trivially in D R (use Lemma 3, the fact F = G ⊆ D R , and closure of D R
Proof. Any function in F
with respect to composition). On the other hand, if f : X → Y ∈ D R then b
f ∈ G = F. But then
b 3 σ0 ◦ b
F
f ◦ σ X = σY0 ◦ σY ◦ f ◦ σ X0 ◦ σ X = f.
Y

We shall now give an example by mapping to a derived function the machine described in
[Blum, Shub & Smale:1989, p. 5] (in order to simplify the discussion we suppose that the machine
works on the reals, and we use the square instead of the absolute value of g k (x)). The machine has a
built-in constant c, and evaluates iteratively a given polynomial g on the input x until (g k (x))2 ≥ c.
There is one register and four nodes. The second node is a computation node which applies g and
moves to the third node, while the third node is a branching node which checks if the square of the
register is greater than or equal to c, moving to the output node in this case, or to the second node
otherwise.

CHAPTER 2. DISTRIBUTIVE COMPUTABILITY

26

Our mapping sends this machine to the function f : R + 4 · R → 4 · R + R defined as follows:
inj1

f 0 : R −−−−−−−−−−−−→ 4 · R
inj2

f 1 : R −−−−−−−−−−−−→ 4 · R
inj3 ◦g

f 2 : R −−−−−−−−−−−−→ 4 · R
1R

f 3 : R −−−−−−−−−−−−→ R × R
((−)2 −c)×1 R

−−−−−−−−−−−−→ R × R
≥×1 R

−−−−−−−−−−−−→ (I + I ) × R
δ −1

−−−−−−−−−−−−→ I × R + I × R
∼
=

−−−−−−−−−−−−→ R + R
(inj2 | inj4 )

−−−−−−−−−−−−→ 4 · R
1R

f 4 : R −−−−−−−−−−−−→ R
An input x generates the following orbit:
x 7→ hx, 1i 7→ hx, 2i 7→ hg(x), 3i.
Now f 3 works as follows:
g(x) 7→ hg(x), g(x)i 7→ hg(x)2 − c, g(x)i 7→
hh∗, ki, g(x)i 7→ hh∗, g(x)i, ki 7→ hg(x), ki 7→ hg(x), 2k + 2i,
where k is 0 if g(x)2 < c, 1 otherwise. In the first case we restart from node 2, obtaining
hg(x), 2i 7→ hg 2 (x), 3i
and so on; in the second case, we apply f 4 and we output g(x).

2.4.5

An application

We shall now apply Theorem 7 in order to obtain a new structural characterization à la Kleene of the
functions R l → R m computable in the BSS model. The characterization is based on iteration rather
than on recursion (a structural characterization based on recursion was given in [Blum, Shub & Smale:1989]),
and it is clearly derived from the operations available in a distributive category.
Definition 9 The set Kν of general ν-recursive functions over R is the smallest set of functions
R l → R m containing the polynomial functions, and closed under the following constructions:
1. (composition) given f : R l → R m and g : R m → R n , form f ◦ g;
2. (juxtaposition) given gi : R m → R n i (1 ≤ i ≤ k), form (g1 , g2 , . . . , gk ) : R m → R
3. (cases) given f, g : R m → R n form h : R × R m → R n , defined by

f (β) if α < 0
h(α, β) =
g(β) if α ≥ 0

P

1≤i≤k

ni

;

2.4. COMPUTABILITY IN AN ORDERED RING

27

4. (ν-operator) given f : R × R n → R × R n , if for every α ∈ R n there is a least n α such that
f n α (−1, α) = hρα , β α i with ρα ≥ 0, then form ν f : R n → R n by setting ν f (α) = β α .
If we consider also partial functions, we can relax the condition given on iteration, and for any
f : R × R n → R × R n define ν f (ν f (α) is undefined if there is no n α as in Definition 9). The
other operations should be redefined as usual. We shall speak in this case of the partial ν-recursive
functions over R.
Theorem 9 Kν = G.
Proof. We firstly prove left-to-right inclusion. We already know that all polynomials are derived
functions. Composition and juxtaposition have corresponding categorical operators. Construction by
cases on f, g : R m → R n can be obtained as follows:
δ −1

≥×1 R m

( f | g)

R × R m −−−−→ (I + I ) × R m −−→ R m + R m −−−→ R n .
Given f : R × R n → R × R n , consider the functions
g

:

inj1
p−1q×1 R n
Rn ∼
= I × R n −−−−−−→ R × R n −−→ R × R n + R n

h

:

R × Rn −
→ R × R n −−−−−→ R × R × R n −−−−−−→ (I + I ) × R × R n

f

δ −1

1 R ×1 R n

≥×1 R×R n

1 R×R n +proj2

−−→ R × R n + R × R n −−−−−−−→ R × R n + R n .
It is a matter of calculation to show that call[ R n , R × R n , R n , (g | h) ] = ν f .
Some more work is required in order to prove that G ⊆ Kν . We apply structural induction
again, following the lines of the proof of Theorem 7. The function computed by iterating the loop
h : X + U + Y → X + U + Y induced by a derived function g : X + U → U + Y can be obtained
by applying the ν operator to a suitable function k : R × R n X +U +Y → R × R n X +U +Y . We shall define
k by juxtaposing the functions k 1 : R × R n X +U +Y → R and k2 : R × R n X +U +Y → R n X +U +Y described
below, which are clearly in Kν 9 :
(
0
if β1 ≥ 0
k1 (α, β) =
−2 otherwise
(
h−1, −1, β3 , . . . , βn X +U +Y i if α = −1
k2 (α, β) =
b
h(β)
otherwise.

Note the usage of the “control variable” α. When k = (k 1 , k2 ) is applied, we check whether α = −1
(first iteration). In this case, we set the first two coordinates of the encoding of (X + U ) + Y to −1:
this forces the element encoded in R n X +U +Y to be an element of X . At the same time, α is set to
−2, so that the subsequent iterations will apply b
h leaving α undisturbed, unless the element encoded
in β becomes an element of Y (i.e., β1 ≥ 0), in which case α is set to 0, stopping iteration (and
necessarily β is left undisturbed by b
h). Since g terminates for every element of X , and the iteration of
b
h necessarily starts from the encoding of an element of X , the termination condition on g implies the
termination condition required by the operator ν, which can actually be applied to k. Precomposition
and postcomposition of νk with trivial maps preparing the input and extracting the output give as a
result the function call[ g ].
This machinery is actually necessary (similarly to what happened in the proof of Theorem 4):
If we did not force the presence of the encoding of an element of X at the first iteration, we could
9 We are assuming, without loss of generality, that X + U + Y is encoded as (X + U ) + Y .

CHAPTER 2. DISTRIBUTIVE COMPUTABILITY

28

iterate over an element of U , over which we could not guarantee termination. The precomposition
and postcomposition would in the end produce a (total) function R n X → R n Y , but the ν operator
would have been applied incorrectly.
We are left to prove that for any derived function f : X → Y we have b
f ∈ Kν . We use structural
induction:
• the functions ∗ : R 2 → R, + : R 2 → R and the constants are obviously representable as
polynomials, and thus in Kν ;

• the function σ I +I ◦ ≥: R → R 3 can be obtained by juxtaposition and cases:
(
h−1, 0, 0i if α < 0
(σ I +I ◦ ≥)(α) =
h0, 0, 0i
if α ≥ 0;
• the projections can be obtained again by juxtaposition, discarding the variables which correspond to the discarded component;
• the first (second) injection outputs h−1, α, 0i (h0, 0, αi) on input α;
• the terminal map is the constant polynomial 0;
• the identities and the inverse distributivity isomorphism can be easily obtained by juxtaposition
of polynomials.
The functions obtained by application of composition and (−, −) are by definition inside K ν ; if
f = (g | h), with g : X 0 → Y e h : X 00 → Y (so X = X 0 + X 00 ), we define a function by cases using
b
g ◦ proj1 , b
f ◦ proj2 : R n X 0 × R n X 00 → R n Y . The resulting function is exactly b
f . This completes the
proof.
The obvious consequence of the previous theorem is that the ν-recursive functions coincide with
the functions computed in the BSS model:
Corollary 4 Kν = F.

Chapter 3

Automata
In this chapter we shall introduce the notion of morphism of automata. Since any function f :
X + U → U + Y can be seen as a one-letter automaton with state space X + U + Y , the operator
call[ − ] will allow to obtain, from automata whose state space has the form X +U + Y and satisfying
certain conditions, automata with state space X +Y , thus realizing an abstraction of the time and space
necessary to compute a function. The notion of morphism will then enable us to “invert” the call[ − ]
operator, because the former automaton will represent the latter in the sense of [Knuth:1966].
As in the previous chapter, the description will be kept at an elementary level: only a small amount
of category theory will be used, and for the time being we shall use as “computational universe” Set,
the familiar category of sets and functions. We assume once for all that a set of basic functions (i.e.,
a distributive graph) has been chosen, and that all functions used are distributively computable.
Firstly we shall give the basic definitions, some of which are probably known to the reader. Then
we shall prove a series of simple but nontrivial theorems about morphisms of automata, in order to
give an intuition about their nature and to prepare the ground for the refinement theorem, which will
be proved in its most general form in Chapter 4.

3.1 Basic definitions
Definition 10 Let M be a monoid and X an M-automaton; that is, a set X endowed with an action
of M
α
α : M × X → X, (m, x)7→m · x;
the action is required to satisfy the usual axioms m 2 · (m 1 · x) = (m 2 m 1 ) · x and 1 · x = x. Define the
category Trans(X) (the transition category of X) as follows:
(i). objects are states (that is, elements) of X ;
(ii). arrows from x to y are state transitions; that is, elements m ∈ M such that m · x = y;
(iii). composition is monoid multiplication.
Note that since each arrow of a transition category is determined by an element m ∈ M and by a
domain and a codomain x, y ∈ X , many distinct arrows will be named by the same element of M.
This fact should cause no confusion, but we shall reserve the possibility of writing arrows in the form
m
x −
→ y whenever necessary. If M is the monoid of natural numbers N, the action α is completely
specified by a function X → X , which we call again α for sake of semplicity.
29

CHAPTER 3. AUTOMATA

30

We shall denote with Ind(M) the set of the indecomposable elements of M, i.e., the elements
m ∈ M such that m = m 0 m 00 implies m 0 = ε or m 00 = ε. These are also all and only the minimal
elements with respect to the prefix (or suffix) preordering on M \ {ε} (in this preordering, m ≤ n iff
n = mm 0 ). Not amazingly, if X is an M-automaton we shall call the arrows of Trans(X) which are
labelled by elements of Ind(M) atomic.

3.1.1

Pseudofunctions

Certain automata on N related to functions f : X + U → U + Y can compute functions by iteration.
To this purpose, in [Khalil & Walters:1993] the notion of pseudofunction has been introduced:
Definition 11 A functional processor or pseudofunction from X to Y is an N-automaton with state
space of the form X + U + Y and action α such that
(i). for each y in Y we have α(y) = y;
(ii). for each x in X there exists a natural number n x such that α n x (x) ∈ Y .
A pseudofunction α defines a function call[ α ] : X → Y (by iteration) as follows:
call[ α ](x) = α n x (x).
We shall call U the set of local states of the pseudofunction α, or the hidden states of the function
call[ α ].
Of course, any function of the form f : X + U → U + Y induces a pseudofunction
( f | inj2 )

inj2

ϕ : X + U + Y −−−−−→ U + Y −−→ X + (U + Y )
(something which we exploited in the proofs of several theorems of Chapter 2), and call[ f ] =
call[ ϕ ].

3.2 Morphisms
Our notion of morphism of automata [Sabadini, Vigna & Walters:1993a] is a generalization of the
morphisms of automata given by a function on states which preserves the action up to substitution of
a letter with a fixed word. Indeed, in our morphisms this substitution is state-dependent.
Definition 12 A morphism of automata (or, in short, a mapping) from X to Y , where X is an Mautomaton and Y is an N -automaton, is a functor from Trans(X) to Trans(Y ).
If M = A∗ and N = B ∗ (i.e., M and N are free monoids) a mapping F from X to Y is given by
two functions (which we shall call ambiguously with the same name)
F :X →Y
and
F : X × A → B∗
a

which satisfy the following condition: if a ∈ A and x −
→ x 0 is an arrow of Trans(X), then
F(x,a)

F(x) −−−−→ F(x 0 ) is an arrow of Trans(Y ).
The following theorem partially characterizes isomorphic automata:

3.2. MORPHISMS

31

Theorem 10 Let X and Y be automata on the monoids M and N , and let X be isomorphic to Y in
the sense of Definition 12. Then | Ind(M)| = | Ind(N )|, and if Ind(M) is a set of generators then the
isomorphism is induced by a family of bijections {ϕ x : Ind(M) → Ind(N )}x∈X .
Proof. Let F : X → Y be an isomorphism. Then F is a bijection on objects, i.e., a bijection between
the sets X and Y , and a bijection between sets of arrows. Firstly, let us show that F preserves and
n1
n2
m
m
→ F(x 0 ), then
reflects atomicity. If x −
→ x 0 is atomic, and F(x −
→ x 0 ) = F(x) −
→y−
m

n1

m

n2

m1

m2

→y−
→ F(x 0 )) = x −→ F −1 (y) −→ x 0
x−
→ x 0 = F −1 (F(x −
→ x 0 )) = F −1 (F(x) −
with

m1

n1

F(x −→ F −1 (y)) = F(x) −
→y

and

m2

n2

F(F −1 (y) −→ x 0 ) = y −
→ F(x 0 ),

so that necessarily n 1 = ε or n 2 = ε. Thus, F preserves atomicity. But symmetrically this is true for
F −1 , so F also reflects atomicity.
We shall denote with ϕx the restriction of F to the atomic arrows outgoing from x. Since X
and Y are complete automata, ϕ x is a bijection between Ind(M) and Ind(N ). In particular, for each
indecomposable m we have
ϕx (m)

m

F(x −
→ x 0 ) = F(x) −−−→ F(x 0 ).
Finally, if Ind(M) is a set of generators then every arrow can be written as a composition of a finite
number of atomic arrows, and the effect of F can be computed by composition knowing just the
bijections ϕx .
Corollary 5 Let X and Y be isomorphic automata on the free monoids A ∗ and B ∗ . Then |A| = |B|.
Note that we cannot claim that X and Y are isomorphic as automata on A ∗ , in the classical sense.
A simple counterexample follows:
·

·
a
a,b

3.2.1

·

∼
=

b

a

·

b

a

b
a,b

·

a

·

b

Refinement

In [Sabadini, Vigna & Walters:1993b] a particular case of mapping, named refinement, is studied.
The notion of refinement plays a particularly important rôle in the theory of distributive computability because the automata built on distributively computable functions admit refinements into the automata built on the relative derived functions. In particular, we shall see that in a precise sense
pseudofunctions are refinement of functions. The notion of refinement is also essential in any model
of distributed and concurrent systems; the quoted reference gives some motivation to this purpose.
Definition 13 A mapping F : X → Y is a refinement iff the functor F : Trans(X) → Trans(Y ) is
a full inclusion.
In other words, in order to give a refinement of X one has to specify a bigger system Y which has
a restriction to a system isomorphic to X. If M = A ∗ and N = B ∗ , the additional condition for F
being a refinement is that the function induced by F between Hom(x, x 0 ) and Hom(F(x), F(x 0 )) is
a bijection, and that the function between the state spaces in injective.

CHAPTER 3. AUTOMATA

32

Note that non all full inclusions in Trans(Y ) can have as domain a category of the form Trans(X).
For instance, consider the automaton
0

a

a

1

a

2

a

The full subcategory contaning the objects 0 and 1 has just one arrow 0 −
→ 1; thus, it cannot be of the
form Trans(X).
In order to give some intuition about the nature of refinements, we shall relate them with simpler
properties. We start by giving the following
m

Definition 14 An expansive mapping is an inclusion F of Trans(X) in Trans(Y ) such that if F(x −
→
n
m
x 0 ) = F(x) −
→ F(x 0 ), where x −
→ x 0 is atomic, there are no x 00 ∈ X , n 0 ∈ N such that n 0 is a
n0

nontrivial suffix of n and F(x) −
→ F(x 00 ).
When an expansive mapping is applied to an atomic transition, the set of states spawned 1 by the
resulting arrow lies entirely outside of the image of X, except for the initial and final states (which
are the image of the domain and of the codomain of the atomic transition). Indeed, if M = A ∗ and
N = B ∗ we can restate Definition 14 as follows:
1. Y = X + U for some set U ;
2. if F(x, a) = bn · · · b1 ∈ B ∗ , then bk · · · b1 · x ∈ U for k = 1, 2, . . . , n − 1.
Expansiveness and fullness are related by the following
Theorem 11 Let X and Y automata on M and N , respectively. If a mapping F : X → Y is a
refinement, then it is expansive.
m

n

Proof. Let m be indecomposable, and F(x −
→ x 0 ) = F(x) −
→ F(x 0 ). Let n 0 be a suffix of n, and
n0

n 00

F(x) −
→ F(x 00 ). Then n = n 00 n 0 , and F(x 00 ) −→ F(x 0 ). By fullness of F, there are m 0 , m 00 ∈ M such
m0

n 00

n0

m 00

→ F(x 00 ) and F(x 00 ) −→ F(x 0 ). By
that the arrows x −→ x 00 and x 00 −→ x 0 have as image F(x) −
composition, we get
m0

n 00

n0

m 00

n

m

→ F(x 0 ) = F(x −
→ x 0 ),
→ F(x 00 ) −→ F(x 0 ) = F(x) −
F(x −→ x 00 −→ x 0 ) = F(x) −
and by faithfulness m = m 00 m 0 . Thus either m 0 = m and m 00 = ε, or m 0 = ε and m 00 = m. In both
cases, n 0 (which is the image of m 0 ) is a trivial suffix of n.
This theorem cannot be reversed. Consider the mapping between the following two automata
b

·

a,b

→

a

0

1

a

b
bab

where · 7→ 0, a 7→ a and b 7→ b2 . It is expansive, but not full (0 −−→ 0 has no counterimage). There
is however a relevant case in which we can invert Theorem 11:
Theorem 12 Let X and Y be N-automata. If a mapping F : X → Y is expansive, then it is a
refinement.
1 If the atomic decomposition of the image of an atomic transition is not unique, the set is not necessarily unique.

3.2. MORPHISMS

33
k

Proof. If F is not a refinement, consider states x, x 0 ∈ X and an arrow F(x) −
→ F(x 0 ) which
0
is not the image of an arrow from x to x . Assume without loss of generality that k is minimal.
n

1

Let F(x) −
→ F(x 00 ), n 6= k, be the image through F of x −
→ x 00 . If k > n, then necessarily
k−n

F(x 00 ) −−→ F(x 0 ) is not in the image of X, which contradicts the minimality of k. But then n > k,
which contradicts expansiveness.

3.2.2

Pseudofunctions and refinement

The fundamental relation between computation by iteration and refinement is the fact that, given a
pseudofunction α : X + U + Y → X + U + Y with the property α n (x) ∈ U + Y for all n (without
loss of generality), we can define an automaton X with state space X + Y which computes call[ α ] in
one step, and which admits a refinement in the automaton defined by α, refinement which is induced
by the inclusion X + Y → X + U + Y (the claim will be proved in Chapter 4, in the context of
extensive categories). In a slogan: the inverse of the application of call[ − ] is a refinement. This fact
generalizes to the following
Theorem 13 Let X be an A ∗ -automaton whose action is defined using functions distributively computable on a basic set. Then X admits a refinement in an A ∗ -automaton whose action is defined using
derived functions.
Proof. For each a ∈ A, α(a, −) : X → X admits a refinement to a pseudofunction ϕa : X + Ua +
X → X + Ua + X . Now define
X
Ua .
Y =I+X+
a∈A

The action of b 6= a on Ua is the unique function Ua → I , while on X and Ua is induced in an
obvious way by ϕa . It is immediate to show that the inclusion X → Y induces a refinement.

3.2.3

Examples

Representations. The existence of a refinement X → Y , where X and Y are N-automata, exhibits
Y as a representation of X in the sense of [Knuth:1966].
An IMP(G) Interpreter. The IMP(G) interpreter described in [Khalil & Walters:1993] is easily
seen to be a refinement of each particular IMP(G) program.
Independent actions are not necessarily parallel. If we consider a fixed machine Y , we may
think of refinements of other machines X in Y as implementations of abstract machines X in a
system Y . The class of abstract machines has unbounded parallelism; however, in relation to Y it
is possible to consider questions of resources. We can make the distinction between actions of X
being “independent” and being “parallel”. Actions are independent if they are parallel in the abstract
machine X. Actions are parallel if they are parallel in the system Y . The following example can
be expressed by saying that independent actions in an abstract machine may not be parallel in the
implementation.
Given two automata X, Y , both on {a}∗ , suppose that there are refinements of X to X 0 and Y
to Y 0 , where X 0 = X + U and Y 0 = Y + U , the meaning being that the set U is the state space
of some temporarily used (and reset after use) resource like a scratch pad, or printer. Then the
synchronous parallel product X × Y of X and Y , which has state space X × Y and action of {a} ∗

CHAPTER 3. AUTOMATA

34

defined componentwise, may be refined to an automaton in which there is only one resource U whose
use is scheduled between X and Y . The state space would be Z = X Y + U Y + X Y + XU . The two
letters b, c would act respectively on the first two and on the last two summands, applying ha, 1i and
h1, ai, respectively (a trap state would complete the automaton in the obvious way). The injection of
X Y as first summand of Z would then define a refinement, which would schedule the parallel action
ha, ai to bc.
Shutdown. Consider a refined description of a system in which a new, destructive action can happen. This is a typical case of a sudden shutdown. We expect that the system can, at any time, be shut
down, thus moving into a state which was impossible to reach before. In this case, the refinement
space is formed by adding a single element, and a new letter to the alphabet; it sends to the new state
any other state. The behaviour of the machine, if we ignore the shutdown state, is unmodified, which
is exactly reflected in our definition of refinement.

3.2.4

Abstraction

Refinements introduce new information in the description of an automaton. In this section, on the
contrary, we shall discuss how to reduce it.
Definition 15 A mapping F : X → Y is an abstraction iff the functor F : Trans(X) → Trans(Y )
is surjective on objects and arrows.
An abstraction is essentially a quotient of automata. Let us consider the following example: for
any automaton X on a free monoid, any partition of the states of X in two classes (linked by at least
one transition) induces an abstraction F having as codomain the automaton Y specified here:
a

0

1
a

The abstraction maps the states in each class respectively to 0 and 1. All atomic transitions which
do not change the class are mapped to the identity of 0 or 1, respectively, while an atomic transition
which crosses the partition boundary is mapped to the suitable a-transition of Y . As a result, each
an

arrow of Trans(X) is mapped to an arrow of the form x −→ y (where x, y = 0 or 1); the exponent
n is equal to the number of changes of class that happened while the state transformations induced
by the arrow were applied. In other words, F forgets the information about the internals of the
automaton, and allows us only to observe two states, and the transitions between those two states.
Note that not all abstractions can be inverted by a refinement. Indeed, an epimorphism F :
Trans(X) → Trans(Y ) does not necessarily have a section which is a full inclusion. The following
counterexample shows this fact:
a

0

b

1

·

→

a

c

b

The mapping is defined by a, b 7→ c. Any section of it has to send c to a or b. The inclusion cannot
then be full because of the arrows (ba)n or (ab)n , respectively.
The following example shows instead a case in which refinement of the abstraction is possible.
Consider the mapping
0

a

1

a

a
a

→

0

1
a

3

a

2

3.3. PARTIAL SPECIFICATION

35

defined by n 7→ n/2 and by
a

0−
→1
a
1−
→2
a
2−
→3
a

3−
→0

ε

7→
7→
7→

0−
→0
a
0−
→1
ε
1−
→1

7→

1−
→ 0.

a

The refinement x 7→ 2x, with
a

x−
→y

7→

a2

2x −
→ 2y

(x, y = 0 or 1),

is a section of the given abstraction.
Note that having a refinement as a section is a property of a specific abstraction, not of the
automata involved. Indeed, using the same two automata of the previous example, consider the
abstraction F defined by n 7→ (n mod 2), with
a

x−
→y

7→

a

(x mod 2) −
→ (y mod 2);

it is easy to see that there is no inversion through a refinement. Indeed, in order to invert F we must
send 0 and 1 in states x and y such that the shortest word in Hom(x, y) (or Hom(y, x)) is a 3 . Since
a
a
F preserves the word length, it is not possible to find a section for 0 −
→ 1 (1 −
→ 0, respectively).

3.2.5

Input/Output

In this section we note that our notion of morphism allows to specify elegantly output of automata.
Our basic assumption is that output is state-dependent, i.e., it depends both on the state and on the
monoid element which is acting.
Definition 16 An automaton on M with output in N is an M-automaton X endowed with a mapping
O X : X → N (where N is seen as a one-state automaton).
The meaning of this definition is that for each state x and each element m of M there is an element
of N which represents the output of the action of m in the state x. The functoriality equations tell us
that no output is possible if no action is specified, and that the output of the composition of actions is
the composition of the output of the single actions.

3.3 Partial specification
Partially specified automata are automata on a free monoid whose action is defined, for each letter in
the alphabet, only on a part of the state space. The non-completeness of information fits flawlessly
in our theory, and it is particularly useful when specifying all details about trap states would be
cumbersome.
Definition 17 A partially specified automaton on A ∗ is a set X , together with, for each a ∈ A, a
decomposition X = X a + Ua and a function2
αa : X a → X.
These functions induce a partial action of A ∗ on X . Again, define the category Trans(X) as follows:
2 It could be argued that one could define a partial specification using functions α : X → X + I ; but even in the general
a
case we shall be working in an extensive category, and in such a category the two concepts coincide.

CHAPTER 3. AUTOMATA

36
(i). objects are states (that is, elements) of X ;

(ii). arrows from x to y are allowable state transitions, i.e., words w ∈ A ∗ such that w · x = y;
(iii). composition is monoid multiplication in A ∗ .
Note that we did not state the definition of partial specification for an automaton on an arbitrary
monoid M. In that case, we have to specify a decomposition X = X m + Um for each m ∈ M, but the
decompositions are not free (if m = m 1 m 2 , and the decompositions associated to m 1 and m 2 allow
to apply them in sequence from a certain state, then the decomposition associated to m has to include
that state).
It is clear that the definition of mapping of automata given in the previous section is still perfectly
valid (being built upon the notion of transition category). Thus, we can formulate our first
Proposition 3 Each partially specified automaton X admits a refinement in an automaton Y on the
same monoid.
Proof. Let Y = X + I , and define the action of Y extending the action of X via the unique map
Uα + I → I (i.e., we are adding a trap state to X). The inclusion X → X + I then induces a full
inclusion Trans(X) → Trans(Y ).
We already showed that not all full subcategories of Trans(Y ) are of the form Trans(X) for an
automaton X. However, the contrary is true for partially specified automata (and gives the main
motivation for introducing them):
Theorem 14 Let Y be a partially specified automaton on B ∗ . For each full subcategory C ⊆
Trans(Y ) there is a partially specified automaton X such that C ∼
= Trans(X).
Proof. For each y, y 0 ∈ C consider the set
w0

w

w 00

N(y,y 0 ) = {y −
→ y 0 | @ y 00 ∈ C, y −→ y 00 , y 00 −→ y 0 such that w = w 00 w 0 },
where w, w 0 , w 00 6= ε. Define a partially specified automaton X on the (not necessarily finite!)
alphabet
X
A=
N(y,y 0 ) ,
y,y 0 ∈C

with an action on X = |C| such that
X

w

y−
→y0

= {y}

w

and obviously (y −
→ y 0 ) · y = y 0 . The mapping F : Trans(X) → C which is the identity on objects
w
w
and sends an element y −
→ y 0 ∈ A to the arrow y −
→ y 0 of C is trivially full. The crucial point of the
proof is showing its faithfulness.
u
v
Let x −
→ x 0, x −
→ x 0 be arrows of Trans(X) which are mapped to the same arrow of C. This
means that
wm

w2

w1

u = (wm−1 wm−2 · · · w1 · x −−→ x 0 ) · · · (w1 · x −→ w2 w1 · x)(x −→ w1 · x)
and

zn

z2

z1

v = (z n−1 z n−2 · · · z 1 · x −
→ x 0 ) · · · (z 1 · x −
→ z 2 z 1 · x)(x −
→ z 1 · x),
with moreover
wm wm−1 · · · w1 = z n z n−1 · · · z 1 .

3.3. PARTIAL SPECIFICATION

37

If any of the two arrows is an identity, so is the other one; otherwise, without loss of generality we
t
can assume z 1 = tw1 . Since C is full, it contains the arrow w1 · x −
→ tw1 · x. But then necessarily
t = ε and w1 = z 1 . The result follows by induction on n + m.
The fullness hypothesis is necessary, as the following counterexample shows: consider the automaton
a

·

a

·

a

·

a

·

·

a

and the subcategory C of its transition category generated by
a2

a

·

·

a

·

·

·

a2

a2

∼ C. Since the generating
Suppose there is a partially specified automaton X such that Trans(X) =
arrows are atomic in C, the same must be true of their counterparts in Trans(X). But this implies that
they are one-letter transitions; and the equation between the composition of the three upper arrows
and the composition of the two lower arrows would imply that a three-letter word is equal to a twoletter word, which is clearly impossible.
Note that, as it happens for algebraic structures such as groups, a finitely generated category
Trans(X) (with “finitely generated” we denote the finiteness of both X and its alphabet A) can
have (full) subcategories which are not isomorphic to any transition category of a finitely generated,
partially specified automaton, even if X is completely specified. For instance, if we consider the
following automaton,
a

0
b

b
b

1

a

2

a

any partially specified automaton X such that Trans(X) is isomorphic to the full subcategory generated by 1 and 2 must have an infinite alphabet. (In this specific case X can be taken to be fully
specified; more generally, whenever the cardinality of the set of letters enabled in x is constant for all
x ∈ X, X can be always turned into an isomorphic, fully specified automaton.)
The full subcategory generated by 0 and 2 provides another interesting example, because it is
isomorphic to a finitely generated, completely specified automaton. This does not happen in general,
as the following example shows:
a

0
b

1

b
a

2

a,b

3

a,b

The full subcategory generated by 1 and 2 has as alphabet a countable set whose action is only defined
on 1.

CHAPTER 3. AUTOMATA

38

3.4 A Categorical Note
We would like to mention that what we exposed in this chapter can be embedded into a very general
view. In what follows we shall use freely a series of categorical concepts.
It is clear that, given an M-automaton X, there is a “forget domain and codomain” functor
m
Trans(X) → M which sends an arrow x −
→ x 0 to m ∈ M. The important idea, developed by
F. W. Lawvere and A. Kock during seminars held in 1971 [Lawvere] is that this functor is not arbitrary, but it is rather a discrete opfibration. Indeed, every discrete opfibration of the form F : C → M
gives rise to an M-automaton X such that Trans(X) ∼
= C. The unique lifting property tell us exactly
that given a state (an object x of C) and an arrow of M (an element m ∈ M) there is a unique arrow
going out of x which is projected by F on m. Since we have already seen that the output in N of an
automaton can be specified by a functor O X : Trans(X) → N , an input/output automaton can be
defined as a span in Cat, i.e., as a diagram
C

N

M

where the “left leg” of the span is a discrete opfibration. If N = {ε}, we get an automaton without
output. Composition of automata with input/output is then defined using the following standard
pullback construction:
C00

C0

C

N
M
P
Functors between transition categories which commute with the legs of the respective spans form the
2-cells of a bicategory of input/output automata, whose objects are small categories (or monoids) and
whose arrows are spans in Cat whose left leg is a discrete opfibration.3 The mappings we defined are
a generalization of such 2-cells, because no commutation condition is imposed.
If instead of monoids M and N we consider arbitrary small categories, we have that the generalized action of the “input category” is not defined everywhere, but rather each state of the automaton
belongs to a certain class (where the classes are the object fibres of the left leg) on which a certain
set of action is defined—i.e., partial specification. The obvious consideration that the identity is a
discrete opfibration exhibits any partially specified automaton X as a span
Trans(X)

Trans(X)

{ε}

Thus, the restriction to free monoids for partially specified automata finds its natural lifting in the
context of automata on categories, rather than monoids.
3 Spans form a bicategory (see [Borceux:1994]), and discrete opfibrations are closed under composition and pullback along
an arbitrary functor.

Chapter 4

The general theory
In this chapter we are going to describe the theory of distributive computability in its most general form. We shall assume a working knowledge of the basics of category theory (category, functor,
equivalence, sum, product, and pullback); suitable references are [Mac Lane:1971] and [Borceux:1994].
The material is divided in three parts: an introduction to distributive categories, which contains a
description of the free distributive category on a distributive graph (whose explicit construction and 2categorical properties are given here for the first time); a review of the basics of extensive categories,
including theorems of Carboni, Khalil, Lack and Walters, followed by a series of new results about
iteration; finally, a proof of the refinement theorem (see Section 3.2.2) in the context of the automata
internal to a given extensive category.

4.1 Distributive categories
Definition 18 A distributive category is a category with finite sums (coproducts) and products such
that the products distribute over the sums, i.e., such that the canonical arrow
δ = (1 X × inj1 | 1 X × inj2 ) : X × Y + X × Z → X × (Y + Z )
has an inverse. A distributive functor is a functor which preserves finite sums and products.
Distributive categories are essential, in our treatment, because they provide categories of (free)
syntax for the definition of data types and programs in the language IMP(G). We start by giving some
examples of data types in a distributive category, and then we introduce the construction of the free
distributive category on a distributive graph, which provides the abstract definition for an IMP(G)
program.

4.1.1

Data types

We present briefly here some examples from [Walters:1989a] which show how data types can be
described using the syntax of a distributive category. Several more examples can be found in the
quoted reference.
Stacks
The archetypical example of a data type is that of a stack of elements of some type (for instance,
integers). Here we shall consider an object X , and we shall say that a stack of X is an object S
39

CHAPTER 4. THE GENERAL THEORY

40
endowed with specified arrows

push : I + X S → S
pop : S → I + X S
which are inverses. Intuitively, the “push” arrow breaks into two arrows 1 → S and X S → S. The
first one creates a new stack (in Set, an arrow 1 → S is just an element of S), while the second one
corresponds to the usual meaning of “pushing data onto an existing stack”. The “pop” arrow can have
two outcomes: either ∗, the only element of I (in Set), or a stack and an element of type X . The fact
that the push and the pop arrows are inverse just tell us that popping a new stack gives an error, that
pushing and popping gives back the same stack and the element just pushed.
Moreover, it is possible “solve” symbolically the
S∼
= (I − X )−1 ,
= I + X S, obtaining S ∼
Pequation
k
∼
which once expanded in a power series, gives S = k≥0 X , which is a possible realization of a stack
of type X if our category has countable
P sums.
It is also important to note that k≥0 X k is the formula which gives the free monoid on X (for
the definition of monoid in a category and the proof of the formula, see [Mac Lane:1971]). The
free monoid is given in Set by the sequences of elements of X , were composition is concatenation.
Thus, the algebraic and the combinatorial view of the data type coincide, in the sense that a possible
algebraic realisation of the data type satisfies its equational definition.
Binary trees
Another fundamental data type is given by the binary trees labelled by X . In this case, we have an
object B and two arrows
break : B → I + B X B
make : I + B X B → B
which are again inverses. Intuitively, the “make” arrow builds a new binary tree from a label and
given left and right subtrees, while the “break” arrow takes a binary tree and gives back its top label
and its two subtrees. The properties of binary trees are derivable from the fact that these two arrows
are inverses.
Once more, it is possible “solve” symbolically the equation P
B ∼
= I + B X B, obtaining X B 2 −
∼
∼
B + I = ∅, which, once expanded in a power series, gives B = k≥0 Ck X k , where the C k ’s are the
Catalan numbers, i.e., the number of binary trees with k nodes. P
We note that, analogously to the previous case, the formula k≥0 Ck X k gives the free X -motor,
an algebraic structure (a monoid with an action of X ; for definition, properties, and a proof of the
formula, see [Kasangian & Vigna:1991b]) which in Set is given by the trees labelled by elements of
X (composition is collation of the root); the same comments of the previous case apply.

4.1.2

The free distributive category on a distributive graph

Recall that a +/×-algebra is an algebra having two constants 0, 1 and two binary operators + and ×.
A distributive term is a term of the free +/×-algebra on {x}. For a distributive term t, we denote by ϕ t
the number of occurrences of generators it contains (for “free places”). Given a set A, a distributive
term t and a list of ϕt elements ai ∈ A, by substitution (following the natural order inside the term)
we obtain a term t[a1 , a2 , . . . , aϕt ] of the free +/×-algebra on A, i.e., a distributive expression on A.
The topos of distributive graphs is the presheaf topos SetG . The objects of G are given by
{∗} + T 2 , where T is the set of distributive terms. For each object ht, ui of G there are ϕt + ϕu arrows
named d1 , d2 , . . . , dϕt , c1 , c2 , . . . , cϕu which go from ht, ui to ∗.

4.1. DISTRIBUTIVE CATEGORIES

41

Given a distributive graph (i.e., a functor) G : G → Set, G(∗) is called the set of objects of the
graph (denoted by A, B, . . .), while the sets G(ht, ui) are the sets of arcs (denoted by a, b, . . .). Every
arc a ∈ G(ht, ui) has an assigned “source” t[G(d1 )(a), . . . , G(dϕt )(a)] and “target” u[G(c1 )(a), . . . , G(cϕu )(a)],
which are both distributive expressions on the objects of G. In other words, a distributive graph is
given by a set of objects A and by a directed graph whose vertices are the distributive expressions
on A (note that we admit multiple arcs and loops, following the notation of [Knuth:1973]). Morphisms (natural trasformations) are maps between sets of objects and between sets of arcs which
preserve the source and target of an arc (the map on objects inducing by substitution the map on
vertices). This shows that the topos SetG is indeed the category of distributive graphs in the sense of
[Walters:1992b].
The essentially equational case.
In order to keep the notation to a minimum, we shall first describe the construction in the context
of distributive categories with chosen sums and products, with functors which strictly preserve the
structure (the resulting algebraic theory is thus essentially equational). Then, we shall introduce the
formal modifications which are necessary in order to handle the more general case.
If D is a distributive category with chosen sums and products (we shall denote in general objects
of a category with X , Y , . . . and arrows with f , g, . . . ) and X 1 , X 2 , . . . , X ϕt are objects of D, the
term t[X 1 , . . . , X ϕt ] of the free +/×-algebra on the objects of D can be interpreted in D, giving an
object t D [[X i , . . . , X ϕt ]] ∈ |D|. Moreover, if F : C → D is a distributive functor (in the sense that it
preserves the chosen sums and products), we have
F(t C [[X i , . . . , X ϕt ]]) = t D [[F(X i ), . . . , F(X ϕt )]].
Let now Dist• be the category of small distributive categories (with chosen sums and products,
and with functors strictly preserving the structure). We describe a forgetful functor U : Dist • → SetG
by the following equations:
(i). U(D)(∗) = |D|;
(ii). U(D)(ht, ui) =

X

D(t D [[X 1 , . . . , X ϕt ]], u D [[Y1 , . . . , Yϕu ]]);

X i ,Y j ∈|D|

(iii). U(D)(di )( f : t D [[X 1 , . . . , X ϕt ]] → u D [[Y1 , . . . , Yϕu ]]) = X i ;
(iv). U(D)(c j )( f : t D [[X 1 , . . . , X ϕt ]] → u D [[Y1 , . . . , Yϕu ]]) = Y j .
It is clear that if F : C → D is a distributive functor, it induces a natural transformation U(F) :
U(C) → U(D). What we want to describe here is a left adjoint of U, i.e., we want to build the free
distributive category on the distributive graph G. Such a category will be denoted by F(G).
The objects of F(G) are given by the distributive expressions on G(∗). The arrows are given by
the terms generated by the following (partial) operators:1
(i). if f 1 : X 1 → Y , f 2 : X 2 → Y , then ( f 1 | f 2 ) : X 1 + X 2 → Y ;
(ii). if f 1 : Y → X 1 , f 2 : Y → X 2 , then ( f 1 , f 2 ) : Y → X 1 × X 2 ;
1 We use the following shorthand: we understand the existence of two operators d and c which give the domain and
codomain of an arrow; whenever we write f : X → Y , we mean d( f ) = X , c( f ) = Y . When these equations appear as
premises, they restrict the applicability of an operator (for instance, composition can by applied only if c( f ) = d(g)), while
when they appear as conclusions, they imply the addition of equations about c and d to the system (for instance, c( f ◦g) = c( f )
and d( f ◦ g) = d(g)). Finally, all “constant” arrows depending on given objects (such as identities) are really operators which
accepts objects and output arrows.

CHAPTER 4. THE GENERAL THEORY

42
(iii). if f : X → Y , g : Y → Z , then g ◦ f : X → Z ;
starting from the following constants:
(i). for each arc a of G,

a : t[G(d1 )(a), . . . , G(dϕt )(a)] → u[G(c1 )(a), . . . , G(cϕu )(a)];
(ii). for each object X , 1 X : X → X , ! X : ∅ → X and ¡ X : X → I ;
(iii). for each pair of objects X 1 , X 2 , projiX 1 ,X 2 : X 1 × X 2 → X i and injiX 1 ,X 2 : X i → X 1 + X 2 ;
(iv). for each triple of objects X, Y, Z , δ −1
X,Y,Z : X × (Y + Z ) → X × Y + X × Z ;
The set of such terms is quotiented by the following equations (i = 1, 2):
(i). (h ◦ g) ◦ f = h ◦ (g ◦ f );
(ii). f ◦ 1 X = 1Y ◦ f = f ;
(iii). if f : ∅ → X then f =! X ;
(iv). if f : X → I then f = ¡ X ;
−1
(v). δ X,Y,Z ◦ δ −1
X,Y,Z = 1(X ×Y )+(X ×Z ) , and δ X,Y,Z ◦ δ X,Y,Z = 1 X ×(Y +Z ) (δ has been described in
Definition 18);

(vi). if f i : X i → Y , then
( f 1 | f 2 ) ◦ injiX 1 ,X 2 = f i ,

f = ( f ◦ inj1X 1 ,X 2 | f ◦ inj2X 1 ,X 2 );

(vii). if f i : Y → X i , then
projiX 1 ,X 2 ◦( f 1 , f 2 ) = f i ,

f = (proj1X 1 ,X 2 ◦ f, proj2X 1 ,X 2 ◦ f ).

It is straightforward to check that the operators + and × define a sum and a product in F(G) for
which the distributive law is true, and that there is a chosen sum and product for any pair of objects.
Moreover, the sum (product) in F(G) is exactly the sum (product) of terms, in the sense that
t F (G) [[A1 , . . . , Aϕt ]] + u F (G) [[B1 , . . . , Bϕu ]] =
(t + u)F (G) [[A1 , . . . , Aϕt , B1 , . . . , Bϕu ]];
this implies that t[A1 , . . . , Aϕt ] = t F (G) [[A1 , . . . , Aϕt ]].
Theorem 15 F is left adjoint to U.
Proof. The unit of the adjunction ηG : G → U(F(G)) is defined by ηG (∗)(A) = A and ηG (ht, ui)(a) =
a; it is trivial to check that ηG is indeed a morphism of distributive graphs.
Given a morphism α : G → U(D), suppose the existence of a functor b
α : F(G) → D such that
U(b
α ) ◦ ηG = α; then for any term t and any A 1 , . . . , Aϕt ∈ G(∗) we have necessarily
b
α (t[A1 , . . . , Aϕt ]) = t D [[b
α (A1 ), . . . , b
α (Aϕt )]] = t D [[α(∗)(A1 ), . . . , α(∗)(Aϕt )]];

4.1. DISTRIBUTIVE CATEGORIES

43

analogously, if for an arc of a of G we have
α(ht, ui)(a) = f,
we have necessarily also
b
α (a : t[G(d1 )(a), . . . , G(dϕt )(a)] → u[G(c1 )(a), . . . , G(cϕu )(a)]) = f.

The other constants have obvious images necessarily induced by the diagram choice, and the image
of a generic term can then be obtained interpreting inductively the operators in D. So b
α is unique.
On the other hand, using the previous equations we can define by induction from α a functor b
α,
because all the equations satisfied by the arrows of F(G) are also satisfied in D. It is then trivial to
show that b
α is distributive. This completes the proof.
The 2-categorical view.

We now drop the condition about the presence of a choice of sums and products. Our treatment will
follow the ideas described in [Walters:1989b].
Note first of all that a distributive expression on A can be thought of as a binary tree whose
internal nodes are labelled by + and ×, and whose leaves are labelled by 0, 1 or by an element of A.
If D is a distributive category and X 1 , X 2 , . . . , X ϕt are objects of D, there will be in general
many objects X of D which interpret the distributive expression t[X 1 , . . . , X ϕt ], in the sense that
each such object is equipped with with a suitable choice of products and coproducts diagrams related
to the operations described by t. The injections and projections of such diagrams can be thought of
as labelling the arcs of t, in such a way that a node labelled by + (×, respectively) is linked to its
children by arcs labelled by the suitable injections (projections, respectively). This labelled tree will
be denoted by t XD {X 1 , . . . , X ϕt }: it essentially “witnesses” how X has been built using the X i ’s. Note
that there is a degree of ambiguity here, in that there can be several different labellings which adapt
to the given data; when using this notation, we shall always have in mind a specific tree, which will
be clear from the context. Given trees t XD {X 1 , . . . , X ϕt }, tYD {Yi , . . . , Yϕt }, and arrows f i : X i → Yi ,
D [[ f , . . . , f ]] for the obvious arrow from X to Y built from the f ’s using the
we shall write t X,Y
1
ϕt
i
operations described in t.
If F : C → D is a distributive functor, it can be “applied” to a tree t XC {X 1 , . . . , X ϕt } by taking
the image through F of all labels (i.e., injections and projections) and all objects. The resulting
tree witnesses the construction in D of F(X ) by means of the F(X i )’s. Finally, we note that given
trees t XD {X 1 , . . . , X ϕt } and tYD {X 1 , . . . , X ϕt }, there is exactly one isomorphism from X to Y which
commutes with all the diagrams of the two trees, in the appropriate sense.
Let now Dist be the 2-category of small distributive categories, and consider the 2-category
Cat(SetG ) ' CatG of the internal categories of SetG . Then, U : Dist → Cat(SetG ) is a forgetful
2-functor defined by:
(i). U(D)(∗) = D;
(ii). U(D)(ht, ui) is a category having as objects triples
h f : X → Y, t XD {X 1 , . . . , X ϕt }, u D
Y {Y1 , . . . , Yϕu }i;
arrows (to a “primed” triple) are ϕt + ϕu -tuples of arrows f i : X i → X i0 , g j : Y j → Y j0 of D
which satisfy
0
D
uD
Y,Y 0 [[g1 , . . . , gϕu ]] ◦ f = f ◦ t X,X 0 [[ f 1 , . . . , f ϕt ]];

CHAPTER 4. THE GENERAL THEORY

44

(iii). U(D)(di )( f : X → Y, t XD {X 1 , . . . , X ϕt }, u D
Y {Y1 , . . . , Yϕu }) = X i , and
U(D)(c j )( f : X → Y, t XD {X 1 , . . . , X ϕt }, u D
Y {Y1 , . . . , Yϕu }) = Y j ;
analogously on arrows.
It is clear that if F : C → D is a distributive functor, it induces a functor U(F) : U(C) → U(D)
(U(F)(∗) = F; for the rest, just apply F to every element of a triple and to every arrow of a tuple).
The same happens for natural transformations.
Let us define the “unit of the adjunction” η G : G → U(F(G)) by ηG (∗)(A) = A and
ηG (ht, ui)(a) = ha : t F (G) [[A1 , . . . , Aϕt ]] → u F (G) [[B1 , . . . , Bϕu ]],
t F (G) {A1 , . . . , Aϕt }, u F (G) {B1 , . . . , Bϕu }i,
where Ai = G(di )(a), B j = G(c j )(a) and the trees are given by the chosen sums and products in
F(G). The universal property we are interested in is
Theorem 16 U(−) ◦ ηG is an equivalence between Dist(F(G), D) and Cat(SetG )(G, U(D)).
Proof. Given a functor F : G → U(D) (note that we see G as a discrete internal category of Set G ),
b : F(G) → D as follows: by choosing for each pair of objects X, Y of D a
we define a functor F
product and a coproduct diagram, we can define for any term t and any A 1 , . . . , Aϕt ∈ G(∗)
D
b
F(t[A
1 , . . . , A ϕt ]) = t [[F(∗)(A1 ), . . . , F(∗)(A ϕt )]];

analogously, if for an arc of a of G we have
F(ht, ui)(a) = h f : X → Y,

t XD {F(∗)(A1 ), . . . , F(∗)(Aϕt )}, u D
Y {F(∗)(B1 ), . . . , F(∗)(Bϕu )}i,

(4.1)

where by functoriality again Ai = G(di )(a) and B j = G(c j )(a), we set
b
b = βa ◦ f ◦ αa : F(t[A
b
F(a)
1 , . . . , Bϕu ]),
1 , . . . , A ϕt ]) → F(u[B

b
b
where αa : F(t[A
1 , . . . , A ϕt ]) → X and βa : Y → F(u[B
1 , . . . , Bϕu ]) denote the unique isomorphisms which commute with the diagrams. The other constants have obvious images induced by the
diagram choice, and the image of a general term can then be obtained interpreting inductively the
operators in D.
b ◦ ηG is given by
In order to show that this association induces an equivalence, we note that U( F)
b
(U( F) ◦ η)(∗)(A) = F(∗)(A), and by
b ◦ η)(ht, ui)(a) = hβ f ◦ f ◦ α f ,
(U( F)

t D {F(∗)(A1 ), . . . , F(∗)(Aϕt )}, u D {F(∗)(B1 ), . . . , F(∗)(Bϕu )}i,

where f : X → Y is the first component of F(ht, ui)(a); then, the isomorphisms α(−) and β(−)
b ◦ η.
induce a natural isomorphism F ∼
= U( F)
The last step is proving that U(−) ◦ ηG is full and faithful. Given functors F, F 0 : G → U(D),
a natural transformation ψ : F ⇒ F 0 is a family of arrows indexed by the objects and by the arcs of
G in such a way that for each object there is a morphism ψ A : F(∗)(A) → F 0 (∗)(A) of D, and for
each arc a ∈ G(ht, ui) there is a morphism
ψa : F(a) → F 0 (a),

4.2. EXTENSIVE CATEGORIES

45

which amounts (using the notation of (4.1), and “priming” the tuple for F 0 (a)) to a ϕt + ϕu -tuple of
B
morphisms ψaAi : F(∗)(Ai ) → F 0 (∗)(Ai ), ψa j : F(∗)(B j ) → F 0 (∗)(B j ) satisfying
A

B

ϕt
ϕu
B1
0
D
A1
uD
Y,Y 0 [[ψa , . . . , ψa ]] ◦ f = f ◦ t X,X 0 [[ψa , . . . , ψa ]].

But such a family of tuples is exactly a natural transformation U(F) ◦ η G ⇒ U(F 0 ) ◦ ηG (the last
equation is the commutativity condition for all the basic arrows; the condition extends immediately
to a generic arrow by structural induction).

4.1.3

The language IMP(G)

Given a distributive graph G, an (isolated) program in the language IMP(G), introduced by Walters
in [Walters:1992b], is simply an arrow
f :X→X
of the free distributive category on G. The arcs and the objects of G are used in order to specify the
signature of the basic operations allowed in an IMP(G) program (for instance, the graph of recursive
functions has set of objects {N} and two arcs p : N → I + N and s : I + N → N). Then, the
free distributive category on G provides the abstract syntax of all IMP(G) programs. The notation
used in the previous section provides instead a concrete syntax, and it will be used in Chapter 6 when
describing the formal tools which allow to manipulate IMP(G) programs.
Given a distributive category D, a distributive graph morphism α : G → U(D) is defined by
assigning to each object of G an object of D (these are the basic objects of Chapter 2) and to each
arc of G an arrow of D (these are the basic functions). Then, the morphism extends to a distributive
functor F(G) → D which allows to interpret the arrows of F(G) in D. The image of an arrow of
F(G) is a derived function, because it is obtained by interpreting in D a term built using exactly the
constants and operations described in Section 2.1.
Following the same lines of the elementary introduction given in Section 2.1, it is now natural
to consider arrows of the form f : X + U → U + Y , and the possibility of iterating such arrows.
However, in a distributive category we have no way of expressing the property that the iteration of
such an arrow terminates, giving as result an arrow X → Y . This is the motivation for the introduction
of extensive categories.

4.2 Extensive categories
Definition 19 A category is said to be extensive if the canonical functor
E/A × E/B → E/(A + B)
is an equivalence, for each pair of objects A, B in E.
Countably extensive categories (i.e., categories which have countable sums and enjoy the extensivity property for countable sums) provide semantical universes in which we can interpret a free
distributive category. The peculiarity of countable extensivity is that it allows to define what is an
arrow computed by iteration.
In an extensive category we can restrict and corestrict at the same time arrows which land into a
sum. If we have an arrow f : C → A + B, we can pull f back along the injections of A and B into
A + B and obtain arrows f dA : f −1 (A) → A and f Be : f −1 (B) → B such that f dA + f Be = f . In
other words, whenever we have an arrow into a sum, we can break the source of the arrow into the
part which maps into the first summand, and the part which maps into the second summand (we shall

CHAPTER 4. THE GENERAL THEORY

46

use the set-like notation f −1 (A) for the part of the domain which lands in A; if X ∼
= A0 + B 0
= A+ B ∼
0
we shall use the notation A ∩ A for the pullback of the injection of A along the injection of A 0 ).
This property derives from the following theorem [Carboni, Lack & Walters:1993]:
Theorem 17 A category with finite sums is extensive iff it has pullbacks along injections, and for
each commutative diagram
f −1 (A)

f −1 (B)

C
f

A

inj1

A+B

inj2

B

the top row is a coproduct diagrams exactly when the two squares are pullbacks.
Another important property of extensive categories we shall use is the cancellation lemma [Lack:1995]:
Theorem 18 If A + B ∼
= A + C, by an isomorphism commuting with the injections of A, then
B∼
= C.
Consider now an arrow f : X + U → U + Y in a countably extensive category. Intuitively, f
describes a dynamical system with initial states in X . By applying f , we obtain either a final state
in Y , or a local state in U ; in the latter case, we can apply again f . We can define the arrow which
f computes by iteration, denoted by call[ X, U, Y, f ] (or call[ f ], if X , U and Y are clear from the
context), as follows: let
f 0 = f |X : X → U + Y
f k+1 = f |U ◦ f k dU : f k−1 (U ) → U + Y.
Then f k−1 (Y ) is the part of X which lands in Y after exactly k + 1 iterations. The iteration of f
P
terminates if k≥0 f k−1 (Y ) ∼
= X (where the isomorphism is given by the injections f k−1 (Y ) → X ),
in which case we can define call[ f ] : X → Y as
X

call[ f ] = f 0 Y e | f 1 Y e | · · · | f k Y e | · · · = ∇ ◦
fk Y e.
k≥0

This framework allows us to define, for any subcategory with finite sums C of a countably extensive
category E, the (for the time being a) set call[ C ] of the arrows computable by iteration in C, which
is formed by the arrows computed by arrows f : X + U → U + Y (in C). The normal form theorem
can be now restated as follows:
Theorem 19 Let E be a countably extensive category, and C a subcategory of E with finite sums.
(i). For each terminating arrow2 f : X → Y of C,
f = call[ inj2 ◦( f | 1Y ) : X + ∅ → ∅ + Y ].
(ii). If f : X + U → U + Y and g : Y + V → V + Z , then
call[ f ] ◦ call[ g ] = call[ X, U + Y + V, Z , f + g. ]
2 Note that in the future we shall avoid to quote explicitly the termination condition; each time call[ − ] will be used, we
shall understand the termination condition for the arrows it is applied to.

4.2. EXTENSIVE CATEGORIES

47

(iii). If f : X + U → U + Y and g : X 0 + U 0 → U 0 + Y 0 , then
call[ f ] + call[ g ] = call[ a ◦ ( f + g) ◦ b ]
where a is the commutativity isomorphism
∼
=

X + X0 + U + U0 −
→ X + U + X 0 + U 0,
and b is the commutativity isomorphism
∼
=

U + Y + U0 + Y0 −
→ U + U 0 + Y + Y 0.
(iv). If f : X + V + U → U + V + Y , then
call[ X, V, Y, call[ X + V, U, V + Y, f ] ] = call[ X, U + V, Y, i ◦ f ] : X → Y,
where i is the commutativity isomorphism
U + V + Y → V + U + Y.
Moreover, if E has finite products, C is distributive, f : X +U → U + Y and g : X 0 +U 0 → U 0 + Y 0 ,
then
0

0

,Y
call[ f ] × call[ g ] = call[ d ◦ ( f |X × g|X 0 | f |U × g|U 0 | f |U × injU
| injU,Y
×g|U 0 ) ],
2
2

where d is the isomorphism
∼
=

→ UU 0 + U Y 0 + Y U 0 + Y Y 0
(U + Y ) × (U 0 + Y 0 ) −
induced by distributivity.
We can interpret the previous claims as follows:
(i). call[ C ] contains the arrows of C;
(ii). call[ C ] is closed under composition (thus, it is a subcategory of E which contains C);
(iii). call[ C ] has finite sums;
(iv). call[ call[ C ] ] = call[ C ] (i.e., call[ − ] is idempotent).
Moreover, if E has finite products and C is distributive then call[ C ] is distributive. The proof of the
normal form theorem for extensive categories has been given (in terms of functional processors) in
[Khalil:1992b], [Khalil:1992a] and [Khalil]. We shall refer from now to the category call[ C ] as to
the iterative closure of C in E.

4.2.1

Functions and functional processors

The way in which a terminating arrow and the relative computed arrow have been defined here differs
from the way it was defined in [Wagner, Khalil & Walters:1995] and [Sabadini, Vigna & Walters:1996].
The form described here is simpler to manage in equivalence proofs, and gives nicer formulae in some
(but not all) parts of the normal form theorem.
The two definitions are of course equivalent, but we wish to formulate this fact more precisely.
Given a prefunctional processor ϕ : X + U + Y → X + U + Y , i.e., a loop which satisfies ϕ ◦

CHAPTER 4. THE GENERAL THEORY

48

inj2X +U,Y = 1Y and which factors3 through the injection U + Y → X + U + Y , we can obtain an
arrow ψ : X + U → U + Y by factoring and restricting to X + U . On the other hand, given an arrow
f : X + U → U + Y , we shall call
inj2X,U +Y

( f | injU,Y
2 )

h : X + U + Y −−−−−−→ U + Y −−−−−→ X + U + Y
the loop induced by f , which is trivially a prefunctional processor.
Theorem 20 The prefunctional processor h : X + U + Y → X + U + Y associated to a terminating
arrow f : X +U → U +Y is a functional processor in the sense of [Wagner, Khalil & Walters:1995];
moreover, both h and f compute the same arrow.
Proof. We set up some notation following [Wagner, Khalil & Walters:1995]. Let i, j and k be the
injections of X , U and Y , respectively, in X + U + Y (the fact that k is also a summation index should
cause no confusion). The following pullbacks
An

an

an0
0
X n−1

Xn

hn

i Xn
iX0

n−1

Y
k

X

h n ◦i

X +U +Y

where X n = (h n ◦ i)−1 (Y ) and X n0 = (h n ◦ i)−1 (X + U ) (so X n + X n0 ∼
= X ) exhibit
An = (h n ◦ i)−1 (Y ) ∩ (h n−1 ◦ i)−1 (X + U )
as the part of X which lands in Y after exactly n iterations. The arrow h is a functional processor iff
the arrows i X n ◦ an : An → X form a coproduct diagram. Then, the arrow computed by iteration by
h is defined by the arrows h n ◦ an .
P
Since f is a terminating arrow, we have a decomposition k≥0 f k−1 (Y ) ∼
= X induced by the
P
iteration of f , and f n−1 (U ) ∼
= k>n f k−1 (Y ) by the cancellation lemma. The idea behind the proof is
that the correspondence between the iteration of f and the iteration of h is described by the following
equations:
(i). An+1 ∼
= f n−1 (Y );
Pn
(ii). X n+1 ∼
= k=0 f k−1 (Y );
P
0
∼
(iii). X n+1
= k>n f k−1 (Y );

(iv). h n+1 = ( f 0 Y e | f 1 Y e | · · · | f n Y e ).

If we can prove that these equations hold, clearly h will be a functional processor computing the
arrow call[ f ].
Since X 0 = ∅ and X 00 = X , for n = 0 we have
−1
−1
X 1 = (h ◦ i)−1 (Y ) = h −1
|X (Y ) = f |X (Y ) = f 0 (Y ),
3 The factoring condition is not imposed in [Wagner, Khalil & Walters:1995], but it will be essential when discussing the
inversion of iteration through refinement, and it can be imposed without loss of generality; for if a prefunctional processor
does not factor through U + Y , one can enlarge the local state space U to V = X + U , injecting in the obvious manner the
input state space X into the new local state space V without affecting the computed arrow. The resulting loop on X + V + Y
obviously factors through the injection V + Y → X + V + Y .

4.2. EXTENSIVE CATEGORIES

49

so A1 = X 1 = f 0−1 (Y ). On the other hand,
X 10 = (h ◦ i)−1 (X + U ) = (inj2X,U +Y ◦ f |X )−1 (X + U ) = f 0−1 (U ) ∼
=

X

f k−1 (Y ).

k>0

Now a tedious but trivial diagram chasing argument shows that the following diagram commutes for
n > 0:
Pn
P
−1
−1
X
k=0 f k (Y )
k>n f k (Y )
inj2X,U ◦ f n dU

( f 0 Y e | f 1 Y e | ··· | f n Y e )

h n+1 ◦i

X +U

(i | j)

X +U +Y

Y

k

But the top row is by definition a coproduct diagram. By Theorem 17 the two squares are pullbacks.
Thus, also the following diagram
Pn

−1
k=0 f n (Y )

f n−1 (Y )
P

k≥n

( f 0 Y e | ··· | f n Y e )

Y
k

f k−1 (Y )

X

X +U +Y

h n+1 ◦i

(where all the
P unspecified arrows
P are the obvious injections) is formed by two pullback squares (being
f n−1 (Y ) = nk=0 f n−1 (Y ) ∩ k≥n f k−1 (Y )). This completes the proof.

Of course, also the following holds:

Theorem 21 The arrow ψ : X + U → U + Y associated to a functional processor ϕ : X + U + Y →
X + U + Y by factorization through U + Y and restriction to X + U is terminating, and both ψ and
ϕ compute the same arrow.
Proof. Since ϕ is the loop induced by ψ, we have that, as is the previous theorem, the following
diagram commutes for all n ≥ 0
ψn−1 (U )

Pn

−1
k=0 ψk (Y )

X

inj2X,U ◦ψn dU

ϕ n+1 ◦i

X +U

(i | j)

X +U +Y

(ψ0 Y e | ψ1 Y e | ··· | ψn Y e )

Y

k

and beingP
the top row a coproduct diagram, the two squares are pullbacks (note that we cannot claim
that U ∼
= k>n ψk−1 (Y ), for ψ is not known to be terminating). But ϕ is a functional processor, and
this implies that the following two squares are pullbacks for all n > 0:
P

k>n

Ak

X +U

Pn

X

k=1

ϕ n ◦i
(i | j)

X +U +Y

k

−1
(Y ) and ϕn = (ψ0 Y e | · · · | ψn−1 Y e ).
which implies An ∼
= ψn−1

Ak

ϕn

Y

CHAPTER 4. THE GENERAL THEORY

50

4.2.2

The semantics of IMP(G) programs

As it is shown in [Carboni, Lack & Walters:1993], an extensive category with finite products is distributive. Thus, given a distributive graph G and a countably extensive category with finite products
E, as in Section 4.1.3 a distributive graph morphism α : G → U(E) extends to the free distributive
category on G, resulting in a semantic assignment for all IMP(G) programs. However, we have now
the possibility to close by iteration the image of F(G) in E. In this way we assign an arrow of E to
all arrows computed by iteration; moreover, by the normal form theorem the extension of G and α by
such an arrow does not change the iterative closure.

4.2.3

Technical lemmata

Lemma 4 Let E and F be a extensive categories, and S : E → F a functor which preserves finite
sums. Then S preserves pullbacks along injections.
Proof. If we have a pullback of f : A → B + C along an injection (of B or C), we can get the
following diagram by pulling back along the other injection:
f −1 (B)

f −1 (C)

A

f dB

f Ce

f

B

inj1

B +C

inj2

C

and then by extensivity the top row is a coproduct diagram. But S preserves finite sums, so that the
following diagram
S( f −1 (B))

S( f −1 (C))

S(A)

S( f dB )

S( f Ce )

S( f )

S(B)

inj1

S(B) + S(C)

inj2

S(C)

has a coproduct diagram as first row. As a consequence, the two squares are pullbacks, and S( f ) dS(B) ∼
=
S( f dB ).
Definition 20 An arrow f : X + U → U + Y of an extensive category E is said to be finitely iterable
if ultimately f k−1 (Y ) ∼
= ∅. Given a subcategory with sums C of E, C is said to be finitely iterable in
E if all its arrows are finitely iterable.
Lemma 5 If the free distributive category generated by a distributive graph is extensive, then it is
finitely iterable within itself.
Proof. We have to prove that, given an arrow f : X +U → U +Y of F(G), ultimately f k−1 (Y ) ∼
= ∅.
Let v : |F(G)| → N be the +/×-algebra morphism which sends each object of G to 1. Then
v(X ) = v(Y
X, Y ∈ |F(G)|, and v(X ) = 0 iff X ∼
= ∅.
P) for all isomorphic
−1
Since 0≤k≤n f k (Y ) is a complemented subobject of X for any n and the only sums in a free
distributive category are the syntactic ones, the upper bound

 X

 X
X
−1
−1
−1
f k (Y ) + v( f n−1 (U )) = v(X )
v( f k (Y )) = v
f k (Y ) ≤ v
0≤k≤n

0≤k≤n

0≤k≤n

4.2. EXTENSIVE CATEGORIES

51

implies that f k−1 (Y ) 6 ∼
= ∅ only for a finite number of k’s.
Whenever C is finitely iterable, we can define the iterative closure call[ C ] even if E does not
possess countable sums, because the infinite sums appearing in the definition of call[ − ] all reduce
to finite sums. This is particularly important in the case of the previous lemma, because then C = E,
and then obviously call[ E ] = E, where the iterative closure is taken within E itself.
We now study the effect of sum preserving functors on iterative closures.
Lemma 6 Let E and F be extensive categories, S : E → F a functor which preserves finite sums,
and f : X + U → U + Y a terminating, finitely iterable arrow. Then S( f ) is a terminating, finitely
iterable arrow, and S(call[ X, U, Y, f ]) = call[ S(X ), S(U ), S(Y ), S( f ) ]. If E, F are countably
extensive and S preserves countable sums the statement is true for any terminating arrow.
Proof. Let us prove that S( f k ) = S( f )k . Clearly S( f 0 ) = S( f )0 . By induction,
S( f )k+1 = S( f )|S(U ) ◦ S( f )k dS(U ) = S( f |U ) ◦ S( f k dU ) = S( f |U ◦ f k dU ) = S( f k+1 ).
Then
S(call[ f ]) = S f 0 Y e | f 1 Y e | · · · | f k Y e | · · ·



= S( f 0 Y e ) | S( f 1 Y e ) | · · · | S( f k Y e ) | · · ·



= S( f 0 ) S(Y )e | S( f 1 ) S(Y )e | · · · | S( f k ) S(Y )e | · · ·



= S( f )0 S(Y )e | S( f )1 S(Y )e | · · · | S( f )k S(Y )e | · · ·
= call[ S( f ) ].



Analogously for the finite case.
Corollary 6 Let E and F be extensive categories, S : E → F a functor which preserves finite sums,
and C a finitely iterable subcategory with sums of E. Then S(call[ C ]) ⊆ call[ S(C) ]. If E, F are
countably extensive and S preserves countable sums, the statement is true for any subcategory with
finite sums.
Proof. The two categories involved have trivially the same class of objects. Moreover, Lemma 6 says
that S(call[ C ]) ⊆ call[ S(D) ].
It is now natural to ask the following question: when is the inclusion of the previous corollary an
equality? This situation is enough important to deserve a name:
Definition 21 A sum preserving functor S : E → F, where E, F are countably extensive categories,
is said to preserve the iteration of a subcategory with finite sums C of E iff
S(call[ C ]) = call[ S(C) ].
The essential reason which keeps an arbitrary functor from preserving iteration is that even if
S( f ) is terminating, f could be nonterminating. For instance, consider the arrow
(inj1 | inj2 | inj3 | inj2 )

f : A + B + A + B −−−−−−−−−−−−−−→ A + B + A,
which is clearly not terminating on A + B. Any sum preserving functor S satisfying S(B) ∼
= ∅ will
bring f into an arrow
S( f ) : S(A) + S(A) → S(A) + S(A)
such that call[ S( f ) ] = 1 S(A) . We shall now give three sufficient conditions for the iteration of a
subcategory being preserved.

CHAPTER 4. THE GENERAL THEORY

52

Theorem 22 A countable sum preserving functor which is conservative (i.e., which reflects isomorphisms) preserves the iteration of any subcategory.
Proof. If S( f ) : S(X ) + S(U ) → S(U ) + S(Y ) is terminating, as in the proof of Lemma 6 we have
X 
X
X
∼
∼
∼
S(X k ) = S
S(X )k =
Xk ,
S(X ) =
k≥0

k≥0

k≥0

where all the isomorphisms are given by the obvious injections. This implies the the inclusion
P
k≥0 X k → X is an isomorphism, by the conservativity of S.
Theorem 23 If C is closed under subobjects, any countable sum preserving functor S : E → F
preserves the iteration of C.
Proof. Let S( f ) be a terminating arrow. If we restrict f to
which is terminating. Moreover,

P

k≥0

X k + U , we obtain an arrow f 0

S( f 0 ) = S( f | Pk≥0 X k +U ) = S( f )|S(Pk≥0 X k +U ) = S( f )|S(X )+S(U ) = S( f ),

so call[ S( f 0 ) ] = call[ S( f ) ].

Theorems 22 and 23 are obviously true also for finitely iterable subcategories and finite sum
preserving functors.
Theorem 24 Any finite sum preserving functor S satisfying S(X ) ∼
= ∅ preserves iter= ∅ =⇒ X ∼
ation of finitely iterable subcategories. If E has complemented subobjects and S preserves countable
sums, it preserves iteration of any subcategory.
P
0 ∼
Proof. With the same notation of the previous two theorems, we have P
k≥0 X k + X = X , where
0
X is obtained by extensivity in the finite case and by complementation of k≥0 X k in the countable
case. Thus we have
X 
S
X k + S(X 0 ) ∼
= S(X ),
k≥0

which by the cancellation lemma implies S(X 0 ) ∼
= ∅. This means that the
= ∅; by hypothesis X 0 ∼
termination of S( f ) implies the termination of f .

4.2.4

The control function theorem

Definition 22 The normal form of a distributive expression on a set A is obtained by interpreting the
distributive expression in the free semiring on A, and reducing it to a sum of monomials. An arc of a
distributive graph is called a control function if the normal form of its target is a sum of at least two
monomials.
Note that in F(G) there is an isomorphism between the interpretation of a distributive expression and
the interpretation of its normal form.
Theorem 25 Let G be a distributive graph which contains no control functions; then F(G) is extensive.

4.2. EXTENSIVE CATEGORIES

53

Proof. We shall prove4 by structural induction that if f : X → Y is a morphism of F(G), and
Y ∼
= V + W , then there are functions f dV : f −1 (V ) → V , f W e : f −1 (W ) → W such that f dV +
f W e = f . This proves that the canonical functor + is full and essentially surjective. Faithfulness
follows trivially from the monicity of the injections of a distributive category.
It is clear that by hypothesis if f is the image of an arc of G then either V ∼
= ∅ or W ∼
= ∅; hence,
either f dV = f or f W e = f . If f is an identity the case is trivial. If f is an injection, it is easy to
check that f dV and f W e are still injections. Finally, if f is a projection or the inverse distributivity
isomorphism the decomposition of the codomain induces trivially the decomposition of the domain.
Suppose now f = h ◦ g, with g : X → Z . Then f satisfies the induction hypothesis, so that
Z ∼
= f −1 (V ) + f −1 (W ). But now g in turn can be broken into gdh −1 (V ) and gh −1 (W )e , so that
h = h dV ◦ gdh −1 (V ) + h W e ◦ gh −1 (W )e .
If f = (h | g), then we have f dV = (h dV | gdV ) and f W e = (h W e | gW e ). Clearly, h −1 (V ) +
−1
g (V ) + h −1 (W ) + g −1 (W ) ∼
= X.
P
IfPf = (g, h) : X → A × B, then by distribution we can write in normal form A ∼
= i Ai and
B∼
= j B j , where the Ai ’s and the B j ’s are monomials, and we can break g into gi : g −1 (Ai ) → Ai ,
P
with g = i gi ; the same can be done for h. Note that if we define C i j = g −1 (Ai ) ∩ h −1 (B j ), then
P
∼
i, j Ci j = X .
Since A × B ∼
= V + W , there is a partition of the pairs hi, ji in two sets K , L such that
X
X
Ai B j ∼
Ai B j ∼
= W.
=V
hi, ji∈L

hi, ji∈K

But this implies that if we define
X
(gi |Ci j , h j |Ci j )
f dV =
hi, ji∈K

fW e =

X

(gi |Ci j , h j |Ci j )

hi, ji∈L

then
f dV + f W e =

X

hi, ji∈K

(gi |Ci j , h j |Ci j ) +

X

(gi |Ci j , h j |Ci j ) =

hi, ji∈L

X

(gi |Ci j , h j |Ci j ) = (g, h).

i, j

The following theorem says that if no “control structure” (in the form of a control function) is
present in the distributive base graph of a free distributive category, then closure by iteration does not
yield any new function.
Theorem 26 Let G be a distributive graph, E an extensive category and S : F(G) → E a distributive
functor. If no arc of G is a control function, then
S(F(G)) = call[ S(F(G)) ].
Proof. Since F(G) is extensive, we have F(G) = call[ F(G) ]. But then by Theorem 23
call[ S(F(G)) ] = S(call[ F(G) ]) = S(F(G)).
4 A different proof has been suggested by R.F.C. Walters. Under the given hypotheses, it is possible to build a distributive
graph G 0 all whose arcs start from a product of objects and end on a single object, and such that F (G) ∼
= F (G 0 ). Then F (G 0 )
is just the free category with sums on the free category with products on G 0 ; but a free category with sums is always extensive.

CHAPTER 4. THE GENERAL THEORY

54

4.3 Refinement in lextensive categories
We are now in the position to prove the refinement theorem (stated in Section 3.2.2) in an extensive
setting. For this purpose, however, we shall need to internalize the notion of transition category to
the extensive universe we are using. This requires the existence of finite limits (pullbacks are necessary in order to define internal categories, while products are necessary in order to define monoids
and monoid actions), and a category which is extensive and has finite limits is called lextensive (or
countably lextensive, in case extensivity is enjoyed for countable sums).
We begin by recalling the definition of internal category:
Definition 23 Let C be a category with pullbacks. An internal category X of C is given by
(i). objects X 0 , X 1 of C, called the object of objects and the object of arrows;
(ii). arrows ∂0 , ∂1 : X 1 → X 0 of C, called domain and codomain;
(iii). an arrow i : X 0 → X 1 , called identity;
(iv). an arrow c : X 1 × X 0 X 1 → X 1 called composition, where X 1 × X 0 X 1 is the pullback of ∂0 and
∂1 (with projections π1 and π0 , respectively—note the reversed indices);
satisfying the following equations:
(i). ∂0 ◦ i = ∂1 ◦ i = 1 X 0 ;
(ii). ∂1 ◦ π1 = ∂1 ◦ c and ∂0 ◦ π0 = ∂0 ◦ c;
(iii). c ◦ (1 X 1 , i ◦ ∂0 ) = c ◦ (i ◦ ∂1 , 1 X 1 ) = 1 X 1 ;
(iv). c ◦ (1 X 1 × X 0 c) = c ◦ (c × X 0 1 X 1 ).
A internal functor F between internal categories X and Y of C is given by a pair of arrows F0 :
X 0 → Y0 , F1 : X 1 → Y1 which satisfies the following equations:
(i). ∂0 ◦ F1 = F0 ◦ ∂0 and ∂1 ◦ F1 = F0 ◦ ∂1 ;
(ii). F1 ◦ i = i ◦ F0 ;
(iii). F1 ◦ c = c ◦ (F1 × F0 F1 ).
An internal functor F is injective on objects if F0 is a mono; it is faithful if F1 is a mono; it is full
if the factorization of F1 through ∂0−1 (F0 ) ∩ ∂1−1 (F0 ) is an epi. A full inclusion is a full and faithful
functor which is injective on objects.
Note that the equations which must be satisfied by the domain, codomain and identity arrows imply that the indicated arrows into the pullback X 1 × X 0 X 1 do exist (for more details, see [Borceux:1994]).
The definition of fullness requires the construction of the pullback diagrams
X1
jq
∂q

F1

∂q−1 (F0 )

Y1
∂q

X0

F0

Y0

4.3. REFINEMENT IN LEXTENSIVE CATEGORIES

55

for q = 0, 1 and of the factorization F10 of F1 through the following pullback:
X1
F10

j1

j0

∂0−1 (F0 ) ∩ ∂1−1 (F0 )

∂0−1 (F0 )

∂1−1 (F0 )

Y1

Definition 24 Let hM, µ, εi be a monoid in a category with finite limits C; an automaton X on M is
given by an object X of C together with a monoid action α : M × X → X . The transition category
of X is the internal category Trans(X) of C defined as follows:
(i). the objects of Trans(X) are given by X , the arrows by M X ;
(ε◦¡ X ,1 X )

(ii). i : X −−−−−→ M X ;
proj2

(iii). ∂0 : M X −−→ X ;
α

(iv). ∂1 : M X −
→ X;
(π1 ,π0 )

(proj1 ,proj3 ,proj4 )

µ×1 X

(v). c : (M X ) × X (M X ) −−−−→ M X × M X −−−−−−−−−−→ M M X −−−→ M X .
Rewording simply our definitions, we shall say that a morphism of automata in C is an internal
functor between the respective transition categories, and that a refinement is a functor which is a full
injection.
Theorem 27 The data of Definition 24 satisfy the equations of an internal category of C.
Proof. The equations about the identity arrow i are trivially satisfied because proj 2 ◦(ε◦ ¡ X , 1 X ) = 1 X
and because of the unit axiom of M. Both ∂0 ◦ π0 and ∂0 ◦ c are just projections on the fourth factor
of (M X ) × X (M X ), and
∂1 ◦ c = α ◦ c
= α ◦ (µ × 1 X ) ◦ (proj1 , proj3 , proj4 ) ◦ (π1 , π0 )
= α ◦ (1 M × α) ◦ (proj1 , proj3 , proj4 ) ◦ (π1 , π0 )
= α ◦ (proj1 ◦π1 , α ◦ π0 )
= α ◦ (proj1 ◦π1 , proj2 ◦π1 )
= α ◦ π1 ,
because of the associativity of the action of M and of the commutativity of the pullback diagram of
(M X ) × X (M X ). We prove the first of the two equations regarding composition with the identity:
c ◦ (1 M X , i ◦ ∂0 ) = (µ × 1 X ) ◦ (proj1 , proj3 , proj4 ) ◦ (π1 , π0 ) ◦ (1 M X , i ◦ ∂0 )
= (µ × 1 X ) ◦ (proj1 , (ε ◦ ¡ X , 1 X ) ◦ proj2 )
= (µ × 1 X ) ◦ (1 M × (ε ◦ ¡ X , 1 X ))
= (µ × 1 X ) ◦ (1 M × ε × 1 X ) ◦ (1 M × (¡ X , 1 X ))
= (proj1 ×1 X ) ◦ (1 M × (¡ X , 1 X ))
= 1M × 1X = 1M X ,

CHAPTER 4. THE GENERAL THEORY

56

the other one having a similar proof. Finally, the associativity equation derives immediately from the
associativity of M.
As we noticed at the beginning of this chapter, in a distributive category with countable sums it is
possible to build certain algebraic structures. In particular, the free monoid on I will be denoted by
N = I + I + · · · . Given a loop f on X , there is an obvious N-automaton with state space X , and
action defined by
2

(1 X | f | f |··· )
α : NX ∼
= X + X + · · · −−−−−−−−−→ X.

We shall describe such automata by giving just the loop f . With these premises, we can finally state
and prove the refinement theorem:
Theorem 28 Let f : X + U → U + Y be a terminating arrow of a lextensive category E. Let X be
the N-automaton
inj2X,Y ◦(call[ f ] | 1Y )

X + Y −−−−−−−−−−−−→ X + Y,
and X 0 be the N-automaton on X + U + Y given by the functional processor h induced by f . Then,
there is a refinement from X to X 0 whose object component is the inclusion F0 : X +Y → X +U +Y .
Proof. We have to define an arrow
F1 : N(X + Y ) → N(X + U + Y )
which satisfies, together with the inclusion F0 : X + Y → X + U + Y , the equations of an internal
functor. By distributivity N(X +Y ) ∼
=
= N X + NY , and F1|NY is just the inclusion in N(X +U +Y ) ∼
N X + NU + NY . For what matters N X , we set
X

g

Xi ∼
=X

i≥0

on the basis of the iteration of f , and we define for j > 0
j,i

gi

ιi+ j

→ X −−→ N X,
F1 : X i −
j,0

j

(F1

j,1

| F1

| ··· )

where ιi+ j is the injection in the i + j-th copy of X . Then F1 : X −−−−−−−−−→ N X and
(F 0 | F 1 | ··· )

1
1
F1|N X : N X −−−−−−−−→ N X → N X + NU + NY ∼
= N(X + U + Y ),

where F10 is the injection of X into the first component of N X .
We have now to show that the functorial equations hold. The domain equation ∂ 0 ◦ F1 = F0 ◦ ∂0
is trivially satisfied. The codomain equation, restricted to NY , is also trivially satisfied because in
both X and X 0 the action on that component is the identity. We now restrict the codomain equation
gi

ιi+ j

→ X −−→ N X , obtaining for j > 0
to X i −
j,i

∂1 ◦ F1 = α 0 ◦ ιi+ j ◦ gi
= h i+ j ◦ i ◦ gi
= k ◦ ( f 0 dY | · · · | f i+ j−1 dY ) ◦ gi
= k ◦ f i dY
= F0 ◦ inj2X,Y ◦ f i dY ,

4.4. SOME CONSIDERATION ON PARTIALITY

57
j

where we used the commutativity of the diagrams in the proof of Theorem 20. Thus, ∂ 1 ◦ F1 =
F0 ◦ inj2X,Y ◦ call[ f ], and (by the definition of F10 )
∂1 ◦ F1|N X = F0 ◦ (inj1X,Y | inj2X,Y ◦ call[ f ] | inj2X,Y ◦ call[ f ] | · · · ) =
F0 ◦ (inj1X,Y | inj2X,Y ◦ call[ f ] | inj2X,Y ◦(call[ f ] | 1Y ) ◦ inj2X,Y ◦ call[ f ] | · · · ) =
F0 ◦ α 0 |N X = F0 ◦ ∂1|N X .
The identity equations are trivial, for both F1 ◦ i and i ◦ F0 are the inclusion of X + Y into the first
summand of N(X + U + Y ) (note also that i = F10 ).
Finally, we show that F is full and faithful. Fidelity is immediate once we notice that F1 is built
using injections (which are monic in any distributive category) and the codomains of all injections
gi

ιi+ j

→ X −−→ N X lies in different copies of X
are disjoint. Indeed, the codomain of two inclusions X i −
when j varies, and in different summands of X when i varies.
−1
0
Now we note that ∂0−1 (F0 ) ∼
= N(X + Y ) and (letting V = ∂1 −1
|NU (X + Y ) and V = ∂1 |NU (U ))
∂1−1 (F0 ) ∼
=X+

XX

X i + V + NY.

j>0 i< j

This can be seen by building the following diagram, whose commutativity can be easily derived from
the commutativity of the diagrams in the proof of Theorem 20:
X+

P

j>0

P

i< j

X i + V + NY

X +Y

N(X + U + Y )
∂1

F0

X +U +Y

P

j>0

P

i≥ j

Xi + V 0

U

The vertical arrows are obtained by suitably restricting and corestricting the action α 0 . The first row
is a coproduct, so the two squares are pullback. As a result,
XX
∂0−1 (F0 ) ∩ ∂1−1 (F0 ) ∼
X i + NY.
=X+
j>0 i< j

j,i

0
Since F1 if given by (F10 | F11 | · · · ) + 1 NY , the codomain of FP
1 is XPand F1 is the injection
into the component X i which lies in the j-th summand of the sum j>0 i< j X i , we have that the
P
P
factorization of F1 through ∂0−1 (F0 ) ∩ ∂1−1 (F0 ) gives j>0 i< j 1 X i , which implies that F1 is an
isomorphism.

4.4 Some consideration on partiality
The general theory described here is based on total functions. The iterative closure call[ C ] is built
using only terminating arrows in order to preserve the good categorical properties (distributivity, for
instance) of C.
In the Set-based case we mentioned that it possible to consider a pcall[ − ] operator returning
partial functions. As long as suitable set-theoretical definitions are used in the definition of the operators (−, −) and (− | −), the theory can be indeed rebuilt without any modification. The categorical
extension, however, is more problematic, because the category of sets and partial functions does not
have products.

58

CHAPTER 4. THE GENERAL THEORY

In [Wagner, Khalil & Walters:1995] a definition is proposed of fix-point solution of a prefunctional processor ϕ : X + U + Y → X + U + Y (called there a program) in a distributive category
D; it is an arrow σ : X + U + Y → Y such that σ ◦ ϕ = σ and σ ◦ k = 1Y (where k is the
injection Y → X + U + Y ). The fix-point semantics ϕ̄ of ϕ is then defined as σ|X . Given a distributive subcategory C ⊆ D, one can consider the category C† of the fix-point semantics of (not
necessarily functional) processors of D, which is distributive. Thus, C† should generalize the operator call[ − ] to the case of arrows without termination condition (we say “generalize” because it is
proved in [Wagner, Khalil & Walters:1995] that a pseudofunction has a unique fix-point semantics
which coincides with the function it computes by iteration).
However, it is easy to see that for any objects X , Y of C the identity on X + Y is an everywhere
nonterminating prefunctional processor. Since the definition of fix-point solution implies that σ can
be defined arbitrarily on the part of the input and local state space on which ϕ does not terminate, we
have that any arrow from X to Y is a fixed-point semantics of the identity on X + Y , so C † is just the
full subcategory of D generated by C.
In order to convince the reader that unwanted functions are included in C† even in nondegenerate
cases, we exhibit another example: let C ⊂ Set be the distributive subcategory generated by the
successor and predecessor functions of Section 2.2; consider a recursively enumerable, nonrecursive
subset A ⊂ N. It is immediate to build a processor with codomain I + I which outputs in the first
copy of I on the elements of A and it is undefined elsewhere. But then the characteristic function of
A is a fix-point semantics of such a processor, and it is by construction nonrecursive.
Thus, in the opinion of the author the correct generalization of the idea of iterative computation
to nonterminating arrows remains an open problem.

Chapter 5

A new coding for IMP(G)
In this chapter we shall introduce a new coding for IMP(G) data and programs which is particularly
suited to implementation. We shall show how the elements of a derived set can be described as a
suitable forest, and that it is possible to associate inductively to a derived arrow a function on forests.
When discussing such strictly syntactical issues, two possibilities arise: a wordy description,
which highlights the main ideas and skips the syntactical details, or a very formal development,
which usually turns the reader away. Since the coding will be used in the formal specification of a
series of IMP(G) tools (see Chapter 6), in this chapter we shall discuss the main mathematical and
algorithmical ideas informally; a fully formal (even executable!) description of the same ideas will
be given in the specification.

5.1 A new efficient coding for IMP(G) data
In [Khalil & Walters:1993] a coding for the data of IMP(G) programs has been proposed which
represents an element of a set X derived from the basic sets A, B, . . . as a word, using the fact that
X is a “subset” of (A + B + · · · + I )∗ . Correspondingly, a specific coding has been given for the
terms built using a certain set of operators which come from the structure of a distributive category.
The coding transforms a term in a series of rewriting rules, whose application emulates the behaviour
of the function described by the term on a given word (representing an element of the domain of the
function).
We are going to propose a new, more efficient coding which is at the basis of the tools described
in the next chapter. The basic idea behind the coding is that, in analogy with standard programming,
products represent structures and sums represent union types. Thus, each time we shall need to
represent an element of a sum, we shall tag it with the index of its summand.

5.1.1

The old coding

Let D be the sum of all the basic sets plus {∗, e}. The length |X | of a derived set X is inductively
given by |∅| = |I | = 1 and |X + Y | = |X × Y | = |X | + |Y | (if X is seen as a tree, it is just its
number of leaves). An element of X is represented by a word over D:
(i). the only element of I is represented by ∗ (∅ has no elements, but we assign it the word e);
(ii). the elements of a basic set are represented by themselves (as one-letter words);
(iii). the elements of X × Y are represented by words uv, and the elements of X + Y by words ue |V |
or e|U | v, where u and v represent elements of X and Y , respectively.
59

CHAPTER 5. A NEW CODING FOR IMP(G)

60

The distinguished element e is used in order to tell which components of a derived set “do hold” a
value. For instance, if X = A + B then the elements of X can be elements of A or elements of B;
correspondingly, a representation of either of the form ae, or of the form eb. It is immediate to see
that the length of the word representing an element of X is |X |.

5.1.2

The new coding

The new coding we are going to propose is based on ordered forests whose leaves are labelled by
elements of the basic sets and whose nodes are labelled by natural numbers. We shall identify the
empty forest with the only element of I , the one-node forests with the elements of the basic sets,
denote by juxtaposition the ordered concatenation of forests and by Gn, f F the creation of a tree with
a root labelled by n ∈ N and having as first-level children the trees of the forest f . The precise
definition and properties of such a structure, the free N-motor on the sum of the basic sets, have
been studied in [Pair & Quère:1968, Vigna:1991, Kasangian & Vigna:1991a]. We shall describe the
manipulation of forest informally; the discussion can be recast in term of algebraic operations and
initiality in the category of N-motors.
We shall define our coding on the basis of a normal form for the derived sets. We shall consider
+ and × as operators of variable arity (something which is allowed by associativity). A flat term (or
object) is defined inductively as:
(i). a basic set;
(ii). a list of flat terms surrounded by “+(” and “)”, or “×(” and “)” (a +-list and a ×-list, respectively).
We confuse again a flat term and and its obvious interpretation as a set, calling both of them flat
objects.
Now we define a normal form (obtained by associative merge) on the flat objects which optimizes
the storage requirements. A flat object in normal form is inductively defined as:
(i). a basic set
(ii). a +-list of length different from 1, whose items are basic sets and ×-lists in normal form;
(iii). a ×-list of length different from 1, whose items are basic sets and +-lists in normal form.
In other words, flat objects in normal form do not contain lists with just one element, and it never
happens that a sublist can be merged in the containing one by associativity.
For each derived set (or flat object) X there is exactly one corresponding flat object in normal
form, obtained by list merging after having applied the mapping ν inductively defined by
ν(I )
ν(∅)

= ×()
= +()

ν(A) = A
ν(X + Y ) = +(ν(X ) ν(Y ))
ν(X × Y )

=

×(ν(X ) ν(Y )).

We shall denote the normal form of a flat object X by X̄ . By abuse of notation, we shall write X̄ for
ν(X ) when X is a derived set. Of course, many derived sets (or flat objects) correspond to a normal
form. Note also that there is a canonical isomorphism between a derived set X , ν(X ) and ν(X ).
Now the representation of an element x ∈ X , where X is a flat object, is defined as follows:

5.1. A NEW EFFICIENT CODING FOR IMP(G) DATA

61

(i). if X is a basic set, x represents itself;
(ii). if X = ×(X 1 X 2 · · · X p ), then x is a tuple hx 1 , x 2 , . . . , x p i, and if u k represents x k as an
element of X k the representation of x as an element of X is u 1 u 2 · · · u p ;
(iii). if X = +(X 1 X 2 · · · X p ), then x is a pair hu, ki, where 0 ≤ k < p and u represents x as an
element of X k , and the representation of x as an element of X is Gk, uF.
Given an element x of X , we shall write Bx for its representation as a forest (following the notation
of [Khalil & Walters:1993]); when X is a derived set, we shall write Bx for the representation of x as
an element of ν(X ). It is immediate that
Proposition 4 For all x, x 0 ∈ X , Bx = Bx 0 implies x = x 0 .
Note that for sake of notational simplicity we shall write the +(X ) (or ×(X )) for the simple
object or ×-list in normal form X (for the simple object or +-list in normal form X , respectively).
The notation is not ambiguous, since there are no +/×-lists in normal form with just one element,
and it allows us to describe in one shot as +(X 1 · · · X p ) a +-list, when p > 1, a ×-list or simple
object, when p = 1, or the empty set, when p = 0 (analogously for ×(X 1 · · · X p )).
Once we reduce to flat objects in normal form, it is immediate, for instance, to note that the space
necessary for storing n · X n is O(n 2 ) with the old coding and O(n) with the new one. In general, the
storage required for the sum of two flat objects is the sum of the storage for X and Y in the old case,
and the maximum (plus one) of the storage for X and Y in the new case.

5.1.3

Normalization and associativity

The new coding we just described has a disadvantage: while the associativity isomorphisms related
to the product, i.e., the maps
a
X × (Y × Z ) −
→ (X × Y ) × Z
derived from the projections, satisfy Bx = Ba(x) for every element x of X , and moreover Bx is exactly
the representation of x as an element of ×(X Y Z ), we have that if
b

X + (Y + Z ) −
→ (X + Y ) + Z
is the analogous isomorphism for the sum and z is an element of Z , Bz = G1, G1, zFF but Bb(z) =
G1, zF. Moreover, the representation of z as an element of +(X Y Z ) is G2, zF. Thus, the associativity
isomorphisms of product induce the identity at the representation level, but this does not happen for
the sum.
However, there is a simple way of overcoming this problem. For a forest u, let ū denote its normal
form with respect to the rewrite rule
G j, Gk, uFF = G j + k, uF.
It is straightforward to prove the following
Proposition 5 Let X , Y and Z be flat objects such that X = +(Y Z ); let Ȳ = +(Y1 · · · Yq ) and
Z̄ = +(Z 1 · · · Z r ), and suppose q, r > 0. Then if x 1 is an element of Y , with representation
u 1 in Ȳ , the representation of inj1 (x1 ) in X̄ is G0, u 1 F; analogously, if x 2 is an element of Z , with
representation u 2 in Z̄ , the representation of inj2 (x2 ) in X̄ is Gq, u 2 F. If q = 0 (or r = 0) the
representation of inj2 (x2 ) (or inj1 (x1 )) is u 2 (u 1 , respectively).

CHAPTER 5. A NEW CODING FOR IMP(G)

62

This proposition has several consequences: first of all, it explains how to obtain the representation
of an element of X as an element of X̄ ; second, it defines the effect of injections on representations;
third, it allows to reverse the effect of the injections:
Corollary 7 With the same notation of Proposition 5, suppose q, r > 1; then an element of Y (or Z )
injected in X̄ is coded as Gn, uF, with 0 ≤ n < q (q ≤ n < q + r , respectively). If q = 1 (r = 1,
respectively) its coding as an element of Ȳ is u, otherwise it is Gn, uF (Gn − q, uF, respectively).
The categorical result underlying the previous discussion is the coherence theorem for monoidal
categories (see [Mac Lane:1971]). The corollary of interest here is that if we choose a normal form
with respect to associativity of + and ×, there is a canonical way of making the interpretation of the
original term and of the normal form isomorphic.
Thus, we shall suppose that all objects are given in flat normal form (some preprocessing can
take care of this fact) and that all arrows are precomposed and postcomposed with the canonical
isomorphisms from and to the normal forms (in practice, we shall work in an equivalent category
where + and × happen to be strict). This has the major advantage that all the monoidal isomorphisms
(associativity and unit axioms) will induce identities at the representation level.

5.2 Coding IMP(G) programs
Recall that an IMP(G) program is an arrow in a free distributive category. Our goal is to transform it
into an operator on forests, which can be actually computed by a real machine.

5.2.1

Coding simple functions

We now introduce the coding of the simple functions, which is given by stating the effect of the
coding on normal form representations. For each basic function a we denote with ā the function that
a induces on the representations (and defined in the obvious way: if u = Bx then ā(u) = Ba(x)).
Ba : u
+(X ··· X p ),+(Y1 ··· Yq )
Binj1 1
:u
+(X ··· X p ),+(Y1 ··· Yq )
Binj2 1
:u
×(X 1 ··· X p ),×(Y1 ··· Yq )
Bproj1
: u 1 · · · u p v1 · · · vq
×(X 1 ··· X p ),×(Y1 ··· Yq )
Bproj2
: u 1 · · · u p v1 · · · vq

7→ ā(u)
7→

G0, uF

7→

G p, uF

7→

u1 · · · u p

B¡ X : u

7→ v1 · · · vq
7→ ε

B1 X : u

7→

u

Note that all operations on the right side produce automatically forests in normal form, except for the
injections, for which the required normalization is shallow: one just need to check that the rewrite
rule G j, Gk, uFF = G j + k, uF is applicable at the outermost level. We supposed p, q > 0, for
otherwise the injections trivialize to identities or initial maps.
The distributivity isomorphism has a more complex description; Corollary 7 tell us how to “unpack” the representation of an element of a sum, and, depending on q or r being equal to one, we

5.3. A TYPE-CHECKING ALGORITHM FOR IMP(G) PROGRAMS

63

have the following four cases:
−1
Bδ×(X
: uG0, vF
1 ··· X p ),+(Y1 ··· Yq ),+(Z 1 ··· Z r )

7→

G0, uvF if q = 1

uGk, vF
uGq, vF

7→
7→

G0, uGk, vFF if q > 1, k < q
Gn, uvF if r = 1

uGk, vF

7→

Gn, uGk − q, vFF if r > 1, k ≥ q

where we assumed p, q, r > 0 and
×(X 1 · · · X p + (Y1 · · · Yq )) = +(S1 · · · Sn );
note that n > 0, and that n > 1 implies p, q = 1, Y1 = ∗() and X 1 = +(S1 · · · Sn ). If p, q or r are
equal to zero, δ −1 is the identity or an injection.

5.2.2

Coding derived functions

To each operator used in the construction of derived arrows we associate inductively an operator on
forests:
B( f, g) : u
Bg ◦ f : u

7→ B f (u) B g(u)
7→ (Bg ◦ B f )(u).

In the case of the (− | −) operator, as for the distributivity isomorphism, we must take some more
care. Suppose dom( f ) = +(X 1 · · · X p ), dom(g) = +(Y1 · · · Yq ) and p, q > 0. Then, following
Corollary 7 we have
B( f | g) : G0, uF

7→ B f (u) if p = 1

Gk, uF
G p, uF

7→ B f (Gk, uF) if p > 1, k < p
7→ B f (u) if q = 1

Gk, uF

7→ B f (Gk − p, uF) if q > 1, k ≥ p.

The relevant result here is the following
Theorem 29 Let f be a derived function. Then B f (Bx) = B f (x).
Proof. A straightforward but tedious exercise in structural induction and case-by-case analysis.
The reader should notice that B− sends arrows to (simple) operations of forests. This will allow
to precompile an arrow into a kind of p-code which is easily executed.

5.3 A type-checking algorithm for IMP(G) programs
In the practical description of IMP(G) programs, we certainly want to forget the associativity isomorphisms, and at the same time to specify structural arrows in a polymorphic form (as we did, for inproj1X,Y

stance, in the proof of Theorem 4). It would indeed be cumbersome to have to write X × Y −−−−→ X
proj1

instead of just X × Y −−→ X . This implies that injections and projections should have constraints
inj1

relaxed with respect to the definition given in Section 2.1: we should admit X +Y −−→ X +(Y + Z ) or
proj1

inj1

proj1

X ×(Y × Z ) −−→ X ×Y . Note that we should admit also X −−→ X +(Y + Z ) or X ×(Y × Z ) −−→ X .
When specifying an IMP(G) program, we shall build an arrow using the usual operators and
constant of a distributive category (see Section 4.1.2), but with two important differences:

CHAPTER 5. A NEW CODING FOR IMP(G)

64

(i). each structural arrow can be also specified in a polymorphic form, e.g., proj 2 ;
(ii). the operators can be applied to any pair of arrows, regardless of the standard equational constraints (such as the domain of g being equal to the codomain of f when building g ◦ f ).
Note that we shall use “arrow” in this relaxed sense in the rest of this chapter, and in the next one.
The second point is imposed by the first one, because the equational conditions on domains and
codomains which restrain the application of an operator cannot be checked for polymorphic arrows.
Thus, there is no guarantee that we did not compose uncomposable functions, or that we did not write
( f, g) when f and g did not have the same domain. The type-checker of IMP(G) is an algorithm
which takes an arrow with specified domain and codomain, and outputs “yes” if there is a way of
instatiating the polymorphic arrows contained in the arrow in such a way to satisfy the usual compositional constraint. (Note that we do not claim that if the type-checker answers “no” no instantiation
is possible.)
Polymorphism is essential because it allows to use a friendly syntax, similar to the one which can
be found in mathematics papers. On the other hand, polymorphism makes type-checking much more
difficult, because suddenly there is a possibility that the (co)domain of an arrow is not computable,
in the following sense: We say that dom( f ) (or cod( f )) is computable for a simple arrow f if f is a
basic arrow, or a completely specified structural arrow; moreover, dom(!) are cod( ¡) computable; if
f is a derived arrow, its (co)domain is computable if the standard equations of category theory allow
to infer it from the (co)domains of the simple arrows it is built from. More details can be found in
Section 6.5.
f
Since the definition of a new arrow will be given in the form X −
→ Y , we shall check that f has
X as domain and Y as codomain up to associativity (and unity) isomorphisms. This means that we
cannot assume that the syntactic structure of the (co)domain will follow the structure of the arrow.
For instance, if f : X → Y and g : X → Z × W then
( f,g)

X −−−→ (Y × Z ) × W
should pass the type check, even if we have to modify the abstract syntax tree of the codomain to
Y × (Z × W ).
The approach we take is to transform the objects found in the program (i.e., the distributive
expressions), which are described using binary sums and products, into flat objects in normal form.
With this premise, the type-check of simple, polymorphic arrows consists just in verifying that the
form of the domain and codomain satisfies certain simple rules; for instance, domain and codomain
of an identity must be the same, while a first projection must to start on ×(X 1 · · · X p ) and end on
×(X 1 , · · · , X p0 ), with 0 < p 0 < p. A simple arrow which is not polymorphic can obviously be
type-checked directly.
( f,g)

Then, each time we have to type-check an arrow of the form X −−−→ Y , we try to split Ȳ , seen
as a ×-list, into two sublists, and we check that f and g are well-typed with respect to the domain X
and to the codomain given by the first and second sublist, respectively (a dual behaviour is kept with
respect to (− | −)). Of course, all splittings have to be tried. For instance, if f : X + X → Z and
g : Y → Z , we can write
( f | g) : X + (X + Y ) → Z .
When the distributive expressions will be turned in flat normal form the domain will become +(X X Y ),
and subsequently the rule for (− | −) will successfully try the splitting +(X X )/+(Y ) (the latter item
being reducible to the normal form Y ).
This mechanism can lead to ambiguous arrows. For instance, definining the arrow twist (commutativity isomorphism) as
(inj2 | inj1 )

X + (X + X ) −−−−−−→ (X + X ) + X

5.3. A TYPE-CHECKING ALGORITHM FOR IMP(G) PROGRAMS

65

does not make clear whether it is required to twist around the first or the second + sign (remember
that associativity is irrelevant). In these cases, it is necessary to specify completely the arrows, as in
(inj2X +X,X | inj1X +X,X )

X + (X + X ) −−−−−−−−−−−−→ (X + X ) + X.
g◦ f

List splitting, however, cannot take care of composition. If we have to check if X −−→ Z , we
need to establish that cod( f ) = dom(g). However, it is not possible in general to compute cod( f )
or dom(g) (also because f and g could be not well-typed). Nonetheless, we expect that arrows with
a unique semantics such as inj1 ◦¡ X : X → I + I should be checkable.
Whenever we compose two arrow, we should solve a set of type equations over objects. Some
theory is necessary in order to establish under which conditions a system of such equations has a
unique solution, and how to compute it. As a simple example, consider the arrow
proj2 ◦ f ◦inj1

X −−−−−−−→ Y 0
with f : X + X 0 → Y × Y 0 . The domain of f and the codomain of inj1 have to be the same, and
by definition of injection we write the equation X + V = X + X 0 (where V is a variable representing
the unknown part of the codomain of inj1 ) which admits the unique solution V = X 0 , because objects
form a cancellative monoid with respect to both sum and product. For analogous reasons we have
Y × Y 0 = V0 × Y 0 , which gives V0 = Y . In this simple case distinct variables appear in distinct
equations, but this does not happen in general.
While this is the “best” solution to the problem of type-checking composition of arrows, it has
big computational disadvantages. Moreover, it can be argued that simpler methods can lead to more
affordable type-checkers whose power is comparable to the previous case, in the sense that the arrows
which are no longer checkable with the simpler method are extremely artificial.
We want to describe here such a method. The basic idea is that when type-checking g ◦ f we just
f

g

need a reasonable guess for a Y such that X −
→Y −
→ Z . If f and g are well-typed with a certain
choice of Y , we have certainly Y = cod( f ) = dom(g). The simplest way of building such a Y is to
compute the domain of g (or the codomain of f ) assuming that f and g are well-typed. This allows
to use that standard equation of category theory, such as cod(( f, g)) = cod( f ) × cod(g). It is easy
to see, for instance, that in the case of inj1 ◦¡ X : X → I + I the algorithm would try to compute the
domain of inj1 , which is unknown, but would then try to compute the codomain of ¡ X , which is I ,
¡X

inj1

→ I and I −−→ I + I would be successful.
and then the type-checking of X −
More generally, it is not difficult to show that
Theorem 30 Let f 0 , f 1 , . . . , f n be a sequence of arrows. If for each k = 1, 2, . . . , n we have that
cod( f k−1 ) or dom( f k ) are computable, then f 0 ◦ f 1 ◦ · · · ◦ f n can be type-checked.
Getting back to our example
proj2 ◦ f ◦inj1

X −−−−−−−→ Y 0 ,
the type checker would perform as follows (supposing ◦ is left associative): dom(proj 2 ) is not comproj2

putable, but cod( f ◦ inj1 ) = cod( f ) = Y × Y 0 is, and Y × Y 0 −−→ Y 0 type-checks correctly. When
inj1

checking f ◦ inj1 , cod(inj1 ) cannot be built, but dom( f ) = X + X 0 , and finally X −−→ X + X 0 and
f

X + X0 −
→ Y × Y 0 type-check correctly.
It is of course possible to build artificial examples such as
inj1 ◦ proj1

X × Z −−−−−−→ X + Y.

66

CHAPTER 5. A NEW CODING FOR IMP(G)

In principle, we could establish (if X , Y and Z are simple objects) that the codomain of proj 1 is X ,
which coincides with the domain of inj1 . Such arrows, however, are almost unreadable by humans
for the same reasons which make it difficult to manage them on a computer.

5.4 Some remarks on implementation
We would like to remark that the new coding proposed here can be easily and efficiently implemented
on a standard computing machine as follows: each tree is represented by a pointer (either to some
basic data representation, or to a forest tagged with a natural number), and a forest is represented by
an array of such pointers. It is not difficult to see that this is the standard way of storing variant record,
for instance in object-oriented languages with dynamic typing. Thus, the coding presented here is an
essential step towards an efficient implementation of distributive programs on standard machines.
It could be argued that the old coding could be “compressed” by representing sequences of the
special e symbol as tagged natural numbers. Thus, for instance, the representation of an element of
n · X n would be of the form e jn x1 x2 · · · x n ekn , which requires O(n) space. However, this would
impose the application of a very complicated “packing/unpacking mechanism” every time a derived
arrow has to be computed. Moreover, we would always need, for instance, O(n) storage for I n
(against O(1) in the new coding).
In other words, in real implementations the new coding has always a good advantage (although
in some cases it is asymptotically equivalent).

Chapter 6

A literate IMP(G) implementation
This chapter presents a series of tools for the manipulation of programs written in IMP(G) which use
the techniques developed in Chapter 5. The tools have been realized inside ASF+SDF, a system for
developing specifications and manipulating rewriting systems created at the University of Amsterdam
[Klint:1993]. The description, which alternates formal and natural language, is an example of literate
programming [Knuth:1984], and has been realized using the tool ToLATEX [Visser & Klint:1994]. The
type-checker has been presented in [Vigna:1995].
The choice of ASF+SDF has the great advantage of making extending or changing the syntax
of the language very easy, so that one can try, for instance, many different mathematical formalisms
(e.g., f ◦ g, f g or f ; g for functional composition). The main disadvantage is the need of large resources, even for running relatively small programs. However, this is not a big issue, since our interest
here is in implementing in detail the algorithmical and mathematical ideas described in Chapter 5.
The description given in the ASF+SDF syntax, while being very near to the standard mathematical
notation, has the advantage of being executable. A direct implementation in a more efficient language
would be straightforward.
The reader interested in understanding every detail of the following pages should have some
knowledge of the ASF+SDF system, but for a general understanding no particular background is necessary. We just remark that in the following sections the formal syntax is context-free (the rules are
written “from right to left”, i.e., they are seen as functions rather than productions), while the equational part specifies rewrite rules with equational conditions. “Execution” in the context of ASF+SDF
means that a term is reduced using the given equations, thought of as reduction rules directed from
left to right (no specified order should be assumed, except that the rules marked by otherwise will be
the last to be executed). A rule is applied only if its conditions are all satisfied.
The key feature of ASF+SDF we shall use is the possibility of specifying list sorts and list variables (for examples of usage of lists, see for instance Section 6.7). When a list sort term is unified
with one or more list sort variables, many splitting are usually possible. For instance, let ABC be
such a term; unification with x + y ∗ (where x + is a list sort variable which cannot be instantiated to
an empty list, and y ∗ is a list sort variable which can be instantiated to any list) can produce several
different results, such as x + = A and y ∗ = C B, or x + = ABC and y ∗ equal to the empty list.
In this case, when ASF+SDF tries to satisfy the conditions of an equation all possible splittings are
checked. On failure, the system backtracks and tries a new splitting, which could possibly lead to a
positive result. This makes an implementation of the type-checking algorithm informally described
in Chapter 5 strightforward, but with a drawback: it is not possible to detect ambiguous arrows. This
is of course a limitation of the present implementation, and not of the algorithm itself.
Note that we omitted from the specification the modules providing layout tokens, boolean variables and integer support, since they are standard.
67

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

68

6.1 Identifiers
This module defines the identifiers allowed in the declaration and definition of objects and arrows.
Instead of hard-coding the names of the structural arrows, we define one sort and one context free
function per structural arrow, and assign a literal to each sort. Then, the literals are referred to through
a variable of the corresponding sort. In this way we obtain three effects: the names can be easily
redefined, we can name in several ways the same structural arrow, and the possibility of a wrong
interpretation of a literal (i.e., as an basic arrow instead of a structural arrow) is avoided, due to the
precedence rules of SDF.
imports Layout
exports
sorts BASIC-ARROW BASIC-OBJ INITIAL TERMINAL IDENTITY
FIRST-INJ SECOND-INJ FIRST-PROJ SECOND-PROJ
INITIAL-MAP TERMINAL-MAP DIST
An arrow or object name must start with a letter (lower case for an arrow, upper case for an object).
Note that we do not allow the usage of dashes, for they would create spurious syntax errors each time
an object is not separated from a DART by a layout token (see Section 6.3). Circumflex accents and
underscores are allowed in order to use (the TEX version of) mathematical notations such as f 1 or k 3 .
lexical syntax
[a-z][A-Za-z0-9 ˆ]∗ → BASIC-ARROW
[A-Z][A-Za-z0-9 ˆ]∗ → BASIC-OBJ
It would be nice to be able to use “¡” for terminal maps, as it is available in ISO-8859.1 (i.e., Latin-1),
but this would make the specification font-dependent; moreover, the current version of ASF+SDF
does not support extended character codes. The alias used for Terminal-Map, however, is exactly “¡”.
context-free syntax
→ TERMINAL
“I ”
“O”
→ INITIAL
“id”
→ IDENTITY
“inj 1” → FIRST-INJ
“inj 2” → SECOND-INJ
“proj 1” → FIRST-PROJ
“proj 2” → SECOND-PROJ
“!”
→ INITIAL-MAP
“term” → TERMINAL-MAP
“dist” → DIST
The following variables are all aliased to a representation which matches the context free syntax. For
instance, First-Proj becomes proj1 . Note that Dist becomes δ −1 .
variables
Initial
Terminal
Identity
First-Inj
First-Proj
Second-Inj
Second-Proj
Initial-Map

→ INITIAL
→ TERMINAL
→ IDENTITY
→ FIRST-INJ
→ FIRST-PROJ
→ SECOND-INJ
→ SECOND-PROJ
→ INITIAL-MAP

6.2. OBJECTS

69

Terminal-Map → TERMINAL-MAP
Dist
→ DIST

6.2 Objects
An object is built by summing or multiplying together objects (starting from simple ones). We have
standard assumptions about the relative priority of sum and product (note that we allow juxtaposition
to denote product).
We note again that the ability to handle ISO-8859.1 codes would be very useful here, because the
symbol “×” is part of its character set. Aliasing “*” to “×” is not possible, for also the occurrences
of “*” in variable name definitions would be aliased.
imports Layout Identifiers6.1
exports
sorts STRUCTURAL-OBJ SIMPLE-OBJ OBJ
context-free syntax
TERMINAL
→ STRUCTURAL-OBJ
INITIAL
→ STRUCTURAL-OBJ
STRUCTURAL-OBJ → SIMPLE-OBJ
BASIC-OBJ
→ SIMPLE-OBJ
SIMPLE-OBJ

→ OBJ

{left}
OBJ “+” OBJ
→ OBJ
{left}
OBJ “∗” OBJ
→ OBJ
{left}
OBJ OBJ
→ OBJ
{bracket}
“(” OBJ “)”
→ OBJ
priorities
{left: OBJ OBJ → OBJ, OBJ “∗”OBJ → OBJ} > OBJ “+”OBJ → OBJ
Object variables are named with a single letter, in order to follow the mathematical custom. We
use different group of letters in order to discriminate between basic, simple and compound entities.
The underscore will be removed by aliasing, and has the sole purpose of avoiding clashes of object
names (we suppose that names like A or X will be rather common in user programs). Note that
since variables representing structural objects are seldom used, we prefer to name them in a different
manner.
variables
→ BASIC-OBJ
“ ”[ABC][0-9]∗[ 0 ]∗
“ ”[ABC]“∗”[0-9]∗[ 0 ]∗ → {BASIC-OBJ “,”}∗
Structural-Obj [0-9]∗[ 0 ]∗ → STRUCTURAL-OBJ
“ ”[ST][0-9]∗[ 0 ]∗
→ SIMPLE-OBJ
→ OBJ
“ ”[XYZ][0-9]∗[ 0 ]∗
“ ”[XYZ]“∗”[0-9]∗[ 0 ]∗ → {OBJ “,”}∗
The only equation described here has the purpose of making a product denoted by juxtaposition
explicit.
equations
[Obj1]

X Y = X ∗Y

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

70

6.3 Arrows
An arrow is built by summing, multiplying, pairing (on sum or products), composing or iterating
other arrows (starting from simple ones). DART-STARTER and DART-ENDER are visual markers
which will be used in order to describe composition of arrows in Section 6.13.
Note that each structural arrow can be described in two ways: a completely specified structural
arrow contains full information about its domain and codomain, while a polymorphic structural arrow
is declared just by assigning a type (identity, first projection, and so on). The unification mechanism
of the type-checker will find out a reasonable meaning for the arrow. Analogously, it is possible to
use the call[ − ] operator in the short form call[ f ].
Composition can be specified in two form: by means of the “;” operator, or using the “◦” operator.
The meaning of f ; g is “do first f , then g,” while the meaning of f ◦ g is “do first g, then f ”.
imports Layout Identifiers6.1 Objects6.2
exports
sorts STRUCTURAL-ARROW SIMPLE-ARROW ARROW
DART-STARTER DART-ENDER DART
lexical syntax
[\−]+
→ DART-STARTER
[\−]+“>” → DART-ENDER
context-free syntax
IDENTITY
→ STRUCTURAL-ARROW
FIRST-INJ
→ STRUCTURAL-ARROW
FIRST-PROJ
→ STRUCTURAL-ARROW
SECOND-INJ
→ STRUCTURAL-ARROW
SECOND-PROJ
→ STRUCTURAL-ARROW
INITIAL-MAP
→ STRUCTURAL-ARROW
TERMINAL-MAP
→ STRUCTURAL-ARROW
DIST
→ STRUCTURAL-ARROW
IDENTITY “(” OBJ “)”
→ STRUCTURAL-ARROW
FIRST-INJ “(” OBJ “,” OBJ “)”
→ STRUCTURAL-ARROW
FIRST-PROJ “(” OBJ “,” OBJ “)”
→ STRUCTURAL-ARROW
SECOND-INJ “(” OBJ “,” OBJ “)” → STRUCTURAL-ARROW
SECOND-PROJ “(” OBJ “,” OBJ “)” → STRUCTURAL-ARROW
INITIAL-MAP “(” OBJ “)”
→ STRUCTURAL-ARROW
TERMINAL-MAP “(” OBJ “)”
→ STRUCTURAL-ARROW
DIST “(” OBJ “,” OBJ “,” OBJ “)” → STRUCTURAL-ARROW
BASIC-ARROW
STRUCTURAL-ARROW

→ SIMPLE-ARROW
→ SIMPLE-ARROW

SIMPLE-ARROW

→ ARROW

ARROW “+” ARROW
ARROW “∗” ARROW
ARROW “|” ARROW
ARROW “,” ARROW
ARROW “;” ARROW

→ ARROW
→ ARROW
→ ARROW
→ ARROW
→ ARROW

{right}
{right}
{right}
{right}
{right}

6.4. SUPPORT

71

ARROW “◦” ARROW

→ ARROW

{right}

“(” ARROW “)”

→ ARROW

{bracket}

call “[” OBJ “,” OBJ “,” OBJ “,”
ARROW “]”

→ ARROW

call “[” ARROW “]”

→ ARROW

DART-STARTER
ARROW
DART-ENDER

→ DART

The reader could have noticed that we allow to pair two arrows with “|” or “,” without external
brackets. Thus, f | g and f, g are valid arrows, while the standard notation would require ( f | g)
and ( f, g). However, dropping the brackets allows to pair an arbitrary number of arrows instead of
just two. Moreover, since we declare that the two kinds of pairing are reciprocally non-associative,
and that they are at the bottom of the priority order, the user will be always forced to surround a
pairing with brackets, except at the outermost level.
priorities
ARROW “;”ARROW → ARROW > ARROW “∗”ARROW → ARROW >
ARROW “+”ARROW → ARROW > {non-assoc: ARROW “|”ARROW → ARROW,
ARROW “,”ARROW → ARROW},
ARROW “◦”ARROW → ARROW >
ARROW “∗”ARROW → ARROW
The same considerations of Section 6.2 about variable naming apply here. Note that Dart-Starter and
Dart-Ender are aliased to − and →.
variables
→ BASIC-ARROW
“ ”[abc][0-9]∗[ 0 ]∗
“ ”[abc]“∗”[0-9]∗[ 0 ]∗
→ {BASIC-ARROW “,”}∗
Structural-Arrow [0-9]∗[ 0 ]∗ → STRUCTURAL-ARROW
“ ”[st][0-9]∗[ 0 ]∗
→ SIMPLE-ARROW
“ ”[fgh][0-9]∗[ 0 ]∗
→ ARROW
Dart-Starter
→ DART-STARTER
Dart-Ender
→ DART-ENDER
The only equation described here has the purpose of reducing a composition denoted by f ◦ g to the
other form.
equations

[Arr1]

g ◦ f = f; g

6.4 Support
This module contains syntax and equations which are needed by all high-level modules. In particular,
it takes care of the conversion to flat normal form.
imports Identifiers6.1 Objects6.2 Arrows6.3 Booleans Ints

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

72

The sort FOBJ (short for “flat object”) describes objects in a form which is much less readable, but
also much less ambiguous, than the one described in Section 6.2. In practice, sums and products will
be lists with explicit bracketing, and we shall arrange things in such a way that flat objects are always
in normal form, i.e., they do not contain lists with just one element or sublists which could be merged
by associativity. The operator flat turns an object into a flat object. The rôle of the additional symbols
⊕ and ⊗ and of the last four operators will be described in detail in the equational part.
exports
sorts FOBJ
context-free syntax
BASIC-OBJ
⊥

→ FOBJ
→ FOBJ

“∗” “(” FOBJ∗ “)”
“+” “(” FOBJ∗ “)”

→ FOBJ
→ FOBJ

“⊕” “(” FOBJ∗ “)”
“⊗” “(” FOBJ∗ “)”

→ FOBJ
→ FOBJ

flat “[” OBJ “]”

→ FOBJ

len “[” FOBJ∗ “]”
slen “[” FOBJ “]”
plen “[” FOBJ “]”

→ INT
→ INT
→ INT

elem INT from FOBJ+ → FOBJ
An arrow specification is given by a basic arrow name, a domain and a codomain. Instead of just
writing down a triple, we prefer a syntax which mimicks the standard mathematical notation f :
X → Y . The sorts SPEC-LIST and BASIC-OBJ-LIST are used during the type-check in order to
store the currently known entities (in other words, they are the symbol tables). Note the different
notation (X → Y and X
Y ) for basic arrows and arrows which have been compiled.
sorts SPEC SPEC-LIST BASIC-OBJ-LIST
context-free syntax
BASIC-ARROW “:” FOBJ “→” FOBJ → SPEC
BASIC-ARROW “:” FOBJ “ ” FOBJ → SPEC
“[” {SPEC “,”}∗ “]”
→ SPEC-LIST
“[” {BASIC-OBJ “,”}∗ “]”
→ BASIC-OBJ-LIST
The following function returns the domain and codomain of a basic arrow, taking them from a specification list; in case of failure, “⊥” is returned. Again, the domain and codomain are returned in a
slightly different form if the arrow has been previously compiled.
sorts DOM-COD
context-free syntax
“[” FOBJ “→” FOBJ “]”
“[” FOBJ “ ” FOBJ “]”
⊥

→ DOM-COD
→ DOM-COD
→ DOM-COD

spec of BASIC-ARROW in SPEC-LIST → DOM-COD
These three functions are predicates, i.e., they are guaranteed to be reducible to true or false. They
are used by the type-checker in order to issue meaningful error messages when the user has typed the
wrong name for an object or an arrow.

6.4. SUPPORT

73

context-free syntax
BASIC-OBJ is in BASIC-OBJ-LIST → BOOL
OBJ is built from BASIC-OBJ-LIST → BOOL
ARROW is built from SPEC-LIST → BOOL
The variables denoting flat objects have names which are implemented directly as TEX commands.
Thus, the choice of the actual symbols is left to the definition of the commands \flX, \flY and
\flZ. The present choice (4, 2 and ) is motivated by the need of choosing symbols easily distinguishable from the ones assigned to (simple) objects (moreover, the author always loved the fact that
4 and 2 are disconnected).
variables
Spec [0-9]∗[ 0 ]∗
→ SPEC
Spec “∗”[0-9]∗[ 0 ]∗ → {SPEC “,”}∗
“4”[0-9]∗[ 0 ]∗
→ FOBJ
“2”[0-9]∗[ 0 ]∗
→ FOBJ
“”[0-9]∗[ 0 ]∗
→ FOBJ
“4”“+”[0-9]∗[ 0 ]∗ → FOBJ+
“2”“+”[0-9]∗[ 0 ]∗ → FOBJ+
“”“+”[0-9]∗[ 0 ]∗ → FOBJ+
“4”“∗”[0-9]∗[ 0 ]∗ → FOBJ∗
“2”“∗”[0-9]∗[ 0 ]∗ → FOBJ∗
“”“∗”[0-9]∗[ 0 ]∗ → FOBJ∗
equations

(De)normalization of flat objects. Our first set of equations defines the rules for normalizing flat
objects. First of all, we discard useless operators; then, we merge associatively sublists. A term in
normal form with respect to these rules is guaranteed to be a flat object in normal form.
+(4) = 4
[Snfp1] ∗(4) = 4
[Snfs1]

[Snfs2]

+(4∗ +(2∗ ) ∗ ) = +(4∗ 2∗ ∗ )

[Snfp2]

∗(4∗ ∗(2∗ ) ∗ )

= ∗(4∗ 2∗ ∗ )

These two rules, on the contrary, aims at denormalizing a flat object in normal form. When we shall
be interested in seeing a given flat object as a sum (possibly with just one summand) we shall apply
the ⊕ operator to the object. Since ⊕ and + merge, but ⊕ is not cancelled when applied to a single
object, the result will always be a ⊕-list (the same, of course, is true for ⊗).
[Snfos3]

⊕(+(4∗ )) = ⊕(4∗ )

[Snfop3]

⊗(∗(4∗ )) = ⊗(4∗ )

Finally, this function inductively traverses an object tree, mapping binary operators to lists of two
elements. The result is a flat object which will be normalized by the previous equations. Note that the

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

74

initial and terminal objects are represented by the empty +-list and by the empty ×-list, respectively.
flat[A]
flat[∅]
[Sfl3] flat[I ]

[Sfl1]

[Sfl2]

[Sfl4]
[Sfl5]

= A
= +()
= ∗()

flat[X ∗ Y ] = ∗(flat[X ] flat[Y ])
flat[X + Y ] = +(flat[X ] flat[Y ])

Calculating the length of a flat object. The following rules specify how to compute the length of a
list of flat objects and the length as a sum (or a product) of a flat object (a sum is seen as a one-factor
product, and a product is seen as a one-summand sum). Note the application of the ⊕/⊗ operators.
= 0

[Slen1]

len[]

[Slen2]

len[4 4∗ ] = 1 + len[4∗ ]

⊕(4) = ⊕(4∗ ) ⇒ slen[4] = len[4∗ ]
∗
∗
[Splen] ⊗(4) = ⊗(4 ) ⇒ plen[4] = len[4 ]
[Sslen]

This function returns the n-th element of a list of flat objects (the first element having index 0). It is
useful when type-checking the data corresponding to a sum.
[Sel1]

elem 0 from 4 4∗ = 4

[Sel2]

n 6= 0 ⇒ elem n from 4 4+ = elem n − 1 from 4+

Extracting the specification of a simple arrow. Here we have to discover the domain and codomain
of a given simple arrow by scanning the given specification list. If the arrow is not known we return
“⊥”.

spec of a in []
= ⊥
∗
[Ssp2] spec of a in [a : 4 → 2, Spec ] = [4 → 2]
2, Spec∗ ] = [4
2]
[Ssp3] spec of a in [a : 4

[Ssp1]

[Ssp4]

a 6= b ⇒ spec of a in [b : 4 → 2, Spec∗ ] = spec of a in [Spec∗ ]

[Ssp5]

a 6= b ⇒ spec of a in [b : 4

Predicates.
list.

2, Spec∗ ] = spec of a in [Spec∗ ]

The following predicate returns true if the given basic object is in the given basic object

[Sii2]

A is in []
= false
∗
A is in [A, A ] = true

[Sii3]

A 6= B ⇒ A is in [B, A∗ ] = A is in [A∗ ]

[Sii1]

6.5. DOMCOD

75

The following two predicates go one step further, and scan inductively an object (arrow) in order to
establish if it has been built using valid simple objects (arrows, respectively). Note the difference
between variables denoting simple and compound entities.
A is built from [A∗ ]

[Sobf1]

= A is in [A∗ ]

Structural-Obj is built from [A ∗ ] = true
∗
[Sobf3] X + Y is built from [A ]
= X is built from [A∗ ] ∧ Y is built from [A∗ ]
[Sobf2]

X ∗ Y is built from [A ∗ ]

[Sobf4]

= X is built from [A∗ ] ∧ Y is built from [A∗ ]

spec of a in [Spec∗ ] = ⊥
[Sabf1]

a is built from [Spec∗ ] = false

spec of a in [Spec∗ ] 6= ⊥
[Sabf2]

a is built from [Spec∗ ] = true

[Sabf3]

s is built from [Spec∗ ] = true

[Sabf4]

f + g is built from [Spec∗ ]

= f is built from [Spec∗ ] ∧ g is built from [Spec∗ ]

f ∗ g is built from [Spec∗ ]
f | g is built from [Spec∗ ]
f , g is built from [Spec∗ ]

= f is built from [Spec∗ ] ∧ g is built from [Spec∗ ]
= f is built from [Spec∗ ] ∧ g is built from [Spec∗ ]
= f is built from [Spec∗ ] ∧ g is built from [Spec∗ ]

[Sabf5]
[Sabf6]
[Sabf7]

[Sabf9]

f ; g is built from [Spec∗ ]
= f is built from [Spec∗ ] ∧ g is built from [Spec∗ ]
call[X , Y , Z , f ] is built from [Spec∗ ] = f is built from [Spec∗ ]

[Sabf10]

call[ f ] is built from [Spec∗ ]

[Sabf8]

= f is built from [Spec∗ ]

6.5 DomCod
This module is devoted to the machinery which is necessary in order to compute the domain and
codomain of an arrow.
imports Objects6.2 Arrows6.3 Booleans Support6.4
It is most important to note that these functions work assuming that their argument is well-typed. If
this is not the case, the result should be checked using the type-checker (see Section 6.9).
exports
context-free syntax
dom “[” ARROW “]” using SPEC-LIST → FOBJ
cod “[” ARROW “]” using SPEC-LIST → FOBJ
The general idea of the algorithm we shall use is as follows: we assume that the given arrow is welltyped, and we apply the standard equations which give the the domain and codomain of an arrow of
a free distributive category. When we get to a structural arrow, there is a definite possibility that we

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

76

cannot compute its domain or codomain. In this case, we return ⊥. Any flat object contaning ⊥ is
reduced to ⊥ by the first two equations, so we can safely apply structural induction.
equations
+(4∗ ⊥ 2∗ ) = ⊥
∗
∗
[DCnf2] ∗(4 ⊥ 2 ) = ⊥

[DCnf1]

Building the (co)domain of a basic or compiled arrow. We can always build the (co)domain of a
basic arrow, or of a compiled arrow, by looking at the given specification list.

spec of a in [Spec∗ ] = [4 → 2]
[DCda1]

dom[a] using [Spec∗ ] = 4

spec of a in [Spec∗ ] = [4
[DCda2]

2]

∗

dom[a] using [Spec ] = 4

spec of a in [Spec∗ ] = ⊥
[DCda3]

dom[a] using [Spec∗ ] = ⊥

spec of a in [Spec∗ ] = [4
[DCca1]

2]

∗

cod[a] using [Spec ] = 2

spec of a in [Spec∗ ] = [4 → 2]
[DCca2]

cod[a] using [Spec∗ ] = 2

spec of a in [Spec∗ ] = ⊥
[DCca3]

cod[a] using [Spec∗ ] = ⊥

Building the (co)domain of a structural arrow. The following list of equations is rather trivial.
We just mention that initial and terminal maps are the only ones for which we can compute something
in the polymorphic case.
[DCdid]

dom[1] using [Spec∗ ]

= ⊥

∗

cod[1] using [Spec ]
= ⊥
∗
[DCdID] dom[1(X )] using [Spec ] = flat[X ]
∗
[DCcID] cod[1(X )] using [Spec ] = flat[X ]

[DCcid]

[DCdi1]

dom[inj1 ] using [Spec∗ ]

= ⊥

∗

[DCdI1]

cod[inj1 ] using [Spec ]
= ⊥
dom[inj1 (X , Y )] using [Spec∗ ] = flat[X ]

[DCcI1]

cod[inj1 (X , Y )] using [Spec∗ ] = flat[X + Y ]

[DCci1]

6.5. DOMCOD

77

dom[inj2 ] using [Spec∗ ]

[DCdi2]

= ⊥

cod[inj2 ] using [Spec∗ ]
= ⊥
∗
[DCdI2] dom[inj2 (X , Y )] using [Spec ] = flat[Y ]

[DCci2]

cod[inj2 (X , Y )] using [Spec∗ ] = flat[X + Y ]

[DCcI2]

[DCdp1]
[DCcp1]

dom[proj1 ] using [Spec∗ ]
cod[proj1 ] using [Spec∗ ]

= ⊥
= ⊥

dom[proj1 (X , Y )] using [Spec∗ ] = flat[X ∗ Y ]
∗
[DCcP1] cod[proj1 (X , Y )] using [Spec ] = flat[X ]

[DCdP1]

dom[proj2 ] using [Spec∗ ]
= ⊥
∗
[DCcp2] cod[proj2 ] using [Spec ]
= ⊥
∗
[DCdP2] dom[proj2 (X , Y )] using [Spec ] = flat[X ∗ Y ]

[DCdp2]

[DCcP2]

[DCdini]

cod[proj2 (X , Y )] using [Spec∗ ] = flat[Y ]
dom[!] using [Spec∗ ]

= +()

cod[!] using [Spec∗ ]
= ⊥
∗
[DCdINI] dom[!(X )] using [Spec ] = +()
∗
[DCcINI] cod[!(X )] using [Spec ] = flat[X ]

[DCcini]

dom[¡] using [Spec∗ ]
= ⊥
∗
¡
[DCcter] cod[ ] using [Spec ]
= ∗()
∗
¡
[DCdTER] dom[ (X )] using [Spec ] = flat[X ]
∗
[DCcTER] cod[¡(X )] using [Spec ] = ∗()

[DCdter]

[DCdd1]

dom[δ −1 ] using [Spec∗ ]

−1 ]
[DCcd2] cod[δ

using [Spec ]

−1 (X ,
[DCdD1] dom[δ
[DCcD2]

= ⊥

∗

= ⊥
∗

Y 1 , Y 2 )] using [Spec ] = flat[X ∗ (Y 1 + Y 2 )]

cod[δ −1 (X , Y 1 , Y 2 )] using [Spec∗ ] = flat[X ∗ Y 1 + X ∗ Y 2 ]

Building the (co)domain of a derived arrow. Composition, sum and product of functions have
very simple rewrite rules (remember that any flat object containing ⊥ reduces to ⊥).
dom[ f + g] using [Spec∗ ] = +(dom[ f ] using [Spec∗ ] dom[g] using [Spec∗ ])
∗
∗
∗
[DCcs] cod[ f + g] using [Spec ] = +(cod[ f ] using [Spec ] cod[g] using [Spec ])
[DCds]

[DCdp]

dom[ f ∗ g] using [Spec∗ ] = ∗(dom[ f ] using [Spec∗ ] dom[g] using [Spec∗ ])

[DCcp]

cod[ f ∗ g] using [Spec∗ ] = ∗(cod[ f ] using [Spec∗ ] cod[g] using [Spec∗ ])

[DCdco]

dom[ f ; g] using [Spec∗ ] = dom[ f ] using [Spec∗ ]

[DCcco]

cod[ f ; g] using [Spec∗ ] = cod[g] using [Spec∗ ]

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

78

The case of the (− | −) and (−, −) operators is more interesting. When computing the codomain of
( f | g), we can take the information either from f or from g. If ( f | g) is well-typed and both f
and g have a computable codomain, then the information will be the same, but it is possible that the
codomain of f or g is not computable because of polymorphism. This is why we analyze all possible
cases. Analogous (but dual) considerations can be done about the (−, −) operator.
[DCdb]

dom[ f | g] using [Spec∗ ] = +(dom[ f ] using [Spec∗ ] dom[g] using [Spec∗ ])
cod[ f ] using [Spec∗ ] 6= ⊥

[DCcb1]

cod[ f | g] using [Spec∗ ] = cod[ f ] using [Spec∗ ]
cod[g] using [Spec∗ ] 6= ⊥

[DCcb2]

cod[ f | g] using [Spec∗ ] = cod[g] using [Spec∗ ]
cod[ f ] using [Spec∗ ] = ⊥, cod[g] using [Spec∗ ] = ⊥

[DCcb3]

cod[ f | g] using [Spec∗ ] = ⊥
dom[ f ] using [Spec∗ ] 6= ⊥

[DCdc1]

dom[ f , g] using [Spec∗ ] = dom[ f ] using [Spec∗ ]
dom[g] using [Spec∗ ] 6= ⊥

[DCdc2]

dom[ f , g] using [Spec∗ ] = dom[g] using [Spec∗ ]
dom[ f ] using [Spec∗ ] = ⊥, dom[g] using [Spec∗ ] = ⊥

[DCdc3]

[DCcc]

dom[ f , g] using [Spec∗ ] = ⊥

cod[ f , g] using [Spec∗ ] = ∗(cod[ f ] using [Spec∗ ] cod[g] using [Spec∗ ])

Building the (co)domain of call[ f ]. Unless an application of call[ − ] has been completely specified, there is nothing we can say about the domain and codomain of an iterated arrow. We could try to
break the domain of f in two summands in all possible ways, but nothing guarantees that the computation of the codomain would be coherent with the chosen splitting (so for f : X +U +U → U +U +Y
we could obtain dom(call[ f ]) = X but cod(call[ f ]) = U + Y ).
[DCdCALL]

dom[call[X , Y , Z , f ]] using [Spec∗ ] = flat[X ]

[DCcCALL]

cod[call[X , Y , Z , f ]] using [Spec∗ ] = flat[Z ]

[DCdcall]

dom[call[ f ]] using [Spec∗ ] = ⊥

[DCccall]

cod[call[ f ]] using [Spec∗ ] = ⊥

6.6. DATA

79

6.6 Data
This module specifies the representation of the elements of a flat object in normal form. It is essentially a description of the operators of the free N-motor [Vigna:1991] on the set of terms of sort
BASIC-DATA. Note that the empty forest, which represents the only element of I , is the empty term,
and that the terms of sort SINGLE-DATA are exactly the trees.
Should syntactical ambiguities arise (we do not know which are the subsorts of BASIC-DATA,
because they are user-specified) the generators (i.e., the terms of sort BASIC-DATA) can be enclosed
in { and }.
imports Layout Ints
exports
sorts DATA BASIC-DATA SINGLE-DATA DATA-DATA
context-free syntax
“{” BASIC-DATA “}” → BASIC-DATA {bracket}
BASIC-DATA
→ SINGLE-DATA
“G” INT “,” DATA “F” → SINGLE-DATA
SINGLE-DATA∗

→ DATA

There will be situations in which we shall want to concatenate two forests. The dot operator serves
this purpose.
context-free syntax
DATA “·” DATA → DATA
variables
→ BASIC-DATA
“ ”[e][0-9]∗[ 0 ]∗
“ ”[u][0-9]∗[ 0 ]∗
→ SINGLE-DATA
“ ”[u]“+”[0-9]∗[ 0 ]∗ → SINGLE-DATA+
“ ”[u]“∗”[0-9]∗[ 0 ]∗ → SINGLE-DATA∗
“ ”[d][0-9]∗[ 0 ]∗
→ DATA
The first equation of this module is fundamental; it normalizes the representation of the elements of
a sum when they are injected into another sum. The other equation implements trivially the concatenation of forests.
equations

[Dnf1]

G m, G n, d F F = G m + n, d F

[Dnf2]

u∗ · u∗0 = u∗ u∗0

6.7 Errors
This module provides error messages and error lists for the compiler and the type-checker. Beside
duplicate or missing identifiers, we could discover that an arrow does not start or end where it should.
We also define a dot operator which concatenates lists of errors.

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

80

imports Objects6.2 Arrows6.3
exports
sorts ERROR ERROR-LIST
context-free syntax
“object name” SIMPLE-OBJ “already used”
→ ERROR
“arrow name” SIMPLE-ARROW “already used”
→ ERROR
→ ERROR
“object” OBJ “contains undeclared basic objects”
“arrow” ARROW “contains undeclared basic arrows” → ERROR
“arrow” ARROW “is not from” OBJ “to” OBJ
→ ERROR
→ ERROR
“arrow” ARROW “is ambiguous”
“[” {ERROR “,”}∗ “]”

→ ERROR-LIST
→ ERROR-LIST {left}

ERROR-LIST “·” ERROR-LIST
variables
Error [0-9]∗[ 0 ]∗
→ ERROR
Error “∗”[0-9]∗[ 0 ]∗ → {ERROR “,”}∗
equations

[Err1]

[Error∗1 ] · [Error∗2 ] = [Error∗1 , Error∗2 ]

6.8 IMP-syntax
The syntax of an IMP(G) program is very simple: we start with a comma-separated list of basic
objects, followed by a comma-separated list of references to basic arrows (a reference being made of
a name, a domain and a codomain). Finally, a colon-separated list of arrow definitions is given. We
use lib for introducing list of references because, in essence, the basic arrows (i.e., the basic graph
G) have the same rôle of a library in a standard programming language.
In this implementation, an arrow is defined by juxtaposing a number of steps; each step is formed
by a dart, i.e., an ARROW surrounded by some graphical syntactic sugar, and by an object (representing the codomain of the current step, and the domain of the following one). The sugar aims at
mimicking the standard notation
g

h

f :X−
→Y −
→Z
for f = h ◦ g, because the semantics of juxtaposition of darts is composition.
imports Arrows6.3 Objects6.2 Identifiers6.1
exports
sorts REF STEP DEF PROGRAM
context-free syntax
BASIC-ARROW “:” OBJ DART-ENDER OBJ → REF
DART OBJ
BASIC-ARROW “:” OBJ STEP+
obj {BASIC-OBJ “,”}∗ “;”
lib {REF “,”}∗ “;”

→ STEP
→ DEF

6.9. IMP-COMPILE
def {DEF “;”}∗ “.”
variables
Def [0-9]∗[ 0 ]∗
→ DEF
Def “∗”[0-9]∗[ 0 ]∗ → {DEF “;”}∗
Step “∗”[0-9]∗[ 0 ]∗ → STEP∗
Step “+”[0-9]∗[ 0 ]∗ → STEP+
Ref [0-9]∗[ 0 ]∗
→ REF
Ref “∗”[0-9]∗[ 0 ]∗ → {REF “,”}∗
Program [0-9]∗[ 0 ]∗ → PROGRAM

81
→ PROGRAM

6.9 IMP-compile
The compilation function B− we are going to specify will transform an arrow into a form which can
be used by the execution module (see Section 6.11). We shall construct inductively a CODE which
mimicks the structure of an arrow f , but uses as building blocks simple operations on forests called
instructions. At the same time, we shall infer the type of the polymorphic arrows, if it is possible.
imports IMP-syntax6.8 Support6.4 DomCod6.5
The basic codes are those instructions which can be executed independently of the basic arrows
chosen and of the arrows which have been previously defined. Distinguishing them greatly simplifies
the rules for compilation and execution. In order to reduce ambiguity, we surround with braces all
instructions and constructors (but in the latter case the braces are aliased away for better readability).
exports
sorts BASIC-CODE CODE
Some of the basic codes and of the code constructors contain a great deal of information, and are
used internally by the compiler. A peephole optimization will completely eliminate the redundant
instructionss from the final result, so we do not export their syntax. The names follow closely the
categorical notation, and the parameters will be explained in the equational part.
hiddens
context-free syntax
“INJ1” “[” INT “,” INT “]”
→ BASIC-CODE
“INJ2” “[” INT “,” INT “]”
→ BASIC-CODE
“PROJ1” “[” INT “,” INT “]”
→ BASIC-CODE
“PROJ2” “[” INT “,” INT “]”
→ BASIC-CODE
“DIST” “[” INT “,” INT “,” INT “,” INT “]” → BASIC-CODE
CODE “,” “[” INT “,” INT “]” CODE

→ CODE

For each instruction described here, instead, the execution module (Section 6.11) contain rules for
execution. The only exeption is the INIT instruction, which can never be executed, since its domain
contains no elements. The TREE instruction corresponds to the Gn, −F operator, while RIGHTDEL
and LEFTDEL delete the rightmost or leftmost n trees of a forest.
exports
context-free syntax
BASIC-ARROW
“NOP”
“INIT”
“TERM”

→ BASIC-CODE
→ BASIC-CODE
→ BASIC-CODE
→ BASIC-CODE

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

82

“DIST” “[” INT “,” INT “,” INT “]”
“TREE” “[” INT “]”
“RIGHTDEL” “[” INT “]”
“LEFTDEL” “[” INT “]”

→ BASIC-CODE
→ BASIC-CODE
→ BASIC-CODE
→ BASIC-CODE

“{” BASIC-CODE “}”

→ CODE

“{” “COMP” “,” BASIC-ARROW “}”
→ CODE
“{” “ITER” “,” CODE “,” INT “,” INT “,” INT “}” → CODE
CODE “ | ” “[” INT “,” INT “]” CODE
CODE “,” CODE

→ CODE
→ CODE

CODE “;” CODE
→ CODE
priorities
CODE “;”CODE → CODE > {non-assoc: CODE “,”“[”INT “,”INT “]”CODE → CODE,
CODE “ | ”“[”INT “,”INT “]”CODE → CODE}
The result of the compilation of a program is a list of pairs whose first element is an arrow identifier,
and the second element is the corresponding code.
sorts COMP-ARROW COMP-ARROW-LIST
context-free syntax
“[” BASIC-ARROW “,” CODE “]” → COMP-ARROW
“[” {COMP-ARROW “,”}∗ “]”
→ COMP-ARROW-LIST
Finally, we specify the sorts to which the compilation function can be applied (note that it is possible
to compile structural arrows without knowing the arrow specification list). The result of a compilation
is a pair formed by a boolean term and a code; however, the boolean term will always be true, because
no rules are provided which return false. This is intentional: if no compilation is possible, the term
will not reduce, and will not unify with a pair.
sorts BOOL-CODE
context-free syntax
“[” BOOL “,” CODE “]”

→ BOOL-CODE

“8” “[[” ARROW “:” FOBJ “→” FOBJ “]]” using SPEC-LIST → BOOL-CODE
“8” “[[” STRUCTURAL-ARROW “:” FOBJ “→” FOBJ “]]” → BOOL-CODE
“8” “[[” OBJ STEP+ “]]” using SPEC-LIST
→ BOOL-CODE
“8” “[[” lib {REF “,”}∗ “;” “]]”
→ SPEC-LIST
“8” “[[” def {DEF “;”}∗ “.” “]]” using SPEC-LIST
→ COMP-ARROW-LIST
“8” “[[” PROGRAM “]]”
→ COMP-ARROW-LIST
variables
“γ ”[0-9]∗[ 0 ]∗
→ CODE
Basic-Code [0-9]∗[ 0 ]∗ → BASIC-CODE
Bool-Code [0-9]∗[ 0 ]∗ → BOOL-CODE
Comp “∗”[0-9]∗[ 0 ]∗ → {COMP-ARROW “,”}∗
The equations described here take care of the compilation of an arrow, or of a whole program. All
polymorphic arrows must be instantiated now. Note that, given an arrow, we cannot in general build
its domain and codomain, due to the polymorphism of structural arrows. But we can, using the
backtracking caused by list matching, check if a given arrow has given domain and codomain. This is
a much weaker statement, which we can usually prove. If we cannot, we shall not be able to rewrite
the term we have to compile.

6.9. IMP-COMPILE

83

The usefulness of flat objects becomes immediately apparent in the rules which inductively try to
assign the correct domain and codomain to structural or derived arrows. Since we need to forget the
associativity isomorphisms, all possible ways of breaking in two a sum of a product have to be tried;
backtracking takes care of that. Note that when a list variable matches a single flat object, condition
evaluation will use the normalization equations [Snfs1] and [Snfp1] of Section 6.4 in order to bring
the flat object into normal form.
For what matters structural arrows, we have to declare the forms of domain and codomain which
are acceptable. For instance, the identity must have the same domain and codomain, while a first
projection must start from a product and end on the first part of it.
Moreover, for each completely specified structural arrow we add a rule which instead of assigning
inductively a domain and a codomain just checks whether the actual domain and codomain of the
arrow match with the specified ones.
The general strategy of the compiler is to create redundant information in the code, which however
avoids special cases during compilation. Then, a simple sequence of peephole optimizations handles
special cases and reduces redundancy.
equations
Compiling a basic (or defined) arrow. For basic arrows compilation is very simple, since it is
assumed that somewhere in the system the application of a basic arrow to its possible arguments
has already been specified equationally. If the arrow has been previously defined in the program,
it appears in the specification list with the special symbol , and in this case we use the COMP
instruction in order to remember to search for the arrow in the compiled arrow list at execution time.

spec of a in [Spec∗ ] = [4 → 2]
[Ca1]

8 [[ a : 4 → 2 ]] using [Spec∗ ] = [true, {a}]

spec of a in [Spec∗ ] = [4
[Ca2]

2]

∗

8 [[ a : 4 → 2 ]] using [Spec ] = [true, {COMP, a}]

Compiling a structural arrow. We do not need the specification list in order to compile a structural
arrow, so we discard it; in this way the rules are much less cluttered.
[Cstr]

8 [[ Structural-Arrow : 4 → 2 ]] using [Spec∗ ] = 8 [[ Structural-Arrow : 4 → 2 ]]

We now compile the structural arrows following the mathematical definition of B−. At the same time,
we check for a possible instantiation of polymorphic arrows. Compilation succeeds only if such an
instantiation exists.
Note that there is an instruction corresponding to the initial map ! X : ∅ → X , but it should never
happen that it has to be executed, unless an arrow is applied to badly-typed data. Correspondingly,
Section 6.11 contains no rule for the execution of INIT.
Let us begin with identities: they must start and end on the same object, but in order to avoid
unwanted assignments, the object cannot be initial or terminal in the polymorphic case.
4 6= +(), 4 6= ∗()
[Cid]

8 [[ 1 : 4 → 4 ]] = [true, {NOP}]
flat[X ] = 4

[CID]

8 [[ 1(X ) : 4 → 4 ]] = [true, {NOP}]

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

84

If a first (second) injection is completely specified, we just have to check that the actual domain
and codomain correspond to the specified ones. Otherwise, using the ⊕ operator (see Section 6.4)
we break the given codomain into two summands in such a way that the domain is first (second)
summand. If we succeed, we output an INJn instruction which records the length (as a sum) of each
summand. With projections we keep a dual behaviour.
Note that in the polymorphic case we do not allow empty lists; in other words, we never instantiate
a polymorphic arrow to a trivial arrow, such as proj1 : A × I → A. This is necessary in order to avoid
(inj2 ,inj1 )

unnatural assignments. For instance, X + X −−−−−→ X + X could be instantiated to an identity,
with inj2 : ∅ → X + X + ∅ and inj1 : X + X → X + X + ∅.
⊕(4) = ⊕(4+ ),  = +(4+ 2+ )
[Ci1]

8 [[ inj1 : 4 →  ]] = [true, {INJ1[len[4+ ], len[2+ ]]}]
flat[X ] = 4, flat[Y ] = 2, +(4 2) = 

[CI1]

8 [[ inj1 (X , Y ) : 4 →  ]] = [true, {INJ1[slen[4], slen[2]]}]
⊕(2) = ⊕(2+ ),  = +(4+ 2+ )

[Ci2]

8 [[ inj2 : 2 →  ]] = [true, {INJ2[len[4+ ], len[2+ ]]}]
flat[X ] = 4, flat[Y ] = 2, +(4 2) = 

[CI2]

8 [[ inj2 (X , Y ) : 2 →  ]] = [true, {INJ2[slen[4], slen[2]]}]
⊗(4) = ⊗(4+ ),  = ∗(4+ 2+ )

[Cp1]

8 [[ proj1 :  → 4 ]] = [true, {PROJ1[len[4+ ], len[2+ ]]}]
flat[X ] = 4, flat[Y ] = 2, ∗(4 2) = 

[CP1]

8 [[ proj1 (X , Y ) :  → 4 ]] = [true, {PROJ1[plen[4], plen[2]]}]
⊗(2) = ⊗(2+ ),  = ∗(4+ 2+ )

[Cp2]

8 [[ proj2 :  → 2 ]] = [true, {PROJ2[len[4+ ], len[2+ ]]}]
flat[X ] = 4, flat[Y ] = 2, ∗(4 2) = 

[CP2]

8 [[ proj2 (X , Y ) :  → 2 ]] = [true, {PROJ2[plen[4], plen[2]]}]

Initial and terminal maps have corresponding instructions. TERM just outputs the empty forest; INIT
is never executed, but it is kept for optimization purposes. Again we avoid unwanted instantiations.
[Cini]

4 6= +() ⇒ 8 [[ ! : +() → 4 ]] = [true, {INIT}]
flat[X ] = 4

[CINI]

[Cter]

8 [[ !(X ) : +() → 4 ]] = [true, {INIT}]
4 6= ∗() ⇒ 8 [[ ¡ : 4 → ∗() ]] = [true, {TERM}]

6.9. IMP-COMPILE

85

flat[X ] = 4
[CTER]

8 [[ ¡(X ) : 4 → ∗() ]] = [true, {TERM}]

The four parameters recorded when compiling a distributivity isomorphism are the length as a product
of the first factor of the domain, the length as a sum of the two summands which make the second
factor of the domain, and the length as a sum of the first summand of the codomain.
Note that many distributivity isomorphisms trivialize when one of this numbers is zero. This is the
reason why the rule for the instantiation of a polymorphic map requires nonempty lists everyhwhere.

[Cd]

[CD]

+
+
+
+
∗(4+ +(2+
1 )) = +(1 ), ∗(4 +(22 )) = +(2 )
+
+ +
8 [[ δ −1 : ∗(4+ +(2+
1 22 )) → +(1 2 ) ]] =
+
+
+
[true, {DIST[len[4 ], len[21 ], len[2+
2 ], len[1 ]]}]

flat[X ] = 4, flat[Y 1 ] = 21 , flat[Y 2 ] = 22 ,
∗(4 +(21 22 )) = 1 , +(∗(4 21 ) ∗(4 22 )) = 2
8 [[ δ −1 (X , Y 1 , Y 2 ) : 1 → 2 ]] =
[true, {DIST[plen[4], slen[21 ], slen[22 ], slen[∗(4 21 )]]}]

Compiling a derived arrow. Now we scan inductively an arrow. Note that product and sums of
functions are compiled in terms of the more primitive (−, −) and (− | −) operators, following the
categorical definition, and that there is a double backtracking: both source and destination must be
broken into sublists.

[Cs]

[Cp]

[Cb]

[Cc]

⊕(1 ) = ⊕(4∗1 2∗1 ), ⊕(2 ) = ⊕(4∗2 2∗2 ),
8 [[ f : +(4∗1 ) → +(4∗2 ) ]] using [Spec∗ ] = [true, γ ],
8 [[ g : +(2∗1 ) → +(2∗2 ) ]] using [Spec∗ ] = [true, γ 0 ]
8 [[ f + g : 1 → 2 ]] using [Spec∗ ] =
[true, γ ; {INJ1[len[4∗2 ], len[2∗2 ]]} | [len[4∗1 ], len[2∗1 ]] γ 0 ; {INJ2[len[4∗2 ], len[2∗2 ]]}]
⊗(1 ) = ⊗(4∗1 2∗1 ), ⊗(2 ) = ⊗(4∗2 2∗2 ),
8 [[ f : ∗(4∗1 ) → ∗(4∗2 ) ]] using [Spec∗ ] = [true, γ ],
8 [[ g : ∗(2∗1 ) → ∗(2∗2 ) ]] using [Spec∗ ] = [true, γ 0 ]
8 [[ f ∗ g : 1 → 2 ]] using [Spec∗ ] =
[true, {PROJ1[len[4∗1 ], len[2∗1 ]]} ; γ ,[len[4∗2 ], len[2∗2 ]] {PROJ2[len[4∗1 ], len[2∗1 ]]} ; γ 0 ]

8 [[ f | g

⊕(1 ) = ⊕(4∗1 2∗1 ),
∗
8 [[ f : +(41 ) → 2 ]] using [Spec∗ ] = [true, γ ],
8 [[ g : +(2∗1 ) → 2 ]] using [Spec∗ ] = [true, γ 0 ]
: 1 → 2 ]] using [Spec∗ ] = [true, γ | [len[4∗1 ], len[2∗1 ]]

γ 0]

⊗(2 ) = ⊗(4∗2 2∗2 ),
8 [[ f : 1 → ∗(4∗2 ) ]] using [Spec∗ ] = [true, γ ],
8 [[ g : 1 → ∗(2∗2 ) ]] using [Spec∗ ] = [true, γ 0 ]
8 [[ f , g : 1 → 2 ]] using [Spec∗ ] = [true, γ ,[len[4∗2 ], len[2∗2 ]] γ 0 ]

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

86

g◦ f

Composition is a different beast. Our problem now is that given an arrow X −−→ Z , we do not
know how to make structural induction because we do not have a candidate for an object Y such that
f

g

f

g

X −
→ Y and Y −
→ Z . The fundamental idea here is that as long as X −
→ Y and Y −
→ Z pass
the type-check, Y can be chosen arbitrarily. This means that we can define a domain and codomain
constructors which work with a certain looseness, for instance supposing that their arguments are
well-typed; this is done in Section 6.5: all we need is just a reasonable guess for Y .
The rule for composition is more complicated exactly because we must establish whether we can
compile f ; g using as “middle object” the domain of g or the codomain of f (in general they will not
be both computable).
cod[ f ] using [Spec∗ ] = 2, 2 6= ⊥,
8 [[ f : 4 → 2 ]] using [Spec∗ ] = [true, γ ],
8 [[ g : 2 →  ]] using [Spec∗ ] = [true, γ 0 ]
[Cco1]

8 [[ f ; g : 4 →  ]] using [Spec∗ ] = [true, γ ; γ 0 ]
dom[g] using [Spec∗ ] = 2, 2 6= ⊥,
8 [[ f : 4 → 2 ]] using [Spec∗ ] = [true, γ ],
8 [[ g : 2 →  ]] using [Spec∗ ] = [true, γ 0 ]

[Cco2]

8 [[ f ; g : 4 →  ]] using [Spec∗ ] = [true, γ ; γ 0 ]

Compiling call[ − ]. First of all, we note that the three numerical arguments used by the ITER
instruction are the length (as a sum) of the input, local and output state space. If the application of
call[ − ] is completely specified, we just have to compute them. Otherwise, we try to compute the
domain (codomain) of f and to break it into two summands in such a way that the second (first)
summand is a first (second) summand for the codomain (domain). Of course, there is a possibility of
backtracking here. Note that we impose that the output space is non-empty.
 6= +(), ⊕(4) = ⊕(4+ ), dom[ f ] using [Spec∗ ] = +(4+ 2+ ),
8 [[ f : +(4+ 2+ ) → +(2+ ) ]] using [Spec∗ ] = [true, γ ]
[Ccall1]

8 [[ call[ f ] : 4 →  ]] using [Spec∗ ] = [true, {ITER, γ , len[4+ ], len[2+ ], slen[]}]
⊕() = ⊕(+ ), cod[ f ] using [Spec∗ ] = +(2+ + ),
8 [[ f : +(4 2+ ) → +(2+ + ) ]] using [Spec∗ ] = [true, γ ]

[Ccall2]

8 [[ call[ f ] : 4 →  ]] using [Spec∗ ] = [true, {ITER, γ , slen[4], len[2+ ], len[+ ]}]
flat[X ] = 4, flat[Y ] = 2, flat[Z ] = ,  6= +(),
8 [[ f : +(4 2) → +(2 ) ]] using [Spec∗ ] = [true, γ ]

[CCALL]

8 [[ call[X , Y , Z , f ] : 4 →  ]] using [Spec∗ ] = [true, {ITER, γ , slen[4], slen[2], slen[]}]

Compiling a program. The following rules describe how B− can be applied to a program, or to
part of it. Note that little or no error checking is performed, because we assume that the program has
been already type-checked.
When applied to a DART, B− returns a boolean and a code, while when applied to a list of
definitions, it returns a list of COMP-ARROW.
8 [[ f : flat[X ] → flat[Y ] ]] using [Spec∗ ] = [true, γ ]
[Cst1]

8 [[ X − f → Y ]] using [Spec∗ ] = [true, γ ]

6.9. IMP-COMPILE

87

8 [[ f : flat[X ] → flat[Y ] ]] using [Spec∗ ] = [true, γ ],
8 [[ Y Step+ ]] using [Spec∗ ] = [true, γ 0 ]
[Cst2]

8 [[ X − f → Y Step+ ]] using [Spec∗ ] = [true, γ ; γ 0 ]

[Cdef1]

8 [[ def . ]] using [Spec∗ ] = []
8 [[ X Step∗ − f → Y ]] using [Spec∗ ] = [true, γ ],
8 [[ def Def∗ . ]] using [a : flat[X ]
flat[Y ], Spec∗ ] = [Comp∗ ]

[Cdef2]

8 [[ def a : X Step∗ − f → Y ; Def∗ . ]] using [Spec∗ ] = [[a, γ ], Comp∗ ]

Finally, the compilation of a whole program is obtained by discarding the object declaration, gathering (without any check) the basic arrow declaration into a specification list, and applying B− to each
arrow definition.
[Clib]

8 [[ lib ; ]] = []
8 [[ lib Ref∗ ; ]] = [Spec∗ ]

[Cref]

8 [[ lib a : X → Y , Ref∗ ; ]] = [a : flat[X ] → flat[Y ], Spec∗ ]

[Cprog]

8 [[ obj A∗ ; lib Ref∗ ; def Def∗ . ]] = 8 [[ def Def∗ . ]] using 8 [[ lib Ref∗ ; ]]

Peephole optimization. Here we are going to examine small fragments of code, in order to make
them more efficient. The rules we apply can in turn activate other rules, until no other rule is applicable. This technique, known as peephole optimization in compiler theory (see [McKeeman:1965]), is
particularly useful in our case because it allows to eliminate a series of trivial maps which would be
very cumbersome to manage during compilation on a case-by-case basis. For instance, composition
with NOP (i.e., with the identity) can be eliminated:
{NOP} ; γ = γ
[CONOP2] γ ; {NOP} = γ
[CONOP1]

If one of the summands of the codomain of an injection is the empty set, the injection is really an
identity or an initial map. Dually for projections.

[COINJ2]

p 6= 0 ⇒ {INJ1[ p, 0]} = {NOP}
q 6= 0 ⇒ {INJ2[0, q]} = {NOP}

[COINJ3]

{INJ1[0, q]} = {INIT}

[COINJ4]

{INJ2[ p, 0]} = {INIT}

[COINJ1]

p 6= 0 ⇒ {PROJ1[ p, 0]} = {NOP}
[COPR2] q 6 = 0 ⇒ {PROJ2[0, q]} = {NOP}
[COPR1]

[COPR3]

{PROJ1[0, q]} = {TERM}

[COPR4]

{PROJ2[ p, 0]} = {TERM}

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

88

Iteration starting from the empty set can only produce the initial map, and if the local state space is
empty we can apply the normal form theorem.
[COITER1]

{ITER, γ , 0, n, p} = {INIT}

[COITER2]

m 6= 0 ⇒ {ITER, γ , m, 0, p} = γ

Initial and terminal maps enjoy the following properties:
{INIT} ; γ = {INIT}
[CODELALL] γ ; {TERM} = {TERM}

[COINIT]

Now we have a series of rules which eliminate trivial cases of the (−, −) and (− | −) operators in
which the arrow really acting is just one.
γ ,[0, q] γ 0 = γ 0
0
[COc2] γ ,[ p, 0] γ = γ

[COc1]

γ | [0, q] γ 0 = γ 0
0
[COb2] γ | [ p, 0] γ = γ
[COb1]

The most trivialized map is the distributivity isomorphism. If one of its parameters is zero, it reduces
δ −1

to an identity or to an injection. For instance, the first rule correspond to the case I × (X + Y ) −−→
I × X + I × Y , where the flat normal form for both the domain and the codomain is +(X Y ), and
δ −1

δ −1 is the identity, while the second rule correspond to the case X × (∅ + Y ) −−→ X × ∅ + X × Y
(with X 6= I ), where the normal form of the domain is ×(X Y ), the normal form of the codomain is
+(×(X + ()) × (X Y )) and δ −1 is the second injection.
[CODIST1]

{DIST[0, q, q 0 , n]} = {NOP}

[CODIST2]

p 6= 0 ⇒ {DIST[ p, 0, q 0 , n]} = {TREE[1]}

[CODIST3]

p 6= 0 ⇒ {DIST[ p, q, 0, n]} = {TREE[0]}

We complete our optimization with the following default rules, which will be applied only when
no other equation is applicable. First of all, we note that an injection just forms a tree, modulo the
rewrite rule G j, Gk, uFF = G j + k, uF (this is true because we can assume p and q not equal to zero).
Analogously, projections can be implemented as cancellation of part of a forest.
[COINJ1]

{INJ1[n, p]}

= {TREE[0]}

[COINJ2]
[COPR1]

{INJ2[n, p]} = {TREE[n]}
otherwise
{PROJ1[ p, q]} = {RIGHTDEL[q]} otherwise

[COPR2]

{PROJ2[ p, q]} = {LEFTDEL[ p]}

otherwise

otherwise

Once we assume that all parameters are nonnull, we can reduce the information carried by the distributivity isomorphism. Note that if n is zero the isomorphism will never be applied, for both its
domain and its codomain would be empty.
[CODIST]

{DIST[ p, q, q 0 , n]} = {DIST[q, q 0 , n]} otherwise

Finally, we discard the arguments of the (−, −) operator.
[COc]

γ ,[ p 0 , q 0 ] γ 0 = γ , γ 0

otherwise

6.10. IMP-TYPECHECK

89

6.10 IMP-typecheck
The type-check function we are going to specify can be applied to several entities, giving different
results (which, however, always contain an error list; the only case in which a boolean term is returned
is when checking if certain data correspond to the representation of an element of a certain flat object).
We export only the case in which type-checking is applied to a whole program, or to some data.
imports IMP-syntax6.8 IMP-compile6.9 Data6.6 Support6.4 DomCod6.5 Errors6.7
exports
context-free syntax
tc “[[” PROGRAM “]]”
→ ERROR-LIST
tc “[[” DATA “,” FOBJ “]]” → BOOL
hiddens
sorts ERROR-LIST-BASIC-OBJ-LIST ERROR-LIST-SPEC-LIST
context-free syntax
ERROR-LIST BASIC-OBJ-LIST → ERROR-LIST-BASIC-OBJ-LIST
ERROR-LIST SPEC-LIST
→ ERROR-LIST-SPEC-LIST
When we type-check the basic object list (see Section 6.13 for the description of the structure of a
program) we return a list of declared objects, and a list of errors (duplicate identifiers).
context-free syntax
tc “[[” obj {BASIC-OBJ “,”}∗ “;” “]]” → ERROR-LIST-BASIC-OBJ-LIST
The following syntax is useful when one or more objects have to be checked; the relative errors are
accumulated in the resulting error list.
context-free syntax
tc “[[” {OBJ “,”}∗ “]]” using BASIC-OBJ-LIST → ERROR-LIST
A list of basic arrows is checked on the basis of a list of basic objects (which we need in order to
check for validity of the domains and codomains). The result is a list of arrow specifications, and a
list of errors.
context-free syntax
tc “[[” lib {REF “,”}∗ “;” “]]”
using BASIC-OBJ-LIST
→ ERROR-LIST-SPEC-LIST
Finally, knowing completely the base graph, we check for arrow steps and definitions. We also need
a function to extract the boolean part of the result of a compilation.
context-free syntax
tc “[[” BOOL-CODE “]]”

→ BOOL

tc “[[” OBJ STEP∗ “]]”
using BASIC-OBJ-LIST SPEC-LIST → ERROR-LIST
tc “[[” def {DEF “;”}∗ “.” “]]”
using BASIC-OBJ-LIST SPEC-LIST → ERROR-LIST
The following equations perform the type-check of an IMP(G) program and of IMP(G) data. The
program is scanned, and a error list is build incrementally. The functions and the predicates of Section
6.4 are at the basis of the conditions.
equations

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

90

Checking data. The type-check of data is rather simple. Essentially, we check whether the structure of the data corresponds to the structure of a flat object. Products must corresponds to concatenations of forests, and sums to creation of a tree whose root label is smaller than the number of
summands. Note that the rule for simple objects does not really guarantee that the basic data e has
the same type of A.
[Td1]

tc [[ G n, d F , +(4+ ) ]] = n < len[4+ ] ∧ tc [[ d, elem n from 4+ ]]

tc [[ u u ∗ , ∗(4 4∗ ) ]]
[Td3] tc [[ , ∗() ]]

= tc [[ u, 4 ]] ∧ tc [[ u ∗ , ∗(4∗ ) ]]
= true

[Td2]

[Td4]

tc [[ e, A ]]

= true

[Td5]

tc [[ d, 4 ]] = false

otherwise

Checking the basic object list. First of all, we scan the list of basic objects; if we meet a duplicate
definition, a suitable error is appended to the error list.
[Tbo1]

tc [[ obj ; ]] = [] []
tc [[ obj A∗ ; ]] = [Error∗ ] [B ∗ ], A is in [B ∗ ] = false

[Tbo2]

tc [[ obj A∗ , A; ]] = [Error∗ ] [A, B ∗ ]
tc [[ obj A∗ ; ]] = [Error∗ ] [B ∗ ], A is in [B ∗ ] = true

[Tbo2]

tc [[ obj A∗ , A; ]] = [Error∗ , object name A already used] [B ∗ ]

Here we obtain from a list of objects a list of errors. This will be useful in the next equations.
[Tobl1]

tc [[ ]] using [A∗ ] = []
X is built from [A∗ ] = true

[Tobl2]

tc [[ X ,

X∗

]] using [A∗ ] = tc [[ X ∗ ]] using [A∗ ]
X is built from [A∗ ] = false

[Tobl3]

tc [[ X , X ∗ ]] using [A∗ ] =
[object X contains undeclared basic objects] · tc [[ X ∗ ]] using [A∗ ]

Checking the basic arrow list. Now each basic arrow declaration is checked in two ways: its
domain and codomain must have been built using known simple objects, and the arrow name must
not have been already used.
[Tba1]

tc [[ lib ; ]] using [A ∗ ] = [] []
tc [[ lib Ref∗ ; ]] using [A∗ ] = [Error∗1 ] [Spec∗ ],
tc [[ X , Y ]] using [A∗ ] = [Error∗2 ],
spec of a in [Spec∗ ] = ⊥

[Tba2]

tc [[ lib Ref∗ , a : X → Y ; ]] using [A∗ ] =
[Error∗1 , Error∗2 ] [a : flat[X ] → flat[Y ], Spec∗ ]

6.10. IMP-TYPECHECK

91

tc [[ lib Ref∗ ; ]] using [A∗ ] = [Error∗1 ] [Spec∗ ],
tc [[ X , Y ]] using [A∗ ] = [Error∗2 ],
spec of a in [Spec∗ ] 6= ⊥
[Tba3]

tc [[ lib Ref∗ , a : X → Y ; ]] using [A∗ ] =
[Error∗1 , Error∗2 , arrow name a already used] [Spec∗ ]

Checking arrow steps and definitions. An arrow step is correctly typed when the arrow it encloses
starts and ends on the specified domain and codomain. A precondition for this to happen is that the
enclosed arrow must have been built using known simple arrows. The compiling function B− is called
in order to discover whether an arrow has given domain and codomain.
[Tnf1]

tc [[ [true, γ ] ]]

[Tnf2]

tc [[ Bool-Code ]] = false

[Tst1]

tc [[ X ]] using [A∗ ] [Spec∗ ] = tc [[ X ]] using [A∗ ]

= true
otherwise

f is built from [Spec∗ ] = false
[Tst2]

tc [[ X − f → Y Step∗ ]] using [A∗ ] [Spec∗ ] =
tc [[ X ]] using [A∗ ] · [arrow f contains undeclared basic arrows]
· tc [[ Y Step∗ ]] using [A∗ ] [Spec∗ ]
f is built from [Spec∗ ] = true,
tc [[ 8 [[ f : flat[X ] → flat[Y ] ]] using [Spec∗ ] ]] = true

[Tst3]

tc [[ X − f → Y Step∗ ]] using [A∗ ] [Spec∗ ] =
tc [[ X ]] using [A∗ ] · tc [[ Y Step∗ ]] using [A∗ ] [Spec∗ ]
f is built from [Spec∗ ] = true,
tc [[ 8 [[ f : flat[X ] → flat[Y ] ]] using [Spec∗ ] ]] = false

[Tst4]

tc [[ X − f → Y Step∗ ]] using [A∗ ] [Spec∗ ] =
tc [[ X ]] using [A∗ ] · [arrow f is not from X to Y ]
· tc [[ Y Step∗ ]] using [A∗ ] [Spec∗ ]

Then, we scan the list of arrow definitions. For an arrow definition to pass the type-check, its name
must be new, and its arrow steps must be correct. If the name is new, the specification of the arrow is
appended to the specification list (because other definitions could use it).
[Tdef1]

tc [[ def . ]] using [A ∗ ] [Spec∗ ] = []

spec of a in [Spec∗ ] = ⊥
[Tdef2]

tc [[ def a : X Step∗ − f → Y ; Def∗ . ]] using [A∗ ] [Spec∗ ] =
tc [[ X Step∗ − f → Y ]] using [A∗ ] [Spec∗ ]
· tc [[ def Def∗ . ]] using [A∗ ] [a : flat[X ] → flat[Y ], Spec∗ ]

spec of a in [Spec∗ ] 6= ⊥
[Tdef3]

∗

tc [[ def a : X Step − f → Y ; Def∗ . ]] using [A∗ ] [Spec∗ ] =
[arrow name a already used]
· tc [[ X Step∗ − f → Y ]] using [A∗ ] [Spec∗ ] · tc [[ def Def∗ . ]] using [A∗ ] [Spec∗ ]

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

92
Checking the whole program.
of the three sections.

[Tprog]

Finally, we type-check a whole program by accumulating the errors

tc [[ obj A∗ ; ]] = [Error∗1 ] [B ∗ ],
tc [[ lib Ref∗ ; ]] using [B ∗ ] = [Error∗2 ] [Spec∗ ],
tc [[ def Def∗ . ]] using [B ∗ ] [Spec∗ ] = [Error∗3 ]
tc [[ obj A∗ ; lib Ref∗ ; def Def∗ . ]] = [Error∗1 , Error∗2 , Error∗3 ]

6.11 IMP-exec
This module specifies the mechanism for executing a program. The syntax declaration is very simple:
it consists of a utility function which extracts the compiled code of an arrow from a list of compiled
arrows, and of some ways of applying code to data.
imports IMP-compile6.9 Data6.6
exports
context-free syntax
code of BASIC-ARROW in COMP-ARROW-LIST → CODE
“{” BASIC-CODE “}” “[” DATA “]”

→ DATA

CODE “[” DATA “]” using COMP-ARROW-LIST → DATA
Again for reasons of efficiency and clarity, in the equational description of the code execution we
suppose that the data are correctly typed.
equations
Executing basic codes.
compiled arrow list.

This first two equations explain how to extract the code of an arrow from a

[Ecode1]

code of a in [[a, γ ], Comp∗ ] = γ

[Ecode2]

a 6= b ⇒ code of a in [[b, γ ], Comp∗ ] = code of a in [Comp∗ ]

Now we discuss the basic instructions. First of all we discard the compiled arrow list.
[Ebasic]

{Basic-Code}[d] using [Comp∗ ] = {Basic-Code}[d]

The equations described here are rather obvious. Recall that the empty term (i.e., the empty forest)
represents the only element of I .
[ENOP]

{NOP}[d]

= d

[EINJ]
[ETERM]

{TREE[n]}[d] = G n, d F
{TERM}[d]
=

[ERDL1]

{RIGHTDEL[0]}[u ∗ ] = u ∗

[ELDL1]

{LEFTDEL[0]}[u ∗ ]

= u∗

6.11. IMP-EXEC

93

[ERDL2]

n 6= 0 ⇒ {RIGHTDEL[n]}[u ∗ u] = {RIGHTDEL[n − 1]}[u ∗ ]

[ELDL2]

n 6= 0 ⇒ {LEFTDEL[n]}[u u ∗ ]

= {LEFTDEL[n − 1]}[u ∗ ]

On the contrary, it is not obvious at all that the following four definitions implement correctly the
distributivity isomorphism. We just remark that the form given here is allowed by the peephole
optimization of Section 6.9, which got rid of a series of embarassing special cases, and that the four
rules implement exactly the mathematical definition given in Section 5.2.1.
The values listed here for q, q 0 and n are all the possible ones, given that n < p + q and that the
cases for which p or q are equal to zero have been eliminated by the optimization phase.
q 6= 1, m < q = true
[EDIST1]

{DIST[q,

q 0,

n]}[u + G m, u ∗ F] = G 0, u + G m, u ∗ F F
q 0 6= 1, m ≥ q = true

[EDIST2]

{DIST[q, q 0 , n]}[u + G m, u ∗ F] = G n, u + G m − q, u ∗ F F

{DIST[1, q 0 , n]}[u + G 0, u ∗ F] = G 0, u + u ∗ F
+
∗
+ ∗
[EDIST4] {DIST[q, 1, n]}[u G q, u F] = G n, u u F
[EDIST3]

The execution of a compiled arrow consists in obtaining its code from the compiled arrow list and
applying the code to the given data.
[ECOMP]

{COMP, a}[d] using [Comp∗ ] = code of a in [Comp∗ ][d] using [Comp∗ ]

Structural induction on the code is a bit tricky, mainly because of the representation problems relative
to sums. Again, the cases listed here for p, q and n are all the possible ones.
p 6= 1, n < p = true
[Eb1]

γ | [ p, q]

γ 0 [G

γ | [ p, q]

γ 0 [G

n, d F] using [Comp∗ ] = γ [G n, d F] using [Comp∗ ]
q 6= 1, n ≥ p = true

[Eb2]

n, d F] using [Comp∗ ] = γ 0 [G n − p, d F] using [Comp∗ ]

γ | [1, q] γ 0 [G 0, d F] using [Comp∗ ] = γ [d] using [Comp∗ ]
∗
∗
0
0
[Eb4] γ | [ p, 1] γ [G p, d F] using [Comp ] = γ [d] using [Comp ]
[Eb3]

Composition and products are much easier to manage:
γ , γ 0 [d] using [Comp∗ ] = γ [d] using [Comp∗ ] · γ 0 [d] using [Comp∗ ]
∗
∗
∗
0
0
[Eco] γ ; γ [d] using [Comp ] = γ [γ [d] using [Comp ]] using [Comp ]
[Ec]

It is however when executing iteration that the new coding for the data of a distributive program is
useful. Due to the representation of a sum, the check for termination is just a check for the integer
index of the data being greater than the length as a sum of the local state space. Note that m, n and
p are all nonzero, and that we must handle as a special case p = 1, for then the representation of the
result must be modified.
γ [G 0, d F] using [Comp∗ ] = G q, d 0 F, q < n = true
[EITER1]

{ITER, γ , m, n, p}[d] using [Comp∗ ] =
{ITER, γ , m, n, p}[G q + m, d 0 F] using [Comp∗ ]

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

94

p 6= 1, γ [G 0, d F] using [Comp∗ ] = G q, d 0 F, q ≥ n = true
[EITER2]

{ITER, γ , m, n, p}[d] using [Comp∗ ] = G q − n, d 0 F
γ [G 0, d F] using [Comp∗ ] = G n, d 0 F

[EITER3]

{ITER, γ , m, n, 1}[d] using [Comp∗ ] = d 0

6.12 IMP-Nat
This module describes the usage of natural numbers in IMP(G), and it can be used as a basis in
order to include new data types into the language. The syntax part has just to declare as a subsort of
BASIC-DATA all the desired data types (in this case, just INT).
imports IMP-exec6.11 Ints
exports
context-free syntax
INT → BASIC-DATA
The equations, on the other hand, must specify the effect of each basic arrow, following the syntax
described in Section 6.11. Here we define the predecessor and successor functions, which must be
declared as s : I + N → N and p : N → I + N .
equations
{s}[G 1, n F] = n + 1
[IMP-Nat2] {s}[G 0, F]
= 0
[IMP-Nat1]

[IMP-Nat3]

{p}[0] = G 0, F

[IMP-Nat4]

n 6= 0 ⇒ {p}[n] = G 1, n − 1 F

The following equations implement sum, truncated difference and multiplications functions from
N × N to N and “greater”, “greater or equal” and “equal” predicates from N × N to I + I (the
first copy of I representing false). Note that the integer module imported here uses “-” for truncated
subtraction; this could not be true for other modules providing an integer data type, and the equations
should be modified accordingly.
[IMP-Nat5]

{plus}[ p q]

= p+q

{minus}[ p q] = p − q
[IMP-Nat7] {times}[ p q] = p ∗ q

[IMP-Nat6]

[IMP-Nat8]
[IMP-Nat9]

p > q = false ⇒ {gt}[ p q] = G 0, F
p > q = true ⇒ {gt}[ p q] = G 1, F

[IMP-Nat10]

p ≥ q = false ⇒ {ge}[ p q] = G 0, F

[IMP-Nat11]

p ≥ q = true ⇒ {ge}[ p q] = G 1, F

[IMP-Nat12]

p 6= q ⇒ {eq}[ p q] = G 0, F

[IMP-Nat13]

p = q ⇒ {eq}[ p q] = G 1, F

6.13. IMP

95

6.13 IMP
This module is the parent of all modules. It imports all which is necessary in order to type-check,
compile and execute IMP(G) programs, and an arbitrary number of data type modules. Moreover, it
describes some useful syntax for executing arrows.
imports IMP-typecheck6.10 IMP-compile6.9 IMP-exec6.11 IMP-Nat6.12
The standard way of executing a program is to give the name of one of the arrows which have been
defined, followed by the data it has to be applied to enclosed in square brackets. The output can be
either an error list produced by the type-checker, or the resulting data.
exports
sorts ERROR-LIST-OR-DATA
context-free syntax
ERROR-LIST
DATA

→ ERROR-LIST-OR-DATA
→ ERROR-LIST-OR-DATA

BASIC-ARROW “[” DATA “]” using PROGRAM → ERROR-LIST-OR-DATA
equations
Executing (part of) a program. When applying an arrow to some data, reasons of efficiency impose that the compiler tries to compile directly the arrow. If the compilation fails, the type-checker
is invoked and an error list is returned. It should be noted, however, that in some cases (for instance,
duplicate references or object declarations) the compiler could blindly compile a program with minor
syntactical errors. However, if the resulting compiled arrow list is executable the code will perform
correctly.
8 [[ Program ]] = [Comp∗ ]
[Ef1]

a[d] using Program = {COMP, a}[d] using [Comp∗ ]

[Ef2]

a[d] using Program = tc [[ Program ]]

otherwise

96

CHAPTER 6. A LITERATE IMP(G) IMPLEMENTATION

Bibliography
[Bloom & Esik:1993] Steve L. Bloom and Z. Esik. Iteration Theories. The Equational Logic of
Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer–Verlag,
1993.
[Blum, Shub & Smale:1989] Lenore Blum, Mike Shub, and Steve Smale. On a theory of computation and complexity over the real numbers: NP-completeness, recursive functions and universal
machines. Bull. Amer. Math. Soc. (N.S.), 21:1–46, 1989.
[Borceux:1994] Francis Borceux. Handbook of Categorical Algebra 1, volume 50 of Encyclopedia
of Mathematics and Its Applications. Cambridge University Press, 1994.
[Carboni, Lack & Walters:1993] Aurelio Carboni, Stephen Lack, and Robert F.C. Walters. Introduction to extensive and distributive categories. J. Pure Appl. Algebra, 84:145–158, 1993.
[Elgot:1975] Calvin C. Elgot. Monadic computation and iterative algebraic theories. Studies in Logic
and the Foundations of Mathematics, 80:175–230, 1975.
[Heller:1990] Alex Heller. An existence theorem for recursion categories. J. Symbolic Logic,
55(3):1252–1268, 1990.
[Kasangian & Vigna:1991a] Stefano Kasangian and Sebastiano Vigna. Introducing a calculus of
trees. In Proceedings of the International Joint Conference on Theory and Practice of Software
Development (TAPSOFT/CAAP ’91), number 493 in Lecture Notes in Computer Science, pages
215–240. Springer–Verlag, 1991.
[Kasangian & Vigna:1991b] Stefano Kasangian and Sebastiano Vigna. Trees in a distributive category. In Proceedings of the Category Theory ’90 Conference in Como, number 1488 in Lecture
Notes in Mathematics, pages 237–248. Springer–Verlag, 1991.
[Khalil] Wafaa Khalil. IMP and Functional Processors. PhD thesis, School of Mathematics and
Statistics, The University of Sydney.
[Khalil & Walters:1993] Wafaa Khalil and Robert F.C. Walters. An imperative language based on
distributive categories II. RAIRO Inform. Théor., 27(6):503–522, 1993.
[Khalil:1992a] Wafaa Khalil. Composing functional processors. Mathematics Report 92-46, Sydney
University, 1992.
[Khalil:1992b] Wafaa Khalil. Functional processors. Mathematics Report 92-44, Sydney University,
1992.
[Kleene:1936] Stephen C. Kleene. General recursive functions of natural numbers. Math. Ann.,
112:727–742, 1936.
97

98

BIBLIOGRAPHY

[Klint:1993] Paul Klint. A meta-environment for generating programming environments. ACM
Transactions on Software Engineering and Methodology, 2(2):176–201, 1993.
[Knuth:1966] Donald E. Knuth. Algorithm and program; information and data. Comm. ACM,
9(9):653–654, 1966. Letter to the Editor.
[Knuth:1973] Donald E. Knuth. The Art of Computer Programming. Addison–Wesley, 1973.
[Knuth:1984] Donald E. Knuth. Literate programming. The Computer Journal, 27(2):97–111, 1984.
Reprinted as Chapter 4 of [Knuth:1992].
[Knuth:1992] Donald E. Knuth. Literate Programming. Number 27 in CSLI Lecture Notes. Center
for the Study of Language and Information, 1992.
[Lack:1995] Stephen Lack. The Algebra of Distributive and Extensive Categories. PhD thesis,
University of Cambridge, 1995.
[Lawvere] F. William Lawvere. Personal electronic communication.
[Mac Lane:1971] Saunders Mac Lane. Categories for the Working Mathematician. Springer–Verlag,
1971.
[Manin:1977] Yu.I. Manin. A Course in Mathematical Logic. Springer–Verlag, New York, 1977.
[McKeeman:1965] W.M. McKeeman. Peephole optimization. Comm. ACM, 8(7):443–444, 1965.
[Michaux:1989] Christian Michaux. Une remarque à propos des machines sur R introduites par
Blum, Shub et Smale. C. R. Acad. Sci. Paris, 309:435–437, 1989.
[Pair & Quère:1968] C. Pair and A. Quère. Définition et étude des bilangages réguliers. Information
and Control, 13:565–593, 1968.
[Sabadini & Walters:1993] Nicoletta Sabadini and Robert F.C. Walters. On functions and processors: an automata theoretic approach to concurrency through distributive categories. Mathematics
Report 93-7, Sydney University, 1993.
[Sabadini, Vigna & Walters:1993a] Nicoletta Sabadini, Sebastiano Vigna, and Robert F.C. Walters.
An automata theoretic approach to concurrency through distributive categories: On morphisms.
Mathematics Report 93-8, Sydney University, 1993.
[Sabadini, Vigna & Walters:1993b] Nicoletta Sabadini, Sebastiano Vigna, and Robert F.C. Walters.
A notion of refinement for automata. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Algebraic Methodology and Software Technology (AMAST’93), Proceedings of the Third International
Conference on Algebraic Methodology and Software Technology, Workshops in Computing, pages
327–334, University of Twente, The Netherlands, 1993. Springer–Verlag.
[Sabadini, Vigna & Walters:1996] Nicoletta Sabadini, Sebastiano Vigna, and Robert F.C. Walters. A
note on recursive functions. Math. Struct. Comp. Sci., 6:127–139, 1996.
[Vigna:1991] Sebastiano Vigna. Una teoria categoriale degli alberi. Tesi di Laurea. Università degli
Studi di Milano, Facoltà di Scienze Matematiche, Fisiche e Naturali, Dipartimento di Matematica,
1991.
[Vigna:1995] Sebastiano Vigna. Specifying IMP(G) using ASF+SDF: A case study. In Proc. of the
ASF+SDF95 workshop on generating tools from algebraic specifications, pages 65–87. Technical
Report P9504 of the University of Amsterdam, 1995.

BIBLIOGRAPHY

99

[Vigna:1996] Sebastiano Vigna. On the relations between distributive computability and the BSS
model. Theoret. Comput. Sci., 162:5–21, 1996.
[Visser & Klint:1994] Eelco Visser and Paul Klint. ToLATEX: The program. Programming Research
Group, University of Amsterdam, 1994.
[Wagner, Khalil & Walters:1995] Eric G. Wagner, Wafaa Khalil, and Robert F.C. Walters. Fix-point
semantics for programs in distributive categories. Fundamenta Informaticae, 22:187–202, 1995.
[Walters:1989a] Robert F.C. Walters. Data types in a distributive category. Bull. Austral. Math. Soc.,
40:79–82, 1989.
[Walters:1989b] Robert F.C. Walters. The free category with products on a multigraph. Journal of
Pure and Applied Algebra, 62:205–210, 1989.
[Walters:1992a] Robert F.C. Walters. Categories and Computer Science. Cambridge University
Press, 1992.
[Walters:1992b] Robert F.C. Walters. An imperative language based on distributive categories. Math.
Struct. Comp. Sci., 2:249–256, 1992.

