Documentation

Linglib.Syntax.Minimalist.Probe.Profile

Probe profiles #

This file defines a probe's locality profile, the head that hosts it together with the category that terminates its search, its horizon. Keine labels a clause bilaterally, by the set of heads it projects, and a clause is transparent to a probe exactly when its label does not contain the horizon. Transparency is then antitone in the extension order of clause spines, which is Upward Entailment, and a probe whose horizon lies in the label of its own sister is vacuous, the premise of the Height–Locality Theorem. A profile denotes a Probe over any goal type that exposes a label; the tree-native counterpart of a horizon is SyntacticObject.behindHorizonIn.

Main definitions #

Main results #

References #

source
structure Minimalist.Probe.Profile :
Type

A probe's profile is the head that hosts it and the category that terminates its search, its horizon; a probe without horizon searches into any domain.

  • probeHead : Cat

    The head that hosts the probe.

  • horizon : Option Cat

    The category that terminates the probe's search, if any.

Instances For
    source
    def Minimalist.Probe.instDecidableEqProfile.decEq (x✝ x✝¹ : Profile) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Minimalist.Probe.instDecidableEqProfile :
      DecidableEq Profile
      Equations
      source
      def Minimalist.Probe.instReprProfile.repr :
      Profile → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance Minimalist.Probe.instReprProfile :
        Repr Profile
        Equations

        Transparency #

        source
        def Minimalist.Probe.Profile.TransparentTo (p : Profile) (L : Finset Cat) :
        Prop

        A domain with bilateral label L is transparent to p when p has no horizon or the label does not contain it.

        Equations
        Instances For
          source
          @[instance_reducible]
          instance Minimalist.Probe.Profile.instDecidableTransparentTo (p : Profile) {L : Finset Cat} :
          Decidable (p.TransparentTo L)
          Equations
          source
          @[simp]
          theorem Minimalist.Probe.Profile.transparentTo_mk_none (head : Cat) (L : Finset Cat) :
          { probeHead := head, horizon := none }.TransparentTo L
          source
          @[simp]
          theorem Minimalist.Probe.Profile.transparentTo_mk_some {L : Finset Cat} {head h : Cat} :
          { probeHead := head, horizon := some h }.TransparentTo L ↔ ¬h ∈ L
          source
          theorem Minimalist.Probe.Profile.TransparentTo.anti {p : Profile} {L₁ L₂ : Finset Cat} (h : L₁ ⊆ L₂) (hL : p.TransparentTo L₂) :
          p.TransparentTo L₁

          Upward Entailment. A label containing every head of a label opaque to p is opaque to p.

          source
          theorem Minimalist.Probe.Profile.transparentTo_label_antitone (p : Profile) :
          Antitone fun (s : ClauseSpine) => p.TransparentTo s.label

          Upward Entailment. Transparency is antitone in the extension order of clause spines, since a spine's label contains the horizon whenever a spine below it does.

          Vacuity #

          source
          def Minimalist.Probe.Profile.sisterLabel :
          Cat → Finset Cat

          The label of the sister of a head on the standard verbal spine, TP under C⁰, CP under Force⁰ and vP under T⁰.

          Equations
          Instances For
            source
            def Minimalist.Probe.Profile.IsVacuous (p : Profile) :
            Prop

            p is vacuous when its horizon lies in the label of its sister on the standard verbal spine, so that its search terminates at its sister and no domain remains. Vacuous probes trigger no dependency and are undetectable, which is what makes the Height–Locality Theorem emerge.

            Equations
            Instances For
              source
              @[instance_reducible]
              instance Minimalist.Probe.Profile.instDecidableIsVacuous (p : Profile) :
              Decidable p.IsVacuous
              Equations
              source
              @[simp]
              theorem Minimalist.Probe.Profile.not_isVacuous_mk_none (head : Cat) :
              ¬{ probeHead := head, horizon := none }.IsVacuous

              A probe without horizon is never vacuous.

              Denotation into the canonical Probe #

              source
              def Minimalist.Probe.Profile.toProbe (p : Profile) {α : Type u_1} (labelOf : α → Finset Cat) :
              Probe α

              The probe a profile denotes over goals exposing a label, which sees a goal iff the goal's label is transparent to it.

              Equations
              Instances For