Documentation

Studies.MarcolliLarson2025

Marcolli and Larson (2025): Theta Theory, Operads and Coloring #

This file runs the theta bud system of Syntax/Minimalist/Theta on the paper's worked examples. The ditransitive Brian gave the book to Mary, whose verb assigns agent, theme and goal with theme before goal, is derivable as a bare comb, satisfies the theta criterion, and once anchored in lexical items belongs to the language of unbalanced theta structures and realizes to its bare Merge structure. A movement landing site admits only the non-theta root. Siloni's parasitic assignment is a dual-receiver generator that the standard rules lack and the se marking adds.

Main statements #

References #

source
def MarcolliLarson2025.giveHier :
ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop

The example's internal theta hierarchy, in which theme outranks goal, per the ditransitive grid the paper builds for give.

Equations
Instances For
    source
    def MarcolliLarson2025.giveComb :
    Bud.Tree (Minimalist.Theta.Color Unit)

    The give comb, in which agent, theme and goal discharge one node at a time below the head leaf carrying the full giver grid.

    Equations
    Instances For
      source
      theorem MarcolliLarson2025.giveComb_derivable :
      (Minimalist.Theta.system giveHier).Derives (Bud.Tree.leaf Minimalist.Theta.Color.nontheta) giveComb

      The give comb is derivable in the complete theta bud system.

      source
      theorem MarcolliLarson2025.giveComb_thetaLocal :
      Bud.Tree.NodeLocal (Minimalist.Theta.ThetaLocal giveHier) giveComb
      source
      theorem MarcolliLarson2025.giveComb_criterion :
      Minimalist.Theta.SatisfiesCriterion giveComb
      source
      def MarcolliLarson2025.moveRule :
      Bud.Tree (Minimalist.Theta.Color Unit)

      A movement landing site over the residual agent grid.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MarcolliLarson2025.moveRule_mem :
        moveRule ∈ (Minimalist.Theta.system giveHier).rules
        source
        theorem MarcolliLarson2025.eq_nontheta_of_cherry_mem {c : Minimalist.Theta.Color Unit} (h : Bud.Tree.cherry c (Minimalist.Theta.Color.free (Minimalist.Theta.upGrid [ArgumentStructure.ThetaRole.agent])) Minimalist.Theta.Color.emptyTree ∈ (Minimalist.Theta.system giveHier).rules) :
        c = Minimalist.Theta.Color.nontheta

        Movement lands only in non-theta positions: above the residual agent grid and a landing site, the only root color the rules admit is the non-theta marker.

        A language-specific generator: parasitic assignment #

        [Sil12]'s syntactic reciprocalization assigns a retained internal role together with the external role to one argument, a last resort licensed by the se morphology. In the coloring model this is a dual-receiver generator: one argument receives two roles against a dual-giver residue, as in the ECM derivation where Jean ends with the matrix experiencer role and the embedded verb's retained agent role.

        source
        def MarcolliLarson2025.parasiticGen :
        Bud.Tree (Minimalist.Theta.Color Unit)

        Parasitic assignment as a generator, at which a dual-receiver argument discharges a dual-giver residue in one step.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MarcolliLarson2025.parasiticGen_notMem :
          parasiticGen ∉ (Minimalist.Theta.system giveHier).rules

          The standard theta bud system contains no parasitic generator: every generator discharges at most one role per argument.

          source
          def MarcolliLarson2025.seSystem :
          Bud.System (Minimalist.Theta.Color Unit)

          The se-marked grammar, the system extended by the parasitic generator.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem MarcolliLarson2025.parasiticGen_derivable :
            seSystem.Derives (Bud.Tree.leaf Minimalist.Theta.Color.nontheta) parasiticGen

            With the marking, the dual-role discharge is derivable: Jean ends with both the matrix experiencer role and the retained embedded agent role.

            source
            theorem MarcolliLarson2025.parasiticGen_not_derivable :
            ¬(Minimalist.Theta.system giveHier).Derives (Bud.Tree.leaf Minimalist.Theta.Color.nontheta) parasiticGen

            Without the marking, the dual-role configuration is underivable: the structure is movement-free and its root receives no role, so the sole-role invariant forbids the dual-receiver argument. The sole-role requirement of [Sil12]'s "I"-reading account.

            Realization #

            source
            theorem MarcolliLarson2025.giveComb_adjunct_derivable :
            (Minimalist.Theta.system giveHier).Derives (Bud.Tree.leaf Minimalist.Theta.Color.nontheta) (Bud.Tree.node Minimalist.Theta.Color.nontheta giveComb (Bud.Tree.leaf Minimalist.Theta.Color.nontheta))

            An adjunct attaches to the give comb by colored Merge, staying derivable.

            source
            def MarcolliLarson2025.anchoredGiveComb (brian gave theBook toMary : Minimalist.LexicalItem.Token) :
            Bud.Tree (Minimalist.Theta.Color Minimalist.LexicalItem.Token)

            The lexically anchored give comb.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem MarcolliLarson2025.anchoredGiveComb_mem_language (brian gave theBook toMary : Minimalist.LexicalItem.Token) :
              anchoredGiveComb brian gave theBook toMary ∈ (Minimalist.Theta.system giveHier).language

              The anchored give comb is an unbalanced theta structure: its root is initial, its leaves are lexical, and each vertex discharges one role of the verb's grid.

              source
              theorem MarcolliLarson2025.realize_anchoredGiveComb (brian gave theBook toMary : Minimalist.LexicalItem.Token) :
              Minimalist.Theta.realize (anchoredGiveComb brian gave theBook toMary) = some ((↑brian).merge ((↑theBook).merge ((↑toMary).merge ↑gave)))

              Pruning the colors realizes the anchored comb as the bare Merge structure of Brian gave the book to Mary.

              source
              theorem MarcolliLarson2025.realize_anchored_move_landing (brian gave theBook toMary : Minimalist.LexicalItem.Token) :
              Minimalist.Theta.realize (Bud.Tree.node Minimalist.Theta.Color.nontheta (anchoredGiveComb brian gave theBook toMary) (Bud.Tree.leaf Minimalist.Theta.Color.emptyTree)) = Minimalist.Theta.realize (anchoredGiveComb brian gave theBook toMary)

              A movement landing site above the anchored comb realizes to the same syntactic object.