Axioms for behavioural congruence of single-pass instruction sequences

TL;DR

This paper develops an axiom system for behavioural congruence in program algebra, focusing on single-pass instruction sequences, with particular attention to axioms involving forward jump instructions.

Contribution

It introduces the first axiom system specifically for behavioural congruence, expanding the algebraic theory of instruction sequences.

Findings

Axiom system for behavioural congruence is sound and complete.

Special axioms for forward jump instructions are provided.

Advances understanding of instruction sequence equivalence.

Abstract

In program algebra, an algebraic theory of single-pass instruction sequences, three congruences on instruction sequences are paid attention to: instruction sequence congruence, structural congruence, and behavioural congruence. Sound and complete axiom systems for the first two congruences were already given in early papers on program algebra. The current paper is the first one that is concerned with an axiom system for the third congruence. The presented axiom system is especially notable for its axioms that have to do with forward jump instructions.

Tables

Table 1. Table 1: Axioms of PGA bc superscript PGA bc \mathrm{PGA^{bc}}

Table 2. Table 2: Axioms of BTA ∞ superscript BTA \mathrm{BTA^{\infty}}

Table 3. Table 3: Axioms for the thread extraction operator

Table 4. Table 4: Additional axioms for PGA br bc superscript subscript PGA br bc \mathrm{PGA_{br}^{bc}}

Table 5. Table 5: Axioms of BTA br subscript BTA br \mathrm{BTA_{br}}

Full text

1 Introduction

Program algebra, an algebraic theory of single-pass instruction sequences, was first presented in [3] as the basis of an approach to programming language semantics. Various issues, including issues relating to programming language expressiveness, computability, computational complexity, algorithm efficiency, algorithmic equivalence of programs, program verification, program performance, program compactness, and program parallelization, have been studied in the setting of program algebra since then. An overview of all the work done to date and some open questions originating from it can be found at [13]. Three congruences on instruction sequences were introduced in [3]: instruction sequence congruence, structural congruence and behavioural congruence. Sound and complete axiom systems for instruction sequence congruence and structural congruence were already provided in [3], but an axiom system for behavioural congruence has never been provided. This paper is concerned with an axiom system for behavioural congruence.

Program algebra is parameterized by a set of uninterpreted basic instructions. In applications of program algebra, this set is instantiated by a set of interpreted basic instructions. In the case of most issues that have been studied in the setting of program algebra, the interpreted basic instructions are instructions to set and get the content of Boolean registers. In the case of a few issues, the interpreted basic instructions are other instructions, e.g. instructions to manipulate the content of counters or instructions to manipulate the content of Turing machine tapes (see e.g. [4]).

In the uninstantiated case, behavioural congruence is the coarsest congruence respecting the behaviour produced by instruction sequences under execution that is possible with uninterpreted basic instructions. In the instantiated cases, behavioural congruence is the coarsest congruence respecting the behaviour produced by instruction sequences under execution that is possible taking the intended interpretation of the basic instructions into account. In this paper, an emphasis is laid on the uninstantiated case. Yet attention is paid to the instantiation in which all possible instructions for Boolean registers are taken as basic instructions.

The single-pass instruction sequences considered in program algebra are non-empty, finite or eventually periodic infinite instruction sequences. In this paper, the soundness question, i.e. the question whether derivable equality implies behavioural congruence, is fully answered in the affirmative. However, the completeness question, i.e. the question whether behavioural congruence implies derivable equality, is answered in the affirmative only for the restriction to finite instruction sequences because of problems in mastering the intricacy of a completeness proof for the unrestricted case.

In [3], basic thread algebra, an algebraic theory of mathematical objects that model in a direct way the behaviours produced by instruction sequences under execution, was introduced to describe which behaviours are produced by the instruction sequences considered in program algebra.111In [3], basic thread algebra is introduced under the name basic polarized process algebra. It is rather awkward to describe and analyze the behaviours of this kind using algebraic theories of processes such as ACP [1, 2], CCS [11, 14] and CSP [10, 12]. However, the objects considered in basic thread algebra can be viewed as representations of processes as considered in ACP (see e.g. [6]). Basic thread algebra is parameterized by a set of uninterpreted basic actions and, when it is used for describing the behaviours produced by instruction sequences under execution, basic instructions are taken as basic actions. Like in [3], basic thread algebra will be used in this paper for describing the behaviours produced by the instruction sequences considered in program algebra and to define the notion of behavioural congruence of instruction sequences.

This paper is organized as follows. First, we introduce a version of program algebra with axioms for instruction sequence congruence, structural congruence, and behavioural congruence (Section 2). Next, we present the preliminaries on basic thread algebra that are needed in the rest of the paper (Section 3). After that, we describe which behaviours are produced by instruction sequences under execution and define a notion of behavioural congruence for instruction sequences (Section 4). Then, we go into the soundness and completeness of the presented axiom system with respect to the defined notion of behavioural congruence (Section 5). Following this, we look at the instantiation of program algebra in which all possible instructions for Boolean registers are taken as basic instructions (Section 6). Finally, we make some concluding remarks (Section 7).

The following should be mentioned in advance. The set $\mathbb{B}$ of Boolean values is a set with two elements whose intended interpretations are the truth values false and true. As is common practice, we represent the elements of $\mathbb{B}$ by the bits [math] and $1$.

This paper draws somewhat from the preliminaries of earlier papers that built on program algebra and basic thread algebra. The most recent one of the papers in question is [9].

2 Program Algebra for Behavioural Congruence

In this section, we present $\mathrm{PGA^{bc}}$. $\mathrm{PGA^{bc}}$ is a version of $\mathrm{PGA}$ (ProGram Algebra) with, in addition to the usual axioms for instruction sequence congruence and structural congruence, axioms for behavioural congruence.

The instruction sequences considered in $\mathrm{PGA^{bc}}$ are single-pass instruction sequences of a particular kind.222The instruction sequences concerned are single-pass in the sense that they are instruction sequences of which each instruction is executed at most once and can be dropped after it has been executed or jumped over. It is assumed that a fixed but arbitrary set $\mathcal{A}$ of basic instructions has been given. $\mathcal{A}$ is the basis for the set of instructions that may occur in the instruction sequences considered in $\mathrm{PGA^{bc}}$. The intuition is that the execution of a basic instruction may modify a state and must produce a Boolean value as reply at its completion. The actual reply may be state-dependent.

The set of instructions of which the instruction sequences considered in $\mathrm{PGA^{bc}}$ are composed is the set that consists of the following elements:

• •

for each $a\in\mathcal{A}$, a plain basic instruction $a$;

• •

for each $a\in\mathcal{A}$, a positive test instruction ${+}a$;

• •

for each $a\in\mathcal{A}$, a negative test instruction ${-}a$;

• •

for each $l\in\mathbb{N}$, a forward jump instruction $\#l$;

• •

a termination instruction $\mathord{!}$.

We write $\mathcal{I}$ for this set. The elements from this set are called primitive instructions.

Primitive instructions are the elements of the instruction sequences considered in $\mathrm{PGA^{bc}}$. On execution of such an instruction sequence, these primitive instructions have the following effects:

• •

the effect of a positive test instruction ${+}a$ is that basic instruction $a$ is executed and execution proceeds with the next primitive instruction if ${1}$ is produced and otherwise the next primitive instruction is skipped and execution proceeds with the primitive instruction following the skipped one — if there is no primitive instruction to proceed with, inaction occurs;

• •

the effect of a negative test instruction ${-}a$ is the same as the effect of ${+}a$, but with the role of the value produced reversed;

• •

the effect of a plain basic instruction $a$ is the same as the effect of ${+}a$, but execution always proceeds as if ${1}$ is produced;

• •

the effect of a forward jump instruction $\#l$ is that execution proceeds with the $l$th next primitive instruction — if $l$ equals [math] or there is no primitive instruction to proceed with, inaction occurs;

• •

the effect of the termination instruction $\mathord{!}$ is that execution terminates.

Inaction occurs if no more basic instructions are executed, but execution does not terminate.

$\mathrm{PGA^{bc}}$ has one sort: the sort $\mathbf{IS}$ of instruction sequences. We make this sort explicit to anticipate the need for many-sortedness later on. To build terms of sort $\mathbf{IS}$, $\mathrm{PGA^{bc}}$ has the following constants and operators:

• •

for each $u\in\mathcal{I}$, the instruction constant $u\mathbin{:\,\to}\mathbf{IS}$ ;

• •

the binary concatenation operator ${\_\hskip 1.00006pt}\mathbin{;}{\_\hskip 1.00006pt}\mathbin{:}\mathbf{IS}\times\mathbf{IS}\to\mathbf{IS}$ ;

• •

the unary repetition operator ${\_\hskip 1.00006pt}^{\omega}\mathbin{:}\mathbf{IS}\to\mathbf{IS}$ .

Terms of sort $\mathbf{IS}$ are built as usual in the one-sorted case. We assume that there are infinitely many variables of sort $\mathbf{IS}$, including $X,Y,Z$. We use infix notation for concatenation and postfix notation for repetition.

A $\mathrm{PGA^{bc}}$ term in which the repetition operator does not occur is called a repetition-free $\mathrm{PGA^{bc}}$ term.

One way of thinking about closed $\mathrm{PGA^{bc}}$ terms is that they represent non-empty, finite or eventually periodic infinite sequences of primitive instructions.333An eventually periodic infinite sequence is an infinite sequence with only finitely many distinct suffixes. The instruction sequence represented by a closed term of the form $t\mathbin{;}t^{\prime}$ is the instruction sequence represented by $t$ concatenated with the instruction sequence represented by $t^{\prime}$. The instruction sequence represented by a closed term of the form $t^{\omega}$ is the instruction sequence represented by $t$ concatenated infinitely many times with itself. A closed $\mathrm{PGA^{bc}}$ term represents a finite instruction sequence if and only if it is a closed repetition-free $\mathrm{PGA^{bc}}$ term.

In this paper, closed $\mathrm{PGA^{bc}}$ terms are considered equal if the instruction sequences that they represent can always take each other’s place in an instruction sequence in the sense that the behaviour produced under execution remains the same irrespective of the interpretation of the instructions from $\mathcal{A}$. In other words, equality of closed terms stands in $\mathrm{PGA^{bc}}$ for a kind of behavioural congruence of the represented instruction sequences. The kind of behavioural congruence in question will be made precise in Section 4.

The axioms of $\mathrm{PGA^{bc}}$ are given in Table 1.

In this table, $n$ stands for an arbitrary natural number from $\mathbb{N}_{1}$,444We write $\mathbb{N}_{1}$ for the set $\{n\in\mathbb{N}\mathrel{\mid}n\geq 1\}$ of positive natural numbers. $u$, $u_{1},\ldots,u_{k}$ and $v_{1},\ldots,v_{k^{\prime}+1}$ stand for arbitrary primitive instructions from $\mathcal{I}$, $k$, $k^{\prime}$, and $l$ stand for arbitrary natural numbers from $\mathbb{N}$, and $a$ stands for an arbitrary basic instruction from $\mathcal{A}$. For each $n\in\mathbb{N}_{1}$, the term $t^{n}$, where $t$ is a $\mathrm{PGA^{bc}}$ term, is defined by induction on $n$ as follows: $t^{1}=t$, and $t^{n+1}=t\mathbin{;}t^{n}$.

If $t=t^{\prime}$ is derivable from PGA1–PGA4, then $t$ and $t^{\prime}$ represent the same instruction sequence. In this case, we say that the represented instruction sequences are instruction sequence congruent. We write $\mathrm{PGA^{isc}}$ for the algebraic theory whose sorts, constants and operators are those of $\mathrm{PGA^{bc}}$, but whose axioms are PGA1–PGA4.

The unfolding equation $X^{\omega}=X\mathbin{;}X^{\omega}$ is derivable from the axioms of $\mathrm{PGA^{isc}}$ by first taking the instance of PGA2 in which $n=2$, then applying PGA4, and finally applying the instance of PGA2 in which $n=2$ again.

A closed $\mathrm{PGA^{bc}}$ term is in first canonical form if it is of the form $t$ or $t\mathbin{;}{t^{\prime}}^{\omega}$, where $t$ and $t^{\prime}$ are closed repetition-free $\mathrm{PGA^{bc}}$ terms. The following proposition relates $\mathrm{PGA^{isc}}$ and first canonical forms.

Proposition 1

For all closed $\mathrm{PGA^{bc}}$ terms $t$, there exists a closed $\mathrm{PGA^{bc}}$ term $t^{\prime}$ that is in first canonical form such that $t=t^{\prime}$ is derivable from the axioms of $\mathrm{PGA^{isc}}$.

Proof

The proof is analogous to the proof of Lemma 2.2 from [5]. ∎

If $t=t^{\prime}$ is derivable from PGA1–PGA8, then $t$ and $t^{\prime}$ represent the same instruction sequence after changing all chained jumps into single jumps and making all jumps ending in the repeating part as short as possible if they are eventually periodic infinite sequences. In this case, we say that the represented instruction sequences are structurally congruent. We write $\mathrm{PGA^{sc}}$ for the algebraic theory whose sorts, constants and operators are those of $\mathrm{PGA^{bc}}$, but whose axioms are PGA1–PGA8.

A closed $\mathrm{PGA^{bc}}$ term $t$ has chained jumps if there exists a closed $\mathrm{PGA^{bc}}$ term $t^{\prime}$ such that $t=t^{\prime}$ is derivable from the axioms of $\mathrm{PGA^{isc}}$ and $t^{\prime}$ contains a subterm of the form $\#n{+}1\mathbin{;}u_{1}\mathbin{;}\ldots\mathbin{;}u_{n}\mathbin{;}\#l$. A closed $\mathrm{PGA^{bc}}$ term $t$ that is in first canonical form has a repeating part if it is of the form $u_{1}\mathbin{;}\ldots\mathbin{;}u_{m}\mathbin{;}(v_{1}\mathbin{;}\ldots\mathbin{;}v_{k})^{\omega}$. A closed $\mathrm{PGA^{bc}}$ term $t$ of the form $u_{1}\mathbin{;}\ldots\mathbin{;}u_{m}\mathbin{;}(v_{1}\mathbin{;}\ldots\mathbin{;}v_{k})^{\omega}$ has shortest possible jumps ending in the repeating part if: (i) for each $i\in[1,m]$ for which $u_{i}$ is of the form $\#l$, $l\leq k+m-i$; (ii) for each $j\in[1,k]$ for which $v_{j}$ is of the form $\#l$, $l\leq k-1$. A closed $\mathrm{PGA^{bc}}$ term is in second canonical form if it is in first canonical form, does not have chained jumps, and has shortest possible jumps ending in the repeating part if it has a repeating part. The following proposition relates $\mathrm{PGA^{sc}}$ and second canonical forms.

Proposition 2

For all closed $\mathrm{PGA^{bc}}$ terms $t$, there exists a closed $\mathrm{PGA^{bc}}$ term $t^{\prime}$ that is in second canonical form such that $t=t^{\prime}$ is derivable from the axioms of $\mathrm{PGA^{sc}}$.

Proof

The proof is analogous to the proof of Lemma 2.3 from [5]. ∎

If $t=t^{\prime}$ is derivable from PGA1–PGA30, then $t$ and $t^{\prime}$ represent instruction sequences that can always take each other’s place in an instruction sequence without affecting the behaviour produced under execution in an essential way. In this case, we say that the represented instruction sequences are behaviourally congruent. In Section 4, we will use basic thread algebra to make precise which behaviours are produced by the represented instruction sequences under execution.

Axioms PGA1–PGA8 originate from [3]. Axioms PGA9–PGA30 are new and some of them did not come into the picture until we recently attempted to obtain a complete axiom system for behavioural congruence.

Henceforth, the instruction sequences of the kind considered in $\mathrm{PGA^{isc}}$, $\mathrm{PGA^{sc}}$, and $\mathrm{PGA^{bc}}$ are called $\mathrm{PGA}$ instruction sequences.

3 Basic Thread Algebra for Finite and Infinite Threads

In this section, we present an extension of $\mathrm{BTA}$ (Basic Thread Algebra) that reflects the idea that infinite threads are identical if their approximations up to any finite depth are identical.

$\mathrm{BTA}$ is concerned with mathematical objects that model in a direct way the behaviours produced by $\mathrm{PGA}$ instruction sequences under execution. The objects in question are called threads. A thread models a behaviour that consists of performing basic actions in a sequential fashion. Upon performing a basic action, a reply from an execution environment determines how the behaviour proceeds subsequently. The basic instructions from $\mathcal{A}$ are taken as basic actions.

$\mathrm{BTA}$ has one sort: the sort $\mathbf{T}$ of threads. We make this sort explicit to anticipate the need for many-sortedness later on. To build terms of sort $\mathbf{T}$, $\mathrm{BTA}$ has the following constants and operators:

• •

the inaction constant $\mathsf{D}\mathbin{:\,\to}\mathbf{T}$;

• •

the termination constant $\mathsf{S}\mathbin{:\,\to}\mathbf{T}$;

• •

for each $a\in\mathcal{A}$, the binary postconditional composition operator ${\_\hskip 1.00006pt}\mathbin{\unlhd\hskip 1.49994pta\hskip 1.49994pt\unrhd}\nolinebreak{\_\hskip 1.00006pt}\mathbin{:}\mathbf{T}\times\mathbf{T}\to\mathbf{T}$.

Terms of sort $\mathbf{T}$ are built as usual in the one-sorted case. We assume that there are infinitely many variables of sort $\mathbf{T}$, including $x,y,z$. We use infix notation for postconditional composition. We introduce basic action prefixing as an abbreviation: $a\circ t$, where $t$ is a $\mathrm{BTA}$ term, abbreviates $t\mathbin{\unlhd\hskip 1.49994pta\hskip 1.49994pt\unrhd}t$. We treat an expression of the form $a\circ t$ and the $\mathrm{BTA}$ term that it abbreviates as syntactically the same.

Different closed $\mathrm{BTA}$ terms are considered to represent different threads. The thread represented by a closed term of the form $t\mathbin{\unlhd\hskip 1.49994pta\hskip 1.49994pt\unrhd}t^{\prime}$ models the behaviour that will first perform $a$, and then proceed as the behaviour modeled by the thread represented by $t$ if the reply from the execution environment is ${1}$ and proceed as the behaviour modeled by the thread represented by $t^{\prime}$ if the reply from the execution environment is ${0}$. The thread represented by $\mathsf{S}$ models the behaviour that will do no more than terminate and the thread represented by $\mathsf{D}$ models the behaviour that will become inactive.

Closed $\mathrm{BTA}$ terms are considered equal if they represent the same thread. Equality of closed terms stands in $\mathrm{BTA}$ for syntactic identity. Therefore, $\mathrm{BTA}$ has no axioms.

Each closed $\mathrm{BTA}$ term represents a finite thread, i.e. a thread with a finite upper bound to the number of basic actions that it can perform. Infinite threads, i.e. threads without a finite upper bound to the number of basic actions that it can perform, can be defined by means of a set of recursion equations (see e.g. [4]). A regular thread is a finite or infinite thread that can only be in a finite number of states. The behaviours produced by $\mathrm{PGA}$ instruction sequences under execution are exactly the behaviours modeled by regular threads.

Two infinite threads are considered identical if their approximations up to any finite depth are identical. The approximation up to depth $n$ of a thread models the behaviour that differs from the behaviour modeled by the thread in that it will become inactive after it has performed $n$ actions unless it would terminate at this point. AIP (Approximation Induction Principle) is a conditional equation that formalizes the above-mentioned view on infinite threads. In AIP, the approximation up to depth $n$ is phrased in terms of the unary projection operator $\pi_{n}\mathbin{:}\mathbf{T}\to\mathbf{T}$.

The axioms for the projection operators and AIP are given in Table 2.

In this table, $a$ stands for an arbitrary basic action from $\mathcal{A}$ and $n$ stands for an arbitrary natural number from $\mathbb{N}$. We write $\mathrm{BTA^{\infty}}$ for $\mathrm{BTA}$ extended with the projection operators, the axioms for the projection operators, and AIP.

4 Thread Extraction and Behavioural Congruence

In this section, we make precise in the setting of $\mathrm{BTA^{\infty}}$ which behaviours are produced by $\mathrm{PGA}$ instruction sequences under execution and introduce the notion of behavioural congruence on $\mathrm{PGA}$ instruction sequences.

To make precise which behaviours are produced by $\mathrm{PGA}$ instruction sequences under execution, we introduce an operator $|{\_\hskip 1.00006pt}|$ meant for extracting from each $\mathrm{PGA}$ instruction sequence the thread that models the behaviour produced by it under execution. For each closed $\mathrm{PGA^{bc}}$ term $t$, $|t|$ represents the thread that models the behaviour produced by the instruction sequence represented by $t$ under execution.

Formally, we combine $\mathrm{PGA^{bc}}$ with $\mathrm{BTA^{\infty}}$ and extend the combination with the thread extraction operator $|{\_\hskip 1.00006pt}|\mathbin{:}\mathbf{IS}\to\mathbf{T}$ and the axioms given in Table 3.

In this table, $a$ stands for an arbitrary basic instruction from $\mathcal{A}$, $u$ stands for an arbitrary primitive instruction from $\mathcal{I}$, and $l$ stands for an arbitrary natural number from $\mathbb{N}$.

If a closed $\mathrm{PGA^{bc}}$ term $t$ represents an instruction sequence that starts with an infinite chain of forward jumps, then TE9 and TE11 can be applied to $|t|$ infinitely often without ever showing that a basic action is performed. In this case, we have to do with inaction and, being consistent with that, $t=\#0\mathbin{;}t^{\prime}$ is derivable from the axioms of $\mathrm{PGA^{sc}}$ for some closed $\mathrm{PGA^{bc}}$ term $t^{\prime}$. By contrast, $t=\#0\mathbin{;}t^{\prime}$ is not derivable from the axioms of $\mathrm{PGA^{isc}}$. If closed $\mathrm{PGA^{bc}}$ terms $t$ and $t^{\prime}$ represent instruction sequences in which no infinite chains of forward jumps occur, then $t=t^{\prime}$ is derivable from the axioms of $\mathrm{PGA^{sc}}$ only if $|t|=|t^{\prime}|$ is derivable from the axioms of $\mathrm{PGA^{isc}}$ and TE1–TE13.

If a closed $\mathrm{PGA^{bc}}$ term $t$ represents an infinite instruction sequence, then we can extract the approximations of the thread modeling the behaviour produced by that instruction sequence under execution up to every finite depth: for each $n\in\mathbb{N}$, there exists a closed $\mathrm{BTA}$ term $t^{\prime\prime}$ such that $\pi_{n}(|t|)=t^{\prime\prime}$ is derivable from the axioms of $\mathrm{PGA^{sc}}$, TE1–TE13, the axioms of $\mathrm{BTA}$, and PR1–PR4. If closed $\mathrm{PGA^{bc}}$ terms $t$ and $t^{\prime}$ represent infinite instruction sequences that produce the same behaviour under execution, then this can be proved using the following instance of AIP: $\bigwedge_{n\geq 0}\pi_{n}(|t|)=\pi_{n}(|t^{\prime}|)\mathrel{\,\Rightarrow\,}|t|=|t^{\prime}|$.

$\mathrm{PGA}$ instruction sequences are behaviourally equivalent if they produce the same behaviour under execution. Behavioural equivalence is not a congruence. Instruction sequences are behaviourally congruent if they produce the same behaviour irrespective of the way they are entered and the way they are left.

Let $t$ and $t^{\prime}$ be closed $\mathrm{PGA^{bc}}$ terms. Then:

• •

$t$ and $t^{\prime}$  are behaviourally equivalent,  written $t\mathrel{\equiv_{\mathsf{be}}}t^{\prime}$, if $|t|=|t^{\prime}|$ is derivable from the axioms of $\mathrm{PGA^{sc}}$, TE1–TE13, and the axioms of $\mathrm{BTA^{\infty}}$.

• •

$t$ and $t^{\prime}$ are behaviourally congruent, written $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$, if, for each $l,n\in\mathbb{N}$, $\#l\mathbin{;}t\mathbin{;}\mathord{!}^{n}\mathrel{\equiv_{\mathsf{be}}}\#l\mathbin{;}t^{\prime}\mathbin{;}\mathord{!}^{n}$.555We use the convention that $t\mathbin{;}{t^{\prime}}^{0}$ stands for $t$.

Behavioural congruence is the largest congruence contained in behavioural equivalence. Moreover, structural congruence implies behavioural congruence.

Proposition 3

For all closed $\mathrm{PGA^{bc}}$ terms $t$ and $t^{\prime}$, $t=t^{\prime}$ is derivable from the axioms of $\mathrm{PGA^{sc}}$ only if $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

Proof

The proof is analogous to the proof of Proposition 2.2 from [5]. In that proof use is made of the uniqueness of solutions of sets of recursion equations where each right-hand side is a $\mathrm{BTA}$ term of the form $\mathsf{D}$, $\mathsf{S}$ or $s\mathbin{\unlhd\hskip 1.49994pta\hskip 1.49994pt\unrhd}s^{\prime}$ with $\mathrm{BTA}$ terms $s$ and $s^{\prime}$ that contain only variables occurring as one of the right-hand sides. This uniqueness follows from AIP (see also Corollary 2.1 from [5]). ∎

Conversely, behavioural congruence does not implies structural congruence. For example, ${+}a\mathbin{;}\mathord{!}\mathbin{;}\mathord{!}\mathrel{\cong_{\mathsf{bc}}}{-}a\mathbin{;}\mathord{!}\mathbin{;}\mathord{!}$, but ${+}a\mathbin{;}\mathord{!}\mathbin{;}\mathord{!}={-}a\mathbin{;}\mathord{!}\mathbin{;}\mathord{!}$ is not derivable from the axioms of $\mathrm{PGA^{sc}}$.

5 Axioms of $\mathrm{PGA^{bc}}$ and Behavioural Congruence

The axioms of $\mathrm{PGA^{bc}}$ are intended to be used for establishing behavioural congruence in a direct way by nothing more than equational reasoning. Two questions arise: the soundness question, i.e. the question whether derivable equality implies behavioural congruence, and the completeness question, i.e. the question whether behavioural congruence implies derivable equality. The two theorems presented in this section concern these questions. The first theorem fully answers the soundness question in the affirmative. The second theorem answers the completeness question in the affirmative only for the restriction obtained by excluding the repetition operator because of problems in mastering the intricacy of a completeness proof for the unrestricted case.

We start with a few additional definitions and results which will be used in the proof of the theorems.

A closed $\mathrm{PGA^{bc}}$ term $t$ has simplifiable control flow if there exists a closed $\mathrm{PGA^{bc}}$ term $t^{\prime}$ such that $t=t^{\prime}$ is derivable from the axioms of $\mathrm{PGA^{isc}}$ and $t^{\prime}$ contains a subterm of the same form as the left-hand side of one of the axioms PGA9–PGA30. The intuition is that a closed $\mathrm{PGA^{bc}}$ term has simplifiable control flow if the instruction sequence that it represents has unnecessary tests, unnecessary jumps or needlessly long jumps. A closed $\mathrm{PGA^{bc}}$ term is in third canonical form if it is in second canonical form and does not have simplifiable control flow.

The following proposition relates $\mathrm{PGA^{bc}}$ and third canonical forms.

Proposition 4

For all closed $\mathrm{PGA^{bc}}$ terms $t$, there exists a closed $\mathrm{PGA^{bc}}$ term $t^{\prime}$ that is in third canonical form such that $t=t^{\prime}$ is derivable from the axioms of $\mathrm{PGA^{bc}}$.

Proof

By Proposition 2, there exists a closed $\mathrm{PGA^{bc}}$ term $t^{\prime\prime}$ that is in second canonical form such that $t=t^{\prime\prime}$ is derivable from the axioms of $\mathrm{PGA^{sc}}$. If $t^{\prime\prime}$ has simplifiable control flow, it can be transformed into a closed $\mathrm{PGA^{bc}}$ term that does not have simplifiable control flow by applications of PGA9–PGA30 possibly alternated with applications of PGA1 and/or PGA4. ∎

Proposition 4 is important to the proof of Theorem 5.2 below. Actually, there are some axioms among PGA9–PGA30 that did not turn up until the elaboration of the proof of Theorem 5.2.

The set of basic $\mathrm{PGA^{bc}}$ terms is inductively defined as follows:

• •

if $u\in\mathcal{I}$, then $u$ is a basic $\mathrm{PGA^{bc}}$ term;

• •

if $u\in\mathcal{I}$ and $t$ is a basic $\mathrm{PGA^{bc}}$ term, then $u\mathbin{;}t$ is a basic $\mathrm{PGA^{bc}}$ term; and

• •

if $t$ is a basic $\mathrm{PGA^{bc}}$ term, then $t^{\omega}$ is a basic $\mathrm{PGA^{bc}}$ term.

Obviously, for all closed $\mathrm{PGA^{bc}}$ terms $t$, there exists a basic $\mathrm{PGA^{bc}}$ term $t^{\prime}$ such that $t=t^{\prime}$ is derivable from PGA1.

Lemma 1

For all basic repetition-free $\mathrm{PGA^{bc}}$ terms $t$ that are in third canonical form, $t$ is of one of the following forms:

1. (a)

$u$, ${}\!\mathbin{;}t^{\prime}$ where $u\in\mathcal{I}$; 2. (b)

$u\mathbin{;}t^{\prime}$, where $u\in\mathcal{I}$ and $t^{\prime}$ is a basic repetition-free $\mathrm{PGA^{bc}}$ term that is in third canonical form.

Proof

This lemma with all occurrences of “third canonical form” replaced by “first canonical form” follows immediately from the definitions of basic $\mathrm{PGA^{bc}}$ term and first canonical form. Moreover, in the case that $t$ is of the form (b), it follows immediately from the definitions concerned that the properties “does not have chained jumps”,“has shortest possible jumps ending in the repeating part”, and “does not have simplifiable control flow” carry over from $t$ to $t^{\prime}$. This means that $t^{\prime}$ is also in third canonical form. ∎

In the rest of this section, we refer to the possible forms of basic $\mathrm{PGA^{bc}}$ terms that are in third canonical form as in Lemma 1.

Lemma 2

For all basic repetition-free $\mathrm{PGA^{bc}}$ terms $t$ and $t^{\prime}$ that are in third canonical form, $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ only if

1. (1)

$t$* is of the form (a) iff $t^{\prime}$ is of the form (a);* 2. (2)

$t$* is of the form (b) iff $t^{\prime}$ is of the form (b).*

Proof

Suppose that $t$ and $t^{\prime}$ are in third canonical form and $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

Property (1) is trivial because, in the case that $t$ is of the form (a), $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ iff $t\equiv t^{\prime}$.666We write $\equiv$ for syntactic identity.

Property (2) follows immediately from Lemma 1 and the consequence of property (1) that, in the case that $t$ is of the form (b), $t^{\prime}$ is not of the form (a). ∎

We now move on to the two theorems announced at the beginning of this section.

Theorem 5.1

For all closed $\mathrm{PGA^{bc}}$ terms $t$ and $t^{\prime}$, $t=t^{\prime}$ is derivable from the axioms of $\mathrm{PGA^{bc}}$ only if $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

Proof

Because $\mathrel{\cong_{\mathsf{bc}}}$ is a congruence, it is sufficient to prove for each axiom of $\mathrm{PGA^{bc}}$ that, for all its closed substitution instances $t=t^{\prime}$, $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$. For PGA1–PGA8, this follows immediately from Proposition 3. For PGA9–PGA30, it follows very straightforwardly from the definition of $\mathrel{\cong_{\mathsf{bc}}}$, TE1–TE13, and in the case of PGA17 and PGA18, the unfolding equation $X^{\omega}=X\mathbin{;}X^{\omega}$. ∎

Theorem 5.2

For all closed repetition-free $\mathrm{PGA^{bc}}$ terms $t$ and $t^{\prime}$, $t=t^{\prime}$ is derivable from the axioms of $\mathrm{PGA^{bc}}$ if $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

Proof

See Appendix 0.A. ∎

We will conclude Appendix 0.A by going into the main problem that we have experienced in mastering the intricacy of a proof of the unrestricted version of Theorem 5.2, which reads as follows:

for all closed $\mathrm{PGA^{bc}}$ terms $t$ and $t^{\prime}$, $t=t^{\prime}$ is derivable from the axioms of $\mathrm{PGA^{bc}}$ if $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

6 The Case of Instructions for Boolean Registers

In this section, we present the instantiation of $\mathrm{PGA^{bc}}$ in which all possible instructions for Boolean registers are taken as basic instructions. This instantiation is called $\mathrm{PGA_{br}^{bc}}$ ($\mathrm{PGA^{bc}}$ with instructions for Boolean registers). In order to justify the additional axioms of $\mathrm{PGA_{br}^{bc}}$, we also present the instantiation of $\mathrm{BTA}$ in which all possible instructions for Boolean registers are taken as basic actions and adapt the definitions of behavioural equivalence and behavioural congruence to closed $\mathrm{PGA_{br}^{bc}}$ terms using this instantiation of $\mathrm{BTA}$.

In $\mathrm{PGA_{br}^{bc}}$, it is assumed that a fixed but arbitrary set $\mathcal{F}$ of foci has been given. Foci serve as names of Boolean register services.

The set of basic instructions used in $\mathrm{PGA_{br}^{bc}}$ consists of the following:

• •

for each $f\in\mathcal{F}$ and $p,q\mathbin{:}\mathbb{B}\to\mathbb{B}$, a basic Boolean register instruction $f.p/q$.

We write $\mathcal{A}_{\mathrm{br}}$ for this set.

The intuition is that the execution of a basic Boolean register instruction may modify the register content of a Boolean register service and must produce a Boolean value as reply at its completion. The actual reply may be dependent on the register content of the Boolean register service. More precisely, the execution of a basic Boolean register instruction has the following effects:

• •

if the register content of the Boolean register service named $f$ is $b$ when the execution of $f.p/q$ starts, then its register content is $q(b)$ when the execution of $f.p/q$ terminates;

• •

if the register content of the Boolean register service named $f$ is $b$ when the execution of $f.p/q$ starts, then the reply produced on termination of the execution of $f.p/q$ is $p(b)$.

The execution of $f.p/q$ has no effect on the register content of Boolean register services other than the one named $f$.

$\mathbb{B}\to\mathbb{B}$, the set of all unary Boolean functions, consists of the following four functions:

• •

the function ${0}$, satisfying ${0}({0})={0}$ and ${0}({1})={0}$;

• •

the function ${1}$, satisfying ${1}({0})={1}$ and ${1}({1})={1}$;

• •

the function ${\hskip 1.1pt\mathrm{i}\hskip 1.1pt}$, satisfying ${\hskip 1.1pt\mathrm{i}\hskip 1.1pt}({0})={0}$ and ${\hskip 1.1pt\mathrm{i}\hskip 1.1pt}({1})={1}$;

• •

the function ${\hskip 0.29999pt\mathrm{c}\hskip 0.29999pt}$, satisfying ${\hskip 0.29999pt\mathrm{c}\hskip 0.29999pt}({0})={1}$ and ${\hskip 0.29999pt\mathrm{c}\hskip 0.29999pt}({1})={0}$.

In [7], we actually used the methods ${0}/{0}$, ${1}/{1}$, and ${\hskip 1.1pt\mathrm{i}\hskip 1.1pt}/{\hskip 1.1pt\mathrm{i}\hskip 1.1pt}$, but denoted them by $\mathsf{set}{:}0$, $\mathsf{set}{:}1$ and $\mathsf{get}$, respectively. In [8], we actually used, in addition to these methods, the method ${\hskip 0.29999pt\mathrm{c}\hskip 0.29999pt}/{\hskip 0.29999pt\mathrm{c}\hskip 0.29999pt}$, but denoted it by $\mathsf{com}$.

We write $\mathcal{I}_{\mathrm{br}}$ for the set $\mathcal{I}$ of primitive instructions in the case where $\mathcal{A}_{\mathrm{br}}$ is taken as the set $\mathcal{A}$.

The constants and operators of $\mathrm{PGA_{br}^{bc}}$ are the constants and operators of $\mathrm{PGA^{bc}}$ in the case where $\mathcal{I}_{\mathrm{br}}$ is taken as the set $\mathcal{I}$.

Closed $\mathrm{PGA_{br}^{bc}}$ terms are considered equal if the instruction sequences that they represent can always take each other’s place in an instruction sequence in the sense that the behaviour produced under execution remains the same under the intended interpretation of the instructions from $\mathcal{A}_{\mathrm{br}}$. In other words, equality of closed terms stands in $\mathrm{PGA_{br}^{bc}}$ for a kind of behavioural congruence of the represented instruction sequences. The kind of behavioural congruence in question will be made precise at the end of this section.

The axioms of $\mathrm{PGA_{br}^{bc}}$ are the axioms of $\mathrm{PGA^{bc}}$ and in addition the axioms given in Table 4.

In this table, $f$ stands for an arbitrary focus from $\mathcal{F}$, and $p$ and $q$ stand for arbitrary unary Boolean functions from $\mathbb{B}\to\mathbb{B}$.

If $t=t^{\prime}$ is derivable from the axioms of $\mathrm{PGA_{br}^{bc}}$, then $t$ and $t^{\prime}$ represent instruction sequences that can always take each other’s place in an instruction sequence without affecting the behaviour produced under execution in an essential way, taking the intended interpretation of the instructions from $\mathcal{A}_{\mathrm{br}}$ into account. Below, we introduce the instantiation of $\mathrm{BTA}$ in which all possible instructions for Boolean registers are taken as basic actions to make this precise.

Henceforth, the instruction sequences of the kind considered in $\mathrm{PGA_{br}^{bc}}$ are called $\mathrm{PGA_{br}}$ instruction sequences.

The instantiation of $\mathrm{BTA}$ referred to above is called $\mathrm{BTA_{br}}$ ($\mathrm{BTA}$ with instructions for Boolean registers). In $\mathrm{BTA_{br}}$, the effects of performing a basic action on both the register content of Boolean register services and the way in which the modeled behaviour proceeds subsequently to performing the basic action concerned correspond to the intended interpretation of the basic action when it is considered to be a basic instruction.

The constants and operators of $\mathrm{BTA_{br}}$ are the constants and operators of $\mathrm{BTA}$ in the case where $\mathcal{A}_{\mathrm{br}}$ is taken as the set $\mathcal{A}$.

The idea behind equality of $\mathrm{BTA_{br}}$ terms is that two closed $\mathrm{BTA_{br}}$ terms are equal if they represent threads that can be made the same by a number of changes that never influences at any step of the modeled behaviour the effects of the basic action performed on the register content of Boolean register services and the way in which the modeled behaviour proceeds. Equality of closed terms stands in $\mathrm{BTA_{br}}$ for a kind of congruence of the represented threads which originates from the notion of effectual equivalence of basic instructions introduced in [9].

The axioms of $\mathrm{BTA_{br}}$ are given in Table 5.

In this table, $f$ stands for an arbitrary focus from $\mathcal{F}$, and $p$ and $q$ stand for arbitrary unary Boolean functions from $\mathbb{B}\to\mathbb{B}$.

Like $\mathrm{BTA}$, we can extend $\mathrm{BTA_{br}}$ with the projection operators, the axioms for the projection operators and AIP. We write $\mathrm{BTA_{br}^{\infty}}$ for the resulting theory.

To make precise which behaviours are produced by $\mathrm{PGA_{br}}$ instruction sequences under execution, we combine $\mathrm{PGA_{br}^{bc}}$ with $\mathrm{BTA_{br}^{\infty}}$ and extend the combination with the thread extraction operator and the axioms for the thread extraction operator.

$\mathrm{PGA_{br}}$ instruction sequences are behaviourally equivalent if the behaviours that they produce under execution are the same under the intended interpretation of the instructions from $\mathcal{A}_{\mathrm{br}}$.

Let $t_{1}$ and $t_{2}$ be closed $\mathrm{PGA_{br}^{bc}}$ terms. Then:

• •

$t$ and $t^{\prime}$  are behaviourally equivalent,  written $t\mathrel{\equiv_{\mathsf{be}}}t^{\prime}$, if $|t|=|t^{\prime}|$ is derivable from the axioms of $\mathrm{PGA^{sc}}$, TE1–TE13, and the axioms of $\mathrm{BTA_{br}^{\infty}}$.

• •

$t$ and $t^{\prime}$ are behaviourally congruent, written $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$, if, for each $l,n\in\mathbb{N}$, $\#l\mathbin{;}t\mathbin{;}\mathord{!}^{n}\mathrel{\equiv_{\mathsf{be}}}\#l\mathbin{;}t^{\prime}\mathbin{;}\mathord{!}^{n}$.

It is obvious that, with this adapted definition of behavioural congruence, Theorem 5.1 goes through for closed $\mathrm{PGA_{br}^{bc}}$ terms and Theorem 5.2 goes through for closed repetition-free $\mathrm{PGA_{br}^{bc}}$ terms.

7 Concluding Remarks

In program algebra, three congruences on instruction sequences are paid attention to: instruction sequence congruence, structural congruence, and behavioural congruence. However, an axiom system for behavioural congruence had never been given. In this paper, we have given an axiom system for behavioural congruence and proved its soundness for closed terms and completeness for closed repetition-free terms. This means that behavioural congruence of finite instruction sequences can now be established in a direct way by nothing more than equational reasoning. In earlier work, it had to be established in an indirect way, namely via thread extraction, by reasoning that was not purely equational. It is an open question whether the axiom system is also complete for closed terms in the case where the closed terms considered are not restricted to the repetition-free ones.

Appendix 0.A Appendix

In this appendix, we outline the proof of Theorem 5.2. We do not give full details of the proof because the full proof is really tedious. We have aimed at providing sufficient information in the outline of the proof to make a reconstruction of the full proof a routine matter.

Proof of Theorem 5.2:

For all closed $\mathrm{PGA^{bc}}$ terms $s$, there exists a basic $\mathrm{PGA^{bc}}$ term $s^{\prime}$ such that $s=s^{\prime}$ is derivable from PGA1. Moreover, for all closed $\mathrm{PGA^{bc}}$ terms $s$ and $s^{\prime}$, $s=s^{\prime}$ is trivially derivable from the axioms of $\mathrm{PGA^{bc}}$ if $s\equiv s^{\prime}$. By these facts, Proposition 4, and Theorem 5.1, it is sufficient to prove:

for all basic repetition-free $\mathrm{PGA^{bc}}$ terms $t$ and $t^{\prime}$ that are in third canonical form, $t\equiv t^{\prime}$ if $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

We prove this by induction on the depth of $t$ and case distinction on the form of $t$ according to Lemma 1.

The case $t\equiv u$, for $u\in\mathcal{I}$, is trivial because $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ only if $t\equiv t^{\prime}$.

The case $t\equiv u\mathbin{;}s$, for $u\in\mathcal{I}$ and basic repetition-free $\mathrm{PGA^{bc}}$ term $s$ that is in third canonical form, is more involved. It follows immediately from Lemma 2 that in this case $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ only if $t^{\prime}\equiv u^{\prime}\mathbin{;}s^{\prime}$ for some $u^{\prime}\in\mathcal{I}$ and basic repetition-free $\mathrm{PGA^{bc}}$ term $s^{\prime}$ that is in third canonical form. Let $u^{\prime}\in\mathcal{I}$ and $s^{\prime}$ be a basic repetition-free $\mathrm{PGA^{bc}}$ term that is in third canonical form such that $t^{\prime}\equiv u^{\prime}\mathbin{;}s^{\prime}$. Then it follows immediately from the definition of $\mathrel{\cong_{\mathsf{bc}}}$ that $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ only if $s\mathrel{\cong_{\mathsf{bc}}}s^{\prime}$. Hence, by the induction hypothesis, we have that $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ only if $s\equiv s^{\prime}$. We proceed with a case analysis on $(u,u^{\prime})$. There exist 25 combinations of kinds of primitive instructions. In 9 of these combinations, it matters whether the basic instructions involved are the same and, in 1 of these combinations, it matters whether the natural numbers involved are the same. Hence, in total, there are 35 cases to consider. However, 5 cases are trivial because in those cases $u\equiv u^{\prime}$ and 13 cases are covered by a symmetric case. Of the remaining 17 cases, 9 cases contradict $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$. Left over are the following 8 cases: $(u,u^{\prime})=({+}a,a)$, $(u,u^{\prime})=({-}a,a)$, $(u,u^{\prime})=({+}a,{-}a)$, $(u,u^{\prime})=(\#l,{+}a)$, $(u,u^{\prime})=(\#l,{-}a)$, $(u,u^{\prime})=(\#l,a)$, $(u,u^{\prime})=(\#l,\#l^{\prime})$ with $l\neq l^{\prime}$, $(u,u^{\prime})=(\#l,\mathord{!})$. The proof now continues with a case analysis on $(s,s^{\prime})$ for each of these eight cases, using implicitly the above-mentioned fact that $s\equiv s^{\prime}$ each time that the conclusion is drawn that there is a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$. We will also implicitly use several times the easy to check fact that, for all basic repetition-free $\mathrm{PGA^{bc}}$ terms $r$ that are in third canonical form, $|r|\neq|\#l{+}2\mathbin{;}r|$ and $|r|\neq|u_{1}\mathbin{;}\ldots\mathbin{;}u_{k+1}\mathbin{;}r|$ if $u_{1}\equiv a$ or $u_{1}\equiv{+}a$ or $u_{1}\equiv{-}a$.

In the analysis for the case $(u,u^{\prime})=({+}a,a)$, we make a case distinction on the form of $s$ according to Lemma 1:

• •

in the case that $s\equiv v$, we make a further case distinction on the form of $v$:

• –

if $v\equiv b$ or $v\equiv{+}b$ or $v\equiv{-}b$, then we have $|{+}a\mathbin{;}v|\neq|a\mathbin{;}v|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• –

if $v\equiv\#0$, then we have $|{+}a\mathbin{;}v\mathbin{;}\mathord{!}|\neq|a\mathbin{;}v\mathbin{;}\mathord{!}|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• –

if $v\equiv\#1$, then $t$ is not in third canonical form;

• –

if $v\equiv\#l{+}2$, then we have $|{+}a\mathbin{;}v\mathbin{;}\mathord{!}|\neq|a\mathbin{;}v\mathbin{;}\mathord{!}|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• –

if $v\equiv\mathord{!}$, then we have $|{+}a\mathbin{;}v|\neq|a\mathbin{;}v|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• •

in the case that $s\equiv v\mathbin{;}r$, for some basic repetition-free $\mathrm{PGA^{bc}}$ term $r$ that is in third canonical form, we make a further case distinction on the form of $v$ as well:

• –

if $v\equiv b$ or $v\equiv{+}b$ or $v\equiv{-}b$, then we have $|{+}a\mathbin{;}v\mathbin{;}r|\neq|a\mathbin{;}v\mathbin{;}r|$, because $r$ is repetition-free, and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• –

if $v\equiv\#0$, then it follows from $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ that $r\equiv\#0$ or $r\equiv\#0\mathbin{;}r^{\prime}$ for some $r^{\prime}$ and hence $t$ is not in third canonical form;

• –

if $v\equiv\#1$, then $t$ is not in third canonical form;

• –

if $v\equiv\#l{+}2$, then we make a further case distinction on the form of $r$ according to Lemma 1:

in the case that $r\equiv w$, we make a further case distinction on the form of $w$:

• ·

if $w\equiv b$ or $w\equiv{+}b$ or $w\equiv{-}b$, then we have $|{+}a\mathbin{;}\#l{+}2\mathbin{;}w|\neq|a\mathbin{;}\#l{+}2\mathbin{;}w|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• ·

if $w\equiv\#0$, then we have $|{+}a\mathbin{;}\#l{+}2\mathbin{;}w\mathbin{;}\mathord{!}^{l{+}1}|\neq|a\mathbin{;}\#l{+}2\mathbin{;}w\mathbin{;}\mathord{!}^{l{+}1}|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• ·

if $w\equiv\#l^{\prime}{+}1$ and $l^{\prime}>l$, then we have $|{+}a\mathbin{;}\#l{+}2\mathbin{;}w\mathbin{;}\mathord{!}^{l{+}1}|\neq|a\mathbin{;}\#l{+}2\mathbin{;}w\mathbin{;}\mathord{!}^{l{+}1}|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• ·

if $w\equiv\#l^{\prime}{+}1$ and $l^{\prime}<l$, then we have $|{+}a\mathbin{;}\#l{+}2\mathbin{;}w\mathbin{;}\mathord{!}^{l^{\prime}{+}1}|\neq|a\mathbin{;}\#l{+}2\mathbin{;}w\mathbin{;}\mathord{!}^{l^{\prime}{+}1}|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• ·

if $w\equiv\#l^{\prime}{+}1$ and $l^{\prime}=l$, then $t$ is not in third canonical form;

• ·

if $w\equiv\mathord{!}$, then we have $|{+}a\mathbin{;}\#l{+}2\mathbin{;}w|\neq|a\mathbin{;}\#l{+}2\mathbin{;}w|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• *

in the case that $r\equiv w\mathbin{;}r^{\prime}$, for some basic repetition-free $\mathrm{PGA^{bc}}$ term $r^{\prime}$ that is in third canonical form, we make a further case distinction on the form of $w$ as well:

• ·

if $w\equiv b$ or $w\equiv{+}b$ or $w\equiv{-}b$, then we have $|{+}a\mathbin{;}\#l{+}2\mathbin{;}w\mathbin{;}r^{\prime}|\neq|a\mathbin{;}\#l{+}2\mathbin{;}w\mathbin{;}r^{\prime}|$, because $r^{\prime}$ is repetition-free, and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• ·

if $w\equiv\#0$, then it follows from $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ that $r^{\prime}\equiv w_{1}\mathbin{;}\ldots\mathbin{;}w_{l}\mathbin{;}\#0$ or $r^{\prime}\equiv w_{1}\mathbin{;}\ldots\mathbin{;}w_{l}\mathbin{;}\#0\mathbin{;}r^{\prime\prime}$ for some $r^{\prime\prime}$ and hence $t$ is not in third canonical form;

• ·

if $w\equiv\#l^{\prime}{+}1$ and $l^{\prime}\neq l$, then we have $|{+}a\mathbin{;}\#l{+}2\mathbin{;}w\mathbin{;}r^{\prime}|\neq|a\mathbin{;}\#l{+}2\mathbin{;}w\mathbin{;}r^{\prime}|$, because $r^{\prime}$ is repetition-free, and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• ·

if $w\equiv\#l^{\prime}{+}1$ and $l^{\prime}=l$, then $t$ is not in third canonical form;

• ·

if $w\equiv\mathord{!}$, then it follows from $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ that $r^{\prime}\equiv w_{1}\mathbin{;}\ldots\mathbin{;}w_{l}\mathbin{;}\mathord{!}$ or $r^{\prime}\equiv w_{1}\mathbin{;}\ldots\mathbin{;}w_{l}\mathbin{;}\mathord{!}\mathbin{;}r^{\prime\prime}$ for some $r^{\prime\prime}$ and hence $t$ is not in third canonical form;

• –

if $v\equiv\mathord{!}$, then it follows from $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ that $r\equiv\mathord{!}$ or $r\equiv\mathord{!}\mathbin{;}r^{\prime}$ for some $r^{\prime}$ and hence $t$ is not in third canonical form.

We conclude from this analysis that, in the case that $t\equiv{+}a\mathbin{;}s$ and $t^{\prime}\equiv a\mathbin{;}s$ for some basic repetition-free $\mathrm{PGA^{bc}}$ term $s$ that is in third canonical form, we have a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

The analyses for the cases $(u,u^{\prime})=({-}a,a)$ and $(u,u^{\prime})=({+}a,{-}a)$ are similar to the analysis for the case $(u,u^{\prime})=({+}a,a)$.

In the analysis for the case $(u,u^{\prime})=(\#l,a)$, we make a case distinction on $l$:

• •

if $l=0$, then we have $|\#l\mathbin{;}s|\neq|a\mathbin{;}s|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• •

if $l=1$, then we have $|\#l\mathbin{;}s|\neq|a\mathbin{;}s|$, because $s$ is repetition-free, and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• •

if $l=l^{\prime}+2$, then we make a further case distinction on the form of $s$ according to Lemma 1:

• –

in the case that $s\equiv v$, we have $|\#l\mathbin{;}s|\neq|a\mathbin{;}s|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• –

in the case that $s\equiv v\mathbin{;}r$, for some basic repetition-free $\mathrm{PGA^{bc}}$ term $r$ that is in third canonical form, it follows from $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ that $r\equiv v_{1}\mathbin{;}\ldots\mathbin{;}v_{l^{\prime}}\mathbin{;}a\mathbin{;}r^{\prime}$ for some basic repetition-free $\mathrm{PGA^{bc}}$ term $r^{\prime}$ that is in third canonical form and we make a further case distinction on the form of $v$:

if $v\equiv b$ or $v\equiv{+}b$ or $v\equiv{-}b$, then we have $|\#l^{\prime}{+}2\mathbin{;}v\mathbin{;}v_{1}\mathbin{;}\ldots\mathbin{;}v_{l^{\prime}}\mathbin{;}a\mathbin{;}r^{\prime}|\neq|a\mathbin{;}v\mathbin{;}v_{1}\mathbin{;}\ldots\mathbin{;}v_{l^{\prime}}\mathbin{;}a\mathbin{;}r^{\prime}|$, because $r^{\prime}$ is repetition-free, and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• *

if $v\equiv\#0$, then it follows from $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ that $r^{\prime}\equiv\#0$ or $r^{\prime}\equiv\#0\mathbin{;}r^{\prime\prime}$ for some $r^{\prime\prime}$ and hence $t$ is not in third canonical form;

• *

if $v\equiv\#l^{\prime\prime}{+}1$ and $l^{\prime\prime}\neq l^{\prime}+1$, then we have $|\#l^{\prime}{+}2\mathbin{;}v\mathbin{;}v_{1}\mathbin{;}\ldots\mathbin{;}v_{l^{\prime}}\mathbin{;}a\mathbin{;}r^{\prime}|\neq|a\mathbin{;}v\mathbin{;}v_{1}\mathbin{;}\ldots\mathbin{;}v_{l^{\prime}}\mathbin{;}a\mathbin{;}r^{\prime}|$, because $r^{\prime}$ is repetition-free, and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• *

if $v\equiv\#l^{\prime\prime}{+}1$ and $l^{\prime\prime}=l^{\prime}+1$, then $t$ is not in third canonical form;

• *

if $v\equiv\mathord{!}$, then it follows from $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ that $r^{\prime}\equiv\mathord{!}$ or $r^{\prime}\equiv\mathord{!}\mathbin{;}r^{\prime\prime}$ for some $r^{\prime\prime}$ and hence $t$ is not in third canonical form.

We conclude from this analysis that, in the case that $t\equiv\#l\mathbin{;}s$ and $t^{\prime}\equiv a\mathbin{;}s$ for some basic repetition-free $\mathrm{PGA^{bc}}$ term $s$ that is in third canonical form, we have a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

The analyses for the cases $(u,u^{\prime})=(\#l,{+}a)$ and $(u,u^{\prime})=(\#l,{-}a)$ are similar to the analysis for the case $(u,u^{\prime})=(\#l,a)$.

In the analyses for the cases $(u,u^{\prime})=(\#l,\#l^{\prime})$, with $l\neq l^{\prime}$, and $(u,u^{\prime})=(\#l,\mathord{!})$, we use the function $\mathrm{len}$, which assigns to each closed repetition-free $\mathrm{PGA^{bc}}$ term the length of the instruction sequence that it represents. This function is recursively defined as follows: $\mathrm{len}(u)=1$ and $\mathrm{len}(t\mathbin{;}t^{\prime})=\mathrm{len}(t)+\mathrm{len}(t^{\prime})$.

In the analysis for the case $(u,u^{\prime})=(\#l,\#l^{\prime})$ with $l\neq l^{\prime}$, we only consider the case $l<l^{\prime}$ (because the cases $l<l^{\prime}$ and $l>l^{\prime}$ are symmetric) and make a case distinction on $l$:

• •

if $l=0$, then we have $|\#0\mathbin{;}s|\neq|\#l^{\prime}\mathbin{;}s|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• •

if $0<l\leq\mathrm{len}(s)$, then it follows from $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ that $s\equiv u_{1}\mathbin{;}\ldots\mathbin{;}u_{l{-}1}\mathbin{;}a\mathbin{;}v_{1}\mathbin{;}\ldots\mathbin{;}v_{l^{\prime}{-}(l{+}1)}\mathbin{;}a\mathbin{;}r$ for some basic repetition-free $\mathrm{PGA^{bc}}$ term $r$ that is in third canonical form and we make a further case distinction on the form of $v$:

• –

if $v_{1}\equiv b$ or $v_{1}\equiv{+}b$ or $v_{1}\equiv{-}b$, then we have $|\#l\mathbin{;}u_{1}\mathbin{;}\ldots\mathbin{;}u_{l{-}1}\mathbin{;}a\mathbin{;}\linebreak[2]v_{1}\mathbin{;}\ldots\mathbin{;}v_{l^{\prime}{-}(l{+}1)}\mathbin{;}a\mathbin{;}r|\neq|\#l^{\prime}\mathbin{;}u_{1}\mathbin{;}\ldots\mathbin{;}u_{l{-}1}\mathbin{;}a\mathbin{;}v_{1}\mathbin{;}\ldots\mathbin{;}v_{l^{\prime}{-}(l{+}1)}\mathbin{;}a\mathbin{;}r|$, because $r$ is repetition-free, and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• –

if $v_{1}\equiv\#0$, then it follows from $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ that $r\equiv\#0$ or $r\equiv\#0\mathbin{;}r^{\prime}$ for some $r^{\prime}$ and hence $t$ is not in third canonical form;

• –

if $v_{1}\equiv\#l^{\prime\prime}{+}1$ and $l^{\prime\prime}\neq l^{\prime}-l$, then we have $|\#l\mathbin{;}u_{1}\mathbin{;}\ldots\mathbin{;}u_{l{-}1}\mathbin{;}a\mathbin{;}\linebreak[2]v_{1}\mathbin{;}\ldots\mathbin{;}v_{l^{\prime}{-}(l{+}1)}\mathbin{;}a\mathbin{;}r|\neq|\#l^{\prime}\mathbin{;}u_{1}\mathbin{;}\ldots\mathbin{;}u_{l{-}1}\mathbin{;}a\mathbin{;}v_{1}\mathbin{;}\ldots\mathbin{;}v_{l^{\prime}{-}(l{+}1)}\mathbin{;}a\mathbin{;}r|$, because $r$ is repetition-free, and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• –

if $v_{1}\equiv\#l^{\prime\prime}{+}1$ and $l^{\prime\prime}=l^{\prime}-l$, then $t$ is not in third canonical form;

• –

if $v_{1}\equiv\mathord{!}$, then it follows from $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ that $r\equiv\mathord{!}$ or $r\equiv\mathord{!}\mathbin{;}r^{\prime}$ for some $r^{\prime}$ and hence $t$ is not in third canonical form;

• •

if $l>\mathrm{len}(s)$, then we have $|\#0\mathbin{;}s\mathbin{;}\mathord{!}^{l{-}\mathrm{len}(s)}|\neq|\#l^{\prime}\mathbin{;}s\mathbin{;}\mathord{!}^{l{-}\mathrm{len}(s)}|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

We conclude from this analysis that, in the case that $t\equiv\#l\mathbin{;}s$ and $t^{\prime}\equiv\#l^{\prime}\mathbin{;}s$, with $l\neq l^{\prime}$, for some basic repetition-free $\mathrm{PGA^{bc}}$ term $s$ that is in third canonical form, we have a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

In the analysis for the case $(u,u^{\prime})=(\#l,\mathord{!})$, we make a case distinction on $l$:

• •

if $l=0$, then we have $|\#l\mathbin{;}s|\neq|\mathord{!}\mathbin{;}s|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$;

• •

if $0<l\leq\mathrm{len}(s)$, then it follows from $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$ that $s\equiv u_{1}\mathbin{;}\ldots\mathbin{;}u_{l{-}1}\mathbin{;}\mathord{!}$ or $s\equiv u_{1}\mathbin{;}\ldots\mathbin{;}u_{l{-}1}\mathbin{;}\mathord{!}\mathbin{;}r$ for some $r$ and hence $t$ is not in third canonical form;

• •

if $l>\mathrm{len}(s)$, then we have $|\#l\mathbin{;}s|\neq|\mathord{!}\mathbin{;}s|$ and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

We conclude from this analysis that, in the case that $t\equiv\#l\mathbin{;}s$ and $t^{\prime}\equiv\mathord{!}\mathbin{;}s$ for some basic repetition-free $\mathrm{PGA^{bc}}$ term $s$ that is in third canonical form, we have a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$.

From the conclusions of the analyses, it follows immediately that for all basic repetition-free $\mathrm{PGA^{bc}}$ terms $t$ and $t^{\prime}$ that are in third canonical form, $t\equiv t^{\prime}$ if $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$. ∎

We conclude this appendix by going into the main problem that we have experienced in mastering the intricacy of a proof of the generalization of Theorem 5.2 from all closed repetition-free $\mathrm{PGA^{bc}}$ terms to all closed $\mathrm{PGA^{bc}}$ terms.

In the proof of Theorem 5.2, case distinctions are made on a large scale. It frequently occurs that the number of cases to be distinguished is kept small by making use of Lemma 1. To devise and prove a generalization of this lemma that is not restricted to repetition-free terms is not a big problem. In the proof of Theorem 5.2, something of the following form occurs at many places: “we have $|s|\neq|s^{\prime}|$ because $r$ is repetition-free, and hence a contradiction with $t\mathrel{\cong_{\mathsf{bc}}}t^{\prime}$”. At several similar places in the proof of the generalization of this theorem, $r$ is not repetition-free and $|s|\neq|s^{\prime}|$ requires an elaborate proof. In some of these proofs, no use can be made of the generalization of Lemma 1 and one gets completely lost in the many deeply nested case distinctions. This is the main problem that we have experienced.