φ-agreement between word tokens

Word.phi is the agreement bundle of a word's features, and two words Agree when their bundles are compatible, an unspecified dimension acting as a wildcard. The relation is reflexive and symmetric but not transitive; HasPhi.Agree is its generic form.

def Morphology.Word.phi (w : Word) : Agreement.Bundle

The agreement bundle of a word's features.

Equations

• w.phi = Agreement.Bundle.ofFeatures w.features

@[instance_reducible]

instance Morphology.instHasPhiWord : HasPhi Word

Equations

• Morphology.instHasPhiWord = { phi := Morphology.Word.phi }

def Morphology.Word.Agree (w1 w2 : Word) : Prop

Two words agree when their bundles are compatible, an unspecified dimension acting as a wildcard; the agreement check binding and concord consumers share.

Equations

• w1.Agree w2 = Compat w1.phi w2.phi

theorem Morphology.Word.hasPhi_agree (w1 w2 : Word) : HasPhi.Agree w1 w2 ↔ w1.Agree w2

On word tokens, generic agreement is Word.Agree.

@[instance_reducible]

instance Morphology.instDecidableAgree (w1 w2 : Word) : Decidable (w1.Agree w2)

Equations

• Morphology.instDecidableAgree w1 w2 = id inferInstance

theorem Morphology.Word.Agree.refl (w : Word) : w.Agree w

theorem Morphology.Word.Agree.symm {w1 w2 : Word} (h : w1.Agree w2) : w2.Agree w1

theorem Morphology.Word.Agree.not_transitive : ¬∀ (w1 w2 w3 : Word), w1.Agree w2 → w2.Agree w3 → w1.Agree w3

φ-agreement is not transitive: underspecified they agrees with both she and he while she and he disagree.