Overt reflexes of a designated constituent

A grammar leaves perceptible traces of a constituent's designated status: of a focus, of an A′-extraction site, of an intermediate landing site of successive-cyclic movement. A Reflex is a perceptible perturbation at a host constituent: a displaced exponent, a morpheme with its marker, a phrase edge, or metrical prominence. A marking system assigns each designated target its finite set of reflexes. Reflexes classify by Reflex.Modality and further by Reflex.Channel, the phonological, morphological and syntactic cut. Like Judgment for acceptability, this is a vocabulary for what a theory predicts: studies translate their predictions into it, and no theory consumes it as machinery.

Main declarations

• Reflex: the four kinds of reflex, Reflex.morpheme carrying its marker as a list of morphs so that one morpheme at two hosts is one marker twice.
• Reflex.IsOvert: a morpheme reflex has a nonempty marker.
• Reflex.PiedPipes, Reflex.AntiPiedPipes, Reflex.ExactlyTargets: Branan and Erlewine's three configurations of host and target in the containment order.
• Reflex.ExactlyTargets.piedPipes_iff, Reflex.ExactlyTargets.antiPiedPipes_iff: reflexes sharing a host relate to a target as the host does.

Implementation notes

• Only perceptible alternants are reflexes. A string-vacuous operation (Hausa subject fronting) contributes none, a default exponent surfacing whatever the designation (the Wolof expletive l-) is not one since reflexes covary with the target, and zero is never one, covert marking being exponence-side competition, which IsOvert states of a morpheme reflex. Deletion of otherwise expected material (Malay voice-marker deletion) is a reflex. Semantic reflexes of movement (intermediate scope, reconstruction) are interpretation facts left to their studies.
• The marker of a morpheme reflex is the list of morphs coding it, as Voice.marker codes a voice, so a fragment whose reflex is a voice alternation passes the voice's marker through. A paradigm alternation with no segmentable exponent, such as the Hausa relative form of the person–aspect complex, carries the alternant as a free morph.
• With constituents ordered by containment, a host is the target itself, properly contains it, is properly contained in it, or is incomparable to it (IncompRel (· ≤ ·), external hosting, as with the verb-hosted extraction morphology of the Mayan Agent Focus configuration). The predicates are stated in the order vocabulary over a reflex set and an explicit target, so a study asserts the target in the claim.
• The claim that every designated target receives an overt reflex is ∀ i, (realize i).Nonempty over a marking system, which Tangale and Hausa focus each refute.

TODO

• The overlap-weakening of Hartmann and Zimmermann's Ex-Situ Generalisation for Hausa, which needs a structured-meaning overlap predicate.

References

• [BE23]
• [Geo17]
• [HZ04]
• [HZ07c]
• [McC02]

inductive Reflex.Channel : Type

The channel of a reflex is the module whose output carries the trace, the literature's cut between phonological, morphological and syntactic reflexes of one process.

• phonological : Channel
• morphological : Channel
• syntactic : Channel

@[instance_reducible]

instance Reflex.instDecidableEqChannel : DecidableEq Channel

Equations

• Reflex.instDecidableEqChannel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Reflex.instReprChannel : Repr Channel

Equations

• Reflex.instReprChannel = { reprPrec := Reflex.instReprChannel.repr }

def Reflex.instReprChannel.repr : Channel → ℕ → Std.Format

Equations

• Reflex.instReprChannel.repr Reflex.Channel.phonological prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reflex.Channel.phonological")).group prec✝
• Reflex.instReprChannel.repr Reflex.Channel.morphological prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reflex.Channel.morphological")).group prec✝
• Reflex.instReprChannel.repr Reflex.Channel.syntactic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reflex.Channel.syntactic")).group prec✝

inductive Reflex.Modality : Type

A marking modality is a kind of perceptible perturbation. The two prosodic cases keep the demarcative and the culminative apart.

• displacement : Modality

  An exponent constituent surfaces displaced from its base position, a syntactic reflex.

• morpheme : Modality

  A dedicated morpheme (affix, particle, or form alternation) at a host, a morphological reflex.

• boundary : Modality

  A phrase edge at a host, a demarcative phonological reflex (the Tangale and Chadic pattern).

• prominence : Modality

  Metrical prominence on a host, a culminative phonological reflex (the English pattern).

@[instance_reducible]

instance Reflex.instDecidableEqModality : DecidableEq Modality

Equations

• Reflex.instDecidableEqModality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Reflex.instReprModality.repr : Modality → ℕ → Std.Format

Equations

• Reflex.instReprModality.repr Reflex.Modality.displacement prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reflex.Modality.displacement")).group prec✝
• Reflex.instReprModality.repr Reflex.Modality.morpheme prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reflex.Modality.morpheme")).group prec✝
• Reflex.instReprModality.repr Reflex.Modality.boundary prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reflex.Modality.boundary")).group prec✝
• Reflex.instReprModality.repr Reflex.Modality.prominence prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reflex.Modality.prominence")).group prec✝

@[instance_reducible]

instance Reflex.instReprModality : Repr Modality

Equations

• Reflex.instReprModality = { reprPrec := Reflex.instReprModality.repr }

inductive Reflex (C : Type u_1) : Type u_1

A single overt reflex at a host constituent.

• displacement {C : Type u_1} (exponent : C) : Reflex C

  An exponent constituent surfaces displaced from its base position.

• morpheme {C : Type u_1} (host : C) (marker : List Morphology.Morph) : Reflex C

  A dedicated morpheme at a host constituent, coded by its marker.

• boundary {C : Type u_1} (edge : C) : Reflex C

  A phrase edge at a host constituent.

• prominence {C : Type u_1} (host : C) : Reflex C

  Metrical prominence on a host constituent.

def instDecidableEqReflex.decEq {C✝ : Type u_1} [DecidableEq C✝] (x✝ x✝¹ : Reflex C✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqReflex.decEq (Reflex.displacement a) (Reflex.displacement b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.displacement exponent) (Reflex.morpheme host marker) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.displacement exponent) (Reflex.boundary edge) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.displacement exponent) (Reflex.prominence host) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.morpheme host marker) (Reflex.displacement exponent) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.morpheme a a_1) (Reflex.morpheme b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.morpheme host marker) (Reflex.boundary edge) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.morpheme host marker) (Reflex.prominence host_1) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.boundary edge) (Reflex.displacement exponent) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.boundary edge) (Reflex.morpheme host marker) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.boundary a) (Reflex.boundary b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.boundary edge) (Reflex.prominence host) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.prominence host) (Reflex.displacement exponent) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.prominence host) (Reflex.morpheme host_1 marker) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.prominence host) (Reflex.boundary edge) = isFalse ⋯
• instDecidableEqReflex.decEq (Reflex.prominence a) (Reflex.prominence b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instDecidableEqReflex {C✝ : Type u_1} [DecidableEq C✝] : DecidableEq (Reflex C✝)

Equations

• instDecidableEqReflex = instDecidableEqReflex.decEq

def instReprReflex.repr {C✝ : Type u_1} [Repr C✝] : Reflex C✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprReflex {C✝ : Type u_1} [Repr C✝] : Repr (Reflex C✝)

Equations

• instReprReflex = { reprPrec := instReprReflex.repr }

def Reflex.Modality.channel : Modality → Channel

The channel a modality marks in.

Equations

• Reflex.Modality.displacement.channel = Reflex.Channel.syntactic
• Reflex.Modality.morpheme.channel = Reflex.Channel.morphological
• Reflex.Modality.boundary.channel = Reflex.Channel.phonological
• Reflex.Modality.prominence.channel = Reflex.Channel.phonological

def Reflex.modality {C : Type u_1} : Reflex C → Modality

The modality of a reflex.

Equations

• (Reflex.displacement exponent).modality = Reflex.Modality.displacement
• (Reflex.morpheme host marker).modality = Reflex.Modality.morpheme
• (Reflex.boundary edge).modality = Reflex.Modality.boundary
• (Reflex.prominence host).modality = Reflex.Modality.prominence

def Reflex.host {C : Type u_1} : Reflex C → C

The host constituent of a reflex.

Equations

• (Reflex.displacement exponent).host = exponent
• (Reflex.morpheme host marker).host = host
• (Reflex.boundary edge).host = edge
• (Reflex.prominence host).host = host

@[simp]

theorem Reflex.modality_displacement {C : Type u_1} (c : C) : (displacement c).modality = Modality.displacement

@[simp]

theorem Reflex.modality_morpheme {C : Type u_1} (c : C) (m : List Morphology.Morph) : (morpheme c m).modality = Modality.morpheme

@[simp]

theorem Reflex.modality_boundary {C : Type u_1} (c : C) : (boundary c).modality = Modality.boundary

@[simp]

theorem Reflex.modality_prominence {C : Type u_1} (c : C) : (prominence c).modality = Modality.prominence

@[simp]

theorem Reflex.host_displacement {C : Type u_1} (c : C) : (displacement c).host = c

@[simp]

theorem Reflex.host_morpheme {C : Type u_1} (c : C) (m : List Morphology.Morph) : (morpheme c m).host = c

@[simp]

theorem Reflex.host_boundary {C : Type u_1} (c : C) : (boundary c).host = c

@[simp]

theorem Reflex.host_prominence {C : Type u_1} (c : C) : (prominence c).host = c

def Reflex.IsOvert {C : Type u_1} : Reflex C → Prop

A morpheme reflex is coded by a nonempty marker; zero is never a reflex.

Equations

• (Reflex.morpheme host m).IsOvert = (m ≠ [])
• x✝.IsOvert = True

@[instance_reducible]

instance Reflex.instDecidableIsOvert {C : Type u_1} (ρ : Reflex C) : Decidable ρ.IsOvert

Equations

• (Reflex.morpheme host marker).instDecidableIsOvert = { decide := !decide (marker = []), reflects_decide := ⋯ }
• (Reflex.displacement exponent).instDecidableIsOvert = { decide := true, reflects_decide := ⋯ }
• (Reflex.boundary edge).instDecidableIsOvert = { decide := true, reflects_decide := ⋯ }
• (Reflex.prominence host).instDecidableIsOvert = { decide := true, reflects_decide := ⋯ }

Host–target containment

With constituents ordered by containment, [BE23] distinguish exact targeting, pied-piping (a host properly contains the target) and anti-pied-piping (a host is properly contained in the target, attested in over sixty languages).

def Reflex.ExactlyTargets {C : Type u_1} (s : Finset (Reflex C)) (target : C) : Prop

Every reflex is hosted by the designated constituent itself.

Equations

• Reflex.ExactlyTargets s target = ∀ ρ ∈ s, ρ.host = target

@[instance_reducible]

instance Reflex.instDecidableExactlyTargetsOfDecidableEq {C : Type u_1} (s : Finset (Reflex C)) (target : C) [DecidableEq C] : Decidable (ExactlyTargets s target)

Equations

• Reflex.instDecidableExactlyTargetsOfDecidableEq s target = { decide := decide (∀ a ∈ s.val.attach, (fun (x : Reflex C) (a : x ∈ s) => x.host = target) ↑a ⋯), reflects_decide := ⋯ }

theorem Reflex.ExactlyTargets.exactlyTargets_iff {C : Type u_1} {s : Finset (Reflex C)} {target host : C} (h : ExactlyTargets s host) (hs : s.Nonempty) : ExactlyTargets s target ↔ host = target

def Reflex.PiedPipes {C : Type u_1} (s : Finset (Reflex C)) (target : C) [Preorder C] : Prop

Some reflex is hosted by a constituent properly containing the target, which is Ross's pied-piping as [BE23] generalize it from movement to all marking morphosyntax.

Equations

• Reflex.PiedPipes s target = ∃ ρ ∈ s, target < ρ.host

def Reflex.AntiPiedPipes {C : Type u_1} (s : Finset (Reflex C)) (target : C) [Preorder C] : Prop

Some reflex is hosted by a proper subconstituent of the target, which is [BE23]'s anti-pied-piping.

Equations

• Reflex.AntiPiedPipes s target = ∃ ρ ∈ s, ρ.host < target

@[instance_reducible]

instance Reflex.instDecidablePiedPipesOfDecidableLT {C : Type u_1} (s : Finset (Reflex C)) (target : C) [Preorder C] [DecidableLT C] : Decidable (PiedPipes s target)

Equations

• Reflex.instDecidablePiedPipesOfDecidableLT s target = { decide := decide (∃ (a : Reflex C) (_ : a ∈ s), (fun (x : Reflex C) => target < x.host) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Reflex.instDecidableAntiPiedPipesOfDecidableLT {C : Type u_1} (s : Finset (Reflex C)) (target : C) [Preorder C] [DecidableLT C] : Decidable (AntiPiedPipes s target)

Equations

• Reflex.instDecidableAntiPiedPipesOfDecidableLT s target = { decide := decide (∃ (a : Reflex C) (_ : a ∈ s), (fun (x : Reflex C) => x.host < target) a), reflects_decide := ⋯ }

theorem Reflex.PiedPipes.not_exactlyTargets {C : Type u_1} {s : Finset (Reflex C)} {target : C} [Preorder C] (h : PiedPipes s target) : ¬ExactlyTargets s target

A pied-piping reflex set does not exactly target its designee.

theorem Reflex.AntiPiedPipes.not_exactlyTargets {C : Type u_1} {s : Finset (Reflex C)} {target : C} [Preorder C] (h : AntiPiedPipes s target) : ¬ExactlyTargets s target

An anti-pied-piping reflex set does not exactly target its designee.

theorem Reflex.ExactlyTargets.piedPipes_iff {C : Type u_1} {s : Finset (Reflex C)} {target host : C} [Preorder C] (h : ExactlyTargets s host) (hs : s.Nonempty) : PiedPipes s target ↔ target < host

A nonempty reflex set hosted throughout by host pied-pipes a target exactly when host properly contains it.

theorem Reflex.ExactlyTargets.antiPiedPipes_iff {C : Type u_1} {s : Finset (Reflex C)} {target host : C} [Preorder C] (h : ExactlyTargets s host) (hs : s.Nonempty) : AntiPiedPipes s target ↔ host < target

A nonempty reflex set hosted throughout by host anti-pied-pipes a target exactly when the target properly contains host.