<figure><img src="image_1.png" /></figure>

HAL
open science

# Completeness of Seiller's Abstract Machine

Hong-Linh Anh-Ton Le, Pierre Valarcher

► To cite this version:

Hong-Linh Anh-Ton Le, Pierre Valarcher. Completeness of Seiller's Abstract Machine. 2025. hal-05137612

HAL Id: hal-05137612

https://hal.u-pec.fr/hal-05137612v1

Preprint submitted on 9 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Completeness of Seiller's Abstract Machine

Hong-Linh Anh-Ton Le

Pierre Valarcher

July 9, 2025

## Abstract

Developing a formal theory of algorithms remains a fundamental challenge in theoretical computer science ([7]). This paper investigates the equivalence between two fundamental algorithmic models: Gurevich's Abstract State Machines (ASMs) [11] and Seiller's Abstract Machine Configurations (AMCs) [19]. We establish that for each AMC (resp. ASM), we have an ASM (resp. AMC) whose computations are isomorphic to the ones of the AMC (resp. ASM). Specifically, we align Seiller's instruction-centric approach with Gurevich's structure-centric methodology, showing that each model can faithfully simulate the other. We draw on prior research on ASMs to develop our own findings on Seiller's model. This work contributes to the theoretical understanding of algorithmic equivalence and provides insights into the broader applicability of Seiller's model compared to Gurevich's.

## 1 Introduction

For a long time, many computational models (in this paper we consider only sequential models) have come to "improve" upon older models by trying to "fit" the specific problems of certain fields (for example, λ-calculus ([20], [1]) aims to directly link a program to the function being computed, Markov machines ([13]) modify the memory on which calculations can be performed) or to represent a "new manner" of programming that was not allowed in the previous model i.e. new algorithm. Each time, it is shown that the new models are as expressive as the old ones. However, these models are developed to provide a "convenience" that the older models weren't capable of, thus bringing an improvement more in algorithmic terms than in terms of denotational expressiveness.

In the mid-1980s, Y. Gurevich ([9, 10]) proposed formalizing these evolutions by seeking a computational model that is complete from an algorithmic point of view, that is, a model that allows for the integration (representation) of all possible "algorithmic improvements." This work was first called evolving algebra, which became the Abstract State Machines [11]. In parallel, Y. Moschovakis developed a theory of algorithms ([15, 17]) to address complexity questions about the notion of algorithm, abstracting from the notion of the machine on which it runs. This leads to profound results in lower bounds complexity [14, 21, 22, 16]. The two approaches have their strengths and limitations:
* Y. Gurevich's ASM (representing memory with first order structures and program by one step assembling language and one update instruction) has been used for specification and verification, but did not give many works on complexity classes (except in [3]) nor lower bounds complexity for classes of models (from our perspective, this is caused by the syntactic limitations of the language's control structures). Some other positive results have been developed in [6] and [8],

* Moschovakis' theory of algorithms has allowed many results on complexity but has more difficulty to encode and characterize models that are more imperative. In other words, this model is richer on control structures but less fine on memory control [17].

The two models are compared in [12]: both approaches use the same tool to represent arbitrary data structures. This allows ASMs to be represented as a recursive program and makes them compatible with the several results of lower bounds of complexity of Moschovakis and van den Dries.

For the past 5 years, a new model for representing algorithms has emerged: Seiller's Machine [19, 18]. It has the ambition to take the best of the two previous models: instructions are unlimited, memory is represented by configuration and programs are structured by graphs.

This work aims to rigorously compare Seiller's models of computation with those of Gurevich. We show that any algorithm derived from an ASM can be simulated step by step by a Seiller algorithm (AMC). Conversely, we show that any algorithm coming from (a subset of) the AMC model is simulated step by step by a specific ASM. The paper is organized as follows: section 2 is devoted to explaining the two models and following sections are dedicated to the proof of simulation.

We conclude by presenting the extensions that Seiller's algorithms could enable.

# 2 Models of algorithms

## 2.1 ASMs

Abstract State Machines were formalized by Yuri Gurevich as a first-order structure that evolves step by step, following a finite set of directives. We will slightly modify the original definition ([11]) without loss of generality:

* the vocabulary *Voc* will be allowed to be infinite (more details on this in the third part)

* the branching rule will be modified:
  if ... then ... `endif` will become if ... then ... `else ...endif`

* the par-rule will be modified: `par ... endpar` will become `seq ... endseq`. For example a rule `seq R₁; R₂ endseq` will be executed by first execut-
ing $R_1$ and then $R_2$. This modification won't change the class of ASMs
defined, but it will facilitate the proof.

* because of the previous point, we'll change update set to update sequence.

**Definition (ASM).** An ASM $M$ is defined by :

* a vocabulary **Voc** which is a set of symbols where each symbol has an arity.
Each element of the vocabulary is :

- either a static function : a function that is not going to change during
the execution

- or a dynamic function : a function that can change during the execution

* a set of states **States**, where each element is a first-order structure of vocabulary **Voc**: a state will have the form $s = (\mathbf{Base}, \mathbf{Voc}^s)$ where

- **Base** is a set

- $\mathbf{Voc}^s$ is a set of function : for each symbol $f$ in $\mathbf{Voc}$ of arity $n$, we
have that $f^s$ is a function of $\mathbf{Voc}^s$ of signature $\mathbf{Base}^n \rightarrow \mathbf{Base}$

* a program : **Prog** of vocabulary **Voc**, the grammar is defined below

*Remark.* The distinction between dynamic and static function is not fundamen-
tally important for the concept of ASM and it will be ignored in Section 4 as
every function can just be considered a dynamic function.

From a vocabulary $\mathbf{Voc} = \{f_1, \dots, f_n\}$, a state $s$ of vocabulary $\mathbf{Voc}$ is of
the form $(X, f_1^s, \dots, f_n^s)$ where $X$ is a set and each function $f_i^s$ has a signature
$X^n \to X$ where $n$ is the arity of $f_i$. $X$ serves as a declaration of the types the
algorithm is going to manipulate. Static function serves as primitive operation
(like + or -) and dynamic function serves as a memory (like the tape of a Turing
machine). As Gurevich says in [11], each dynamic function is a memory where
the input is to be seen as an address and the output as the value contained at
this address : for example, a tape of a Turing machine will be a unary function
taking a position as an input and returning the value at that position.

The way ASMs modify their state is done through updates.

**Definition (Update).** An update is a triplet $(f, (a_1, \dots, a_n), a_0)$ where $f \in \mathbf{Voc}^{n-ary}, a_0, \dots, a_n \in \mathbf{Base}$.

An update sequence is a list of updates or another element called **stop**, the
constructor for the list will be noted ::.

An update $(f, (a_1, \dots, a_n), a)$ act on a state $s$ by modifying the function $f^s$: the modified function is such that $(a_1, \dots, a_n) \mapsto a$ and all other part of the function remain unchanged for example the transition of a 1-taped Turing machine will be of the form $(\mathbf{tape}, p, s)$ where $p$ is the current position of the head and $s$ is the new symbol that will replace the old one.
**Definition (Update execution).** Let $s$ be a state. The execution of an update $u = (f, \vec{a}, a)$ on $s$ gives a new state that we will write $s \triangleleft u$ such that : for each $g \in \text{Voc}$ of arity $k$ and each $k$-tuple $\vec{b}$

$$g^{s \triangleleft u}(\vec{b}) = \begin{cases} a & \text{if } \vec{a} = \vec{b} \text{ and } f = g \\ g^s(\vec{b}) & \text{else} \end{cases}$$

We extend this to update sequences : for $u$ an update and $l$ an update sequence

* $s \triangleleft \epsilon = s$

* $s \triangleleft l :: u = (s \triangleleft l) \triangleleft u$

The question is then how do we extract from the states the value necessary to construct updates ? With terms of vocabulary $\text{Voc}$ and their valuation (in the state).

**Definition ((Closed) Term).** A term $t$ (of vocabulary $\text{Voc}$) is defined by induction on :

* $c$ where $c$ is a function symbol of $\text{Voc}$ of arity 0

* $f(t_1, \dots, t_n)$ where $f$ is a function symbol of $\text{Voc}$ of arity $n$

**Definition (Valuation of a term: $[]$).** Let $s = \{\text{Base}, \text{Voc}^s\}$ be a state. $[]_s$ is defined by induction on $\text{Voc}$-term by :

* $c \mapsto c^s$ where $c$ is a symbol of arity 0

* $f(t_1, \dots, t_n) \mapsto f^s([t_1]_s, \dots, [t_n]_s)$ where $f$ is a symbol of arity $n$ and $t_1, \dots, t_n$ are $\text{Voc}$-terms

Programs of ASM are slightly different to usual programs : they are meant to only describe one transition. Most of the time, a program will describe the execution as a whole : the model will follow the program line by line, each one of them being (approximately) one transition / step of the execution.

**Definition (Program).** Let $\text{Voc}$ be a vocabulary. A program (or rule) $\text{Prog}$ (of vocabulary $\text{Voc}$) is defined by induction on :

* **upd-rule** : $f(t_1, \dots, t_n) := t_0$ where $f \in \text{Voc}$ of arity $n$ and $t_0, \dots, t_n$ are closed $\text{Voc}$-terms

* **seq-rule** : $\text{seq } R_1; \dots; R_n$ endseq where $R_1, \dots, R_n$ are $\text{Voc}$-rules

* **if-rule** : if $\varphi$ then $R_1$ else $R_2$endif where $\varphi$ is a closed $\text{Voc}$-term and $R_1, R_2$ are $\text{Voc}$-rules

*Remark.* When writing multiline programs, we'll omit `endseq` and `endif`: instead we'll use the indentation to mark the block of rules contained in each rule.
**Definition** (Update sequence of a program : []). Let $s$ be a state. We define the update sequence of a program on a state, noted []$_s$, by:

• $f(t_1, \dots, t_n) := t_0 \mapsto (f, ([t_1]_s, \dots, [t_n]_s), [t_0]_s)$

• par $R_1; \dots; R_n$ endpar $\mapsto [[R_1]]_s :: \dots :: [[R_n]]_s$

• if $\varphi$ then $R_1$ else $R_2$ endif $\mapsto$
$$
\begin{cases}
[[R_1]]_s & \text{if } [\varphi]_s = \text{true} \\
[[R_2]]_s & \text{else}
\end{cases}
$$

**Definition** (Execution of a program : ◁). Let $\mathbf{Voc}$ be a vocabulary and $s$ be a state of vocabulary $\mathbf{Voc}$. We define the execution of a program $\mathbf{Prog}$ on a state $s$, noted $s \triangleleft \mathbf{R}$, as :

$$s \triangleleft \mathbf{Prog} = s \triangleleft [[\mathbf{Prog}]_s]$$

**Definition** (Computation for an ASM). A computation (for an ASM) is a sequence that starts from an initial state and where we get from one state to the next with one execution of the program : i.e.

$$s_0 \rightarrow s_1 \rightarrow s_2 \rightarrow \dots$$

where $s_0 \in \text{Init}$ and $s_{i+1} = s_i \triangleleft \text{Prog}$ for each $i \in \mathbb{N}$

*Remark.* Note that each execution of an ASM is infinite. This may pose a problem when trying to compare it to AMCs that have computation that can stop. To mitigate the absence of proper termination, we use a similar encoding to the one Gurevich used in [5] : in case of the termination of the computation, we'll arrive to some recognizable states that are also fixed points (this will be developed in Section 3).

An example of an ASM, *ea1*, is given in Appendix A

## 2.2 AMC and $\alpha$-machines

AMCs (and $\alpha$-machines) were introduced by Thomas Seiller as a framework for representing models of computation. While they do not encompass his (complete) notion of algorithms, they capture an aspect of it. The following definition is largely based on [19].

An AMC consists of a set of configurations and a set of instructions that act on these configurations. The instructions themselves are simply symbols; it is the action $\alpha$ that provides their semantic interpretation.

**Definition** (AMC). An AMC $\alpha$ is :

• $\mathcal{X}$ : a set of configurations

• $I$ : a set of instructions (that can and will usually be infinite)

• $\alpha : \mathbb{M}(I) \times \mathcal{X}$ : a monoid action of the free monoid $\mathbb{M}(I)$ on $\mathcal{X}$

Compared to the ASM approach :
* X is equivalent to the dynamic part of the ASM-state

* I and α may be seen, in a first time, as the static part of the ASM-state

Here, there is a formal distinction between the “static” part of the machine and the “dynamic” part. In Gurevich’s approach there is no formal distinction and aside from stating the kind of function they are, nothing differentiate them.

To fully define models of computation in Seiller framework we need to add a notion of programs. However, as Th. Seiller said in [19], "some will view this notion of model of computation too general" : this will be the case for this article. For this article we’ll limit ourselves to **deterministic machines** with a **finite program**.

α-machines are AMCs with a program. This program takes the form of a graph where nodes are labeled with symbols called states (different from the ones of ASMs) and edges labeled with sequences of instructions.

**Definition (α-machine).** An α-machine P is :

* $S^P$: a (finite) set of state, containing a special element **end**

* $E^P$: a set of edges (finite)

* $P = \{(m_e, i_e \to f_e) \mid e \in E^P, m_e \in \mathbb{M}(I), i_e, f_e \in S^P \setminus \{\text{end}\} \}$ (finite) : the machine

*Remarks.*

* $(m, i \to f)$ is a notation, it should be seen as a triplet $(m, i, f)$. It represent a possible transition from a state $i$ to a state $f$ by executing $m$

* We won't use the set of edges $E^P$ later on. Instead of writing $\exists e \in E^P$, $(m_e, i_e \to f_e) \in P$, we'll write $\exists (m, i \to f) \in P$.

* There is no edges coming from/going to **end**: the state is here to catch terminating computations.

From a node $s$ and a configuration $x$, we determine the edge(s) that we can take by looking at each edge $(m, s \to f)$ with starting node $s$ and checking if $\alpha(m)(x) \downarrow$ or not : if it is, the edge is a possible transition. That makes general $\alpha$-machine an inherently non-deterministic model, so we need an additional property to characterize deterministic $\alpha$-machines.

**Definition (Deterministic α-machine).** A deterministic α-machine $P$ is an α-machine that verifies :

$$ \forall (s, x) \in S^P \times X, \quad \exists^{\leq 1} (m, i \to f) \in P \text{ s.t. } i = s \land \alpha(m)(x) \downarrow $$

*Remark.* The absence of an edge verifying the previous property means the termination of the computation.
The previous definition gives the existence of an edge that verify the property : we'll call it the transition edge and note it "te" :

**Definition (Transition edge : te).** Let $P$ be a deterministic $\alpha$-machine. For a pair $(s, x) \in S^P \times X$, if it exists, we call its transition edge the only labeled edge $(m, i \to f) \in P$ such that $i = s$ and $\alpha(m_e)(x)$ and we note it $te_P(s, x)$ If it doesn't exists, we note $te_P(s, x) \downarrow$

Once we have a deterministic $\alpha$-machine, we can define a transition function of this machine : that is the function that either takes each times the only possible edge to transition or stops.

**Definition ($\tau_P$).** Let $\alpha : \mathbb{M}(I) \rightsquigarrow \mathbb{X}$ be an AMC and $P$ be a deterministic $\alpha$-machine. We define $\tau_P : S^P \times \mathbb{X} \cup \{\perp\} \to S^P \times \mathbb{X} \cup \{\perp\}$ such that

$$ \forall (s, x) \in S^P \times X, \tau^P(s, x) = \begin{cases} (\text{end}, \perp) & \text{if } te_P(s, x) \downarrow \\ (te_{P3}(s, x), \alpha(te_{P1}(s, x))(x)) & \text{else} \end{cases} $$

And $\tau_P(\text{end}, \perp) = (\text{end}, \perp)$

*Remark.* The $(\text{end}, \perp)$ element here represent the end of a computation. Instead of having the transition function be a partial function in the case of termination, end and $\perp$ where added to signifies the end of computation.

We can then define a computation as - starting from an initial state and configuration - the sequence that successively apply $\tau^P$, the transition function.

**Definition (AMC-Computation).** For a deterministic $\alpha$-machine $P$, an computation of $P$ on $(s, x)$ is a sequence :

$$ (s, x) = c_0 \to c_1 \to c_3 \to \dots $$

such that

$$ \forall i \in \mathbb{N}, \quad \tau^P(c_i) = c_{i+1} $$

An example of an AMC, ea2, is given in Appendix B

## 3 AMCs to ASMs

This section and the next shows a correspondence between ASM and AMC (or rather $\alpha$-machine). This correspondence works in 2 parts: on one hand, an AMC is equivalent to the core of an ASM: its base set, its vocabulary along with its states, and on the other hand, an $\alpha$-machine is equivalent to an entire ASM; in particular, $P$ is equivalent to Prog. For the remainder of this section, we assume the existence of an AMC $\alpha : \mathbb{M}(I) \rightsquigarrow \mathbb{X}$ and a deterministic $\alpha$-machine $P$. The objective now is to define an ASM that will be "equivalent" to $P$.
## 3.1 The core of the ASM

Let's first give this core of the ASM.

**Definition.**

* Base set: $\text{Base}_P = \mathbb{X} \cup \{\perp\} \cup S^P$.
These are all the elements that we will manipulate. As defined in Def.2.2, the element $\perp$ serves as a recognizable configuration for termination. While $S^P$ does not appear in the definition of an AMC, it is still an element we manipulate during transitions.

* Vocabulary: $\text{Voc}_P = \{\text{state}, \text{config}\} \cup I$ where both state,config are 0-ary, dynamic and each $i \in I$ is unary static function.
state will contain an element of $S^P$ representing the current state, and
config will contain an element of $\mathbb{X} \cup \perp$ representing the current configuration. The functions in $I$ are static functions that correspond (mostly) to the instructions of the AMC.

* Static functions: $\forall i \in I, i: x \mapsto \begin{cases} \alpha(i)(x) & \text{if } x \in \mathbb{X} \wedge \alpha(i)(x) \downarrow \\ \perp & \text{else} \end{cases}$

* States: $\text{States}_P = \{s = (\text{Base}_P, I, \text{state}^s, \text{config}^s) \mid \text{state}^s \in S^P, \text{config} \in \mathbb{X}\}$

The set of states in this formalization consists of exactly those elements previously enumerated in the preceding points, with each state representing a distinct configuration of the system as described above.

Our next objective is to translate the AMC-graph into an ASM-program. We will do so by translating each basic component of the graph into the corresponding component of the formalism of ASMs. We will then assemble those components back into a program.

A central component of each edge in $P$ is its sequence of instructions. We translate sequences of instruction to term of vocabulary $\text{Voc}_P$ by mapping sequentialization of instruction to composition of the corresponding instruction-function

**Definition** ($\text{tr}_I$). $\text{tr}_I$ is defined by induction on update sequences:

* $\epsilon \mapsto \text{config}$

* $m; i \mapsto i(\text{tr}_I(m))$

**Proposition 1.** Let $m \in \mathbb{M}(I)$, $x \in \mathbb{X}$. We have:

* $\alpha(m)(x) \uparrow \Rightarrow \forall s \in S^P, [\text{tr}_I(m)]_{\text{st}(s,x)} = \perp$

* $\alpha(m)(x) \downarrow \Rightarrow \forall s \in S^P, [\text{tr}_I(m)]_{\text{st}(s,x)} = \alpha(m)(x)$

*Proof.* We will prove it by induction on $m$. Let $x \in \mathbb{X}$ and $s \in S^P$:
• $\epsilon: \alpha(\epsilon)(x) = x$, by definition, $[\mathrm{tr}_I(\epsilon)]_{\mathrm{st}(s,x)} = [\mathrm{config}]_{\mathrm{st}(s,x)} = x$

• $m; i$: We suppose that

$$ - \alpha(m)(x) \uparrow \Rightarrow \forall s \in S^P, [\mathrm{tr}_I(m)]_{\mathrm{st}(s,x)} = \perp \quad (1) $$

$$ - \alpha(m)(x) \downarrow \Rightarrow \forall s \in S^P, [\mathrm{tr}_I(m)]_{\mathrm{st}(s,x)} = \alpha(m)(x) \quad (2) $$

Reminder : $\alpha(m;i)(x) = \alpha(i)(\alpha(m)(x))$

- Suppose that $\alpha(m;i)(x) \uparrow$, then

* either $\alpha(m)(x) \uparrow$, then (by (1)) $[\mathrm{tr}_I(m)]_{\mathrm{st}(s,x)} = \perp$ and so : $[\mathrm{tr}_I(m;i)]_{\mathrm{st}(s,x)} = i([\mathrm{tr}_I(m)]_{\mathrm{st}(s,x)}) = i(\perp) = \perp$

* or $\alpha(m)(x) \downarrow$ and $\alpha(i)(\alpha(m)(x)) \uparrow$, then (by (2)) $[\mathrm{tr}_I(m)]_{\mathrm{st}(s,x)} = \alpha(m)(x)$ and so : $[\mathrm{tr}_I(m;i)]_{\mathrm{st}(s,x)} = i([\mathrm{tr}_I(m)]_{\mathrm{st}(s,x)}) = i(\alpha(m)(x)) = \perp$ by def. of $i$

- Suppose that $\alpha(m;i)(x) \downarrow$, then $\alpha(m)(x) \downarrow$ and $\alpha(i)(\alpha(m)(x)) \downarrow$

* by (2), we have that $[\mathrm{tr}_I(m)]_{\mathrm{st}(s,x)} = \alpha(m)(x)$

* we have that $[\mathrm{tr}_I(m;i)]_{\mathrm{st}(s,x)} = i([\mathrm{tr}_I(m)]_{\mathrm{st}(s,x)}) = i(\alpha(m)(x)) = \alpha(i)(\alpha(m)(x)) = \alpha(m;i)(x)$

□

According to Def.2.2, a transition from a state-configuration pair $(s, x)$ is determined through a two-phase process. First, we must identify the appropriate edge from the set of possible transitions: we examine all edges originating from state $s$ and search for an edge, if one exists, whose sequence of instructions is well-defined on configuration $x$. We will keep this process of determining the transition in the translated program.

The function $\mathrm{Node}_P$ maps each state to its set of outgoing edges. More formally, given a state $s$, $\mathrm{Node}_P(s)$ returns the collection of all edges that have $s$ as their source state. This function effectively characterizes the local transition structure of our system by identifying all possible transitions that could be taken from any given state. In the context of our state transition system, this mapping allows us to determine the set of potential next transitions at each step of computation.

**Definition** ($\mathrm{Node}_P$).

$\mathrm{Node}_P : S^P \to \mathcal{P}(P)$

$$ s \mapsto \{(m, i \to f) \in P \mid i = s\} $$

Once we have a set of edges we can transition from, the goal is to determine which is the transition edge and do the transition. We sequentialize this verification so that, if no transition edge is found, we "stop" the computation.

**Definition** ($\mathrm{tr}_{\mathrm{node}}$). $\mathrm{tr}_{\mathrm{node}}$ is going to be defined by induction on the size of a set of edges :
• $\{\} \mapsto \text{seq}$

config := $\perp$

state := end

• $\{(m_1, i_1 \to f_1), \dots, (m_n, i_n, f_n)\} \mapsto \text{if } \text{tr}_I(m) \neq \perp \text{ then}$

config := tr_I(m)

state := f

else

tr_edges({(m_2, i_2 \to f_2), \dots, (m_n, i_n, f_n)})

**Proposition 2.** Let $E = \{(m_1, i \to f_1), \dots, (m_n, i \to f_n)\}$ be a set of edges of $P$ (that share the same starting state), $x$ be in $X$ and $s = (\text{Base}_P, I, i, x)$ If the transition edge $(m, s \to f)$ is in this set, then $[[\text{tr}_{\text{node}}(E)]]_s = (\text{config}, \emptyset, \alpha(m)(x)) :: (\text{state}, \emptyset, f)$ otherwise $[[\text{tr}_{\text{node}}(E)]]_s = (\text{config}, \emptyset, \perp) :: (\text{state}, \emptyset, \text{end})$

*Proof.* There are 2 cases :

• The transition edge is in this set. By induction on $n$, the size of the set of edges :

- $l = 1$: because $\text{Node}_P$ has only 1 element, $\text{te}_P(s, x) = (m_1, i \to f_1)$. By definition of deterministic $\alpha$-machine, we have $\alpha(m_1)(x) \downarrow$ so, by Prop.1, $[\text{tr}_I(m_1) \neq \perp]_s = \text{true}$. Therefore $[[\text{tr}_{\text{node}}(E)]]_s = (\text{config}, \emptyset, \alpha(m)(x)) :: (\text{state}, \emptyset, f)$

- $l$: we have 2 cases

* $\text{te}_P(s, x) = (m_1, i \to f_1)$ : same justification as previously

* $\text{te}_P(s, x) = (m_i, i \to f_i)$ with $i \ge 2$: we use the I.H. on $\{(m_2, s \to f_2), \dots, (m_n, s \to f_n)\}$

• The transition edge is not in this set or there is no transition edge. By induction on $n$ the size of the set of edges :

- $l = 0$: $[[\text{tr}_{\text{node}}(E)]]_s = (\text{config}, \emptyset, \perp) :: (\text{state}, \emptyset, \text{end})$

- $l$: we have $\alpha(m_1)(x) \uparrow$ so, by Prop.1, $[\text{tr}_I(m_1) \neq \perp]_s = \text{false}$ so $[[\text{tr}_{\text{node}}(E)]]_s = [[\text{tr}_{\text{node}}(\{(m_2, s \to f_2), \dots, (m_n, s \to f_n)\})]]_s$ and by the induction hypothesis, because the transition edge is not in $\{(m_2, s \to f_2), \dots, (m_n, s \to f_n)\}$, we have that $[[\text{tr}_{\text{node}}(\{(m_2, s \to f_2), \dots, (m_n, s \to f_n)\})]] = (\text{config}, \emptyset, \alpha(m)(x)) :: (\text{state}, \emptyset, f)$

□

The program will then determine which node we are in and how we transition from it.
**Definition (Prog<sub>P</sub>).**

First, we order $S^P: s_1 < s_2 < \dots < s_k$. We then define Prog<sub>P</sub> as :

$\mathbf{Prog}_P = \mathbf{seq}$

$$
\begin{align*}
\mathbf{if} \ state &= s_1 \ \mathbf{then} \\
&\quad \mathrm{tr}_{\mathrm{node}}(\mathrm{Node}_P(s_1)) \\
\mathbf{if} \ state &= s_2 \ \mathbf{then} \\
&\quad \mathrm{tr}_{\mathrm{node}}(\mathrm{Node}_P(s_2)) \\
\dots \\
\mathbf{if} \ state &= s_k \ \mathbf{then} \\
&\quad \mathrm{tr}_{\mathrm{node}}(\mathrm{Node}_P(s_k))
\end{align*}
$$

*Remark.* We hid the *else* part of the *if*-rules as they just contain an empty *seq*-rule.

**Definition** (*M*<sub>*P*</sub>). *M*<sub>*P*</sub> is the ASM defined by :

• the states : States<sub>P</sub>

• the vocabulary : Voc<sub>P</sub>

• the program : Prog<sub>P</sub>

For the equivalence, we'll need a way to go from AMC-configuration to
ASM-states.

**Definition (st).**

$$
\mathbf{st} : \begin{array}{l} S^P \times \mathbb{X} \cup \{\perp\} \\ (s, x) \end{array} \rightarrow \begin{array}{l} \mathbf{States}_P \\ (X, I, s, x) \end{array}
$$

aaaaaaaa

**Theorem 1.** Let $(s_0, x_0) \dashv_P (s_1, x_1) \dashv_P \dots$ be a computation of $P$. We have
that :

$$
\mathbf{st}(s_0, x_0) \dashv_{M_P} \mathbf{st}(s_1, x_1) \dashv_{M_P} \dots
$$

is a computation of $M_P$

The proof for this theorem is done by induction on the following proposition.

**Proposition 3.**

$$
\text{Let } (s, x) \in S^P \times X \cup \{\perp\}
$$

$$
\mathbf{st}(s, x) \triangleleft \mathbf{Prog}_P = \mathbf{st}(\tau^P(s, x))
$$

*Proof.* Let $(s, x) \in S^P \times \mathbb{X} \cup \{\perp\}$. For the rest of this proof : we will shorten $[[\mathbf{st}(s,x)]$ as $[[], [[\mathbf{st}(s,x)]$ as $[]$ and we'll enumerate Node<sub>P</sub>(s) as $\{(m_1, s \to f_1), \dots, (m_l, s \to f_l)\}$. First, for each $i$, if $s = s_i$ then $[\mathbf{state} = s_i] = \mathbf{true}$ otherwise $[\mathbf{state} = s_i] = \mathbf{false}$, so we have that $[\mathbf{Prog}_P] = \mathrm{tr}_{\mathrm{node}}(\mathrm{Node}_P(s))$. Now, there are 2 cases :
* the transition edge does not exists : $te_P(s, x) \uparrow$. In that case $\tau_P(s, x) = (\text{end}, \perp)$. For $\text{Prog}_P$ : by Prop.2 $\text{tr}_{\text{node}}(\text{Node}_P(s)) = (\text{config}, \emptyset, \perp) :: (\text{state}, \emptyset, \text{end})$. So $\text{st}(s, x) \triangleleft \text{Prog}_P = \text{st}(s, x) \triangleleft \text{tr}_{\text{node}}(\text{Node}_P(s)) = \text{st}(s, x) \triangleleft (\text{config}, \emptyset, \perp) :: (\text{state}, \emptyset, \text{end}) = \text{st}(s, \perp) \triangleleft (\text{state}, \emptyset, \text{end}) = \text{st}(\text{end}, \perp)$

* the transition edge exists : we'll note $(m, s \to f) = te_P(s, x)$. By definition, $\tau^P(s, x) = (f, \alpha(m)(x))$. For $\text{Prog}_P$ : by Prop.2 $\text{tr}_{\text{node}}(\text{Node}_P(s)) = (\text{config}, \emptyset, \alpha(m)(x)) :: (\text{state}, \emptyset, f)$. So $\text{st}(s, x) \triangleleft \text{Prog}_P = \text{st}(s, x) \triangleleft \text{tr}_{\text{node}}(\text{Node}_P(s)) = \text{st}(s, x) \triangleleft (\text{config}, \emptyset, \alpha(m)(x)) :: (\text{state}, \emptyset, \emptyset) = \text{st}(s, \alpha(m)(x)) \triangleleft (\text{state}, \emptyset, f) = \text{st}(f, \alpha(m)(x))$

<figure><img src="image_3.png" /></figure>

An example is given in Appendix B

# 4 ASM to AMC

Now our goal is to show a way to represent ASMs with AMCs.

## 4.1 The AMC

In [19], Seiller gives an AMC that is supposed to represent ASM. One problem arise when trying to translate an ASM to a corresponding $\alpha$-machine : we need to have a way to remember the valuation of some terms before we transition. Take for example the simple program :

seq

a := b

b := a

where a and b are 0-ary. By the definition given in Section 2, the semantic of this program will be to swap the values of a and b. However, the form of the AMC given by Seiller only allows us to "fire" updates lazily : it results in a program that copies the value of b in a.

The following AMC aim to fix this problem by having an additional state that will store the state "before transition". It will come with a new instruction.

For the rest of this section, we'll assume the existence of an ASM M.

**Definition ($\alpha_M$).** The AMC is defined by :

* $X_M = \text{States} \times \text{States}$ : the first state will be called current-state and the second one copy-state
* $I_M = \text{Upd} \cup \text{Test} \cup \{\text{copy}\} :$
  - $\text{Upd} = \{\text{update}(f(t_1, \dots, t_n) \leftarrow t_0) \mid f \in \Upsilon\text{n-ary}, t_0, \dots, t_n \in \Upsilon\text{-terms}\}$
  - $\text{Test} = \{\text{test}(t) \mid t \in \Upsilon\text{-term}\}$

* $\alpha_M : \mathbb{M}(I_M) \mathrel{\frown} \mathbb{X}_M$
  - $\text{copy} : (s_1, s_2) \mapsto (s_1, s_1)$
  - $\text{update}(R) : (s_1, s_2) \mapsto (s_1 \triangleleft [[R]]_{s_2}, s_2)$
  - $\text{test}(\varphi) : (s_1, s_2) \mapsto \begin{cases} (s_1, s_2) & \text{if } [[\varphi]]_{s_2} = \text{true} \\ \uparrow & \text{else} \end{cases}$

## 4.2 The $\alpha$-machine of an ASM

The process will be similar to the one of Section 3. However, while we tried to maintain (to some extent) the "shape" of the $\alpha$-machine, ASM-programs do not have much external structure : the structure of the program only describe how a transition is organized and not how the execution is organized. The result is that the equivalent $\alpha$-machine will lack a lot of structure, having only 1 state (other than end).

We'll introduce some operation on set of sequences of instructions :

* For two sets $E_1, E_2 \in \mathcal{P}(\mathbb{M}(I))$
  $E_1; E_2 =_{\text{def.}} \{m_1; m_2 \mid m_1 \in E_1, m_2 \in E_2\}$

* For an instruction $i \in I$, $E \subseteq \mathcal{P}(\mathbb{M}(I))$
  $i; E =_{\text{def.}} \{i; m \mid m \in E\}$

Branching control structures in an $\alpha$-machine are constructed with several edges, each representing a different choice. This is what we'll do here : each **if**-rule will double the number of edges and **seq**-rules will multiply the number of edges to account for each combination of choices we made in the **if**-rules. This will be formalized in Def.4.3 and proved in Prop.5 and Prop.6.

Each edge represents one of the possible update sequences produced by the program: the **update** instructions represent the different updates in the update sequence. The **test** instructions, being partial identities, are not part of the update sequence; instead, they serve to determine the correct update sequence to take: the transition edge.

**Definition (tr<sub>rule</sub>).*

* $f(t_1, \dots, t_n) := t_0 \mapsto \{\text{update}(f(t_1, \dots, t_n) \leftarrow t_0)\}$

* seq $R_1; \dots; R_n$ endseq $\mapsto$ tr<sub>rule</sub>($R_1$); \dots; tr<sub>rule</sub>($R_2$)

* if $\varphi$ then $R_1$ else $R_2$ endif $\mapsto$ test($\varphi$); tr<sub>rule</sub>($R_1$) $\cup$ test($\neg \varphi$); tr<sub>rule</sub>($R_2$)
Once we have "broken down" the ASM-program into a set of edges, we can build the $\alpha$-machine : each edge will simply go from $s_0$ to $s_0$. We also need to add the copy instruction at the beginning of each edge to store the state before the transition.

**Definition** ($P_M$). $P_M$ is defined by :

$$P_M := \{(\text{copy}; m, s_0 \to s_0) \mid m \in \text{tr}_{\text{rule}}(\text{Prog})\}$$

for the rest of this paper, we'll omit ($s_0 \to s_0$) : $P$ will be seen as a subset of $M(I)$.

## 4.3 Main Result

**Theorem 2.** Let $s_0 \to_M s_1 \to_M s_2 \to_M \dots$ be a computation of $M$. We define

$$a_0 \to_{P_M} a_1 \to_{P_M} a_2 \to_{P_M} \dots$$

as a computation of $P_M$ of first state $a_0 = (s_0, -)$. We have that for each $i$,

$$\text{proj}_1(a_i) = s_i$$

The proof of this theorem is done by induction on the last proposition (7).

**Definition** ($I_M^{\text{ASM}}$).

$$I_M^{\text{ASM}} =_{\text{def.}} I_M \setminus \{\text{copy}\}$$

The following point are 2 properties of the instructions of $I_M^{\text{ASM}}$ :

1. Aside from copy, no instruction modify the copy-state : $\forall s_1, s_2 \in S, \forall m \in M(I_{\text{ASM}})$ : if $\alpha(m)(s_1, s_2) \downarrow$ then $\text{proj}_2(\alpha(m)(s_1, s_2)) = s_2$

2. As all tests are made by valuing from the copy-state modification to the current-state do not change the tests : $\forall s_1, s'_1, s_2 \in S, \forall m \in M(I_{\text{ASM}}), \alpha(m)(s_1, s_2) \downarrow \Leftrightarrow \alpha(m)(s'_1, s_2) \downarrow$

From these properties, we can infer a lemma that tells us that update instructions have no effect on test instructions.

**Lemma.** $\forall i_1, \dots, i_n \in I_{\text{ASM}}$ :

$$\text{dom}(\alpha(i_1; \dots; i_n)) = \bigcap_{k=1}^{n} \text{dom}(\alpha(i_k))$$

First, we need to characterize the transition edge (and to do so, prove that $P_M$ is deterministic) : it can be found directly from Prog and s.

**Definition** (edge). Let $s \in S$, edge$_s$ :

* $f(t_1, \dots, t_n) := t_0 \mapsto \text{update}(f(t_1, \dots, t_n) \leftarrow t_0)$
* `par R₁;...;Rₙ endpar` ↦ `edgeₙ(R₁);...;edgeₙ(Rₙ)`

* `if ϕ then R₁ else R₂ else` ↦
  `edgeₙ(R₁) if [ϕ]ₙ = true edgeₙ(R₂) else`

**Proposition 4.** *P*<sub>M</sub> is deterministic and, ∀s, − ∈ **States**, te<sub>P<sub>M</sub></sub>(s, −) = copy; edge<sub>s</sub>(Prog)

*Proof.* Let s be a **States**. We will prove by induction on the ASM program **Prog** that there is only one element e in tr<sub>rule</sub>(**Prog**) such that α(e)(s, s) ↓ and it is edge<sub>s</sub>(**Prog**):

* **Prog** = f(t₁, ..., tₙ) := t₀ : P contains only 1 edge whose domain is S × S and this edge is **update**(*f*(*t*₁, ..., *t*ₙ) ← *t*₀)

* if ϕ then R₁ else R₂ else : we have 2 cases

- `[ϕ]ₙ = true`: then there are 2 types of edge in tr<sub>rule</sub>(Prog) : those of the form **test**(*ϕ*); *m*₁ and **test**(*¬ϕ*); *m*₂ but α(**test**(*¬ϕ*))(*s*, *s*) = α(**test**(*¬ϕ*))(*s*, *s*) ↑, so it has to be of the form **test**(*ϕ*); *m*₁ and α(**test**(*ϕ*))(*s*, *s*) ↓. Furthermore, by induction, there is an unique edge *m* such that α(*m*)(*s*, *s*) ↓. By the previous Lemma 4.3, **test**(*ϕ*); *m* is the wanted edge

- `[ϕ]ₙ = false`: same reasoning but with `¬ϕ` and `E₂`

* **seq R₁;...;Rₙ endseq**: by the property 2 and the Lemma 4.3, we can prove that α(**edge**<sub>s</sub>(R₁);...;**edge**<sub>s</sub>(Rₙ))(s, s) ↓. We also need to prove that it is the only edge possible : by the property 2 and the Lemma 4.3, we would have that any *m*ᵢ ≠ **edge**<sub>s</sub>(Rᵢ) exclude (*s*, *s*) from the domain of the edge

☐

Once we have the transition edge, we need to prove that its semantic is the same the one of Prog on the same state. As said previously, each edge is supposed to represent an update sequence : the following **extr** function gives, from an edge and a state, the update sequence that this edge represent.

**Definition (extr).** Let $s \in S$, $\text{extr}_s$ :

* $\varepsilon \mapsto \varepsilon$

* `copy` ↦ `ε`

* `test(ϕ)` ↦ `ε`

* `update(f(t₁, ..., tₙ) ← t₀) ↦ (f, ([t₁]s, ..., [tₙ]s), [t₀]s)`

* `i; m ↦ extr_s(i) :: extr_s(m)`

**Proposition 5.** Let $- , s$ be **States** and $m$ be a sequence of $I_{\text{ASM}}$. If $\alpha(m)(-, s) \downarrow$
then $\alpha(m)(-, s) = (- \triangleleft \text{extr}_s(m), s)$
Proof. Let $- , s$ be States. By induction on $m$ : (we'll suppose that $\alpha(m)(-, s) \downarrow$)

• $m = \varepsilon$ : We have that $\alpha(\varepsilon)(-, s) = (-, s) = (- \triangleleft \varepsilon, s)$

• $m = i; m'$ : There are 2 cases

- $i = \mathbf{test}(\varphi)$ : Given that $\alpha(m)(-, s) \downarrow$, we have in particular that
  $\alpha(\mathbf{test}(\varphi))(-, s) \downarrow$ and because the $\mathbf{test}$ instructions are partial
  identity, $\alpha(\mathbf{test}(\varphi))(-, s) = (-, s)$. Therefore $\alpha(\mathbf{test}(\varphi); m')(-, s) = \alpha(m')(-, s)$

$= (- \triangleleft \mathbf{extr}_s(m'), s)$ by I.H.

$= (- \triangleleft \mathbf{extr}_s(\mathbf{test}(\varphi)) :: \mathbf{extr}_s(\mathbf{test}(\varphi)); m')$

$= (- \triangleleft \mathbf{extr}_s(\mathbf{test}(\varphi); m'), s)$

- $i = \mathbf{update}(f(\vec{t}) \leftarrow t_0)$ : We have that

$$
\alpha(\mathbf{update}(f(\vec{t}) \leftarrow t_0); m')(-, s) = \alpha(m')(\neg \triangleleft (f, ([\vec{t}]_s), [t_0]_s), s)
$$

$= (- \triangleleft (f, ([\vec{t}]_s), [t_0]_s) \triangleleft \mathbf{extr}_s(m'), s)$ by I.H.

$= (- \triangleleft (f, ([\vec{t}]_s), [t_0]_s) :: \mathbf{extr}_s(m'), s)$

$= (- \triangleleft \mathbf{extr}_s(\mathbf{update}(f(\vec{t}) \leftarrow t_0); m'), s)$

□

We now prove that the update sequence extracted from the transition edge
is equal to the update sequence of the program *Prog* we started from.

**Proposition 6.** $\forall s, - \in S$

$$
\mathrm{extr}_s(\mathrm{edge}_s(\mathrm{Prog})) = [[\mathrm{Prog}]_s]
$$

Proof. Let $s, - \in \mathbf{States}$. By induction on $\mathbf{Prog}$:

• $f(\vec{t}) := t_0$ : we have that $\mathbf{extr}_s(\mathbf{edge}_s(\mathbf{Prog})) = \mathbf{extr}_s(\mathbf{update}(f(\vec{t}) \leftarrow t_0))$

$$
= (f, [\vec{t}]_s, [t_0]_s)
$$

$$
= [[\mathbf{Prog}]_s]
$$

• if $\varphi$ then $R_1$ else $R_2$ endif : we have 2 cases

- $[\varphi]_s = \text{true}$ : we have that $\text{extr}_s(\text{edge}_s(\text{Prog})) = \text{extr}_s(\text{test}(\varphi); \text{edge}_s(R_1))$

$$
= \mathbf{extr}_s(\mathbf{edge}_s(R_1))
$$

$$
= [[R_1]]_s \quad \text{by I.H.}
$$

$$
= [[\mathbf{Prog}]_s]
$$

- $[\varphi]_s = \mathbf{false}$ : same reasoning but with $\neg\varphi$ and $R_2$
• seq $R_1;...;R_n$ endseq: we have that $\text{extr}_s(\text{edge}_s(\text{Prog}))$
$= \text{extr}_s(\text{edge}_s(R_1);...;\text{edge}_s(R_n))$
$\vdots$
$\text{I.H.} \quad \text{extr}_s(\text{edge}_s(R_1)) :: ... :: \text{extr}_s(\text{edge}_s(R_n))$
$\vdots$
$= [[R_1]]_s :: ... :: [[R_n]]_s = [[\text{Prog}]]_s$
$\square$

**Proposition 7.** Let $s, -$ be States, we have that

$$ \tau_{P_M}(s, -) = (s \triangleleft \text{Prog}_M, s) $$

*Proof.* Let $s, -$ be States, we have that:

$$
\begin{align*}
\tau_{P_M}(s, -) &= \alpha(\text{te}_{P_M}(s, -))(s, -) \\
&= \alpha(\text{copy}; \text{edge}_s(\text{Prog}))(s, -) \quad \text{by Prop.4} \\
&= \alpha(\text{edge}_s(\text{Prog}))(s, s) \\
&= (s \triangleleft \text{extr}_s(\text{edge}_s(\text{Prog})), s) \quad \text{by Prop.5} \\
&= (s \triangleleft [[\text{Prog}]_s, s) \quad \text{by Prop.6} \\
&= (s \triangleleft \text{Prog}, s)
\end{align*}
$$

<figure><img src="image_4.png" /></figure>

An example is given in Appendix A

# 5 Conclusion

The main objective of this article was to demonstrate the operational similarity between Abstract State Machines (ASMs) and Seiller's Algorithms (AMCs). Although we have established a general equivalence, this relationship can be nuanced and refined according to specific cases. For example, the Euclidean algorithm *ea2* (in appendix B) could have been simulated by an ASM with a core close to that of *ea1* (in appendix *ea1*), simply requiring the addition of a variable and a type to represent AMC states.

Despite this operational equivalence, a major conceptual difference persists between the two approaches. Gurevich considers ASMs to represent his complete notion of algorithm, whereas Seiller views his equivalent notion (AMCs) as only part of what constitutes an algorithm. This philosophical divergence reflects fundamentally different positions on the very nature of algorithms.

This difference can largely be explained by the viewpoint defended by Gurevich, Dershowitz, and Blass in their article [2]. These authors argue against the formalization of a relation for comparing algorithms (hence the provocative
title of their publication). To our knowledge, there is no formalization of a relation between different ASMs, although the notion of refinement presented in [4] seems to constitute a non-formalized relation between these models.

Seiller, on the other hand, has chosen a different approach by integrating the comparison of algorithms directly into his theory. His notion of AMC actually represents only the "lower level" of his conception of algorithms. In his vision, algorithms are fundamentally graph structures that can be defined at multiple levels: computational models, data structures, and theories/logics. This triple categorization, associated with the representation of algorithms as graphs, notably allows for the formalization of the notion of implementation. Thus, ea2 can be considered as a particular implementation of the Euclidean algorithm (on integers, using the modulo operation). This algorithm can, of course, admit implementations other than ea2.

## References

[1] Hendrik Pieter Barendregt. *The Lambda Calculus: Its Syntax and Semantics*, volume 103 of *Studies in Logic and the Foundations of Mathematics*. North-Holland, 1985.

[2] Andreas Blass, Nachum Dershowitz, and Yuri Gurevich. When are two algorithms the same? *Bull. Symb. Log.*, 15(2):145–168, 2009. URL: https://doi.org/10.2178/bsl/124394848, doi:10.2178/BSL/124394848.

[3] Andreas Blass and Yuri Gurevich. The linear time hierarchy theorems for asm and rams. *Springer J. of Universal Computer Science*, pages 247–278, 04 1997.

[4] Egon Börger and Alexander Raschke. *Modeling Companion for Software Practitioners*. Springer, 2018. doi:10.1007/978-3-662-56641-1.

[5] Nachum Dershowitz and Yuri Gurevich. A natural axiomatization of computability and proof of church’s thesis. *Bull. Symb. Log.*, 14(3):299–350, 2008. URL: https://doi.org/10.2178/bsl/1231081370, doi:10.2178/BSL/1231081370.

[6] Serge Grigorieff and Pierre Valarcher. Evolving multialgebras unify all usual sequential computation models. In Jean-Yves Marion and Thomas Schwentick, editors, *27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010, March 4-6, 2010, Nancy, France*, volume 5 of *LIPIcs*, pages 417–428. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. URL: https://doi.org/10.4230/LIPICS.STACS.2010.2473, doi:10.4230/LIPICS.STACS.2010.2473.

[7] Serge Grigorieff and Pierre Valarcher. Classes of algorithms: Formalization and comparison. *Bull. EATCS*, 107:95–127, 2012. URL: http://bulletin.eatcs.org/index.php/beatcs/article/view/70/66.
[8] Serge Grigorieff and Pierre Valarcher. Functionals using bounded information and the dynamics of algorithms. In *Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012*, pages 345–354. IEEE Computer Society, 2012. doi:10.1109/LICS.2012.45.

[9] Yuri Gurevich. Logic and the challenge of computer science. In E. Borger, editor, *Current Trends in Theoretical Computer Science*, pages 1–57. Computer Science Press, 1988.

[10] Yuri Gurevich. *Evolving Algebras 1993: Lipari Guide*, pages 9–36. Oxford University Press, specification and validation methods edition, 01 1995. URL: https://www.microsoft.com/en-us/research/publication/103-evolving-algebras-1993-lipari-guide/.

[11] Yuri Gurevich. Sequential abstract-state machines capture sequential algorithms. *ACM Trans. Comput. Logic*, 1(1):77–111, 7 2000. doi:10.1145/343369.343384.

[12] Hong-Linh Lê. Théorie des algorithmes : étude comparée. Master's thesis, Université Paris Cité, September 2023. URL: https://cloud.lacl.fr/s/9x8YbwRJEGQgTn8.

[13] Andrey Andreevich Markov. The theory of algorithms. *American Mathematical Society Translations, Series 2*, 15:1–14, 1960. Translation from the Russian, Trudy Instituta im. Steklova 38 (1951) 176–189.

[14] Yannis N. Moschovakis. On primitive recursive algorithms and the greatest common divisor function. *Theoretical Computer Science*, 301:1–30, 2003.

[15] Yiannis N. Moschovakis. Abstract recursion as a foundation of the theory of algorithms. In M. M. Richter et al., editors, *Computation and Proof Theory*, volume 1104 of *Lecture Notes in Mathematics*, pages 289–364. Springer-Verlag, Berlin, 1984.

[16] Yiannis N. Moschovakis. Recursion and complexity. In S. Barry Cooper, Benedikt Löwe, and Leen Torenvliet, editors, *New Computational Paradigms, First Conference on Computability in Europe, CiE 2005, Amsterdam, The Netherlands, June 8-12, 2005, Proceedings*, volume 3526 of *Lecture Notes in Computer Science*, pages 350–357. Springer, 2005. doi:10.1007/11494645\_44.

[17] Yiannis N. Moschovakis and Vasilis Paschalis. Elementary algorithms and their implementations. In S. B. Cooper, Benedikt Löwe, and Andrea Sorbi, editors, *New Computational Paradigms*, pages 81–118. Springer, 2008.

[18] Luc Pellissier and Thomas Seiller. Lower bounds for prams over Z. *CoRR*, abs/2002.10888, 2020. URL: https://arxiv.org/abs/2002.10888, arXiv:2002.10888.
[19] Thomas Seiller. *Mathematical Informatics*. Accreditation to supervise research, Université Sorbonne Paris Nord, 6 2024. URL: https://theses.hal.science/tel-04616661.

[20] Alan M. Turing. Computability and λ-definability. *The Journal of Symbolic Logic*, 2(4):153–163, 12 1937.

[21] Lou van den Dries. Is the euclidean algorithm optimal among its peers? *The Bulletin of Symbolic Logic*, 10:390–418, 2004.

[22] Lou van den Dries. Arithmetic complexity. *ACM Transactions on Computational Logic*, 10:1–49, 2009.
## A An ASM and its translation : ea1

The ASM `ea1` is defined by:

* $\text{Voc}_{\text{ea1}} = \{0, \%, a, b\}$ where 0, a, b are constant (0-ary) and % is a binary function.

* $\text{States}_{\text{ea1}}$: each state $s$ has $\mathbb{N}$ as a base set, $0^s$ (noted 0) is valued as 0 (the integer), $\%^s$ (we'll note it %) is the modulo operation and $a^s, b^s$ are in $\mathbb{N}$.

* $\text{Prog}_{\text{ea1}} = \begin{cases} \text{if } b \neq 0 & \text{then} \\ \text{seq} \\ a := b \\ b := a\%b \\ \text{else} \\ \text{seq} \end{cases}$

If we take the initial state $(\mathbb{N}, 0, \%, 7, 3)$, the computation is going to be:

$$ (\mathbb{N}, 0, \%, 7, 3) \rightarrow (\mathbb{N}, 0, \%, 3, 1) \rightarrow (\mathbb{N}, 0, \%, 1, 0) \rightarrow (\mathbb{N}, 0, \%, 1, 0) \rightarrow \dots $$

$\text{Prog}_{\text{ea1}}$ is an if-rule each one leading to seq-rule (only followed by upd-rule), this will lead to 2 edges : copy; test($b \neq 0$); update($a \leftarrow b$); update($b \leftarrow a\%b$) and test($\neg b \neq 0$). $P_{\text{ea1}}$ will be the $\alpha_{\text{ea1}}$-machine defined as :

$$ P_{\text{ea1}} = \{(\text{copy}; \text{test}(b \neq 0); \text{update}(a \leftarrow b); \text{update}(b \leftarrow a\%b), s_0 \rightarrow s_0), \\ (\text{test}(\neg b \neq 0), s_0 \rightarrow s_0)\} $$

## B An AMC and its translation : ea2

The AMC $\alpha_{\text{ea2}}$ is defined by:

* $I_{\alpha_{\text{ea2}}} = \{\text{eq}_0, \text{neq}_0, \text{mod}, \text{swap}\}$

* $X_{\alpha_{\text{ea2}}} = \mathbb{N} \times \mathbb{N}$

* $\alpha_{\text{ea1}}: \begin{array}{rcl} \text{eq}_0 & \mapsto & \left( \begin{array}{lcl} (a, b) & \mapsto & \begin{cases} (a, b) & \text{if } b = 0 \\ \uparrow & \text{else} \end{cases} \end{array} \right) \\ \text{neq}_0 & \mapsto & \left( \begin{array}{lcl} (a, b) & \mapsto & \begin{cases} (a, b) & \text{if } b \neq 0 \\ \uparrow & \text{else} \end{cases} \end{array} \right) \\ \text{mod} & \mapsto & ((a, b) \mapsto (a\%b, b)) \\ \text{swap} & \mapsto & ((a, b) \mapsto (b, a)) \end{array}$

And we define the $\alpha$-machine `ea2` by:
• $S_{ea2} = \{s_0, s_1, s_2\}$

• $ea2 = \{(\text{neq}_0, s_0 \to s_1), (\text{mod}; \text{swap}, s_1 \to s_0), (\text{eq}_0, s_0 \to s_2)\}$

<figure><img src="image_5.png" /></figure>

We have the following computation on starting configuration (7,3) :

$$ \begin{array}{rcl} (s_0, (7,3)) & \to & (s_1, (7,3)) \to (s_0, (3,1)) \to (s_1, (3,1)) \to (s_0, (1,0)) \to (s_2, (1,0)) \\ & & \to (\mathbf{end}, \perp) \to \dots \end{array} $$

There are 4 values of $\text{tr}_I$ that interest us:

• $\epsilon \mapsto \text{config}$

• $\text{neq}_0 \mapsto \text{neq}_0(\text{config})$

• $\text{eq}_0 \mapsto \text{eq}_0(\text{config})$

• $\text{mod}; \text{swap} \mapsto \text{swap}(\text{mod}(\text{config}))$
The ASM program Π<sub>P</sub> is defined as :

```
if state = s₀ then
  if neq₀(config) ≠ ⊥ then
    config := neq₀(config)
    state := s₁
  else
    if eq₀(config) ≠ ⊥ then
      config := eq₀(config)
      state := s₂
    else
      config := ⊥
      state := end
if state = s₁ then
  if swap(mod(config)) ≠ ⊥ then
    config := swap(mod(config))
    state := s₀
  else
    config := ⊥
    state := end
if state = s₂ then
  if config ≠ ⊥ then
    config := config
    state := s₂
  else
    config := ⊥
    state := end
```

*Remark.* The seq do not appear in the above program : rules within the same indentation block are to be treated as a seq-rule