Deal (2024): Interaction, Satisfaction, and the PCC

Deal derives the Person Case Constraint from a probe specified by an interaction condition, the features it copies from a goal, and a satisfaction condition, the feature that halts its search, with no uninterpretable features anywhere. The probe meets the direct object first, so a direct object that satisfies it bleeds Agree with the indirect object: satisfaction by [PART] gives the strong PCC, by [SPKR] the me-first PCC, and an insatiable probe no PCC. Dynamic interaction lets a feature copied from the direct object narrow the interaction condition, so that the indirect object must bear it too, which gives the weak and the strictly descending PCC. A probe that meets the indirect object first yields the reverse PCC of section 6.2.

Main results

• Deal2024.typology: the runs of the probes derive the typology tables (53) and (57).
• Deal2024.rows: the clitic combinations of French, Bulgarian, Italian, Spanish, Shapsug Adyghe and Slovenian are grammatical exactly when the language's grammar licenses them.
• Deal2024.agrees_with_pConstraint, Deal2024.agrees_with_gluttony: on the six cells of table (1) the four varieties coincide with the P-Constraint grammars of Pancheva and Zubizarreta and the gluttony probes of Coon and Keine, the competitors of section 7.
• Deal2024.universal5_prominence, Deal2024.universal5_addressee: with the cells read as scenarios and each variety as an argument coding, the strong, weak, me-first and strictly descending varieties obey Haspelmath's scenario universal under 1 > 2 > 3, and the strong, weak, you-first and A-descending ones under 2 > 1 > 3, as his section 7.1 claims of the PCC.
• Deal2024.strictlyDescending_iff_downstream, Deal2024.aDescending_iff_downstream: the two descending statements say that the scenario is downstream under their rankings.

Implementation notes

The features of the geometry (7) are the person segments of Minimalist.PersonSegment, [φ] its root π, [PART] participant, [SPKR] speaker and [ADDR] addressee, so a second person and an inclusive first person bear [ADDR]. The interaction condition is the set of features copied so far, a goal being visible when it bears them all, which is the set conception the paper's footnote 10 allows; the paper's single interaction feature is the most specific one copied. Table (1) has no reflexive cells, so the classification of grammars ranges over its six cells, PCC.distinctPairs; the mechanism's verdicts on reflexive combinations are not stated.

References

• [Dea24]
• [Has21c]
• [PZ18]
• [CK21]

Probes and their runs

structure Deal2024.Grammar : Type

A grammar fixes the satisfaction condition, none for an insatiable probe, and the features that interact dynamically, copied into the interaction condition when a goal bears them.

• satisfaction : Option Minimalist.PersonSegment
• dynamic : Finset Minimalist.PersonSegment

def Deal2024.instDecidableEqGrammar.decEq (x✝ x✝¹ : Grammar) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Deal2024.instDecidableEqGrammar : DecidableEq Grammar

Equations

• Deal2024.instDecidableEqGrammar = Deal2024.instDecidableEqGrammar.decEq

@[instance_reducible]

instance Deal2024.instFintypeGrammar : Fintype Grammar

Equations

• Deal2024.instFintypeGrammar = Fintype.ofEquiv ((_ : Option Minimalist.PersonSegment) × Finset Minimalist.PersonSegment) Deal2024.Grammar.proxyTypeEquiv

structure Deal2024.ProbeState : Type

The state of a probe during its walk over the goals records the interaction condition, whether the probe has been satisfied, and the positions of the goals it has interacted with.

• int : Finset Minimalist.PersonSegment
• satisfied : Bool
• agreed : List ℕ

def Deal2024.instDecidableEqProbeState.decEq (x✝ x✝¹ : ProbeState) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Deal2024.instDecidableEqProbeState : DecidableEq ProbeState

Equations

• Deal2024.instDecidableEqProbeState = Deal2024.instDecidableEqProbeState.decEq

def Deal2024.ProbeState.initial : ProbeState

The initial state is [INT:φ], unsatisfied, with nothing agreed.

Equations

• Deal2024.ProbeState.initial = { int := {Minimalist.PersonSegment.pi}, satisfied := false, agreed := [] }

def Deal2024.ProbeState.probe (st : ProbeState) : Minimalist.Probe Person

The probe a state denotes sees a goal when the goal bears every feature of the interaction condition.

Equations

• st.probe = Minimalist.Probe.relativized fun (p : Person) => decide (st.int ⊆ Minimalist.PersonSegment.spec p)

def Deal2024.step (g : Grammar) (st : ProbeState) (t : Person × ℕ) : ProbeState

In one step of the walk a satisfied probe is inert, (8b); otherwise a visible goal is interacted with, its position recorded, the goal's dynamic features are copied into the interaction condition, and the probe is satisfied when the goal bears the satisfaction feature, (44) and (45).

Equations

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

def Deal2024.runProbe (g : Grammar) (goals : List Person) : ProbeState

The run of a probe over a goal sequence in interaction order.

Equations

• Deal2024.runProbe g goals = List.foldl (Deal2024.step g) Deal2024.ProbeState.initial goals.zipIdx

theorem Deal2024.int_subset_step (g : Grammar) (st : ProbeState) (t : Person × ℕ) : st.int ⊆ (step g st t).int

Dynamic interaction only narrows the probe, since the interaction condition only grows along a run.

theorem Deal2024.probe_sat_antitone (g : Grammar) (st : ProbeState) (t : Person × ℕ) (a : Person) (h : (step g st t).probe.sat a = true) : st.probe.sat a = true

The probe a later state denotes sees no more than an earlier one.

theorem Deal2024.step_of_satisfied (g : Grammar) (st : ProbeState) (t : Person × ℕ) (h : st.satisfied = true) : step g st t = st

A satisfied probe is inert.

def Deal2024.Licit (g : Grammar) (s : Clause.Scenario Person) : Prop

A clitic combination ⟨IO, DO⟩ is licit when the probe, meeting the direct object first, interacts with both objects, section 3.1; the reverse PCC of section 6.2, where the probe meets the indirect object first, is licitness of the swapped pair.

Equations

• Deal2024.Licit g s = ((Deal2024.runProbe g [s.low, s.high]).agreed = [0, 1])

@[instance_reducible]

instance Deal2024.instDecidablePredScenarioPersonLicit (g : Grammar) : DecidablePred (Licit g)

Equations

• Deal2024.instDecidablePredScenarioPersonLicit g x✝ = Deal2024.instDecidablePredScenarioPersonLicit._aux_1 g x✝

The grammars

def Deal2024.strong : Grammar

The strong PCC is the probe [INT:φ, SAT:PART], (15).

Equations

• Deal2024.strong = { satisfaction := some Minimalist.PersonSegment.participant, dynamic := ∅ }

def Deal2024.meFirst : Grammar

The me-first PCC is the probe [INT:φ, SAT:SPKR], (33).

Equations

• Deal2024.meFirst = { satisfaction := some Minimalist.PersonSegment.speaker, dynamic := ∅ }

def Deal2024.noPCC : Grammar

The insatiable probe [INT:φ, SAT:-] of Ubykh and Moro derives no PCC.

Equations

• Deal2024.noPCC = { satisfaction := none, dynamic := ∅ }

def Deal2024.weak : Grammar

The weak PCC is an insatiable probe with [PART] interacting dynamically, (38).

Equations

• Deal2024.weak = { satisfaction := none, dynamic := {Minimalist.PersonSegment.participant} }

def Deal2024.strictlyDescending : Grammar

The strictly descending PCC is [SAT:SPKR] with [PART] interacting dynamically, (50).

Equations

• Deal2024.strictlyDescending = { satisfaction := some Minimalist.PersonSegment.speaker, dynamic := {Minimalist.PersonSegment.participant} }

def Deal2024.youFirst : Grammar

The you-first PCC is [SAT:ADDR], section 6.1.

Equations

• Deal2024.youFirst = { satisfaction := some Minimalist.PersonSegment.addressee, dynamic := ∅ }

def Deal2024.aDescending : Grammar

The A-descending PCC is [SAT:ADDR] with [PART] interacting dynamically, section 6.1.

Equations

• Deal2024.aDescending = { satisfaction := some Minimalist.PersonSegment.addressee, dynamic := {Minimalist.PersonSegment.participant} }

The typology

def Deal2024.addresseeRank : Person → ℕ

The rank of a person on the hierarchy 2 > 1 > 3 of the A-descending PCC.

Equations

• Deal2024.addresseeRank Person.second = 2
• Deal2024.addresseeRank Person.first = 1
• Deal2024.addresseeRank Person.firstInclusive = 1
• Deal2024.addresseeRank Person.firstExclusive = 1
• Deal2024.addresseeRank Person.third = 0

inductive Deal2024.PCCType : Type

The PCC varieties are the four of table (1), the two the feature [ADDR] adds, and none.

• strong : PCCType
• weak : PCCType
• meFirst : PCCType
• strictlyDescending : PCCType
• youFirst : PCCType
• aDescending : PCCType
• none : PCCType

@[instance_reducible]

instance Deal2024.instDecidableEqPCCType : DecidableEq PCCType

Equations

• Deal2024.instDecidableEqPCCType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Deal2024.instReprPCCType.repr : PCCType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Deal2024.instReprPCCType.repr Deal2024.PCCType.strong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Deal2024.PCCType.strong")).group prec✝
• Deal2024.instReprPCCType.repr Deal2024.PCCType.weak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Deal2024.PCCType.weak")).group prec✝
• Deal2024.instReprPCCType.repr Deal2024.PCCType.meFirst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Deal2024.PCCType.meFirst")).group prec✝
• Deal2024.instReprPCCType.repr Deal2024.PCCType.youFirst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Deal2024.PCCType.youFirst")).group prec✝
• Deal2024.instReprPCCType.repr Deal2024.PCCType.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Deal2024.PCCType.none")).group prec✝

@[instance_reducible]

instance Deal2024.instReprPCCType : Repr PCCType

Equations

• Deal2024.instReprPCCType = { reprPrec := Deal2024.instReprPCCType.repr }

@[instance_reducible]

instance Deal2024.instFintypePCCType : Fintype PCCType

Equations

• Deal2024.instFintypePCCType = { elems := { val := ↑Deal2024.PCCType.enumList, nodup := Deal2024.PCCType.enumList_nodup }, complete := Deal2024.instFintypePCCType._proof_1 }

def Deal2024.PCCType.Licit : PCCType → Clause.Scenario Person → Prop

The descriptive statements of (2) and section 6.1, one per variety, say that the direct object must be third person; that if there is a third person, the direct object must be third person; that if there is a first person, it must be the indirect object; that the indirect object must outrank the direct object on 1 > 2 > 3; that if there is a second person, it must be the indirect object; that the indirect object must outrank the direct object on 2 > 1 > 3; and nothing.

Equations

• Deal2024.PCCType.strong.Licit x✝ = ¬x✝.low.IsSAP
• Deal2024.PCCType.weak.Licit x✝ = (¬x✝.high.IsSAP → ¬x✝.low.IsSAP)
• Deal2024.PCCType.meFirst.Licit x✝ = ¬x✝.low.IncludesSpeaker
• Deal2024.PCCType.strictlyDescending.Licit x✝ = (x✝.low.prominence < x✝.high.prominence)
• Deal2024.PCCType.youFirst.Licit x✝ = (Minimalist.PersonSegment.addressee ∉ Minimalist.PersonSegment.spec x✝.low)
• Deal2024.PCCType.aDescending.Licit x✝ = (Deal2024.addresseeRank x✝.low < Deal2024.addresseeRank x✝.high)
• Deal2024.PCCType.none.Licit x✝ = True

@[instance_reducible]

instance Deal2024.instDecidablePredScenarioPersonLicit_1 (t : PCCType) : DecidablePred t.Licit

Equations

• One or more equations did not get rendered due to their size.
• Deal2024.instDecidablePredScenarioPersonLicit_1 Deal2024.PCCType.strong x✝ = { decide := !decide x✝.low.IsSAP, reflects_decide := ⋯ }
• Deal2024.instDecidablePredScenarioPersonLicit_1 Deal2024.PCCType.meFirst x✝ = { decide := !decide x✝.low.IncludesSpeaker, reflects_decide := ⋯ }
• Deal2024.instDecidablePredScenarioPersonLicit_1 Deal2024.PCCType.strictlyDescending x✝ = Deal2024.instDecidablePredScenarioPersonLicit_1._aux_4 x✝
• Deal2024.instDecidablePredScenarioPersonLicit_1 Deal2024.PCCType.aDescending x✝ = { decide := (Deal2024.addresseeRank x✝.low).succ.ble (Deal2024.addresseeRank x✝.high), reflects_decide := ⋯ }
• Deal2024.instDecidablePredScenarioPersonLicit_1 Deal2024.PCCType.none x✝ = { decide := true, reflects_decide := ⋯ }

theorem Deal2024.strictlyDescending_iff_downstream (s : Clause.Scenario Person) : PCCType.strictlyDescending.Licit s ↔ (Clause.Scenario.map Person.prominence s).kind = Clause.Scenario.Kind.downstream

The strictly descending PCC holds of an IO–DO combination exactly when the scenario is downstream on 1 > 2 > 3.

theorem Deal2024.aDescending_iff_downstream (s : Clause.Scenario Person) : PCCType.aDescending.Licit s ↔ (Clause.Scenario.map addresseeRank s).kind = Clause.Scenario.Kind.downstream

The A-descending PCC holds exactly when the scenario is downstream on 2 > 1 > 3.

def Deal2024.PCCType.coding (t : PCCType) (s : Clause.Scenario Person) : ℕ

A variety codes a combination as the clitic cluster where it is licit and as the longer repair where it is not.

Equations

• t.coding s = if t.Licit s then 0 else 1

def Deal2024.MoreUsualOn {β : Type u_1} [LinearOrder β] (rank : Person → β) (s t : Clause.Scenario Person) : Prop

Under a person ranking, a cell of table (1) is more usual than another when its kind is higher.

Equations

• Deal2024.MoreUsualOn rank s t = (s ∈ PCC.distinctPairs ∧ t ∈ PCC.distinctPairs ∧ (Clause.Scenario.map rank t).kind < (Clause.Scenario.map rank s).kind)

@[instance_reducible]

instance Deal2024.instDecidableMoreUsualOn {β : Type u_1} [LinearOrder β] (rank : Person → β) (s t : Clause.Scenario Person) : Decidable (MoreUsualOn rank s t)

Equations

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

theorem Deal2024.universal5_prominence (t : PCCType) : Haspelmath2021.RoleReferenceUniversal (MoreUsualOn Person.prominence) t.coding ↔ t ∈ [PCCType.strong, PCCType.weak, PCCType.meFirst, PCCType.strictlyDescending, PCCType.none]

Under the person scale 1 > 2 > 3, a variety never bans a more usual combination of table (1) while allowing a less usual one exactly when it is the strong, weak, me-first or strictly descending PCC, as section 7.1 of [Has21c] requires. The addressee-first varieties ban the downstream 1 > 2.

theorem Deal2024.universal5_addressee (t : PCCType) : Haspelmath2021.RoleReferenceUniversal (MoreUsualOn addresseeRank) t.coding ↔ t ∈ [PCCType.strong, PCCType.weak, PCCType.youFirst, PCCType.aDescending, PCCType.none]

Under the ranking 2 > 1 > 3 it is the strong, weak, you-first and A-descending varieties that obey the scenario universal; me-first and strictly descending ban the then-downstream 2 > 1.

theorem Deal2024.participant_third_licit (t : PCCType) (io : Person) (h : io.IsSAP) : t.Licit { high := io, low := Person.third }

Every variety allows a participant IO with a third-person DO, the ⟨⊤, ⊥⟩ of the binary person scale, as the person-role universal 9b of [Has21c] requires.

theorem Deal2024.strong_iff_greekT (s : Clause.Scenario Person) : PCCType.strong.Licit s ↔ Haspelmath2021.greekT (Clause.Scenario.map Person.toClass s) = 0

The strong PCC is Modern Greek's T coding in [Has21c]'s (45), the clitic being available exactly where the DO is aliophoric.

def Deal2024.PCCType.all : List PCCType

Equations

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

def Deal2024.Grammar.pattern (g : Grammar) : Option PCCType

The variety a grammar derives is the one whose statement it matches on the six cells.

Equations

• g.pattern = List.find? (fun (t : Deal2024.PCCType) => decide (∀ s ∈ PCC.distinctPairs, Deal2024.Licit g s ↔ t.Licit s)) Deal2024.PCCType.all

def Deal2024.table57 (g : Grammar) : Option PCCType

Table (57), the typology by satisfaction condition and dynamic interaction features, with table (53) as its rows and columns without [ADDR]; a probe satisfied by [φ] Agrees with the direct object alone and derives no variety, and dynamic [φ] changes nothing.

Equations

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

theorem Deal2024.typology (g : Grammar) : g.pattern = table57 g

Every grammar derives the variety that table (57) gives it, so the runs derive the tables.

theorem Deal2024.licit_of_sat_part (d : Finset Minimalist.PersonSegment) (s : Clause.Scenario Person) : Licit { satisfaction := some Minimalist.PersonSegment.participant, dynamic := d } s ↔ Licit strong s

Satisfaction by [PART] absorbs dynamic interaction. A direct object bearing a dynamic feature bears [PART] and satisfies the probe first, so every column-one grammar of the table licenses exactly what the strong PCC does, for every pair of persons.

theorem Deal2024.sd_off_diagonal_iff_outranks (s : Clause.Scenario Person) (h : s.high.prominence ≠ s.low.prominence) : Licit strictlyDescending s ↔ s.low.prominence < s.high.prominence

Off the diagonal, for objects of distinct person, the strictly descending PCC requires the indirect object to outrank the direct object on 1 > 2 > 3.

The competitors (section 7)

theorem Deal2024.agrees_with_pConstraint (s : Clause.Scenario Person) : s ∈ PCC.distinctPairs → (Licit strong s ↔ PCC.IsLicit PCC.strongGrammar s) ∧ (Licit weak s ↔ PCC.IsLicit PCC.weakGrammar s) ∧ (Licit meFirst s ↔ PCC.IsLicit PCC.meFirstGrammar s) ∧ (Licit strictlyDescending s ↔ PCC.IsLicit PCC.ultraStrongGrammar s)

On the six cells of table (1) the four varieties coincide with the P-Constraint grammars of [PZ18], strictly descending with ultra-strong.

theorem Deal2024.agrees_with_gluttony (s : Clause.Scenario Person) : s ∈ PCC.distinctPairs → (Licit strong s ↔ ¬CoonKeine2021.PCCViolation CoonKeine2021.weakProbe true s) ∧ (Licit weak s ↔ ¬CoonKeine2021.PCCViolation CoonKeine2021.weakProbe false s) ∧ (Licit meFirst s ↔ ¬CoonKeine2021.PCCViolation CoonKeine2021.meFirstProbe false s) ∧ (Licit strictlyDescending s ↔ ¬CoonKeine2021.PCCViolation CoonKeine2021.ultrastrongProbe false s)

On the six cells the four varieties coincide with the gluttony probes of [CK21], so a probe that stops too early and one that agrees too much draw the same lines there.

The rows

def Deal2024.personOf (e : Datum) (key : String) : Option Person

Equations

• Deal2024.personOf e key = match e.feature? key with | some "1" => some Person.first | some "2" => some Person.second | some "3" => some Person.third | x => none

def Deal2024.grammarsOf (e : Datum) : List Grammar

The grammars of a row's language are listed by its pattern, Slovenian speakers having a strong or a weak PCC.

Equations

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

theorem Deal2024.rows (e : Datum) : e ∈ Examples.all → ∀ g ∈ grammarsOf e, ∀ io ∈ personOf e "io", ∀ do_ ∈ personOf e "do", e.judgment = Judgment.acceptable ↔ if e.feature? "preference" = some "io" then Licit g { high := do_, low := io } else Licit g { high := io, low := do_ }

Every clitic combination of the rows is grammatical exactly when the language's grammar licenses it, the probe meeting the indirect object first in the reverse-PCC rows of Shapsug Adyghe and of Slovenian with the direct object clitic first.