Bakay, Akkuş and Dillon (2026): hierarchical relations in antecedent retrieval

This file formalizes the structural claims behind three visual-world experiments on the Turkish reciprocal birbirleri, which must be bound by a c-commanding antecedent in its own clause. Bakay, Akkuş and Dillon ask whether c-command between the noun phrases of one clause guides antecedent retrieval, and they deconfound it from clause-mateness, case, subjecthood and linear order. The target, an embedded subject or an indirect object, and the distractor, a possessor inside the subject or inside an adjunct noun phrase or the complement of a postposition, share the reciprocal's clause and case. The four embedded structures are phrase-structure trees here, and Principle A over their clause configuration makes the embedded subject and an indirect object available and the matrix subject and every distractor unavailable (available_iff), as the paper's coindexations record (rows_available).

The paper weighs two ways retrieval could use the relation. On the cue-based account of Lewis and Vasishth the reciprocal cues features stored with each candidate, and c-command enters through Kush's local feature, carried by the noun phrases attached to the spine of the current clause or serving as its arguments. On every stimulus that feature holds of exactly the available antecedents (local_iff_available), so the target out-activates each distractor under any weighting that gives the hierarchical cue weight (target_retrieved); a distractor that matches the reciprocal in number still out-activates one that does not whenever item-level cues carry weight, the interference both weightings predict (distractor_interference). On the representational account after McElree and Oberauer, the noun phrases that c-command the retrieval site from within its clause sit in a privileged store. That store holds exactly the available antecedents (privileged_iff_available), so no distractor is accessed (not_privileged_second).

Implementation notes

• The trees keep the noun phrases, the heads that embed them and the verbal spine, and omit adverbs. The embedded clause is the complement of the matrix verb, and an adjunct is a sister of the lowest verb phrase.
• Argumenthood in Kush's feature is read off attachment, so a noun phrase is local when its mother is a clause or verb-phrase node of the retrieval site's clause.
• A cue is matched either against the hierarchical feature or against an item-level feature, and activation is the count of matched cues weighted by where they are matched.

References

• Ö. Bakay, F. Akkuş and B. Dillon, Hierarchical relations guide memory retrieval in sentence comprehension: Evidence from a local anaphor in Turkish (2026)
• N. Chomsky, Lectures on Government and Binding (1981)
• T. Reinhart, The Syntactic Domain of Anaphora (1976)
• R. L. Lewis and S. Vasishth, An Activation-Based Model of Sentence Processing as Skilled Memory Retrieval (2005)
• D. W. Kush, Respecting Relations: Memory Access and Antecedent Retrieval in Incremental Sentence Processing (2013)
• B. McElree, Accessing Recent Events (2006)
• K. Oberauer, Access to information in working memory: Exploring the focus of attention (2002)

The stimuli

inductive BakayEtAl2026.Structure : Type

The embedded-clause structures of the stimuli, by the clause's second noun phrase. It is a possessor inside the subject in (5a), a possessor inside an adjunct noun phrase in (5b) and (10c), the complement of a postposition in (8b) and (10b), and an indirect object in (8a), (8c) and (10a).

• possessorInSubject : Structure
• possessorInAdjunct : Structure
• postpositionalAdjunct : Structure
• indirectObject : Structure

@[instance_reducible]

instance BakayEtAl2026.instDecidableEqStructure : DecidableEq Structure

Equations

• BakayEtAl2026.instDecidableEqStructure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BakayEtAl2026.instFintypeStructure : Fintype Structure

Equations

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

@[instance_reducible]

instance BakayEtAl2026.instReprStructure : Repr Structure

Equations

• BakayEtAl2026.instReprStructure = { reprPrec := BakayEtAl2026.instReprStructure.repr }

def BakayEtAl2026.instReprStructure.repr : Structure → ℕ → Std.Format

Equations

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

def BakayEtAl2026.np : PhraseStructure.Tree PhraseStructure.Cat Unit

np is a one-word noun phrase.

Equations

• BakayEtAl2026.np = PhraseStructure.Tree.terminal PhraseStructure.Cat.N ()

def BakayEtAl2026.possessive : PhraseStructure.Tree PhraseStructure.Cat Unit

possessive is a noun phrase of a possessor and its head noun.

Equations

• BakayEtAl2026.possessive = PhraseStructure.Tree.node PhraseStructure.Cat.N [BakayEtAl2026.np, PhraseStructure.Tree.terminal PhraseStructure.Cat.N ()]

def BakayEtAl2026.reciprocalVP : PhraseStructure.Tree PhraseStructure.Cat Unit

reciprocalVP is the lowest verb phrase, of the reciprocal object and the embedded verb.

Equations

• BakayEtAl2026.reciprocalVP = PhraseStructure.Tree.node PhraseStructure.Cat.V [BakayEtAl2026.np, PhraseStructure.Tree.terminal PhraseStructure.Cat.V ()]

def BakayEtAl2026.Structure.clause : Structure → PhraseStructure.Tree PhraseStructure.Cat Unit

The embedded clause of a structure.

Equations

• One or more equations did not get rendered due to their size.
• BakayEtAl2026.Structure.possessorInSubject.clause = PhraseStructure.Tree.node PhraseStructure.Cat.S [BakayEtAl2026.possessive, BakayEtAl2026.reciprocalVP]

def BakayEtAl2026.Structure.tree (s : Structure) : PhraseStructure.Tree PhraseStructure.Cat Unit

A stimulus is the matrix subject over the embedded clause and the matrix verb.

Equations

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

inductive BakayEtAl2026.Role : Type

The noun phrases of a stimulus are the matrix subject, the embedded subject, the embedded clause's second noun phrase, a distractor or an indirect object, and the reciprocal.

• matrixSubject : Role
• embeddedSubject : Role
• second : Role
• reciprocal : Role

@[instance_reducible]

instance BakayEtAl2026.instDecidableEqRole : DecidableEq Role

Equations

• BakayEtAl2026.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BakayEtAl2026.instFintypeRole : Fintype Role

Equations

• BakayEtAl2026.instFintypeRole = { elems := { val := ↑BakayEtAl2026.Role.enumList, nodup := BakayEtAl2026.Role.enumList_nodup }, complete := BakayEtAl2026.instFintypeRole._proof_1 }

def BakayEtAl2026.instReprRole.repr : Role → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• BakayEtAl2026.instReprRole.repr BakayEtAl2026.Role.second prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BakayEtAl2026.Role.second")).group prec✝

@[instance_reducible]

instance BakayEtAl2026.instReprRole : Repr Role

Equations

• BakayEtAl2026.instReprRole = { reprPrec := BakayEtAl2026.instReprRole.repr }

def BakayEtAl2026.Structure.path : Structure → Role → Core.Order.TreePath

The position of a noun phrase in a stimulus.

Equations

• x✝.path BakayEtAl2026.Role.matrixSubject = { toList := [0] }
• x✝.path BakayEtAl2026.Role.embeddedSubject = { toList := [1, 0, 0] }
• BakayEtAl2026.Structure.possessorInSubject.path BakayEtAl2026.Role.second = { toList := [1, 0, 0, 0] }
• BakayEtAl2026.Structure.possessorInSubject.path BakayEtAl2026.Role.reciprocal = { toList := [1, 0, 1, 0] }
• BakayEtAl2026.Structure.indirectObject.path BakayEtAl2026.Role.second = { toList := [1, 0, 1, 0] }
• x✝.path BakayEtAl2026.Role.second = { toList := [1, 0, 1, 0, 0] }
• x✝.path BakayEtAl2026.Role.reciprocal = { toList := [1, 0, 1, 1, 0] }

theorem BakayEtAl2026.path_mem_labeled (s : Structure) (r : Role) : s.path r ∈ s.tree.labeled {PhraseStructure.Cat.N}

Every noun phrase of a stimulus sits at a noun phrase of its tree.

theorem BakayEtAl2026.path_injective (s : Structure) : Function.Injective s.path

Distinct noun phrases of a stimulus sit at distinct positions.

@[reducible, inline]

abbrev BakayEtAl2026.Structure.configuration (s : Structure) : Binding.Configuration Role

The binding configuration on the noun phrases of a stimulus is its tree's clause configuration read at their positions.

Equations

• s.configuration = Binding.Configuration.comap s.path s.tree.clauseConfiguration

def BakayEtAl2026.Role.Available (s : Structure) (r : Role) : Prop

A noun phrase is an available antecedent when the reciprocal, coindexed with it alone, meets Principle A.

Equations

• BakayEtAl2026.Role.Available s r = s.configuration.Condition (Binding.pair r BakayEtAl2026.Role.reciprocal) ∅ BakayEtAl2026.Role.reciprocal Binding.BindingClass.reciprocal

@[instance_reducible]

instance BakayEtAl2026.instDecidableAvailable (s : Structure) (r : Role) : Decidable (Role.Available s r)

Equations

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

theorem BakayEtAl2026.available_iff (s : Structure) (r : Role) : Role.Available s r ↔ r = Role.embeddedSubject ∨ s = Structure.indirectObject ∧ r = Role.second

The embedded subject is available in every structure, and the second noun phrase exactly when it is an indirect object. The matrix subject lies outside the reciprocal's clause, and a distractor does not c-command the reciprocal.

Cue-based retrieval

def BakayEtAl2026.Local (t : PhraseStructure.Tree PhraseStructure.Cat Unit) (p q : Core.Order.TreePath) : Prop

The noun phrase at p carries Kush's local feature at a retrieval site q when its mother is a clause or verb-phrase node sharing the minimal clause of q, so that it hangs from the spine of that clause.

Equations

• BakayEtAl2026.Local t p q = (p.parent ∈ t.labeled {PhraseStructure.Cat.S, PhraseStructure.Cat.V} ∧ (p.parent, q) ∈ PhraseStructure.mateRelation (t.labeled {PhraseStructure.Cat.S}))

@[instance_reducible]

instance BakayEtAl2026.instDecidableLocal (t : PhraseStructure.Tree PhraseStructure.Cat Unit) (p q : Core.Order.TreePath) : Decidable (Local t p q)

Equations

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

theorem BakayEtAl2026.local_iff_available (s : Structure) (r : Role) (hr : r ≠ Role.reciprocal) : Local s.tree (s.path r) (s.path Role.reciprocal) ↔ Role.Available s r

On every stimulus Kush's feature at the reciprocal holds of exactly the available antecedents.

inductive BakayEtAl2026.CueSource : Type

A retrieval cue is matched against the hierarchical feature or against an item-level feature stored with the candidate.

• hierarchical : CueSource
• itemLevel : CueSource

@[instance_reducible]

instance BakayEtAl2026.instDecidableEqCueSource : DecidableEq CueSource

Equations

• BakayEtAl2026.instDecidableEqCueSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BakayEtAl2026.instFintypeCueSource : Fintype CueSource

Equations

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

@[instance_reducible]

instance BakayEtAl2026.instReprCueSource : Repr CueSource

Equations

• BakayEtAl2026.instReprCueSource = { reprPrec := BakayEtAl2026.instReprCueSource.repr }

def BakayEtAl2026.instReprCueSource.repr : CueSource → ℕ → Std.Format

Equations

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

structure BakayEtAl2026.Cue (F : Type u_1) : Type u_1

A retrieval cue is a feature a candidate should carry, tagged with where it is matched.

• source : CueSource

  Where the cue is matched.

• feature : F

  The feature the cue seeks.

def BakayEtAl2026.matchCount {F : Type u_1} [DecidableEq F] (feats : List F) (cues : List (Cue F)) (s : CueSource) : ℕ

matchCount feats cues s counts the cues matched at s that a candidate with the features feats matches.

Equations

• BakayEtAl2026.matchCount feats cues s = List.countP (fun (c : BakayEtAl2026.Cue F) => decide (c.source = s ∧ c.feature ∈ feats)) cues

def BakayEtAl2026.weightedActivation {F : Type u_1} [DecidableEq F] (w : CueSource → ℕ) (feats : List F) (cues : List (Cue F)) : ℕ

Activation is the count of matched cues, weighted by where they are matched.

Equations

• BakayEtAl2026.weightedActivation w feats cues = ∑ s : BakayEtAl2026.CueSource, w s * BakayEtAl2026.matchCount feats cues s

theorem BakayEtAl2026.matchCount_le {F : Type u_1} [DecidableEq F] {a b : List F} {cues : List (Cue F)} (h : ∀ c ∈ cues, c.feature ∈ b → c.feature ∈ a) (s : CueSource) : matchCount b cues s ≤ matchCount a cues s

A candidate that matches whatever cue another matches matches at least as many cues at every source.

theorem BakayEtAl2026.weightedActivation_lt {F : Type u_1} [DecidableEq F] {w : CueSource → ℕ} {a b : List F} {cues : List (Cue F)} (hle : ∀ (s : CueSource), matchCount b cues s ≤ matchCount a cues s) (hlt : ∃ (s : CueSource), 0 < w s ∧ matchCount b cues s < matchCount a cues s) : weightedActivation w b cues < weightedActivation w a cues

A candidate whose matches dominate another's at every source, strictly at a source with positive weight, out-activates it.

inductive BakayEtAl2026.Feature : Type

A noun phrase is stored with Kush's local feature, a clause-mate feature, its number and its case.

• local : Feature
• clauseMate : Feature
• number (n : Number) : Feature
• marking (c : Case) : Feature

def BakayEtAl2026.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) : Decidable (x✝ = x✝¹)

Equations

• BakayEtAl2026.instDecidableEqFeature.decEq BakayEtAl2026.Feature.local BakayEtAl2026.Feature.local = isTrue ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq BakayEtAl2026.Feature.local BakayEtAl2026.Feature.clauseMate = isFalse BakayEtAl2026.instDecidableEqFeature.decEq._proof_3
• BakayEtAl2026.instDecidableEqFeature.decEq BakayEtAl2026.Feature.local (BakayEtAl2026.Feature.number n) = isFalse ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq BakayEtAl2026.Feature.local (BakayEtAl2026.Feature.marking c) = isFalse ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq BakayEtAl2026.Feature.clauseMate BakayEtAl2026.Feature.local = isFalse BakayEtAl2026.instDecidableEqFeature.decEq._proof_6
• BakayEtAl2026.instDecidableEqFeature.decEq BakayEtAl2026.Feature.clauseMate BakayEtAl2026.Feature.clauseMate = isTrue ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq BakayEtAl2026.Feature.clauseMate (BakayEtAl2026.Feature.number n) = isFalse ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq BakayEtAl2026.Feature.clauseMate (BakayEtAl2026.Feature.marking c) = isFalse ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq (BakayEtAl2026.Feature.number n) BakayEtAl2026.Feature.local = isFalse ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq (BakayEtAl2026.Feature.number n) BakayEtAl2026.Feature.clauseMate = isFalse ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq (BakayEtAl2026.Feature.number a) (BakayEtAl2026.Feature.number b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq (BakayEtAl2026.Feature.number n) (BakayEtAl2026.Feature.marking c) = isFalse ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq (BakayEtAl2026.Feature.marking c) BakayEtAl2026.Feature.local = isFalse ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq (BakayEtAl2026.Feature.marking c) BakayEtAl2026.Feature.clauseMate = isFalse ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq (BakayEtAl2026.Feature.marking c) (BakayEtAl2026.Feature.number n) = isFalse ⋯
• BakayEtAl2026.instDecidableEqFeature.decEq (BakayEtAl2026.Feature.marking a) (BakayEtAl2026.Feature.marking b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BakayEtAl2026.instDecidableEqFeature : DecidableEq Feature

Equations

• BakayEtAl2026.instDecidableEqFeature = BakayEtAl2026.instDecidableEqFeature.decEq

def BakayEtAl2026.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BakayEtAl2026.instReprFeature : Repr Feature

Equations

• BakayEtAl2026.instReprFeature = { reprPrec := BakayEtAl2026.instReprFeature.repr }

def BakayEtAl2026.Role.features (s : Structure) (r : Role) (n : Number) (c : Case) : List Feature

The features of the noun phrase r of s, of number n and case c. It carries the local feature when Kush's feature holds of it at the reciprocal, and the clause-mate feature when it shares the reciprocal's minimal clause.

Equations

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

def BakayEtAl2026.birbirleriCues : List (Cue Feature)

Birbirleri cues the local feature, the clause-mate feature and the number of the fragment's reciprocal, which its antecedent shares.

Equations

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

theorem BakayEtAl2026.birbirleriCues_eq : birbirleriCues = [{ source := CueSource.hierarchical, feature := Feature.local }, { source := CueSource.itemLevel, feature := Feature.clauseMate }, { source := CueSource.itemLevel, feature := Feature.number Number.plural }]

theorem BakayEtAl2026.features_embeddedSubject (s : Structure) (n : Number) (c : Case) : Role.features s Role.embeddedSubject n c = [Feature.local, Feature.clauseMate, Feature.number n, Feature.marking c]

theorem BakayEtAl2026.features_second {s : Structure} (hs : s ≠ Structure.indirectObject) (n : Number) (c : Case) : Role.features s Role.second n c = [Feature.clauseMate, Feature.number n, Feature.marking c]

theorem BakayEtAl2026.target_retrieved {s : Structure} (hs : s ≠ Structure.indirectObject) {w : CueSource → ℕ} (hw : 0 < w CueSource.hierarchical) (n : Number) (cT cD : Case) : weightedActivation w (Role.features s Role.second n cD) birbirleriCues < weightedActivation w (Role.features s Role.embeddedSubject Number.plural cT) birbirleriCues

The plural embedded subject out-activates a distractor of any number and case under any weighting that gives the hierarchical cue weight. The subject matches every cue, and the distractor lacks the local feature.

theorem BakayEtAl2026.distractor_interference {s : Structure} (hs : s ≠ Structure.indirectObject) {w : CueSource → ℕ} (hw : 0 < w CueSource.itemLevel) (c : Case) : weightedActivation w (Role.features s Role.second Number.singular c) birbirleriCues < weightedActivation w (Role.features s Role.second Number.plural c) birbirleriCues

A distractor that matches the reciprocal in number out-activates one that does not, under any weighting that gives item-level cues weight.

The privileged representation

def BakayEtAl2026.Privileged (s : Structure) (r : Role) : Prop

A noun phrase is in the privileged store at the reciprocal when it c-commands the reciprocal from within the reciprocal's clause.

Equations

• BakayEtAl2026.Privileged s r = (r ∈ s.configuration.domain BakayEtAl2026.Role.reciprocal ∧ s.configuration.commands r BakayEtAl2026.Role.reciprocal)

theorem BakayEtAl2026.privileged_iff_available {s : Structure} {r : Role} (hr : r ≠ Role.reciprocal) : Privileged s r ↔ Role.Available s r

The privileged store holds exactly Principle A's available antecedents.

theorem BakayEtAl2026.not_privileged_second {s : Structure} (hs : s ≠ Structure.indirectObject) : ¬Privileged s Role.second

No distractor enters the privileged store.

The paper's stimuli

def BakayEtAl2026.structure? (x : Datum) : Option Structure

The structure a row records, by its distractor or its second noun phrase.

Equations

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

def BakayEtAl2026.roles : List (String × Role)

The noun phrases the rows' readings name.

Equations

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

theorem BakayEtAl2026.rows_parse (x : Datum) : x ∈ Examples.all → (structure? x).isSome = true ∧ ∀ y ∈ x.readings, (List.lookup y.1 roles).isSome = true

Every row records its structure, and every reading names a noun phrase.

theorem BakayEtAl2026.rows_available (x : Datum) : x ∈ Examples.all → ∀ s ∈ structure? x, ∀ y ∈ x.readings, ∀ r ∈ List.lookup y.1 roles, y.2 = Judgment.acceptable ↔ Role.Available s r

Each row's coindexations are Principle A on its structure.