van Craenenbroeck (2014): On diagnosing complement-taking roots

Harley argues that roots take complements from criteria that should diagnose one structure: a noun and a verb of one root select their objects alike, one strands adjuncts and not arguments, and an idiom built from a root and its object alone passivizes and nominalizes. The commentary finds the criteria mismatched. In English and Frisian an argument that a noun and a verb select alike can still be stranded by a proform, as only adjuncts were to be, and Dutch idioms that passivize and survive as nominalized infinitives lose their reading under a nominalizing suffix. Arguments, like adjuncts, would then be severed from the root, introduced by a functional head over it, and proforms would stand for phrases at different heights.

The mismatch is that pronominalization and selection read different properties of a configuration. A proform strands the argument when a phrase of its category separates the argument from the root, and a noun and a verb select their objects alike when the argument is merged with a head that categorizes nothing. Taking the argument as its complement, the root is not separated from it; with the argument in the specifier of the categorizer, the categorizer selects it. Only the argument in the specifier of a functional head over the root has both properties.

Main statements

• derives_iff: of the root taking the argument as its complement, the root modifying the categorizer, the argument in the specifier of the categorizer, and the argument in the specifier of a functional head over the root, only the last derives the selection and the pronominalization examples.
• not_fits: no idiom domain derives the judgments of the idioms that passivize and survive as nominalized infinitives.

Implementation notes

• A proform stands for a phrase of its category, and a selection restriction relates an argument to the head it is merged with. A configuration chooses the category of each proform, and the to that introduces the stranded argument of (11) is set aside, as the paper does.
• The configurations are shapes without words, which play no part in either reading; that of (14) is the functional projection as printed, without the categorizer above it.
• An idiom's domain is the root's phrase, vP or VoiceP, as in the classification the paper adopts. An idiomatic reading survives a form that alters no head of its domain: the passive alters Voice, and the nominalized infinitive, the Dutch counterpart of the English gerund, and the suffixal nominalization alter v.

References

• [vC14]
• [Har14b]
• [Emb04]

Pronominalization and selection

inductive VanCraenenbroeck2014.Config : Type

In the configurations of a root and its argument, the root takes the argument as its complement, as in (12), or modifies the categorizer whose complement it is, or the argument is in the specifier of the categorizer, or in the specifier of a functional head over the root, as in (14).

• complement : Config
• modifier : Config
• specifier : Config
• severed : Config

@[instance_reducible]

instance VanCraenenbroeck2014.instDecidableEqConfig : DecidableEq Config

Equations

• VanCraenenbroeck2014.instDecidableEqConfig x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VanCraenenbroeck2014.instReprConfig.repr : Config → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VanCraenenbroeck2014.instReprConfig : Repr Config

Equations

• VanCraenenbroeck2014.instReprConfig = { reprPrec := VanCraenenbroeck2014.instReprConfig.repr }

def VanCraenenbroeck2014.Config.tree (x : DistributedMorphology.Categorizer) : Config → PhraseStructure.Tree DistributedMorphology.RootCategorization.Cat Unit

A configuration's phrase under a categorizer.

Equations

• One or more equations did not get rendered due to their size.
• VanCraenenbroeck2014.Config.tree x VanCraenenbroeck2014.Config.specifier = DistributedMorphology.RootCategorization.specifierTree { x := x, root := (), head := (), arg := () }

def VanCraenenbroeck2014.Config.rootPos : Config → Core.Order.TreePath

The position of the root.

Equations

• VanCraenenbroeck2014.Config.complement.rootPos = { toList := [0, 0] }
• VanCraenenbroeck2014.Config.modifier.rootPos = { toList := [0, 0] }
• VanCraenenbroeck2014.Config.specifier.rootPos = { toList := [1, 0, 0] }
• VanCraenenbroeck2014.Config.severed.rootPos = { toList := [1, 1] }

def VanCraenenbroeck2014.Config.argPos : Config → Core.Order.TreePath

The position of the argument.

Equations

• VanCraenenbroeck2014.Config.complement.argPos = { toList := [1, 1] }
• VanCraenenbroeck2014.Config.modifier.argPos = { toList := [1] }
• VanCraenenbroeck2014.Config.specifier.argPos = { toList := [0] }
• VanCraenenbroeck2014.Config.severed.argPos = { toList := [0] }

inductive VanCraenenbroeck2014.Use : Type

A proform strands the argument or includes it.

• stranded : Use
• included : Use

@[instance_reducible]

instance VanCraenenbroeck2014.instDecidableEqUse : DecidableEq Use

Equations

• VanCraenenbroeck2014.instDecidableEqUse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VanCraenenbroeck2014.instReprUse : Repr Use

Equations

• VanCraenenbroeck2014.instReprUse = { reprPrec := VanCraenenbroeck2014.instReprUse.repr }

def VanCraenenbroeck2014.instReprUse.repr : Use → ℕ → Std.Format

Equations

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

def VanCraenenbroeck2014.Config.Licenses (c : Config) (x : DistributedMorphology.Categorizer) (X : DistributedMorphology.RootCategorization.Cat) : Use → Prop

A proform of category X may stand for a phrase that contains the root and strands or includes the argument.

Equations

• One or more equations did not get rendered due to their size.
• c.Licenses x X VanCraenenbroeck2014.Use.stranded = DistributedMorphology.Strands X (VanCraenenbroeck2014.Config.tree x c) c.rootPos c.argPos

@[instance_reducible]

instance VanCraenenbroeck2014.instDecidableLicenses (c : Config) (x : DistributedMorphology.Categorizer) (X : DistributedMorphology.RootCategorization.Cat) (u : Use) : Decidable (c.Licenses x X u)

Equations

• VanCraenenbroeck2014.instDecidableLicenses c x X VanCraenenbroeck2014.Use.stranded = VanCraenenbroeck2014.instDecidableLicenses._aux_1 c x X
• VanCraenenbroeck2014.instDecidableLicenses c x X VanCraenenbroeck2014.Use.included = VanCraenenbroeck2014.instDecidableLicenses._aux_3 c x X

inductive VanCraenenbroeck2014.Proform : Type

The proforms of (11), (13) and (17), English the same or likewise and Frisian ien.

• sameLikewise : Proform
• ien : Proform

@[instance_reducible]

instance VanCraenenbroeck2014.instDecidableEqProform : DecidableEq Proform

Equations

• VanCraenenbroeck2014.instDecidableEqProform x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VanCraenenbroeck2014.instReprProform.repr : Proform → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VanCraenenbroeck2014.instReprProform : Repr Proform

Equations

• VanCraenenbroeck2014.instReprProform = { reprPrec := VanCraenenbroeck2014.instReprProform.repr }

def VanCraenenbroeck2014.proformTable : List (String × Proform)

The proforms as named in the rows.

Equations

• VanCraenenbroeck2014.proformTable = [("the same/likewise", VanCraenenbroeck2014.Proform.sameLikewise), ("ien", VanCraenenbroeck2014.Proform.ien)]

def VanCraenenbroeck2014.categoryTable : List (String × DistributedMorphology.Categorizer)

The categories as named in the rows.

Equations

• VanCraenenbroeck2014.categoryTable = [("verb", DistributedMorphology.Categorizer.v), ("noun", DistributedMorphology.Categorizer.n)]

def VanCraenenbroeck2014.useTable : List (String × Use)

The uses as named in the rows.

Equations

• VanCraenenbroeck2014.useTable = [("stranded", VanCraenenbroeck2014.Use.stranded), ("included", VanCraenenbroeck2014.Use.included)]

def VanCraenenbroeck2014.selectionData : List DistributedMorphology.Categorizer

The categories of the selection examples (10) and (15).

Equations

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

def VanCraenenbroeck2014.pronominalizationData : List (DistributedMorphology.Categorizer × Proform × Use × Judgment)

The pronominalization examples (11), (13) and (17), each with the category of the pronominalized phrase, the proform, its use and the judgment.

Equations

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

theorem VanCraenenbroeck2014.length_data : selectionData.length = 4 ∧ pronominalizationData.length = 4

def VanCraenenbroeck2014.Config.Derives (c : Config) : Prop

A configuration derives the examples when the argument is merged with one head in the nouns and the verbs of the selection examples, and each proform has a category that licenses exactly the uses the pronominalization examples accept.

Equations

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

@[instance_reducible]

instance VanCraenenbroeck2014.instDecidableDerives (c : Config) : Decidable c.Derives

Equations

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

theorem VanCraenenbroeck2014.derives_iff (c : Config) : c.Derives ↔ c = Config.severed

Only the severed argument derives the examples. Where the root takes the argument as its complement or modifies the categorizer no proform strands the argument, as RootCategorization.not_strands_argPos shows in every context; where the argument is in the specifier of the categorizer, the verb and the noun merge it with different heads.

Idiomatization

inductive VanCraenenbroeck2014.Domain : Type

The domain of an idiom, the root's phrase, vP or VoiceP.

• root : Domain
• v : Domain
• voice : Domain

@[instance_reducible]

instance VanCraenenbroeck2014.instDecidableEqDomain : DecidableEq Domain

Equations

• VanCraenenbroeck2014.instDecidableEqDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VanCraenenbroeck2014.instReprDomain.repr : Domain → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VanCraenenbroeck2014.instReprDomain : Repr Domain

Equations

• VanCraenenbroeck2014.instReprDomain = { reprPrec := VanCraenenbroeck2014.instReprDomain.repr }

def VanCraenenbroeck2014.Domain.rank : Domain → ℕ

The height of a domain's head on the clausal spine.

Equations

• VanCraenenbroeck2014.Domain.root.rank = 0
• VanCraenenbroeck2014.Domain.v.rank = 1
• VanCraenenbroeck2014.Domain.voice.rank = 2

inductive VanCraenenbroeck2014.Form : Type

The forms of an idiom in (18)–(22).

• active : Form
• passive : Form
• nominalizedInfinitive : Form
• nominalization : Form

@[instance_reducible]

instance VanCraenenbroeck2014.instDecidableEqForm : DecidableEq Form

Equations

• VanCraenenbroeck2014.instDecidableEqForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VanCraenenbroeck2014.instReprForm.repr : Form → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VanCraenenbroeck2014.instReprForm : Repr Form

Equations

• VanCraenenbroeck2014.instReprForm = { reprPrec := VanCraenenbroeck2014.instReprForm.repr }

def VanCraenenbroeck2014.Form.altered : Form → Option Domain

The lowest head a form alters.

Equations

• VanCraenenbroeck2014.Form.active.altered = none
• VanCraenenbroeck2014.Form.passive.altered = some VanCraenenbroeck2014.Domain.voice
• VanCraenenbroeck2014.Form.nominalizedInfinitive.altered = some VanCraenenbroeck2014.Domain.v
• VanCraenenbroeck2014.Form.nominalization.altered = some VanCraenenbroeck2014.Domain.v

def VanCraenenbroeck2014.Survives (d : Domain) (f : Form) : Prop

An idiomatic reading survives a form that alters no head of its domain.

Equations

• VanCraenenbroeck2014.Survives d f = ∀ h ∈ f.altered, d.rank < h.rank

@[instance_reducible]

instance VanCraenenbroeck2014.instDecidableSurvives (d : Domain) (f : Form) : Decidable (Survives d f)

Equations

• VanCraenenbroeck2014.instDecidableSurvives d f = VanCraenenbroeck2014.instDecidableSurvives._aux_1 d f

inductive VanCraenenbroeck2014.Idiom : Type

The idioms of (18)–(22) are iemand de bons geven 'dump someone', iemand de das omdoen 'be the end of someone', de strijdbijl begraven 'bury the hatchet' and het ijs breken 'break the ice'.

• bons : Idiom
• das : Idiom
• strijdbijl : Idiom
• ijs : Idiom

@[instance_reducible]

instance VanCraenenbroeck2014.instDecidableEqIdiom : DecidableEq Idiom

Equations

• VanCraenenbroeck2014.instDecidableEqIdiom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VanCraenenbroeck2014.instReprIdiom.repr : Idiom → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VanCraenenbroeck2014.instReprIdiom : Repr Idiom

Equations

• VanCraenenbroeck2014.instReprIdiom = { reprPrec := VanCraenenbroeck2014.instReprIdiom.repr }

def VanCraenenbroeck2014.idiomTable : List (String × Idiom)

The idioms as named in the rows.

Equations

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

def VanCraenenbroeck2014.formTable : List (String × Form)

The forms as named in the rows.

Equations

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

def VanCraenenbroeck2014.idiomData : List (Idiom × Form × Judgment)

The idiom examples, the idiom and its form with the judgment of its idiomatic reading.

Equations

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

theorem VanCraenenbroeck2014.length_idiomData : idiomData.length = 14

def VanCraenenbroeck2014.Fits (i : Idiom) (d : Domain) : Prop

An idiom fits a domain when its reading survives exactly the forms its examples accept.

Equations

• VanCraenenbroeck2014.Fits i d = ∀ r ∈ VanCraenenbroeck2014.idiomData, r.1 = i → (r.2.2 = Judgment.acceptable ↔ VanCraenenbroeck2014.Survives d r.2.1)

@[instance_reducible]

instance VanCraenenbroeck2014.instDecidableFits (i : Idiom) (d : Domain) : Decidable (Fits i d)

Equations

• VanCraenenbroeck2014.instDecidableFits i d = VanCraenenbroeck2014.instDecidableFits._aux_1 i d

theorem VanCraenenbroeck2014.fits_bons_iff (d : Domain) : Fits Idiom.bons d ↔ d = Domain.voice

iemand de bons geven, which neither passivizes nor nominalizes, is an idiom of VoiceP.

theorem VanCraenenbroeck2014.fits_das_iff (d : Domain) : Fits Idiom.das d ↔ d = Domain.v

iemand de das omdoen, which passivizes and does not nominalize, is an idiom of vP.

theorem VanCraenenbroeck2014.not_fits (d : Domain) : ¬Fits Idiom.strijdbijl d ∧ ¬Fits Idiom.ijs d

No domain fits. The idioms that passivize and survive as nominalized infinitives should be built from the root and its object alone, and then survive the suffixal nominalization too.