Staps and Rooryck (2024): Formalizing Spatial-Causal Polysemy of Agent Prepositions

Staps and Rooryck analyze the French agent prepositions par and de. Against accounts on which the agent preposition of a passive is a vacuous case marker, they give each preposition one polymorphically typed denotation, in the sense of Tyler and Evans's principled polysemy, instantiated by the syntactic context. In causal adjuncts, in Copley and Harley's force-theoretic frame, de names a causing situation and par a force. In passives the by-phrase is the external argument of Angelopoulos, Collins and Terzi, combined with the verb by Event Identification. The agentive instantiations share the at-issue relation Initiator and differ in presupposition, high proto-agentivity for par and low for de, where proto-agentivity is relational in the terms of Dowty and of Hopper and Thompson: bringing about a change, volitionality and telicity, with change primary. Over the fragment's verbs this derives the paper's readings, such as the exclusion of de by verbs of change.

Main definitions

• parCausal: par in a causal adjunct.
• deCausal: de in a causal adjunct.
• parAgentive: par in a passive.
• deAgentive: de in a passive.
• Construal: the agent's relation to the event, ordered by proto-agentivity.

Main results

• parCausal_net_of_deCausal: a cause de names is, through its net force, one par names.
• voicePass_eventIdentification: passive Voice's closure is redundant under a by-phrase.
• change_verbs_exclude_de: verbs of change exclude de.
• psych_verbs_allow_both: psych verbs allow both prepositions.
• dependsOnProximate_of_dependsOnDistal: an effect depends on a distal cause only where it depends on the proximate one.

Implementation notes

The paper gives no threshold between high and low proto-agentivity and reports an informal survey of twenty-one speakers on a six-point scale only to confirm its judgments; the means it reports are not reproduced. Change on a contextually inferred scale, which lets the psych verbs take par when the emotion has effects, is beyond the lexical construals and is not formalized. The stative/dynamic contrast, which the paper finds never decisive on its own, is not a coordinate of Construal. Straub's generalization that non-stative verbs take par, stative verbs with animate agents either preposition and stative verbs with inanimate agents de is described in the paper as too coarse, since a stative verb with an inanimate agent allows par when a change on an inferred scale is at stake.

References

• [SR24]
• [TE03]
• [Cro12]
• [CH15]
• [CH22]
• [ACT20]
• [Kra96]
• [Dow91]
• [HT80]
• [Str74]
• [HP05]

Polymorphic types

inductive StapsRooryck2024.SemDomain : Type

The domain types of the paper's type system are entities, situations and forces.

• e : SemDomain
• s : SemDomain
• f : SemDomain

@[instance_reducible]

instance StapsRooryck2024.instDecidableEqSemDomain : DecidableEq SemDomain

Equations

• StapsRooryck2024.instDecidableEqSemDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance StapsRooryck2024.instReprSemDomain : Repr SemDomain

Equations

• StapsRooryck2024.instReprSemDomain = { reprPrec := StapsRooryck2024.instReprSemDomain.repr }

def StapsRooryck2024.instReprSemDomain.repr : SemDomain → ℕ → Std.Format

Equations

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

structure StapsRooryck2024.PrepType : Type

A preposition type ⟨η, ⟨θ, t⟩⟩ pairs the domain of the ground with the domain of the figure.

• ground : SemDomain
• figure : SemDomain

@[instance_reducible]

instance StapsRooryck2024.instDecidableEqPrepType : DecidableEq PrepType

Equations

• StapsRooryck2024.instDecidableEqPrepType = StapsRooryck2024.instDecidableEqPrepType.decEq

def StapsRooryck2024.instDecidableEqPrepType.decEq (x✝ x✝¹ : PrepType) : Decidable (x✝ = x✝¹)

Equations

• StapsRooryck2024.instDecidableEqPrepType.decEq { ground := a, figure := a_1 } { ground := b, figure := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def StapsRooryck2024.instReprPrepType.repr : PrepType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance StapsRooryck2024.instReprPrepType : Repr PrepType

Equations

• StapsRooryck2024.instReprPrepType = { reprPrec := StapsRooryck2024.instReprPrepType.repr }

def StapsRooryck2024.Dom (Entity S : Type u) : SemDomain → Type u

Dom interprets the domain types in the force-theoretic frame of [CH22], where a force is a function from situations to situations.

Equations

• StapsRooryck2024.Dom Entity S StapsRooryck2024.SemDomain.e = Entity
• StapsRooryck2024.Dom Entity S StapsRooryck2024.SemDomain.s = S
• StapsRooryck2024.Dom Entity S StapsRooryck2024.SemDomain.f = (S → S)

@[reducible, inline]

abbrev StapsRooryck2024.Rel (Entity S : Type u) (t : PrepType) : Type u

A relation of type ⟨η, ⟨θ, t⟩⟩ relates a ground to a figure.

Equations

• StapsRooryck2024.Rel Entity S t = (StapsRooryck2024.Dom Entity S t.ground → StapsRooryck2024.Dom Entity S t.figure → Prop)

Causal adjuncts

def StapsRooryck2024.parCausal {Entity S : Type u} (net : S → S → S) : Rel Entity S { ground := SemDomain.f, figure := SemDomain.s }

par in a causal adjunct, at type ⟨f, ⟨s, t⟩⟩ (14b), holds when the situation comes about through the force, the net force of some situation the force maps to it.

Equations

• StapsRooryck2024.parCausal net f s = ∃ (s₀ : S), net s₀ = f ∧ f s₀ = s

def StapsRooryck2024.deCausal {Entity S : Type u} (net : S → S → S) : Rel Entity S { ground := SemDomain.s, figure := SemDomain.s }

de in a causal adjunct, at type ⟨s, ⟨s, t⟩⟩ (15b), holds when the situation arises from the causing situation, whose net force maps it to the situation.

Equations

• StapsRooryck2024.deCausal net s s' = (net s s = s')

theorem StapsRooryck2024.parCausal_net_of_deCausal {Entity S : Type u} (net : S → S → S) {s s' : S} (h : deCausal net s s') : parCausal net (net s) s'

A cause de names as a situation is, through its net force, a cause par names as a force, so both prepositions describe the same causal event.

By-phrases in passives

def StapsRooryck2024.byPhrase {Entity : Type u_1} {E : Type u_2} (init : Entity → E → Prop) (x : Entity) : E → Prop

The by-phrase (10b) is the agentive instantiation applied to its argument, a predicate of events at type ⟨s, t⟩.

Equations

• StapsRooryck2024.byPhrase init x = init x

def StapsRooryck2024.voicePass {Entity : Type u_1} {E : Type u_2} (p : Entity → E → Prop) : E → Prop

Passive Voice (9b) is the existential closure of the external argument.

Equations

• StapsRooryck2024.voicePass p e = ∃ (x : Entity), p x e

theorem StapsRooryck2024.voicePass_eventIdentification {Entity : Type u_1} {E : Type u_2} (init : Entity → E → Prop) (body : E → Prop) (j : Entity) (e : E) : voicePass (ArgumentStructure.eventIdentification (fun (x : Entity) (e : E) => init x e ∧ body e) (byPhrase init j)) e ↔ init j e ∧ body e

In (10) the by-phrase combines with the verb's denotation by Event Identification and the closure passive Voice performs is redundant, since the by-phrase supplies the initiator.

noncomputable def StapsRooryck2024.parAgentive {Entity : Type u_1} {E : Type u_2} (init High : Entity → E → Prop) (x : Entity) : E → SignType

par in a passive (35a) is the initiator relation, presupposing high proto-agentivity of the agent in the event. The evaluation point of the trivalent proposition is the event.

Equations

• StapsRooryck2024.parAgentive init High x = {e : E | High x e}.indicator fun (e : E) => SignType.ofProp (init x e)

noncomputable def StapsRooryck2024.deAgentive {Entity : Type u_1} {E : Type u_2} (init High : Entity → E → Prop) (x : Entity) : E → SignType

de in a passive (35b) is the initiator relation, presupposing low proto-agentivity.

Equations

• StapsRooryck2024.deAgentive init High x = {e : E | ¬High x e}.indicator fun (e : E) => SignType.ofProp (init x e)

theorem StapsRooryck2024.agentive_eq_one_iff_of_ne_zero {Entity : Type u_1} {E : Type u_2} (init High : Entity → E → Prop) (x : Entity) (e : E) : (parAgentive init High x e ≠ 0 → (parAgentive init High x e = 1 ↔ init x e)) ∧ (deAgentive init High x e ≠ 0 → (deAgentive init High x e = 1 ↔ init x e))

The two prepositions share their at-issue content, each being the initiator relation wherever it is defined.

theorem StapsRooryck2024.parAgentive_ne_zero_iff {Entity : Type u_1} {E : Type u_2} (init High : Entity → E → Prop) (x : Entity) (e : E) : parAgentive init High x e ≠ 0 ↔ deAgentive init High x e = 0

Their presuppositions are complementary.

Proto-agentivity

structure StapsRooryck2024.Construal : Type

A construal records the agent's relation to the event by the relational proto-agentivity properties the paper finds decisive, bringing about a change, volitionality and telicity.

• change : Bool
• volition : Bool
• telic : Bool

@[instance_reducible]

instance StapsRooryck2024.instDecidableEqConstrual : DecidableEq Construal

Equations

• StapsRooryck2024.instDecidableEqConstrual = StapsRooryck2024.instDecidableEqConstrual.decEq

def StapsRooryck2024.instDecidableEqConstrual.decEq (x✝ x✝¹ : Construal) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance StapsRooryck2024.instReprConstrual : Repr Construal

Equations

• StapsRooryck2024.instReprConstrual = { reprPrec := StapsRooryck2024.instReprConstrual.repr }

def StapsRooryck2024.instReprConstrual.repr : Construal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance StapsRooryck2024.instFintypeConstrual : Fintype Construal

Equations

• StapsRooryck2024.instFintypeConstrual = Fintype.ofEquiv ((_ : Bool) × (_ : Bool) × Bool) StapsRooryck2024.Construal.proxyTypeEquiv

def StapsRooryck2024.Construal.LE (c d : Construal) : Prop

In the order of proto-agentivity (34), change is primary, and among construals agreeing on change, more volitionality or telicity is more proto-agentive.

Equations

• c.LE d = ((c.change = true → d.change = true) ∧ (c.change = d.change → (c.volition = true → d.volition = true) ∧ (c.telic = true → d.telic = true)))

@[instance_reducible]

instance StapsRooryck2024.Construal.instLE : LE Construal

Equations

• StapsRooryck2024.Construal.instLE = { le := StapsRooryck2024.Construal.LE }

@[instance_reducible]

instance StapsRooryck2024.Construal.instDecidableLe (c d : Construal) : Decidable (c ≤ d)

Equations

• c.instDecidableLe d = id (id inferInstance)

@[instance_reducible]

instance StapsRooryck2024.Construal.instPartialOrder : PartialOrder Construal

Equations

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

@[instance_reducible]

instance StapsRooryck2024.Construal.instDecidableLT : DecidableLT Construal

Equations

• StapsRooryck2024.Construal.instDecidableLT = decidableLTOfDecidableLE

theorem StapsRooryck2024.Construal.lt_of_change (c d : Construal) : c.change = false → d.change = true → c < d

By (34a), a construal bringing about a change is more proto-agentive than any that does not, whatever their volitionality and telicity.

theorem StapsRooryck2024.Construal.le_iff_of_not_change (c d : Construal) : c.change = false → d.change = false → (c ≤ d ↔ (c.volition = true → d.volition = true) ∧ (c.telic = true → d.telic = true))

By (34b), among construals that bring about no change, proto-agentivity is volitionality and telicity.

def StapsRooryck2024.construal (v : Verb) : Construal

The construal a verb entry lexicalizes reads change off the subject's causation entailment, volitionality off its volition entailment, and telicity off the Vendler class.

Equations

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

def StapsRooryck2024.ParSelects (senses : List Verb) (v : Verb) : Prop

Par selects a sense whose construal is at least as proto-agentive as that of every sense the verb makes available.

Equations

• StapsRooryck2024.ParSelects senses v = ∀ u ∈ senses, StapsRooryck2024.construal u ≤ StapsRooryck2024.construal v

def StapsRooryck2024.DeSelects (senses : List Verb) (v : Verb) : Prop

De selects a sense whose construal brings about no change and is at most as proto-agentive as that of every sense the verb makes available.

Equations

• StapsRooryck2024.DeSelects senses v = ((StapsRooryck2024.construal v).change = false ∧ ∀ u ∈ senses, StapsRooryck2024.construal v ≤ StapsRooryck2024.construal u)

@[instance_reducible]

instance StapsRooryck2024.instDecidableParSelects (senses : List Verb) (v : Verb) : Decidable (ParSelects senses v)

Equations

• StapsRooryck2024.instDecidableParSelects senses v = id inferInstance

@[instance_reducible]

instance StapsRooryck2024.instDecidableDeSelects (senses : List Verb) (v : Verb) : Decidable (DeSelects senses v)

Equations

• StapsRooryck2024.instDecidableDeSelects senses v = id inferInstance

theorem StapsRooryck2024.change_verbs_exclude_de (v : Verb) : v ∈ [French.Verbs.laver, French.Verbs.briser, French.Verbs.ecrire, French.Verbs.construire, French.Verbs.tuer] → ParSelects [v] v ∧ ¬DeSelects [v] v

The prototypically transitive verbs of Table 1 bring about a change and exclude de.

theorem StapsRooryck2024.psych_verbs_allow_both (v : Verb) : v ∈ [French.Verbs.aimer, French.Verbs.adorer, French.Verbs.respecter] → ParSelects [v] v ∧ DeSelects [v] v

The psych verbs of Table 1 bring about no change and allow both prepositions.

def StapsRooryck2024.suivreSenses : List Verb

The two senses of suivre are goal-directed following and the positional relation.

Equations

• StapsRooryck2024.suivreSenses = [French.Verbs.suivreDyn, French.Verbs.suivreStat]

theorem StapsRooryck2024.par_suivre : ParSelects suivreSenses French.Verbs.suivreDyn ∧ ¬ParSelects suivreSenses French.Verbs.suivreStat

Par selects the volitional sense of suivre (25b).

theorem StapsRooryck2024.de_suivre : DeSelects suivreSenses French.Verbs.suivreStat ∧ ¬DeSelects suivreSenses French.Verbs.suivreDyn

De selects the positional sense of suivre (26a).

def StapsRooryck2024.abandonnerSenses : List Verb

The two senses of abandonner are the telic abandoning and the stative neglect.

Equations

• StapsRooryck2024.abandonnerSenses = [French.Verbs.abandonner, French.Verbs.abandonnerStat]

theorem StapsRooryck2024.par_abandonner : ParSelects abandonnerSenses French.Verbs.abandonner ∧ ¬ParSelects abandonnerSenses French.Verbs.abandonnerStat

Par selects the telic sense of abandonner (31a).

theorem StapsRooryck2024.de_abandonner : DeSelects abandonnerSenses French.Verbs.abandonnerStat ∧ ¬DeSelects abandonnerSenses French.Verbs.abandonner

De selects the atelic sense of abandonner (31b).

Causal distance

def StapsRooryck2024.DependsOnDistal {P : Type u_1} {Q : Type u_2} {X : Type u_3} {Y : Type u_4} {Z : Type u_5} (g : P → X → Y) (h : Q → Y → Z) (p : P) (q : Q) (x : X) : Prop

In the causal model (36), where Y depends on X and Z on Y, the effect depends on the distal cause in a case when another value of the distal cause changes it.

Equations

• StapsRooryck2024.DependsOnDistal g h p q x = ∃ (x' : X), h q (g p x') ≠ h q (g p x)

def StapsRooryck2024.DependsOnProximate {P : Type u_1} {Q : Type u_2} {X : Type u_3} {Y : Type u_4} {Z : Type u_5} (g : P → X → Y) (h : Q → Y → Z) (p : P) (q : Q) (x : X) : Prop

The effect depends on the proximate cause in a case when another value of it changes the effect.

Equations

• StapsRooryck2024.DependsOnProximate g h p q x = ∃ (y' : Y), h q y' ≠ h q (g p x)

theorem StapsRooryck2024.dependsOnProximate_of_dependsOnDistal {P : Type u_1} {Q : Type u_2} {X : Type u_3} {Y : Type u_4} {Z : Type u_5} (g : P → X → Y) (h : Q → Y → Z) {p : P} {q : Q} {x : X} (hd : DependsOnDistal g h p q x) : DependsOnProximate g h p q x

The cases in which the effect depends on the distal cause are among those in which it depends on the proximate cause. Greater causal distance means less dependency, which the paper offers as a reason the ablative de marks low proto-agentivity.