inductive DepGrammar.CRDC.ValentType : Type

Syntactic types of valents in a valency frame

• N : ValentType
• T : ValentType
• I : ValentType
• A : ValentType
• Pa : ValentType
• Pr : ValentType
• C : ValentType
• P : ValentType
• R : ValentType

def DepGrammar.CRDC.instReprValentType.repr : ValentType → ℕ → Std.Format

Equations

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

instance DepGrammar.CRDC.instReprValentType : Repr ValentType

Equations

• DepGrammar.CRDC.instReprValentType = { reprPrec := DepGrammar.CRDC.instReprValentType.repr }

instance DepGrammar.CRDC.instDecidableEqValentType : DecidableEq ValentType

Equations

• DepGrammar.CRDC.instDecidableEqValentType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure DepGrammar.CRDC.ValentSlot : Type

A slot in a valency frame

Captures the notation from @cite{osborne-2019}:

• isArgument corresponds to the a subscript
• isRaised corresponds to the ↑ marker
• label captures grammatical function (subj, obj, etc.)

• type : ValentType

  The syntactic type of this valent

• isArgument : Bool

  Is this valent semantically selected (an argument)?

• isRaised : Bool

  Is this valent "raised" (appears elsewhere in structure)?

• label : Option String

  Grammatical function label

def DepGrammar.CRDC.instReprValentSlot.repr : ValentSlot → ℕ → Std.Format

Equations

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

instance DepGrammar.CRDC.instReprValentSlot : Repr ValentSlot

Equations

• DepGrammar.CRDC.instReprValentSlot = { reprPrec := DepGrammar.CRDC.instReprValentSlot.repr }

def DepGrammar.CRDC.instDecidableEqValentSlot.decEq (x✝ x✝¹ : ValentSlot) : Decidable (x✝ = x✝¹)

Equations

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

instance DepGrammar.CRDC.instDecidableEqValentSlot : DecidableEq ValentSlot

Equations

• DepGrammar.CRDC.instDecidableEqValentSlot = DepGrammar.CRDC.instDecidableEqValentSlot.decEq

structure DepGrammar.CRDC.ValencyFrame : Type

A valency frame specifies the combinatory potential of a word

Following @cite{osborne-2019}, valents are ordered by obliqueness: subject > direct object > indirect object > oblique

• carrier : String

  The word this frame belongs to

• isFinite : Bool

  Whether this is for a finite form

• valents : List ValentSlot

  The valent slots, ordered by obliqueness (subject first)

def DepGrammar.CRDC.instReprValencyFrame.repr : ValencyFrame → ℕ → Std.Format

Equations

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

instance DepGrammar.CRDC.instReprValencyFrame : Repr ValencyFrame

Equations

• DepGrammar.CRDC.instReprValencyFrame = { reprPrec := DepGrammar.CRDC.instReprValencyFrame.repr }

def DepGrammar.CRDC.Na_subj : ValentSlot

Na = Nominal argument (subject position)

Equations

• DepGrammar.CRDC.Na_subj = { type := DepGrammar.CRDC.ValentType.N, isArgument := true, label := some "subj" }

def DepGrammar.CRDC.Na_obj : ValentSlot

Na = Nominal argument (object position)

Equations

• DepGrammar.CRDC.Na_obj = { type := DepGrammar.CRDC.ValentType.N, isArgument := true, label := some "obj" }

def DepGrammar.CRDC.Na_iobj : ValentSlot

Na = Nominal argument (indirect object)

Equations

• DepGrammar.CRDC.Na_iobj = { type := DepGrammar.CRDC.ValentType.N, isArgument := true, label := some "iobj" }

def DepGrammar.CRDC.N_raised : ValentSlot

N = Nominal non-argument (raised element)

Equations

• DepGrammar.CRDC.N_raised = { type := DepGrammar.CRDC.ValentType.N, isArgument := false, isRaised := true }

def DepGrammar.CRDC.Ta : ValentSlot

Ta = To-infinitive argument

Equations

• DepGrammar.CRDC.Ta = { type := DepGrammar.CRDC.ValentType.T, isArgument := true }

def DepGrammar.CRDC.R_subj : ValentSlot

R = Raised subject (unrestricted category, not selected)

Equations

• DepGrammar.CRDC.R_subj = { type := DepGrammar.CRDC.ValentType.R, isArgument := false, label := some "subj" }

inductive DepGrammar.CRDC.ValentStatus : Type

Valent status for CRDC binding

In Osborne & Li's terms:

• Full valent: Can serve as antecedent (typically subject arguments)
• Conjunct valent: Must find antecedent among preceding full valents

• full : ValentStatus
• conjunct : ValentStatus

def DepGrammar.CRDC.instReprValentStatus.repr : ValentStatus → ℕ → Std.Format

Equations

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

instance DepGrammar.CRDC.instReprValentStatus : Repr ValentStatus

Equations

• DepGrammar.CRDC.instReprValentStatus = { reprPrec := DepGrammar.CRDC.instReprValentStatus.repr }

instance DepGrammar.CRDC.instDecidableEqValentStatus : DecidableEq ValentStatus

Equations

• DepGrammar.CRDC.instDecidableEqValentStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DepGrammar.CRDC.valentStatus (slot : ValentSlot) (position : ℕ) : ValentStatus

Determine if a valent slot is a "full valent" or "conjunct valent"

The key insight from CRDC: binding is determined by position in the valency frame, not by tree geometry or obliqueness hierarchy.

For simple transitives:

• Position 0 (subject) = full valent
• Position 1+ = conjunct valent (if reflexive)

This captures the intuition that subjects can bind objects, but not vice versa, purely from valency frame structure.

Equations

• DepGrammar.CRDC.valentStatus slot position = if (position == 0 && slot.isArgument) = true then DepGrammar.CRDC.ValentStatus.full else DepGrammar.CRDC.ValentStatus.conjunct

structure DepGrammar.CRDC.CRDCConfig : Type

Configuration for checking CRDC

The CRDC states: A reflexive (conjunct valent) must be bound by a preceding full valent in the same valency frame.

• frame : ValencyFrame

  The valency frame of the predicate

• antecedentIdx : ℕ

  Index of the potential antecedent in the frame

• anaphorIdx : ℕ

  Index of the anaphor in the frame

def DepGrammar.CRDC.getAt? {α : Type} (xs : List α) (i : ℕ) : Option α

Get element at index from list

Equations

• DepGrammar.CRDC.getAt? xs i = xs[i]?

def DepGrammar.CRDC.crdcSatisfied (config : CRDCConfig) : Bool

Check if CRDC is satisfied

Requirements:

1. Antecedent must be a full valent
2. Anaphor must be a conjunct valent
3. Antecedent must precede anaphor in valency frame

Equations

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

def DepGrammar.CRDC.intransitiveFrame (verb : String) : ValencyFrame

Valency frame for intransitive verbs: sleepf [Na]

Example: "They slept"

Equations

• DepGrammar.CRDC.intransitiveFrame verb = { carrier := verb, isFinite := true, valents := [DepGrammar.CRDC.Na_subj] }

def DepGrammar.CRDC.transitiveFrame (verb : String) : ValencyFrame

Valency frame for transitive verbs: discussf [Na, Na]

Example: "We discussed the issue"

Equations

• DepGrammar.CRDC.transitiveFrame verb = { carrier := verb, isFinite := true, valents := [DepGrammar.CRDC.Na_subj, DepGrammar.CRDC.Na_obj] }

def DepGrammar.CRDC.ditransitiveFrame (verb : String) : ValencyFrame

Valency frame for ditransitive verbs: givef [Na, Na, Na]

Example: "Sam gave them a pie"

Equations

• DepGrammar.CRDC.ditransitiveFrame verb = { carrier := verb, isFinite := true, valents := [DepGrammar.CRDC.Na_subj, DepGrammar.CRDC.Na_iobj, DepGrammar.CRDC.Na_obj] }

def DepGrammar.CRDC.raisingFrame (verb : String) : ValencyFrame

Valency frame for raising verbs: appearf [N, Ta]

Example: "Tom appears to be upset" Note: First N lacks a subscript (not semantically selected)

Equations

• DepGrammar.CRDC.raisingFrame verb = { carrier := verb, isFinite := true, valents := [DepGrammar.CRDC.N_raised, DepGrammar.CRDC.Ta] }

structure DepGrammar.CRDC.ValencyClause : Type

A clause analyzed with its valency frame

• subject : Word
• verb : Word
• object : Option Word
• frame : ValencyFrame

  The valency frame for this verb form

def DepGrammar.CRDC.instReprValencyClause.repr : ValencyClause → ℕ → Std.Format

Equations

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

instance DepGrammar.CRDC.instReprValencyClause : Repr ValencyClause

Equations

• DepGrammar.CRDC.instReprValencyClause = { reprPrec := DepGrammar.CRDC.instReprValencyClause.repr }

def DepGrammar.CRDC.parseValencyClause (ws : List Word) : Option ValencyClause

Parse a sentence into a valency clause

Equations

• One or more equations did not get rendered due to their size.
• DepGrammar.CRDC.parseValencyClause ws = none

def DepGrammar.CRDC.reflexiveLicensed (clause : ValencyClause) : Bool

Reflexive licensing under CRDC

A reflexive must be:

1. A conjunct valent in some valency frame
2. Preceded by a full valent in that frame
3. In agreement with the full valent

Equations

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

def DepGrammar.CRDC.reciprocalLicensed (clause : ValencyClause) : Bool

Reciprocal licensing under CRDC

A reciprocal must be:

1. A conjunct valent in some valency frame
2. Preceded by a full valent in that frame
3. The full valent must be plural

Equations

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

def DepGrammar.CRDC.pronounLocallyFree (_clause : ValencyClause) : Bool

Pronoun constraint under CRDC

A pronoun as conjunct valent cannot corefer with the full valent in the same valency frame.

Equations

• DepGrammar.CRDC.pronounLocallyFree _clause = false

def DepGrammar.CRDC.grammaticalForCoreference (ws : List Word) : Bool

Is a sentence grammatical for coreference under CRDC?

Equations

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

def DepGrammar.CRDC.reflexiveLicensedInSentence (ws : List Word) : Bool

Check if reflexive is licensed in a sentence

Equations

• DepGrammar.CRDC.reflexiveLicensedInSentence ws = match DepGrammar.CRDC.parseValencyClause ws with | none => false | some clause => DepGrammar.CRDC.reflexiveLicensed clause

def DepGrammar.CRDC.pronounCoreferenceBlocked (ws : List Word) : Bool

Check if pronoun coreference is blocked

Equations

• DepGrammar.CRDC.pronounCoreferenceBlocked ws = match DepGrammar.CRDC.parseValencyClause ws with | none => false | some val => true

def DepGrammar.CRDC.computeCoreferenceStatus (clause : ValencyClause) (i j : ℕ) : Interfaces.CoreferenceStatus

Compute coreference status using CRDC

Equations

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