Feature bundles

This file defines the dimensions in which agreement targets covary and the analytical feature bundle over them, a value or nothing in each dimension.

An agreement bundle gives each dimension a slot of the flat order of Core/Order/Flat.lean, so its partial order, its bottom, the wholly unspecified bundle, and its unification are the pointwise ones. Each dimension is a token feature with that feature's values, and a token's bundle is its features read along that inclusion, Agreement.Bundle.ofFeatures.

Main definitions

• Agreement.Dimension — the five dimensions a target's form may covary in
• Agreement.Dimension.toFeature, Agreement.Dimension.Value — the token feature a dimension is, and its values
• Agreement.Bundle — a value or ⊥ in each dimension
• Agreement.Bundle.set, Agreement.Bundle.personNumber — a bundle with one dimension set, and the bundle valued in person and number alone
• Agreement.Bundle.ofFeatures — the restriction of a token's features

References

• [Cor98] — the three indisputable agreement features and the two contested ones
• [Nor19] — the dimensions of the concord survey

inductive Agreement.Dimension : Type

A dimension is a feature in which a target's form may covary with another element, one of the three indisputable agreement features or the two contested ones ([Cor98]).

• person : Dimension
• number : Dimension
• gender : Dimension
• case : Dimension
• definiteness : Dimension

@[instance_reducible]

instance Agreement.instDecidableEqDimension : DecidableEq Dimension

Equations

• Agreement.instDecidableEqDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Agreement.instReprDimension : Repr Dimension

Equations

• Agreement.instReprDimension = { reprPrec := Agreement.instReprDimension.repr }

def Agreement.instReprDimension.repr : Dimension → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Agreement.instReprDimension.repr Agreement.Dimension.person prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Agreement.Dimension.person")).group prec✝
• Agreement.instReprDimension.repr Agreement.Dimension.number prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Agreement.Dimension.number")).group prec✝
• Agreement.instReprDimension.repr Agreement.Dimension.gender prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Agreement.Dimension.gender")).group prec✝
• Agreement.instReprDimension.repr Agreement.Dimension.case prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Agreement.Dimension.case")).group prec✝

@[instance_reducible]

instance Agreement.instFintypeDimension : Fintype Dimension

Equations

• Agreement.instFintypeDimension = { elems := { val := ↑Agreement.Dimension.enumList, nodup := Agreement.Dimension.enumList_nodup }, complete := Agreement.instFintypeDimension._proof_1 }

@[reducible, inline]

abbrev Agreement.Dimension.toFeature : Dimension → Morphology.Feature

The token feature a dimension is. It is reducible, so that the values of a dimension reduce to those of its feature when coercions are sought.

Equations

• Agreement.Dimension.person.toFeature = Morphology.Feature.person
• Agreement.Dimension.number.toFeature = Morphology.Feature.number
• Agreement.Dimension.gender.toFeature = Morphology.Feature.gender
• Agreement.Dimension.case.toFeature = Morphology.Feature.case
• Agreement.Dimension.definiteness.toFeature = Morphology.Feature.definiteness

@[reducible, inline]

abbrev Agreement.Dimension.Value (d : Dimension) : Type

The values of a dimension are those of the token feature it is.

Equations

• d.Value = d.toFeature.Value

@[instance_reducible]

instance Agreement.instDecidableEqValue (d : Dimension) : DecidableEq d.Value

Equations

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

@[reducible, inline]

abbrev Agreement.Bundle : Type

A feature bundle assigns each dimension a value or ⊥.

Equations

• Agreement.Bundle = ((d : Agreement.Dimension) → Flat d.Value)

def Agreement.Bundle.set (d : Dimension) (v : d.Value) (b : Bundle) : Bundle

The bundle with the dimension d set to the value v.

Equations

• Agreement.Bundle.set d v b = Function.update b d (some v)

def Agreement.Bundle.personNumber (p : Person) (n : Number) : Bundle

The bundle valued in person and number alone.

Equations

• Agreement.Bundle.personNumber p n = Agreement.Bundle.set Agreement.Dimension.number n (Agreement.Bundle.set Agreement.Dimension.person p ⊥)

@[simp]

theorem Agreement.Bundle.personNumber_person (p : Person) (n : Number) : personNumber p n Dimension.person = ↑p

@[simp]

theorem Agreement.Bundle.personNumber_number (p : Person) (n : Number) : personNumber p n Dimension.number = ↑n

@[simp]

theorem Agreement.Bundle.personNumber_gender (p : Person) (n : Number) : personNumber p n Dimension.gender = ⊥

@[simp]

theorem Agreement.Bundle.personNumber_case (p : Person) (n : Number) : personNumber p n Dimension.case = ⊥

@[simp]

theorem Agreement.Bundle.personNumber_definiteness (p : Person) (n : Number) : personNumber p n Dimension.definiteness = ⊥

def Agreement.Bundle.ofFeatures (f : Morphology.Features) : Bundle

The restriction of a token's features to the agreement dimensions reads them along Dimension.toFeature.

Equations

• Agreement.Bundle.ofFeatures f d = f d.toFeature

@[simp]

theorem Agreement.Bundle.ofFeatures_apply (f : Morphology.Features) (d : Dimension) : ofFeatures f d = f d.toFeature

@[instance_reducible]

instance Agreement.instReprBundle : Repr Bundle

Equations

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