Docs / Syntax / Minimalist / Label / Head

Heads

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

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, copy states 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

Marcolli et al. 2025, Mathematical Structure of Syntactic Merge: An Algebraic Model for Generative Linguistics formalized

Declarations

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 Marcolli et al. 2025, Lemma 1.13.7.

class Head L41–49

(β : Type u_1) [Mul β] [Zero β] :

Type u_1

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

Used by head_zero, mem_head_or_mem_head_of_mem_head_mul, mem_head_or_mem_head_of_mem_head_map_mul

Used in Syntax/Minimalist/Derivation/Licensing, Syntax/Minimalist/Label/RaisingHead, Syntax/Minimalist/Label/Selection, Privizentseva2026

L55

theorem mem_head_or_mem_head_of_mem_head_mul L57–59

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

t ∈ head x ∨ t ∈ head y

Built from

The head of the image of a product is the head of a factor's image: a licensing's head function is endocentric (Marcolli et al. 2025, Lemma 1.13.7).

theorem mem_head_or_mem_head_of_mem_head_map_mul L61–65

{β : 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)

Built from