Documentation

Linglib.Theories.Phonology.OptimalityTheory.StratalCorr

Stratal OT ↔ Corr ↔ TCT — Architectural Bridge #

@cite{kiparsky-2000} @cite{benua-1997}

The substrate-level integration between Stratal OT (@cite{kiparsky-2000}) and TCT (@cite{benua-1997}) over the unifying Corr Role α substrate.

The polemic of @cite{benua-1997} #

Benua's thesis defends a strong architectural claim: for every stratal analysis there exists a TCT analysis producing the same surface predictions. The two architectures explain misapplication patterns (over- and underapplication) for different structural reasons but converge on the same outputs:

Stratal: misapplication is epiphenomenal — at cycle 1 the rule applies (or doesn't) under the stratum's grammar; at cycle 2 the rule sees the cycle-1 output as input, and IDENT-IO at the higher stratum preserves features. The misapplication "comes for free" from the chain of cycles.
TCT: misapplication is primitive — a single parallel evaluation with high-ranked OO-Faith forcing the derivative to match the base. The cycles are eliminated; the chain becomes a pair of correspondence-related forms.

What this file provides #

The structural bridge: stratal derivations and TCT diagrams are both Corr Role α instances over different role enums, with a canonical projection between them. Specifically:

StratalRole enum encodes the four salient time-points of a stratal derivation: stem-input, stem-output, word-output, phrase-output.
StratalDerivation.toCorr packages a 3-stratum derivation as a Corr StratalRole α with feeding edges between adjacent strata.
stratalToTCTRole projects a stratal role onto the corresponding TCT role: stem-output ↦ base, phrase-output ↦ derivative. The project function then carries this to a Corr TCT.Role α.
The bridge theorem project_preserves_phrase_as_derivative makes the identification "stratal phrase-output = TCT derivative" true by construction.

What this file does NOT yet provide #

The grammar-level bridge: a constructive translation stratalToTCT : StratalGrammar → TCTGrammar such that for all inputs, their surface predictions agree. That requires modeling each architecture's grammar (constraint rankings + GEN/EVAL machinery) as a function Input → Output, then proving the translation respects that function. Documented as the next major scientific step.

This file establishes the substrate so that future work can state the grammar bridge in shared types — currently StratalDerivation and Corr TCT.Role α live in non-communicating namespaces.

inductive Phonology.Stratal.StratalRole :

Roles for a stratal correspondence diagram. Each stratum has an output (the result of evaluating that stratum's grammar); the stem also has an input (the underlying form). Word- and phrase-stratum inputs are identical to the previous stratum's output (the feeding relation), so they need no separate role.

Four roles:

.sIn — stem-stratum input (= underlying form)
.sOut — stem-stratum output
.wOut — word-stratum output
.pOut — phrase-stratum output (= surface form)

sIn : StratalRole
sOut : StratalRole
wOut : StratalRole
pOut : StratalRole

Instances For

@[implicit_reducible]

instance Phonology.Stratal.instDecidableEqStratalRole :

DecidableEq StratalRole

Equations

Phonology.Stratal.instDecidableEqStratalRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phonology.Stratal.instReprStratalRole.repr :

StratalRole → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Phonology.Stratal.instReprStratalRole :

Repr StratalRole

Equations

Phonology.Stratal.instReprStratalRole = { reprPrec := Phonology.Stratal.instReprStratalRole.repr }

def Phonology.Stratal.StratalRole.label :

StratalRole → String

Display label for a stratal role.

Equations

Phonology.Stratal.StratalRole.sIn.label = "Stem-In"
Phonology.Stratal.StratalRole.sOut.label = "Stem-Out"
Phonology.Stratal.StratalRole.wOut.label = "Word-Out"
Phonology.Stratal.StratalRole.pOut.label = "Phrase-Out"

Instances For

def Phonology.Stratal.parallelEdge {α : Type u_1} (s₁ s₂ : List α) :

Finset (ℕ × ℕ)

Build the parallel-pair edge between two equal-or-shorter forms: (0, 0), (1, 1), … up to the shorter length. The substrate edge type for both within-stratum (IO-correspondence) and cross-stratum (feeding) relations.

Equations

Phonology.Stratal.parallelEdge s₁ s₂ = Finset.image (fun (i : ℕ) => (i, i)) (Finset.range (min s₁.length s₂.length))

Instances For

theorem Phonology.Stratal.parallelEdge_wf {α : Type u_1} (s₁ s₂ : List α) (p : ℕ × ℕ) :

p ∈ parallelEdge s₁ s₂ → p.1 < s₁.length ∧ p.2 < s₂.length

A stratal derivation over a uniform segment type α, packaged as a Corr StratalRole α. The cross-role edges encode:

- `(.sIn ↔ .sOut)`: stem-stratum IO-correspondence
- `(.sOut ↔ .wOut)`: stem feeds word
- `(.wOut ↔ .pOut)`: word feeds phrase

All other role pairs (e.g., `(.sIn, .wOut)` direct) are empty —
the feeding chain is captured by composing adjacent edges, not by
direct cross-stratum correspondence. (Direct edges would be
available via `Quiver.Path`; see `RoleQuiv` in `Correspondence.lean`.)

Specialized to homogeneous candidate types; the heterogeneous case
`StratalDerivation S W P` doesn't fit `Corr Role α` directly without
a uniform encoding.

def Phonology.Stratal.adjacentStrata :

StratalRole → StratalRole → Bool

Adjacent strata in a 4-role chain: .sIn ↔ .sOut, .sOut ↔ .wOut, .wOut ↔ .pOut. The chain-shape predicate for Corr.diagram.

Equations

Instances For

def Phonology.Stratal.stratalDerivToCorr {α : Type} (input stemOut wordOut phraseOut : List α) :

Correspondence.Corr StratalRole α

A stratal derivation as a 4-role Corr StratalRole α, with parallel-pair feeding edges along the adjacent-strata chain. Defined via Corr.diagram with the adjacentStrata predicate. The pre-Stage-2 hand-rolled version had ~50 LOC of match + wf boilerplate including 3 redundant swap-image clauses (no-ops since parallel-pair edges are symmetric).

Equations

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

Instances For

@[simp]

theorem Phonology.Stratal.stratalDerivToCorr_form_sIn {α : Type} (input stemOut wordOut phraseOut : List α) :

(stratalDerivToCorr input stemOut wordOut phraseOut).form StratalRole.sIn = input

@[simp]

theorem Phonology.Stratal.stratalDerivToCorr_form_sOut {α : Type} (input stemOut wordOut phraseOut : List α) :

(stratalDerivToCorr input stemOut wordOut phraseOut).form StratalRole.sOut = stemOut

@[simp]

theorem Phonology.Stratal.stratalDerivToCorr_form_wOut {α : Type} (input stemOut wordOut phraseOut : List α) :

(stratalDerivToCorr input stemOut wordOut phraseOut).form StratalRole.wOut = wordOut

@[simp]

theorem Phonology.Stratal.stratalDerivToCorr_form_pOut {α : Type} (input stemOut wordOut phraseOut : List α) :

(stratalDerivToCorr input stemOut wordOut phraseOut).form StratalRole.pOut = phraseOut

def Phonology.StratalToTCT.stratalToTCTRole :

Stratal.StratalRole → Option TCT.Role

The canonical projection from stratal roles to TCT roles, encoding Benua's identification:

.sIn (underlying form) → .input
.sOut (stem output, the morphologically simpler related word) → .base
.pOut (phrase output, the surface of the complex form) → .derivative

The .wOut role has no TCT counterpart — TCT does not distinguish a "word stratum" between base and derivative. In Benua's reduction of stratal-to-parallel, the word-level evaluation is folded into the derivative's parallel evaluation against the frozen stem-output base.

Returns none for .wOut; consumers must specify how to handle intermediate strata when projecting to TCT.

Equations

Instances For

def Phonology.StratalToTCT.project {α : Type} (input stemOut wordOut phraseOut : List α) :

Correspondence.Corr TCT.Role α

Project a stratal correspondence diagram down to a 3-role TCT diagram. The .wOut form is dropped; the OO-correspondence between .sOut and .pOut is reconstructed as the parallel-pair correspondence between c.form .sOut and c.form .pOut (truncated by min).

Defined via Corr.diagram with off-diagonal edge predicate.

Equations

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

Instances For

theorem Phonology.StratalToTCT.project_preserves_phrase_as_derivative {α : Type} (input stemOut wordOut phraseOut : List α) :

(project input stemOut wordOut phraseOut).form TCT.Role.derivative = phraseOut

The phrase output of a stratal derivation equals the derivative form of its TCT projection. The structural content of Benua's architectural-equivalence claim: stratal's surface form is TCT's derivative output, by construction of the projection.

True by rfl because the projection defines .derivative ↦ phraseOut directly. The empirical content — that grammar-derived surface forms agree under the translation — requires the deferred stratalToTCT : StratalGrammar → TCTGrammar constructive translation.

theorem Phonology.StratalToTCT.project_preserves_stem_as_base {α : Type} (input stemOut wordOut phraseOut : List α) :

(project input stemOut wordOut phraseOut).form TCT.Role.base = stemOut

The stem output of a stratal derivation equals the base form of its TCT projection. The other half of Benua's identification: stratal's stem-stratum result is TCT's frozen base.

theorem Phonology.StratalToTCT.project_preserves_underlying_as_input {α : Type} (input stemOut wordOut phraseOut : List α) :

(project input stemOut wordOut phraseOut).form TCT.Role.input = input

The underlying form (stem input) maps to TCT's input.

theorem Phonology.StratalToTCT.project_oo_edge_eq_parallel {α : Type} (input stemOut wordOut phraseOut : List α) :

(project input stemOut wordOut phraseOut).edge TCT.Role.base TCT.Role.derivative = Stratal.parallelEdge stemOut phraseOut

The bridge theorem: the OO-correspondence edge in the projected TCT diagram (between .base and .derivative) is the parallel-pair correspondence between stemOut and phraseOut. This is the formal content of "stem-output IS the OO-base for the phrase output" — Benua's claim that the OO-correspondence in TCT replaces the chain of cycles in stratal.