Chains on planar syntactic objects

A planar syntactic object is a copy-theoretic representation. A vertex Vertex.lex tok is a pronounced copy of tok and a vertex Vertex.traceOf tok a deleted one, the trace Internal Merge leaves, Marcolli, Chomsky and Berwick's cancellation T/T_v with the head of T_v remembered. The chain of a token is the list of its copies, and a copy stands for the maximal projection of its token, so a moved phrase sits where its head projects. A token moves when it has a deleted copy. A token bound in situ by an operator, as for Pesetsky, has a single copy. A deleted copy above the pronounced one is Huang's covert movement, and a pronounced copy between two deleted ones is Sato and Ngui's partial movement, so where a phrase is pronounced and where it takes scope come apart without a separate choice of the copy to spell out. A token with two pronounced copies is shared, dominated by two mothers, Citko's Parallel Merge.

A copy is linked to the nearest copy above it, the one whose projection c-commands it with no other copy's projection in between, c-command being Reinhart's (RoseTree.CCommands). A token with one copy has no link (links_eq_nil_of_length_le_one). The locality conditions on links are in SyntacticObject/Locality.lean.

Main definitions

• Minimalist.tokenList, Minimalist.traceList: the pronounced and the deleted copies.
• occurrences, traces, chain, Moves, IsShared: the copies of a token.
• projectionAt: the phrase a copy stands for, its maximal projection along head daughters (headIndex?, PhraseStructure.maximalProjectionAt).
• HasAntecedent, orphanTraces: whether a pronounced copy c-commands a deleted one, and the deleted copies without antecedents, seen from their own conjunct copies.
• IsLink, links, chainTop: the links of a chain and its scope position.

Implementation notes

• Positions, not terms, individuate copies: two deleted copies of one token are the same term.
• The head daughters follow the raising head, and the drawing convention only where it is undefined (headIndex?, SyntacticObject/Position.lean), so that a phrase with a specifier merged in place still has a maximal projection to locate a copy in.
• A chain here is the copies an object contains; the replay of a derivation (Derivation.externalize?) builds overt chains with bound traces, while covert movement, sharing and copies without antecedents are available to the representation only.

TODO

• A successful Derivation.externalize? has no deleted copy without an antecedent.

References

• [MCB25]
• [Cit05]
• [Pes87]
• [Hua82a]
• [SN17]
• [BP90]

Copies

def Minimalist.positions {β : Type u_1} (f : SyntacticObject.Vertex → Option β) (t : RoseTree SyntacticObject.Vertex) : List (Core.Order.TreePath × β)

The positions of t whose label f accepts, with the values, in preorder.

Equations

• One or more equations did not get rendered due to their size.

theorem Minimalist.mem_positions_iff {β : Type u_1} {f : SyntacticObject.Vertex → Option β} {t : RoseTree SyntacticObject.Vertex} {p : Core.Order.TreePath} {b : β} : (p, b) ∈ positions f t ↔ ∃ (s : RoseTree SyntacticObject.Vertex), t.subtreeAt p.toList = some s ∧ f s.value = some b

theorem Minimalist.nodup_map_fst_positions {β : Type u_1} (f : SyntacticObject.Vertex → Option β) (t : RoseTree SyntacticObject.Vertex) : (List.map Prod.fst (positions f t)).Nodup

def Minimalist.tokenList : RoseTree SyntacticObject.Vertex → List (Core.Order.TreePath × LexicalItem.Token)

The pronounced copies, left to right.

Equations

• Minimalist.tokenList = Minimalist.positions (Sum.elim id fun (x : Option Minimalist.LexicalItem.Token) => none)

def Minimalist.traceList : RoseTree SyntacticObject.Vertex → List (Core.Order.TreePath × LexicalItem.Token)

The deleted copies, left to right.

Equations

• Minimalist.traceList = Minimalist.positions (Sum.elim (fun (x : Option Minimalist.LexicalItem.Token) => none) id)

def Minimalist.occurrences (t : PlanarSyntacticObject) (tok : LexicalItem.Token) : List Core.Order.TreePath

The positions of the pronounced copies of tok.

Equations

• Minimalist.occurrences t tok = List.filterMap (fun (x : Core.Order.TreePath × Minimalist.LexicalItem.Token) => if x.2 = tok then some x.1 else none) (Minimalist.tokenList ↑t)

def Minimalist.traces (t : PlanarSyntacticObject) (tok : LexicalItem.Token) : List Core.Order.TreePath

The positions of the deleted copies of tok.

Equations

• Minimalist.traces t tok = List.filterMap (fun (x : Core.Order.TreePath × Minimalist.LexicalItem.Token) => if x.2 = tok then some x.1 else none) (Minimalist.traceList ↑t)

def Minimalist.chain (t : PlanarSyntacticObject) (tok : LexicalItem.Token) : List Core.Order.TreePath

The chain of tok lists the positions of its copies, pronounced or deleted, left to right.

Equations

• Minimalist.chain t tok = List.filterMap (fun (x : Core.Order.TreePath × Minimalist.LexicalItem.Token) => if x.2 = tok then some x.1 else none) (Minimalist.positions (Sum.elim id id) ↑t)

def Minimalist.Moves (t : PlanarSyntacticObject) (tok : LexicalItem.Token) : Prop

tok moves when it has a deleted copy.

Equations

• Minimalist.Moves t tok = (Minimalist.traces t tok ≠ [])

@[instance_reducible]

instance Minimalist.instDecidableMoves (t : PlanarSyntacticObject) (tok : LexicalItem.Token) : Decidable (Moves t tok)

Equations

• Minimalist.instDecidableMoves t tok = { decide := !decide (Minimalist.traces t tok = []), reflects_decide := ⋯ }

def Minimalist.IsShared (t : PlanarSyntacticObject) (tok : LexicalItem.Token) : Prop

tok is shared, dominated by two mothers, when it has two pronounced copies.

Equations

• Minimalist.IsShared t tok = (2 ≤ (Minimalist.occurrences t tok).length)

@[instance_reducible]

instance Minimalist.instDecidableIsShared (t : PlanarSyntacticObject) (tok : LexicalItem.Token) : Decidable (IsShared t tok)

Equations

• Minimalist.instDecidableIsShared t tok = { decide := Nat.ble 2 (Minimalist.occurrences t tok).length, reflects_decide := ⋯ }

The phrase a copy stands for

def Minimalist.projectionAt (t : PlanarSyntacticObject) (p : Core.Order.TreePath) : Core.Order.TreePath

The maximal projection of the copy at p is the highest position reached from p by climbing while the position is the head daughter of its mother.

Equations

• Minimalist.projectionAt t p = PhraseStructure.maximalProjectionAt (fun (q : Core.Order.TreePath) => ((↑t).subtreeAt q.toList).bind Minimalist.headIndex?) p

theorem Minimalist.projectionAt_le (t : PlanarSyntacticObject) (p : Core.Order.TreePath) : projectionAt t p ≤ p

def Minimalist.HasAntecedent (t : PlanarSyntacticObject) (x : Core.Order.TreePath × LexicalItem.Token) : Prop

A deleted copy has an antecedent when the projection of a pronounced copy of its token c-commands it.

Equations

• Minimalist.HasAntecedent t x = ∃ p ∈ Minimalist.occurrences t x.2, (↑t).CCommands (Minimalist.projectionAt t p) x.1

@[instance_reducible]

instance Minimalist.instDecidableHasAntecedent (t : PlanarSyntacticObject) (x : Core.Order.TreePath × LexicalItem.Token) : Decidable (HasAntecedent t x)

Equations

• Minimalist.instDecidableHasAntecedent t x = Minimalist.instDecidableHasAntecedent._aux_1 t x

def Minimalist.orphanTraces (t : PlanarSyntacticObject) : List (Core.Order.TreePath × LexicalItem.Token)

The deleted copies without antecedents.

Equations

• Minimalist.orphanTraces t = List.filter (fun (x : Core.Order.TreePath × Minimalist.LexicalItem.Token) => decide ¬Minimalist.HasAntecedent t x) (Minimalist.traceList ↑t)

Links

def Minimalist.IsLink (t : PlanarSyntacticObject) (tok : LexicalItem.Token) (p q : Core.Order.TreePath) : Prop

The copy at p is linked to the copy at q below it when its projection c-commands q and the projection of no other copy of tok lies between them.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Minimalist.instDecidableIsLink (t : PlanarSyntacticObject) (tok : LexicalItem.Token) (p q : Core.Order.TreePath) : Decidable (IsLink t tok p q)

Equations

• One or more equations did not get rendered due to their size.

def Minimalist.links (t : PlanarSyntacticObject) (tok : LexicalItem.Token) : List (Core.Order.TreePath × Core.Order.TreePath)

The links of the chain of tok pair each copy with the projection of the copy linked to it.

Equations

• One or more equations did not get rendered due to their size.

def Minimalist.chainTop (t : PlanarSyntacticObject) (tok : LexicalItem.Token) : List Core.Order.TreePath

The top of the chain of tok consists of the copies no copy's projection c-commands, where it takes scope.

Equations

• One or more equations did not get rendered due to their size.

theorem Minimalist.not_isLink_self (t : PlanarSyntacticObject) (tok : LexicalItem.Token) (p : Core.Order.TreePath) : ¬IsLink t tok p p

theorem Minimalist.links_eq_nil_of_length_le_one (t : PlanarSyntacticObject) (tok : LexicalItem.Token) (h : (chain t tok).length ≤ 1) : links t tok = []

A token with at most one copy has no link.