Spell-out of planar syntactic objects

PF pronounces the pronounced copies of a planar syntactic object (Chain.lean) and nothing else, so a deleted copy, a trace, is silent wherever it stands. A shared token is one token, pronounced once, at its last occurrence, as Wilder and de Vries linearize multidominance, so that material two conjuncts share is pronounced in the second. An [E] feature on a head silences the head's complement, after Merchant, and since a shared token is one token, eliding either of its occurrences silences it everywhere. An [E] head applies once per distinct complement.

Main definitions

• pronouncedAt, elidedDomains, IsSilenced: pronunciation under [E].
• pfYield, pfPhon: the pronounced tokens and forms, left to right.

Main statements

• nodup_pfYield: a token is pronounced once at most, however many mothers dominate it.

References

• [Wil99]
• [dV09]
• [Mer01]

def Minimalist.pronouncedAt (t : PlanarSyntacticObject) (tok : LexicalItem.Token) : Option Core.Order.TreePath

tok is pronounced at its last occurrence.

Equations

• Minimalist.pronouncedAt t tok = (Minimalist.occurrences t tok).getLast?

Ellipsis

def Minimalist.complement (p : Core.Order.TreePath) : Core.Order.TreePath

The complement of the head at p is its sister.

Equations

• Minimalist.complement p = { toList := p.toList.dropLast ++ [1 - p.toList.getLastD 0] }

def Minimalist.eHeads (t : PlanarSyntacticObject) : List Core.Order.TreePath

The [E] heads.

Equations

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

def Minimalist.elidedDomains (t : PlanarSyntacticObject) : List Core.Order.TreePath

The elided domains are the distinct complements of the [E] heads, in the order of the heads, so a shared head over one shared complement applies once and over two complements twice.

Equations

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

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

tok is silenced when one of its occurrences lies in an elided domain.

Equations

• Minimalist.IsSilenced t tok = ∃ K ∈ Minimalist.elidedDomains t, ∃ p ∈ Minimalist.occurrences t tok, K ≤ p

@[instance_reducible]

instance Minimalist.instDecidableIsSilenced (t : PlanarSyntacticObject) (tok : LexicalItem.Token) : Decidable (IsSilenced t tok)

Equations

• Minimalist.instDecidableIsSilenced t tok = Minimalist.instDecidableIsSilenced._aux_1 t tok

def Minimalist.pfYield (t : PlanarSyntacticObject) : List LexicalItem.Token

The pronounced tokens, left to right, each at its last occurrence unless silenced.

Equations

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

def Minimalist.pfPhon (t : PlanarSyntacticObject) : List String

The pronounced forms, left to right.

Equations

• Minimalist.pfPhon t = List.filterMap (fun (x : Minimalist.LexicalItem.Token) => x.item.phonForm?) (Minimalist.pfYield t)

theorem Minimalist.nodup_pfYield (t : PlanarSyntacticObject) : (pfYield t).Nodup

A token is pronounced once at most, however many mothers dominate it.