Docs / Syntax / Minimalist / Label / MinimalSearch

Labeling by minimal search

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

Source

The labeling algorithm is minimal search from a syntactic object for the heads it contains: a head merged with a phrase labels the result, and two phrases leave a head of each, which label only by a feature they agree in. Search sees the terms every occurrence of which lies inside an occurrence of the object, so the lower copy of a phrase that has moved on is invisible to it.

Main definitions

Main results

Implementation notes

  • Search runs on the tree, not on the daughters' labels, so a phrase with a specifier contributes the specifier's heads too. Copies of one head count once, and tokens are fresh, as chain reduction takes them, so repetitions are never identified.
  • Under remnant movement the landing site of the remnant loses the label of what moved out of it, and a head occurring only in a lower copy can be found.

TODO

  • labelsAt depends only on the term at a position; the isomorphism between the positions of two occurrences is missing.
  • On a derivation, labels on the contraction agree with those on the copy object when each lower copy is c-commanded by a higher occurrence; stating it needs the contraction's positions embedded in the copy object's.

References

Declarations

y is in the domain of x in t: every occurrence of y is a term of an occurrence of x, Chomsky 2013's condition under which the labeling algorithm searching x sees y.

def LinearizedSyntacticObject.InDomainL70–72
(t : LinearizedSyntacticObject) (y x : SyntacticObject) :
Prop

Used by LinearizedSyntacticObject.instDecidableInDomain, LinearizedSyntacticObject.InDomain.trans, LinearizedSyntacticObject.findsHead_iff, LinearizedSyntacticObject.findsHead_of_covBy, LinearizedSyntacticObject.labelsAt_merge_head, LinearizedSyntacticObject.isLabeledBy_merge_head, LinearizedSyntacticObject.labelsAt_merge_heads, LinearizedSyntacticObject.labels_merge_heads, LinearizedSyntacticObject.inDomain_iff_of_immediatelyContains, LinearizedSyntacticObject.inDomain_iff_of_covBy, LinearizedSyntacticObject.findsHead_iff_of_covBy, LinearizedSyntacticObject.labelsAt_merge, LinearizedSyntacticObject.labelsAt_merge_of_not_inDomain, LinearizedSyntacticObject.labelDaughter_iff_of_merge_head

Minimal search from the occurrence at n finds the head at q: a head in the domain of the term at n that no other is closer than.

def LinearizedSyntacticObject.FindsHeadL77–81
(t : LinearizedSyntacticObject) (n q : (↑t).Positions) :
Prop

The definition is too large to print here; read it in the source.

Used by LinearizedSyntacticObject.instDecidablePredPositionsVertexTokenValRoseTreeIsSyntacticObjectMkFindsHead, LinearizedSyntacticObject.labelsAt, LinearizedSyntacticObject.mem_labelsAt, LinearizedSyntacticObject.findsHead_iff, LinearizedSyntacticObject.findsHead_self, LinearizedSyntacticObject.findsHead_of_covBy, LinearizedSyntacticObject.findsHead_iff_of_covBy

L83–90

The heads minimal search from the occurrence at n finds.

def LinearizedSyntacticObject.labelsAtL92–94
(t : LinearizedSyntacticObject) (n : (↑t).Positions) :
Finset LexicalItem.Token

Built from

Used by LinearizedSyntacticObject.labels, LinearizedSyntacticObject.mem_labelsAt, LinearizedSyntacticObject.mem_labels, LinearizedSyntacticObject.labelsAt_subset_labels, LinearizedSyntacticObject.labels_eq_of_forall_labelsAt_eq, LinearizedSyntacticObject.labelsAt_merge_head, LinearizedSyntacticObject.labelsAt_merge_heads, LinearizedSyntacticObject.labelsAt_merge, LinearizedSyntacticObject.labelsAt_merge_of_not_inDomain, LinearizedSyntacticObject.LabelDaughter

The labels of x: the heads minimal search from an occurrence of x finds.

def LinearizedSyntacticObject.labelsL96–98
(t : LinearizedSyntacticObject) (x : SyntacticObject) :
Finset LexicalItem.Token

Built from

Used by LinearizedSyntacticObject.IsLabeledBy, LinearizedSyntacticObject.instDecidableIsLabeledBy, LinearizedSyntacticObject.IsLabeledByFeature, LinearizedSyntacticObject.card_labels_eq_one_iff, LinearizedSyntacticObject.instDecidableExistsTokenIsLabeledBy, LinearizedSyntacticObject.mem_labels, LinearizedSyntacticObject.labelsAt_subset_labels, LinearizedSyntacticObject.labels_eq_of_forall_labelsAt_eq, LinearizedSyntacticObject.labels_merge_heads

Used in Boskovic2018, Chomsky2013

x is labeled by the head a: minimal search finds a alone.

def LinearizedSyntacticObject.IsLabeledByL100–101
(t : LinearizedSyntacticObject) (x : SyntacticObject) (a : LexicalItem.Token) :
Prop

Built from

Used by LinearizedSyntacticObject.instDecidableIsLabeledBy, LinearizedSyntacticObject.IsLabeled, LinearizedSyntacticObject.card_labels_eq_one_iff, LinearizedSyntacticObject.instDecidableExistsTokenIsLabeledBy, LinearizedSyntacticObject.isLabeledBy_merge_head

Used in Chomsky2013, Chomsky2015

x is labeled by the feature f: minimal search finds several heads, none a daughter of x, each two of which agree in f. Two phrases are labeled by a most prominent feature they share, such as Q or the φ-features, in Chomsky 2013, and the label is written ⟨F, F⟩ in Chomsky 2015.

def LinearizedSyntacticObject.IsLabeledByFeatureL109–115
(t : LinearizedSyntacticObject) {F : Type u_1} (Agreed : F → LexicalItem.Token → LexicalItem.Token → Prop) (x : SyntacticObject) (f : F) :
Prop

Built from

Used by LinearizedSyntacticObject.instDecidableIsLabeledByFeatureOfDecidableRelToken, LinearizedSyntacticObject.IsLabeled, LinearizedSyntacticObject.IsLabeledByFeature.mono

Used in Chomsky2013, Chomsky2015

x is labeled, by a head or by a feature its heads agree in.

def LinearizedSyntacticObject.IsLabeledL123–125
(t : LinearizedSyntacticObject) {F : Type u_1} (Agreed : F → LexicalItem.Token → LexicalItem.Token → Prop) (x : SyntacticObject) :
Prop

Built from ,

Used by LinearizedSyntacticObject.instDecidableIsLabeledOfFintypeOfDecidableRelToken, LinearizedSyntacticObject.IsLabeled.mono

What minimal search finds

Search finds the visible heads that no visible head asymmetrically c-commands.

theorem LinearizedSyntacticObject.findsHead_iffL173–181
{t : LinearizedSyntacticObject} {n q : (↑t).Positions} :
t.FindsHead n q ↔ (n ≤ q ∧ t.InDomain (t.termAt q) (t.termAt n) ∧ t.IsHeadAt q) ∧ ∀ ⦃q' : (↑t).Positions⦄, n ≤ q' → t.InDomain (t.termAt q') (t.termAt n) → t.IsHeadAt q' → ¬((↑t).CCommands ↑q' ↑q ∧ ¬(↑t).CCommands ↑q ↑q')

Built from ,

Search below a daughter

L284–300

Two non-heads leave the heads of both, when neither has moved out of their merge and they share no token.

theorem LinearizedSyntacticObject.labelsAt_mergeL302–325
{t : LinearizedSyntacticObject} {n c d : (↑t).Positions} (hc : n ⋖ c) (hd : n ⋖ d) (hcd : c ≠ d) (hch : ¬t.IsHeadAt c) (hdh : ¬t.IsHeadAt d) (hdisj : Disjoint (t.termAt c).yield (t.termAt d).yield) (hvc : t.InDomain (t.termAt c) (t.termAt n)) (hvd : t.InDomain (t.termAt d) (t.termAt n)) :
t.labelsAt n = t.labelsAt c ∪ t.labelsAt d

Built from ,

A daughter that has moved on is invisible: the heads found are those of the other daughter.

theorem LinearizedSyntacticObject.labelsAt_merge_of_not_inDomainL327–350
{t : LinearizedSyntacticObject} {n c d : (↑t).Positions} (hc : n ⋖ c) (hd : n ⋖ d) (hcd : c ≠ d) (hcv : ∀ tok ∈ (t.termAt c).yield, ¬t.InDomain (↑tok) (t.termAt n)) (hdisj : Disjoint (t.termAt c).yield (t.termAt d).yield) (hvd : t.InDomain (t.termAt d) (t.termAt n)) :
t.labelsAt n = t.labelsAt d

Built from ,

The head relation of labels