User:CircuitCraft/Definition:Abstract Machine

Definition

An abstract machine is a $2$-tuple $\struct {S, \vdash}$ where:

$S$ is a set called the configurations.

${\vdash} \subset S \times S$ is a relation from $S$ to itself, called the transition relation.

Reachable Configuration

Let $\struct {S, \vdash}$ be an abstract machine.

Let $a, b \in S$ be configurations.

$b$ is reachable from $a$ if and only if there is a finite sequence $\sequence {s_0, s_1, \dotsc, s_n}$ such that:

$a = s_0 \vdash s_1 \vdash \dotso \vdash s_n = b$

Halting from a Configuration

Let $M = \struct {S, \vdash}$ be an abstract machine.

Let $a \in S$ be a configuration.

Let there exist $N \in \N$ such that there does not exist a finite sequence:

$a \vdash s_1 \vdash \dotso \vdash s_N$

Then $M$ halts from $a$.

Deterministic

Let $M = \struct {S, \vdash}$ be an abstract machine.

$M$ is deterministic if and only if $\vdash$ is many-to-one.