Person segments

The person features that Agree manipulates are the person nodes of Harley and Ritter's feature geometry: the root π, which every nominal bears, [participant], and its dependents [speaker] and [addressee]. Béjar and Rezac call them the segments of an articulated person probe. The segments a person bears are read off the geometry, a bare [participant] receiving [speaker] by default.

Main definitions

• Minimalist.PersonSegment: the person segments, ordered by the dominance of the geometry.
• Minimalist.PersonSegment.toNode: a segment as a node of the geometry.
• Minimalist.PersonSegment.spec: the segments a person bears.

Main results

• Minimalist.PersonSegment.spec_isLowerSet: a person bears whatever its segments depend on.

Implementation notes

π is Harley and Ritter's root Referring Expression node, which Deal writes [φ].

References

• [HR02]
• [BR09]
• [Dea24]

inductive Minimalist.PersonSegment : Type

A segment of the person feature, a person node of the geometry of [HR02].

• pi : PersonSegment

  π, the root, borne by every nominal.

• participant : PersonSegment

  [participant], borne by the first and second persons.

• speaker : PersonSegment

  [speaker], borne by the persons that include the speaker.

• addressee : PersonSegment

  [addressee], borne by the persons that include the addressee.

@[instance_reducible]

instance Minimalist.instDecidableEqPersonSegment : DecidableEq PersonSegment

Equations

• Minimalist.instDecidableEqPersonSegment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.instReprPersonSegment : Repr PersonSegment

Equations

• Minimalist.instReprPersonSegment = { reprPrec := Minimalist.instReprPersonSegment.repr }

def Minimalist.instReprPersonSegment.repr : PersonSegment → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.instFintypePersonSegment : Fintype PersonSegment

Equations

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

def Minimalist.PersonSegment.toNode : PersonSegment → Phi.Geometry.Node

The node of the geometry a segment is.

Equations

• Minimalist.PersonSegment.pi.toNode = ⊥
• Minimalist.PersonSegment.participant.toNode = Phi.Geometry.Node.participant
• Minimalist.PersonSegment.speaker.toNode = Phi.Geometry.Node.speaker
• Minimalist.PersonSegment.addressee.toNode = Phi.Geometry.Node.addressee

theorem Minimalist.PersonSegment.toNode_injective : Function.Injective toNode

@[instance_reducible]

instance Minimalist.PersonSegment.instPartialOrder : PartialOrder PersonSegment

Segments are ordered by the dominance of the geometry, a ≤ b when b depends on a.

Equations

• Minimalist.PersonSegment.instPartialOrder = PartialOrder.lift Minimalist.PersonSegment.toNode Minimalist.PersonSegment.toNode_injective

@[instance_reducible]

instance Minimalist.PersonSegment.instDecidableLE : DecidableLE PersonSegment

Equations

• a.instDecidableLE b = { decide := decide (a.toNode = b.toNode) || decide (a.toNode ∈ b.toNode.ancestors), reflects_decide := ⋯ }

@[instance_reducible]

instance Minimalist.PersonSegment.instOrderBot : OrderBot PersonSegment

Equations

• Minimalist.PersonSegment.instOrderBot = { bot := Minimalist.PersonSegment.pi, bot_le := Minimalist.PersonSegment.instOrderBot._proof_1 }

def Minimalist.PersonSegment.spec (p : Person) : Finset PersonSegment

The segments a person bears, the nodes of its geometry.

Equations

• Minimalist.PersonSegment.spec p = {x : Minimalist.PersonSegment | x.toNode ∈ Phi.Geometry.personFeatures p}

theorem Minimalist.PersonSegment.mem_spec {s : PersonSegment} {p : Person} : s ∈ spec p ↔ s.toNode ∈ Phi.Geometry.personFeatures p

@[simp]

theorem Minimalist.PersonSegment.pi_mem_spec (p : Person) : pi ∈ spec p

theorem Minimalist.PersonSegment.spec_isLowerSet (p : Person) : IsLowerSet ↑(spec p)

A person bears whatever its segments depend on.