Embick (2004): On the structure of resultative participles in English

The verbalizer v[FIENT] denotes a transition toward a state, and a Root combines with it in one of two ways. As its complement, the Root names the state the transition reaches, so The metal is flattened is the state of having become flat. Merged with it in a single complex head, Direct Merge, the Root names the means of the transition, so John hammered the metal flat is becoming flat by hammering, the complement of v[FIENT] then being a full aP. The Root is v[FIENT]'s sister either way, so sisterhood does not tell the two apart: the complement is projected over, the directly merged Root adjoined. A condition that the complement of every v[FIENT] be predicated of the DP in its specifier derives the Direct Object Restriction and the gaps among resultative participles.

Of the configurations in which Distributed Morphology lets a categorizer categorize a Root, as its complement or as a modifier merged with it, this analysis uses both. Head movement brings a Root complement into the head, where it forms the complex head that Direct Merge builds, so Vocabulary Insertion, which realizes complex heads, cannot tell the two configurations apart: only their interpretation does.

Main statements

• headDaughter?_moveRoot: head movement of a Root complement builds the complex head of Direct Merge, so every vocabulary realizes v[FIENT] alike in the two (realize_moveRoot).
• isSegment_directMerge: the Root is v[FIENT]'s sister in both structures, projected over as a complement and adjoined under Direct Merge.
• interp_directMerge: a directly merged Root is the means and the aP the result.
• acceptable_iff_interpretable: the condition on v[FIENT] and the argument structure of Roots derive the judgments.

Implementation notes

• The domain of v[FIENT] is recorded by the DP in its specifier, a Root directly merged with it, and its complement, a bare Root, an aP, or a resultative participle with its own v[FIENT]. Event variables are left out, as the paper leaves them out, and the FIENT(P)(x) of the means rule is read as FIENT(P(x)), as its application to hammer flat does.
• Which half of the means rule applies, whether the merged Root takes the DP as its argument, depends on the example, so each row records it. Argument taking is recorded only for the Roots that the rows put in complement position.

TODO

The dative gap (John is given a book), the Asp heads that make participles stative, and the diagnostics separating resultative from stative participles are not formalized.

References

• [Emb04]

Roots

inductive Embick2004.Root : Type

The Roots of the examples.

• hammer : Root
• flat : Root
• laugh : Root
• hoarse : Root
• freeze : Root
• solid : Root
• smoke : Root
• thin : Root
• kick : Root
• open : Root

@[instance_reducible]

instance Embick2004.instDecidableEqRoot : DecidableEq Root

Equations

• Embick2004.instDecidableEqRoot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Embick2004.instReprRoot.repr : Root → ℕ → Std.Format

Equations

• Embick2004.instReprRoot.repr Embick2004.Root.hammer prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Root.hammer")).group prec✝
• Embick2004.instReprRoot.repr Embick2004.Root.flat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Root.flat")).group prec✝
• Embick2004.instReprRoot.repr Embick2004.Root.laugh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Root.laugh")).group prec✝
• Embick2004.instReprRoot.repr Embick2004.Root.hoarse prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Root.hoarse")).group prec✝
• Embick2004.instReprRoot.repr Embick2004.Root.freeze prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Root.freeze")).group prec✝
• Embick2004.instReprRoot.repr Embick2004.Root.solid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Root.solid")).group prec✝
• Embick2004.instReprRoot.repr Embick2004.Root.smoke prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Root.smoke")).group prec✝
• Embick2004.instReprRoot.repr Embick2004.Root.thin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Root.thin")).group prec✝
• Embick2004.instReprRoot.repr Embick2004.Root.kick prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Root.kick")).group prec✝
• Embick2004.instReprRoot.repr Embick2004.Root.open prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Root.open")).group prec✝

@[instance_reducible]

instance Embick2004.instReprRoot : Repr Root

Equations

• Embick2004.instReprRoot = { reprPrec := Embick2004.instReprRoot.repr }

inductive Embick2004.DP : Type

The DPs of the examples.

• john : DP
• theMetal : DP
• theRiver : DP
• theDoor : DP
• himself : DP

@[instance_reducible]

instance Embick2004.instDecidableEqDP : DecidableEq DP

Equations

• Embick2004.instDecidableEqDP x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Embick2004.instReprDP : Repr DP

Equations

• Embick2004.instReprDP = { reprPrec := Embick2004.instReprDP.repr }

def Embick2004.instReprDP.repr : DP → ℕ → Std.Format

Equations

• Embick2004.instReprDP.repr Embick2004.DP.john prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.DP.john")).group prec✝
• Embick2004.instReprDP.repr Embick2004.DP.theMetal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.DP.theMetal")).group prec✝
• Embick2004.instReprDP.repr Embick2004.DP.theRiver prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.DP.theRiver")).group prec✝
• Embick2004.instReprDP.repr Embick2004.DP.theDoor prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.DP.theDoor")).group prec✝
• Embick2004.instReprDP.repr Embick2004.DP.himself prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.DP.himself")).group prec✝

def Embick2004.TakesArgument (r : Root) : Prop

√HAMMER and √FLAT take an argument and √LAUGH takes none (§4.1).

Equations

• Embick2004.TakesArgument r = (r = Embick2004.Root.hammer ∨ r = Embick2004.Root.flat)

@[instance_reducible]

instance Embick2004.instDecidablePredRootTakesArgument : DecidablePred TakesArgument

Equations

• Embick2004.instDecidablePredRootTakesArgument x✝ = { decide := decide (x✝ = Embick2004.Root.hammer) || decide (x✝ = Embick2004.Root.flat), reflects_decide := ⋯ }

The two configurations

inductive Embick2004.Cat : Type

The categories are the verbalizer, the Root's own, the adjectivizer, aspect and determiner phrases.

• v : Cat
• root : Cat
• a : Cat
• asp : Cat
• d : Cat

@[instance_reducible]

instance Embick2004.instDecidableEqCat : DecidableEq Cat

Equations

• Embick2004.instDecidableEqCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Embick2004.instReprCat : Repr Cat

Equations

• Embick2004.instReprCat = { reprPrec := Embick2004.instReprCat.repr }

def Embick2004.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• Embick2004.instReprCat.repr Embick2004.Cat.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Cat.v")).group prec✝
• Embick2004.instReprCat.repr Embick2004.Cat.root prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Cat.root")).group prec✝
• Embick2004.instReprCat.repr Embick2004.Cat.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Cat.a")).group prec✝
• Embick2004.instReprCat.repr Embick2004.Cat.asp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Cat.asp")).group prec✝
• Embick2004.instReprCat.repr Embick2004.Cat.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Cat.d")).group prec✝

inductive Embick2004.Word : Type

The terminals are v[FIENT], Roots, the adjectivizer, AspR and DPs.

• fient : Word
• root (r : Root) : Word
• adj : Word
• aspR : Word
• dp (x : DP) : Word

@[instance_reducible]

instance Embick2004.instDecidableEqWord : DecidableEq Word

Equations

• Embick2004.instDecidableEqWord = Embick2004.instDecidableEqWord.decEq

def Embick2004.instDecidableEqWord.decEq (x✝ x✝¹ : Word) : Decidable (x✝ = x✝¹)

Equations

• Embick2004.instDecidableEqWord.decEq Embick2004.Word.fient Embick2004.Word.fient = isTrue ⋯
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.fient (Embick2004.Word.root r) = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.fient Embick2004.Word.adj = isFalse Embick2004.instDecidableEqWord.decEq._proof_4
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.fient Embick2004.Word.aspR = isFalse Embick2004.instDecidableEqWord.decEq._proof_5
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.fient (Embick2004.Word.dp x_2) = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq (Embick2004.Word.root r) Embick2004.Word.fient = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq (Embick2004.Word.root a) (Embick2004.Word.root b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Embick2004.instDecidableEqWord.decEq (Embick2004.Word.root r) Embick2004.Word.adj = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq (Embick2004.Word.root r) Embick2004.Word.aspR = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq (Embick2004.Word.root r) (Embick2004.Word.dp x_2) = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.adj Embick2004.Word.fient = isFalse Embick2004.instDecidableEqWord.decEq._proof_12
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.adj (Embick2004.Word.root r) = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.adj Embick2004.Word.adj = isTrue ⋯
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.adj Embick2004.Word.aspR = isFalse Embick2004.instDecidableEqWord.decEq._proof_14
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.adj (Embick2004.Word.dp x_2) = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.aspR Embick2004.Word.fient = isFalse Embick2004.instDecidableEqWord.decEq._proof_16
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.aspR (Embick2004.Word.root r) = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.aspR Embick2004.Word.adj = isFalse Embick2004.instDecidableEqWord.decEq._proof_18
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.aspR Embick2004.Word.aspR = isTrue ⋯
• Embick2004.instDecidableEqWord.decEq Embick2004.Word.aspR (Embick2004.Word.dp x_2) = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq (Embick2004.Word.dp x_2) Embick2004.Word.fient = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq (Embick2004.Word.dp x_2) (Embick2004.Word.root r) = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq (Embick2004.Word.dp x_2) Embick2004.Word.adj = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq (Embick2004.Word.dp x_2) Embick2004.Word.aspR = isFalse ⋯
• Embick2004.instDecidableEqWord.decEq (Embick2004.Word.dp a) (Embick2004.Word.dp b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Embick2004.instReprWord.repr : Word → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Embick2004.instReprWord.repr Embick2004.Word.fient prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Word.fient")).group prec✝
• Embick2004.instReprWord.repr Embick2004.Word.adj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Word.adj")).group prec✝
• Embick2004.instReprWord.repr Embick2004.Word.aspR prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Word.aspR")).group prec✝

@[instance_reducible]

instance Embick2004.instReprWord : Repr Word

Equations

• Embick2004.instReprWord = { reprPrec := Embick2004.instReprWord.repr }

def Embick2004.rootComplement (r : Root) : PhraseStructure.Tree Cat Word

The Root complement structure (47), v[FIENT] taking the Root as its complement.

Equations

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

def Embick2004.directMerge (r : Root) : PhraseStructure.Tree Cat Word

The complex head that Direct Merge builds (48), the Root adjoined to v[FIENT].

Equations

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

theorem Embick2004.children_perm (r : Root) : (RoseTree.children (rootComplement r)).Perm (RoseTree.children (directMerge r))

The Root and v[FIENT] are sisters in both structures.

theorem Embick2004.headIndex?_rootComplement (r : Root) : (rootComplement r).headIndex? = some 0

v[FIENT] heads both structures, as the daughter of their category.

theorem Embick2004.headIndex?_directMerge (r : Root) : (directMerge r).headIndex? = some 1

theorem Embick2004.isSegment_directMerge (r : Root) : ¬(RoseTree.value (rootComplement r)).IsSegment ∧ (RoseTree.value (directMerge r)).IsSegment

What tells the structures apart is how v[FIENT] heads them: a Root complement is projected over, while a directly merged Root makes the mother a further segment of v[FIENT].

Head movement and Vocabulary Insertion

def Embick2004.moveRoot : PhraseStructure.Tree Cat Word → PhraseStructure.Tree Cat Word

Head movement of a bare Root complement adjoins the Root to the head it is the complement of, leaving a trace.

Equations

• One or more equations did not get rendered due to their size.
• Embick2004.moveRoot x✝ = x✝

def Embick2004.headDaughter? (t : PhraseStructure.Tree Cat Word) : Option (PhraseStructure.Tree Cat Word)

The head daughter of a tree.

Equations

• Embick2004.headDaughter? t = t.headIndex?.bind fun (x : ℕ) => (RoseTree.children t)[x]?

theorem Embick2004.headDaughter?_moveRoot (r : Root) : headDaughter? (moveRoot (rootComplement r)) = some (directMerge r)

Head movement of a Root complement builds exactly the complex head of Direct Merge.

def Embick2004.complexHead? : PhraseStructure.Tree Cat Word → Option (DistributedMorphology.ComplexHead Root Word)

A complex head of v[FIENT] with a Root adjoined, read as the Root with the head above it.

Equations

• One or more equations did not get rendered due to their size.
• Embick2004.complexHead? x✝ = none

inductive Embick2004.Feature : Type

The features Vocabulary Items mention, v[FIENT] and the identity of a Root.

• fient : Feature
• root (r : Root) : Feature

def Embick2004.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) : Decidable (x✝ = x✝¹)

Equations

• Embick2004.instDecidableEqFeature.decEq Embick2004.Feature.fient Embick2004.Feature.fient = isTrue ⋯
• Embick2004.instDecidableEqFeature.decEq Embick2004.Feature.fient (Embick2004.Feature.root r) = isFalse ⋯
• Embick2004.instDecidableEqFeature.decEq (Embick2004.Feature.root r) Embick2004.Feature.fient = isFalse ⋯
• Embick2004.instDecidableEqFeature.decEq (Embick2004.Feature.root a) (Embick2004.Feature.root b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Embick2004.instDecidableEqFeature : DecidableEq Feature

Equations

• Embick2004.instDecidableEqFeature = Embick2004.instDecidableEqFeature.decEq

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

Equations

• One or more equations did not get rendered due to their size.
• Embick2004.instReprFeature.repr Embick2004.Feature.fient prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2004.Feature.fient")).group prec✝

@[instance_reducible]

instance Embick2004.instReprFeature : Repr Feature

Equations

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

def Embick2004.realize (vocab : List (DistributedMorphology.VocabularyItem Feature String)) (w : DistributedMorphology.ComplexHead Root Word) : Option String

The exponent a vocabulary inserts at v[FIENT] in a complex head, with the Root as its inner context.

Equations

• Embick2004.realize vocab w = DistributedMorphology.subsetPrinciple vocab { focus := [Embick2004.Feature.fient], leftCtx := [[Embick2004.Feature.root w.root]] }

def Embick2004.vocabulary : List (DistributedMorphology.VocabularyItem Feature String)

v[FIENT] is spelled out as -en next to √FLAT and as null next to √HAMMER (fn. 24).

Equations

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

theorem Embick2004.realize_flat : realize vocabulary { root := Root.flat, heads := [Word.fient] } = some "-en"

theorem Embick2004.realize_hammer : realize vocabulary { root := Root.hammer, heads := [Word.fient] } = some ""

theorem Embick2004.realize_moveRoot (vocab : List (DistributedMorphology.VocabularyItem Feature String)) (r : Root) : Option.map (realize vocab) ((headDaughter? (moveRoot (rootComplement r))).bind complexHead?) = Option.map (realize vocab) (complexHead? (directMerge r))

Every vocabulary realizes v[FIENT] alike whether its Root moved from complement position or was directly merged, so hammer-ed has the null v[FIENT] of hammer-ed flat.

Interpretation

inductive Embick2004.MeansRule : Type

The means rule (49) has two halves, as the directly merged Root takes the DP in the specifier as its argument or takes none.

• argument : MeansRule
• noArgument : MeansRule

@[instance_reducible]

instance Embick2004.instDecidableEqMeansRule : DecidableEq MeansRule

Equations

• Embick2004.instDecidableEqMeansRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Embick2004.instReprMeansRule.repr : MeansRule → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Embick2004.instReprMeansRule : Repr MeansRule

Equations

• Embick2004.instReprMeansRule = { reprPrec := Embick2004.instReprMeansRule.repr }

inductive Embick2004.Complement : Type

The complement of v[FIENT] is a bare Root, an aP over a Root, or a resultative participle, AspR over a lower v[FIENT] with its own specifier and Root complement (58).

• root (r : Root) : Complement
• aP (r : Root) : Complement
• participle (spec : Option DP) (r : Root) : Complement

def Embick2004.instDecidableEqComplement.decEq (x✝ x✝¹ : Complement) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Embick2004.instDecidableEqComplement.decEq (Embick2004.Complement.root a) (Embick2004.Complement.root b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Embick2004.instDecidableEqComplement.decEq (Embick2004.Complement.root r) (Embick2004.Complement.aP r_1) = isFalse ⋯
• Embick2004.instDecidableEqComplement.decEq (Embick2004.Complement.root r) (Embick2004.Complement.participle spec r_1) = isFalse ⋯
• Embick2004.instDecidableEqComplement.decEq (Embick2004.Complement.aP r) (Embick2004.Complement.root r_1) = isFalse ⋯
• Embick2004.instDecidableEqComplement.decEq (Embick2004.Complement.aP a) (Embick2004.Complement.aP b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Embick2004.instDecidableEqComplement.decEq (Embick2004.Complement.aP r) (Embick2004.Complement.participle spec r_1) = isFalse ⋯
• Embick2004.instDecidableEqComplement.decEq (Embick2004.Complement.participle spec r) (Embick2004.Complement.root r_1) = isFalse ⋯
• Embick2004.instDecidableEqComplement.decEq (Embick2004.Complement.participle spec r) (Embick2004.Complement.aP r_1) = isFalse ⋯

@[instance_reducible]

instance Embick2004.instDecidableEqComplement : DecidableEq Complement

Equations

• Embick2004.instDecidableEqComplement = Embick2004.instDecidableEqComplement.decEq

@[instance_reducible]

instance Embick2004.instReprComplement : Repr Complement

Equations

• Embick2004.instReprComplement = { reprPrec := Embick2004.instReprComplement.repr }

def Embick2004.instReprComplement.repr : Complement → ℕ → Std.Format

Equations

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

structure Embick2004.FientP : Type

The domain of v[FIENT] (41) records the DP in its specifier, the Root directly merged with it if any, its complement, and the half of the means rule that interprets a merged Root.

• spec : Option DP
• merged : Option Root
• comp : Complement
• means : Option MeansRule

def Embick2004.instDecidableEqFientP.decEq (x✝ x✝¹ : FientP) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Embick2004.instDecidableEqFientP : DecidableEq FientP

Equations

• Embick2004.instDecidableEqFientP = Embick2004.instDecidableEqFientP.decEq

def Embick2004.instReprFientP.repr : FientP → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Embick2004.instReprFientP : Repr FientP

Equations

• Embick2004.instReprFientP = { reprPrec := Embick2004.instReprFientP.repr }

structure Embick2004.Model (E : Type u_1) : Type u_1

A model supplies the transition FIENT, the means relation BY, BY X Y saying that Y comes about by X, the content of each Root with an argument and without one, and the referents of the DPs.

• fient : Prop → Prop
• by_ : Prop → Prop → Prop
• pred : Root → E → Prop
• prop : Root → Prop
• dp : DP → E

def Embick2004.FientP.SatisfiesFient : FientP → Prop

Condition (54). The complement of every v[FIENT] is predicated of a DP in its specifier, so a resultative participle complement, with a v[FIENT] of its own, needs a DP in each specifier.

Equations

• { spec := spec, merged := merged, comp := Embick2004.Complement.participle inner r, means := means }.SatisfiesFient = (spec.isSome = true ∧ inner.isSome = true)
• { spec := spec, merged := merged, comp := comp, means := means }.SatisfiesFient = (spec.isSome = true)

def Embick2004.FientP.interp {E : Type u_1} (M : Model E) : FientP → Option Prop

The interpretation of the domain of v[FIENT], none where there is none. A Root complement is the state the transition reaches and must take the DP in the specifier as its argument (44). A directly merged Root is the means by which the state of the aP comes about (49). Any other structure leaves a bare Root uncategorized or a v[FIENT] without a DP in its specifier.

Equations

• One or more equations did not get rendered due to their size.
• Embick2004.FientP.interp M x✝ = none

def Embick2004.FientP.Interpretable : FientP → Prop

The structures that have an interpretation.

Equations

• { spec := some val, merged := none, comp := Embick2004.Complement.root r, means := means }.Interpretable = Embick2004.TakesArgument r
• { spec := some val, merged := some val_1, comp := Embick2004.Complement.aP r, means := some val_2 }.Interpretable = True
• x✝.Interpretable = False

@[instance_reducible]

instance Embick2004.FientP.instDecidablePredInterpretable : DecidablePred Interpretable

Equations

• One or more equations did not get rendered due to their size.
• { spec := some val, merged := some val_1, comp := Embick2004.Complement.aP r, means := some val_2 }.instDecidablePredInterpretable = isTrue trivial
• { spec := none, merged := merged, comp := comp, means := means }.instDecidablePredInterpretable = isFalse ⋯
• { spec := some val, merged := none, comp := Embick2004.Complement.aP r, means := means }.instDecidablePredInterpretable = isFalse ⋯
• { spec := some val, merged := none, comp := Embick2004.Complement.participle spec r, means := means }.instDecidablePredInterpretable = isFalse ⋯
• { spec := some val, merged := some val_1, comp := Embick2004.Complement.root r, means := means }.instDecidablePredInterpretable = isFalse ⋯
• { spec := some val, merged := some val_1, comp := Embick2004.Complement.participle spec r, means := means }.instDecidablePredInterpretable = isFalse ⋯
• { spec := some val, merged := some val_1, comp := Embick2004.Complement.aP r, means := none }.instDecidablePredInterpretable = isFalse ⋯

theorem Embick2004.FientP.isSome_interp_iff {E : Type u_1} (M : Model E) (p : FientP) : (interp M p).isSome = true ↔ p.Interpretable

theorem Embick2004.FientP.Interpretable.satisfiesFient {p : FientP} (h : p.Interpretable) : p.SatisfiesFient

An interpretable structure satisfies the condition on v[FIENT].

theorem Embick2004.FientP.not_satisfiesFient_participle (x : DP) (m : Option Root) (r : Root) (μ : Option MeansRule) : ¬{ spec := some x, merged := m, comp := Complement.participle none r, means := μ }.SatisfiesFient ∧ ¬{ spec := none, merged := m, comp := Complement.participle (some x) r, means := μ }.SatisfiesFient

A resultative participle with a single DP violates the condition on v[FIENT] wherever the DP is generated, since one of the two v[FIENT] heads is left without a specifier (57b).

theorem Embick2004.FientP.interp_rootComplement {E : Type u_1} (M : Model E) (x : DP) {r : Root} (hr : TakesArgument r) (μ : Option MeansRule) : interp M { spec := some x, merged := none, comp := Complement.root r, means := μ } = some (M.fient (M.pred r (M.dp x)))

A Root complement names the state the transition reaches: The metal is hammered is FIENT(Hammer(the metal)) (44).

theorem Embick2004.FientP.interp_directMerge {E : Type u_1} (M : Model E) (x : DP) (m a : Root) : interp M { spec := some x, merged := some m, comp := Complement.aP a, means := some MeansRule.argument } = some (M.by_ (M.pred m (M.dp x)) (M.fient (M.pred a (M.dp x))))

A directly merged Root names the means and the aP the result: John hammered the metal flat is BY(Hammer(the metal), FIENT(Flat(the metal))), becoming flat by hammering and not becoming hammered by flattening (50).

theorem Embick2004.FientP.interp_directMerge_noArgument {E : Type u_1} (M : Model E) (x : DP) (m a : Root) : interp M { spec := some x, merged := some m, comp := Complement.aP a, means := some MeansRule.noArgument } = some (M.by_ (M.prop m) (M.fient (M.pred a (M.dp x))))

A Root merged without an argument is no predicate of the DP: John smoked himself thin is BY(Smoke, FIENT(Thin(himself))) and does not entail that John smoked himself (52).

The examples

def Embick2004.rootTable : List (String × Root)

The Roots as named in the rows.

Equations

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

def Embick2004.dpTable : List (String × DP)

The DPs as named in the rows.

Equations

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

def Embick2004.optional? {α : Type u_1} (d : Datum) (key : String) (table : List (String × α)) : Option (Option α)

The value of an optional feature, none when the row writes "none".

Equations

• Embick2004.optional? d key table = if d.feature? key = some "none" then some none else Option.map some (d.parse? key table)

def Embick2004.FientP.ofDatum (d : Datum) : Option FientP

The domain of v[FIENT] an example is analysed with.

Equations

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

def Embick2004.data : List (FientP × Judgment)

The examples with their analyses and judgments.

Equations

• Embick2004.data = List.filterMap (fun (d : Datum) => Option.map (fun (x : Embick2004.FientP) => (x, d.judgment)) (Embick2004.FientP.ofDatum d)) Embick2004.Examples.all

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

Every example has its analysis.

theorem Embick2004.acceptable_iff_interpretable (p : FientP × Judgment) : p ∈ data → (p.2 = Judgment.acceptable ↔ p.1.Interpretable)

An example is acceptable exactly when its analysis is interpretable: The metal is hammered and John laughed himself hoarse are, John is laughed, John laughed hoarse and John kicked the door opened are not.