Residuals of string functions

This file characterizes the subsequential, Mealy-computable and bimachine-computable functions by their residuals, in the style of the Myhill–Nerode theorem for languages. The prefix function of f : List α → List β sends a word u to the longest common prefix of the outputs of f on the extensions of u, and the residual of f by u sends v to what f outputs on u ++ v beyond that prefix. Residuals compose as a right action of words, and a function is subsequential if and only if it has finitely many residuals, the characterization of Oncina and García recalled by Chandlee, Eyraud and Heinz. A subsequential function is Mealy-computable exactly when it is also length- and prefix-preserving, the Nerode criterion of Eilenberg and Holcombe.

A length-preserving function whose output at a position can depend on input unboundedly far to its right, as in bidirectional harmony, has infinitely many residuals in this sense. Such functions are characterized instead by their synchronous residuals and coresiduals, which cut the output where the input is cut: a length-preserving function is bimachine-computable if and only if it has finitely many of each, the length-preserving stratum of the canonical bimachine of Reutenauer and Schützenberger surveyed by Filiot and Reynier.

Main definitions

• Function.prefixFunction f u: the longest common prefix of f on the extensions of u
• Function.residual f u: the residual of f by the word u
• Function.syncResidual f u, Function.syncCoresidual f y: the output after u and before y of a length-preserving f

Main results

• Function.residual_append: residuals compose as a right action of words
• isLeftSubsequential_iff_finite_range_residual: f is left-subsequential if and only if it has finitely many residuals
• isMealyComputable_iff_residual: f is Mealy-computable if and only if it is length- and prefix-preserving with finitely many residuals
• isLengthPreservingBimachineComputable_iff_syncResidual: a length-preserving f is bimachine-computable if and only if it has finitely many synchronous residuals and coresiduals

Implementation notes

The prefix function takes the supremum in ℕ of the lengths of the common prefixes, so it and the residual are noncomputable. For a prefix-preserving f the prefix function is f itself (prefixFunction_eq_self) and the residual drops f u (residual_eq_drop), which on length-preserving functions is the synchronous residual (residual_eq_syncResidual).

References

• S. Eilenberg, Automata, Languages and Machines, Volume A (1974)
• W. M. L. Holcombe, Algebraic Automata Theory (1982)
• C. Reutenauer and M. P. Schützenberger, Minimization of Rational Word Functions (1991)
• E. Filiot and P. A. Reynier, Transducers, Logic and Algebra for Functions of Finite Words (2016)
• J. Chandlee, R. Eyraud and J. Heinz, Output Strictly Local Functions (2015)

The prefix function and residuals

noncomputable def Function.prefixFunction {α : Type u_1} {β : Type u_2} (f : List α → List β) (u : List α) : List β

The prefix function of f sends u to the longest common prefix of the outputs of f on the extensions of u, the output already determined after reading u.

Equations

• Function.prefixFunction f u = List.take (sSup {n : ℕ | n ≤ (f u).length ∧ ∀ (w : List α), List.take n (f u) <+: f (u ++ w)}) (f u)

noncomputable def Function.residual {α : Type u_1} {β : Type u_2} (f : List α → List β) (u : List α) : List α → List β

The residual of f by u sends v to what f outputs on u ++ v beyond the prefix function at u, the analogue for string functions of Language.leftQuotient.

Equations

• Function.residual f u v = List.drop (Function.prefixFunction f u).length (f (u ++ v))

theorem Function.prefixFunction_prefix {α : Type u_1} {β : Type u_2} {f : List α → List β} (u w : List α) : prefixFunction f u <+: f (u ++ w)

theorem Function.prefix_prefixFunction_iff {α : Type u_1} {β : Type u_2} {f : List α → List β} {u : List α} {p : List β} : p <+: prefixFunction f u ↔ ∀ (w : List α), p <+: f (u ++ w)

The prefix function at u is the greatest common prefix of f on the extensions of u.

theorem Function.prefixFunction_eq_self {α : Type u_1} {β : Type u_2} {f : List α → List β} {u : List α} (h : ∀ (w : List α), f u <+: f (u ++ w)) : prefixFunction f u = f u

theorem Function.prefixFunction_append_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} (u v : List α) : prefixFunction f u ++ residual f u v = f (u ++ v)

theorem Function.append_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} {u : List α} (h : ∀ (w : List α), f u <+: f (u ++ w)) (v : List α) : f u ++ residual f u v = f (u ++ v)

A function prefix-preserving at u extends its output on u by the residual.

theorem Function.residual_eq_drop {α : Type u_1} {β : Type u_2} {f : List α → List β} {u : List α} (h : ∀ (w : List α), f u <+: f (u ++ w)) : residual f u = fun (v : List α) => List.drop (f u).length (f (u ++ v))

theorem Function.residual_nil {α : Type u_1} {β : Type u_2} {f : List α → List β} (h : f [] = []) : residual f [] = f

theorem Function.prefixFunction_eq_of_forall {α : Type u_1} {β : Type u_2} {f g : List α → List β} {u v : List α} {P : List β} (h : ∀ (w : List α), f (u ++ w) = P ++ g (v ++ w)) : prefixFunction f u = P ++ prefixFunction g v

If f on the extensions of u is P followed by g on the extensions of v, then its prefix function at u is P followed by that of g at v.

theorem Function.residual_eq_of_forall {α : Type u_1} {β : Type u_2} {f g : List α → List β} {u v : List α} {P : List β} (h : ∀ (w : List α), f (u ++ w) = P ++ g (v ++ w)) : residual f u = residual g v

theorem Function.residual_append {α : Type u_1} {β : Type u_2} {f : List α → List β} (u v : List α) : residual f (u ++ v) = residual (residual f u) v

Residuals compose as a right action of words, the residual by u ++ v being the residual by v of the residual by u.

Residuals through a state summary

A function that extends its output by one block per letter, the block read off a summary W of the input whose update is determined, has residuals that factor through W; conversely a prefix-preserving function whose residuals factor through W extends by blocks read off W. The strictly local function classes are the instances with W a bounded window.

theorem Function.isPrefix_append_of_append_singleton {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : ∀ (u : List α) (x : α), f u <+: f (u ++ [x])) (u v : List α) : f u <+: f (u ++ v)

A function extending its output at every letter is prefix-preserving.

theorem Function.factorsThrough_residual_of_append_singleton {α : Type u_1} {β : Type u_2} {f : List α → List β} {γ : Type u_3} {W : List α → γ} (δ : γ → α → γ) (g : γ → α → List β) (hW : ∀ (u : List α) (x : α), W (u ++ [x]) = δ (W u) x) (hf : ∀ (u : List α) (x : α), f (u ++ [x]) = f u ++ g (W u) x) : FactorsThrough (residual f) W

Residuals of a function built block by block from a state summary factor through it.

theorem Function.exists_append_singleton_of_factorsThrough_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} {γ : Type u_3} {W : List α → γ} (hpre : ∀ (u v : List α), f u <+: f (u ++ v)) (hW : FactorsThrough (residual f) W) : ∃ (g : γ → α → List β), ∀ (u : List α) (x : α), f (u ++ [x]) = f u ++ g (W u) x

A prefix-preserving function whose residuals factor through W extends by blocks read off W.

Myhill–Nerode for subsequential transducers

theorem SubsequentialTransducer.residual_run {α : Type u_1} {β : Type u_2} {σ : Type u_3} (T : SubsequentialTransducer σ α β) (u : List α) : Function.residual T.run u = Function.residual (T.runFrom (T.stateAfter T.start u)) []

Residuals of a transducer's run factor through its states.

theorem IsLeftSubsequential.finite_range_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsLeftSubsequential f) : (Set.range (Function.residual f)).Finite

theorem IsLeftSubsequential.of_finite_range_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : (Set.range (Function.residual f)).Finite) : IsLeftSubsequential f

A function with finitely many residuals is left-subsequential. The residuals are the states, each emitting its prefix function on the next letter and its value on [] at the end, and a fresh start state reads the first letter off f itself.

theorem isLeftSubsequential_iff_finite_range_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} : IsLeftSubsequential f ↔ (Set.range (Function.residual f)).Finite

Myhill–Nerode for subsequential transducers. A function is left-subsequential if and only if it has finitely many residuals ([CEH15], after Oncina and García).

theorem isRightSubsequential_iff_finite_range_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} : IsRightSubsequential f ↔ (Set.range (Function.residual (List.revConj f))).Finite

A function is right-subsequential if and only if its reverse-conjugate has finitely many residuals.

Myhill–Nerode for Mealy machines

theorem Mealy.residual_run {α : Type u_1} {β : Type u_2} {σ : Type u_3} (T : Mealy σ α β) (u : List α) : Function.residual T.run u = T.runFrom (T.stateAfter T.start u)

Residuals of a machine's run are its runs from the states it reaches.

theorem IsMealyComputable.length_eq {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsMealyComputable f) (xs : List α) : (f xs).length = xs.length

theorem IsMealyComputable.isPrefix {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsMealyComputable f) (u v : List α) : f u <+: f (u ++ v)

theorem IsMealyComputable.finite_range_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsMealyComputable f) : (Set.range (Function.residual f)).Finite

theorem isMealyComputable_of_stateSummary {α : Type u_1} {β : Type u_2} {f : List α → List β} {σ : Type u_3} [Fintype σ] (state : List α → σ) (δ : σ → α → σ) (out : σ → α → β) (hδ : ∀ (u : List α) (x : α), state (u ++ [x]) = δ (state u) x) (hout : ∀ (u : List α) (x : α) (w : List α), (f (u ++ x :: w))[u.length]? = some (out (state u) x)) (hlen : ∀ (xs : List α), (f xs).length = xs.length) : IsMealyComputable f

A length-preserving f with a finite state : List α → σ that is left-congruent (hδ) and determines f's output at each position (hout) is Mealy-computable.

theorem isMealyComputable_of_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hlen : ∀ (xs : List α), (f xs).length = xs.length) (hpre : ∀ (u v : List α), f u <+: f (u ++ v)) (hfin : (Set.range (Function.residual f)).Finite) : IsMealyComputable f

A length-preserving, prefix-preserving function with finitely many residuals is Mealy-computable, with the residuals themselves as the states.

theorem isMealyComputable_iff_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} : IsMealyComputable f ↔ (∀ (xs : List α), (f xs).length = xs.length) ∧ (∀ (u v : List α), f u <+: f (u ++ v)) ∧ (Set.range (Function.residual f)).Finite

Myhill–Nerode for Mealy machines. A function is Mealy-computable if and only if it is length-preserving, prefix-preserving, and has finitely many residuals.

Synchronous residuals and coresiduals

def Function.syncResidual {α : Type u_1} {β : Type u_2} (f : List α → List β) (u : List α) : List α → List β

The synchronous residual of f by u is the output of f on u ++ v past the first u.length symbols, the cells after u of a length-preserving f.

Equations

• Function.syncResidual f u v = List.drop u.length (f (u ++ v))

def Function.syncCoresidual {α : Type u_1} {β : Type u_2} (f : List α → List β) (y : List α) : List α → List β

The synchronous coresidual of f by y is the output of f on u ++ y up to its first u.length symbols, the cells before y of a length-preserving f.

Equations

• Function.syncCoresidual f y u = List.take u.length (f (u ++ y))

theorem Function.syncResidual_append_singleton {α : Type u_1} {β : Type u_2} (f : List α → List β) (u : List α) (x : α) : syncResidual f (u ++ [x]) = fun (v : List α) => List.drop 1 (syncResidual f u (x :: v))

theorem Function.syncCoresidual_cons {α : Type u_1} {β : Type u_2} (f : List α → List β) (x : α) (y : List α) : syncCoresidual f (x :: y) = fun (u : List α) => List.take u.length (syncCoresidual f y (u ++ [x]))

Synchronous coresiduals step by prepending a letter, the right-to-left congruence.

theorem Function.getElem?_syncResidual_cons {α : Type u_1} {β : Type u_2} (f : List α → List β) (u : List α) (x : α) (w : List α) : (syncResidual f u (x :: w))[0]? = (f (u ++ x :: w))[u.length]?

The cell at the seam, read through the synchronous residual.

theorem Function.getElem?_syncCoresidual_append {α : Type u_1} {β : Type u_2} (f : List α → List β) (u : List α) (x : α) (w : List α) : (syncCoresidual f w (u ++ [x]))[u.length]? = (f (u ++ x :: w))[u.length]?

The cell at the seam, read through the synchronous coresidual.

theorem Function.residual_eq_syncResidual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hlen : ∀ (xs : List α), (f xs).length = xs.length) (hpre : ∀ (u v : List α), f u <+: f (u ++ v)) : residual f = syncResidual f

On a length- and prefix-preserving function the residual is the synchronous residual.

Myhill–Nerode for bimachines

theorem Bimachine.lState_append {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (u v : List α) : B.lState (u ++ v) = B.lStateAfter (B.lState u) v

Scanning past a prefix reseeds the left state.

theorem Bimachine.rState_append {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (u y : List α) : B.rState (u ++ y) = { lInit := B.lInit, lStep := B.lStep, rInit := B.rState y, rStep := B.rStep, output := B.output }.rState u

A pending suffix reseeds the right state.

theorem Bimachine.drop_runFrom_append {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (w : B.LetterToLetter) (l : L) (x v : List α) : List.drop x.length (B.runFrom l (x ++ v)) = B.runFrom (B.lStateAfter l x) v

Dropping a scanned prefix of a letter-to-letter bimachine run reseeds the left state.

theorem Bimachine.take_runFrom_append {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (w : B.LetterToLetter) (l : L) (u y : List α) : List.take u.length (B.runFrom l (u ++ y)) = { lInit := B.lInit, lStep := B.lStep, rInit := B.rState y, rStep := B.rStep, output := B.output }.runFrom l u

Taking the unscanned prefix of a bimachine run reseeds the right state.

theorem Bimachine.syncResidual_run {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (w : B.LetterToLetter) (x : List α) : Function.syncResidual B.run x = B.runFrom (B.lState x)

Residuals of a bimachine's run reseed the left automaton.

theorem Bimachine.syncCoresidual_run {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (w : B.LetterToLetter) (y : List α) : Function.syncCoresidual B.run y = { lInit := B.lInit, lStep := B.lStep, rInit := B.rState y, rStep := B.rStep, output := B.output }.run

Coresiduals of a bimachine's run reseed the right automaton.

Necessity

theorem IsLengthPreservingBimachineComputable.finite_range_syncResidual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsLengthPreservingBimachineComputable f) : (Set.range (Function.syncResidual f)).Finite

theorem IsLengthPreservingBimachineComputable.finite_range_syncCoresidual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsLengthPreservingBimachineComputable f) : (Set.range (Function.syncCoresidual f)).Finite

Sufficiency

theorem isLengthPreservingBimachineComputable_of_stateSummaries {α : Type u_1} {β : Type u_2} {f : List α → List β} {L : Type u_5} {R : Type u_6} [Fintype L] [Fintype R] (stateL : List α → L) (δL : L → α → L) (stateR : List α → R) (δR : R → α → R) (out : L → α → R → β) (hδL : ∀ (u : List α) (x : α), stateL (u ++ [x]) = δL (stateL u) x) (hδR : ∀ (x : α) (w : List α), stateR (x :: w) = δR (stateR w) x) (hout : ∀ (u : List α) (x : α) (w : List α), (f (u ++ x :: w))[u.length]? = some (out (stateL u) x (stateR w))) (hlen : ∀ (xs : List α), (f xs).length = xs.length) : IsLengthPreservingBimachineComputable f

A length-preserving f with finite left and right summaries, congruent in their respective scan directions and jointly determining each output cell, is bimachine-computable.

theorem isLengthPreservingBimachineComputable_of_syncResidual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hlen : ∀ (xs : List α), (f xs).length = xs.length) (hfinL : (Set.range (Function.syncResidual f)).Finite) (hfinR : (Set.range (Function.syncCoresidual f)).Finite) : IsLengthPreservingBimachineComputable f

A length-preserving function with finitely many residuals and coresiduals is bimachine-computable, with syncResidual classes as the left states and syncCoresidual classes as the right states, and with the cell output read off representatives, which is well-defined by exchanging one context at a time.

theorem isLengthPreservingBimachineComputable_iff_syncResidual {α : Type u_1} {β : Type u_2} {f : List α → List β} : IsLengthPreservingBimachineComputable f ↔ (∀ (xs : List α), (f xs).length = xs.length) ∧ (Set.range (Function.syncResidual f)).Finite ∧ (Set.range (Function.syncCoresidual f)).Finite

Myhill–Nerode for bimachines. A function is bimachine-computable if and only if it is length-preserving with finitely many residuals and finitely many coresiduals.