Constraint Systems — The Unified Interface

A ConstraintSystem packages the three components of any constraint-based grammar into a single record:

1. a finite candidate set,
2. a score function (whatever value type the framework needs), and
3. a decoder that turns scored candidates into a probability distribution.

  Candidates  ──score──▶  Score   ──decoder──▶   P : Cand → ℝ

Different frameworks differ only in what they pick for each component. Smart constructors below assemble the standard frameworks:

• otSystem — OT: Score = LexProfile Nat n, decoder = argminDecoder
• hgSystem — HG: Score = ℝ, decoder = argmaxDecoder
• maxEntSystem — MaxEnt: Score = ℝ, decoder = softmaxDecoder α

Every system exposes a single predict operation, so downstream code can compare frameworks (or replace one with another) without touching the rest of the analysis.

Stochastic frameworks that put noise on weights or candidates (NHG, Normal MaxEnt, Stochastic OT) are RUM specializations: the noise kernel composes with the deterministic decoder. See NoiseKernel.lean for the Dirac / Gumbel / Gaussian bridges.

structure Core.Constraint.ConstraintSystem (Cand : Type u_1) (Score : Type u_2) : Type (max u_1 u_2)

A constraint-based grammar: candidate set + score function + decoder.

Cand is the candidate type (often something like an output form, a syntactic structure, or an input/output pair). Score is whatever value the constraints aggregate to — ℝ for HG/MaxEnt, LexProfile Nat n for OT, etc.

• candidates : Finset Cand

  The finite set of candidates this system evaluates.

• score : Cand → Score

  The aggregated score for each candidate.

• decoder : Decoder Cand Score

  The choice rule: scored candidates → probability distribution.

def Core.Constraint.ConstraintSystem.predict {Cand : Type u_1} {Score : Type u_2} (s : ConstraintSystem Cand Score) : Cand → ℝ

The predicted probability of each candidate.

Equations

• s.predict = s.decoder.decode s.candidates s.score

theorem Core.Constraint.ConstraintSystem.predict_nonneg {Cand : Type u_1} {Score : Type u_2} (s : ConstraintSystem Cand Score) [s.decoder.IsProb] (c : Cand) : 0 ≤ s.predict c

A system whose decoder is IsProb produces non-negative predictions.

theorem Core.Constraint.ConstraintSystem.predict_sum_eq_one {Cand : Type u_1} {Score : Type u_2} (s : ConstraintSystem Cand Score) [s.decoder.IsProb] (hne : s.candidates.Nonempty) : ∑ c ∈ s.candidates, s.predict c = 1

A system whose decoder is IsProb predicts a probability distribution over its candidate set.

noncomputable def Core.Constraint.otSystem {Cand : Type u_1} {n : ℕ} (candidates : Finset Cand) (profile : Cand → LexProfile ℕ n) : ConstraintSystem Cand (LexProfile ℕ n)

Build an Optimality Theory system: lexicographic minimum on a violation profile. The candidate set must be finite; profile c gives the n-tuple of constraint violations for candidate c ranked in order of dominance.

Equivalent to choosing the OT winner(s) by argmin on the lex order.

Equations

• Core.Constraint.otSystem candidates profile = { candidates := candidates, score := profile, decoder := Core.Constraint.argminDecoder }

noncomputable def Core.Constraint.hgSystem {Cand : Type u_1} (candidates : Finset Cand) (constraints : List (WeightedConstraint Cand)) : ConstraintSystem Cand ℝ

Build a (deterministic) Harmonic Grammar system: real-valued harmony score, choose the candidate(s) that maximise it.

The harmony score is harmonyScoreR constraints c = -Σⱼ wⱼ · Cⱼ(c). Higher harmony = lower (weighted) violation = more grammatical.

Equations

• Core.Constraint.hgSystem candidates constraints = { candidates := candidates, score := Core.Constraint.harmonyScoreR constraints, decoder := Core.Constraint.argmaxDecoder }

noncomputable def Core.Constraint.maxEntSystem {Cand : Type u_1} (candidates : Finset Cand) (constraints : List (WeightedConstraint Cand)) (α : ℝ := 1) : ConstraintSystem Cand ℝ

Build a MaxEnt Harmonic Grammar system: same harmony score as hgSystem, but soft-decode with temperature α. As α → ∞, this converges to hgSystem (see softmax_argmax_limit in Core.Agent.RationalAction).

The default α = 1 matches @cite{goldwater-johnson-2003}'s standard MaxEnt formulation.

Equations

• Core.Constraint.maxEntSystem candidates constraints α = { candidates := candidates, score := Core.Constraint.harmonyScoreR constraints, decoder := Core.Constraint.softmaxDecoder α }

Core.Constraint.Evaluation.Tableau is the established study-file API for OT (used by mkTableau ... .optimal = {winner} patterns). The bridge below shows that Tableau is a special case of ConstraintSystem: the OT score profile : C → ViolationProfile n is exactly a LexProfile Nat n-valued score (definitionally), and Tableau.optimal is exactly the support of the argminDecoder distribution. So existing OT studies can keep their Tableau/optimal formulation and additionally expose the unified ConstraintSystem.predict view via tableauSystem.

noncomputable def Core.Constraint.tableauSystem {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Evaluation.Tableau C n) : ConstraintSystem C (LexProfile ℕ n)

An OT tableau viewed as a generic ConstraintSystem. The score type LexProfile Nat n is definitionally ViolationProfile n, so the argminDecoder's LinearOrder requirement is satisfied by the standard Pi.Lex instance.

Equations

• Core.Constraint.tableauSystem t = { candidates := t.candidates, score := t.profile, decoder := Core.Constraint.argminDecoder }

theorem Core.Constraint.tableauSystem_predict_eq {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Evaluation.Tableau C n) (c : C) : (tableauSystem t).predict c = if c ∈ t.optimal then (↑t.optimal.card)⁻¹ else 0

The unifying identity: tableauSystem's prediction is uniform over Tableau.optimal. Since Tableau.optimal IS the argmin filter set by definition, the argminDecoder reduces to the standard "uniform over winners" formula. All other bridge results follow.

theorem Core.Constraint.tableauSystem_predict_pos_iff_optimal {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Evaluation.Tableau C n) (c : C) : 0 < (tableauSystem t).predict c ↔ c ∈ t.optimal

A candidate is in the support of the tableauSystem distribution iff it is in the tableau's optimal set.

theorem Core.Constraint.tableauSystem_predict_unique_winner {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Evaluation.Tableau C n) (winner : C) (h : t.optimal = {winner}) : (tableauSystem t).predict winner = 1

When Tableau.optimal = {winner} (the typical deterministic-OT pattern used in study files via by decide), the unified predict view assigns probability 1 to the winner.

theorem Core.Constraint.tableauSystem_predict_loser {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Evaluation.Tableau C n) (winner loser : C) (hne : loser ≠ winner) (h : t.optimal = {winner}) : (tableauSystem t).predict loser = 0

And losers in a unique-winner tableau receive probability 0.

Closed-form, monotonicity, and probability-distribution lemmas for ConstraintSystems decoded by softmaxDecoder. The hypothesis hd : s.decoder = softmaxDecoder α is rfl for systems built via maxEntSystem or via the explicit-record pattern study files use ({ candidates := …, score := …, decoder := softmaxDecoder 1 }), so study-file proofs collapse to one-line delegations.

theorem Core.Constraint.ConstraintSystem.predict_softmax_of_mem {Cand : Type u_1} (s : ConstraintSystem Cand ℝ) {α : ℝ} (hd : s.decoder = softmaxDecoder α) {c : Cand} (hc : c ∈ s.candidates) : s.predict c = Real.exp (α * s.score c) / ∑ c' ∈ s.candidates, Real.exp (α * s.score c')

For a system whose decoder is softmaxDecoder α, the predicted probability of an in-set candidate has the standard MaxEnt closed form exp(α · score(c)) / Σ exp(α · score(c')).

theorem Core.Constraint.ConstraintSystem.predict_softmax_lt_of_score_lt {Cand : Type u_1} (s : ConstraintSystem Cand ℝ) {α : ℝ} (hα : 0 < α) (hd : s.decoder = softmaxDecoder α) {c1 c2 : Cand} (h1 : c1 ∈ s.candidates) (h2 : c2 ∈ s.candidates) (hlt : s.score c1 < s.score c2) : s.predict c1 < s.predict c2

Softmax monotonicity: for α > 0 and both candidates in the candidate set, the candidate with strictly higher score gets strictly higher predicted probability. Lets MaxEnt study files derive ranking facts from raw harmony comparisons in one line.

theorem Core.Constraint.ConstraintSystem.predict_softmax_eq_of_score_eq {Cand : Type u_1} (s : ConstraintSystem Cand ℝ) {α : ℝ} (hd : s.decoder = softmaxDecoder α) {c1 c2 : Cand} (h1 : c1 ∈ s.candidates) (h2 : c2 ∈ s.candidates) (heq : s.score c1 = s.score c2) : s.predict c1 = s.predict c2

Softmax equality: candidates with equal scores get equal predicted probability. Lets MaxEnt study files derive equiprobability from raw score equality in one line.

theorem Core.Constraint.ConstraintSystem.predict_softmax_isProb {Cand : Type u_1} (s : ConstraintSystem Cand ℝ) {α : ℝ} (hd : s.decoder = softmaxDecoder α) (hne : s.candidates.Nonempty) : ∑ c ∈ s.candidates, s.predict c = 1

For a system whose decoder is softmaxDecoder α, predicted probabilities sum to 1 over the (non-empty) candidate set. Specialises predict_sum_eq_one so study files needn't supply the IsProb instance argument explicitly.