Wh-modifiers

Wh-the-hell and its kin (the heck, in the world, Mandarin daodi, Japanese ittai) are wh-modifiers with a distribution bare wh-words lack ([Pes87]'s aggressively non-D-linked phrases; [HN08], [JA20] on the English family). An entry records the one parameter on which [CS26] separate English and Singlish the-hell from Mandarin daodi: whether the modifier reaches its matrix scope position only on the wh-phrase it adjoins to ([Mer02]) or by movement of its own ([Cho12]). WhModifier.Licensed is the resulting scope condition, taking as a parameter whether the host reaches that position, which a syntax of the host's question supplies.

References

• [Pes87]
• [Mer02]
• [Cho12]
• [CS26]
• [HN08]
• [JA20]

inductive WhModifier.Mobility : Type

How the modifier reaches its scope position: adjoined to the wh-head and carried by the wh-phrase (English and Singlish the-hell, [Mer02]), or by movement of its own (Mandarin daodi, [Cho12]).

• parasitic : Mobility
• independent : Mobility

@[instance_reducible]

instance WhModifier.instDecidableEqMobility : DecidableEq Mobility

Equations

• WhModifier.instDecidableEqMobility x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WhModifier.instReprMobility.repr : Mobility → Nat → Std.Format

Equations

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

@[instance_reducible]

instance WhModifier.instReprMobility : Repr Mobility

Equations

• WhModifier.instReprMobility = { reprPrec := WhModifier.instReprMobility.repr }

structure WhModifier : Type

An aggressively non-D-linked wh-modifier ([Pes87]): form, gloss, and how it reaches its scope position.

• form : String
• gloss : String
• mobility : Mobility

def instDecidableEqWhModifier.decEq (x✝ x✝¹ : WhModifier) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqWhModifier : DecidableEq WhModifier

Equations

• instDecidableEqWhModifier = instDecidableEqWhModifier.decEq

def instReprWhModifier.repr : WhModifier → Nat → Std.Format

Equations

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

@[instance_reducible]

instance instReprWhModifier : Repr WhModifier

Equations

• instReprWhModifier = { reprPrec := instReprWhModifier.repr }

def WhModifier.Licensed (m : WhModifier) (hostReachesScope : Prop) : Prop

The modifier is licensed iff it reaches its matrix scope position: with its host, when the host does, or on its own.

Equations

• m.Licensed hostReachesScope = (hostReachesScope ∨ m.mobility = WhModifier.Mobility.independent)

@[instance_reducible]

instance WhModifier.instDecidableLicensed (m : WhModifier) (P : Prop) [Decidable P] : Decidable (m.Licensed P)

Equations

• m.instDecidableLicensed P = { decide := decide P || decide (m.mobility = WhModifier.Mobility.independent), reflects_decide := ⋯ }

theorem WhModifier.licensed_iff_of_parasitic {m : WhModifier} (P : Prop) (h : m.mobility = Mobility.parasitic) : m.Licensed P ↔ P

A parasitic modifier is licensed iff its host reaches the scope position.

theorem WhModifier.licensed_of_independent {m : WhModifier} (P : Prop) (h : m.mobility = Mobility.independent) : m.Licensed P

An independent modifier is licensed whatever its host does.