Lax916827.RegularEquivalenceDecidable

Decidable equivalence of regular functions

concepts/Lax916827/RegularEquivalenceDecidable.lean · lax-916827

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax916827.RegularEquivalenceDecidable

⊢Lax916827Proofs.Results.decidable_twoWayCodeRel_eq

In the paper

page 87 of the paper of lax-157538, Transducers

Theorem

Equivalence is decidable for regular functions (Theorem C.1.4 of Transducers), the functions being given by two-way transducers, which compute exactly the regular functions (Theorem C.2.9). The book reduces to equivalence of weighted automata over the rationals, as for rational functions: the class of functions that can be post-composed with weighted automata is closed under composition, contains the rational functions (Theorem B.3.6), and contains map reverse and map duplicate by two constructions with triples of states.

Lean source view on GitHub

1	import Lax132576.TransducerCodes
2	import Lax916827.TwoWayCodes
3
4	/-!
5	---
6	title: Decidable equivalence of regular functions
7	type: theorem
8	---
9	Equivalence is decidable for regular functions (Theorem C.1.4 of
10	Transducers), the functions being given by two-way transducers, which compute
11	exactly the regular functions (Theorem C.2.9). The book reduces to equivalence
12	of weighted automata over the rationals, as for rational functions: the class of
13	functions that can be post-composed with weighted automata is closed under
14	composition, contains the rational functions (Theorem B.3.6), and contains map
15	reverse and map duplicate by two constructions with triples of states.
16
17	# Formalization notes
18
19	The two transducers are given by codes (`TwoWayCodes`), under the promise that
20	both are total, and the decided property is equality of the coded relations.
21	The proof does not follow the book's reduction to the letter: the bound on the
22	length of a shortest distinguishing input is obtained from the
23	crossing-sequence decomposition of a two-way run and Schützenberger's rank
24	criterion, which gives an explicit arithmetic bound in the sizes of the codes,
25	and the two coded transducers are compared on all inputs up to that bound over
26	the letters of the codes and one fresh letter.
27	-/
28
29	namespace Lax916827.RegularEquivalenceDecidable
30
31	open Lax132576.TransducerCodes Lax916827.TwoWayCodes
32
33	/-- Equivalence of two total coded two-way transducers is decidable. -/
34	axiom decidable_twoWayCodeRel_eq :
35	DecidableUnderPromise
36	(fun p : TwoWayCode × TwoWayCode => TwoWayCodeTotal p.1 ∧ TwoWayCodeTotal p.2)
37	(fun p => twoWayCodeRel p.1 = twoWayCodeRel p.2)
38
39	end Lax916827.RegularEquivalenceDecidable
40

Show Proof

Formalization notes

The two transducers are given by codes ( $TwoWayCodes$ ), under the promise that both are total, and the decided property is equality of the coded relations. The proof does not follow the book's reduction to the letter: the bound on the length of a shortest distinguishing input is obtained from the crossing-sequence decomposition of a two-way run and Schützenberger's rank criterion, which gives an explicit arithmetic bound in the sizes of the codes, and the two coded transducers are compared on all inputs up to that bound over the letters of the codes and one fresh letter.

Builds on

Used by

none

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