Documentation

Linglib.Syntax.HPSG.Construction

The construct hierarchy of Sign-Based Construction Grammar in RSRL #

A construct pairs a mother sign with daughter signs, and a construction is a constraint on the constructs of one sort. Construct sorts are classified by how they are headed and by the kind of clause they form. A sort below one sort of each dimension inherits the constraints on both, since a constraint on a sort holds of every entity below it. This file states in RSRL the fragment of Sign-Based Construction Grammar with which Sag analyses the English filler-gap clauses.

The headed construction gives the mother the category of its head daughter. The filler-head construction identifies the filler daughter with the first sign on the head daughter's GAP list and passes the rest of the list to the mother. Each filler-gap clause adds constraints on the categories of its daughters and on the inversion, independence and verb form of its head, the clause types fix the semantic type and verb form of the mother, and the topicalized, wh-exclamative and the-clause constructions give the head daughter exactly one gap. The principle memberDef defines list membership, uniquely on lists without cycles.

Main definitions #

Main results #

Implementation notes #

As in Sag's grammars, a GAP list contains signs. Signs are overt or covert, only overt signs are daughters of constructs, and a word leaves a covert sign of sort gap on its GAP list for an argument that it does not realize. The features of SYN and the index of SEM are attributes of the sign itself. The filler-head construction identifies the SYN value of the filler with that of the gap except for WH and REL, which are not in the signature, so the filler and the gap share their CAT and GAP values, and, in Sag's synopsis of the framework, their index. Daughters are attributes named by their role rather than members of a DTRS list. As in Sag's signature, a verbal category has a verb form and an independence value and a verb an inversion value; of the features he declares, only those that the constructions here mention are in the signature, so WH, REL, VAL, SELECT, AUX and STORE are not, and the semantic type of the mother stands in for its meaning. Sag places the topicalized clause below the filler-head construct alone and gives its head daughter an austinean meaning, which the mother's meaning inherits; here the mother's type is stated.

The aux-initial construction is stated in Studies/SagEtAl2020 and the coordinate construction in Studies/SagWasowBender2003. The worked constructs are in Studies/Sag2010, which checks the paper's judgments against the grammar and derives the island status of the five clauses.

References #

Sorts #

source
inductive HPSG.Construction.Srt :
Type

The sorts of the fragment.

Instances For
    source
    @[instance_reducible]
    instance HPSG.Construction.instDecidableEqSrt :
    DecidableEq Srt
    Equations
    source
    @[instance_reducible]
    instance HPSG.Construction.instFintypeSrt :
    Fintype Srt
    Equations
    source
    @[instance_reducible]
    instance HPSG.Construction.instReprSrt :
    Repr Srt
    Equations
    source
    def HPSG.Construction.instReprSrt.repr :
    Srt → ℕ → Std.Format
    Equations
    Instances For
      source
      def HPSG.Construction.Srt.parents :
      Srt → List Srt

      The immediate supersorts of a sort. Each filler-gap clause other than the topicalized clause and each aux-initial clause has two, a headed construct and a clause type.

      Equations
      Instances For
        source
        def HPSG.Construction.Srt.rank :
        Srt → ℕ

        The length of the longest chain from a sort up to top.

        Equations
        Instances For
          source
          theorem HPSG.Construction.Srt.rank_lt_of_mem_parents (σ τ : Srt) :
          τ ∈ σ.parents → τ.rank < σ.rank

          Every immediate supersort of a sort has a lower rank.

          source
          @[instance_reducible]
          instance HPSG.Construction.instPartialOrderSrt :
          PartialOrder Srt
          Equations
          source
          @[instance_reducible]
          instance HPSG.Construction.instDecidableLESrt :
          DecidableLE Srt
          Equations
          • One or more equations did not get rendered due to their size.

          Attributes and the signature #

          source
          inductive HPSG.Construction.Attr :
          Type

          The attributes. A construct has a mother and daughters. A sign has a category, a GAP list, a semantic type and an index. A verbal category has a verb form and is independent or not, and a verb is inverted or not. A nonempty list has a first element and a rest.

          Instances For
            source
            @[instance_reducible]
            instance HPSG.Construction.instDecidableEqAttr :
            DecidableEq Attr
            Equations
            source
            @[instance_reducible]
            instance HPSG.Construction.instFintypeAttr :
            Fintype Attr
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def HPSG.Construction.instReprAttr.repr :
            Attr → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance HPSG.Construction.instReprAttr :
              Repr Attr
              Equations
              source
              def HPSG.Construction.Attr.decl :
              Attr → List (Srt × Srt)

              The sorts that introduce each attribute, with its value sort there. The mother of a phrasal construct and its daughters are overt, and a list contains signs.

              Equations
              Instances For
                source
                inductive HPSG.Construction.Rel :
                Type

                The one relation symbol is list membership.

                Instances For
                  source
                  @[instance_reducible]
                  instance HPSG.Construction.instDecidableEqRel :
                  DecidableEq Rel
                  Equations
                  source
                  @[instance_reducible]
                  instance HPSG.Construction.instFintypeRel :
                  Fintype Rel
                  Equations
                  source
                  @[instance_reducible]
                  instance HPSG.Construction.instReprRel :
                  Repr Rel
                  Equations
                  source
                  def HPSG.Construction.instReprRel.repr :
                  Rel → ℕ → Std.Format
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[reducible]
                    def HPSG.Construction.sig :
                    RSRL.Signature Srt

                    The signature of the fragment.

                    Equations
                    Instances For
                      source
                      def HPSG.Construction.noRel {U : Type u_1} (ρ : sig.Rel) :
                      Set (Fin (sig.arity ρ) → U)

                      The interpretation of member that holds of nothing, for models whose principles do not mention the relation.

                      Equations
                      Instances For
                        source
                        @[instance_reducible]
                        instance HPSG.Construction.instDecidablePredForallFinAritySrtSigNoRel {U : Type u_1} (ρ : sig.Rel) :
                        DecidablePred (noRel ρ)
                        Equations

                        Constructions #

                        source
                        def HPSG.Construction.headedPrinciple :
                        RSRL.Constraint sig

                        The headed construction of [Sag10]: the mother of a headed construct has the category of its head daughter.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def HPSG.Construction.fillerHeadPrinciple :
                          RSRL.Constraint sig

                          The filler-head construction ([Sag10] (58), [Sag12] (141)). The head daughter is verbal. The filler daughter shares its category, its GAP list and its index with the first sign on the head daughter's GAP list, and the mother's GAP list is the rest of the head daughter's.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def HPSG.Construction.corePrinciple :
                            RSRL.Constraint sig

                            The core clause construction of [Sag10]: the mother of a core clause is finite or infinitival.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def HPSG.Construction.declarativePrinciple :
                              RSRL.Constraint sig

                              The mother of a declarative clause has an austinean semantic type.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def HPSG.Construction.interrogativePrinciple :
                                RSRL.Constraint sig

                                The mother of an interrogative clause denotes a question.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  def HPSG.Construction.exclamativePrinciple :
                                  RSRL.Constraint sig

                                  The mother of an exclamative clause denotes a fact.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    def HPSG.Construction.relativePrinciple :
                                    RSRL.Constraint sig

                                    The relative construction ([Sag10] (91)): the mother of a relative clause is neither inverted nor independent.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      def HPSG.Construction.topPrinciple :
                                      RSRL.Constraint sig

                                      The topicalization construction ([Sag10] (61)). The filler daughter is nonverbal. The head daughter is an uninverted, independent, finite projection of a verb, which excludes the complementizer-headed clause that a the-clause allows, and it has exactly one gap. The mother is austinean.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        def HPSG.Construction.whExclPrinciple :
                                        RSRL.Constraint sig

                                        The wh-exclamative construction ([Sag10] (70)). The filler daughter is nonverbal, and the head daughter is uninverted and finite and has exactly one gap.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          def HPSG.Construction.nsWhIntPrinciple :
                                          RSRL.Constraint sig

                                          The nonsubject wh-interrogative construction ([Sag10] (80)). The filler daughter is nonverbal, and the head daughter is inverted exactly when it is independent.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            def HPSG.Construction.whRelPrinciple :
                                            RSRL.Constraint sig

                                            The wh-relative construction ([Sag10] (90)) gives the mother the semantic type of a modifier.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              def HPSG.Construction.finWhRelPrinciple :
                                              RSRL.Constraint sig

                                              The finite wh-relative construction ([Sag10] (92)). The mother is finite and the filler daughter nominal, a noun phrase or a prepositional phrase.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                source
                                                def HPSG.Construction.infWhRelPrinciple :
                                                RSRL.Constraint sig

                                                The infinitival wh-relative construction of [Sag10]. The filler daughter is a prepositional phrase and the head daughter is infinitival.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  def HPSG.Construction.thePrinciple :
                                                  RSRL.Constraint sig

                                                  The the-clause construction ([Sag10] (108)). The filler daughter is nonverbal, and the head daughter is finite and has exactly one gap.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    source
                                                    def HPSG.Construction.constraints :
                                                    List (RSRL.Constraint sig)

                                                    The constructions of the fragment.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      source
                                                      def HPSG.Construction.grammar :
                                                      RSRL.Grammar sig

                                                      The grammar of the fragment.

                                                      Equations
                                                      Instances For
                                                        source
                                                        theorem HPSG.Construction.freeVars_grammar (d : RSRL.Desc sig) :
                                                        d ∈ grammar → d.freeVars = ∅

                                                        Every principle of the grammar is closed, so its satisfaction does not depend on the variable assignment.

                                                        Inheritance #

                                                        source
                                                        theorem HPSG.Construction.map_sort_inherited_fillerGap :
                                                        List.map (fun (x : RSRL.Constraint sig) => x.sort) (RSRL.Constraint.inherited constraints Srt.topCl) = [Srt.headedCxt, Srt.fillerHeadCxt, Srt.topCl] ∧ List.map (fun (x : RSRL.Constraint sig) => x.sort) (RSRL.Constraint.inherited constraints Srt.whExclCl) = [Srt.headedCxt, Srt.fillerHeadCxt, Srt.coreCl, Srt.exclamativeCl, Srt.whExclCl] ∧ List.map (fun (x : RSRL.Constraint sig) => x.sort) (RSRL.Constraint.inherited constraints Srt.nsWhIntCl) = [Srt.headedCxt, Srt.fillerHeadCxt, Srt.coreCl, Srt.interrogativeCl, Srt.nsWhIntCl] ∧ List.map (fun (x : RSRL.Constraint sig) => x.sort) (RSRL.Constraint.inherited constraints Srt.finWhRelCl) = [Srt.headedCxt, Srt.fillerHeadCxt, Srt.relativeCl, Srt.whRelCl, Srt.finWhRelCl] ∧ List.map (fun (x : RSRL.Constraint sig) => x.sort) (RSRL.Constraint.inherited constraints Srt.infWhRelCl) = [Srt.headedCxt, Srt.fillerHeadCxt, Srt.relativeCl, Srt.whRelCl, Srt.infWhRelCl] ∧ List.map (fun (x : RSRL.Constraint sig) => x.sort) (RSRL.Constraint.inherited constraints Srt.theCl) = [Srt.headedCxt, Srt.fillerHeadCxt, Srt.coreCl, Srt.declarativeCl, Srt.theCl]

                                                        Each filler-gap clause inherits the headed and filler-head constructions and the constructions on the clause types above it, and has a construction of its own. A finite wh-relative inherits five constructions.

                                                        source
                                                        theorem HPSG.Construction.satisfies_body {U : Type u_1} {I : RSRL.Interpretation sig U} {u : U} (hI : I.Models grammar) {c : RSRL.Constraint sig} (hc : c ∈ constraints) (hu : I.S u ≤ c.sort) :
                                                        I.Satisfies (fun (x : ℕ) => u) u c.body

                                                        In a model of the grammar, every entity satisfies each construction on a sort above its own.

                                                        source
                                                        theorem HPSG.Construction.forall_satisfies_grammar_iff_of_nsWhIntCl {U : Type u_1} {I : RSRL.Interpretation sig U} {g : ℕ → U} {u : U} (hu : I.S u = Srt.nsWhIntCl) :
                                                        (∀ d ∈ grammar, I.Satisfies g u d) ↔ ∀ c ∈ [headedPrinciple, fillerHeadPrinciple, corePrinciple, interrogativePrinciple, nsWhIntPrinciple], I.Satisfies g u c.body

                                                        An entity of the nonsubject wh-interrogative sort satisfies the grammar exactly when it satisfies the headed, filler-head, core clause, interrogative and nonsubject wh-interrogative constructions. Only the last is stated on its sort.

                                                        source
                                                        theorem HPSG.Construction.satisfies_mtrGap_iff {U : Type u_1} {I : RSRL.Interpretation sig U} {u : U} (hI : I.Models grammar) (hu : I.S u ≤ Srt.fillerHeadCxt) (σ : Srt) :
                                                        I.Satisfies (fun (x : ℕ) => u) u (RSRL.Desc.sortAssign (RSRL.Term.path [Attr.MTR, Attr.GAP]) σ) ↔ I.Satisfies (fun (x : ℕ) => u) u (RSRL.Desc.sortAssign (RSRL.Term.path [Attr.HDDTR, Attr.GAP, Attr.REST]) σ)

                                                        In a model of the grammar, the mother of a filler-head construct has a GAP list of sort σ exactly when the rest of its head daughter's list does, since the filler discharges the first gap and the rest passes up. The mother's list is therefore empty exactly when the head daughter has one gap.

                                                        source
                                                        theorem HPSG.Construction.satisfies_hdCat_iff {U : Type u_1} {I : RSRL.Interpretation sig U} {u : U} (hI : I.Models grammar) (hu : I.S u ≤ Srt.headedCxt) (p : RSRL.Path sig) (σ : Srt) :
                                                        I.Satisfies (fun (x : ℕ) => u) u (RSRL.Desc.sortAssign (RSRL.Term.path (Attr.MTR :: Attr.CAT :: p)) σ) ↔ I.Satisfies (fun (x : ℕ) => u) u (RSRL.Desc.sortAssign (RSRL.Term.path (Attr.HDDTR :: Attr.CAT :: p)) σ)

                                                        In a model of the grammar, the mother and the head daughter of a headed construct share their category, so a feature of the mother's category has the same value on the head's.

                                                        source
                                                        theorem HPSG.Construction.satisfies_le_of_mem_termDenot {U : Type u_1} {I : RSRL.Interpretation sig U} {g : ℕ → U} {u : U} (hI : I.IsWellTyped) {p : RSRL.Path sig} {α : Attr} {σ : Srt} (hσ : ∀ d ∈ α.decl, d.1 ≤ σ) {v : U} (hv : v ∈ I.termDenot g (RSRL.Term.path (p ++ [α])) u) :
                                                        I.Satisfies g u (RSRL.Desc.sortAssign (RSRL.Term.path p) σ)

                                                        In a well-typed interpretation, an entity on which an attribute is defined has a sort below one that introduces the attribute. A category with an inversion value is therefore a verb.

                                                        source
                                                        theorem HPSG.Construction.not_le_covertExpr {U : Type u_1} {I : RSRL.Interpretation sig U} {u : U} (hI : I.IsWellTyped) {α : sig.Attr} (hα : α ∈ [Attr.MTR, Attr.HDDTR, Attr.FILLERDTR, Attr.CONJ1, Attr.CONJ2]) {v : U} (hv : I.A α u = some v) :
                                                        ¬I.S v ≤ Srt.covertExpr

                                                        No daughter or mother of a construct is covert in a well-typed interpretation, since the signs of a phrasal construct are overt expressions [Sag12]. A gap, which stands on a GAP list for an unrealized argument, is therefore never a daughter.

                                                        The GAP list as a set #

                                                        The filler-head construction discharges the first sign on the GAP list. The relation member, which memberDef defines, lets a principle speak of any element instead.

                                                        source
                                                        def HPSG.Construction.ListMem {U : Type u_1} (I : RSRL.Interpretation sig U) (x l : U) :
                                                        Prop

                                                        The entity x is an element of the list l when some cell that REST reaches from l has x as its first element.

                                                        Equations
                                                        Instances For
                                                          source
                                                          @[instance_reducible]
                                                          instance HPSG.Construction.instDecidableListMemOfFintypeOfDecidableEq {U : Type u_1} {I : RSRL.Interpretation sig U} [Fintype U] [DecidableEq U] (x l : U) :
                                                          Decidable (ListMem I x l)
                                                          Equations
                                                          source
                                                          theorem HPSG.Construction.listMem_iff {U : Type u_1} {I : RSRL.Interpretation sig U} {x l : U} :
                                                          ListMem I x l ↔ I.A Attr.FIRST l = some x ∨ ∃ (y : U), I.A Attr.REST l = some y ∧ ListMem I x y

                                                          An element of a list is the first element or an element of the rest.

                                                          source
                                                          def HPSG.Construction.memberDef :
                                                          RSRL.Desc sig

                                                          The principle that defines member. The entity x is a member of L exactly when L is a nonempty list and x is its first element or a member of its rest. The rest reaches the relation through the bound variable 2, since a relation symbol applies to variables.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            source
                                                            theorem HPSG.Construction.satisfies_memberDef_iff {U : Type u_1} {I : RSRL.Interpretation sig U} {g : ℕ → U} {u : U} :
                                                            I.Satisfies g u memberDef ↔ ∀ (x : U), I.IsComponentOf u x → ∀ (l : U), I.IsComponentOf u l → (I.R Rel.member ![x, l] ↔ I.S l ≤ Srt.nelist ∧ (I.A Attr.FIRST l = some x ∨ ∃ (y : U), I.A Attr.REST l = some y ∧ I.R Rel.member ![x, y]))

                                                            An entity satisfies memberDef when member relates two of its components exactly as the principle says, the rest of a list being a component wherever the list is.

                                                            source
                                                            theorem HPSG.Construction.models_memberDef_of_forall {U : Type u_1} {I : RSRL.Interpretation sig U} (hI : I.IsWellTyped) (h : ∀ (u x l : U), I.IsComponentOf u x → I.IsComponentOf u l → (I.R Rel.member ![x, l] ↔ ListMem I x l)) :
                                                            I.Models [memberDef]

                                                            A well-typed interpretation models memberDef when member holds of two components of an entity just when the first is an element of the second.

                                                            source
                                                            theorem HPSG.Construction.models_memberDef_iff {U : Type u_1} {I : RSRL.Interpretation sig U} (hI : I.IsWellTyped) (hwf : WellFounded fun (b a : U) => I.A Attr.REST a = some b) :
                                                            I.Models [memberDef] ↔ ∀ (u x l : U), I.IsComponentOf u x → I.IsComponentOf u l → (I.R Rel.member ![x, l] ↔ ListMem I x l)

                                                            On lists without cycles the principle memberDef defines list membership. A well-typed interpretation models it exactly when member holds of two components of an entity just when the first is an element of the second.