User:CircuitCraft/Definition:Automaton

From ProofWiki
Jump to navigation Jump to search

Definition

An automaton is a $3$-tuple $\struct {S, \Sigma, \vdash}$, where:

$S$ is a set, called the configurations
$\Sigma$ is a set, called the input alphabet
${\vdash} \subset \paren {S \times \Sigma} \times S$ is a left-total relation

Input

An input string to an automaton is a finite string over $\Sigma$.

Reachable

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

Let $C = c_0 c_1 \dotsm c_n$.

$b$ is reachable from $a$ on input $C$ if and only if there exists a finite sequence $\sequence {s_0, s_1, \dotsc, s_n, s_{n + 1} }$ such that:

$s_0 = a$
$s_{n + 1} = b$
$\paren {s_i, c_i} \vdash s_{i + 1}$ for every $0 \le i \le n$

Associated Abstract Machine

Let $M = \struct {S, \Sigma, \vdash}$ be an automaton.

The associated abstract machine is defined as: $M' = \struct {S', \vdash'}$ where:

$S' = S \times \Sigma^*$
$\tuple {a, c_0 c_1 \dotsm c_m} \vdash' \tuple {b, d_0 d_1 \dotsm d_n}$ if and only if:
$m = n + 1$
$d_i = c_{i + 1}$ for every $0 \le i \le n$
$\tuple {a, c_0} \vdash b$