Question typology — substrate

@cite{wals-2013} @cite{pesetsky-1987} @cite{huang-1982} @cite{sato-ngui-2017} @cite{chan-shen-2026}

Per-language question-typology substrate for Fragment import. Mirrors the Linglib/Typology/{Domain}.lean pattern (Possession, Case, Phonology, WordOrder).

Substrate enums

• WhMovementStrategy (WALS Ch 93A)
• WhInterpMechanism (@cite{pesetsky-1987}, @cite{huang-1982}, @cite{sato-ngui-2017})
• QParticlePosition (WALS Ch 92A)
• PolarQuestionStrategy (WALS Ch 116A)
• QuestionProfile: bundle struct over Chs 92A/93A/116A
• MWFParameter: multiple-wh-fronting parameter (@cite{rudin-1988}, with @cite{citko-gracanin-yuksek-2025}'s tri-valued refinement splitting non-MWF into vP-only vs both-edges asterisk languages)
• PhaseEdge: which phase edge an asterisk lands on
• EdgeAsterisk/MWFViolation/EllipsisRepairsMWF: Prop predicates derived from MWFParameter

Theory-laden caveats

• WhInterpMechanism is NOT theory-neutral. The four mechanisms (overtMovement, covertMovement, partialMovement, unselectiveBinding) commit to a movement-vs-binding split that is contested. Cable 2010's Q-particle Agree analysis, Reinhart's choice functions, and Beck 2006's intervention-based account each derive the same surface position via different mechanisms. The partialMovement case is specifically Sato & Ngui 2017's Singlish analysis.

• The cartographic clause-typing locus is contested. Rizzi 1997 places it at Force⁰[+Q]; Holmberg 2016 places it at Pol⁰; Dayal 2025 places it at C with PerspP-shift. QuestionProfile is silent on this — see Phenomena/Questions/Studies/Dayal2025.lean, Phenomena/Questions/Studies/Holmberg2016.lean, and Theories/Syntax/Minimalist/Questions.lean for competing analyses.

WALS aggregates

WALS chapter aggregate distributions (ch92Total, ch93Total, etc.) live in this file at the substrate layer per the project's "WALS goes to Linglib/Typology/" rule. Cross-linguistic theorems consuming Fragment per-language data live in Phenomena/Questions/Studies/Dryer2013.lean.

inductive Typology.Question.WhMovementStrategy : Type

WALS Ch 93A: position of interrogative phrases (wh-words).

• initial : WhMovementStrategy

  Wh-phrase obligatorily fronted (overt wh-movement).

• inSitu : WhMovementStrategy

  Wh-phrase stays in situ.

• mixed : WhMovementStrategy

  Both strategies available.

@[implicit_reducible]

instance Typology.Question.instDecidableEqWhMovementStrategy : DecidableEq WhMovementStrategy

Equations

• Typology.Question.instDecidableEqWhMovementStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Question.instReprWhMovementStrategy.repr : WhMovementStrategy → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Question.instReprWhMovementStrategy : Repr WhMovementStrategy

Equations

• Typology.Question.instReprWhMovementStrategy = { reprPrec := Typology.Question.instReprWhMovementStrategy.repr }

inductive Typology.Question.WhInterpMechanism : Type

How a wh-phrase is interpreted at the syntax-semantics interface. Distinct from WhMovementStrategy (surface position): the same surface position (in-situ) can arise from different mechanisms (covert movement vs unselective binding), with different empirical consequences for island sensitivity and modifier licensing.

@cite{pesetsky-1987} @cite{sato-ngui-2017} @cite{chan-shen-2026}

• overtMovement : WhInterpMechanism

  Successive cyclic overt movement to matrix Spec-CP.

• covertMovement : WhInterpMechanism

  Single LF movement to Spec-CP (@cite{huang-1982}; Mandarin daodi).

• partialMovement : WhInterpMechanism

  Two-step: overt to intermediate Spec-CP, then covert to matrix Spec-CP. This is Singlish partial wh-movement (@cite{sato-ngui-2017}). Distinct from .covertMovement because the overt-then-covert derivation has both a Spell-Out landing site and a separate covert step that crosses islands at LF.

• unselectiveBinding : WhInterpMechanism

  Q operator in C binds variable in situ; no movement (overt or covert). Island-insensitive.

@[implicit_reducible]

instance Typology.Question.instDecidableEqWhInterpMechanism : DecidableEq WhInterpMechanism

Equations

• Typology.Question.instDecidableEqWhInterpMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Question.instReprWhInterpMechanism.repr : WhInterpMechanism → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Question.instReprWhInterpMechanism : Repr WhInterpMechanism

Equations

• Typology.Question.instReprWhInterpMechanism = { reprPrec := Typology.Question.instReprWhInterpMechanism.repr }

def Typology.Question.WhInterpMechanism.ReachesSpecCP : WhInterpMechanism → Prop

Does this mechanism involve the wh-phrase reaching matrix Spec-CP (overtly or covertly, in one step or two)?

Equations

• Typology.Question.WhInterpMechanism.overtMovement.ReachesSpecCP = True
• Typology.Question.WhInterpMechanism.covertMovement.ReachesSpecCP = True
• Typology.Question.WhInterpMechanism.partialMovement.ReachesSpecCP = True
• Typology.Question.WhInterpMechanism.unselectiveBinding.ReachesSpecCP = False

@[implicit_reducible]

instance Typology.Question.instDecidableReachesSpecCP (m : WhInterpMechanism) : Decidable m.ReachesSpecCP

Equations

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

def Typology.Question.WhInterpMechanism.IslandSensitive : WhInterpMechanism → Prop

Is this mechanism sensitive to syntactic islands? Partial movement is island-sensitive at its covert step (@cite{sato-ngui-2017}: ex 15).

Equations

• Typology.Question.WhInterpMechanism.overtMovement.IslandSensitive = True
• Typology.Question.WhInterpMechanism.covertMovement.IslandSensitive = True
• Typology.Question.WhInterpMechanism.partialMovement.IslandSensitive = True
• Typology.Question.WhInterpMechanism.unselectiveBinding.IslandSensitive = False

@[implicit_reducible]

instance Typology.Question.instDecidableIslandSensitive (m : WhInterpMechanism) : Decidable m.IslandSensitive

Equations

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

def Typology.Question.WhInterpMechanism.HasCovertStep : WhInterpMechanism → Prop

Does this mechanism involve a covert movement step? Distinguishes overt-only from covert/partial. Used by analyses that care about LF-only operations (e.g., island sensitivity diagnostics).

Equations

• Typology.Question.WhInterpMechanism.overtMovement.HasCovertStep = False
• Typology.Question.WhInterpMechanism.covertMovement.HasCovertStep = True
• Typology.Question.WhInterpMechanism.partialMovement.HasCovertStep = True
• Typology.Question.WhInterpMechanism.unselectiveBinding.HasCovertStep = False

@[implicit_reducible]

instance Typology.Question.instDecidableHasCovertStep (m : WhInterpMechanism) : Decidable m.HasCovertStep

Equations

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

theorem Typology.Question.reachesSpecCP_iff_islandSensitive (m : WhInterpMechanism) : m.ReachesSpecCP ↔ m.IslandSensitive

For all current mechanisms, ReachesSpecCP and IslandSensitive coincide. This is a contingent fact about the current taxonomy, not a necessary truth: a future mechanism (e.g., long-distance Agree) could be island-sensitive without reaching Spec-CP, or reach Spec-CP without island sensitivity. The predicates are kept separate for this reason.

inductive Typology.Question.QParticlePosition : Type

WALS Ch 92A: position of polar question particles.

• initial : QParticlePosition

  Particle precedes the clause.

• final : QParticlePosition

  Particle follows the clause.

• secondPosition : QParticlePosition

  Particle in second (Wackernagel) position.

• otherPosition : QParticlePosition

  Other position.

• eitherOfTwo : QParticlePosition

  In either of two positions.

• noParticle : QParticlePosition

  No question particle in the language.

@[implicit_reducible]

instance Typology.Question.instDecidableEqQParticlePosition : DecidableEq QParticlePosition

Equations

• Typology.Question.instDecidableEqQParticlePosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Question.instReprQParticlePosition.repr : QParticlePosition → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Question.instReprQParticlePosition : Repr QParticlePosition

Equations

• Typology.Question.instReprQParticlePosition = { reprPrec := Typology.Question.instReprQParticlePosition.repr }

inductive Typology.Question.PolarQuestionStrategy : Type

WALS Ch 116A: how polar questions are formed.

• particle : PolarQuestionStrategy

  Dedicated question particle.

• verbMorphology : PolarQuestionStrategy

  Interrogative verb morphology.

• particleOrMorphology : PolarQuestionStrategy

  Mixture of particle and verb morphology.

• wordOrder : PolarQuestionStrategy

  Interrogative word order (e.g., subject-aux inversion).

• absenceOfDeclarative : PolarQuestionStrategy

  Absence of declarative morphemes.

• intonationOnly : PolarQuestionStrategy

  Interrogative intonation only.

• noDistinction : PolarQuestionStrategy

  No interrogative-declarative distinction.

@[implicit_reducible]

instance Typology.Question.instDecidableEqPolarQuestionStrategy : DecidableEq PolarQuestionStrategy

Equations

• Typology.Question.instDecidableEqPolarQuestionStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Question.instReprPolarQuestionStrategy.repr : PolarQuestionStrategy → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Question.instReprPolarQuestionStrategy : Repr PolarQuestionStrategy

Equations

• Typology.Question.instReprPolarQuestionStrategy = { reprPrec := Typology.Question.instReprPolarQuestionStrategy.repr }

structure Typology.Question.QuestionProfile : Type

A language's question-formation profile across @cite{wals-2013} Chs 92A, 93A, 116A. Each field is Option since WALS samples vary by chapter.

• language : String

  Language name.

• walsCode : String

  WALS language code.

• qParticlePos : Option QParticlePosition

  Ch 92A: position of polar question particles.

• whMovement : Option WhMovementStrategy

  Ch 93A: wh-phrase position in content questions.

• polarStrategy : Option PolarQuestionStrategy

  Ch 116A: strategy for forming polar questions.

def Typology.Question.instReprQuestionProfile.repr : QuestionProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Question.instReprQuestionProfile : Repr QuestionProfile

Equations

• Typology.Question.instReprQuestionProfile = { reprPrec := Typology.Question.instReprQuestionProfile.repr }

def Typology.Question.instDecidableEqQuestionProfile.decEq (x✝ x✝¹ : QuestionProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Typology.Question.instDecidableEqQuestionProfile : DecidableEq QuestionProfile

Equations

• Typology.Question.instDecidableEqQuestionProfile = Typology.Question.instDecidableEqQuestionProfile.decEq

def Typology.Question.fromWALS92A : Data.WALS.F92A.PositionOfPolarQuestionParticles → QParticlePosition

WALS Ch 92A → QParticlePosition.

Equations

• Typology.Question.fromWALS92A Data.WALS.F92A.PositionOfPolarQuestionParticles.initial = Typology.Question.QParticlePosition.initial
• Typology.Question.fromWALS92A Data.WALS.F92A.PositionOfPolarQuestionParticles.final = Typology.Question.QParticlePosition.final
• Typology.Question.fromWALS92A Data.WALS.F92A.PositionOfPolarQuestionParticles.secondPosition = Typology.Question.QParticlePosition.secondPosition
• Typology.Question.fromWALS92A Data.WALS.F92A.PositionOfPolarQuestionParticles.otherPosition = Typology.Question.QParticlePosition.otherPosition
• Typology.Question.fromWALS92A Data.WALS.F92A.PositionOfPolarQuestionParticles.inEitherOfTwoPositions = Typology.Question.QParticlePosition.eitherOfTwo
• Typology.Question.fromWALS92A Data.WALS.F92A.PositionOfPolarQuestionParticles.noQuestionParticle = Typology.Question.QParticlePosition.noParticle

def Typology.Question.fromWALS93A : Data.WALS.F93A.PositionOfInterrogativePhrasesInContentQuestions → WhMovementStrategy

WALS Ch 93A → WhMovementStrategy.

Equations

• Typology.Question.fromWALS93A Data.WALS.F93A.PositionOfInterrogativePhrasesInContentQuestions.initialInterrogativePhrase = Typology.Question.WhMovementStrategy.initial
• Typology.Question.fromWALS93A Data.WALS.F93A.PositionOfInterrogativePhrasesInContentQuestions.notInitialInterrogativePhrase = Typology.Question.WhMovementStrategy.inSitu
• Typology.Question.fromWALS93A Data.WALS.F93A.PositionOfInterrogativePhrasesInContentQuestions.mixed = Typology.Question.WhMovementStrategy.mixed

def Typology.Question.fromWALS116A : Data.WALS.F116A.PolarQuestionType → PolarQuestionStrategy

WALS Ch 116A → PolarQuestionStrategy.

Equations

• Typology.Question.fromWALS116A Data.WALS.F116A.PolarQuestionType.questionParticle = Typology.Question.PolarQuestionStrategy.particle
• Typology.Question.fromWALS116A Data.WALS.F116A.PolarQuestionType.interrogativeVerbMorphology = Typology.Question.PolarQuestionStrategy.verbMorphology
• Typology.Question.fromWALS116A Data.WALS.F116A.PolarQuestionType.mixtureOfPreviousTwoTypes = Typology.Question.PolarQuestionStrategy.particleOrMorphology
• Typology.Question.fromWALS116A Data.WALS.F116A.PolarQuestionType.interrogativeWordOrder = Typology.Question.PolarQuestionStrategy.wordOrder
• Typology.Question.fromWALS116A Data.WALS.F116A.PolarQuestionType.absenceOfDeclarativeMorphemes = Typology.Question.PolarQuestionStrategy.absenceOfDeclarative
• Typology.Question.fromWALS116A Data.WALS.F116A.PolarQuestionType.interrogativeIntonationOnly = Typology.Question.PolarQuestionStrategy.intonationOnly
• Typology.Question.fromWALS116A Data.WALS.F116A.PolarQuestionType.noInterrogativeDeclarativeDistinction = Typology.Question.PolarQuestionStrategy.noDistinction

inductive Typology.Question.MWFParameter : Type

The MWF parameter as in @cite{rudin-1988} + @cite{citko-gracanin-yuksek-2025}.

The textbook contrast (@cite{rudin-1988}) is binary — MWF (Bulgarian, Romanian) vs non-MWF (English, German, Greek). C&G-Y refine the non-MWF case by where the PF asterisk for multiple wh-specifiers lands: vP-only (sluicing repairs by deleting vP) vs both vP and CP (sluicing leaves the CP-edge asterisk unrepaired). The tripartition lets the multiple-sluicing asymmetry be derived from the parameter rather than stipulated as an independent flag.

• fronts : MWFParameter

  Multiple wh-fronting language (Bulgarian, Romanian). No PF asterisk at any edge.

• nonFrontsVPOnly : MWFParameter

  Non-MWF with vP-only asterisk (German, Greek; @cite{citko-gracanin-yuksek-2025} "English variety B"). Sluicing (deleting the vP edge) repairs.

• nonFrontsBothEdges : MWFParameter

  Non-MWF with asterisks at both vP and CP edges (@cite{citko-gracanin-yuksek-2025} "English variety A"). Sluicing cannot repair — the CP-edge asterisk survives ellipsis.

@[implicit_reducible]

instance Typology.Question.instDecidableEqMWFParameter : DecidableEq MWFParameter

Equations

• Typology.Question.instDecidableEqMWFParameter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Question.instReprMWFParameter : Repr MWFParameter

Equations

• Typology.Question.instReprMWFParameter = { reprPrec := Typology.Question.instReprMWFParameter.repr }

def Typology.Question.instReprMWFParameter.repr : MWFParameter → Nat → Std.Format

Equations

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

inductive Typology.Question.PhaseEdge : Type

Which phase edge is being checked for an MWF asterisk.

• vP : PhaseEdge
• CP : PhaseEdge

@[implicit_reducible]

instance Typology.Question.instDecidableEqPhaseEdge : DecidableEq PhaseEdge

Equations

• Typology.Question.instDecidableEqPhaseEdge x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Question.instReprPhaseEdge.repr : PhaseEdge → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Question.instReprPhaseEdge : Repr PhaseEdge

Equations

• Typology.Question.instReprPhaseEdge = { reprPrec := Typology.Question.instReprPhaseEdge.repr }

def Typology.Question.MWFParameter.AllowsMWF : MWFParameter → Prop

The language allows multiple wh-fronting in matrix questions.

Equations

• Typology.Question.MWFParameter.fronts.AllowsMWF = True
• Typology.Question.MWFParameter.nonFrontsVPOnly.AllowsMWF = False
• Typology.Question.MWFParameter.nonFrontsBothEdges.AllowsMWF = False

@[implicit_reducible]

instance Typology.Question.MWFParameter.instDecidableAllowsMWF (p : MWFParameter) : Decidable p.AllowsMWF

Equations

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

def Typology.Question.MWFParameter.EdgeAsterisk : MWFParameter → PhaseEdge → Nat → Prop

The given phase edge incurs a PF asterisk under n > 1 wh-specifiers. Generalizes the per-edge vPEdgeAsterisk / cPEdgeAsterisk distinction earlier revisions of this code carried as separate definitions.

Equations

• Typology.Question.MWFParameter.fronts.EdgeAsterisk x✝¹ x✝ = False
• Typology.Question.MWFParameter.nonFrontsVPOnly.EdgeAsterisk Typology.Question.PhaseEdge.vP x✝ = (x✝ > 1)
• Typology.Question.MWFParameter.nonFrontsVPOnly.EdgeAsterisk Typology.Question.PhaseEdge.CP x✝ = False
• Typology.Question.MWFParameter.nonFrontsBothEdges.EdgeAsterisk x✝¹ x✝ = (x✝ > 1)

@[implicit_reducible]

instance Typology.Question.MWFParameter.instDecidableEdgeAsterisk (p : MWFParameter) (e : PhaseEdge) (n : Nat) : Decidable (p.EdgeAsterisk e n)

Equations

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

def Typology.Question.MWFViolation (p : MWFParameter) (n : Nat) : Prop

A multiple-wh-fronting violation: some phase edge incurs an asterisk for n wh-specifiers.

Equations

• Typology.Question.MWFViolation p n = (p.EdgeAsterisk Typology.Question.PhaseEdge.vP n ∨ p.EdgeAsterisk Typology.Question.PhaseEdge.CP n)

@[implicit_reducible]

instance Typology.Question.instDecidableMWFViolation (p : MWFParameter) (n : Nat) : Decidable (MWFViolation p n)

Equations

• Typology.Question.instDecidableMWFViolation p n = id inferInstance

def Typology.Question.EllipsisRepairsMWF (p : MWFParameter) (n : Nat) (vpEdgeDeleted : Bool) : Prop

Ellipsis of the vP edge repairs an MWF violation iff doing so eliminates every asterisk — i.e., there is no surviving CP-edge asterisk. In nonFrontsVPOnly languages, deleting the vP edge removes the only asterisk; in nonFrontsBothEdges, the CP-edge asterisk survives.

Equations

• Typology.Question.EllipsisRepairsMWF p n vpEdgeDeleted = (¬Typology.Question.MWFViolation p n ∨ vpEdgeDeleted = true ∧ ¬p.EdgeAsterisk Typology.Question.PhaseEdge.CP n)

@[implicit_reducible]

instance Typology.Question.instDecidableEllipsisRepairsMWF (p : MWFParameter) (n : Nat) (vpDel : Bool) : Decidable (EllipsisRepairsMWF p n vpDel)

Equations

• Typology.Question.instDecidableEllipsisRepairsMWF p n vpDel = id inferInstance

theorem Typology.Question.single_wh_no_violation (p : MWFParameter) : ¬MWFViolation p 1

Single wh-specifier never triggers an MWF violation.

theorem Typology.Question.zero_wh_no_violation (p : MWFParameter) : ¬MWFViolation p 0

Zero wh-specifiers never trigger an MWF violation.

theorem Typology.Question.mwf_language_no_violation (p : MWFParameter) (h : p.AllowsMWF) (n : Nat) : ¬MWFViolation p n

MWF languages never have violations.