English inflectional suffixes and their spelling

The regular inflectional suffixes of English are -s, -ed, -ing, -er and -est. A suffix is written on its base with four spelling alternations, which the Cambridge Grammar states once for nouns, verbs and adjectives. Three change the end of the base: a final consonant letter doubles before a suffix that begins with a vowel (hopping), a final e drops before one (hoping), and a final y after a consonant becomes i, or ie before -s (pitied, tries). The fourth is in the suffix: -s is -es after a sibilant and after o (foxes, goes).

Main definitions

• English.Inflection.s, ed, ing, er, est: the suffixes.
• English.Inflection.attach: the spelling of a base with a suffix.
• English.Inflection.spell: the spelling of a sequence of morphs.

Main statements

• English.Inflection.suffix_attach: a suffixed form ends in its suffix.
• English.Inflection.rdrop_prefix_attach: the alternations reach no further into the base than its last two letters.

Implementation notes

• The rules read the spelling. A vowel symbol is a vowel letter or y, other than the u of qu and an initial y.
• A final consonant doubles when the last syllable is stressed. A base of one syllable is, and its spelling shows that it has one; for a longer base the argument doubling says so, regretted against visited.
• An entry lists what the rules do not give: ch for /k/ (epochs), a final e that is the vowel of a longer base (acme), ie for /ɪ/ (sortieing), a doubled s (gasses) and nouns in o with -s (dynamos).

References

• [HP02]

The suffixes

def English.Inflection.s : Morphology.Morph

The -s of the plural and of the third person singular present.

Equations

• English.Inflection.s = Morphology.Morph.suff "s"

def English.Inflection.ed : Morphology.Morph

The -ed of the past and the past participle.

Equations

• English.Inflection.ed = Morphology.Morph.suff "ed"

def English.Inflection.ing : Morphology.Morph

The -ing of the present participle.

Equations

• English.Inflection.ing = Morphology.Morph.suff "ing"

def English.Inflection.er : Morphology.Morph

The -er of the comparative.

Equations

• English.Inflection.er = Morphology.Morph.suff "er"

def English.Inflection.est : Morphology.Morph

The -est of the superlative.

Equations

• English.Inflection.est = Morphology.Morph.suff "est"

Spelling

A base is read from its end, so the rules take its reversal r.

def English.Inflection.IsVowelLetter (c : Char) : Prop

The letters a, e, i, o and u.

Equations

• English.Inflection.IsVowelLetter c = (c ∈ ['a', 'e', 'i', 'o', 'u'])

@[instance_reducible]

instance English.Inflection.instDecidablePredCharIsVowelLetter : DecidablePred IsVowelLetter

Equations

• English.Inflection.instDecidablePredCharIsVowelLetter c = { decide := decide (List.elem c ['a', 'e', 'i', 'o', 'u'] = true), reflects_decide := ⋯ }

def English.Inflection.EndsInVowel (r : List Char) : Prop

EndsInVowel r says that the spelling whose reversal is r ends in a vowel symbol, which is a vowel letter or y other than the u of qu and an initial y.

Equations

• English.Inflection.EndsInVowel r = ((∃ c ∈ r.head?, English.Inflection.IsVowelLetter c ∨ c = 'y') ∧ ¬['u', 'q'] <+: r ∧ r ≠ ['y'])

@[instance_reducible]

instance English.Inflection.instDecidablePredListCharEndsInVowel : DecidablePred EndsInVowel

Equations

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

def English.Inflection.alternant : List Char → List Char → List Char

alternant r suffix is the suffix as written after the base whose reversal is r. The suffix -s is -es after s, x, z, sh and ch, and after o that follows a consonant.

Equations

• English.Inflection.alternant ('s' :: tail) ['s'] = ['e', 's']
• English.Inflection.alternant ('x' :: tail) ['s'] = ['e', 's']
• English.Inflection.alternant ('z' :: tail) ['s'] = ['e', 's']
• English.Inflection.alternant ('h' :: 's' :: tail) ['s'] = ['e', 's']
• English.Inflection.alternant ('h' :: 'c' :: tail) ['s'] = ['e', 's']
• English.Inflection.alternant ('o' :: c :: r) ['s'] = if English.Inflection.EndsInVowel (c :: r) then ['s'] else ['e', 's']
• English.Inflection.alternant x✝¹ x✝ = x✝

def English.Inflection.baseBefore (r suffix : List Char) (doubling : Bool := false) : List Char

baseBefore r suffix doubling is the reversal of the base as written before suffix, where r is the reversal of the base. A final y after a consonant is i, or ie before -s, and stays before i, where a final ie is y. A final e drops before a vowel when the base has another vowel, but ee, oe and ye keep it before i. A final consonant letter other than h, w, x and y doubles before a vowel after a single vowel letter, in a base of one syllable or, if doubling holds, a longer one; an s does not double before -es.

Equations

• One or more equations did not get rendered due to their size.
• English.Inflection.baseBefore ('y' :: r') (x :: tail) doubling = if English.Inflection.EndsInVowel r' ∨ x = 'i' then 'y' :: r' else if x :: tail = ['s'] then 'e' :: 'i' :: r' else 'i' :: r'
• English.Inflection.baseBefore ('e' :: 'i' :: r') ('i' :: tail) doubling = 'y' :: r'
• English.Inflection.baseBefore r suffix doubling = r

def English.Inflection.attach (b suffix : List Char) (doubling : Bool := false) : List Char

attach b suffix doubling is the spelling of the base b with suffix. For a base of more than one syllable, doubling says that its final consonant doubles, as it does when the last syllable is stressed.

Equations

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

def English.Inflection.spell (ms : List Morphology.Morph) (doubling : Bool := false) : String

spell ms doubling is the spelling of the sequence of morphs ms, with each suffix written on what precedes it in its word by attach and the words separated by spaces.

Equations

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

theorem English.Inflection.suffix_alternant (r suffix : List Char) : suffix <:+ alternant r suffix

theorem English.Inflection.suffix_attach (doubling : Bool) (b suffix : List Char) : suffix <:+ attach b suffix doubling

A suffixed form ends in its suffix.

theorem English.Inflection.drop_suffix_baseBefore (doubling : Bool) (r suffix : List Char) : List.drop 2 r <:+ baseBefore r suffix doubling

theorem English.Inflection.rdrop_prefix_attach (doubling : Bool) (b suffix : List Char) : b.rdrop 2 <+: attach b suffix doubling

The alternations reach no further into the base than its last two letters.

The grammar's examples