Token features

The morphosyntactic features a word token carries: the agreement dimensions, valued in the analytical inventories Person, Number, Gender and Case, and the nominal and verbal features of the Universal Dependencies annotation, definiteness, degree, pronoun type, reflexivity, verb form, tense, aspect, mood, voice and polarity, valued in the tag inventories until an analytical one exists. A token's features give each feature a value or ⊥, a slot of the flat order, so subsumption, unification and generalization are the pointwise order, partial join and meet; the Universal Dependencies annotation of a token is the matter of Morphology/Word/UD.lean.

Main declarations

• Morphology.Feature, Morphology.Feature.Value — the features and their value types
• Morphology.Features — the bundle, with the constructor Features.of naming the values it specifies
• Morphology.Features.IsWh — an interrogative or relative pro-form

References

• [dMMNZ21]
• [Shi86]

inductive Morphology.Feature : Type

The morphosyntactic features of a token.

• person : Feature
• number : Feature
• gender : Feature
• case : Feature
• definiteness : Feature
• degree : Feature
• pronType : Feature
• reflex : Feature
• verbForm : Feature
• tense : Feature
• aspect : Feature
• mood : Feature
• voice : Feature
• polarity : Feature

@[instance_reducible]

instance Morphology.instDecidableEqFeature : DecidableEq Feature

Equations

• Morphology.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Morphology.instReprFeature.repr Morphology.Feature.person prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.Feature.person")).group prec✝
• Morphology.instReprFeature.repr Morphology.Feature.number prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.Feature.number")).group prec✝
• Morphology.instReprFeature.repr Morphology.Feature.gender prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.Feature.gender")).group prec✝
• Morphology.instReprFeature.repr Morphology.Feature.case prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.Feature.case")).group prec✝
• Morphology.instReprFeature.repr Morphology.Feature.degree prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.Feature.degree")).group prec✝
• Morphology.instReprFeature.repr Morphology.Feature.reflex prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.Feature.reflex")).group prec✝
• Morphology.instReprFeature.repr Morphology.Feature.tense prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.Feature.tense")).group prec✝
• Morphology.instReprFeature.repr Morphology.Feature.aspect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.Feature.aspect")).group prec✝
• Morphology.instReprFeature.repr Morphology.Feature.mood prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.Feature.mood")).group prec✝
• Morphology.instReprFeature.repr Morphology.Feature.voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.Feature.voice")).group prec✝

@[instance_reducible]

instance Morphology.instReprFeature : Repr Feature

Equations

• Morphology.instReprFeature = { reprPrec := Morphology.instReprFeature.repr }

@[instance_reducible]

instance Morphology.instFintypeFeature : Fintype Feature

Equations

• Morphology.instFintypeFeature = { elems := { val := ↑Morphology.Feature.enumList, nodup := Morphology.Feature.enumList_nodup }, complete := Morphology.instFintypeFeature._proof_1 }

@[reducible, inline]

abbrev Morphology.Feature.Value : Feature → Type

The value type of each feature: the analytical inventory for the agreement dimensions and the Universal Dependencies tags otherwise, reflexivity being privative.

Equations

• Morphology.Feature.person.Value = Person
• Morphology.Feature.number.Value = Number
• Morphology.Feature.gender.Value = Gender
• Morphology.Feature.case.Value = Case
• Morphology.Feature.definiteness.Value = UD.Definite
• Morphology.Feature.degree.Value = UD.Degree
• Morphology.Feature.pronType.Value = UD.PronType
• Morphology.Feature.reflex.Value = Unit
• Morphology.Feature.verbForm.Value = UD.VerbForm
• Morphology.Feature.tense.Value = UD.Tense
• Morphology.Feature.aspect.Value = UD.Aspect
• Morphology.Feature.mood.Value = UD.Mood
• Morphology.Feature.voice.Value = UD.Voice
• Morphology.Feature.polarity.Value = UD.Polarity

@[instance_reducible]

instance Morphology.instDecidableEqValue (t : Feature) : DecidableEq t.Value

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Morphology.instReprValue (t : Feature) : Repr t.Value

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Morphology.Features : Type

A token's features: a value or ⊥ in each feature.

Equations

• Morphology.Features = ((f : Morphology.Feature) → Flat f.Value)

def Morphology.Features.of (person : Option Person := none) (number : Option Number := none) (gender : Option Gender := none) (case_ : Option Case := none) (definiteness : Option UD.Definite := none) (degree : Option UD.Degree := none) (pronType : Option UD.PronType := none) (reflex : Bool := false) (verbForm : Option UD.VerbForm := none) (tense : Option UD.Tense := none) (aspect : Option UD.Aspect := none) (mood : Option UD.Mood := none) (voice : Option UD.Voice := none) (polarity : Option UD.Polarity := none) : Features

The bundle specifying the named values and nothing else.

Equations

• One or more equations did not get rendered due to their size.
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.person = person
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.number = number
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.gender = gender
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.case = case_
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.definiteness = definiteness
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.degree = degree
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.pronType = pronType
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.verbForm = verbForm
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.tense = tense
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.aspect = aspect
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.mood = mood
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.voice = voice
• Morphology.Features.of person number gender case_ definiteness degree pronType reflex verbForm tense aspect mood voice polarity Morphology.Feature.polarity = polarity

@[instance_reducible]

instance Morphology.Features.instRepr : Repr Features

Equations

• One or more equations did not get rendered due to their size.

def Morphology.Features.IsWh (f : Features) : Prop

The token is an interrogative or relative pro-form.

Equations

• f.IsWh = (f Morphology.Feature.pronType = some UD.PronType.Int ∨ f Morphology.Feature.pronType = some UD.PronType.Rel)

@[instance_reducible]

instance Morphology.Features.instDecidableIsWh (f : Features) : Decidable f.IsWh

Equations

• One or more equations did not get rendered due to their size.