Benua (1997): the stratal ↔ TCT architectural equivalence

[Kip00] [Ben97]

The stratal-OT ↔ TCT correspondence that [Ben97] argues for, formalized over the shared Corr Role α substrate. (Paper-anchored to [Ben97]; consumed only by this study, so it lives in the study directory, not the OT theory layer.)

The substrate-level integration between Stratal OT ([Kip00]) and TCT ([Ben97]) over the unifying Corr Role α substrate.

The polemic of [Ben97]

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 Benua1997.StratalCorr.StratalRole : Type

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

@[implicit_reducible]

instance Benua1997.StratalCorr.instDecidableEqStratalRole : DecidableEq StratalRole

Equations

• Benua1997.StratalCorr.instDecidableEqStratalRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Benua1997.StratalCorr.instReprStratalRole.repr : StratalRole → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Benua1997.StratalCorr.instReprStratalRole : Repr StratalRole

Equations

• Benua1997.StratalCorr.instReprStratalRole = { reprPrec := Benua1997.StratalCorr.instReprStratalRole.repr }

def Benua1997.StratalCorr.StratalRole.label : StratalRole → String

Display label for a stratal role.

Equations

• Benua1997.StratalCorr.StratalRole.sIn.label = "Stem-In"
• Benua1997.StratalCorr.StratalRole.sOut.label = "Stem-Out"
• Benua1997.StratalCorr.StratalRole.wOut.label = "Word-Out"
• Benua1997.StratalCorr.StratalRole.pOut.label = "Phrase-Out"

def Benua1997.StratalCorr.parallelEdge {α : Type u_1} (s₁ s₂ : List α) : Finset (Fin s₁.length × Fin s₂.length)

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. The in-range bound is carried by the Fin-indexed type (Corr.diagDiag), so no separate well-formedness lemma is needed.

Equations

• Benua1997.StratalCorr.parallelEdge s₁ s₂ = OptimalityTheory.Correspondence.Corr.diagDiag s₁.length 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 Benua1997.StratalCorr.adjacentStrata (a b : StratalRole) : Prop

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

Equations

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

@[implicit_reducible]

instance Benua1997.StratalCorr.instDecidableRelStratalRoleAdjacentStrata : DecidableRel adjacentStrata

Equations

• Benua1997.StratalCorr.instDecidableRelStratalRoleAdjacentStrata a b = id inferInstance

def Benua1997.StratalCorr.stratalDerivToCorr {α : Type u_1} (input stemOut wordOut phraseOut : List α) : OptimalityTheory.Correspondence.Corr StratalRole α

A stratal derivation as a 4-role Corr StratalRole α, with parallel-pair feeding edges along the adjacent-strata chain (via Corr.diagram with the adjacentStrata predicate).

Equations

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

@[simp]

theorem Benua1997.StratalCorr.stratalDerivToCorr_form_sIn {α : Type u_1} (input stemOut wordOut phraseOut : List α) : (stratalDerivToCorr input stemOut wordOut phraseOut).form StratalRole.sIn = input

@[simp]

theorem Benua1997.StratalCorr.stratalDerivToCorr_form_sOut {α : Type u_1} (input stemOut wordOut phraseOut : List α) : (stratalDerivToCorr input stemOut wordOut phraseOut).form StratalRole.sOut = stemOut

@[simp]

theorem Benua1997.StratalCorr.stratalDerivToCorr_form_wOut {α : Type u_1} (input stemOut wordOut phraseOut : List α) : (stratalDerivToCorr input stemOut wordOut phraseOut).form StratalRole.wOut = wordOut

@[simp]

theorem Benua1997.StratalCorr.stratalDerivToCorr_form_pOut {α : Type u_1} (input stemOut wordOut phraseOut : List α) : (stratalDerivToCorr input stemOut wordOut phraseOut).form StratalRole.pOut = phraseOut

def Benua1997.StratalToTCT.stratalToTCTRole : StratalCorr.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

• Benua1997.StratalToTCT.stratalToTCTRole Benua1997.StratalCorr.StratalRole.sIn = some Benua1997.TCT.Role.input
• Benua1997.StratalToTCT.stratalToTCTRole Benua1997.StratalCorr.StratalRole.sOut = some Benua1997.TCT.Role.base
• Benua1997.StratalToTCT.stratalToTCTRole Benua1997.StratalCorr.StratalRole.wOut = none
• Benua1997.StratalToTCT.stratalToTCTRole Benua1997.StratalCorr.StratalRole.pOut = some Benua1997.TCT.Role.derivative

def Benua1997.StratalToTCT.project {α : Type u_1} (input stemOut wordOut phraseOut : List α) : OptimalityTheory.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.

theorem Benua1997.StratalToTCT.project_preserves_phrase_as_derivative {α : Type u_1} (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 Benua1997.StratalToTCT.project_preserves_stem_as_base {α : Type u_1} (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 Benua1997.StratalToTCT.project_preserves_underlying_as_input {α : Type u_1} (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 Benua1997.StratalToTCT.project_oo_edge_eq_parallel {α : Type u_1} (input stemOut wordOut phraseOut : List α) : (project input stemOut wordOut phraseOut).edge TCT.Role.base TCT.Role.derivative = StratalCorr.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.