HPSG binding theory in RSRL

This file states Principles A and B of HPSG binding theory as RSRL descriptions and checks them on small models of a transitive clause. One argument locally o-commands another when both are on the same argument structure and the first is less oblique. It locally o-binds the other when, in addition, the two share their index and agree in gender and number. Principle A requires a locally o-commanded anaphor to be locally o-bound, and Principle B requires a personal pronoun to be locally o-free. The two principles are the framework-neutral Conditions A and B of Syntax/Binding over local o-command, with the anaphors that nothing locally o-commands exempt.

Main definitions

• HPSG.RSRL.Binding.bindingSig: the signature, with nominal-object sorts, indices, gender and number values, and the relation of local o-command.
• HPSG.RSRL.Binding.principleA: Principle A.
• HPSG.RSRL.Binding.principleB: Principle B.
• HPSG.RSRL.Binding.clause: the model of a transitive clause with a given object.
• HPSG.RSRL.Binding.configuration: local o-command as a framework-neutral binding configuration.

Main results

• HPSG.RSRL.Binding.models_grammar_iff: a clause models the principles exactly when its codependence satisfies the framework-neutral Conditions A and B over local o-command, with the anaphors that nothing locally o-commands exempt.

Implementation notes

Coindexation and agreement are token identity of the IDX, GEND and NUM values, so a coindexed anaphor that clashes with its antecedent in gender or number is not bound. The argument structure of the verb is flattened into the attributes SUBJ and OBJ, and each model interprets local o-command directly.

References

• [PS94]
• [Ric00]
• [Mul24]

The signature

inductive HPSG.RSRL.Binding.Srt : Type

The sorts are signs, the nominal objects with their three species, referential indices, and the gender and number values.

• top : Srt
• sign : Srt
• synsem : Srt
• ana : Srt
• ppro : Srt
• npro : Srt
• idx : Srt
• gender : Srt
• masc : Srt
• fem : Srt
• number : Srt
• sing : Srt
• plur : Srt

@[instance_reducible]

instance HPSG.RSRL.Binding.instDecidableEqSrt : DecidableEq Srt

Equations

• HPSG.RSRL.Binding.instDecidableEqSrt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HPSG.RSRL.Binding.instFintypeSrt : Fintype Srt

Equations

• HPSG.RSRL.Binding.instFintypeSrt = { elems := { val := ↑HPSG.RSRL.Binding.Srt.enumList, nodup := HPSG.RSRL.Binding.Srt.enumList_nodup }, complete := HPSG.RSRL.Binding.instFintypeSrt._proof_1 }

@[instance_reducible]

instance HPSG.RSRL.Binding.instReprSrt : Repr Srt

Equations

• HPSG.RSRL.Binding.instReprSrt = { reprPrec := HPSG.RSRL.Binding.instReprSrt.repr }

def HPSG.RSRL.Binding.instReprSrt.repr : Srt → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• HPSG.RSRL.Binding.instReprSrt.repr HPSG.RSRL.Binding.Srt.top prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.RSRL.Binding.Srt.top")).group prec✝
• HPSG.RSRL.Binding.instReprSrt.repr HPSG.RSRL.Binding.Srt.ana prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.RSRL.Binding.Srt.ana")).group prec✝
• HPSG.RSRL.Binding.instReprSrt.repr HPSG.RSRL.Binding.Srt.idx prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.RSRL.Binding.Srt.idx")).group prec✝
• HPSG.RSRL.Binding.instReprSrt.repr HPSG.RSRL.Binding.Srt.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.RSRL.Binding.Srt.fem")).group prec✝

inductive HPSG.RSRL.Binding.Attr : Type

The attributes are the two arguments of a sign and the index, gender and number of a nominal object.

• SUBJ : Attr
• OBJ : Attr
• IDX : Attr
• GEND : Attr
• NUM : Attr

@[instance_reducible]

instance HPSG.RSRL.Binding.instDecidableEqAttr : DecidableEq Attr

Equations

• HPSG.RSRL.Binding.instDecidableEqAttr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HPSG.RSRL.Binding.instFintypeAttr : Fintype Attr

Equations

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

def HPSG.RSRL.Binding.instReprAttr.repr : Attr → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HPSG.RSRL.Binding.instReprAttr : Repr Attr

Equations

• HPSG.RSRL.Binding.instReprAttr = { reprPrec := HPSG.RSRL.Binding.instReprAttr.repr }

inductive HPSG.RSRL.Binding.Rel : Type

The one relation symbol is local o-command.

• locO : Rel

@[instance_reducible]

instance HPSG.RSRL.Binding.instDecidableEqRel : DecidableEq Rel

Equations

• HPSG.RSRL.Binding.instDecidableEqRel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HPSG.RSRL.Binding.instFintypeRel : Fintype Rel

Equations

• HPSG.RSRL.Binding.instFintypeRel = { elems := { val := ↑HPSG.RSRL.Binding.Rel.enumList, nodup := HPSG.RSRL.Binding.Rel.enumList_nodup }, complete := HPSG.RSRL.Binding.instFintypeRel._proof_1 }

@[instance_reducible]

instance HPSG.RSRL.Binding.instReprRel : Repr Rel

Equations

• HPSG.RSRL.Binding.instReprRel = { reprPrec := HPSG.RSRL.Binding.instReprRel.repr }

def HPSG.RSRL.Binding.instReprRel.repr : Rel → ℕ → Std.Format

Equations

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

def HPSG.RSRL.Binding.Srt.parent : Srt → Option Srt

The immediate supersort of each sort other than top.

Equations

• HPSG.RSRL.Binding.Srt.top.parent = none
• HPSG.RSRL.Binding.Srt.sign.parent = some HPSG.RSRL.Binding.Srt.top
• HPSG.RSRL.Binding.Srt.synsem.parent = some HPSG.RSRL.Binding.Srt.top
• HPSG.RSRL.Binding.Srt.idx.parent = some HPSG.RSRL.Binding.Srt.top
• HPSG.RSRL.Binding.Srt.gender.parent = some HPSG.RSRL.Binding.Srt.top
• HPSG.RSRL.Binding.Srt.number.parent = some HPSG.RSRL.Binding.Srt.top
• HPSG.RSRL.Binding.Srt.ana.parent = some HPSG.RSRL.Binding.Srt.synsem
• HPSG.RSRL.Binding.Srt.ppro.parent = some HPSG.RSRL.Binding.Srt.synsem
• HPSG.RSRL.Binding.Srt.npro.parent = some HPSG.RSRL.Binding.Srt.synsem
• HPSG.RSRL.Binding.Srt.masc.parent = some HPSG.RSRL.Binding.Srt.gender
• HPSG.RSRL.Binding.Srt.fem.parent = some HPSG.RSRL.Binding.Srt.gender
• HPSG.RSRL.Binding.Srt.sing.parent = some HPSG.RSRL.Binding.Srt.number
• HPSG.RSRL.Binding.Srt.plur.parent = some HPSG.RSRL.Binding.Srt.number

def HPSG.RSRL.Binding.Srt.rank : Srt → ℕ

The depth of a sort below top.

Equations

• HPSG.RSRL.Binding.Srt.top.rank = 0
• HPSG.RSRL.Binding.Srt.sign.rank = 1
• HPSG.RSRL.Binding.Srt.synsem.rank = 1
• HPSG.RSRL.Binding.Srt.idx.rank = 1
• HPSG.RSRL.Binding.Srt.gender.rank = 1
• HPSG.RSRL.Binding.Srt.number.rank = 1
• HPSG.RSRL.Binding.Srt.ana.rank = 2
• HPSG.RSRL.Binding.Srt.ppro.rank = 2
• HPSG.RSRL.Binding.Srt.npro.rank = 2
• HPSG.RSRL.Binding.Srt.masc.rank = 2
• HPSG.RSRL.Binding.Srt.fem.rank = 2
• HPSG.RSRL.Binding.Srt.sing.rank = 2
• HPSG.RSRL.Binding.Srt.plur.rank = 2

@[instance_reducible]

instance HPSG.RSRL.Binding.instPartialOrderSrt : PartialOrder Srt

Equations

• HPSG.RSRL.Binding.instPartialOrderSrt = partialOrderOfCovers (fun (σ τ : HPSG.RSRL.Binding.Srt) => σ.parent = some τ) HPSG.RSRL.Binding.Srt.rank HPSG.RSRL.Binding.instPartialOrderSrt._proof_1

@[instance_reducible]

instance HPSG.RSRL.Binding.instDecidableLESrt : DecidableLE Srt

Equations

• HPSG.RSRL.Binding.instDecidableLESrt = decidableLEOfRank (fun (x : HPSG.RSRL.Binding.Srt) => x.parent.toList) HPSG.RSRL.Binding.Srt.rank ⋯ HPSG.RSRL.Binding.instDecidableLESrt._proof_2

def HPSG.RSRL.Binding.Attr.decl : Attr → List (Srt × Srt)

A sign introduces the subject and the object, and a nominal object introduces the index, the gender and the number.

Equations

• HPSG.RSRL.Binding.Attr.SUBJ.decl = [(HPSG.RSRL.Binding.Srt.sign, HPSG.RSRL.Binding.Srt.synsem)]
• HPSG.RSRL.Binding.Attr.OBJ.decl = [(HPSG.RSRL.Binding.Srt.sign, HPSG.RSRL.Binding.Srt.synsem)]
• HPSG.RSRL.Binding.Attr.IDX.decl = [(HPSG.RSRL.Binding.Srt.synsem, HPSG.RSRL.Binding.Srt.idx)]
• HPSG.RSRL.Binding.Attr.GEND.decl = [(HPSG.RSRL.Binding.Srt.synsem, HPSG.RSRL.Binding.Srt.gender)]
• HPSG.RSRL.Binding.Attr.NUM.decl = [(HPSG.RSRL.Binding.Srt.synsem, HPSG.RSRL.Binding.Srt.number)]

@[reducible]

def HPSG.RSRL.Binding.sig : Signature Srt

The signature of the binding fragment.

Equations

• HPSG.RSRL.Binding.sig = HPSG.RSRL.Signature.ofDecl HPSG.RSRL.Binding.Attr HPSG.RSRL.Binding.Rel (fun (x : HPSG.RSRL.Binding.Rel) => 2) HPSG.RSRL.Binding.Attr.decl HPSG.RSRL.Binding.sig._proof_1

Principles A and B

def HPSG.RSRL.Binding.coindexed (x y : ℕ) : Desc sig

The entities at the variables x and y are coindexed when they share their index.

Equations

• HPSG.RSRL.Binding.coindexed x y = HPSG.RSRL.Desc.pathEq ((HPSG.RSRL.Term.var x).feat HPSG.RSRL.Binding.Attr.IDX) ((HPSG.RSRL.Term.var y).feat HPSG.RSRL.Binding.Attr.IDX)

def HPSG.RSRL.Binding.agrees (x y : ℕ) : Desc sig

The entities at the variables x and y agree when they share their gender and their number.

Equations

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

def HPSG.RSRL.Binding.locallyOBinds (y x : ℕ) : Desc sig

The entity at y locally o-binds the entity at x when it locally o-commands it, is coindexed with it, and agrees with it.

Equations

• HPSG.RSRL.Binding.locallyOBinds y x = (HPSG.RSRL.Desc.rel HPSG.RSRL.Binding.Rel.locO ![y, x]).and ((HPSG.RSRL.Binding.coindexed x y).and (HPSG.RSRL.Binding.agrees x y))

def HPSG.RSRL.Binding.principleA : Desc sig

Principle A says that a locally o-commanded anaphor is locally o-bound.

Equations

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

def HPSG.RSRL.Binding.principleB : Desc sig

Principle B says that a personal pronoun is locally o-free.

Equations

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

def HPSG.RSRL.Binding.grammar : Grammar sig

The grammar of the binding fragment.

Equations

• HPSG.RSRL.Binding.grammar = [HPSG.RSRL.Binding.principleA, HPSG.RSRL.Binding.principleB]

theorem HPSG.RSRL.Binding.freeVars_grammar (d : Desc sig) : d ∈ grammar → d.freeVars = ∅

The two principles are closed, whereas the binding condition they quantify over has both of its variables free.

Models of a transitive clause

inductive HPSG.RSRL.Binding.Ent : Type

The entities of a transitive clause are the verb's sign, its subject and object, two indices, and the gender and number values.

• s : Ent
• subj : Ent
• obj : Ent
• iSubj : Ent
• iObj : Ent
• gMasc : Ent
• gFem : Ent
• nSing : Ent
• nPlur : Ent

@[instance_reducible]

instance HPSG.RSRL.Binding.instDecidableEqEnt : DecidableEq Ent

Equations

• HPSG.RSRL.Binding.instDecidableEqEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HPSG.RSRL.Binding.instFintypeEnt : Fintype Ent

Equations

• HPSG.RSRL.Binding.instFintypeEnt = { elems := { val := ↑HPSG.RSRL.Binding.Ent.enumList, nodup := HPSG.RSRL.Binding.Ent.enumList_nodup }, complete := HPSG.RSRL.Binding.instFintypeEnt._proof_1 }

def HPSG.RSRL.Binding.instReprEnt.repr : Ent → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• HPSG.RSRL.Binding.instReprEnt.repr HPSG.RSRL.Binding.Ent.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.RSRL.Binding.Ent.s")).group prec✝
• HPSG.RSRL.Binding.instReprEnt.repr HPSG.RSRL.Binding.Ent.obj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.RSRL.Binding.Ent.obj")).group prec✝

@[instance_reducible]

instance HPSG.RSRL.Binding.instReprEnt : Repr Ent

Equations

• HPSG.RSRL.Binding.instReprEnt = { reprPrec := HPSG.RSRL.Binding.instReprEnt.repr }

@[reducible]

def HPSG.RSRL.Binding.clause (objSort : Srt) (objIdx objGend objNum : Ent) : Interpretation sig Ent

The model of a transitive clause whose subject is a masculine singular nonpronoun indexed iSubj that locally o-commands the object. The object has the given sort, index, gender and number.

Equations

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

@[instance_reducible]

instance HPSG.RSRL.Binding.instDecidablePredForallFinAritySrtSigEntRClause (objSort : Srt) (objIdx objGend objNum : Ent) (ρ : sig.Rel) : DecidablePred ((clause objSort objIdx objGend objNum).R ρ)

Equations

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

theorem HPSG.RSRL.Binding.clause_isTotallyWellTyped (σ : Srt) : σ ∈ [Srt.ana, Srt.ppro, Srt.npro] → ∀ i ∈ [Ent.iSubj, Ent.iObj], ∀ γ ∈ [Ent.gMasc, Ent.gFem], ∀ n ∈ [Ent.nSing, Ent.nPlur], (clause σ i γ n).IsSortResolved ∧ (clause σ i γ n).IsTotallyWellTyped

Every clause whose object is a species of nominal object with an index, a gender and a number is sort-resolved and totally well-typed.

The framework-neutral conditions

def HPSG.RSRL.Binding.configuration : Binding.Configuration Ent

Local o-command gives a binding configuration on the entities of a clause, in which the subject commands the object and every domain is the whole clause, local o-command being local already.

Equations

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

@[instance_reducible]

instance HPSG.RSRL.Binding.instDecidableRelEntCommandsConfiguration : DecidableRel configuration.commands

Equations

• HPSG.RSRL.Binding.instDecidableRelEntCommandsConfiguration x✝¹ x✝ = { decide := decide (x✝¹ = HPSG.RSRL.Binding.Ent.subj) && decide (x✝ = HPSG.RSRL.Binding.Ent.obj), reflects_decide := ⋯ }

@[instance_reducible]

instance HPSG.RSRL.Binding.instDecidablePredEntMemSetDomainConfiguration (b : Ent) : DecidablePred fun (x : Ent) => x ∈ configuration.domain b

Equations

• HPSG.RSRL.Binding.instDecidablePredEntMemSetDomainConfiguration b x✝ = { decide := true, reflects_decide := ⋯ }

def HPSG.RSRL.Binding.Codependent (I : Interpretation sig Ent) (x y : Ent) : Prop

Two entities of a model are codependent when they share their index, gender and number, that is, when they are coindexed and agree.

Equations

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

@[instance_reducible]

instance HPSG.RSRL.Binding.instDecidableRelEntCodependent (I : Interpretation sig Ent) : DecidableRel (Codependent I)

Equations

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

def HPSG.RSRL.Binding.Srt.bindingClass : Srt → Option Binding.BindingClass

An anaphor falls under Condition A and a personal pronoun under Condition B. The fragment states no Principle C, so a nonpronoun has no binding class.

Equations

• HPSG.RSRL.Binding.Srt.ana.bindingClass = some Binding.BindingClass.reflexive
• HPSG.RSRL.Binding.Srt.ppro.bindingClass = some Binding.BindingClass.pronoun
• x✝.bindingClass = none

theorem HPSG.RSRL.Binding.models_grammar_iff (σ : Srt) : σ ∈ [Srt.ana, Srt.ppro, Srt.npro] → ∀ i ∈ [Ent.iSubj, Ent.iObj], ∀ γ ∈ [Ent.gMasc, Ent.gFem], ∀ n ∈ [Ent.nSing, Ent.nPlur], (clause σ i γ n).Models grammar ↔ configuration.Satisfies (Codependent (clause σ i γ n)) configuration.exempt fun (x : Ent) => ((clause σ i γ n).S x).bindingClass

A clause models the principles exactly when its codependence satisfies the framework-neutral Conditions A and B over local o-command, with the anaphors that nothing locally o-commands exempt.