Documentation

Linglib.Core.Constraint.OT.EvalMode

OT — Evaluation Mode (Parallel vs Directional) #

@cite{eisner-2000} @cite{eisner-2002} @cite{lamont-2022a} @cite{lamont-2022b}

Encodes @cite{lamont-2022b}'s reframing: directionality is a property of EVAL, not of constraints. We do not define DirectionalConstraint C := C → List Nat — that is the obsolete constraint-side encoding. Instead, an EvalMode parameter governs how violation profiles are lex-compared.

Encoding convention #

A constraint's violation profile is a List Nat interpreted as an indicator vector: position i of the list records the violation status at position i of the form. For binary violations, entries are 0 (no violation) or 1 (violation present). For gradient violations, entries are arbitrary Nats.

Under this convention:

Why no sorting #

An earlier version of this file sorted position vectors ascending before lex-comparing under directional .leftToRight. That destroyed the position information: for input /kāk^H + rī^H + dō^H/ (paper, fig. 3), the three depth-1 candidates have indicator vectors [0,1,1], [1,0,1], [1,1,0] — all sort to [0,1,1], making them indistinguishable. The correct semantics is plain LexLE on the position-ordered indicator (no sorting): then [0,1,1] < [1,0,1] < [1,1,0] lex, picking the leftmost-deletion candidate as the winner — which is what @cite{mcpherson-lamont-2026} require.

The forgetful map count := positions.length lets a counting constraint embed cleanly into the directional setting as the degenerate case where every violation collapses to a single tally. The EvalMode.le_singleton theorem is the structural soundness statement: when comparing two single-violation profiles, all EvalModes agree with Nat ≤. Note: multi-violation profiles distinguish the modes — the paper's whole argument (paper, eqs. 60–62) hinges on parallel and directional eval giving different winners for /kāk^H + rī^H + dō^H/.

Why this lives in Core/Constraint/OT/ rather than Phonology/ #

EvalMode is a property of the OT evaluation procedure, not of the phonology-specific candidate type. Like ERC, it lives at the framework layer so that future phonology-, syntax-, and pragmatics-side users can share one notion of directional EVAL.

Sibling, not refactor #

This file does not modify NamedConstraint.eval : C → Nat (which is load-bearing for Weighted.lean/MaxEnt.lean/NoisyHG.lean — see Core/Constraint/Evaluation.lean). The directional dispatch is consumed by HarmonicSerialism.lean's combinator, which currently routes the directional arm to the parallel optimum as a stub; a true DirectionalTableau consumer lands when a study file requires it.

source
inductive Core.Constraint.OT.Direction :
Type

Direction of lex comparison on violation position vectors. @cite{eisner-2000} §3, @cite{eisner-2002}.

Instances For
    source
    @[implicit_reducible]
    instance Core.Constraint.OT.instDecidableEqDirection :
    DecidableEq Direction
    Equations
    source
    @[implicit_reducible]
    instance Core.Constraint.OT.instReprDirection :
    Repr Direction
    Equations
    source
    def Core.Constraint.OT.instReprDirection.repr :
    Direction → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Core.Constraint.OT.instInhabitedDirection.default :
      Direction
      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Core.Constraint.OT.instInhabitedDirection :
        Inhabited Direction
        Equations
        source
        inductive Core.Constraint.OT.EvalMode :
        Type

        Evaluation mode for the OT EVAL function.

        parallel is classical @cite{prince-smolensky-1993} OT. directional instances correspond to @cite{eisner-2000}'s direction of evaluation; @cite{lamont-2022b} reframes directionality as a property of EVAL (not of constraints), and shows it is needed to break ties locally without invoking globally-aware tie-breakers.

        Instances For
          source
          def Core.Constraint.OT.instDecidableEqEvalMode.decEq (x✝ x✝¹ : EvalMode) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            @[implicit_reducible]
            instance Core.Constraint.OT.instDecidableEqEvalMode :
            DecidableEq EvalMode
            Equations
            source
            def Core.Constraint.OT.instReprEvalMode.repr :
            EvalMode → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[implicit_reducible]
              instance Core.Constraint.OT.instReprEvalMode :
              Repr EvalMode
              Equations
              source
              def Core.Constraint.OT.instInhabitedEvalMode.default :
              EvalMode
              Equations
              Instances For
                source
                @[implicit_reducible]
                instance Core.Constraint.OT.instInhabitedEvalMode :
                Inhabited EvalMode
                Equations
                source
                def Core.Constraint.OT.EvalMode.le :
                EvalMode → List ℕ → List ℕ → Prop

                Compare two indicator-vector violation profiles under an EvalMode, returning a Prop (decidable). The result EvalMode.le m a b reads "candidate a is at least as harmonic as candidate b under m."

                Convention: a, b : List Nat are indicator vectors with positions in left-to-right order (entry i = violation status at position i of the form). For parallel constraints, the convention is a singleton [count]; the modes coincide on singletons.

                • parallel: LexLE a b directly (Layered Grounding).
                • directional .leftToRight: LexLE a b — same as parallel, because the convention puts positions in left-to-right order already, and LexLE compares from the leftmost entry.
                • directional .rightToLeft: LexLE a.reverse b.reverse — compare from the rightmost entry by reversing both vectors.

                The substrate keeps parallel and directional .leftToRight as distinct EvalMode cases (even though le is the same function for them) so that downstream consumers can dispatch on the mode at higher levels (e.g., a DirectionalTableau may ONLY accept directional modes; a count-based Tableau may ONLY accept parallel).

                Equations
                Instances For
                  source
                  @[implicit_reducible]
                  instance Core.Constraint.OT.EvalMode.instDecidableLe (m : EvalMode) (a b : List ℕ) :
                  Decidable (m.le a b)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  theorem Core.Constraint.OT.EvalMode.le_singleton (m : EvalMode) (k k' : ℕ) :
                  m.le [k] [k'] ↔ k ≤ k'

                  Single-violation degeneracy. When comparing two profiles each consisting of a single violation count [k] and [k'], all EvalModes agree with Nat ≤. This is the structural reason that a counting constraint (which records [k] for k violations as a single position-vector slot) embeds cleanly into the directional setting as a degenerate case — and the algebraic justification for why NamedConstraint.eval : C → Nat (count-based) and the directional indicator-vector encoding agree on simple cases.