Head-Filler Schema and SLASH Feature

@cite{ginzburg-sag-2000} @cite{pollard-sag-1994} @cite{mueller-2013}

HPSG's third combination schema: the Head-Filler Schema handles long-distance dependencies (extraction, wh-movement). A filler XP combines with a sentence containing a gap (SLASH feature) of matching category.

Together with Head-Complement and Head-Subject (in Basic.lean), this completes HPSG's three immediate dominance schemata.

Key types

• SlashValue — the set of categories expected to fill gaps
• SynsemSlash — extends Synsem with SLASH
• HeadFillerRule — filler combines with S[SLASH {XP}], discharging the gap
• HPSGSchema — unifies all three schemata
• TrackedSign — sign paired with its SLASH value
• GapRestriction — island constraints via GAP restrictions

Connection to @cite{mueller-2013}

Müller §2.3: "the formalization of internal Merge and that of the head-filler schema are very similar" — both handle displacement by pairing a moved element with its extraction site.

SLASH features

structure HPSG.SlashValue : Type

The SLASH value: a set of categories for which gaps exist.

In HPSG, SLASH is a set-valued feature on phrases. A phrase with SLASH {NP} contains an NP gap somewhere inside it. The Head-Filler schema discharges one element from this set.

• gaps : List UD.UPOS

  Categories of gaps in this phrase

instance HPSG.instReprSlashValue : Repr SlashValue

Equations

• HPSG.instReprSlashValue = { reprPrec := HPSG.instReprSlashValue.repr }

def HPSG.instReprSlashValue.repr : SlashValue → Nat → Std.Format

Equations

• HPSG.instReprSlashValue.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "gaps" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.gaps)).group) " }"

instance HPSG.instDecidableEqSlashValue : DecidableEq SlashValue

Equations

• HPSG.instDecidableEqSlashValue = HPSG.instDecidableEqSlashValue.decEq

def HPSG.instDecidableEqSlashValue.decEq (x✝ x✝¹ : SlashValue) : Decidable (x✝ = x✝¹)

Equations

• HPSG.instDecidableEqSlashValue.decEq { gaps := a } { gaps := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def HPSG.SlashValue.empty : SlashValue

Empty SLASH value (no gaps).

Equations

• HPSG.SlashValue.empty = { gaps := [] }

def HPSG.SlashValue.contains (sv : SlashValue) (c : UD.UPOS) : Bool

Check if SLASH contains a specific category.

Equations

• sv.contains c = sv.gaps.contains c

def HPSG.SlashValue.discharge (sv : SlashValue) (c : UD.UPOS) : SlashValue

Remove a category from SLASH (when a gap is filled).

Equations

• sv.discharge c = { gaps := sv.gaps.erase c }

def HPSG.SlashValue.isEmpty (sv : SlashValue) : Bool

Is this SLASH value empty (no gaps)?

Equations

• sv.isEmpty = sv.gaps.isEmpty

def HPSG.SlashValue.union (s1 s2 : SlashValue) : SlashValue

Union of two SLASH values.

Equations

• s1.union s2 = { gaps := s1.gaps ++ s2.gaps }

instance HPSG.instBEqSlashValue : BEq SlashValue

Equations

• HPSG.instBEqSlashValue = { beq := fun (a b : HPSG.SlashValue) => a.gaps == b.gaps }

Nominal Category Compatibility

In HPSG, all nominals share a single head type (noun). Our UD-based system distinguishes NOUN, PRON, and PROPN. For SLASH matching, these are compatible.

def HPSG.categoriesMatch (c1 c2 : UD.UPOS) : Bool

Are two categories compatible for SLASH matching? All nominal categories (NOUN, PRON, PROPN) match each other.

Equations

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

def HPSG.SlashValue.containsCompatible (sv : SlashValue) (c : UD.UPOS) : Bool

Check if SLASH contains a compatible category (using nominal matching).

Equations

• sv.containsCompatible c = sv.gaps.any (HPSG.categoriesMatch c)

def HPSG.SlashValue.dischargeCompatible (sv : SlashValue) (c : UD.UPOS) : SlashValue

Discharge a compatible category from SLASH.

Equations

• sv.dischargeCompatible c = match List.findIdx? (HPSG.categoriesMatch c) sv.gaps with | some idx => { gaps := sv.gaps.eraseIdx idx } | none => sv

Extended SYNSEM with SLASH

structure HPSG.SynsemSlash : Type

Extended SYNSEM value including the SLASH feature.

This extends the basic Synsem from HPSG.Basic with nonlocal features.

• local_ : Synsem

  Local syntax-semantics features

• slash : SlashValue

  Nonlocal SLASH feature (gap set)

instance HPSG.instReprSynsemSlash : Repr SynsemSlash

Equations

• HPSG.instReprSynsemSlash = { reprPrec := HPSG.instReprSynsemSlash.repr }

def HPSG.instReprSynsemSlash.repr : SynsemSlash → Nat → Std.Format

Equations

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

def HPSG.SynsemSlash.cat (ss : SynsemSlash) : UD.UPOS

Get the category from an extended synsem.

Equations

• ss.cat = ss.local_.cat

Head-Filler Schema

structure HPSG.HeadFillerRule : Type

Head-Filler Schema: filler XP combines with a clause containing a gap.

Schema 3:

       S
      / \
   XP S[SLASH {XP}]
(filler) (head)

The filler's category must match one of the gaps in the head's SLASH set. The result has that gap discharged from SLASH.

• filler : Sign

  The filler phrase (the extracted constituent)

• headPhrase : Sign

  The head phrase (sentence with a gap)

• headSlash : SlashValue

  The SLASH value on the head phrase before combination

• result : Sign

  The result phrase

• slashMatch : self.headSlash.contains self.filler.synsem.cat = true

  The filler's category matches a gap in the head

• resultSlash : SlashValue

  The result has the gap discharged

Unified schema type

inductive HPSG.HPSGSchema : Type

All four HPSG immediate dominance schemata, unified.

This inductive covers the complete set of phrase structure schemata needed for HPSG phrase building. @cite{mueller-2013} argues the first three correspond to three universal combination modes; Head-Modifier handles adjunction (relative clauses, adjective/PP modification).

• headComp : HeadCompRule → HPSGSchema

  Head-Complement: head combines with complements (Schema 1)

• headSubj : HeadSubjRule → HPSGSchema

  Head-Subject: subject combines with head phrase (Schema 2)

• headFiller : HeadFillerRule → HPSGSchema

  Head-Filler: filler combines with gapped clause (Schema 3)

• headMod : HeadModRule → HPSGSchema

  Head-Modifier: head combines with a modifier (Schema 4)

def HPSG.HPSGSchema.result : HPSGSchema → Sign

Get the result sign from any schema application.

Equations

• (HPSG.HPSGSchema.headComp r).result = r.result
• (HPSG.HPSGSchema.headSubj r).result = r.result
• (HPSG.HPSGSchema.headFiller r).result = r.result
• (HPSG.HPSGSchema.headMod r).result = r.result

def HPSG.HPSGSchema.head : HPSGSchema → Sign

Get the head sign from any schema application.

Equations

• (HPSG.HPSGSchema.headComp r).head = r.head
• (HPSG.HPSGSchema.headSubj r).head = r.headPhrase
• (HPSG.HPSGSchema.headFiller r).head = r.headPhrase
• (HPSG.HPSGSchema.headMod r).head = r.headSign

Gap Introduction (Argument Realization Principle)

Per @cite{sag-wasow-bender-2003} Ch. 6, a gap arises when one of a word's ARG-ST elements is realized as GAP rather than COMPS. The GAP value becomes the word's local SLASH contribution.

ARG-ST = SPR ⊕ COMPS ⊕ GAP

A verb with ARG-ST ⟨NP_subj, NP_obj⟩ can realize as:

• Normal: SPR ⟨NP_subj⟩, COMPS ⟨NP_obj⟩, GAP ⟨⟩
• Gapped: SPR ⟨NP_subj⟩, COMPS ⟨⟩, GAP ⟨NP_obj⟩ → SLASH {NP}

def HPSG.gapComplement (w : Word) (ss : Synsem) (gapIdx : Nat) : Option (Sign × SlashValue)

Create a gapped version of a word sign: one complement is removed from COMPS and becomes a SLASH element (via GAP).

Returns the gapped sign and the resulting SLASH value.

Equations

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

structure HPSG.TrackedSign : Type

A sign paired with its SLASH value.

Tracks the nonlocal SLASH feature alongside a locally-typed sign, avoiding modification of the Sign type itself.

• sign : Sign
• slash : SlashValue

instance HPSG.instReprTrackedSign : Repr TrackedSign

Equations

• HPSG.instReprTrackedSign = { reprPrec := HPSG.instReprTrackedSign.repr }

def HPSG.instReprTrackedSign.repr : TrackedSign → Nat → Std.Format

Equations

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

SLASH Amalgamation (Nonlocal Feature Principle)

@cite{sag-wasow-bender-2003} Ch. 6: In a headed phrase, the mother's SLASH is the union of its daughters' SLASH values, minus any elements discharged by the Head-Filler Schema.

def HPSG.amalgamateHeadComp (head comp : TrackedSign) : TrackedSign

Amalgamate SLASH through Head-Complement: head's SLASH ∪ comp's SLASH.

Equations

• HPSG.amalgamateHeadComp head comp = { sign := head.sign, slash := head.slash.union comp.slash }

def HPSG.amalgamateHeadSubj (subj head : TrackedSign) : TrackedSign

Amalgamate SLASH through Head-Subject: subject's SLASH ∪ head's SLASH.

Equations

• HPSG.amalgamateHeadSubj subj head = { sign := head.sign, slash := subj.slash.union head.slash }

theorem HPSG.head_determines_cat_headComp (r : HeadCompRule) : r.result.synsem.cat = r.head.synsem.cat

The head's category propagates to the result (Head Feature Principle).

In all three schemata, the category of the result phrase equals the category of the head daughter. This is the HPSG analogue of the Minimalist labeling algorithm.

theorem HPSG.slash_discharged_default (filler headPhrase result : Sign) (headSlash : SlashValue) (slashMatch : headSlash.contains filler.synsem.cat = true) : { filler := filler, headPhrase := headPhrase, headSlash := headSlash, result := result, slashMatch := slashMatch }.resultSlash = headSlash.discharge filler.synsem.cat

When constructing a HeadFillerRule with the default resultSlash, the gap matching the filler is discharged.

Islands as GAP restrictions

@cite{hofmeister-sag-2010} argues that island constraints are construction-specific restrictions on the GAP value, not universal Subjacency. This eliminates the need for a separate island module in the grammar.

• Absolute islands: [GAP ⟨⟩] on the mother — no F-G dependency can penetrate (topicalization, exclamatives)
• Weak islands: [GAP list(NP)] — only NP gaps pass through (e.g., wh-islands allow NP extraction but not PP)
• Unrestricted: any GAP value permeates (no island constraint)

inductive HPSG.GapRestriction : Type

GAP restriction on a construction.

This classifies constructions by what kinds of gaps they permit, deriving island effects from the same feature system used for non-island dependencies.

• unrestricted : GapRestriction
• npOnly : GapRestriction
• noGap : GapRestriction

instance HPSG.instReprGapRestriction : Repr GapRestriction

Equations

• HPSG.instReprGapRestriction = { reprPrec := HPSG.instReprGapRestriction.repr }

def HPSG.instReprGapRestriction.repr : GapRestriction → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• HPSG.instReprGapRestriction.repr HPSG.GapRestriction.npOnly prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.GapRestriction.npOnly")).group prec✝
• HPSG.instReprGapRestriction.repr HPSG.GapRestriction.noGap prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.GapRestriction.noGap")).group prec✝

instance HPSG.instDecidableEqGapRestriction : DecidableEq GapRestriction

Equations

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

instance HPSG.instBEqGapRestriction : BEq GapRestriction

Equations

• HPSG.instBEqGapRestriction = { beq := HPSG.instBEqGapRestriction.beq }

def HPSG.instBEqGapRestriction.beq : GapRestriction → GapRestriction → Bool

Equations

• HPSG.instBEqGapRestriction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def HPSG.GapRestriction.isAbsoluteIsland : GapRestriction → Bool

Does this GAP restriction block all extraction?

Equations

• HPSG.GapRestriction.noGap.isAbsoluteIsland = true
• x✝.isAbsoluteIsland = false

def HPSG.GapRestriction.allowsNPExtraction : GapRestriction → Bool

Does this GAP restriction allow NP extraction?

Equations

• HPSG.GapRestriction.unrestricted.allowsNPExtraction = true
• HPSG.GapRestriction.npOnly.allowsNPExtraction = true
• HPSG.GapRestriction.noGap.allowsNPExtraction = false

def HPSG.SlashValue.satisfiesRestriction (sv : SlashValue) (r : GapRestriction) : Bool

A SLASH value satisfies a GAP restriction if all its gaps are permitted by the restriction.

Equations

• sv.satisfiesRestriction HPSG.GapRestriction.unrestricted = true
• sv.satisfiesRestriction HPSG.GapRestriction.npOnly = sv.gaps.all fun (x : UD.UPOS) => x == UD.UPOS.NOUN
• sv.satisfiesRestriction HPSG.GapRestriction.noGap = sv.gaps.isEmpty

theorem HPSG.empty_satisfies_any_restriction (r : GapRestriction) : SlashValue.empty.satisfiesRestriction r = true

Empty SLASH always satisfies any restriction.

Object extraction: "What did John see ___?"

Derivation sketch:

1. "see" has COMPS ⟨NP⟩
2. Gap complement: COMPS ⟨⟩, SLASH {NP}
3. Head-Subject with "John": S[SLASH {NP}]
4. Head-Filler with "what": S[SLASH {}] — gap discharged

theorem HPSG.extraction_complete : HPSG.result_slash✝.isEmpty = true

Full end-to-end derivation: gap introduction → SLASH amalgamation → Head-Filler discharge → empty SLASH.

Islands block SLASH propagation

When a construction has a GAP restriction of .noGap, no SLASH values can percolate through it. This blocks extraction from islands.

Example: "*What did John wonder who saw ___?"

• The embedded question "who saw ___" has SLASH {NP}
• But the embedded question construction has [GAP ⟨⟩] (.noGap)
• SLASH cannot pass through → extraction blocked

def HPSG.propagateSlash (sv : SlashValue) (restriction : GapRestriction) : SlashValue

Check that a SLASH value can propagate through a construction. Returns the SLASH that survives the restriction.

Equations

• HPSG.propagateSlash sv restriction = if sv.satisfiesRestriction restriction = true then sv else HPSG.SlashValue.empty

theorem HPSG.extraction_from_nonisland (c : UD.UPOS) : (propagateSlash { gaps := [c] } GapRestriction.unrestricted).gaps = [c]

Extraction from a non-island construction always succeeds.

theorem HPSG.extraction_blocked_by_island (gaps : List UD.UPOS) (h : gaps ≠ []) : (propagateSlash { gaps := gaps } GapRestriction.noGap).isEmpty = true

Extraction from an absolute island is always blocked.