User:CircuitCraft/Definition:Abstract Machine/Halting

Definition

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$.