Linked frames and fusion

This file defines argument structures as linked frames and the fusion of one argument structure with another. A linked frame is an argument frame whose slots are linked to the thematic roles they admit, each slot either required of whatever fills the frame or open. A verb's lexical argument structure and the meaning of an argument structure construction are both linked frames. A clause arises when the verb's argument structure is fused with an event structure: a correspondence between their slots under which every pair of corresponding slots admits a common role, every slot the verb requires is fused, and every slot the event structure requires is filled. The slots of the event structure that nothing fuses with are contributed by it.

Main definitions

• RoleSlot, LinkedFrame: a slot's admitted roles, and a frame with its slots linked
• LinkedFrame.IsProfiled: a slot is profiled when it is a core slot of the frame
• LinkedFrame.Extends: one argument structure admits at least the roles of another
• IsFusion: a correspondence of slots obeying coherence and the two obligations
• contributed: the slots of the event structure no slot of the verb fuses with
• SubeventRelation: how the verb's event relates to the event structure's

Main results

• IsFusion.exists_fused: an event structure with a required slot shares a participant with every verb fused with it
• isFusion_refl: the identity correspondence fuses an argument structure with itself

Implementation notes

The roles a slot admits form a set of ThetaRole labels, and two slots are compatible when their sets meet. A correspondence is a map from slots to optional slots; IsFusionOn restates IsFusion over the verb's slots so that it can be decided, and ofFin builds a correspondence from a map between slot indices.

References

• [Gol95]
• [GJ04]
• [LRH05]

structure ArgumentStructure.RoleSlot : Type

A RoleSlot records the thematic roles a slot admits and whether the slot is required, whether of a verb that must express it or of a construction that must fuse it with a role of the verb, a solid line in [Gol95]'s diagrams (p. 51).

• admits : Finset ThetaRole

  The roles the slot admits.

• obligatory : Bool

  Whether the slot is required.

@[instance_reducible]

instance ArgumentStructure.instDecidableEqRoleSlot : DecidableEq RoleSlot

Equations

• ArgumentStructure.instDecidableEqRoleSlot = ArgumentStructure.instDecidableEqRoleSlot.decEq

def ArgumentStructure.instDecidableEqRoleSlot.decEq (x✝ x✝¹ : RoleSlot) : Decidable (x✝ = x✝¹)

Equations

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

structure ArgumentStructure.LinkedFrame : Type

A LinkedFrame is an argument structure, an argument frame with the role each of its slots is linked to. A verb's lexical argument structure (Verb.linkedFrame?) and the meaning of an argument structure construction ([Gol95] Fig. 2.4) are linked frames.

• frame : ArgumentFrame

  The frame.

• roles : List (ArgumentFrame.Slot × RoleSlot)

  The slots linked to roles.

@[instance_reducible]

instance ArgumentStructure.instDecidableEqLinkedFrame : DecidableEq LinkedFrame

Equations

• ArgumentStructure.instDecidableEqLinkedFrame = ArgumentStructure.instDecidableEqLinkedFrame.decEq

def ArgumentStructure.instDecidableEqLinkedFrame.decEq (x✝ x✝¹ : LinkedFrame) : Decidable (x✝ = x✝¹)

Equations

• ArgumentStructure.instDecidableEqLinkedFrame.decEq { frame := a, roles := a_1 } { frame := b, roles := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def ArgumentStructure.LinkedFrame.admits (L : LinkedFrame) (s : ArgumentFrame.Slot) : Finset ThetaRole

L.admits s is the set of roles the slot s admits, empty when s is not linked.

Equations

• L.admits s = (Option.map (fun (x : ArgumentStructure.RoleSlot) => x.admits) (List.lookup s L.roles)).getD ∅

def ArgumentStructure.LinkedFrame.obligatory (L : LinkedFrame) : List ArgumentFrame.Slot

L.obligatory lists the required slots.

Equations

• L.obligatory = List.map (fun (x : ArgumentFrame.Slot × ArgumentStructure.RoleSlot) => x.1) (List.filter (fun (x : ArgumentFrame.Slot × ArgumentStructure.RoleSlot) => x.2.obligatory) L.roles)

@[reducible, inline]

abbrev ArgumentStructure.LinkedFrame.IsProfiled (L : LinkedFrame) (s : ArgumentFrame.Slot) : Prop

A slot is profiled when it is a core slot of the frame, a subject or a nominal complement: "Every argument role linked to a direct grammatical relation (SUBJ, OBJ, or OBJ2) is constructionally profiled" ([Gol95], p. 48).

Equations

• L.IsProfiled s = (s ∈ L.frame.coreSlots)

def ArgumentStructure.LinkedFrame.WF (L : LinkedFrame) : Prop

A linked frame is well formed when every slot it links is a slot of its frame.

Equations

• L.WF = ∀ x ∈ L.roles, x.1 ∈ L.frame.slots

@[instance_reducible]

instance ArgumentStructure.LinkedFrame.instDecidableWF (L : LinkedFrame) : Decidable L.WF

Equations

• L.instDecidableWF = ArgumentStructure.LinkedFrame.instDecidableWF._aux_1 L

def ArgumentStructure.LinkedFrame.Extends (L L' : LinkedFrame) : Prop

L.Extends L' holds when L' has the frame of L and admits at each slot every role L admits there, as a paper's construal of a verb extends the argument structure its lexical entry derives.

Equations

• L.Extends L' = (L.frame = L'.frame ∧ ∀ x ∈ L.roles, x.2.admits ⊆ L'.admits x.1)

@[instance_reducible]

instance ArgumentStructure.LinkedFrame.instDecidableExtends (L L' : LinkedFrame) : Decidable (L.Extends L')

Equations

• L.instDecidableExtends L' = { decide := decide (L.frame = L'.frame) && decide (∀ x ∈ L.roles, x.2.admits ⊆ L'.admits x.1), reflects_decide := ⋯ }

inductive ArgumentStructure.SubeventRelation : Type

A SubeventRelation is how the event a verb designates relates to the event structure it is fused with ([Gol95], p. 65; [GJ04] §3).

• subtype : SubeventRelation

  The verb's event is a subtype of the event structure's, what the diagrams of [Gol95] label "instance".

• means : SubeventRelation

  The verb's event is the means of the event structure's.

• result : SubeventRelation

  The verb's event is the result of the event structure's.

• precondition : SubeventRelation

  The verb's event is a precondition of the event structure's.

• manner : SubeventRelation

  The verb's event is the manner of the event structure's.

• identification : SubeventRelation

  The verb's event is the means of identifying the event structure's.

• intendedResult : SubeventRelation

  The verb's event is the intended result of the event structure's.

• coOccurrence : SubeventRelation

  The two events merely co-occur ([GJ04] (18a)).

@[instance_reducible]

instance ArgumentStructure.instDecidableEqSubeventRelation : DecidableEq SubeventRelation

Equations

• ArgumentStructure.instDecidableEqSubeventRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ArgumentStructure.instReprSubeventRelation.repr : SubeventRelation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentStructure.instReprSubeventRelation : Repr SubeventRelation

Equations

• ArgumentStructure.instReprSubeventRelation = { reprPrec := ArgumentStructure.instReprSubeventRelation.repr }

structure ArgumentStructure.IsFusion (V C : LinkedFrame) (σ : ArgumentFrame.Slot → Option ArgumentFrame.Slot) : Prop

IsFusion V C σ holds when σ fuses the argument structure V with the event structure C: corresponding slots admit a common role, the Semantic Coherence Principle of [Gol95] (p. 50), σ lands in C's frame, and every required slot on either side takes part.

• coherent (s t : ArgumentFrame.Slot) : σ s = some t → ¬Disjoint (V.admits s) (C.admits t)

  Corresponding slots admit a common role.

• mem_target (s t : ArgumentFrame.Slot) : σ s = some t → t ∈ C.frame.slots

  The correspondence lands in the frame of the event structure.

• obligatory_source (s : ArgumentFrame.Slot) : s ∈ V.obligatory → (σ s).isSome = true

  Every required slot of the verb is fused.

• obligatory_target (t : ArgumentFrame.Slot) : t ∈ C.obligatory → ∃ s ∈ V.frame.slots, σ s = some t

  Every required slot of the event structure is fused with a slot of the verb.

def ArgumentStructure.contributed (V C : LinkedFrame) (σ : ArgumentFrame.Slot → Option ArgumentFrame.Slot) : List ArgumentFrame.Slot

contributed V C σ lists the slots of C that no slot of V fuses with, the roles a construction contributes to a verb ([Gol95], p. 54).

Equations

• ArgumentStructure.contributed V C σ = List.filter (fun (t : ArgumentFrame.Slot) => V.frame.slots.all fun (s : ArgumentFrame.Slot) => σ s != some t) C.frame.slots

def ArgumentStructure.IsFusionOn (V C : LinkedFrame) (σ : ArgumentFrame.Slot → Option ArgumentFrame.Slot) : Prop

IsFusionOn V C σ restates IsFusion V C σ over the slots of V, a decidable form.

Equations

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

@[instance_reducible]

instance ArgumentStructure.instDecidableIsFusionOn (V C : LinkedFrame) (σ : ArgumentFrame.Slot → Option ArgumentFrame.Slot) : Decidable (IsFusionOn V C σ)

Equations

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

def ArgumentStructure.ofFin (vs cs : List ArgumentFrame.Slot) (f : Fin vs.length → Option (Fin cs.length)) : ArgumentFrame.Slot → Option ArgumentFrame.Slot

ofFin vs cs f is the correspondence that sends the ith slot of vs to the f ith slot of cs, and every other slot nowhere.

Equations

• ArgumentStructure.ofFin vs cs f s = match List.idxOf? s vs with | some i => if hi : i < vs.length then Option.map (fun (j : Fin cs.length) => cs[j]) (f ⟨i, hi⟩) else none | none => none

theorem ArgumentStructure.mem_contributed_iff {V C : LinkedFrame} {σ : ArgumentFrame.Slot → Option ArgumentFrame.Slot} {t : ArgumentFrame.Slot} : t ∈ contributed V C σ ↔ t ∈ C.frame.slots ∧ ∀ s ∈ V.frame.slots, σ s ≠ some t

theorem ArgumentStructure.isFusionOn_iff_isFusion {V C : LinkedFrame} {σ : ArgumentFrame.Slot → Option ArgumentFrame.Slot} (hσ : ∀ s ∉ V.frame.slots, σ s = none) : IsFusionOn V C σ ↔ IsFusion V C σ

IsFusionOn is IsFusion for a correspondence that sends no slot outside the verb's frame anywhere.

theorem ArgumentStructure.IsFusion.exists_fused {V C : LinkedFrame} {σ : ArgumentFrame.Slot → Option ArgumentFrame.Slot} (h : IsFusion V C σ) (ha : C.obligatory ≠ []) : ∃ (s : ArgumentFrame.Slot) (t : ArgumentFrame.Slot), σ s = some t

An event structure with a required slot shares a participant with every verb fused with it, the Shared Participant Condition [Gol95] adopts from Matsumoto (p. 65).

theorem ArgumentStructure.isFusion_refl {V : LinkedFrame} (hV : V.WF) (hne : ∀ s ∈ V.frame.slots, (V.admits s).Nonempty) : IsFusion V V fun (s : ArgumentFrame.Slot) => if s ∈ V.frame.slots then some s else none

The identity correspondence fuses a well-formed argument structure whose slots all admit some role with itself, the case in which a verb's own argument structure is the clause's.