Documentation

Linglib.Theories.Semantics.Causation.CauserSort

Causer sort lattice #

@cite{beavers-zubair-2013} @cite{levin-hovav-1995}

CauserSort is the sortal-type lattice for causers from @cite{beavers-zubair-2013} ex. (81). Atoms are event, state, individual; named sorts are event, state, eventuality (= event ⊔ state), individual, and any (top). The order is subset-on-atoms.

The structure is a SemilatticeSup (joins exist for every pair) but not a Lattice — event ⊓ state would be the empty Finset, which has no constructor.

The anticausativization operator (B&Z's ex. (77)) requires the surviving causer position to resolve to individual, which mechanically blocks roots that select for event or eventuality (e.g., murder, destroy). The volitive operator (their ex. (71)) requires event. Both predictions follow from ≤-checks on the lattice rather than from stipulated lexical exceptions.

inductive Semantics.Causation.CauserSortAtom :

The three irreducible sorts (atoms) a causer position may resolve to. Used as the underlying Finset of CauserSort; not intended as a standalone API.

event : CauserSortAtom
state : CauserSortAtom
individual : CauserSortAtom

Instances For

@[implicit_reducible]

instance Semantics.Causation.instDecidableEqCauserSortAtom :

DecidableEq CauserSortAtom

Equations

Semantics.Causation.instDecidableEqCauserSortAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Causation.instReprCauserSortAtom.repr :

CauserSortAtom → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Causation.instReprCauserSortAtom :

Repr CauserSortAtom

Equations

Semantics.Causation.instReprCauserSortAtom = { reprPrec := Semantics.Causation.instReprCauserSortAtom.repr }

@[implicit_reducible]

instance Semantics.Causation.instFintypeCauserSortAtom :

Fintype CauserSortAtom

Equations

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

inductive Semantics.Causation.CauserSort :

Sortal type a verb may select for its causer argument (@cite{beavers-zubair-2013} ex. (81), p. 40).

The Hasse diagram:

          any (U)
         /        \
   eventuality   individual (U_I)
    (U_V)
    /     \
 event   state
 (U_E)   (U_S)

Verbs select for the SMALLEST sort their causer must satisfy:

break-roots (kada-): any — no sortal restriction
destroy-roots: eventuality — must be a state or event
murder-roots (minimara-): event — must be an event (forces agentivity since events have agents in the relevant sense)

The causer-suppression operator requires the suppressed causer position to resolve to individual. Suppression is well-formed iff individual ≤ s — only any and individual itself satisfy this.

event : CauserSort
U_E in B&Z's notation: the causer must be an event.
state : CauserSort
U_S: the causer must be a state. Predicted but not lexically attested: B&Z 2013 fn. 40 (p. 40) note they have not discussed verbs lexically selecting a stative causer, suggesting bloom-type ICOS verbs (cf. @cite{levin-hovav-1995} p. 97) as a possible case for future work. Kept as a constructor so the lattice retains the structure (81) advertises.
eventuality : CauserSort
U_V = U_E ∪ U_S: the causer must be an eventuality.
individual : CauserSort
U_I: the causer must be an individual.
any : CauserSort
U: no sortal restriction.

Instances For

@[implicit_reducible]

instance Semantics.Causation.instDecidableEqCauserSort :

DecidableEq CauserSort

Equations

Semantics.Causation.instDecidableEqCauserSort x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Causation.instReprCauserSort.repr :

CauserSort → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Causation.instReprCauserSort :

Repr CauserSort

Equations

Semantics.Causation.instReprCauserSort = { reprPrec := Semantics.Causation.instReprCauserSort.repr }

@[implicit_reducible]

instance Semantics.Causation.instFintypeCauserSort :

Fintype CauserSort

Equations

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

def Semantics.Causation.CauserSort.toAtoms :

CauserSort → Finset CauserSortAtom

The Finset of atoms a sort covers. The subsort order is Finset.Subset pulled back through this map.

Equations

Instances For

@[implicit_reducible]

instance Semantics.Causation.CauserSort.instLE :

Equations

Semantics.Causation.CauserSort.instLE = { le := fun (s t : Semantics.Causation.CauserSort) => s.toAtoms ⊆ t.toAtoms }

@[implicit_reducible]

instance Semantics.Causation.CauserSort.instDecidableRelLe :

DecidableRel fun (x1 x2 : CauserSort) => x1 ≤ x2

Equations

s.instDecidableRelLe t = s.toAtoms.instDecidableRelSubset t.toAtoms

@[implicit_reducible]

instance Semantics.Causation.CauserSort.instPartialOrder :

PartialOrder CauserSort

Equations

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

def Semantics.Causation.CauserSort.sup :

CauserSort → CauserSort → CauserSort

Join: the smallest named sort whose atoms include both inputs. Each case is a specific (s, t) pair; no overlapping wildcards.

Equations

Instances For

@[implicit_reducible]

instance Semantics.Causation.CauserSort.instMax :

Equations

Semantics.Causation.CauserSort.instMax = { max := Semantics.Causation.CauserSort.sup }

@[implicit_reducible]

instance Semantics.Causation.CauserSort.instSemilatticeSup :

SemilatticeSup CauserSort

Equations

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

@[reducible, inline]

abbrev Semantics.Causation.CauserSort.admitsIndividual (s : CauserSort) :

The well-formedness condition for the B&Z 2013 causer-suppression operator (their ex. (77)): the suppressed causer position resolves to individual, so the verb's selected sort must admit individual values.

This is the predictive engine of B&Z 2013: the lattice structure determines which roots anticausativize, by structural type-checking rather than by stipulation.

Equations

s.admitsIndividual = (Semantics.Causation.CauserSort.individual ≤ s)

Instances For

@[reducible, inline]

abbrev Semantics.Causation.CauserSort.admitsVolitive (s : CauserSort) :

The well-formedness condition for B&Z's volitive operator (their ex. (71), p. 35): ⟦+∅_vol⟧ = λP...λv ∈ U_E λe[...] requires the penultimate argument to be an event. After causer suppression the surviving subject is sortally individual, so the volitive cannot apply — the formal content of "anticausatives are always involitive" (@cite{beavers-zubair-2013} §8).

Equations

s.admitsVolitive = (Semantics.Causation.CauserSort.event ≤ s)

Instances For