Docs / Syntax / Minimalist / Label / RaisingHead

The raising head

import Linglib.Syntax.Minimalist.Label.RaisingHead · namespace Minimalist

Source

Marcolli, Chomsky and Berwick state labeling over a partial head function and require that function to be raising: the object Internal Merge forms is headed by the head of what it raised out of, so the landing site of a wh-phrase beside a C is headed by C. The raising head reads this off the finished object from the selection head, a lower copy satisfying selection as the phrase it copies and otherwise invisible (CopyState): where two phrases merge and the head of one has a lower copy inside the other, the first has raised out of the second, which projects. A planar embedding is a total head function extending it, and the head function HeadFunction.raising takes the daughter carrying the raising head, and the embedding's head where there is none.

Main definitions

Main results

Implementation notes

  • The drawing convention puts specifiers to the left of their heads and heads to the left of their complements: a left leaf that selects nothing is a specifier and the right daughter heads, a left leaf that selects is the head, and otherwise the right daughter heads. It decides only where the raising head is undefined, at a phrase merged in place beside another phrase, which the labeling algorithm leaves unlabeled until one of the two moves on (HeadFunction.label).
  • The raising head also delimits the phases of Locality/Phase.lean.

TODO

  • The trace of a token is the lower copy of the phrase the token heads; a moved head, whose lower copy would still select, is not distinguished.
  • The positions at or below the maximal projection of a head occurring once carry exactly the terms within its projection, where the raising head is defined along the projection line.

References

Declarations

A constituent's copy state is its selection state, or a lower copy of the phrase a token heads, which satisfies selection as that phrase and is otherwise invisible to the raising algorithm.

inductive CopyStateL64–72
:
Type

Derives DecidableEq.

Used by CopyState.instZero, CopyState.instMul, CopyState.instCommMagma, CopyState.instMulZeroClass, CopyState.head, CopyState.mul_self, CopyState.instHead, RaisingState, RaisingState.raise

L78–85

The raising head

The raising state of a constituent pairs its copy state with the tokens whose lower copies it contains.

structure RaisingStateL146–153
:
Type
  • state : CopyState

    The copy state.

  • copies : Multiset LexicalItem.Token

    The tokens heading the phrases of which the constituent contains a lower copy.

Derives DecidableEq.

Built from

Used by RaisingState.instZero, RaisingState.raise, RaisingState.instMul, RaisingState.mul_def, RaisingState.raise_comm, RaisingState.instCommMagma, RaisingState.instHead, raisingTraceState, SyntacticObject.raisingCheck, SyntacticObject.raisingCheckHom

The raising head of a syntactic object, Marcolli et al. 2025's raising head function: the selection head where there is one, and at a landing site the head of the phrase moved out of.

def SyntacticObject.raisingHeadL219–222
(s : SyntacticObject) :
Option LexicalItem.Token

Built from ,

Used by SyntacticObject.raisingHead_merge, SyntacticObject.raisingHead_merge_self, treeRaisingHead_subtree

Used in Syntax/Minimalist/Locality/Phase

Head daughters

L258–268

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

theorem exists_headIndex?_of_treeRaisingHeadL281–299
{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 ℓ

Built from ,