Documentation

Linglib.Comparisons.FrameComposition

Frame Composition: Unification vs. Function Application #

@cite{pollard-sag-1994} @cite{loebner-2021}

linglib has multiple frame-like structures — ThematicFrame (neo-Davidsonian role bundles), HPSG Sign (typed feature structures), Frame2 (TTR records) — each with its own composition mechanism.

@cite{loebner-2021} claims these are all instances of D-frames, and that their composition should be understood as frame unification. This module makes the structural identity explicit and shows where unification and Montague FA make different predictions.

Key Comparisons #

ThematicFrame is a D-frame. Its fields (agent, patient, theme,...) are functional attributes mapping entities to event participation. The agent_unique axiom in ThematicAxioms is exactly Löbner's functional-attribute constraint: each event has at most one agent.

HPSG feature sharing is frame unification. The Head Feature Principle (HFP) requires the phrase's HEAD features to equal the head daughter's HEAD features — identity unification.

FA vs unification for compounds. Montague FA requires one daughter to be a function over the other's type. For N-N compounds ("plastic bag"), neither constituent is naturally "the function." Frame unification handles this directly: the modifier fills an attribute slot. Predicate Modification (PM) is a restricted form of unification — it conjoins two ⟨e,t⟩ predicates but cannot target a specific attribute the way unification does.

source
inductive Comparisons.FrameComposition.HeadAttr :
Type

HPSG head feature names as frame attributes.

Instances For
    source
    instance Comparisons.FrameComposition.instDecidableEqHeadAttr :
    DecidableEq HeadAttr
    Equations
    source
    def Comparisons.FrameComposition.instReprHeadAttr.repr :
    HeadAttr → Nat → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Comparisons.FrameComposition.instReprHeadAttr :
      Repr HeadAttr
      Equations
      source
      def Comparisons.FrameComposition.instBEqHeadAttr.beq :
      HeadAttr → HeadAttr → Bool
      Equations
      Instances For
        source
        instance Comparisons.FrameComposition.instBEqHeadAttr :
        BEq HeadAttr
        Equations
        source
        inductive Comparisons.FrameComposition.HeadVal :
        Type

        Head feature values as a sum type (heterogeneous → homogeneous).

        Instances For
          source
          def Comparisons.FrameComposition.instDecidableEqHeadVal.decEq (x✝ x✝¹ : HeadVal) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            instance Comparisons.FrameComposition.instDecidableEqHeadVal :
            DecidableEq HeadVal
            Equations
            source
            instance Comparisons.FrameComposition.instReprHeadVal :
            Repr HeadVal
            Equations
            source
            def Comparisons.FrameComposition.instReprHeadVal.repr :
            HeadVal → Nat → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Comparisons.FrameComposition.instBEqHeadVal.beq :
              HeadVal → HeadVal → Bool
              Equations
              Instances For
                source
                instance Comparisons.FrameComposition.instBEqHeadVal :
                BEq HeadVal
                Equations
                source
                def Comparisons.FrameComposition.headFeaturesToDFrame (hf : HPSG.HeadFeatures) :
                Semantics.TypeTheoretic.DFrame HeadAttr HeadVal

                Project HPSG HeadFeatures into a D-frame. Each feature becomes a functional attribute (exactly one value).

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Comparisons.FrameComposition.headFeatures_total (hf : HPSG.HeadFeatures) (a : HeadAttr) :
                  (headFeaturesToDFrame hf).get a ≠ none

                  All head feature attributes are defined (total frame).

                  source
                  theorem Comparisons.FrameComposition.hfp_is_trivial_unification (hf : HPSG.HeadFeatures) (a : HeadAttr) :
                  ((headFeaturesToDFrame hf).unify (headFeaturesToDFrame hf)).get a = (headFeaturesToDFrame hf).get a

                  The Head Feature Principle says the phrase's HEAD = the head daughter's HEAD. In frame terms: unifying a frame with itself is identity. This is trivially compatible — no conflict possible.

                  source
                  theorem Comparisons.FrameComposition.unification_targets_specific_attr :
                  Semantics.TypeTheoretic.plasticBag.get Semantics.TypeTheoretic.ArtifactAttr.material = some Semantics.TypeTheoretic.ArtifactVal.plastic ∧ Semantics.TypeTheoretic.plasticBag.get Semantics.TypeTheoretic.ArtifactAttr.shape = Semantics.TypeTheoretic.bagFrame.get Semantics.TypeTheoretic.ArtifactAttr.shape ∧ Semantics.TypeTheoretic.plasticBag.get Semantics.TypeTheoretic.ArtifactAttr.use = Semantics.TypeTheoretic.bagFrame.get Semantics.TypeTheoretic.ArtifactAttr.use

                  Frame unification explains which attribute a modifier fills.

                  PM would just conjoin "is a bag" ∧ "is plastic" — but it doesn't explain why MATERIAL (not SHAPE or USE) is the relevant dimension. Frame unification makes the semantic contribution of each constituent explicit: the modifier fills exactly the MATERIAL slot, leaving SHAPE and USE unchanged.

                  source
                  theorem Comparisons.FrameComposition.head_determines_reference :
                  Semantics.TypeTheoretic.plasticBag.central = Semantics.TypeTheoretic.bagFrame.central ∧ Semantics.TypeTheoretic.plasticBag.central ≠ Semantics.TypeTheoretic.plasticMod.central

                  Unification is order-sensitive on the central node: the head determines what the compound "refers to." "plastic bag" refers to a bag (not to plastic).

                  source
                  theorem Comparisons.FrameComposition.cross_categorial_sharing :
                  (∀ (a : Semantics.TypeTheoretic.PriceAttr), Semantics.TypeTheoretic.priceNoun.get a = Semantics.TypeTheoretic.cheapAdj.get a) ∧ Semantics.TypeTheoretic.priceNoun.central ≠ Semantics.TypeTheoretic.cheapAdj.central

                  Löbner's insight (§3.1.1): words from different syntactic categories (price N, cheap Adj, cost V) can share one conceptual frame, differing only in perspective (central node).

                  In Montague semantics, these three words are unrelated lambda terms (a relational noun, a modifier, a transitive verb) with no shared structure. In frame semantics, the shared structure is explicit and the type difference is derived from perspective.