Stanojević and Steedman (2021): Formal Basis of a Language Universal #
This file formalizes [SS21]'s proof of the universal [Ste20a]
proposes: over a natural order of dominance, a chain of first-order categories
X₁|X₂, X₂|X₃, …, Xₙ|Xₙ₊₁ each realizable with either slash direction, combinatory categorial
grammar derives all and only the separable permutations of the canonical linearization. The
chain is the multimodal grammar nodGrammar over the lexicon giving word i both Xᵢ/Xᵢ₊₁
and Xᵢ\Xᵢ₊₁, and the separable permutations of a span are SepPerm, the separating-tree
characterization of [BBL98]: a singleton, or two contiguous parts of the span
concatenated in canonical or inverted order. Completeness (derives_of_sepPerm) is the
paper's three lemmas in one induction, canonical splits combining by forward and inverted
splits by backward composition; soundness (sepPerm_of_derives) is the rule induction, in
which application and second-order composition never fire over a first-order chain; the
universal is derives_fwd_iff with its mirror derives_bwd_iff.
The enumeration sepPerms lists the separable permutations of a span by their separating
trees and makes SepPerm decidable. Over four elements it has the third large Schröder number
of members, twenty-two of the twenty-four orders (card_sepPerms_four); the two orders it
excludes, 2413 and 3142, are the noun-phrase and verb-cluster orders unattested in the surveys
of [Cin05], [Nch12] and [Abe16], and the grammar does not derive them
(not_derives_2413, not_derives_3142). Every order of demonstrative, numeral, adjective
and noun that [Cin05] attests is separable, and the non-separable orders are exactly
the paper's (g) and (j) (cinque_attested_separable, cinque_not_sepPerm_iff). The chance
that a theory excluding two of the twenty-four orders survives twenty-one attested ones
sampled uniformly is the paper's one in a hundred (chanceUnfalsified_two_of_twentyfour).
Implementation notes #
The paper's Theorem 3, that the separable permutations of n elements number the
(n - 1)th large Schröder number of [SS91], is stated at n = 4 against
mathlib's Nat.largeSchroder; the general count goes through the normal-form separating trees
of the paper's fourth section and is not formalized. The pattern-avoidance characterization of
[Wes96] and the extension to second-order categories and type-raising are not
formalized. The dominance relation is the first-order case of [KK09]'s
dependency structures for CCG. The tokens are the chain positions themselves, so a derived
string is the permutation it realizes.
References #
The natural order of dominance #
The forward realization Xᵢ/Xᵢ₊₁ of chain position i.
Equations
- StanojevicSteedman2021.fwd i = (CCG.Cat.atom i).rslash CCG.Modality.dot (CCG.Cat.atom (i + 1))
Instances For
The backward realization Xᵢ\Xᵢ₊₁ of chain position i.
Equations
- StanojevicSteedman2021.bwd i = (CCG.Cat.atom i).lslash CCG.Modality.dot (CCG.Cat.atom (i + 1))
Instances For
The natural-order-of-dominance lexicon over n words gives each position both slash
realizations of its chain category, the paper's order-free |.
Equations
- StanojevicSteedman2021.nodLexicon n = List.flatMap (fun (i : ℕ) => [(i + 1, StanojevicSteedman2021.fwd (i + 1)), (i + 1, StanojevicSteedman2021.bwd (i + 1))]) (List.range n)
Instances For
The NOD grammar is the multimodal grammar over the chain lexicon. The start atom plays no role in the span-level claims.
Equations
Instances For
Separable permutations #
The separable permutations of the span i…j, by separating trees. Each is a singleton, or
two contiguous parts of the span concatenated in canonical (pos) or inverted (neg) order.
- single
(i : ℕ)
: SepPerm i i [i]
A single word is a separable permutation of its own span.
- pos
{i j k : ℕ}
{u v : List ℕ}
: SepPerm i j u → SepPerm (j + 1) k v → SepPerm i k (u ++ v)
Contiguous parts in canonical order.
- neg
{i j k : ℕ}
{u v : List ℕ}
: SepPerm i j u → SepPerm (j + 1) k v → SepPerm i k (v ++ u)
Contiguous parts in inverted order.
Instances For
A separable permutation of i…j is a permutation of the canonical linearization: the
leaves of a separating tree are determined by its shape and labels.
The separable permutations of i…j listed by their separating trees, with fuel bounding
the span length.
Equations
- One or more equations did not get rendered due to their size.
- StanojevicSteedman2021.sepPermsAux 0 x✝¹ x✝ = ∅
Instances For
The separable permutations of the span i…j.
Equations
- StanojevicSteedman2021.sepPerms i j = StanojevicSteedman2021.sepPermsAux (j + 1 - i) i j
Instances For
Equations
- StanojevicSteedman2021.instDecidableSepPerm i j l = decidable_of_iff (l ∈ StanojevicSteedman2021.sepPerms i j) ⋯
The separable permutations of 1…4 number the third large Schröder number, twenty-two of
the twenty-four orders, which is Theorem 3 at four elements.
Completeness #
Every separable permutation of the span i…j is derivable at both slashings of the span
category Xᵢ|Xⱼ₊₁, the paper's three lemmas in one induction: canonical splits combine by
(possibly crossing) forward composition, inverted splits by backward composition, and the
strengthened both-slashes hypothesis feeds the harmonic and crossing cases alike.
Soundness #
Everything derivable over the NOD grammar is a span category Xᵢ|Xⱼ₊₁ over a separable
permutation of i…j. All derivable categories are first-order, so application, which needs
an atomic secondary, and second-order composition, which needs a second-order secondary,
never fire.
The universal #
CCG derives exactly the separable permutations, the paper's Theorems 1 and 2, at the forward slashing of the span category.
The mirror of derives_fwd_iff, at the backward slashing.
The NOD grammar over n words derives only permutations of the canonical linearization.
The four-word chain does not derive the order 2413, the paper's (g).
The four-word chain does not derive the order 3142, the paper's (j).
The typological record #
The position of a nominal category in the natural order of dominance of the paper's (1), which orders demonstrative, numeral, adjective and noun.
Equations
Instances For
Every order of demonstrative, numeral, adjective and noun that [Cin05] attests is a separable permutation of the natural order of dominance.
Among the twenty-four nominal orders, the non-separable ones are exactly the paper's (g) and (j), unattested in every survey.
The chance that a theory excluding e of N equiprobable orders is not falsified by a
attested orders sampled without replacement: the sets of a orders consistent with the theory
over all sets of a orders.
Equations
- StanojevicSteedman2021.chanceUnfalsified N e a = ↑((N - e).choose a) / ↑(N.choose a)
Instances For
Excluding two of the twenty-four orders and surviving twenty-one attested ones has a chance of about one in a hundred, the paper's (19).
With the twenty-second order accepted as attested the chance drops to one in 276, the paper's (20).