Zwicky and Pullum (1983): Cliticization vs. Inflection: English n't

This file formalizes [ZP83]'s six criteria for telling clitics from inflectional affixes and their application to the English contracted negator -n't. Clitics show a low degree of selection with respect to their hosts, no arbitrary gaps, no morphophonological or semantic idiosyncrasies, are not affected by syntactic rules, and can attach to material already containing clitics; affixes show the opposite on each count (criteria A–F). A morpheme's profile on the six criteria (CliticAffixProfile) determines its status (CliticAffixProfile.classify): the English contracted auxiliaries 's, 've and 'd are clitic-like on every criterion and classify as simple clitics, the affixes -ed, -s and -est are affix-like on every criterion, and -n't, taken almost without exception to be a clitic, is affix-like on every criterion and classifies as an inflectional affix (nt_is_affix). Two of the criteria are checked against the fragment of English auxiliaries: the paradigm gaps mayn't and amn't of criterion B (may_gap, am_gap) and the irregular forms won't, can't, shan't, don't and mustn't of criterion C (irregularNegatives). The semantic idiosyncrasy of criterion D, that can't means NOT(CAN(P)) while mustn't means MUST(NOT(P)), is recorded as opposite scope patterns (scope_idiosyncrasy), and the two scopings are separated on a Kripke model (neg_over_poss_ne_poss_over_neg, neg_over_nec_ne_nec_over_neg).

Implementation notes

• The classification takes the paper's two unanimous poles as decisive: six affix-like answers make an inflectional affix, six clitic-like answers a simple clitic. The paper defines special clitics distributionally, not as an intermediate score; the middle branch is a default.
• The criteria of a profile are Boolean data read off the paper's discussion; only the two fragment-checked criteria are derived.

References

• [ZP83]

The six criteria

inductive Morphology.Diagnostics.SelectionDegree : Type

The degree of selection of a bound morpheme with respect to its hosts, criterion A.

• low : SelectionDegree

  Words of virtually any category, as for the contracted auxiliaries.

• singleCategory : SelectionDegree

  Words of one major category, as for the past tense -ed.

• closedClass : SelectionDegree

  A closed list of stems, as for -n't on the finite auxiliaries.

@[instance_reducible]

instance Morphology.Diagnostics.instDecidableEqSelectionDegree : DecidableEq SelectionDegree

Equations

• Morphology.Diagnostics.instDecidableEqSelectionDegree x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Morphology.Diagnostics.instReprSelectionDegree : Repr SelectionDegree

Equations

• Morphology.Diagnostics.instReprSelectionDegree = { reprPrec := Morphology.Diagnostics.instReprSelectionDegree.repr }

def Morphology.Diagnostics.instReprSelectionDegree.repr : SelectionDegree → ℕ → Std.Format

Equations

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

def Morphology.Diagnostics.SelectionDegree.IsHighSelection (s : SelectionDegree) : Prop

Affixes are more selective than clitics.

Equations

• s.IsHighSelection = (s ≠ Morphology.Diagnostics.SelectionDegree.low)

@[instance_reducible]

instance Morphology.Diagnostics.instDecidablePredSelectionDegreeIsHighSelection : DecidablePred SelectionDegree.IsHighSelection

Equations

• Morphology.Diagnostics.instDecidablePredSelectionDegreeIsHighSelection s = { decide := !decide (s = Morphology.Diagnostics.SelectionDegree.low), reflects_decide := ⋯ }

inductive Morphology.Diagnostics.MorphStatus : Type

The status of a bound form on the word, clitic, affix cline.

• freeWord : MorphStatus

  A syntactically independent word.

• simpleClitic : MorphStatus

  A simple clitic, an optional variant of a full form in the full form's positions.

• specialClitic : MorphStatus

  A special clitic, without a corresponding full form or with a distribution of its own.

• inflAffix : MorphStatus

  An inflectional affix.

• derivAffix : MorphStatus

  A derivational affix.

@[instance_reducible]

instance Morphology.Diagnostics.instDecidableEqMorphStatus : DecidableEq MorphStatus

Equations

• Morphology.Diagnostics.instDecidableEqMorphStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Morphology.Diagnostics.instReprMorphStatus : Repr MorphStatus

Equations

• Morphology.Diagnostics.instReprMorphStatus = { reprPrec := Morphology.Diagnostics.instReprMorphStatus.repr }

def Morphology.Diagnostics.instReprMorphStatus.repr : MorphStatus → ℕ → Std.Format

Equations

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

def Morphology.Diagnostics.MorphStatus.IsAffix (s : MorphStatus) : Prop

An inflectional or derivational affix.

Equations

• s.IsAffix = (s = Morphology.Diagnostics.MorphStatus.inflAffix ∨ s = Morphology.Diagnostics.MorphStatus.derivAffix)

@[instance_reducible]

instance Morphology.Diagnostics.instDecidablePredMorphStatusIsAffix : DecidablePred MorphStatus.IsAffix

Equations

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

def Morphology.Diagnostics.MorphStatus.IsClitic (s : MorphStatus) : Prop

A simple or special clitic.

Equations

• s.IsClitic = (s = Morphology.Diagnostics.MorphStatus.simpleClitic ∨ s = Morphology.Diagnostics.MorphStatus.specialClitic)

@[instance_reducible]

instance Morphology.Diagnostics.instDecidablePredMorphStatusIsClitic : DecidablePred MorphStatus.IsClitic

Equations

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

structure Morphology.Diagnostics.CliticAffixProfile : Type

A morpheme's answers to the six criteria.

• selection : SelectionDegree

  Criterion A.

• hasArbitraryGaps : Bool

  Criterion B: arbitrary gaps in the set of combinations.

• hasMorphophonIdiosyncrasies : Bool

  Criterion C: morphophonological idiosyncrasies of the combinations.

• hasSemanticIdiosyncrasies : Bool

  Criterion D: semantic idiosyncrasies of the combinations.

• syntacticRulesApply : Bool

  Criterion E: syntactic rules affect the combinations.

• attachesToCliticizedMaterial : Bool

  Criterion F: the morpheme attaches to material already containing clitics.

@[instance_reducible]

instance Morphology.Diagnostics.instDecidableEqCliticAffixProfile : DecidableEq CliticAffixProfile

Equations

• Morphology.Diagnostics.instDecidableEqCliticAffixProfile = Morphology.Diagnostics.instDecidableEqCliticAffixProfile.decEq

def Morphology.Diagnostics.instDecidableEqCliticAffixProfile.decEq (x✝ x✝¹ : CliticAffixProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Morphology.Diagnostics.instReprCliticAffixProfile.repr : CliticAffixProfile → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.Diagnostics.instReprCliticAffixProfile : Repr CliticAffixProfile

Equations

• Morphology.Diagnostics.instReprCliticAffixProfile = { reprPrec := Morphology.Diagnostics.instReprCliticAffixProfile.repr }

def Morphology.Diagnostics.CliticAffixProfile.affixScore (p : CliticAffixProfile) : ℕ

The number of criteria on which the profile is affix-like.

Equations

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

def Morphology.Diagnostics.CliticAffixProfile.cliticScore (p : CliticAffixProfile) : ℕ

The number of criteria on which the profile is clitic-like.

Equations

• p.cliticScore = 6 - p.affixScore

def Morphology.Diagnostics.CliticAffixProfile.classify (p : CliticAffixProfile) : MorphStatus

The status a profile determines: affix-like on every criterion is an inflectional affix, clitic-like on every criterion a simple clitic.

Equations

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

theorem Morphology.Diagnostics.CliticAffixProfile.classify_of_affixScore_eq_six (p : CliticAffixProfile) (h : p.affixScore = 6) : p.classify = MorphStatus.inflAffix

theorem Morphology.Diagnostics.CliticAffixProfile.classify_of_affixScore_eq_zero (p : CliticAffixProfile) (h : p.affixScore = 0) : p.classify = MorphStatus.simpleClitic

The profiles

def ZwickyPullum1983.cliticS : Morphology.Diagnostics.CliticAffixProfile

The contracted auxiliary 's: clitic-like on every criterion.

Equations

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

def ZwickyPullum1983.cliticVe : Morphology.Diagnostics.CliticAffixProfile

The contracted auxiliary 've.

Equations

• ZwickyPullum1983.cliticVe = ZwickyPullum1983.cliticS

def ZwickyPullum1983.cliticD : Morphology.Diagnostics.CliticAffixProfile

The contracted auxiliary 'd.

Equations

• ZwickyPullum1983.cliticD = ZwickyPullum1983.cliticS

def ZwickyPullum1983.affixEd : Morphology.Diagnostics.CliticAffixProfile

The past tense -ed: affix-like on every criterion.

Equations

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

def ZwickyPullum1983.affixPluralS : Morphology.Diagnostics.CliticAffixProfile

The plural -s.

Equations

• ZwickyPullum1983.affixPluralS = ZwickyPullum1983.affixEd

def ZwickyPullum1983.affixEst : Morphology.Diagnostics.CliticAffixProfile

The superlative -est.

Equations

• ZwickyPullum1983.affixEst = ZwickyPullum1983.affixEd

def ZwickyPullum1983.negNt : Morphology.Diagnostics.CliticAffixProfile

The contracted negator -n't: selective for the finite auxiliaries, with the gaps mayn't and amn't, the irregular won't and can't, the scope idiosyncrasy of mustn't against can't, subject to inversion, and unable to attach to I'd.

Equations

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

theorem ZwickyPullum1983.cliticS_is_clitic : cliticS.classify = Morphology.Diagnostics.MorphStatus.simpleClitic

theorem ZwickyPullum1983.affixEd_is_affix : affixEd.classify = Morphology.Diagnostics.MorphStatus.inflAffix

theorem ZwickyPullum1983.nt_is_affix : negNt.classify = Morphology.Diagnostics.MorphStatus.inflAffix

-n't is an inflectional affix, not a clitic.

theorem ZwickyPullum1983.nt_affixScore : negNt.affixScore = 6

-n't is affix-like on all six criteria.

Criteria B and C on the fragment

theorem ZwickyPullum1983.may_gap : English.Auxiliaries.negative English.Auxiliaries.may = none

mayn't is a paradigm gap.

theorem ZwickyPullum1983.am_gap : English.Auxiliaries.negative English.Auxiliaries.am = none

amn't is a paradigm gap.

def ZwickyPullum1983.irregularNegatives : List Auxiliary

The contracted negatives whose form is not the auxiliary with -n't suffixed: won't, can't, shan't, don't and mustn't.

Equations

• ZwickyPullum1983.irregularNegatives = [English.Auxiliaries.wont, English.Auxiliaries.cant, English.Auxiliaries.shant, English.Auxiliaries.dont, English.Auxiliaries.mustnt]

theorem ZwickyPullum1983.irregular_are_negatives (a : Auxiliary) : a ∈ irregularNegatives → a ∈ English.Auxiliaries.negatives

Criterion D: the scope of the contracted negator

inductive ZwickyPullum1983.NegModalScope : Type

The scope of negation relative to the modal in a contracted negative.

• negOverModal : NegModalScope

  NOT(MODAL(P)), as in you can't go.

• modalOverNeg : NegModalScope

  MODAL(NOT(P)), as in you mustn't go.

@[instance_reducible]

instance ZwickyPullum1983.instDecidableEqNegModalScope : DecidableEq NegModalScope

Equations

• ZwickyPullum1983.instDecidableEqNegModalScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ZwickyPullum1983.instReprNegModalScope.repr : NegModalScope → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ZwickyPullum1983.instReprNegModalScope : Repr NegModalScope

Equations

• ZwickyPullum1983.instReprNegModalScope = { reprPrec := ZwickyPullum1983.instReprNegModalScope.repr }

structure ZwickyPullum1983.ContractedNegScope : Type

The modal force and the scope reading a contracted negative selects.

• force : Modality.ModalForce
• scope : NegModalScope

@[instance_reducible]

instance ZwickyPullum1983.instDecidableEqContractedNegScope : DecidableEq ContractedNegScope

Equations

• ZwickyPullum1983.instDecidableEqContractedNegScope = ZwickyPullum1983.instDecidableEqContractedNegScope.decEq

def ZwickyPullum1983.instDecidableEqContractedNegScope.decEq (x✝ x✝¹ : ContractedNegScope) : Decidable (x✝ = x✝¹)

Equations

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

def ZwickyPullum1983.instReprContractedNegScope.repr : ContractedNegScope → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ZwickyPullum1983.instReprContractedNegScope : Repr ContractedNegScope

Equations

• ZwickyPullum1983.instReprContractedNegScope = { reprPrec := ZwickyPullum1983.instReprContractedNegScope.repr }

def ZwickyPullum1983.cantScope : ContractedNegScope

can't denies the possibility.

Equations

• ZwickyPullum1983.cantScope = { force := Modality.ModalForce.possibility, scope := ZwickyPullum1983.NegModalScope.negOverModal }

def ZwickyPullum1983.mustntScope : ContractedNegScope

mustn't requires the negation.

Equations

• ZwickyPullum1983.mustntScope = { force := Modality.ModalForce.necessity, scope := ZwickyPullum1983.NegModalScope.modalOverNeg }

theorem ZwickyPullum1983.scope_idiosyncrasy : cantScope.scope ≠ mustntScope.scope

The two contracted forms select opposite scopes, the irregularity in the connection between the contracted and the uncontracted form.

theorem ZwickyPullum1983.neg_over_poss_ne_poss_over_neg : ∃ (R : SetRel (Fin 4) (Fin 4)), ¬∀ (p : Fin 4 → Prop) (w : Fin 4), ¬ModalLogic.Diamond R p w ↔ ModalLogic.Diamond R (fun (w' : Fin 4) => ¬p w') w

NOT(CAN(P)) and CAN(NOT(P)) come apart: on the frame, both P and ¬P are possible at the actual world.

theorem ZwickyPullum1983.neg_over_nec_ne_nec_over_neg : ∃ (R : SetRel (Fin 4) (Fin 4)), ¬∀ (p : Fin 4 → Prop) (w : Fin 4), ¬ModalLogic.Box R p w ↔ ModalLogic.Box R (fun (w' : Fin 4) => ¬p w') w

NOT(MUST(P)) and MUST(NOT(P)) come apart: on the frame, P is not necessary at the actual world, yet not necessarily false either.