Lax132576.RationalRelations

Nondeterministic automata with output and rational relations

concepts/Lax132576/RationalRelations.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
page 36 of the paper of lax-157538, Transducers

Definition

A nondeterministic automaton with output (Definition B.1.1 of Transducers) consists of input and output alphabets $A$ and $B$ , a finite set of states $Q$ , initial and final subsets $I, F \subseteq Q$ , and a finite transition relation

\delta \subseteq Q \times A^* \times B^* \times Q.

It is a directed graph whose edges are labelled by pairs of an input string and an output string; a run is a path from an initial to a final state, and its input and output strings are the concatenations of the labels along it. The semantics of the automaton is the relation $R \subseteq A^* \times B^*$ of the pairs (input string, output string) of its accepting runs, and a relation is rational (Definition B.1.2) if it is the semantics of such an automaton. Rational relations are input/output symmetric, and a single input may have infinitely many outputs, through transitions with empty input.

An automaton with output is unambiguous if every input string has exactly one accepting run; the relations computed by unambiguous automata are the second item of Theorem B.2.3. A state is productive if it occurs in some accepting run (Claim B.4.4).

Lean source view on GitHub

1	import Lax132576.LabelledAutomata
2
3	/-!
4	---
5	title: Nondeterministic automata with output and rational relations
6	type: definition
7	---
8	A nondeterministic automaton with output (Definition B.1.1 of Transducers)
9	consists of input and output alphabets $A$ and $B$ , a finite set of states $Q$ ,
10	initial and final subsets $I, F \subseteq Q$ , and a finite transition relation
11	$\delta \subseteq Q \times A^* \times B^* \times Q.$
12	It is a directed graph whose edges are labelled by pairs of an input string and
13	an output string; a run is a path from an initial to a final state, and its
14	input and output strings are the concatenations of the labels along it. The
15	semantics of the automaton is the relation $R \subseteq A^* \times B^*$ of the
16	pairs (input string, output string) of its accepting runs, and a relation is
17	rational (Definition B.1.2) if it is the semantics of such an automaton.
18	Rational relations are input/output symmetric, and a single input may have
19	infinitely many outputs, through transitions with empty input.
20
21	An automaton with output is unambiguous if every input string has exactly
22	one accepting run; the relations computed by unambiguous automata are the second
23	item of Theorem B.2.3. A state is productive if it occurs in some accepting
24	run (Claim B.4.4).
25
26	# Formalization notes
27
28	An automaton with output is a labelled automaton (`LabelledAutomata`) whose
29	labels are output strings, `NFAO A B Q := LabAut A (List B) Q`. `rel M w v` says
30	that some accepting run reads `w` and writes `v`. `IsRationalRel R` asks for a
31	finite state space and an automaton over it whose relation is `R`; the
32	alphabets are arbitrary types, their finiteness being a hypothesis of the
33	theorems that need it.
34	-/
35
36	namespace Lax132576.RationalRelations
37
38	open Lax132576.LabelledAutomata
39
40	/-- A nondeterministic automaton with output: a labelled automaton whose labels
41	are output strings. -/
42	abbrev NFAO (A B Q : Type) := LabAut A (List B) Q
43
44	namespace NFAO
45
46	variable {A B Q : Type}
47
48	/-- The output string of a path: the concatenation of the outputs of its
49	transitions. -/
50	def outputOf (ts : List (Q × List A × List B × Q)) : List B := (LabAut.labelsOf ts).flatten
51
52	/-- The relation computed by an automaton with output: `w` is related to `v` if
53	some accepting run reads `w` and writes `v`. -/
54	def rel (M : NFAO A B Q) (w : List A) (v : List B) : Prop :=
55	∃ ts, M.Accepting ts ∧ LabAut.inputOf ts = w ∧ outputOf ts = v
56
57	/-- An automaton with output is unambiguous if every input string has exactly one
58	accepting run. -/
59	def Unambiguous (M : NFAO A B Q) : Prop :=
60	∀ w : List A, ∃! ts, M.Accepting ts ∧ LabAut.inputOf ts = w
61
62	/-- A state is productive if it occurs in some accepting run. -/
63	def Productive (M : NFAO A B Q) (q : Q) : Prop :=
64	∃ q₀ ∈ M.init, ∃ p ∈ M.final, ∃ ts₁ ts₂, M.Path q₀ ts₁ q ∧ M.Path q ts₂ p
65
66	end NFAO
67
68	/-- A relation is rational if it is computed by a nondeterministic automaton with
69	output with a finite state space. -/
70	def IsRationalRel {A B : Type} (R : List A → List B → Prop) : Prop :=
71	∃ (Q : Type) (_ : Finite Q) (M : NFAO A B Q), ∀ w v, R w v ↔ M.rel w v
72
73	/-- A relation computed by an unambiguous automaton with output. -/
74	def IsUnambiguousRel {A B : Type} (R : List A → List B → Prop) : Prop :=
75	∃ (Q : Type) (_ : Finite Q) (M : NFAO A B Q), M.Unambiguous ∧ ∀ w v, R w v ↔ M.rel w v
76
77	end Lax132576.RationalRelations
78

Formalization notes

An automaton with output is a labelled automaton ( $LabelledAutomata$ ) whose labels are output strings, $NFAO A B Q := LabAut A (List B) Q$ . $rel M w v$ says that some accepting run reads $w$ and writes $v$ . $IsRationalRel R$ asks for a finite state space and an automaton over it whose relation is $R$ ; the alphabets are arbitrary types, their finiteness being a hypothesis of the theorems that need it.

Builds on

Lax132576.LabelledAutomata

Used by

From Mathlib

none

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