On the Expressiveness of
Single-Pass Instruction Sequences⋆

arXiv:0810.1106v3 [cs.PL] 13 Jan 2009

J.A. Bergstra and C.A. Middelburg
Programming Research Group, University of Amsterdam,
Kruislaan 403, 1098 SJ Amsterdam, the Netherlands
J.A.Bergstra@uva.nl,C.A.Middelburg@uva.nl

Abstract. We perceive programs as single-pass instruction sequences. A
single-pass instruction sequence under execution is considered to produce
a behaviour to be controlled by some execution environment. Threads
as considered in basic thread algebra model such behaviours. We show
that all regular threads, i.e. threads that can only be in a finite number
of states, can be produced by single-pass instruction sequences without
jump instructions if use can be made of Boolean registers. We also show
that, in the case where goto instructions are used instead of jump instructions, a bound to the number of labels restricts the expressiveness.
Keywords: single-pass instruction sequence, regular thread, expressiveness, jump-free instruction sequence.
1998 ACM Computing Classification: D.1.4, D.3.3, F.1.1, F.3.3.

1

Introduction

With the work presented in this paper, we carry on the line of research with
which a start was made in [2]. The working hypothesis of this line of research
is that single-pass instruction sequence is a central notion of computer science
which merits investigation for its own sake. In this line of research, program
algebra is taken for the basis of the investigations. Program algebra is a setting
suited for investigating single-pass instruction sequences. It does not provide a
notation for programs that is intended for actual programming.
The starting-point of program algebra is the perception of a program as a
single-pass instruction sequence, i.e. a finite or infinite sequence of instructions of
which each instruction is executed at most once and can be dropped after it has
been executed or jumped over. This perception is simple, appealing, and links up
with practice. A single-pass instruction sequence under execution is considered
to produce a behaviour to be controlled by some execution environment. Threads
as considered in basic thread algebra model such behaviours: upon each action
performed by a thread, a reply from the execution environment determines how
⋆

This research was partly carried out in the framework of the Jacquard-project Symbiosis, which is funded by the Netherlands Organisation for Scientific Research
(NWO).

the thread proceeds. A thread may make use of services, i.e. components of the
execution environment.
Each Turing machine can be simulated by means of a thread that makes use
of a service. The thread and service correspond to the finite control and tape of
the Turing machine. The threads that correspond to the finite controls of Turing
machines are examples of regular threads, i.e. threads that can only be in a
finite number of states. The behaviours of all single-pass instruction sequences
considered in program algebra are regular threads and each regular thread is
produced by some single-pass instruction sequence. In this paper, we show that
each regular thread can be produced by some single-pass instruction sequence
without jump instructions if use can be made of services that make up Boolean
registers.
The primitive instructions of program algebra include jump instructions. An
interesting variant of program algebra is obtained by leaving out jump instructions and adding labels and goto instructions. It is easy to see that each regular
thread can also be produced by some single-pass instruction sequence with labels
and goto instructions. In this paper, we show that a bound to the number of
labels restricts the expressiveness of this variant.
This paper is organized as follows. First, we review basic thread algebra
and program algebra (Sections 2 and 3). Next, we present a mechanism for
interaction of threads with services and give a description of Boolean register
services (Sections 4 and 5). After that, we show that each regular thread can be
produced by some single-pass instruction sequence without jump instructions if
use can be made of Boolean register services (Section 6). Then, we introduce the
variant of program algebra obtained by leaving out jump instructions and adding
labels and goto instructions (Section 7). Following this, we show that a bound
to the number of labels restricts the expressiveness of this variant (Section 8).
Finally, we make some concluding remarks (Section 9).

2

Basic Thread Algebra

In this section, we review BTA, which is concerned with the behaviours that
sequential programs exhibit on execution. These behaviours are called threads.
In BTA, it is assumed that a fixed but arbitrary set A of basic actions has
been given. A thread performs actions in a sequential fashion. Upon each action
performed, a reply from the execution environment of the thread determines how
it proceeds. To simplify matters, there are only two possible replies: T and F.
BTA has one sort: the sort T of threads. To build terms of sort T, it has the
following constants and operators:
– the deadlock constant D : T;
– the termination constant S : T;
– for each a ∈ A, the binary postconditional composition operator
T × T → T.

2

EaD :

Table 1. Axioms for guarded recursion
hX|Ei = htX |Ei

if X = tX ∈ E RDP

E ⇒ X = hX|Ei if X ∈ V(E)

RSP

Table 2. Approximation induction principle
V

n≥0

πn (x) = πn (y) ⇒ x = y

π0 (x) = D

AIP
P0

πn+1 (S) = S

P1

πn+1 (D) = D

P2

πn+1 (x E a D y) = πn (x) E a D πn (y) P3

We assume that there are infinitely many variables of sort T, including x, y, z.
We introduce action prefixing as an abbreviation: a ◦ p abbreviates p E a D p.
The thread denoted by a closed term of the form p E a D q will first perform
a, and then proceed as the thread denoted by p if the reply from the execution
environment is T and proceed as the thread denoted by q if the reply from
the execution environment is F. The threads denoted by D and S will become
inactive and terminate, respectively. This implies that each closed BTA term
denotes a thread that will become inactive or terminate after it has performed
finitely many actions. Infinite threads can be described by guarded recursion.
A guarded recursive specification over BTA is a set of recursion equations
E = {X = tX | X ∈ V }, where V is a set of variables of sort T and each tX is a
BTA term of the form D, S or t E a D t′ with t and t′ that contain only variables
from V . We write V(E) for the set of all variables that occur in E. We are
only interested in models of BTA in which guarded recursive specifications have
unique solutions, such as the projective limit model of BTA presented in [1].
For each guarded recursive specification E and each X ∈ V(E), we introduce
a constant hX|Ei of sort T standing for the unique solution of E for X. The
axioms for these constants are given in Table 1. In this table, we write htX |Ei
for tX with, for all Y ∈ V(E), all occurrences of Y in tX replaced by hY |Ei.
X, tX and E stand for an arbitrary variable of sort T, an arbitrary BTA term of
sort T and an arbitrary guarded recursive specification over BTA, respectively.
Side conditions are added to restrict what X, tX and E stand for.
Closed terms that denote the same infinite thread cannot always be proved
equal by means of the axioms given in Table 1. We introduce AIP (Approximation Induction Principle) to remedy this. AIP is based on the view that two
threads are identical if their approximations up to any finite depth are identical.
The approximation up to depth n of a thread is obtained by cutting it off after
it has performed n actions. In AIP, the approximation up to depth n is phrased
in terms of the unary projection operator πn : T → T. AIP and the axioms for
the projection operators are given in Table 2.

3

Table 3. Axioms of PGA
(X ; Y ) ; Z = X ; (Y ; Z) PGA1
(X n )ω = X ω

PGA2

Xω ; Y = Xω

PGA3

(X ; Y )ω = X ; (Y ; X)ω PGA4

3

Program Algebra

In this section, we review PGA. The perception of a program as a single-pass
instruction sequence is the starting-point of PGA.
In PGA, it is assumed that a fixed but arbitrary set A of basic instructions
has been given. PGA has the following primitive instructions:
–
–
–
–
–

for each a ∈ A, a plain basic instruction a;
for each a ∈ A, a positive test instruction +a;
for each a ∈ A, a negative test instruction −a;
for each l ∈ N, a forward jump instruction #l;
a termination instruction !.

We write I for the set of all primitive instructions.
The intuition is that the execution of a basic instruction a produces either T
or F at its completion. In the case of a positive test instruction +a, a is executed
and execution proceeds with the next primitive instruction if T is produced.
Otherwise, the next primitive instruction is skipped and execution proceeds with
the primitive instruction following the skipped one. If there is no next instruction
to be executed, deadlock occurs. In the case of a negative test instruction −a,
the role of the value produced is reversed. In the case of a plain basic instruction
a, execution always proceeds as if T is produced. The effect of a forward jump
instruction #l is that execution proceeds with the l-th next instruction. If l
equals 0 or the l-th next instruction does not exist, deadlock occurs. The effect
of the termination instruction ! is that execution terminates.
PGA has the following constants and operators:
– for each u ∈ I, an instruction constant u ;
– the binary concatenation operator ; ;
– the unary repetition operator ω .
We assume that there are infinite many variables, including X, Y, Z.
A closed PGA term is considered to denote a non-empty, finite or periodic
infinite sequence of primitive instructions.1 Closed PGA terms are considered
equal if they denote the same instruction sequence. The axioms for instruction
sequence equivalence are given in Table 3. In this table, n stands for an arbitrary
natural number greater than 0. For each PGA term P , the term P n is defined by
1

A periodic infinite sequence is an infinite sequence with only finitely many subsequences.

4

Table 4. Defining equations for thread extraction operation
|a| = a ◦ D

|#l| = D

|a ; X| = a ◦ |X|

|#0 ; X| = D

|+a| = a ◦ D

|#1 ; X| = |X|

|+a ; X| = |X| E a D |#2 ; X|

|#l + 2 ; u| = D

|−a| = a ◦ D

|#l + 2 ; u ; X| = |#l + 1 ; X|

|−a ; X| = |#2 ; X| E a D |X|

|!| = S
|! ; X| = S

induction on n as follows: P 1 = P and P n+1 = P ;P n . The equation X ω = X ;X ω
is derivable. Each closed PGA term is derivably equal to one of the form P or
P ; Qω , where P and Q are closed PGA terms in which the repetition operator
does not occur.
The behaviours of the instruction sequences denoted by closed PGA terms
are considered threads, with basic instructions taken for basic actions. The thread
extraction operation | | determines, for each closed PGA term P , a closed term
of BTA with guarded recursion that denotes the behaviour of the instruction
sequence denoted by P . The thread extraction operation is defined by the equations given in Table 4 (for a ∈ A, l ∈ N and u ∈ I) and the rule that |#l ; X| = D
if #l is the beginning of an infinite jump chain. This rule is formalized in e.g. [4].

4

Interaction of Threads with Services

A thread may make use of services. That is, a thread may perform an action for
the purpose of interacting with a service that takes the action as a command to
be processed. The processing of an action may involve a change of state of the
service and at completion of the processing of the action the service returns a
reply value to the thread. In this section, we introduce the use operators, which
are concerned with this kind of interaction between threads and services.
It is assumed that a fixed but arbitrary set F of foci and a fixed but arbitrary
set M of methods have been given. Each focus plays the role of a name of some
service provided by an execution environment that can be requested to process
a command. Each method plays the role of a command proper. For the set A
of actions, we take the set {f.m | f ∈ F, m ∈ M}. Performing an action f.m is
taken as making a request to the service named f to process command m.
A service H consists of
–
–
–
–

a set S of states;
an effect function eff : M × S → S;
a yield function yld : M × S → {T, F, B};
an initial state s0 ∈ S;

satisfying the following condition:
∀m ∈ M, s ∈ S • (yld (m, s) = B ⇒ ∀m′ ∈ M • yld (m′ , eff (m, s)) = B) .
5

Table 5. Axioms for use operators
S /f H = S

TSU1

D /f H = D

TSU2

(x E g.m D y) /f H = (x /f H) E g.m D (y /f H)
∂
H
∂m
∂
/f ∂m H

if f 6= g

TSU3

(x E f.m D y) /f H = x /f

if H(m) = T TSU4

(x E f.m D y) /f H = y

if H(m) = F TSU5

(x E f.m D y) /f H = D
if H(m) = B TSU6
V
π
(x)
/
H
=
π
(y)
/
H
⇒
x
/
H
=
y
/
H
TSU7
n
n
f
f
f
f
n≥0

The set S contains the states in which the service may be, and the functions eff
and yld give, for each method m and state s, the state and reply, respectively,
that result from processing m in state s.
Let H = (S, eff , yld , s0 ) be a service and let m ∈ M. Then the derived service
∂
H, is the service (S, eff , yld , eff (m, s0 )); and
of H after processing m, written ∂m
the reply of H after processing m, written H(m), is yld (m, s0 ).
When a thread makes a request to service H to process m:
– if H(m) 6= B, then the request is accepted, the reply is H(m), and the service
∂
proceeds as ∂m
H;
– if H(m) = B, then the request is rejected.
We introduce the sort S of services and, for each f ∈ F, the binary use
operator /f : T × S → T. The axioms for these operators are given in Table 5.
Intuitively, p /f H is the thread that results from processing all actions performed by thread p that are of the form f.m by service H. When an action of the
form f.m performed by thread p is processed by service H, the postconditional
composition concerned is eliminated on the basis of the reply value produced.
No internal action is left as a trace of the processed action, like with the use
operators found in papers on thread interleaving
(see e.g. [3]).
V
Combining TSU2 and TSU7, we obtain n≥0 πn (x)/f H = D ⇒ x/f H = D.

5

Instruction Sequences Acting on Boolean Registers

Our study of jump-free instruction sequences in Section 6 is concerned with
instruction sequences that act on Boolean registers. In this section, we describe
services that make up Boolean registers.
A Boolean register service accepts the following methods:
– a set to true method set:T;
– a set to false method set:F;
– a get method get.
We write MBR for the set {set:T, set:F, get}. It is assumed that MBR ⊆ M.
The methods accepted by Boolean register services can be explained as follows:
6

– set:T : the contents of the Boolean register becomes T and the reply is T;
– set:F : the contents of the Boolean register becomes F and the reply is F;
– get : nothing changes and the reply is the contents of the Boolean register.
Let s ∈ {T, F, B}. Then the Boolean register service with initial state s, written BR s , is the service ({T, F, B} , eff , eff , s), where the function eff is defined
as follows (b ∈ {T, F}):
eff (set:T, b) = T ,
eff (set:F, b) = F ,

eff (m, b) = B if m 6∈ MBR ,
eff (m, B) = B .

eff (get, b) = b ,
Notice that the effect and yield functions of a Boolean register service are the
same.

6

Jump-Free Instruction Sequences

In this section, we show that each thread that can only be in a finite number of
states can be produced by some single-pass instruction sequence without jump
instructions if use can be made of Boolean register services.
First, we make precise what it means that a thread can only be in a finite
number of states. We assume that a fixed but arbitrary model M of BTA extended with guarded recursion and the use mechanism has been given, we use
the term thread only for the elements from the domain of M, and we denote the
interpretations of constants and operators in M by the constants and operators
themselves.
Let p be a thread. Then the set of states or residual threads of p, written
Res(p), is inductively defined as follows:
– p ∈ Res(p);
– if q E a D r ∈ Res(p), then q ∈ Res(p) and r ∈ Res(p).
We say that p is a regular thread if Res(p) is finite.
We will make use of the fact that being a regular thread coincides with being
the solution of a finite guarded recursive specification of a restricted form.
A linear recursive specification over BTA is a guarded recursive specification
E = {X = tX | X ∈ V }, where each tX is a term of the form D, S or Y E a D Z
with Y, Z ∈ V .
Proposition 1. Let p be a thread. Then p is a regular thread iff there exists a
finite linear recursive specification E and a variable X ∈ V(E) such that p is the
solution of E for X.
Proof. This proposition generalizes Theorem 1 from [6] from the projective limit
model to an arbitrary model. However, the proof of that theorem is applicable
to any model.
⊓
⊔

7

In the proof of the next theorem, we associate a closed PGA term P in which
jump instructions do not occur with a finite linear recursive specification

E = Xi = Xl(i) E ai D Xr(i) | i ∈ [1, n] ∪ {Xn+1 = S, Xn+2 = D} .
In P , a number of Boolean register services is used for specific purposes. The
purpose of each individual Boolean register is reflected in the focus that serves
as its name:
– for each i ∈ [1, n + 2], s:i serves as the name of a Boolean register that is
used to indicate whether the current state of hX1 |Ei is hXi |Ei;
– rt serves as the name of a Boolean register that is used to indicate whether
the reply upon the action performed by hX1 |Ei in its current state is T;
– rf serves as the name of a Boolean register that is used to indicate whether
the reply upon the action performed by hX1 |Ei in its current state is F;
– e serves as the name of a Boolean register that is used to achieve that instructions not related to the current state of hX1 |Ei are passed correctly;
– f serves as the name of a Boolean register that is used to achieve with the
instruction +f.set:F that the following instruction is skipped.
Now we turn to the theorem announced above. It states rigorously that the
solution of every finite linear recursive specification can be produced by an instruction sequence without jump instructions if use can be made of Boolean
register services.
Theorem 1. Let a finite linear recursive specification

E = Xi = Xl(i) E ai D Xr(i) | i ∈ [1, n] ∪ {Xn+1 = S, Xn+2 = D}
be given. Then there exists a closed PGA term P in which jump instructions do
not occur such that
hX1 |Ei
= ((((. . . (|P | /s:1 BR F ) . . . /s:n+2 BR F ) /rt BR F ) /rf BR F ) /e BR F ) /f BR F .
Proof. We associate a closed PGA term P in which jump instructions do not
occur with E as follows:
P = s:1.set:T ; (Q1 ; . . . ; Qn+1 )ω ,
where, for each i ∈ [1, n]:
Qi

= +s:i.get ; e.set:T ;
+s:i.get ; s:i.set:F ;
+e.get ; −ai ; +f.set:F ; rt.set:T ;
+e.get ; +rt.get ; +f.set:F ; rf.set:T ;
+rt.get ; s:l(i).set:T ;
+rf.get ; s:r(i).set:T ;
rt.set:F ; rf.set:F ; e.set:F ,
8

and
Qn+1 = +s:n+1.get ; ! .
We use the following abbreviations (for i ∈ [1, n + 1] and j ∈ [1, n + 2]):
Pi′
for Qi ; . . . ; Qn+1 ; (Q1 ; . . . ; Qn+1 )ω ;
′
|Pi′ |br
j for ((((. . . (|Pi | /s:1 BR b1 ) . . . /s:n+2 BR bn+2 ) /rt BR F ) /rf BR F ) /e BR F ) /f BR F ,
where bj = T and, for each j ′ ∈ [1, n + 2] such that j ′ 6= j, bj ′ = F.
From the definition of thread extraction, the definition of Boolean register services, and axiom TSU4, it follows that
((((. . . (|P | /s:1 BR F ) . . . /s:n+2 BR F ) /rt BR F ) /rf BR F ) /e BR F ) /f BR F
= |P1′ |br
1 .
This leaves us to show that hX1 |Ei = |P1′ |br
1 .
Using the definition of thread extraction, the definition of Boolean register
services, and axioms P0, P2, TSU1, TSU2, TSU4, TSU5 and TSU7, we easily
prove the following:
′
br
|Pi′ |br
j = |Pi+1 |j

if 1 ≤ i ≤ n ∧ 1 ≤ j ≤ n + 1 ∧ i 6= j (1)

′ br
|Pi′ |br
if i = n + 1 ∧ 1 ≤ j ≤ n + 1 ∧ i 6= j (2)
j = |P1 |j
′ br
′
br
′
br
|Pi |i = |Pi+1 |l(i) E ai D |Pi+1 |r(i) if 1 ≤ i ≤ n
(3)

|Pi′ |br
i =S
′ br
|Pi |j = D

if i = n + 1
if 1 ≤ i ≤ n + 1 ∧ j = n + 2

(4)
(5)

From Properties 1 and 2, it follows that
′ br
|Pi′ |br
j = |Pj |j if 1 ≤ i ≤ n + 1 ∧ 1 ≤ j ≤ n + 1 ∧ i 6= j .

From this and Property 3, it follows that
′
br
′
br
|Pi′ |br
i = |Pl(i) |l(i) E ai D |Pr(i) |r(i) if 1 ≤ i ≤ n .

From this and Properties 4 and 5, it follows that |P1′ |br
1 is a solution of E for
X1 . Because linear recursive specifications have unique solutions, it follows that
⊓
⊔
hX1 |Ei = |P1′ |br
1 .
Theorem 1 goes through in the case where E = {X1 = D}: a witnessing P
is (f.get)ω . It follows from the proof of Proposition 1 given in [6] that, for each
regular thread p, either p is the solution of {X1 = D} for X1 or there exists a
finite linear recursive specification E of the form considered in Theorem 1 such
that p is the solution of E for X1 . Hence, we have the following corollary of
Proposition 1 and Theorem 1:
Corollary 1. For each regular thread p, there exists a closed PGA term P in
which jump instructions do not occur such that p is the thread denoted by
((((. . . (|P | /s:1 BR F ) . . . /s:n+2 BR F ) /rt BR F ) /rf BR F ) /e BR F ) /f BR F .
9

In other words, each regular thread can be produced by an instruction sequence
without jump instructions if use can be made of Boolean register services.
The construction of such instructions sequences given in the proof of Theorem 1 is weakly reminiscent of the construction of structured programs from flow
charts found in [5]. However, our construction is more extreme: it yields programs
that contain neither unstructured jumps nor a rendering of the conditional and
loop constructs used in structured programming.

7

Program Algebra with Labels and Goto’s

In this section, we introduce PGAg , a variant of PGA obtained by leaving out
jump instructions and adding labels and goto instructions.
In PGAg , like in PGA, it is assumed that a fixed but arbitrary set A of basic
instructions has been given. PGAg has the following primitive instructions:
–
–
–
–
–
–

for each a ∈ A, a plain basic instruction a;
for each a ∈ A, a positive test instruction +a;
for each a ∈ A, a negative test instruction −a;
for each l ∈ N, a label instruction [l];
for each l ∈ N, a goto instruction #[l];
a termination instruction !.

We write Ig for the set of all primitive instructions of PGAg .
The plain basic instructions, the positive test instructions, the negative test
instructions, and the termination instruction are as in PGA. Upon execution,
a label instruction [l] is simply skipped. If there is no next instruction to be
executed, deadlock occurs. The effect of a goto instruction #[l] is that execution
proceeds with the occurrence of the label instruction [l] next following if it exists.
If there is no occurrence of the label instruction [l], deadlock occurs.
PGAg has a constant u for each u ∈ Ig . The operators of PGAg are the same
as the operators as PGA. Likewise, the axioms of PGAg are the same as the
axioms as PGA.
Just like in the case of PGA, the behaviours of the instruction sequences
denoted by closed PGAg terms are considered threads. The behaviours of the
instruction sequences denoted by closed PGAg terms are indirectly given by the
behaviour preserving function pgag2pga from the set of all closed PGAg terms
to the set of all closed PGA terms defined by
pgag2pga(u1 ; . . . ; un ) = pgag2pga(u1 ; . . . ; un ; (#[1])ω ) ,
pgag2pga(u1 ; . . . ; un ; (un+1 ; . . . ; um )ω )
= φ1 (u1 ) ; . . . ; φn (un ) ; (φn+1 (un+1 ) ; . . . ; φm (um ))ω ,
where the auxiliary functions φj : Ig → I are defined as follows (1 ≤ j ≤ m):
φj ([l])

= #1 ,

φj (#[l]) = #tgt j (l) ,
φj (u)

=u

if u is not a label or goto instruction ,
10

where
– tgt j (l) = i if the leftmost occurrence of [l] in uj ; . . . ; um ; un+1 ; . . . ; um is
the i-th instruction;
– tgt j (l) = 0 if there are no occurrences of [l] in uj ; . . . ; um ; un+1 ; . . . ; um .
Let P be a closed PGAg term. Then the behaviour of P is |pgag2pga(P )|. The
approach to semantics followed here is introduced under the name projection
semantics in [2]. The function pgag2pga is called a projection.

8

A Bounded Number of Labels

In this section, we show that a bound to the number of labels restricts the
expressiveness of PGAg . We will refer to PGAg terms that do not contain label
instructions [l] with l > k as PGAkg terms. Moreover, we will write Ikg for the set
Ig \ {[l] | l > k}.
We define an alternative projection for closed PGAkg terms, which takes into
account that these terms contain only label instructions [l] with 1 ≤ l ≤ k. The
alternative projection pgag2pgak from the set of all closed PGAkg terms to the
set of all closed PGA terms is defined by
pgag2pgak (u1 ; . . . ; un ) = pgag2pgak (u1 ; . . . ; un ; (#[1])ω ) ,
pgag2pgak (u1 ; . . . ; un ; (un+1 ; . . . ; um )ω )
= ψ(u1 , u2 ) ; . . . ; ψ(un , un+1 ) ;
(ψ(un+1 , un+2 ) ; . . . ; ψ(um−1 , um ) ; ψ(um , un+1 ))ω ,
where the auxiliary function ψ : Ikg × Ikg → I is defined as follows:
ψ(u′ , u′′ ) = ψ ′ (u′ ) ; #k+2 ; #k+2 ; ψ ′′ (u′′ ) ,
where the auxiliary functions ψ ′ , ψ ′′ : Ikg → I are defined as follows:
ψ ′ ([l])

= #1 ,

′

ψ (#[l]) = #l+2
ψ ′ (#[l]) = #0

if l ≤ k ,
if l > k ,

ψ ′ (u)

if u is not a label or goto instruction ,

=u

ψ ′′ ([l]) = (#k+3)l−1 ; #k−l+1 ; (#k+3)k−l ,
ψ ′′ (u)

= (#k+3)k if u is not a label instruction .

In order to clarify the alternative projection, we explain how the intended
effect of a goto instruction is obtained. If uj is #[l], then ψ ′ (uj ) is #l+2. The
effect of #l+2 is a jump to the l-th instruction in ψ ′′ (uj+1 ) if j < m and a jump
to the l-th instruction in ψ ′′ (un+1 ) if j = m. If this instruction is #k−l+1, then
its effect is a jump to the occurrence of #1 that replaces [l]. However, if this
11

instruction is #k+3, then its effect is a jump to the l-th instruction in ψ ′′ (uj+2 )
if j < m − 1, a jump to the l-th instruction in ψ ′′ (un+1 ) if j = m − 1, and a
jump to the l-th instruction in ψ ′′ (un+2 ) if j = m.
In the proof of Theorem 2 below, chains of forward jumps are removed in
favour of single jumps. The following proposition justifies these removals.
Proposition 2. For each PGA context C[ ]:
|C[#n + 1 ; u1 ; . . . ; un ; #m]| = |C[#m + n + 1 ; u1 ; . . . ; un ; #m]| .
Proof. Contexts of the forms C[ ]ω ;Q and P ;C[ ]ω ;Q do not need to be considered
because of axiom PGA3. For eight of the remaining twelve forms, the equation
to be proved follows immediately from the equations to be proved for the other
forms, to wit ;Q, P ; ;Q, P ; ω and P ;(Q ; )ω , the axioms of PGA, the defining
equations for thread extraction, and the easy to prove fact that |P ; #0| = |P |.
In the case of the form ; Q, the equation concerned is easily proved by
induction on n. In the case of the form P ; ; Q, only P in which the repetition
operator does not occur need to be considered because of axiom PGA3. For such
P , the equation concerned is easily proved by induction on the length of P , using
the equation proved for the form ; Q. In the case of the form P ; ω , only P in
which the repetition operator does not occur need to be considered because of
axiom PGA3. For such P , the equations for the approximating forms P ; k are
easily proved by induction on k, using the equation proved for the form P ; ; Q.
From these equations, the equation for the form P ; ω follows using AIP. In the
case of the form P ; (Q ; )ω , the equation concerned is proved like in the case of
⊓
⊔
the form P ; ω .
The following theorem states rigorously that the projections pgag2pga and
pgag2pgak give rise to instruction sequences with the same behaviour.
Theorem 2. For each closed PGAkg term P , |pgag2pga(P )| = |pgag2pgak (P )|.
Proof. Because pgag2pga(u1 ; . . . ; un ) = pgag2pga(u1 ; . . . ; un ; (#[1])ω ) and
pgag2pgak (u1 ; . . . ; un ) = pgag2pgak (u1 ; . . . ; un ; (#[1])ω ), we only consider the
case where the repetition operator occurs in P .
We make use of an auxiliary function | , |. This function determines, for each
natural number and closed PGA term in which the repetition operator occurs,
a closed term of BTA with guarded recursion. The function | , | is defined as
follows:
|i, u1 ; . . . ; un ; (un+1 ; . . . ; um )ω |
= |ui ; . . . ; um ; (un+1 ; . . . ; um )ω | if 1 ≤ i ≤ m ,
|i, u1 ; . . . ; un ; (un+1 ; . . . ; um )ω | = D if ¬ 1 ≤ i ≤ m .
Let P = u1 ; . . . ; un ; (un+1 ; . . . ; um )ω be a closed PGAkg term, let P ′ =
pgag2pga(P ), and let P ′′ = pgag2pgak (P ). Moreover, let ρ : N → N be such that
f (i) = (k + 3) · (i − 1) + 1. Then it follows easily from the definitions of | , |,
| |, pgag2pga and pgag2pgak , the axioms of PGA and Proposition 2 that for
1 ≤ i ≤ m:
12

|i, P ′ | = a ◦ |i + 1, P ′ |
′

if ui = a ,

′

′

|i, P | = |i + 1, P | E a D |i + 2, P | if ui = +a ,
|i, P ′ | = |i + 2, P ′ | E a D |i + 1, P ′ | if ui = −a ,
|i, P ′ | = |i + 1, P ′ |
if ui = [l] ,
|i, P ′ | = |i + n, P ′ |
|i, P ′ | = S

if ui = #[l] ∧ tgt i (l) = n ,
if ui = ! .

and
|ρ(i), P ′′ | = a ◦ |ρ(i + 1), P ′′ |
′′

if ui = a ,

′′

′′

|ρ(i), P | = |ρ(i + 1), P | E a D |ρ(i + 2), P | if ui = +a ,
|ρ(i), P ′′ | = |ρ(i + 2), P ′′ | E a D |ρ(i + 1), P ′′ | if ui = −a ,
|ρ(i), P ′′ | = |ρ(i + 1), P ′′ |
|ρ(i), P ′′ | = |ρ(i + n), P ′′ |

if ui = [l] ,
if ui = #[l] ∧ tgt i (l) = n ,

|ρ(i), P ′′ | = S

if ui = !

(where tgti is as in the definition of pgag2pga). Because |pgag2pga(P )| =
|1, P ′ | and |pgag2pgak (P )| = |ρ(1), P ′′ |, this means that |pgag2pga(P )| and
|pgag2pgak (P )| are solutions of the same guarded recursive specification. Because guarded recursive specifications have unique solutions, it follows that
|pgag2pga(P )| = |pgag2pgak (P )|.
⊓
⊔
The projection pgag2pgak (P ) yields only closed PGA terms that do not contain
jump instructions #l with l > k + 3. Hence, we have the following corollary of
Theorem 2:
Corollary 2. For each closed PGAkg term P , there exists a closed PGA term P ′
not containing jump instructions #l with l > k + 3 such that |pgag2pga(P )| =
|P ′ |.
It follows from Corollary 2 that, if a regular thread cannot be denoted by a
closed PGA term that does not contain jump instructions #l with l > k + 3, it
cannot be denoted by a closed PGAkg term. Moreover, it is known that, for each
k ∈ N, there exists a closed PGA term for which there does not exist a closed
PGA term not containing jump instructions #l with l > k + 3 that denotes
the same thread (see e.g. [6], Proposition 3). Hence, we also have the following
corollary:
Corollary 3. For each k ∈ N, there exists a closed PGA term P for which there
does not exist a closed PGAkg term P ′ such that |P | = |pgag2pga(P ′ )|.

9

Conclusions

Program algebra is a setting suited for investigating single-pass instruction sequences. In this setting, we have shown that each behaviour that can be produced by a single-pass instruction sequence under execution can be produced
13

by a single-pass instruction sequence without jump instructions if use can be
made of Boolean register services. This is considered an interesting expressiveness result. An important variant of program algebra is obtained by leaving out
jump instructions and adding labels and goto instructions. We have also shown
that a bound to the number of labels restricts the expressiveness of this variant.
Earlier expressiveness results on single-pass instruction sequences as considered
in program algebra are collected in [6].
Program algebra does not provide a notation for programs that is intended
for actual programming. However, to demonstrate that single-pass instruction
sequences as considered in program algebra are suited for explaining programs
in the form of assembly programs as well as programs in the form of structured
programs, a hierarchy of program notations rooted in program algebra is introduced in [2]. One program notation belonging to this hierarchy, called PGLDg ,
is a simple program notation, close to existing assembly languages, with labels
and goto instructions. We remark that a projection from the set of all PGLDg
programs to the set of all closed PGAg terms can easily be devised.
The idea that programs are in essence single-pass instruction sequences underlies the choice for the name program algebra. The name seems to imply that
program algebra is suited for investigating programs in general. We do not intend
to claim this generality, which in any case does not matter when investigating
single-pass instruction sequences. The name program algebra might as well be
used as a collective name for algebras that are based on any viewpoint concerning
programs. To our knowledge, it is not common to use the name as such.
Acknowledgements
We thank Alban Ponse, colleague at the University of Amsterdam, and Stephan
Schroevers, graduate student at the University of Amsterdam, for carefully reading a preliminary version of this paper and pointing out some flaws in it.

References
1. Bergstra, J.A., Bethke, I.: Polarized process algebra and program equivalence. In:
J.C.M. Baeten, J.K. Lenstra, J. Parrow, G.J. Woeginger (eds.) Proceedings 30th
ICALP, Lecture Notes in Computer Science, vol. 2719, pp. 1–21. Springer-Verlag
(2003)
2. Bergstra, J.A., Loots, M.E.: Program algebra for sequential code. Journal of Logic
and Algebraic Programming 51(2), 125–156 (2002)
3. Bergstra, J.A., Middelburg, C.A.: Distributed strategic interleaving with load balancing. Future Generation Computer Systems 24(6), 530–548 (2008)
4. Bergstra, J.A., Middelburg, C.A.: Program algebra with a jump-shift instruction.
Journal of Applied Logic 6(4), 553–563 (2008)
5. Cooper, D.C.: Böhm and Jacopini’s reduction of flow charts. Communications of
the ACM 10(8), 463, 473 (1967)
6. Ponse, A., van der Zwaag, M.B.: An introduction to program and thread algebra.
In: A. Beckmann, et al. (eds.) CiE 2006, Lecture Notes in Computer Science, vol.
3988, pp. 445–458. Springer-Verlag (2006)

14

