Lax132576.LabelledAutomata

Automata with labelled transitions

concepts/Lax132576/LabelledAutomata.lean · lax-132576

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 36 of the paper of lax-157538, Transducers

Definition

The two nondeterministic models of Part B of Transducers — nondeterministic automata with output (Definition B.1.1) and weighted automata (Definition B.3.2) — are automata whose finitely many transitions are labelled by an input string together with a label from some set: an output string in the first case, an element of a semiring in the second. This concept is their common basis: a finite set of transitions

\delta \subseteq Q \times A^* \times L \times Q,

each a directed edge from a state to a state carrying an input string and a label, together with initial and final subsets of the state space. A run is a path that begins in an initial state and ends in a final state; its input string is the concatenation of the input strings of its transitions, and its labels are read off in the order in which the transitions are taken.

Lean source view on GitHub

1	import Mathlib.Data.Set.Finite.Basic
2
3	/-!
4	---
5	title: Automata with labelled transitions
6	type: definition
7	---
8	The two nondeterministic models of Part B of Transducers — nondeterministic
9	automata with output (Definition B.1.1) and weighted automata (Definition
10	B.3.2) — are automata whose finitely many transitions are labelled by an input
11	string together with a label from some set: an output string in the first
12	case, an element of a semiring in the second. This concept is their common
13	basis: a finite set of transitions
14	$\delta \subseteq Q \times A^* \times L \times Q,$
15	each a directed edge from a state to a state carrying an input string and a
16	label, together with initial and final subsets of the state space. A run is a
17	path that begins in an initial state and ends in a final state; its input string
18	is the concatenation of the input strings of its transitions, and its labels are
19	read off in the order in which the transitions are taken.
20
21	# Formalization notes
22
23	A path is the list of the transitions it uses, so that two runs with the same
24	input are different objects when they use different transitions — which is what
25	"exactly one accepting run" (unambiguity) and "finitely many accepting runs"
26	(weighted automata) have to count. `Path M q ts p` says that `ts` is a path from
27	`q` to `p`, and `Accepting` that a path starts in an initial state and ends in a
28	final one. The state space is a type parameter; its finiteness is required in
29	`RationalRelations` and `WeightedAutomata` where a function is said to be
30	computed by an automaton. The transition relation is a `Set` with a finiteness
31	proof, as the book's "finite set".
32	-/
33
34	namespace Lax132576.LabelledAutomata
35
36	/-- An automaton whose finitely many transitions are labelled by an input string and
37	a label from `L`, with distinguished sets of initial and final states. -/
38	structure LabAut (A L Q : Type) where
39	/-- The set of initial states. -/
40	init : Set Q
41	/-- The set of final states. -/
42	final : Set Q
43	/-- The transition relation. -/
44	δ : Set (Q × List A × L × Q)
45	/-- There are only finitely many transitions. -/
46	δ_finite : δ.Finite
47
48	namespace LabAut
49
50	variable {A L Q : Type}
51
52	/-- A path in the automaton, given as the list of the transitions it uses. -/
53	inductive Path (M : LabAut A L Q) : Q → List (Q × List A × L × Q) → Q → Prop
54	\| nil (q : Q) : Path M q [] q
55	\| cons {q : Q} {u : List A} {l : L} {q' : Q} {ts : List (Q × List A × L × Q)} {p : Q} :
56	(q, u, l, q') ∈ M.δ → Path M q' ts p → Path M q ((q, u, l, q') :: ts) p
57
58	/-- The input string of a path: the concatenation of the input strings of its
59	transitions. -/
60	def inputOf (ts : List (Q × List A × L × Q)) : List A := (ts.map (fun t => t.2.1)).flatten
61
62	/-- The labels along a path, in the order of the transitions. -/
63	def labelsOf (ts : List (Q × List A × L × Q)) : List L := ts.map (fun t => t.2.2.1)
64
65	/-- A path is accepting if it starts in an initial state and ends in a final state.
66	-/
67	def Accepting (M : LabAut A L Q) (ts : List (Q × List A × L × Q)) : Prop :=
68	∃ q ∈ M.init, ∃ p ∈ M.final, M.Path q ts p
69
70	/-- The accepting paths with a given input string. -/
71	def acceptingOn (M : LabAut A L Q) (w : List A) : Set (List (Q × List A × L × Q)) :=
72	{ts \| M.Accepting ts ∧ inputOf ts = w}
73
74	end LabAut
75
76	end Lax132576.LabelledAutomata
77

Formalization notes

A path is the list of the transitions it uses, so that two runs with the same input are different objects when they use different transitions — which is what "exactly one accepting run" (unambiguity) and "finitely many accepting runs" (weighted automata) have to count. $Path M q ts p$ says that $ts$ is a path from $q$ to $p$ , and $Accepting$ that a path starts in an initial state and ends in a final one. The state space is a type parameter; its finiteness is required in $RationalRelations$ and $WeightedAutomata$ where a function is said to be computed by an automaton. The transition relation is a $Set$ with a finiteness proof, as the book's "finite set".

Builds on

none

Used by

From Mathlib

Mathlib.Data.Set.Finite.Basic

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive