Documentation

Linglib.Syntax.HPSG.Binding

HPSG Binding Theory (Principles A & B) in RSRL, with φ-agreement #

[PS94], [Ric00], [Mul24]

The relational, quantified HPSG binding principles in the RSRL substrate, exercising the rel/ex/all machinery of Description.lean. Following HPSG Binding Theory ([Mul24], Ch. 20): local o-command ("less oblique, same ARG-ST", the relation locO), o-bind (coindexed ∧ o-commands ∧ agrees in φ), Principle A (a locally o-commanded anaphor is locally o-bound), Principle B (a pronoun is locally o-free).

Coindexation is token identity of INDEX (pathEq). Binding additionally requires φ-agreement (GEND/NUM token-identical between binder and bindee) — so a coindexed but φ-clashing anaphor (John likes herself, gender; they like himself, number) is not bound and Principle A is violated. This is the model-theoretic counterpart of the neutral binding engine's Word.Agree check (Syntax/Binding/Basic), against which Studies/SagWasowBender2003 cross-checks.

ARG-ST is modeled via SUBJ/OBJ attributes and locO interpreted per model.

Signature: nom-obj hierarchy, INDEX, φ-features, and the o-command relation #

source
inductive HPSG.RSRL.Binding.BSort :
Type

Sorts: a sign, synsem objects with the nom-obj species (ana/ppro/npro), an atomic idx (referential index), and the φ-value hierarchies gender > {masc, fem} and number > {sing, plur}.

Instances For
    source
    @[implicit_reducible]
    instance HPSG.RSRL.Binding.instDecidableEqBSort :
    DecidableEq BSort
    Equations
    source
    @[implicit_reducible]
    instance HPSG.RSRL.Binding.instFintypeBSort :
    Fintype BSort
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def HPSG.RSRL.Binding.instReprBSort.repr :
    BSort → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance HPSG.RSRL.Binding.instReprBSort :
      Repr BSort
      Equations
      source
      inductive HPSG.RSRL.Binding.BAttr :
      Type

      Attributes: SUBJ/OBJ (a sign's arguments — a flattened ARG-ST), IDX (a synsem's referential index), and the φ-features GEND/NUM.

      Instances For
        source
        @[implicit_reducible]
        instance HPSG.RSRL.Binding.instDecidableEqBAttr :
        DecidableEq BAttr
        Equations
        source
        @[implicit_reducible]
        instance HPSG.RSRL.Binding.instFintypeBAttr :
        Fintype BAttr
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def HPSG.RSRL.Binding.instReprBAttr.repr :
        BAttr → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance HPSG.RSRL.Binding.instReprBAttr :
          Repr BAttr
          Equations
          source
          inductive HPSG.RSRL.Binding.BRel :
          Type

          One relation: local o-command, locO (arity 2).

          Instances For
            source
            @[implicit_reducible]
            instance HPSG.RSRL.Binding.instDecidableEqBRel :
            DecidableEq BRel
            Equations
            source
            @[implicit_reducible]
            instance HPSG.RSRL.Binding.instFintypeBRel :
            Fintype BRel
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def HPSG.RSRL.Binding.instReprBRel.repr :
            BRel → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[implicit_reducible]
              instance HPSG.RSRL.Binding.instReprBRel :
              Repr BRel
              Equations
              source
              def HPSG.RSRL.Binding.bCovers :
              BSort → BSort → Bool

              Direct subsumption ("covers"): the DAG edges. Nom-obj species cover synsem; gender/number values cover their φ root; sign/synsem/idx/gender/number cover top.

              Equations
              Instances For
                source
                def HPSG.RSRL.Binding.bRank :
                BSort → ℕ

                Specificity depth; every covers edge strictly increases it (giving antisymmetry).

                Equations
                Instances For
                  source
                  @[implicit_reducible]
                  instance HPSG.RSRL.Binding.instPartialOrderBSort :
                  PartialOrder BSort
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  @[implicit_reducible]
                  instance HPSG.RSRL.Binding.instDecidableLEBSort :
                  DecidableLE BSort
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  def HPSG.RSRL.Binding.bapprop :
                  BSort → BAttr → Option BSort

                  Appropriateness: a sign has SUBJ/OBJ synsems; every synsem species has an IDX, a GEND, and a NUM.

                  Equations
                  Instances For
                    source
                    @[reducible]
                    def HPSG.RSRL.Binding.bindingSig :
                    Signature BSort
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Principles A and B as descriptions #

                      Variable 0 is the bound synsem x; 1 is the candidate binder y.

                      source
                      def HPSG.RSRL.Binding.coindexed (x y : ℕ) :
                      Desc bindingSig

                      Coindexation of the entities at variables x and y: token identity of their INDEX.

                      Equations
                      Instances For
                        source
                        def HPSG.RSRL.Binding.agrees (x y : ℕ) :
                        Desc bindingSig

                        φ-agreement of x and y: token identity of their GEND and NUM (HPSG agreement as re-entrancy).

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def HPSG.RSRL.Binding.locallyOBinds (y x : ℕ) :
                          Desc bindingSig

                          y locally o-binds x: locO(y, x), coindexed, and agreeing in φ.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def HPSG.RSRL.Binding.principleA :
                            Desc bindingSig

                            Principle A: a locally o-commanded anaphor must be locally o-bound.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def HPSG.RSRL.Binding.principleB :
                              Desc bindingSig

                              Principle B: a personal pronoun must be locally o-free — no component locally o-binds it.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def HPSG.RSRL.Binding.bindingGrammar :
                                Grammar bindingSig

                                The binding fragment's grammar.

                                Equations
                                Instances For

                                  Worked models #

                                  One transitive-clause carrier and one builder clause; the binding configurations are instantiations differing in the object's sort, index, and φ-features. The subject is a masculine-singular npro indexed iSubj.

                                  source
                                  inductive HPSG.RSRL.Binding.BindEnt :
                                  Type

                                  Entities of a transitive clause: verb sign, subject, object, two indices, and the gender/number value objects (gMasc/gFem, nSing/nPlur).

                                  Instances For
                                    source
                                    @[implicit_reducible]
                                    instance HPSG.RSRL.Binding.instDecidableEqBindEnt :
                                    DecidableEq BindEnt
                                    Equations
                                    source
                                    @[implicit_reducible]
                                    instance HPSG.RSRL.Binding.instFintypeBindEnt :
                                    Fintype BindEnt
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    source
                                    @[implicit_reducible]
                                    instance HPSG.RSRL.Binding.instReprBindEnt :
                                    Repr BindEnt
                                    Equations
                                    source
                                    def HPSG.RSRL.Binding.instReprBindEnt.repr :
                                    BindEnt → ℕ → Std.Format
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      @[reducible]
                                      def HPSG.RSRL.Binding.clause (objSort : BSort) (objIdx objGend objNum : BindEnt) :
                                      Interpretation bindingSig

                                      A transitive clause "subj V obj": the subject is a masc-sing npro indexed iSubj and locally o-commands the object; the object has sort objSort, index objIdx, gender objGend, number objNum. Coindexation is objIdx = iSubj; agreement is objGend = gMasc ∧ objNum = nSing.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        @[implicit_reducible]
                                        instance HPSG.RSRL.Binding.instDecidablePredListUBSortClauseR (objSort : BSort) (objIdx objGend objNum : BindEnt) (ρ : bindingSig.Rel) :
                                        DecidablePred ((clause objSort objIdx objGend objNum).R ρ)
                                        Equations