Lax194892.ForTransducers

For-transducers

concepts/Lax194892/ForTransducers.lean · lax-194892

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 157 of the paper of lax-157538, Transducers
page 157 of the paper of lax-157538, Transducers

Definition

A for-transducer (Section D.1 of Transducers) is an imperative program with $for$ loops ranging over the positions of the input string, in increasing or decreasing order. It has position variables, bound by the loops and read only, and Boolean variables, initially false and assignable; its tests compare positions ( $x == y$ , $x <= y$ ), read the letter at a position ( $w[x] == a$ ) and read Boolean variables, with Boolean connectives; and its statements are $output(b)$ , assignment to a Boolean variable, sequential composition, conditionals and loops. The output of a run is the concatenation of the output letters produced. A for-transducer is in prenex form (Definition D.1.2) if it is a block of nested loops whose body is loop-free and produces at most one output letter per iteration, followed by a loop-free epilogue. For-transducers compute exactly the polyregular functions (Theorem D.1.1).

Lean source view on GitHub

1	import Mathlib.Logic.Function.Basic
2	import Mathlib.Data.List.Basic
3
4	/-!
5	---
6	title: For-transducers
7	type: definition
8	---
9	A for-transducer (Section D.1 of Transducers) is an imperative program
10	with `for` loops ranging over the positions of the input string, in increasing
11	or decreasing order. It has position variables, bound by the loops and read
12	only, and Boolean variables, initially false and assignable; its tests compare
13	positions (`x == y`, `x <= y`), read the letter at a position (`w[x] == a`) and
14	read Boolean variables, with Boolean connectives; and its statements are
15	`output(b)`, assignment to a Boolean variable, sequential composition,
16	conditionals and loops. The output of a run is the concatenation of the output
17	letters produced. A for-transducer is in prenex form (Definition D.1.2) if it
18	is a block of nested loops whose body is loop-free and produces at most one
19	output letter per iteration, followed by a loop-free epilogue. For-transducers
20	compute exactly the polyregular functions (Theorem D.1.1).
21
22	# Formalization notes
23
24	Variables of both kinds are named by natural numbers; a valuation of the
25	position variables is `ℕ → ℕ` and of the Boolean variables `ℕ → Bool`. `exec`
26	runs a program from a valuation and returns the final Boolean valuation and the
27	output; `eval P w` is the output from the all-zero valuations. `loop true x P`
28	ranges over the positions in increasing order, `loop false x P` in decreasing
29	order.
30	-/
31
32	namespace Lax194892.ForTransducers
33
34	/-- Tests of a for-transducer. -/
35	inductive ForTest (A : Type) : Type
36	/-- The value of a Boolean variable. -/
37	\| boolVar : ℕ → ForTest A
38	/-- The equality test `x == y` on position variables. -/
39	\| eqPos : ℕ → ℕ → ForTest A
40	/-- The order test `x <= y` on position variables. -/
41	\| lePos : ℕ → ℕ → ForTest A
42	/-- The label test `w[x] == a`. -/
43	\| label : ℕ → A → ForTest A
44	/-- Negation. -/
45	\| not : ForTest A → ForTest A
46	/-- Conjunction. -/
47	\| and : ForTest A → ForTest A → ForTest A
48	/-- Disjunction. -/
49	\| or : ForTest A → ForTest A → ForTest A
50
51	/-- Programs of a for-transducer. -/
52	inductive ForProg (A B : Type) : Type
53	/-- The empty program. -/
54	\| skip : ForProg A B
55	/-- `output(b)`. -/
56	\| output : B → ForProg A B
57	/-- `X = true` / `X = false`. -/
58	\| assign : ℕ → Bool → ForProg A B
59	/-- Sequential composition `I ; J`. -/
60	\| seq : ForProg A B → ForProg A B → ForProg A B
61	/-- A conditional. -/
62	\| ite : ForTest A → ForProg A B → ForProg A B → ForProg A B
63	/-- `for x in positions(w)` (`true`) or `for x in positions_reverse(w)` (`false`). -/
64	\| loop : Bool → ℕ → ForProg A B → ForProg A B
65
66	namespace ForTest
67
68	variable {A : Type}
69
70	/-- The truth value of a test under valuations of the position and Boolean
71	variables. -/
72	def Holds (w : List A) (pos : ℕ → ℕ) (bv : ℕ → Bool) : ForTest A → Prop
73	\| boolVar i => bv i = true
74	\| eqPos i j => pos i = pos j
75	\| lePos i j => pos i ≤ pos j
76	\| label i a => w[pos i]? = some a
77	\| not t => ¬ Holds w pos bv t
78	\| and t s => Holds w pos bv t ∧ Holds w pos bv s
79	\| or t s => Holds w pos bv t ∨ Holds w pos bv s
80
81	end ForTest
82
83	/-- Running the body of a loop over a list of positions, threading the Boolean
84	valuation and concatenating the outputs. -/
85	def forLoopRun {B : Type} (body : (ℕ → Bool) → ℕ → (ℕ → Bool) × List B) :
86	List ℕ → (ℕ → Bool) → (ℕ → Bool) × List B
87	\| [], bv => (bv, [])
88	\| p :: ps, bv =>
89	let r := body bv p
90	let r' := forLoopRun body ps r.1
91	(r'.1, r.2 ++ r'.2)
92
93	namespace ForProg
94
95	variable {A B : Type}
96
97	open scoped Classical in
98	/-- The semantics of a program: the final Boolean valuation and the output. -/
99	noncomputable def exec (w : List A) :
100	ForProg A B → (ℕ → ℕ) → (ℕ → Bool) → (ℕ → Bool) × List B
101	\| skip, _, bv => (bv, [])
102	\| output b, _, bv => (bv, [b])
103	\| assign i v, _, bv => (Function.update bv i v, [])
104	\| seq P Q, pos, bv =>
105	let r := exec w P pos bv
106	let r' := exec w Q pos r.1
107	(r'.1, r.2 ++ r'.2)
108	\| ite t P Q, pos, bv =>
109	if ForTest.Holds w pos bv t then exec w P pos bv else exec w Q pos bv
110	\| loop dir x P, pos, bv =>
111	forLoopRun (fun bv' p => exec w P (Function.update pos x p) bv')
112	(if dir then List.range w.length else (List.range w.length).reverse) bv
113
114	/-- The function computed by a for-transducer. -/
115	noncomputable def eval (P : ForProg A B) (w : List A) : List B :=
116	(exec w P (fun _ => 0) (fun _ => false)).2
117
118	/-- A program without loops. -/
119	def LoopFree : ForProg A B → Prop
120	\| skip => True
121	\| output _ => True
122	\| assign _ _ => True
123	\| seq P Q => LoopFree P ∧ LoopFree Q
124	\| ite _ P Q => LoopFree P ∧ LoopFree Q
125	\| loop _ _ _ => False
126
127	/-- Nested loops `for x₁ in τ₁: ⋯ for x_k in τ_k: body`. -/
128	def nestLoops : List (Bool × ℕ) → ForProg A B → ForProg A B
129	\| [], body => body
130	\| (d, x) :: rest, body => ForProg.loop d x (nestLoops rest body)
131
132	/-- A program produces at most one output letter per execution. -/
133	def OutputsAtMostOne (P : ForProg A B) : Prop :=
134	∀ (w : List A) (pos : ℕ → ℕ) (bv : ℕ → Bool), ((exec w P pos bv).2).length ≤ 1
135
136	/-- Prenex form: nested loops whose body is loop-free and outputs at most one
137	letter per iteration, followed by a loop-free epilogue. -/
138	def PrenexForm (P : ForProg A B) : Prop :=
139	∃ (ls : List (Bool × ℕ)) (body epilogue : ForProg A B),
140	LoopFree body ∧ LoopFree epilogue ∧ OutputsAtMostOne body ∧
141	P = ForProg.seq (nestLoops ls body) epilogue
142
143	end ForProg
144
145	/-- A function computed by a for-transducer. -/
146	def IsForTransducer {A B : Type} (f : List A → List B) : Prop :=
147	∃ P : ForProg A B, ∀ w, P.eval w = f w
148
149	end Lax194892.ForTransducers
150

Formalization notes

Variables of both kinds are named by natural numbers; a valuation of the position variables is $ℕ → ℕ$ and of the Boolean variables $ℕ → Bool$ . $exec$ runs a program from a valuation and returns the final Boolean valuation and the output; $eval P w$ is the output from the all-zero valuations. $loop true x P$ ranges over the positions in increasing order, $loop false x P$ in decreasing order.

Builds on

none

Used by

From Mathlib

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