Weak determinism

A function on strings over one alphabet is weakly deterministic, in Heinz and Lai's sense, when it is a right-subsequential function after a left-subsequential one that never lengthens its input. The length bound keeps the first pass from marking up its output: Elgot and Mezei's decomposition of an arbitrary regular function needs new symbols in between, and over an alphabet of two or more letters new symbols can be coded as longer strings. Subsequential functions that do not lengthen their input are weakly deterministic, and a weakly deterministic function that preserves the empty word is regular. Later rival classes are named for their mechanisms, such as the non-interacting bimachines of IsNonInteractingBimachineComputable.

Main definitions

• IsWeaklyDeterministic f: f is a right-subsequential function after a left-subsequential one that does not lengthen its input

Main results

• IsRightSubsequential.isWeaklyDeterministic, IsLeftSubsequential.isWeaklyDeterministic: subsequential functions that do not lengthen their input are weakly deterministic
• IsWeaklyDeterministic.isBimachineComputable: weakly deterministic functions preserving the empty word are regular

Implementation notes

Heinz and Lai's Corollary 1 places every subsequential function in the class. With the length bound on the first pass the left-subsequential half is proved here only for functions that do not lengthen their input.

References

• [HL13]
• [EM65]

def IsWeaklyDeterministic {α : Type u_1} (f : List α → List α) : Prop

f is weakly deterministic when it is a right-subsequential function after a left-subsequential one, over the alphabet of f, whose first pass never lengthens its input.

Equations

• IsWeaklyDeterministic f = ∃ (L : List α → List α) (R : List α → List α), IsLeftSubsequential L ∧ (∀ (x : List α), (L x).length ≤ x.length) ∧ IsRightSubsequential R ∧ R ∘ L = f

theorem IsRightSubsequential.isWeaklyDeterministic {α : Type u_1} {f : List α → List α} (hf : IsRightSubsequential f) : IsWeaklyDeterministic f

A right-subsequential function is weakly deterministic, after the identity.

theorem IsLeftSubsequential.isWeaklyDeterministic {α : Type u_1} {f : List α → List α} (hf : IsLeftSubsequential f) (hlen : ∀ (x : List α), (f x).length ≤ x.length) : IsWeaklyDeterministic f

A left-subsequential function that does not lengthen its input is weakly deterministic, before the identity.

theorem IsWeaklyDeterministic.isBimachineComputable {α : Type u_1} {f : List α → List α} (hf : IsWeaklyDeterministic f) (hnil : f [] = []) : IsBimachineComputable f

A weakly deterministic function that preserves the empty word is computed by a bimachine.