Binding theory

A configuration says which positions command which and gives each position a binding domain; an anaphoric dependency says which positions are antecedents of which. A position binds another when it is an antecedent of it, distinct from it, that commands it. An anaphor is bound in its domain (Condition A), a pronominal is not (Condition B), and an R-expression is not bound at all (Condition C), the three conditions of Chomsky's binding theory.

Frameworks differ in what they supply. Chomsky binds coindexed noun phrases under c-command within the governing category, Pollard and Sag under local o-command, and Charnavel within the smallest spell-out domain. The dependency is a relation L, with L a b read as "a is an antecedent of b"; coindexation is one encoding of it, and the logical binding that Reuland reviews is another.

Condition A holds of the anaphors outside an exempt set. Chomsky exempts none and Pollard and Sag exempt an anaphor that nothing in its domain commands (Configuration.exempt). Charnavel argues that exemption is only apparent: the anaphor is bound in its domain by a silent pronoun, and looks exempt when that position is left out of account.

Main definitions

• Binding.BindingClass, Binding.bindingClassOf: anaphor, pronominal or R-expression, read off a word's morphology.
• Binding.Configuration: a command relation and a binding domain, ordered pointwise; Configuration.comap pulls one back along a map of positions, and Configuration.monoclausal is the configuration of a single binding domain.
• Binding.pair: the dependency relating two positions to each other alone.
• Configuration.Binds, Bound, LocallyBound, LocallyCommanded, exempt.
• Configuration.Condition, Configuration.Satisfies: Conditions A, B and C.
• Configuration.covertlyBound: the positions bound in their domain by a position that a restriction of the configuration leaves out.

Main statements

• Configuration.condition_iff_not_condition_pronoun: outside the exempt set an anaphor and a pronominal with one domain are in complementary distribution.
• Configuration.condition_exempt_iff: with the structural exemption, an anaphor meets its condition when, if commanded in its domain, it is bound there.
• Configuration.condition_mono, condition_pronoun_anti, condition_rExpression_anti: more command binds more, so Condition A is monotone in the configuration and B and C antitone.
• Configuration.condition_comap: Condition A with nothing exempt among all positions is Condition A among some of them with those bound by a position left out exempt.

Implementation notes

The conditions restrict binding. Coreference that is not binding falls outside Condition B, as Reuland stresses, and outside this file.

References

• [Cho81]
• [PS94]
• [Reu18]
• [Cha19c]

Binding classes

inductive Binding.BindingClass : Type

A nominal's binding class is an anaphor, reflexive or reciprocal, a pronominal, or an R-expression, which fall under Conditions A, B and C.

• reflexive : BindingClass

  Reflexive anaphor (himself, herself, themselves).

• reciprocal : BindingClass

  Reciprocal anaphor (each other, one another).

• pronoun : BindingClass

  Pronominal (he, she, they, …).

• rExpression : BindingClass

  Referring expression (proper name, full noun phrase).

@[instance_reducible]

instance Binding.instReprBindingClass : Repr BindingClass

Equations

• Binding.instReprBindingClass = { reprPrec := Binding.instReprBindingClass.repr }

def Binding.instReprBindingClass.repr : BindingClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Binding.instDecidableEqBindingClass : DecidableEq BindingClass

Equations

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

@[instance_reducible]

instance Binding.instFintypeBindingClass : Fintype BindingClass

Equations

• Binding.instFintypeBindingClass = { elems := { val := ↑Binding.BindingClass.enumList, nodup := Binding.BindingClass.enumList_nodup }, complete := Binding.instFintypeBindingClass._proof_1 }

def Binding.BindingClass.IsAnaphor (c : BindingClass) : Prop

A class is an anaphor's, subject to Condition A, when it is reflexive or reciprocal.

Equations

• c.IsAnaphor = (c = Binding.BindingClass.reflexive ∨ c = Binding.BindingClass.reciprocal)

def Binding.BindingClass.IsPronominal (c : BindingClass) : Prop

A class is a pronominal's, subject to Condition B.

Equations

• c.IsPronominal = (c = Binding.BindingClass.pronoun)

def Binding.BindingClass.IsRExpression (c : BindingClass) : Prop

A class is a referring expression's, subject to Condition C.

Equations

• c.IsRExpression = (c = Binding.BindingClass.rExpression)

@[instance_reducible]

instance Binding.BindingClass.instDecidableIsAnaphor (c : BindingClass) : Decidable c.IsAnaphor

Equations

• c.instDecidableIsAnaphor = { decide := decide (c = Binding.BindingClass.reflexive) || decide (c = Binding.BindingClass.reciprocal), reflects_decide := ⋯ }

@[instance_reducible]

instance Binding.BindingClass.instDecidableIsPronominal (c : BindingClass) : Decidable c.IsPronominal

Equations

• c.instDecidableIsPronominal = Binding.BindingClass.instDecidableIsPronominal._aux_1 c

@[instance_reducible]

instance Binding.BindingClass.instDecidableIsRExpression (c : BindingClass) : Decidable c.IsRExpression

Equations

• c.instDecidableIsRExpression = Binding.BindingClass.instDecidableIsRExpression._aux_1 c

def Binding.isNominalCat (cat : UD.UPOS) : Bool

A part of speech is nominal when it is a proper noun, a common noun or a pronoun.

Equations

• Binding.isNominalCat cat = (cat == UD.UPOS.PROPN || cat == UD.UPOS.NOUN || cat == UD.UPOS.PRON)

def Binding.bindingClassOf (w : Morphology.Word) : Option BindingClass

bindingClassOf w reads the binding class of w off its morphology and category. Reflexive marking makes a reflexive, the reciprocal pronoun type a reciprocal, any other pronoun a pronominal, and a noun an R-expression.

Equations

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

Configurations

structure Binding.Configuration (ι : Type u_1) : Type u_1

A binding configuration on the positions ι says which positions command which and gives each position its binding domain.

• commands : ι → ι → Prop

  commands a b holds when a commands b.

• domain : ι → Set ι

  domain b is the binding domain of b.

def Binding.pair {ι : Type u_1} (a b x y : ι) : Prop

pair a b is the dependency that relates a and b to each other and nothing else.

Equations

• Binding.pair a b x y = (x = a ∧ y = b ∨ x = b ∧ y = a)

@[instance_reducible]

instance Binding.instDecidableRelPairOfDecidableEq {ι : Type u_1} [DecidableEq ι] (a b : ι) : DecidableRel (pair a b)

Equations

• Binding.instDecidableRelPairOfDecidableEq a b x✝¹ x✝ = { decide := decide (x✝¹ = a ∧ x✝ = b) || decide (x✝¹ = b ∧ x✝ = a), reflects_decide := ⋯ }

theorem Binding.pair_comm {ι : Type u_1} (a b : ι) : pair a b = pair b a

@[instance_reducible]

instance Binding.Configuration.instPartialOrder {ι : Type u_1} : PartialOrder (Configuration ι)

Configurations are ordered pointwise, s ≤ t when t commands whatever s commands and each domain of s lies in the corresponding domain of t.

Equations

• Binding.Configuration.instPartialOrder = PartialOrder.lift (fun (s : Binding.Configuration ι) => (s.commands, s.domain)) ⋯

theorem Binding.Configuration.le_def {ι : Type u_1} {s t : Configuration ι} : s ≤ t ↔ s.commands ≤ t.commands ∧ s.domain ≤ t.domain

def Binding.Configuration.comap {ι : Type u_1} {κ : Type u_2} (f : κ → ι) (s : Configuration ι) : Configuration κ

s.comap f is the configuration that s induces along f, in which one position commands another when their images do and a position's domain is the preimage of its image's.

Equations

• Binding.Configuration.comap f s = { commands := fun (a b : κ) => s.commands (f a) (f b), domain := fun (b : κ) => f ⁻¹' s.domain (f b) }

theorem Binding.Configuration.comap_mono {ι : Type u_1} {κ : Type u_2} (f : κ → ι) : Monotone (comap f)

@[instance_reducible]

instance Binding.Configuration.instDecidableRelCommandsComap {ι : Type u_1} {κ : Type u_2} (f : κ → ι) (s : Configuration ι) [DecidableRel s.commands] : DecidableRel (comap f s).commands

Equations

• Binding.Configuration.instDecidableRelCommandsComap f s x✝¹ x✝ = Binding.Configuration.instDecidableRelCommandsComap._aux_1 f s x✝¹ x✝

@[instance_reducible]

instance Binding.Configuration.instDecidablePredMemSetDomainComap {ι : Type u_1} {κ : Type u_2} (f : κ → ι) (s : Configuration ι) [(b : ι) → DecidablePred fun (x : ι) => x ∈ s.domain b] (b : κ) : DecidablePred fun (x : κ) => x ∈ (comap f s).domain b

Equations

• Binding.Configuration.instDecidablePredMemSetDomainComap f s b x✝ = Binding.Configuration.instDecidablePredMemSetDomainComap._aux_1 f s b x✝

def Binding.Configuration.monoclausal {ι : Type u_1} {α : Type u_2} (pos : ι → Option α) (R : α → α → Prop) : Configuration ι

monoclausal pos R is the configuration of a single binding domain. The map pos reads a position as an object, one position commands another when its object R-commands the other's, and every position lies in every domain.

Equations

• Binding.Configuration.monoclausal pos R = { commands := fun (a b : ι) => ∃ x ∈ pos a, ∃ y ∈ pos b, R x y, domain := fun (x : ι) => Set.univ }

theorem Binding.Configuration.monoclausal_mono {ι : Type u_1} {α : Type u_2} {pos : ι → Option α} {R R' : α → α → Prop} (h : R ≤ R') : monoclausal pos R ≤ monoclausal pos R'

@[instance_reducible]

instance Binding.Configuration.instDecidableRelCommandsMonoclausal {ι : Type u_1} {α : Type u_2} (pos : ι → Option α) (R : α → α → Prop) [DecidableRel R] : DecidableRel (monoclausal pos R).commands

Equations

• Binding.Configuration.instDecidableRelCommandsMonoclausal pos R x✝¹ x✝ = Binding.Configuration.instDecidableRelCommandsMonoclausal._aux_1 pos R x✝¹ x✝

@[instance_reducible]

instance Binding.Configuration.instDecidablePredMemSetDomainMonoclausal {ι : Type u_1} {α : Type u_2} (pos : ι → Option α) (R : α → α → Prop) (b : ι) : DecidablePred fun (x : ι) => x ∈ (monoclausal pos R).domain b

Equations

• Binding.Configuration.instDecidablePredMemSetDomainMonoclausal pos R b x✝ = { decide := true, reflects_decide := ⋯ }

def Binding.Configuration.Binds {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) (a b : ι) : Prop

a binds b along the dependency L when a is an antecedent of b other than b itself and commands b.

Equations

• s.Binds L a b = (a ≠ b ∧ L a b ∧ s.commands a b)

def Binding.Configuration.Bound {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) (b : ι) : Prop

b is bound when some position binds it.

Equations

• s.Bound L b = ∃ (a : ι), s.Binds L a b

def Binding.Configuration.LocallyBound {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) (b : ι) : Prop

b is locally bound when some position in its domain binds it.

Equations

• s.LocallyBound L b = ∃ a ∈ s.domain b, s.Binds L a b

def Binding.Configuration.LocallyCommanded {ι : Type u_1} (s : Configuration ι) (b : ι) : Prop

b is locally commanded when some position other than b in its domain commands it.

Equations

• s.LocallyCommanded b = ∃ a ∈ s.domain b, a ≠ b ∧ s.commands a b

def Binding.Configuration.exempt {ι : Type u_1} (s : Configuration ι) : Set ι

exempt is the set of positions that nothing in their domain commands.

Equations

• s.exempt = {b : ι | ¬s.LocallyCommanded b}

def Binding.Configuration.Condition {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) (E : Set ι) (b : ι) : BindingClass → Prop

Condition E b c is the condition a nominal of class c at b must meet when the positions in E are exempt from Condition A. An anaphor is bound in its domain unless exempt, a pronominal is not bound in its domain, and an R-expression is not bound.

Equations

• s.Condition L E b Binding.BindingClass.reflexive = (b ∈ E ∨ s.LocallyBound L b)
• s.Condition L E b Binding.BindingClass.reciprocal = (b ∈ E ∨ s.LocallyBound L b)
• s.Condition L E b Binding.BindingClass.pronoun = ¬s.LocallyBound L b
• s.Condition L E b Binding.BindingClass.rExpression = ¬s.Bound L b

def Binding.Configuration.Satisfies {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) (E : Set ι) (cls : ι → Option BindingClass) : Prop

The dependency L satisfies the binding theory, with the positions in E exempt from Condition A, when every position the classifier cls classifies meets its class's condition.

Equations

• s.Satisfies L E cls = ∀ (b : ι) (c : Binding.BindingClass), cls b = some c → s.Condition L E b c

theorem Binding.Configuration.Binds.commands {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {a b : ι} (h : s.Binds L a b) : s.commands a b

theorem Binding.Configuration.Binds.mono {ι : Type u_1} {s : Configuration ι} {L L' : ι → ι → Prop} {a b : ι} (hL : L ≤ L') (h : s.Binds L a b) : s.Binds L' a b

theorem Binding.Configuration.Bound.mono {ι : Type u_1} {s : Configuration ι} {L L' : ι → ι → Prop} {b : ι} (hL : L ≤ L') (h : s.Bound L b) : s.Bound L' b

theorem Binding.Configuration.LocallyBound.mono {ι : Type u_1} {s : Configuration ι} {L L' : ι → ι → Prop} {b : ι} (hL : L ≤ L') (h : s.LocallyBound L b) : s.LocallyBound L' b

theorem Binding.Configuration.Binds.of_le {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {t : Configuration ι} {a b : ι} (hst : s ≤ t) (h : s.Binds L a b) : t.Binds L a b

theorem Binding.Configuration.Bound.of_le {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {t : Configuration ι} {b : ι} (hst : s ≤ t) (h : s.Bound L b) : t.Bound L b

theorem Binding.Configuration.LocallyBound.of_le {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {t : Configuration ι} {b : ι} (hst : s ≤ t) (h : s.LocallyBound L b) : t.LocallyBound L b

theorem Binding.Configuration.LocallyBound.bound {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {b : ι} (h : s.LocallyBound L b) : s.Bound L b

theorem Binding.Configuration.LocallyBound.locallyCommanded {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {b : ι} (h : s.LocallyBound L b) : s.LocallyCommanded b

theorem Binding.Configuration.not_locallyBound_of_mem_exempt {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {b : ι} (hb : b ∈ s.exempt) : ¬s.LocallyBound L b

theorem Binding.Configuration.bound_iff_binds {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {a b : ι} (h : ∀ (x : ι), L x b → x = a ∨ x = b) : s.Bound L b ↔ s.Binds L a b

A position whose only antecedents are a and itself is bound exactly when a binds it.

theorem Binding.Configuration.binds_pair_iff {ι : Type u_1} {s : Configuration ι} {a b x : ι} (hab : a ≠ b) : s.Binds (pair a b) x b ↔ x = a ∧ s.commands a b

theorem Binding.Configuration.bound_pair_iff {ι : Type u_1} {s : Configuration ι} {a b : ι} (hab : a ≠ b) : s.Bound (pair a b) b ↔ s.commands a b

Under the dependency relating a and b alone, b is bound exactly when a commands it.

theorem Binding.Configuration.locallyBound_pair_iff {ι : Type u_1} {s : Configuration ι} {a b : ι} (hab : a ≠ b) : s.LocallyBound (pair a b) b ↔ a ∈ s.domain b ∧ s.commands a b

Under the dependency relating a and b alone, b is locally bound exactly when a lies in its domain and commands it.

theorem Binding.Configuration.condition_anaphor {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {E : Set ι} {b : ι} {c : BindingClass} (hc : c.IsAnaphor) : s.Condition L E b c ↔ b ∈ E ∨ s.LocallyBound L b

theorem Binding.Configuration.condition_iff_not_condition_pronoun {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {E : Set ι} {b : ι} {c : BindingClass} (hc : c.IsAnaphor) (hb : b ∉ E) : s.Condition L E b c ↔ ¬s.Condition L E b BindingClass.pronoun

Outside the exempt positions an anaphor meets its condition exactly where a pronominal fails its own.

theorem Binding.Configuration.condition_of_mem {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {E : Set ι} {b : ι} {c : BindingClass} (hc : c.IsAnaphor) (hb : b ∈ E) : s.Condition L E b c

At an exempt position an anaphor meets its condition under any dependency.

theorem Binding.Configuration.condition_exempt_iff {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {b : ι} {c : BindingClass} (hc : c.IsAnaphor) : s.Condition L s.exempt b c ↔ s.LocallyCommanded b → s.LocallyBound L b

With the structural exemption, an anaphor meets its condition exactly when it is bound in its domain if anything there commands it.

theorem Binding.Configuration.condition_empty_iff {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {b : ι} {c : BindingClass} (hc : c.IsAnaphor) : s.Condition L ∅ b c ↔ s.Condition L s.exempt b c ∧ s.LocallyCommanded b

Without exemption an anaphor meets its condition exactly when it meets it under the structural exemption and something in its domain commands it.

theorem Binding.Configuration.condition_pronoun_of_rExpression {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {E : Set ι} {b : ι} (h : s.Condition L E b BindingClass.rExpression) : s.Condition L E b BindingClass.pronoun

A position that meets Condition C meets Condition B, since a position that is not bound is not bound in its domain.

theorem Binding.Configuration.Satisfies.mono_exempt {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {E E' : Set ι} {cls : ι → Option BindingClass} (hE : E ⊆ E') (h : s.Satisfies L E cls) : s.Satisfies L E' cls

Exempting more positions weakens the theory.

theorem Binding.Configuration.condition_mono {ι : Type u_1} {L : ι → ι → Prop} {E : Set ι} {b : ι} {c : BindingClass} (hc : c.IsAnaphor) : Monotone fun (s : Configuration ι) => s.Condition L E b c

An anaphor's condition is monotone in the configuration, since more command and larger domains bind more.

theorem Binding.Configuration.condition_pronoun_anti {ι : Type u_1} {L : ι → ι → Prop} {E : Set ι} {b : ι} : Antitone fun (s : Configuration ι) => s.Condition L E b BindingClass.pronoun

A pronominal's condition is antitone in the configuration.

theorem Binding.Configuration.condition_rExpression_anti {ι : Type u_1} {L : ι → ι → Prop} {E : Set ι} {b : ι} : Antitone fun (s : Configuration ι) => s.Condition L E b BindingClass.rExpression

An R-expression's condition is antitone in the configuration.

Positions left out of account

A configuration restricts along an injection f to the positions f reaches. A position bound in its domain by one that f does not reach is bound in the whole configuration and may be free in the restriction.

def Binding.Configuration.covertlyBound {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) {κ : Type u_2} (f : κ → ι) : Set κ

s.covertlyBound L f is the set of positions whose images are bound in their domains by a position outside the range of f.

Equations

• s.covertlyBound L f = {b : κ | ∃ x ∈ s.domain (f b), x ∉ Set.range f ∧ s.Binds L x (f b)}

theorem Binding.Configuration.binds_comap {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {κ : Type u_2} {f : κ → ι} {a b : κ} (hf : Function.Injective f) : (comap f s).Binds (Function.onFun L f) a b ↔ s.Binds L (f a) (f b)

theorem Binding.Configuration.locallyBound_comap_or {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {κ : Type u_2} {f : κ → ι} {b : κ} (hf : Function.Injective f) : (comap f s).LocallyBound (Function.onFun L f) b ∨ b ∈ s.covertlyBound L f ↔ s.LocallyBound L (f b)

A position is bound in its domain when a position f reaches binds it there or one that f does not reach does.

theorem Binding.Configuration.bound_comap_or {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {κ : Type u_2} {f : κ → ι} {b : κ} (hf : Function.Injective f) : ((comap f s).Bound (Function.onFun L f) b ∨ ∃ x ∉ Set.range f, s.Binds L x (f b)) ↔ s.Bound L (f b)

theorem Binding.Configuration.condition_comap {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {E : Set ι} {c : BindingClass} {κ : Type u_2} {f : κ → ι} {b : κ} (hf : Function.Injective f) (hc : c.IsAnaphor) : (comap f s).Condition (Function.onFun L f) (f ⁻¹' E ∪ s.covertlyBound L f) b c ↔ s.Condition L E (f b) c

An anaphor meets Condition A among all positions exactly when it meets it among those f reaches with the covertly bound positions exempt.

theorem Binding.Configuration.mem_covertlyBound_of_condition {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {c : BindingClass} {κ : Type u_2} {f : κ → ι} {b : κ} (hf : Function.Injective f) (hc : c.IsAnaphor) (h : s.Condition L ∅ (f b) c) (hb : ¬(comap f s).LocallyBound (Function.onFun L f) b) : b ∈ s.covertlyBound L f

An anaphor that meets Condition A among all positions with nothing exempt, and that no position f reaches binds in its domain, is covertly bound.

theorem Binding.Configuration.condition_pronoun_comap {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {E : Set ι} {κ : Type u_2} {f : κ → ι} {b : κ} (hf : Function.Injective f) {F : Set κ} : (comap f s).Condition (Function.onFun L f) F b BindingClass.pronoun ∧ b ∉ s.covertlyBound L f ↔ s.Condition L E (f b) BindingClass.pronoun

A pronominal meets Condition B among all positions exactly when it meets it among those f reaches and no position left out binds it in its domain.

theorem Binding.Configuration.condition_rExpression_comap {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {E : Set ι} {κ : Type u_2} {f : κ → ι} {b : κ} (hf : Function.Injective f) {F : Set κ} : ((comap f s).Condition (Function.onFun L f) F b BindingClass.rExpression ∧ ¬∃ x ∉ Set.range f, s.Binds L x (f b)) ↔ s.Condition L E (f b) BindingClass.rExpression

An R-expression meets Condition C among all positions exactly when it meets it among those f reaches and no position left out binds it.

theorem Binding.Configuration.rel_of_mem_covertlyBound {ι : Type u_1} {s : Configuration ι} {L : ι → ι → Prop} {κ : Type u_2} {f : κ → ι} {a b : κ} (hs : ∀ ⦃x y : ι⦄, L x y → L y x) (ht : ∀ ⦃x y z : ι⦄, L x y → L y z → L x z) (h : ∀ x ∈ s.domain (f a), ∀ y ∈ s.domain (f b), x ∉ Set.range f → y ∉ Set.range f → x = y) (ha : a ∈ s.covertlyBound L f) (hb : b ∈ s.covertlyBound L f) : L (f a) (f b)

Two covertly bound positions whose domains hold at most one position left out between them have the same binder, so a symmetric and transitive dependency, as coindexation is, relates them.

@[instance_reducible]

instance Binding.Configuration.instDecidableBinds {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) [DecidableEq ι] [DecidableRel L] [DecidableRel s.commands] (a b : ι) : Decidable (s.Binds L a b)

Equations

• s.instDecidableBinds L a b = { decide := decide (a ≠ b) && decide (L a b ∧ s.commands a b), reflects_decide := ⋯ }

@[instance_reducible]

instance Binding.Configuration.instDecidableBound {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) [Fintype ι] [DecidableEq ι] [DecidableRel L] [DecidableRel s.commands] (b : ι) : Decidable (s.Bound L b)

Equations

• s.instDecidableBound L b = { decide := decide (∃ a ∈ Finset.univ, (fun (x : ι) => s.Binds L x b) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Binding.Configuration.instDecidableLocallyBound {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) [Fintype ι] [DecidableEq ι] [DecidableRel L] [DecidableRel s.commands] [(b : ι) → DecidablePred fun (x : ι) => x ∈ s.domain b] (b : ι) : Decidable (s.LocallyBound L b)

Equations

• s.instDecidableLocallyBound L b = { decide := decide (∃ a ∈ Finset.univ, (fun (x : ι) => x ∈ s.domain b ∧ s.Binds L x b) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Binding.Configuration.instDecidableLocallyCommanded {ι : Type u_1} (s : Configuration ι) [Fintype ι] [DecidableEq ι] [DecidableRel s.commands] [(b : ι) → DecidablePred fun (x : ι) => x ∈ s.domain b] (b : ι) : Decidable (s.LocallyCommanded b)

Equations

• s.instDecidableLocallyCommanded b = { decide := decide (∃ a ∈ Finset.univ, (fun (x : ι) => x ∈ s.domain b ∧ x ≠ b ∧ s.commands x b) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Binding.Configuration.instDecidableMemSetCovertlyBoundOfFintype {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) [Fintype ι] [DecidableEq ι] [DecidableRel L] [DecidableRel s.commands] [(b : ι) → DecidablePred fun (x : ι) => x ∈ s.domain b] {κ : Type u_2} [Fintype κ] (f : κ → ι) (b : κ) : Decidable (b ∈ s.covertlyBound L f)

Equations

• s.instDecidableMemSetCovertlyBoundOfFintype L f b = { decide := decide (∃ a ∈ Finset.univ, (fun (x : ι) => x ∈ s.domain (f b) ∧ x ∉ Set.range f ∧ s.Binds L x (f b)) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Binding.Configuration.instDecidablePredMemSetExempt {ι : Type u_1} (s : Configuration ι) [Fintype ι] [DecidableEq ι] [DecidableRel s.commands] [(b : ι) → DecidablePred fun (x : ι) => x ∈ s.domain b] : DecidablePred fun (x : ι) => x ∈ s.exempt

Equations

• s.instDecidablePredMemSetExempt x✝ = { decide := !decide (s.LocallyCommanded x✝), reflects_decide := ⋯ }

@[instance_reducible]

instance Binding.Configuration.instDecidableConditionOfDecidablePredMemSet {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) [Fintype ι] [DecidableEq ι] [DecidableRel L] [DecidableRel s.commands] [(b : ι) → DecidablePred fun (x : ι) => x ∈ s.domain b] (E : Set ι) [DecidablePred fun (x : ι) => x ∈ E] (b : ι) (c : BindingClass) : Decidable (s.Condition L E b c)

Equations

• s.instDecidableConditionOfDecidablePredMemSet L E b Binding.BindingClass.reflexive = { decide := decide (b ∈ E) || decide (s.LocallyBound L b), reflects_decide := ⋯ }
• s.instDecidableConditionOfDecidablePredMemSet L E b Binding.BindingClass.reciprocal = { decide := decide (b ∈ E) || decide (s.LocallyBound L b), reflects_decide := ⋯ }
• s.instDecidableConditionOfDecidablePredMemSet L E b Binding.BindingClass.pronoun = { decide := !decide (s.LocallyBound L b), reflects_decide := ⋯ }
• s.instDecidableConditionOfDecidablePredMemSet L E b Binding.BindingClass.rExpression = { decide := !decide (s.Bound L b), reflects_decide := ⋯ }

@[instance_reducible]

instance Binding.Configuration.instDecidableSatisfiesOfDecidablePredMemSet {ι : Type u_1} (s : Configuration ι) (L : ι → ι → Prop) [Fintype ι] [DecidableEq ι] [DecidableRel L] [DecidableRel s.commands] [(b : ι) → DecidablePred fun (x : ι) => x ∈ s.domain b] (E : Set ι) [DecidablePred fun (x : ι) => x ∈ E] (cls : ι → Option BindingClass) : Decidable (s.Satisfies L E cls)

Equations

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