Documentation

Linglib.Syntax.Minimalist.SyntacticObject.Position

Positions of planar syntactic objects #

The positions of a planar syntactic object, the paths to its vertices, form a rooted tree (RoseTree.Positions). Each carries a term, the subtree there read as a syntactic object: the terms at the covers of a position are the terms its term immediately contains, and the terms at the positions below it are the terms its term contains, so c-command by a term occurring once is c-command from its position. Each position also has a head daughter, the daughter carrying its raising head, and where the raising head is undefined the daughter the drawing convention of the embedding makes the head: [MCB25] (Lemma 1.13.5) identify a planar embedding with a total head function, which extends the raising head.

Main definitions #

Main statements #

Implementation notes #

TODO #

References #

Terms at positions #

source
theorem Minimalist.PlanarSyntacticObject.isSyntacticObject_subtree {t : PlanarSyntacticObject} (p : (↑t).Positions) :
IsSyntacticObject (UnorderedTree.mk p.subtree)
source
def Minimalist.PlanarSyntacticObject.termAt (t : PlanarSyntacticObject) (p : (↑t).Positions) :
SyntacticObject

The term of t at a position.

Equations
Instances For
    source
    @[simp]
    theorem Minimalist.PlanarSyntacticObject.termAt_bot {t : PlanarSyntacticObject} :
    t.termAt ⊥ = ↑t
    source
    theorem Minimalist.PlanarSyntacticObject.immediatelyContains_termAt {t : PlanarSyntacticObject} {p : (↑t).Positions} {y : SyntacticObject} :
    (t.termAt p).ImmediatelyContains y ↔ ∃ (q : (↑t).Positions), p ⋖ q ∧ t.termAt q = y

    The term at a position immediately contains the terms at its covers.

    source
    theorem Minimalist.PlanarSyntacticObject.containsOrEq_termAt {t : PlanarSyntacticObject} {p : (↑t).Positions} {y : SyntacticObject} :
    (t.termAt p).ContainsOrEq y ↔ ∃ (q : (↑t).Positions), p ≤ q ∧ t.termAt q = y

    The term at a position contains or equals the terms at the positions below it.

    source
    theorem Minimalist.PlanarSyntacticObject.mem_terms_iff {t : PlanarSyntacticObject} {y : SyntacticObject} :
    y ∈ (↑t).terms ↔ ∃ (q : (↑t).Positions), t.termAt q = y

    The terms of a planar object are the terms at its positions.

    source
    theorem Minimalist.PlanarSyntacticObject.isBranchingAt_parent {t : PlanarSyntacticObject} {a : (↑t).Positions} (ha : a ≠ ⊥) :
    (↑t).IsBranchingAt (↑a).parent

    In a syntactic object the parent of a position other than the root branches.

    source
    theorem Minimalist.PlanarSyntacticObject.exists_cCommands_termAt_of_cCommands {t : PlanarSyntacticObject} {y x : SyntacticObject} (h : (↑t).CCommands x y) :
    ∃ (p : (↑t).Positions) (q : (↑t).Positions), (↑t).CCommands ↑p ↑q ∧ t.termAt p = x ∧ t.termAt q = y

    C-command between terms is witnessed by c-command between occurrences of them, with no condition on how often they occur.

    source
    theorem Minimalist.PlanarSyntacticObject.cCommands_termAt_of_cCommands {t : PlanarSyntacticObject} {p q : (↑t).Positions} (hs : ∀ (d : (↑t).Positions), Order.pred p ⋖ d → d ≠ p → t.termAt d ≠ t.termAt p) (h : (↑t).CCommands ↑p ↑q) :
    (↑t).CCommands (t.termAt p) (t.termAt q)

    C-command between occurrences is c-command between their terms when the commander's term differs from those of its sisters, [CS16b]'s Theorem 3; their Merge applies only to distinct objects, which secures the condition.

    source
    theorem Minimalist.PlanarSyntacticObject.cCommands_termAt_iff {t : PlanarSyntacticObject} {a : (↑t).Positions} {x : SyntacticObject} (hu : ∀ (q : (↑t).Positions), t.termAt q = t.termAt a → q = a) :
    (↑t).CCommands (t.termAt a) x ↔ ∃ (q : (↑t).Positions), (↑t).CCommands ↑a ↑q ∧ t.termAt q = x

    C-command by a term occurring only at a is c-command from a.

    source
    theorem Minimalist.PlanarSyntacticObject.eq_termAt_pred_of_immediatelyContains {t : PlanarSyntacticObject} {a : (↑t).Positions} (hu : ∀ (q : (↑t).Positions), t.termAt q = t.termAt a → q = a) {m : SyntacticObject} (hm : m ∈ (↑t).terms) (h : m.ImmediatelyContains (t.termAt a)) :
    m = t.termAt (Order.pred a)

    A term immediately containing the term at a, which occurs only there, is the term at its parent.

    Head daughters #

    source
    def Minimalist.treeRaisingHead (s : RoseTree SyntacticObject.Vertex) :
    Option LexicalItem.Token

    The raising head of a planar tree, that of its unordered image.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Minimalist.treeRaisingHead_subtree {t : PlanarSyntacticObject} (p : (↑t).Positions) :
      treeRaisingHead p.subtree = (t.termAt p).raisingHead
      source
      def Minimalist.conventionHeadPos? :
      RoseTree SyntacticObject.Vertex → Option (List ℕ)

      The drawing convention makes a token or trace leaf its own head; at a binary node it takes a left leaf that selects nothing for a specifier and looks for the head in the right daughter, takes a left leaf that selects for the head, and otherwise looks in the right daughter. This is the head path it assigns.

      Equations
      Instances For
        source
        def Minimalist.headIndex? (s : RoseTree SyntacticObject.Vertex) :
        Option ℕ

        The head daughter of a planar tree is the first daughter carrying its raising head, and where it has none, the first step of the drawing convention's head path.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Minimalist.exists_headIndex?_of_treeRaisingHead {s : RoseTree SyntacticObject.Vertex} {ℓ : LexicalItem.Token} (hs : IsSyntacticObject (UnorderedTree.mk s)) (hc : s.children ≠ []) (h : treeRaisingHead s = some ℓ) :
          ∃ (i : ℕ) (c : RoseTree SyntacticObject.Vertex), headIndex? s = some i ∧ s.children[i]? = some c ∧ treeRaisingHead c = some ℓ

          Where a planar syntactic object with daughters has a raising head, its head daughter carries it.