Match Theory

import Linglib.Phonology.Prosody.Match · namespace Prosody

This file defines the Match constraints of the syntax–prosody interface. A constituent structure over a string is the family of spans its constituents cover, so a syntactic input enters as the spans of its constituents of a category, counted in the syllables of the output, and a prosodic candidate as the spans of its nodes at a level. Match(α, π) requires each α-span to be the span of a π-node and Match(π, α) each π-span to be an α-span: two-sided alignment, both edges of a constituent coinciding with those of one constituent of the other category. One-sided alignment is Constraint.alignLeft and Constraint.alignRight on the same families. MAX(α, π) asks only that each α-constituent have a corresponding π-node, one containing its head and no head from outside it, no π-node answering to two α-constituents.

Main definitions

Prosody.levelSpans: the spans of the nodes of a prosodic tree at a level.
Prosody.Corresponds: a node corresponds to a constituent, containing its head and no foreign head.
Prosody.syntaxProsodyMatch, Prosody.prosodySyntaxMatch: Match(α, π) and Match(π, α).
Prosody.syntaxProsodyMax: MAX(α, π), existential correspondence.

Main results

Prosody.deficiency_corresponds_le: MAX(α, π) asks no more than Match(α, π).

Implementation notes

The syntactic family is a list of spans rather than a tree, so the constraints read any syntactic representation, a phrase-structure tree or a morphological word, once the spans of its constituents are given in the syllables of the output. The list keeps multiplicity, so a φ recursively over a φ of the same span is counted twice.

References

Selkirk 2011, The Syntax-Phonology Interface
Itô & Mester 2019, Match as Syntax-Prosody MAX/DEP: Prosodic Enclisis in English formalized

Declarations

The spans of the ℓ-nodes of a prosodic tree, the span counterpart of levelPositions.

@[reducible, inline] abbrev levelSpans L56–57

(ℓ : Level) (t : Tree) :

List (ℕ × ℕ)

levelSpans ℓ t = RoseTree.spans t fun (x : RoseTree Constituent) => x.value.level = ℓ

Used by syntaxProsodyMatch, prosodySyntaxMatch, syntaxProsodyMax

Used in HartmannZimmermann2004, ItoMester2009

Match(α, π) (Selkirk 2011): one violation for each span of the syntactic family α that is the span of no π-node, the two edges of the constituent coinciding with those of no π-node (Itô & Mester 2019).

def syntaxProsodyMatch L59–63

(α : List (ℕ × ℕ)) (π : Level) :

OptimalityTheory.Constraint Tree

syntaxProsodyMatch α π = OptimalityTheory.Constraint.comap (fun (t : Tree) => (α, levelSpans π t)) (OptimalityTheory.Constraint.align Eq)

Built from

Used in Bennett2018

Match(π, α) (Selkirk 2011): one violation for each π-node whose span is the span of no constituent of the syntactic family α.

def prosodySyntaxMatch L65–68

(π : Level) (α : List (ℕ × ℕ)) :

OptimalityTheory.Constraint Tree

prosodySyntaxMatch π α = OptimalityTheory.Constraint.comap (fun (t : Tree) => (levelSpans π t, α)) (OptimalityTheory.Constraint.align Eq)

Built from

Used in Bennett2018, Brodkin2026

A node of span p corresponds to the constituent a of the family α, given by its span and the position of its head, when it contains the head of a and no head of α lying outside a (Itô & Mester 2019).

@[reducible, inline] abbrev Corresponds L70–74

(α : List ((ℕ × ℕ) × ℕ)) (a : (ℕ × ℕ) × ℕ) (p : ℕ × ℕ) :

Prop

Corresponds α a p = (a.2 ∈ Set.Ico p.1 p.2 ∧ ∀ b ∈ α, b.2 ∈ Set.Ico p.1 p.2 → b.2 ∈ Set.Ico a.1.1 a.1.2)

Used by syntaxProsodyMax, deficiency_corresponds_le

MAX(α, π) (Itô & Mester 2019): one violation for each constituent of the family α, given by its span and the position of its head, left without a corresponding π-node by the best correspondence in which no π-node answers to two constituents. A π-node over two sister constituents answers to neither, and a constituent and its subconstituents need a π-node each.

def syntaxProsodyMax L76–82

(α : List ((ℕ × ℕ) × ℕ)) (π : Level) :

OptimalityTheory.Constraint Tree

syntaxProsodyMax α π = OptimalityTheory.Constraint.comap (fun (t : Tree) => (α, levelSpans π t)) (OptimalityTheory.Constraint.deficiency (Corresponds α))

Built from ,

Used in Brodkin2026

Existential correspondence asks no more than Match (Itô & Mester 2019): where the constituents of α have distinct spans each containing its head, fewer of them lack a corresponding node than lack a node of the same span.

theorem deficiency_corresponds_le L86–95

{α : List ((ℕ × ℕ) × ℕ)} (hα : (List.map (fun (x : (ℕ × ℕ) × ℕ) => x.1) α).Nodup) (hhead : ∀ a ∈ α, a.2 ∈ Set.Ico a.1.1 a.1.2) (m : List (ℕ × ℕ)) :

OptimalityTheory.Constraint.deficiency (Corresponds α) (α, m) ≤ OptimalityTheory.Constraint.align Eq (List.map (fun (x : (ℕ × ℕ) × ℕ) => x.1) α, m)

Built from