Scan direction

The orientation of a left-to-right vs right-to-left scan, shared by the transducer machines and the side-determinacy predicates of the subregular function theory, with the window of positions a direction cuts around a target coordinate, and the reverse conjugation revConj realizing the flip on string functions. Extracted to its own leaf so the footprint-predicate file (Dependence.lean) does not have to depend on the transducer machine file just to name a left/right tag.

inductive ScanDirection : Type

The orientation of an FST scan: left consumes input head-first, right tail-first (via List.reverse conjugation). The two scan modes give rise to distinct function classes — isomorphic under reversal but not equal as subclasses of the rational functions over un-reversed strings.

• left : ScanDirection
• right : ScanDirection

@[instance_reducible]

instance instDecidableEqScanDirection : DecidableEq ScanDirection

Equations

• instDecidableEqScanDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprScanDirection.repr : ScanDirection → ℕ → Std.Format

Equations

• instReprScanDirection.repr ScanDirection.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ScanDirection.left")).group prec✝
• instReprScanDirection.repr ScanDirection.right prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ScanDirection.right")).group prec✝

@[instance_reducible]

instance instReprScanDirection : Repr ScanDirection

Equations

• instReprScanDirection = { reprPrec := instReprScanDirection.repr }

def ScanDirection.window : ScanDirection → ℕ → ℕ → Set ℕ

The input positions not d-far from target i on side s.

Equations

• ScanDirection.left.window x✝¹ x✝ = Set.Ici (x✝¹ - x✝)
• ScanDirection.right.window x✝¹ x✝ = Set.Iic (x✝¹ + x✝)

@[simp]

theorem ScanDirection.window_left {i d : ℕ} : left.window i d = Set.Ici (i - d)

@[simp]

theorem ScanDirection.window_right {i d : ℕ} : right.window i d = Set.Iic (i + d)

Reverse conjugation

The action of flipping scan direction on string functions: right-scan function classes are the List.revConj-images of the left-scan ones, so their theory transports along the involution rather than being restated.

def List.revConj {α : Type u_1} {β : Type u_2} (f : List α → List β) : List α → List β

Conjugation by List.reverse: compute on the reversed input, reverse the result.

Equations

• List.revConj f xs = (f xs.reverse).reverse

@[simp]

theorem List.revConj_revConj {α : Type u_1} {β : Type u_2} (f : List α → List β) : revConj (revConj f) = f

theorem List.revConj_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : List β → List γ) (f : List α → List β) : revConj (g ∘ f) = revConj g ∘ revConj f

@[simp]

theorem List.revConj_id {α : Type u_1} : revConj id = id

theorem List.revConj_eq_iff {α : Type u_1} {β : Type u_2} {h f : List α → List β} : revConj h = f ↔ h = revConj f