De Belder and van Craenenbroeck (2015): How to Merge a Root

Merge is asymmetric and unary: it selects a single item from the resource and pairs it with the object under construction, the selected item projecting. The first Merge of a derivation, Primary Merge, finds no object yet and pairs its item with the null derivation, the empty set, which leaves a radically empty terminal at the foot of the structure. That terminal is where a root is inserted after syntax. It has no features, it projects nothing and so has no category, it is a position rather than a kind of item, and it lies below all the functional material of its derivation. A phrase with several roots is built from layered derivations: each is spelled out and readmitted to the resource as an atom, opaque to later operations and unable to project, so that there is one root for every derivational workspace.

Since the root position has no features, Vocabulary Insertion may put any item into it, functional items included, and their features play no part in the syntax. Dutch uses wh-words, pronouns, conjunctions, articles and particles as roots, the pronoun ik 'I' in a root position triggers default third person agreement, and the conjunction maar 'but' used as a verb selects no clause. Neither an early insertion model, in which only featureless items are roots, nor a late insertion model that reserves root positions for items marked as roots derives these examples.

Main statements

• roots_eq_primaryMerges: every object a derivation builds has one root for each Primary Merge, that is, for each derivational workspace.
• derives_iff: of the models that let only featureless items or any item realize a root position, inserting items before or after syntax, only the one that inserts any item after syntax derives the Dutch examples.

Implementation notes

• An object's label is the bundle that projects in it. Following the refinement of (42), an item readmitted to the resource does not project, so its mother takes the label of its sister.
• An item is functional when it belongs to a closed class, as each example records. The person and number of ik are those of Dutch.Pronouns.ik; the wh-typing that waarom would bring to (2) is not modelled, and (10) and (11) carry the argument that an item in a root position has no syntactic effect.
• The early insertion model with featureless roots is Borer's exoskeletal model, and the late insertion model with root positions reserved for lexical items is that of a [Root] feature.

References

• [DBvC15]
• [Bor05]
• [HM93]
• [HN99b]

Unary Merge and the null derivation

inductive DeBelderVanCraenenbroeck2015.Obj (F : Type u) : Type u

An object of Unary Merge is the null derivation, or the ordered pair of an item selected from the resource with the object under construction.

• null {F : Type u} : Obj F

  The null derivation, the empty set Primary Merge pairs its item with.

• pair {F : Type u} : Item F → Obj F → Obj F

  The ordered pair of a selected item with the object under construction.

inductive DeBelderVanCraenenbroeck2015.Item (F : Type u) : Type u

An item of a resource is a bundle of grammatical features, or the output of an earlier derivation readmitted to the resource as an atom.

• bundle {F : Type u} : Finset F → Item F

  A bundle of grammatical features.

• atom {F : Type u} : Obj F → Item F

  An earlier derivation readmitted as an atom.

def DeBelderVanCraenenbroeck2015.Obj.IsNull {F : Type u} : Obj F → Prop

The object is the null derivation.

Equations

• DeBelderVanCraenenbroeck2015.Obj.null.IsNull = True
• (DeBelderVanCraenenbroeck2015.Obj.pair a a_1).IsNull = False

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instDecidableIsNull {F : Type u} (o : Obj F) : Decidable o.IsNull

Equations

• DeBelderVanCraenenbroeck2015.instDecidableIsNull DeBelderVanCraenenbroeck2015.Obj.null = { decide := true, reflects_decide := ⋯ }
• DeBelderVanCraenenbroeck2015.instDecidableIsNull (DeBelderVanCraenenbroeck2015.Obj.pair a a_1) = { decide := false, reflects_decide := ⋯ }

def DeBelderVanCraenenbroeck2015.Obj.label {F : Type u} : Obj F → Option (Finset F)

The bundle that projects in an object. A selected bundle projects; a readmitted atom cannot, and the null derivation, having no features, projects nothing.

Equations

• DeBelderVanCraenenbroeck2015.Obj.null.label = none
• (DeBelderVanCraenenbroeck2015.Obj.pair (DeBelderVanCraenenbroeck2015.Item.bundle f) a).label = some f
• (DeBelderVanCraenenbroeck2015.Obj.pair (DeBelderVanCraenenbroeck2015.Item.atom a) δ).label = δ.label

def DeBelderVanCraenenbroeck2015.Obj.roots {F : Type u} : Obj F → ℕ

The root positions of an object, its null derivations, those inside its atoms included.

Equations

• DeBelderVanCraenenbroeck2015.Obj.null.roots = 1
• (DeBelderVanCraenenbroeck2015.Obj.pair a a_1).roots = a.roots + a_1.roots

def DeBelderVanCraenenbroeck2015.Item.roots {F : Type u} : Item F → ℕ

The root positions of an item.

Equations

• (DeBelderVanCraenenbroeck2015.Item.bundle a).roots = 0
• (DeBelderVanCraenenbroeck2015.Item.atom o).roots = o.roots

def DeBelderVanCraenenbroeck2015.Obj.primaryMerges {F : Type u} : Obj F → ℕ

The Primary Merges of an object, the pairs whose object under construction is the null derivation.

Equations

• DeBelderVanCraenenbroeck2015.Obj.null.primaryMerges = 0
• (DeBelderVanCraenenbroeck2015.Obj.pair a DeBelderVanCraenenbroeck2015.Obj.null).primaryMerges = a.primaryMerges + 1
• (DeBelderVanCraenenbroeck2015.Obj.pair a (DeBelderVanCraenenbroeck2015.Obj.pair b δ)).primaryMerges = a.primaryMerges + (DeBelderVanCraenenbroeck2015.Obj.pair b δ).primaryMerges

def DeBelderVanCraenenbroeck2015.Item.primaryMerges {F : Type u} : Item F → ℕ

The Primary Merges of an item.

Equations

• (DeBelderVanCraenenbroeck2015.Item.bundle a).primaryMerges = 0
• (DeBelderVanCraenenbroeck2015.Item.atom o).primaryMerges = o.primaryMerges

structure DeBelderVanCraenenbroeck2015.State (F : Type u) : Type u

A state of a derivation, its resource and the object under construction.

• resource : List (Item F)
• object : Obj F

inductive DeBelderVanCraenenbroeck2015.Step {F : Type u} : State F → State F → Prop

A step of a derivation.

• merge {F : Type u} (R₁ R₂ : List (Item F)) (a : Item F) (δ : Obj F) : Step { resource := R₁ ++ a :: R₂, object := δ } { resource := R₁ ++ R₂, object := Obj.pair a δ }

  Unary Merge selects an item from the resource and pairs it with the object under construction.

• readmit {F : Type u} (R : List (Item F)) (a : Item F) (δ : Obj F) : Step { resource := R, object := Obj.pair a δ } { resource := Item.atom (Obj.pair a δ) :: R, object := Obj.null }

  The object is spelled out and readmitted to the resource as an atom, emptying the workspace for a new Primary Merge.

def DeBelderVanCraenenbroeck2015.State.init {F : Type u} (R : List (Finset F)) : State F

The state a derivation starts from, its resource of bundles and the null derivation.

Equations

• DeBelderVanCraenenbroeck2015.State.init R = { resource := List.map DeBelderVanCraenenbroeck2015.Item.bundle R, object := DeBelderVanCraenenbroeck2015.Obj.null }

def DeBelderVanCraenenbroeck2015.State.roots {F : Type u} (s : State F) : ℕ

The root positions of a state.

Equations

• s.roots = s.object.roots + (List.map DeBelderVanCraenenbroeck2015.Item.roots s.resource).sum

def DeBelderVanCraenenbroeck2015.State.primaryMerges {F : Type u} (s : State F) : ℕ

The Primary Merges of a state.

Equations

• s.primaryMerges = s.object.primaryMerges + (List.map DeBelderVanCraenenbroeck2015.Item.primaryMerges s.resource).sum

def DeBelderVanCraenenbroeck2015.State.Balanced {F : Type u} (s : State F) : Prop

A state has one root for each Primary Merge, and one more while its workspace is empty.

Equations

• s.Balanced = (s.roots = s.primaryMerges + if s.object.IsNull then 1 else 0)

theorem DeBelderVanCraenenbroeck2015.State.balanced_init {F : Type u} (R : List (Finset F)) : (init R).Balanced

theorem DeBelderVanCraenenbroeck2015.Step.balanced {F : Type u} {s t : State F} (h : Step s t) (hs : s.Balanced) : t.Balanced

theorem DeBelderVanCraenenbroeck2015.State.Balanced.of_reflTransGen {F : Type u} {s t : State F} (h : Relation.ReflTransGen Step s t) (hs : s.Balanced) : t.Balanced

theorem DeBelderVanCraenenbroeck2015.roots_eq_primaryMerges {F : Type u} {R : List (Finset F)} {o : Obj F} (h : Relation.ReflTransGen Step (State.init R) { resource := [], object := o }) (ho : ¬o.IsNull) : o.roots = o.primaryMerges

One derivational workspace, one root. Every object a derivation builds from a resource of bundles has one root for each Primary Merge, the first Merge of each derivational workspace.

def DeBelderVanCraenenbroeck2015.Obj.atoms {F : Type u} : Obj F → List (Obj F)

The atoms of an object's own workspace, the derivations readmitted to it, opaque to the operations of that workspace.

Equations

• DeBelderVanCraenenbroeck2015.Obj.null.atoms = []
• (DeBelderVanCraenenbroeck2015.Obj.pair (DeBelderVanCraenenbroeck2015.Item.bundle f) a).atoms = a.atoms
• (DeBelderVanCraenenbroeck2015.Obj.pair (DeBelderVanCraenenbroeck2015.Item.atom a) δ).atoms = a :: δ.atoms

def DeBelderVanCraenenbroeck2015.Obj.bundles {F : Type u} : Obj F → List (Finset F)

The bundles of an object's own workspace, open to its operations.

Equations

• DeBelderVanCraenenbroeck2015.Obj.null.bundles = []
• (DeBelderVanCraenenbroeck2015.Obj.pair (DeBelderVanCraenenbroeck2015.Item.bundle f) a).bundles = f :: a.bundles
• (DeBelderVanCraenenbroeck2015.Obj.pair (DeBelderVanCraenenbroeck2015.Item.atom a) δ).bundles = δ.bundles

The sample derivations

inductive DeBelderVanCraenenbroeck2015.Feature : Type

The grammatical features of the sample derivations.

• v : Feature
• f : Feature
• definite : Feature
• plural : Feature

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instDecidableEqFeature : DecidableEq Feature

Equations

• DeBelderVanCraenenbroeck2015.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instReprFeature : Repr Feature

Equations

• DeBelderVanCraenenbroeck2015.instReprFeature = { reprPrec := DeBelderVanCraenenbroeck2015.instReprFeature.repr }

def DeBelderVanCraenenbroeck2015.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

def DeBelderVanCraenenbroeck2015.theBooks : Obj Feature

the books of (18), the definite and plural features over the null derivation.

Equations

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

theorem DeBelderVanCraenenbroeck2015.derivation_theBooks : Relation.ReflTransGen Step (State.init [{Feature.definite}, {Feature.plural}]) { resource := [], object := theBooks }

The derivation (17)–(18) of the books from the resource of its definite and plural features.

theorem DeBelderVanCraenenbroeck2015.label_theBooks : theBooks.label = some {Feature.definite} ∧ theBooks.roots = 1

def DeBelderVanCraenenbroeck2015.dp : Obj Feature

A definite DP, its feature over the null derivation.

Equations

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

def DeBelderVanCraenenbroeck2015.vV : Obj Feature

The v-V complex, v over the null derivation.

Equations

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

def DeBelderVanCraenenbroeck2015.theChildEatsTheCookie : Obj Feature

In The child eats the cookie of (41) the subject and the v-V complex, each spelled out in a derivation of its own and readmitted as an atom, are merged over the direct object.

Equations

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

theorem DeBelderVanCraenenbroeck2015.derivation_theChildEatsTheCookie : Relation.ReflTransGen Step (State.init [{Feature.v}, {Feature.definite}, {Feature.definite}]) { resource := [], object := theChildEatsTheCookie }

The derivation (33)–(41) builds and readmits the subject, then the v-V complex, and builds the direct object last, merging the atoms over it.

theorem DeBelderVanCraenenbroeck2015.atoms_theChildEatsTheCookie : theChildEatsTheCookie.atoms = [dp, vV] ∧ theChildEatsTheCookie.bundles = [{Feature.definite}] ∧ theChildEatsTheCookie.roots = 3

In (41) the subject and the v-V complex are atoms, opaque to extraction, while the direct object's feature is open to it, and the clause has three roots.

def DeBelderVanCraenenbroeck2015.eatTheCookie : Obj Feature

eat the cookie of (42), the direct object merged with F⁰ and the v-V complex over them.

Equations

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

theorem DeBelderVanCraenenbroeck2015.derivation_eatTheCookie : Relation.ReflTransGen Step (State.init [{Feature.v}, {Feature.f}, {Feature.definite}]) { resource := [], object := eatTheCookie }

theorem DeBelderVanCraenenbroeck2015.label_eatTheCookie : eatTheCookie.label = some {Feature.f}

In (42) F⁰ labels the phrase, since the readmitted v-V complex cannot project.

Functional items in root positions

inductive DeBelderVanCraenenbroeck2015.ItemClass : Type

The items in root positions belong to the open class or to the closed classes of the functional items.

• lexical : ItemClass
• wh : ItemClass
• pronoun : ItemClass
• conjunction : ItemClass
• article : ItemClass
• particle : ItemClass
• adverb : ItemClass

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instDecidableEqItemClass : DecidableEq ItemClass

Equations

• DeBelderVanCraenenbroeck2015.instDecidableEqItemClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DeBelderVanCraenenbroeck2015.instReprItemClass.repr : ItemClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instReprItemClass : Repr ItemClass

Equations

• DeBelderVanCraenenbroeck2015.instReprItemClass = { reprPrec := DeBelderVanCraenenbroeck2015.instReprItemClass.repr }

inductive DeBelderVanCraenenbroeck2015.Realizers : Type

Which items may realize a root position.

• featureless : Realizers

  Only items without grammatical features, the lexical ones.

• any : Realizers

  Any item.

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instDecidableEqRealizers : DecidableEq Realizers

Equations

• DeBelderVanCraenenbroeck2015.instDecidableEqRealizers x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DeBelderVanCraenenbroeck2015.instReprRealizers.repr : Realizers → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instReprRealizers : Repr Realizers

Equations

• DeBelderVanCraenenbroeck2015.instReprRealizers = { reprPrec := DeBelderVanCraenenbroeck2015.instReprRealizers.repr }

inductive DeBelderVanCraenenbroeck2015.Insertion : Type

When items are inserted.

• early : Insertion

  Before syntax, their features visible to it.

• late : Insertion

  After syntax.

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instDecidableEqInsertion : DecidableEq Insertion

Equations

• DeBelderVanCraenenbroeck2015.instDecidableEqInsertion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DeBelderVanCraenenbroeck2015.instReprInsertion.repr : Insertion → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instReprInsertion : Repr Insertion

Equations

• DeBelderVanCraenenbroeck2015.instReprInsertion = { reprPrec := DeBelderVanCraenenbroeck2015.instReprInsertion.repr }

structure DeBelderVanCraenenbroeck2015.Model : Type

A model of root insertion says which items may realize a root position and when items are inserted.

• realizers : Realizers
• insertion : Insertion

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instDecidableEqModel : DecidableEq Model

Equations

• DeBelderVanCraenenbroeck2015.instDecidableEqModel = DeBelderVanCraenenbroeck2015.instDecidableEqModel.decEq

def DeBelderVanCraenenbroeck2015.instDecidableEqModel.decEq (x✝ x✝¹ : Model) : Decidable (x✝ = x✝¹)

Equations

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

def DeBelderVanCraenenbroeck2015.instReprModel.repr : Model → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instReprModel : Repr Model

Equations

• DeBelderVanCraenenbroeck2015.instReprModel = { reprPrec := DeBelderVanCraenenbroeck2015.instReprModel.repr }

def DeBelderVanCraenenbroeck2015.Model.exoSkeletal : Model

Borer's exoskeletal model, in which items are inserted early and the featureless ones are roots.

Equations

• DeBelderVanCraenenbroeck2015.Model.exoSkeletal = { realizers := DeBelderVanCraenenbroeck2015.Realizers.featureless, insertion := DeBelderVanCraenenbroeck2015.Insertion.early }

def DeBelderVanCraenenbroeck2015.Model.rootFeature : Model

Late insertion with a [Root] feature, which reserves root positions for lexical items.

Equations

• DeBelderVanCraenenbroeck2015.Model.rootFeature = { realizers := DeBelderVanCraenenbroeck2015.Realizers.featureless, insertion := DeBelderVanCraenenbroeck2015.Insertion.late }

def DeBelderVanCraenenbroeck2015.Model.primaryMerge : Model

Late insertion into the empty position of Primary Merge, which any item may realize.

Equations

• DeBelderVanCraenenbroeck2015.Model.primaryMerge = { realizers := DeBelderVanCraenenbroeck2015.Realizers.any, insertion := DeBelderVanCraenenbroeck2015.Insertion.late }

def DeBelderVanCraenenbroeck2015.Model.Realizes (M : Model) (c : ItemClass) : Prop

A model lets an item of a class realize a root position.

Equations

• M.Realizes c = (M.realizers = DeBelderVanCraenenbroeck2015.Realizers.any ∨ c = DeBelderVanCraenenbroeck2015.ItemClass.lexical)

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instDecidableRealizes (M : Model) (c : ItemClass) : Decidable (M.Realizes c)

Equations

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

inductive DeBelderVanCraenenbroeck2015.Phi : Type

The person and number features.

• person (p : Person) : Phi
• number (n : Number) : Phi

def DeBelderVanCraenenbroeck2015.instDecidableEqPhi.decEq (x✝ x✝¹ : Phi) : Decidable (x✝ = x✝¹)

Equations

• DeBelderVanCraenenbroeck2015.instDecidableEqPhi.decEq (DeBelderVanCraenenbroeck2015.Phi.person a) (DeBelderVanCraenenbroeck2015.Phi.person b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• DeBelderVanCraenenbroeck2015.instDecidableEqPhi.decEq (DeBelderVanCraenenbroeck2015.Phi.person p) (DeBelderVanCraenenbroeck2015.Phi.number n) = isFalse ⋯
• DeBelderVanCraenenbroeck2015.instDecidableEqPhi.decEq (DeBelderVanCraenenbroeck2015.Phi.number n) (DeBelderVanCraenenbroeck2015.Phi.person p) = isFalse ⋯
• DeBelderVanCraenenbroeck2015.instDecidableEqPhi.decEq (DeBelderVanCraenenbroeck2015.Phi.number a) (DeBelderVanCraenenbroeck2015.Phi.number b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instDecidableEqPhi : DecidableEq Phi

Equations

• DeBelderVanCraenenbroeck2015.instDecidableEqPhi = DeBelderVanCraenenbroeck2015.instDecidableEqPhi.decEq

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instReprPhi : Repr Phi

Equations

• DeBelderVanCraenenbroeck2015.instReprPhi = { reprPrec := DeBelderVanCraenenbroeck2015.instReprPhi.repr }

def DeBelderVanCraenenbroeck2015.instReprPhi.repr : Phi → ℕ → Std.Format

Equations

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

def DeBelderVanCraenenbroeck2015.phiOf (p : Pronoun) : List Phi

The person and number of a pronoun.

Equations

• DeBelderVanCraenenbroeck2015.phiOf p = List.map DeBelderVanCraenenbroeck2015.Phi.person p.person.toList ++ List.map DeBelderVanCraenenbroeck2015.Phi.number p.number.toList

def DeBelderVanCraenenbroeck2015.zijn : Morphology.Exponence.RuleSet (DistributedMorphology.VocabularyItem Phi String)

The present forms of zijn 'be', third person singular is the Elsewhere form.

Equations

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

def DeBelderVanCraenenbroeck2015.Model.visiblePhi (M : Model) : List Phi

ik in a root position brings its own person and number to the syntax when it is inserted early, and none when it is inserted late.

Equations

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

def DeBelderVanCraenenbroeck2015.Model.copula (M : Model) : Option String

The copula agreeing with a subject whose root position ik realizes.

Equations

• M.copula = DistributedMorphology.subsetPrinciple DeBelderVanCraenenbroeck2015.zijn ↑M.visiblePhi

inductive DeBelderVanCraenenbroeck2015.Construction : Type

An example tests whether an item may be in a root position, the agreement it triggers there, or the complement it selects there.

• rootPosition : Construction
• agreement : Construction
• selection : Construction

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instDecidableEqConstruction : DecidableEq Construction

Equations

• DeBelderVanCraenenbroeck2015.instDecidableEqConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DeBelderVanCraenenbroeck2015.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instReprConstruction : Repr Construction

Equations

• DeBelderVanCraenenbroeck2015.instReprConstruction = { reprPrec := DeBelderVanCraenenbroeck2015.instReprConstruction.repr }

def DeBelderVanCraenenbroeck2015.Model.Accepts (M : Model) (c : ItemClass) (form : Option String) : Construction → Prop

A model predicts an item of a class acceptable in a construction, with the copula form. An item of a functional class selects a clause only when its features are visible to syntax.

Equations

• M.Accepts c form DeBelderVanCraenenbroeck2015.Construction.rootPosition = M.Realizes c
• M.Accepts c form DeBelderVanCraenenbroeck2015.Construction.agreement = (M.Realizes c ∧ M.copula = form)
• M.Accepts c form DeBelderVanCraenenbroeck2015.Construction.selection = (M.Realizes c ∧ M.insertion = DeBelderVanCraenenbroeck2015.Insertion.early)

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instDecidableAccepts (M : Model) (c : ItemClass) (form : Option String) (k : Construction) : Decidable (M.Accepts c form k)

Equations

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

def DeBelderVanCraenenbroeck2015.classTable : List (String × ItemClass)

The classes as named in the rows.

Equations

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

def DeBelderVanCraenenbroeck2015.constructionTable : List (String × Construction)

The constructions as named in the rows.

Equations

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

def DeBelderVanCraenenbroeck2015.data : List (Construction × ItemClass × Option String × Judgment)

The examples (2)–(11), each with its construction, the class of the item in the root position, the copula of the agreement example, and the judgment.

Equations

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

theorem DeBelderVanCraenenbroeck2015.data_length : data.length = Examples.all.length

def DeBelderVanCraenenbroeck2015.Model.Derives (M : Model) : Prop

A model derives the examples when it accepts exactly the acceptable ones.

Equations

• M.Derives = ∀ r ∈ DeBelderVanCraenenbroeck2015.data, r.2.2.2 = Judgment.acceptable ↔ M.Accepts r.2.1 r.2.2.1 r.1

@[instance_reducible]

instance DeBelderVanCraenenbroeck2015.instDecidableDerives (M : Model) : Decidable M.Derives

Equations

• DeBelderVanCraenenbroeck2015.instDecidableDerives M = DeBelderVanCraenenbroeck2015.instDecidableDerives._aux_1 M

theorem DeBelderVanCraenenbroeck2015.derives_iff (M : Model) : M.Derives ↔ M = Model.primaryMerge

Roots are defined structurally, and inserted late. Only the model that lets any item realize a root position and inserts items after syntax derives the examples: the exoskeletal and the [Root] feature models exclude the functional items of (2)–(9), and inserting them early would give ik first person agreement in (10) and maar its clause in (11).