Cinque 2005: Deriving Greenberg's Universal 20 and its exceptions

Of the 24 orders of demonstrative, numeral, adjective and noun, 14 are attested, in very unequal numbers of languages, and Greenberg's Universal 20 in Hawkins's revision (1) misdescribes the postnominal ones. The paper derives exactly the attested orders from one order of Merge, [Dem [Num [A [N]]]] (7a), and leftward movement of the NP alone or of a phrase containing it past each modifier in turn (7b): no movement and pied-piping of the whose-picture type, [NP [XP]], are unmarked; movement without pied-piping, pied-piping of the picture-of-who type, [XP [NP]], and partial rather than total raising are marked; head movement and movement of a phrase without the overt NP are excluded, the asymmetry Kayne's antisymmetry imposes. Each attested order has such a derivation and each unattested one would need a wrong order of Merge (6a–x), and the number of marked options a derivation uses tracks frequency: none for the two orders of very many languages, two for orders of few or very few.

table is (6) with each order's frequency and the count of marked options the paper's analysis of it states; stagesOf enumerates the derivations of (7) on the substrate's Derivation, an optional raise of any subtree containing the overt noun after each Merge, with the orders read by the substrate's externalization, and u20_reachable_iff_attested is the paper's result. The marked options are derived from the derivations rather than transcribed: raising the modifier's whole complement pied-pipes, of the whose-picture type when the noun is its specifier, raising a proper part strands, and a derivation is partial when the noun moves but not to the left edge; markedOptions takes the least count over an order's derivations. The derived counts are the paper's for every order with a stated count except (6w), which (7b-v) classes as partial while the count omits it (markedOptions_eq_stated, markedOptions_w); with two marked options rather than one, its very few languages fit the frequency claim markedness_extremes. The demonstrative is Cat.Dem.

References

• G. Cinque, Deriving Greenberg's Universal 20 and its exceptions (2005)
• J. H. Greenberg, Some Universals of Grammar with Particular Reference to the Order of Meaningful Elements (1963)
• J. A. Hawkins, Word Order Universals (1983)
• R. S. Kayne, The Antisymmetry of Syntax (1994)

The orders and their frequencies (6)

inductive Cinque2005.Freq : Type

The paper's frequency labels.

• veryMany : Freq
• many : Freq
• few : Freq
• veryFew : Freq
• unattested : Freq

@[instance_reducible]

instance Cinque2005.instDecidableEqFreq : DecidableEq Freq

Equations

• Cinque2005.instDecidableEqFreq x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cinque2005.instReprFreq.repr : Freq → ℕ → Std.Format

Equations

• Cinque2005.instReprFreq.repr Cinque2005.Freq.veryMany prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cinque2005.Freq.veryMany")).group prec✝
• Cinque2005.instReprFreq.repr Cinque2005.Freq.many prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cinque2005.Freq.many")).group prec✝
• Cinque2005.instReprFreq.repr Cinque2005.Freq.few prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cinque2005.Freq.few")).group prec✝
• Cinque2005.instReprFreq.repr Cinque2005.Freq.veryFew prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cinque2005.Freq.veryFew")).group prec✝
• Cinque2005.instReprFreq.repr Cinque2005.Freq.unattested prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cinque2005.Freq.unattested")).group prec✝

@[instance_reducible]

instance Cinque2005.instReprFreq : Repr Freq

Equations

• Cinque2005.instReprFreq = { reprPrec := Cinque2005.instReprFreq.repr }

structure Cinque2005.OrderRow : Type

A row of (6) records an order of Dem, Num, A and N, its frequency, and the number of marked options the paper's derivation of it counts, none for the unattested orders and for (6p).

• order : List Minimalist.Cat
• freq : Freq
• stated : Option ℕ

@[instance_reducible]

instance Cinque2005.instDecidableEqOrderRow : DecidableEq OrderRow

Equations

• Cinque2005.instDecidableEqOrderRow = Cinque2005.instDecidableEqOrderRow.decEq

def Cinque2005.instDecidableEqOrderRow.decEq (x✝ x✝¹ : OrderRow) : Decidable (x✝ = x✝¹)

Equations

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

def Cinque2005.instReprOrderRow.repr : OrderRow → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cinque2005.instReprOrderRow : Repr OrderRow

Equations

• Cinque2005.instReprOrderRow = { reprPrec := Cinque2005.instReprOrderRow.repr }

def Cinque2005.OrderRow.Attested (r : OrderRow) : Prop

The order is attested.

Equations

• r.Attested = (r.freq ≠ Cinque2005.Freq.unattested)

@[instance_reducible]

instance Cinque2005.instDecidableAttested (r : OrderRow) : Decidable r.Attested

Equations

• Cinque2005.instDecidableAttested r = { decide := !decide (r.freq = Cinque2005.Freq.unattested), reflects_decide := ⋯ }

def Cinque2005.table : List OrderRow

(6a)–(6x).

Equations

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

The derivation space (7)

inductive Cinque2005.Marked : Type

The marked options of (7b) are raising without pied-piping (iii), pied-piping of the picture-of-who type (iv), and partial rather than total raising (v).

• withoutPiedPiping : Marked
• pictureOfWho : Marked
• partialMovement : Marked

@[instance_reducible]

instance Cinque2005.instDecidableEqMarked : DecidableEq Marked

Equations

• Cinque2005.instDecidableEqMarked x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cinque2005.instReprMarked.repr : Marked → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cinque2005.instReprMarked : Repr Marked

Equations

• Cinque2005.instReprMarked = { reprPrec := Cinque2005.instReprMarked.repr }

def Cinque2005.tokN : Minimalist.LexicalItem.Token

Equations

• Cinque2005.tokN = { item := Minimalist.LexicalItem.of Minimalist.Cat.N [], id := 1 }

def Cinque2005.tokA : Minimalist.LexicalItem.Token

Equations

• Cinque2005.tokA = { item := Minimalist.LexicalItem.of Minimalist.Cat.A [], id := 2 }

def Cinque2005.tokNum : Minimalist.LexicalItem.Token

Equations

• Cinque2005.tokNum = { item := Minimalist.LexicalItem.of Minimalist.Cat.Num [], id := 3 }

def Cinque2005.tokDem : Minimalist.LexicalItem.Token

Equations

• Cinque2005.tokDem = { item := Minimalist.LexicalItem.of Minimalist.Cat.Dem [], id := 4 }

def Cinque2005.hasN : RoseTree Minimalist.SyntacticObject.Vertex → Bool

The tree contains the overt noun; a trace does not count (7b-vi).

Equations

• Cinque2005.hasN (RoseTree.node (Sum.inl (some t)) children) = (t == Cinque2005.tokN)
• Cinque2005.hasN (RoseTree.node (Sum.inl none) [l, r]) = (Cinque2005.hasN l || Cinque2005.hasN r)
• Cinque2005.hasN (RoseTree.node value children) = false

def Cinque2005.specHasN : RoseTree Minimalist.SyntacticObject.Vertex → Bool

The noun is the tree's specifier, [NP [XP]] (fn. 21).

Equations

• Cinque2005.specHasN (RoseTree.node (Sum.inl (some t)) children) = (t == Cinque2005.tokN)
• Cinque2005.specHasN (RoseTree.node (Sum.inl none) [l, r]) = Cinque2005.hasN l
• Cinque2005.specHasN (RoseTree.node value children) = false

def Cinque2005.markOf (c s : RoseTree Minimalist.SyntacticObject.Vertex) : Option Marked

The marked option used by raising s past a modifier whose complement is c. The whole complement pied-pipes, of the whose-picture type when the noun is its specifier and of the picture-of-who type otherwise, and a proper part strands the rest.

Equations

• Cinque2005.markOf c s = if (s == c) = true then if Cinque2005.specHasN s = true then none else some Cinque2005.Marked.pictureOfWho else some Cinque2005.Marked.withoutPiedPiping

structure Cinque2005.Stage : Type

A stage of the enumeration records the derivation, its ordered form, the marked options of its raises and their number.

• derivation : Minimalist.Derivation
• planar : Minimalist.PlanarSyntacticObject
• marks : List Marked
• raises : ℕ

def Cinque2005.step (m : Minimalist.LexicalItem.Token) (st : Stage) : List Stage

Merge the modifier m above the current object, then optionally raise a subtree containing the overt noun to the left edge.

Equations

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

def Cinque2005.stagesOf (ms : List Minimalist.LexicalItem.Token) : List Stage

The derivations (7) allows from the noun and the modifiers ms, merged in turn, with an optional raise after each Merge.

Equations

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

def Cinque2005.stages : List Stage

The derivations of A, Num and Dem.

Equations

• Cinque2005.stages = Cinque2005.stagesOf [Cinque2005.tokA, Cinque2005.tokNum, Cinque2005.tokDem]

def Cinque2005.Stage.order (st : Stage) : List Minimalist.Cat

The surface order of a stage, read by the substrate's externalization.

Equations

• st.order = st.derivation.surfaceCats

def Cinque2005.reachableOrders : List (List Minimalist.Cat)

The orders some derivation reaches.

Equations

• Cinque2005.reachableOrders = (List.map Cinque2005.Stage.order Cinque2005.stages).eraseDups

theorem Cinque2005.u20_reachable_iff_attested : (table.all fun (r : OrderRow) => decide (decide (r.order ∈ reachableOrders) = decide r.Attested)) = true

Universal 20 is derived, an order being reachable iff it is attested, so the 14 attested orders have derivations and the 10 unattested do not.

Markedness and frequency (7b)

def Cinque2005.Stage.marked (st : Stage) : List Marked

The marked options of a stage, partial movement (7b-v) among them when the noun has moved but not to the left edge.

Equations

• st.marked = (if 0 < st.raises ∧ st.order.head? ≠ some Minimalist.Cat.N then [Cinque2005.Marked.partialMovement] else []) ++ st.marks

def Cinque2005.markedOptions (ord : List Minimalist.Cat) : Option ℕ

The number of distinct marked options in the least marked derivation of an order.

Equations

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

theorem Cinque2005.markedOptions_eq_stated : ((List.filter (fun (r : OrderRow) => r.stated.isSome && r.order != [Minimalist.Cat.A, Minimalist.Cat.N, Minimalist.Cat.Num, Minimalist.Cat.Dem]) table).all fun (r : OrderRow) => decide (markedOptions r.order = r.stated)) = true

The derived count is the paper's for every order with a stated count except (6w).

theorem Cinque2005.markedOptions_w : markedOptions [Minimalist.Cat.A, Minimalist.Cat.N, Minimalist.Cat.Num, Minimalist.Cat.Dem] = some 2

For (6w), A N Num Dem, the paper counts one marked option, the picture-of-who pied-piping of [A N] past Num, but (7b-v) lists the order as partial, and no derivation avoids it, since the noun never passes A.

theorem Cinque2005.markedOptions_p : markedOptions [Minimalist.Cat.N, Minimalist.Cat.Dem, Minimalist.Cat.A, Minimalist.Cat.Num] = some 1

(6p), N Dem A Num, for which the paper states no count, has one marked option, the extraction of the noun past Dem.

theorem Cinque2005.markedness_extremes : ((List.filter (fun (r : OrderRow) => decide r.Attested) table).all fun (r : OrderRow) => decide ((markedOptions r.order = some 0 ↔ r.freq = Freq.veryMany) ∧ (markedOptions r.order = some 2 → r.freq = Freq.few ∨ r.freq = Freq.veryFew))) = true

Marked options predict the extremes of frequency. An attested order has no marked option iff it is found in very many languages, and an order with two is found in few or very few.