Optimality Theory — Core Vocabulary

OT-specific vocabulary layered on Core.Logic.ConstraintEvaluation. Provides named constraints with a faithfulness/markedness distinction, convenience constructors for building tableaux from ranked constraint lists, and factorial typology computation.

Connection to ConstraintEvaluation

ConstraintEvaluation provides the generic engine (lexLE, OTTableau, OTTableau.optimal). This module adds OT-specific structure: constraint families, named constraints, and the factorial typology pattern (enumerate all rankings, compute optima, count distinct outcomes).

inductive Core.OT.ConstraintFamily : Type

Constraint families in OT.

• faithfulness : ConstraintFamily

  Faithfulness: penalizes deviation from the input.

• markedness : ConstraintFamily

  Markedness: penalizes marked structures in the output.

instance Core.OT.instDecidableEqConstraintFamily : DecidableEq ConstraintFamily

Equations

• Core.OT.instDecidableEqConstraintFamily x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.OT.instBEqConstraintFamily.beq : ConstraintFamily → ConstraintFamily → Bool

Equations

• Core.OT.instBEqConstraintFamily.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.OT.instBEqConstraintFamily : BEq ConstraintFamily

Equations

• Core.OT.instBEqConstraintFamily = { beq := Core.OT.instBEqConstraintFamily.beq }

def Core.OT.instReprConstraintFamily.repr : ConstraintFamily → Nat → Std.Format

Equations

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

instance Core.OT.instReprConstraintFamily : Repr ConstraintFamily

Equations

• Core.OT.instReprConstraintFamily = { reprPrec := Core.OT.instReprConstraintFamily.repr }

structure Core.OT.NamedConstraint (C : Type) : Type

A named OT constraint with family classification. eval c returns the number of violations candidate c incurs.

• name : String
• family : ConstraintFamily
• eval : C → Nat

def Core.OT.buildProfile {C : Type} (ranking : List (NamedConstraint C)) (c : C) : List Nat

Build a violation profile from a ranked list of named constraints. Position 0 = highest-ranked constraint.

Equations

• Core.OT.buildProfile ranking c = List.map (fun (con : Core.OT.NamedConstraint C) => con.eval c) ranking

def Core.OT.buildTableau {C : Type} (candidates : List C) (ranking : List (NamedConstraint C)) (h : candidates ≠ []) : ConstraintEvaluation.OTTableau C

Build an OT tableau from a candidate list and a constraint ranking.

Equations

• Core.OT.buildTableau candidates ranking h = { candidates := candidates, profile := Core.OT.buildProfile ranking, nonempty := h }

def Core.OT.permutations {α : Type} : List α → List (List α)

All permutations of a list.

Equations

• Core.OT.permutations [] = [[]]
• Core.OT.permutations (x_1 :: xs) = List.flatMap (Core.OT.insertEverywhere✝ x_1) (Core.OT.permutations xs)

def Core.OT.factorialOptima {C : Type} [DecidableEq C] (candidates : List C) (constraints : List (NamedConstraint C)) (h : candidates ≠ []) : List (List C)

For each permutation of constraints, compute the set of optimal candidates. Return the list of distinct optimal sets.

This is the core of OT factorial typology: the number of distinct optimal sets equals the number of language types predicted by the constraint set.

Equations

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

def Core.OT.factorialTypologySize {C : Type} [DecidableEq C] (candidates : List C) (constraints : List (NamedConstraint C)) (h : candidates ≠ []) : Nat

Number of distinct language types predicted by the factorial typology. Equals |factorialOptima|.

Equations

• Core.OT.factorialTypologySize candidates constraints h = (Core.OT.factorialOptima candidates constraints h).length