Clause spines

A clause spine is the list of heads a clause projects, from the lexical head upward, so a bare VP is [V], a finite clause [V, v, T, C], and a nominalized complement the finite clause with the nominal shell [N, D] appended. A spine is an extended projection in Grimshaw's sense when each head extends the one below it. Keine observes that category features project bilaterally within an extended projection, so a clause is labeled by the set of every head it projects. The label of a spine is that finset, and spines are preordered by inclusion of labels, the extension order, in which the clause sizes of one extended projection form a chain and a nominalized clause and a finite clause are incomparable. A head divides a spine into its complement, the heads below it, and the shell above it.

Main definitions

• Minimalist.ClauseSpine: the list of heads a clause projects, bottom-up.
• Minimalist.ClauseSpine.label: the bilateral label, the finset of heads a spine projects.
• Minimalist.ClauseSpine.IsExtendedProjection: a spine each of whose heads extends the one below it.
• Minimalist.ClauseSpine.append: the spine with a nominal or adpositional shell over it.
• Minimalist.ClauseSpine.below, Minimalist.ClauseSpine.above: the heads below the first occurrence of a category, its complement, and above the last, the shell over it.
• Minimalist.ClauseSpine.vP, Minimalist.ClauseSpine.tP, Minimalist.ClauseSpine.cP: the clause sizes of the verbal extended projection.

Main results

• Minimalist.ClauseSpine.le_def: the extension order is inclusion of labels.
• Minimalist.ClauseSpine.IsExtendedProjection.pairwise: in an extended projection every head extends each head below it.
• Minimalist.ClauseSpine.below_prefix: the complement of a head lies inside the complement of every head above it.

Implementation notes

ClauseSpine is a one-field structure rather than List Cat so that its order is inclusion of labels, not the lexicographic order of lists.

References

• [Gri05b]
• [Kei19]
• [Kei20]
• [Dea26]

structure Minimalist.ClauseSpine : Type

A clause spine is the list of heads a clause projects, from the lexical head upward.

• heads : List Cat

  The projected heads, bottom-up.

def Minimalist.instReprClauseSpine.repr : ClauseSpine → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.instReprClauseSpine : Repr ClauseSpine

Equations

• Minimalist.instReprClauseSpine = { reprPrec := Minimalist.instReprClauseSpine.repr }

def Minimalist.instDecidableEqClauseSpine.decEq (x✝ x✝¹ : ClauseSpine) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqClauseSpine.decEq { heads := a } { heads := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.instDecidableEqClauseSpine : DecidableEq ClauseSpine

Equations

• Minimalist.instDecidableEqClauseSpine = Minimalist.instDecidableEqClauseSpine.decEq

@[instance_reducible]

instance Minimalist.ClauseSpine.instMembershipCat : Membership Cat ClauseSpine

Equations

• Minimalist.ClauseSpine.instMembershipCat = { mem := fun (s : Minimalist.ClauseSpine) (c : Minimalist.Cat) => c ∈ s.heads }

@[simp]

theorem Minimalist.ClauseSpine.mem_def {s : ClauseSpine} {c : Cat} : c ∈ s ↔ c ∈ s.heads

@[instance_reducible]

instance Minimalist.ClauseSpine.instDecidableMemCat (c : Cat) (s : ClauseSpine) : Decidable (c ∈ s)

Equations

• Minimalist.ClauseSpine.instDecidableMemCat c s = { decide := decide (List.elem c s.heads = true), reflects_decide := ⋯ }

@[instance_reducible]

instance Minimalist.ClauseSpine.instDecidableForallForallMemCatOfDecidablePred (P : Cat → Prop) [DecidablePred P] (s : ClauseSpine) : Decidable (∀ (c : Cat), c ∈ s → P c)

Equations

• Minimalist.ClauseSpine.instDecidableForallForallMemCatOfDecidablePred P s = List.decidableBAll P s.heads

@[instance_reducible]

instance Minimalist.ClauseSpine.instDecidableExistsCatAndMemOfDecidablePred (P : Cat → Prop) [DecidablePred P] (s : ClauseSpine) : Decidable (∃ (c : Cat), c ∈ s ∧ P c)

Equations

• Minimalist.ClauseSpine.instDecidableExistsCatAndMemOfDecidablePred P s = List.decidableBEx P s.heads

Extended projections

def Minimalist.ClauseSpine.IsExtendedProjection (s : ClauseSpine) : Prop

A spine is an extended projection when each head extends the one below it, so that its heads are of one family and their F-values do not decrease.

Equations

• s.IsExtendedProjection = List.IsChain Minimalist.Cat.ExtendsTo s.heads

@[instance_reducible]

instance Minimalist.ClauseSpine.instDecidableIsExtendedProjection (s : ClauseSpine) : Decidable s.IsExtendedProjection

Equations

• s.instDecidableIsExtendedProjection = Minimalist.ClauseSpine.instDecidableIsExtendedProjection._aux_1 s

theorem Minimalist.ClauseSpine.IsExtendedProjection.pairwise {s : ClauseSpine} (h : s.IsExtendedProjection) : List.Pairwise Cat.ExtendsTo s.heads

In an extended projection every head extends each head below it.

Labels and the extension order

def Minimalist.ClauseSpine.label (s : ClauseSpine) : Finset Cat

The bilateral label of a spine is the set of heads it projects.

Equations

• s.label = s.heads.toFinset

@[simp]

theorem Minimalist.ClauseSpine.mem_label {s : ClauseSpine} {c : Cat} : c ∈ s.label ↔ c ∈ s

@[instance_reducible]

instance Minimalist.ClauseSpine.instPreorder : Preorder ClauseSpine

The extension order. A spine lies below another when the other projects every head it does, as the clause sizes of one extended projection do.

Equations

• Minimalist.ClauseSpine.instPreorder = Preorder.lift Minimalist.ClauseSpine.label

theorem Minimalist.ClauseSpine.le_def {s t : ClauseSpine} : s ≤ t ↔ s.label ⊆ t.label

theorem Minimalist.ClauseSpine.le_iff_forall_mem {s t : ClauseSpine} : s ≤ t ↔ ∀ (c : Cat), c ∈ s → c ∈ t

@[instance_reducible]

instance Minimalist.ClauseSpine.instDecidableLE : DecidableLE ClauseSpine

Equations

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

@[instance_reducible]

instance Minimalist.ClauseSpine.instDecidableLT : DecidableLT ClauseSpine

Equations

• s.instDecidableLT t = { decide := decide (s.label ⊆ t.label) && decide ¬t.label ⊆ s.label, reflects_decide := ⋯ }

Shells

def Minimalist.ClauseSpine.append (s : ClauseSpine) (l : List Cat) : ClauseSpine

Appending heads to a spine projects a nominal or adpositional shell over the clause.

Equations

• s.append l = { heads := s.heads ++ l }

@[simp]

theorem Minimalist.ClauseSpine.heads_append (s : ClauseSpine) (l : List Cat) : (s.append l).heads = s.heads ++ l

@[simp]

theorem Minimalist.ClauseSpine.mem_append {s : ClauseSpine} {c : Cat} {l : List Cat} : c ∈ s.append l ↔ c ∈ s ∨ c ∈ l

theorem Minimalist.ClauseSpine.le_append (s : ClauseSpine) (l : List Cat) : s ≤ s.append l

Complements and shells of a head

def Minimalist.ClauseSpine.below (s : ClauseSpine) (c : Cat) : List Cat

The heads strictly below the first occurrence of c, the complement of c.

Equations

• s.below c = List.takeWhile (fun (x : Minimalist.Cat) => x != c) s.heads

def Minimalist.ClauseSpine.above (s : ClauseSpine) (c : Cat) : List Cat

The heads strictly above the last occurrence of c, so that s.above .C is the shell over the CP of s and [] for a bare CP.

Equations

• s.above c = List.rtakeWhile (fun (x : Minimalist.Cat) => x != c) s.heads

theorem Minimalist.ClauseSpine.notMem_below_self (s : ClauseSpine) (c : Cat) : ¬c ∈ s.below c

A head is not in its own complement.

theorem Minimalist.ClauseSpine.below_prefix {s : ClauseSpine} {c d : Cat} (h : c ∈ s.below d) : s.below c <+: s.below d

The complement of a head lies inside the complement of every head above it.

theorem Minimalist.ClauseSpine.above_append {c : Cat} {l : List Cat} (s : ClauseSpine) (h : ¬c ∈ l) : (s.append l).above c = s.above c ++ l

Clause sizes

def Minimalist.ClauseSpine.vP : ClauseSpine

The vP-sized clause [V, v], the small nonfinite clause.

Equations

• Minimalist.ClauseSpine.vP = { heads := [Minimalist.Cat.V, Minimalist.Cat.v] }

def Minimalist.ClauseSpine.tP : ClauseSpine

The TP-sized clause [V, v, T], the large nonfinite clause.

Equations

• Minimalist.ClauseSpine.tP = { heads := [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T] }

def Minimalist.ClauseSpine.cP : ClauseSpine

The CP-sized clause [V, v, T, C], the finite clause.

Equations

• Minimalist.ClauseSpine.cP = { heads := [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T, Minimalist.Cat.C] }

theorem Minimalist.ClauseSpine.vP_le_tP : vP ≤ tP

theorem Minimalist.ClauseSpine.tP_le_cP : tP ≤ cP

theorem Minimalist.ClauseSpine.cP_isExtendedProjection : cP.IsExtendedProjection