Heads

A licensing of Merge is a morphism of magmas out of the syntactic objects into a commutative magma with zero, 0 being the failure of Merge, and its head function reads a head off each value. Marcolli, Chomsky and Berwick's head functions are partial, and the head of a Merge is the head of the daughter that projects; Head records that law on the target, so the head function of every licensing is endocentric. Where 0 absorbs, the domain of a licensing is closed under daughters (ne_zero_and_ne_zero_of_mul after map_mul), though not under Merge, since an exocentric Merge of two headed objects has no head. Selection, labeling and raising are instances.

Main definitions

• Minimalist.Head: an endocentric head on a magma with zero.

Main statements

• Minimalist.mem_head_or_mem_head_of_mem_head_mul: a product's head is a factor's head.
• Minimalist.mem_head_or_mem_head_of_mem_head_map_mul: so is the head of the image of a product under a morphism of magmas.

References

• [MCB25]

class Minimalist.Head (β : Type u_1) [Mul β] [Zero β] : Type u_1

An endocentric head on a magma with zero: 0, the failure of Merge, has no head, and the head of a product is the head of one of its factors, the characterization of heads in [MCB25], Lemma 1.13.7.

• head : β → Option LexicalItem.Token

  The projecting head, if any.

• head_zero : head 0 = none
• mem_head_or_mem_head_of_mem_head_mul {x y : β} {t : LexicalItem.Token} : t ∈ head (x * y) → t ∈ head x ∨ t ∈ head y

@[simp]

theorem Minimalist.head_zero {β : Type u_1} [Mul β] [Zero β] [Head β] : head 0 = none

theorem Minimalist.mem_head_or_mem_head_of_mem_head_mul {β : Type u_1} [Mul β] [Zero β] [Head β] {x y : β} {t : LexicalItem.Token} (h : t ∈ head (x * y)) : t ∈ head x ∨ t ∈ head y

theorem Minimalist.mem_head_or_mem_head_of_mem_head_map_mul {β : Type u_1} [Mul β] [Zero β] [Head β] {M : Type u_2} [Mul M] (φ : M →ₙ* β) {x y : M} {t : LexicalItem.Token} (h : t ∈ head (φ (x * y))) : t ∈ head (φ x) ∨ t ∈ head (φ y)

The head of the image of a product is the head of a factor's image: a licensing's head function is endocentric ([MCB25], Lemma 1.13.7).