φ-agreement between word tokens

Word.phi projects a word's person, number, and gender. Two words Agree when these features unify (UD.MorphFeatures.compatible), an unspecified feature 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) : UD.MorphFeatures

The φ-feature subset (person, number, gender) of a word.

Equations

• w.phi = { number := w.features.number, gender := w.features.gender, person := w.features.person }

@[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 φ-features (person, number, gender) are compatible, an unspecified feature acting as a wildcard. This is the feature-based agreement check binding and concord consumers share.

Equations

• w1.Agree w2 = (w1.phi.compatible w2.phi = true)

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

φ-agreement is symmetric.

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.

theorem Morphology.Word.Agree.hasNumber_compatible {w1 w2 : Word} (h : w1.Agree w2) : HasNumber.Compatible w1 w2

φ-agreement entails number compatibility (HasNumber.Compatible).