Documentation

Linglib.Semantics.Focus.Realization

Focus realization #

What a grammar overtly does to mark a focus: a Realization pairs the focus constituent with the list of grammatical Reflexes marking it — a displaced exponent, a dedicated morpheme, a phrase-edge, or a metrical prominence — the demarcative vs culminative cut kept visible in the type. Overtness is derived (IsOvert: the reflex list is nonempty), not flagged; strategy labels are shape classifications over reflexes; and multi-channel marking (Hausa ex-situ focus: displacement + Relative morphology + stabilizer) is a multi-element list. Consumed by [HZ07] (Hausa) and [HZ04] (Tangale), whose systems each refute EveryFocusPerceptible — the universalist claim that every focus receives an overt reflex.

Implementation notes #

String-vacuous operations (Hausa subject fronting) contribute no reflex: the reflex list carries only perceptible material, which is what makes IsOvert honest. Host-vs-focus tightness relations (and the overlap-weakening of [HZ07]'s Ex-Situ Generalisation) are deferred until pied-piping data land; note Mereology.Overlap is vacuous over orders with a bottom, so that member must use ¬ Disjoint or bot-free carriers.

source
inductive Semantics.Focus.Reflex (C : Type u_2) :
Type u_2

A single overt reflex of focus marking.

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

    An exponent constituent surfaces displaced from its base position (movement that is not string-vacuous).

  • morpheme {C : Type u_2} (host : C) : Reflex C

    A dedicated morpheme — affix, particle, or form alternation — at a host constituent.

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

    A demarcative prosodic event: a phrase-edge at a host constituent (the Tangale/Chadic pattern).

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

    A culminative prosodic event: metrical prominence on a host (the English pattern).

Instances For
    source
    def Semantics.Focus.instDecidableEqReflex.decEq {C✝ : Type u_2} [DecidableEq C✝] (x✝ x✝¹ : Reflex C✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Focus.instDecidableEqReflex {C✝ : Type u_2} [DecidableEq C✝] :
      DecidableEq (Reflex C✝)
      Equations
      source
      @[implicit_reducible]
      instance Semantics.Focus.instReprReflex {C✝ : Type u_2} [Repr C✝] :
      Repr (Reflex C✝)
      Equations
      source
      def Semantics.Focus.instReprReflex.repr {C✝ : Type u_2} [Repr C✝] :
      Reflex C✝ → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        structure Semantics.Focus.Realization (C : Type u_2) :
        Type u_2

        A focus realization: the focus constituent and the grammatical reflexes marking it.

        • focus : C
        • reflexes : List (Reflex C)
        Instances For
          source
          def Semantics.Focus.instReprRealization.repr {C✝ : Type u_2} [Repr C✝] :
          Realization C✝ → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[implicit_reducible]
            instance Semantics.Focus.instReprRealization {C✝ : Type u_2} [Repr C✝] :
            Repr (Realization C✝)
            Equations
            source
            def Semantics.Focus.Realization.IsOvert {C : Type u_1} (r : Realization C) :
            Prop

            Overt marking, derived: some reflex surfaces.

            Equations
            Instances For
              source
              @[implicit_reducible]
              instance Semantics.Focus.instDecidableIsOvert {C : Type u_1} (r : Realization C) :
              Decidable r.IsOvert
              Equations
              source
              def Semantics.Focus.EveryFocusPerceptible {C : Type u_1} {I : Type u_2} (realize : I → Realization C) :
              Prop

              The universalist claim over a marking system realize: every focus receives an overt reflex. Hausa and Tangale each refute their instance.

              Equations
              Instances For