Documentation

Studies.LamontOHaraSmith2019

Lamont, O'Hara and Smith (2019): Weakly deterministic transformations are subregular #

Unbounded tonal plateauing turns every toneless unit between two high tones into a high tone, so the fate of a target depends on material unboundedly far away on both sides. Heinz and Lai, and Jardine after them, conjectured that such maps are not weakly deterministic. Lamont, O'Hara and Smith show that plateauing is weakly deterministic in Heinz and Lai's sense (Figure 1). A left-to-right pass that preserves length and alphabet rewrites every HLH as HHH, so that HLH never survives it, and then writes HLH as a code for an H with another H to its left; a right-to-left pass decodes it.

Main definitions #

markLeft, resolveRight: the transducers A and B of Figure 1

Main results #

utp_map_eq_resolve_mark: B after A computes plateauing
length_markLeft_run: A preserves length
utp_isWeaklyDeterministic: plateauing is weakly deterministic

Implementation notes #

A toneless unit is Tone.TBU.O, the paper's L. Since SubsequentialTransducer.runRight reverses the run, B's blocks are written reversed. The figure gives B no H transition from q4; A never writes an H there, and B keeps it.
The proof splits a word into Ls, an H, blocks Lʲ H, and Ls. A writes each block as H, HH or Lʲ⁻² HLH, and B, reading right to left, holds back at most one H.
Not formalized: §2, where first-last plateauing and double-edged spread are shown regular but not weakly deterministic by a counting argument, and the characterization of Theorem 3.1.

References #

The transducers #

inductive LamontOHaraSmith2019.MarkState :

A is in q0 before any H, in q1 after an H with nothing held back, in q2 holding back one L, and in q3 having held back two.

Instances For

@[instance_reducible]

instance LamontOHaraSmith2019.instDecidableEqMarkState :

DecidableEq MarkState

Equations

LamontOHaraSmith2019.instDecidableEqMarkState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LamontOHaraSmith2019.instReprMarkState :

Equations

LamontOHaraSmith2019.instReprMarkState = { reprPrec := LamontOHaraSmith2019.instReprMarkState.repr }

def LamontOHaraSmith2019.instReprMarkState.repr :

MarkState → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

@[instance_reducible]

instance LamontOHaraSmith2019.instFintypeMarkState :

Fintype MarkState

Equations

One or more equations did not get rendered due to their size.

def LamontOHaraSmith2019.markStep :

MarkState → Tone.TBU → MarkState

The transitions of A.

Equations

Instances For

def LamontOHaraSmith2019.markFinal :

MarkState → List Tone.TBU

What A writes at the end of the word, the Ls it holds back.

Equations

Instances For

def LamontOHaraSmith2019.markLeft :

SubsequentialTransducer MarkState Tone.TBU Tone.TBU

Transducer A of Figure 1, the left-to-right pass.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem LamontOHaraSmith2019.markLeft_start :

markLeft.start = MarkState.q0

@[simp]

theorem LamontOHaraSmith2019.markLeft_step :

markLeft.step = markStep

@[simp]

theorem LamontOHaraSmith2019.markLeft_output :

markLeft.output = markOutput

@[simp]

theorem LamontOHaraSmith2019.markLeft_finalOutput :

markLeft.finalOutput = markFinal

inductive LamontOHaraSmith2019.ResolveState :

Reading right to left, B is in q0 before any H, in q1 holding back an H, in q2 holding back an L and an H, in q3 inside a plateau, and in q4 past the last code.

Instances For

@[instance_reducible]

instance LamontOHaraSmith2019.instDecidableEqResolveState :

DecidableEq ResolveState

Equations

LamontOHaraSmith2019.instDecidableEqResolveState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LamontOHaraSmith2019.instReprResolveState :

Repr ResolveState

Equations

LamontOHaraSmith2019.instReprResolveState = { reprPrec := LamontOHaraSmith2019.instReprResolveState.repr }

def LamontOHaraSmith2019.instReprResolveState.repr :

ResolveState → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

@[instance_reducible]

instance LamontOHaraSmith2019.instFintypeResolveState :

Fintype ResolveState

Equations

One or more equations did not get rendered due to their size.

def LamontOHaraSmith2019.resolveStep :

ResolveState → Tone.TBU → ResolveState

The transitions of B.

Equations

Instances For

def LamontOHaraSmith2019.resolveOutput :

ResolveState → Tone.TBU → List Tone.TBU

The blocks B writes, each reversed.

Equations

Instances For

def LamontOHaraSmith2019.resolveFinal :

ResolveState → List Tone.TBU

What B writes at the end of the word, reversed.

Equations

Instances For

def LamontOHaraSmith2019.resolveRight :

SubsequentialTransducer ResolveState Tone.TBU Tone.TBU

Transducer B of Figure 1, the right-to-left pass, as run by runRight.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem LamontOHaraSmith2019.resolveRight_start :

resolveRight.start = ResolveState.q0

@[simp]

theorem LamontOHaraSmith2019.resolveRight_step :

resolveRight.step = resolveStep

@[simp]

theorem LamontOHaraSmith2019.resolveRight_output :

resolveRight.output = resolveOutput

@[simp]

theorem LamontOHaraSmith2019.resolveRight_finalOutput :

resolveRight.finalOutput = resolveFinal

The first pass #

The second pass #

Plateauing #

theorem LamontOHaraSmith2019.utp_map_eq_resolve_mark (w : List Tone.TBU) :

Tone.utp.map w = resolveRight.runRight (markLeft.run w)

B after A computes unbounded tonal plateauing (Figure 1).

theorem LamontOHaraSmith2019.length_markLeft_run (w : List Tone.TBU) :

(markLeft.run w).length = w.length

A preserves length.

theorem LamontOHaraSmith2019.utp_isWeaklyDeterministic :

IsWeaklyDeterministic Tone.utp.map

Unbounded tonal plateauing is weakly deterministic in Heinz and Lai's sense.