Morphs

import Linglib.Morphology.Morph · namespace Morphology

A morph is a minimal segmental form together with its attachment kind: root, prefix, suffix, infix, proclitic, enclitic, or free form. It is the form side of Haspelmath's form–content pairing, never zero and never discontinuous.

Main declarations

Morph.Kind: a bound morph has a position relative to its host (Morph.Position) and an attachment, affix or clitic (Morph.Attachment); roots and free forms have neither.
Morph: an attachment kind with the bare segmental material; Morph.pref, Morph.suff, Morph.infixed, Morph.procl, Morph.encl, Morph.root and Morph.free build the morphs of each kind.
Morph.Kind.position?, Morph.Kind.side?, Morph.Kind.attachment?: the projections of a bound kind; an infix is bound inside its host, on no side.
Morph.Side.attach: attachment of an element on a side of a sequence, the linear shadow of attachment on a word tree.
Morph.Kind.JoinsAt: adjacent morphs of two kinds are in one word at an attachment.
Morph.wordsAt, Morph.surface: the words of a sequence of morphs at an attachment, read off the kinds of adjacent morphs, and its surface form in boundary notation.
Morph.IsBoundary, Morph.wordsOf: the morph boundaries of that notation, and the words of a text in it as their morph forms.

Main results

Morph.flatMap_wordsAt: the words at .affix nest in the words at .clitic.
Morph.wordsAt_append_cons: a host with morphs bound before and after it is one word.
Morph.wordsAt_append_of_eq_singleton, Morph.wordsAt_append: a word stays one word when morphs bound after it follow, and two sequences unjoined at their junction keep their words.
Morph.countP_le_one_of_mem_wordsAt: every word has at most one morph that is not bound.
Morph.surface_singleton: a single morph surfaces as itself.

Implementation notes

Morph.Side is the two-sided part of Morph.Position that attachment to a sequence or a word tree uses. ToString writes Leipzig boundary notation (un-, -able, <um>, l=, =s), which brackets infixes and has no separate mark for endoclitics. An affix attaches more tightly than a clitic: the words at .affix keep a clitic apart, as Haspelmath's definition of the word does, and the words at .clitic are the units separated by spaces. In a sequence an infix follows its host, as in Word.Tree.toList, and two adjacent roots are two words, a compound being a Word.Tree.compound. A discontinuous exponent, such as a circumfix, is a list of such sequences, which its owner joins with …. Morph.surface folds with ++ rather than calling String.join and String.intercalate, whose bodies a module cannot unfold, so that decide evaluates a surface form.

References

Haspelmath 2020, The morph as a minimal linguistic form
Haspelmath 2023, Defining the Word formalized

Declarations

L75–81

Where a bound morph sits relative to its host.

inductive Morph.Position L83–91

Type

before : Position
Prefixes and proclitics sit before the host.
inside : Position
Infixes and endoclitics sit inside the host.
after : Position
Suffixes and enclitics sit after the host.

Derives DecidableEq, Repr, Fintype.

Used by Morph.Kind, Morph.Side.toPosition, Morph.Position.side?, Morph.Position.side?_eq_some_iff, Morph.Position.side?_eq_none_iff, Morph.Kind.position?, Morph.Kind.position?_bound, Morph.Kind.attachment?_bound, Morph.Kind.side?_bound, Morph.Kind.position?_eq_some_iff, Morph.Kind.attachment?_eq_some_iff, Morph.Kind.isSome_position?_iff, Morph.Kind.isSome_attachment?_iff, Morph.bound, Morph.bound_kind, Morph.bound_form, Morph.wordsAt_append_cons, Morph.wordsAt_append_of_eq_singleton

A bound morph attaches as an affix or as a clitic, by its descriptive label.

inductive Morph.Attachment L93–99

Type

affix : Attachment
An affix is written with -.
clitic : Attachment
A clitic is written with =.

Derives DecidableEq, Repr, Fintype.

Used by Morph.Kind, Morph.Kind.attachment?, Morph.Kind.position?_bound, Morph.Kind.attachment?_bound, Morph.Kind.side?_bound, Morph.Kind.position?_eq_some_iff, Morph.Kind.attachment?_eq_some_iff, Morph.Kind.side?_eq_some_iff, Morph.Kind.isSome_position?_iff, Morph.Kind.isSome_attachment?_iff, Morph.bound, Morph.bound_kind, Morph.bound_form, Morph.Attachment.instLinearOrder, Morph.Attachment.affix_le, Morph.Attachment.le_clitic, Morph.Kind.JoinsAt, Morph.instDecidableRelKindJoinsAt, Morph.Kind.JoinsAt.mono, Morph.JoinsAt, Morph.instDecidableRelJoinsAt, Morph.JoinsAt.mono, Morph.wordsAt, Morph.flatten_wordsAt, Morph.wordsAt_nil, Morph.wordsAt_singleton, Morph.flatMap_wordsAt, Morph.wordsAt_append_cons, Morph.wordsAt_append_of_eq_singleton, Morph.wordsAt_append, Morph.countP_le_one_of_isChain_joinsAt, Morph.countP_le_one_of_mem_wordsAt

The kind of a morph says how it attaches.

inductive Morph.Kind L101–109

Type

bound (position : Position) (attachment : Attachment) : Kind
A bound morph sits at a position relative to its host, as an affix or a clitic.
root : Kind
The morph is a root.
free : Kind
The morph is free and not a root, as a particle or an auxiliary is.

Derives DecidableEq, Repr, Fintype.

Built from ,

Used by Morph, Morph.Kind.position?, Morph.Kind.attachment?, Morph.Kind.side?, Morph.Kind.position?_eq_some_iff, Morph.Kind.attachment?_eq_some_iff, Morph.Kind.side?_eq_some_iff, Morph.Kind.isSome_position?_iff, Morph.Kind.isSome_attachment?_iff, Morph.Kind.JoinsAt, Morph.Kind.JoinsAt.mono

Used in Phonology/Hiatus/Elision, Syntax/Category/Classifier/Basic, Casali1997, Pater2001, Vago2017

A morph is a minimal segmental form with its attachment kind.

structure Morph L111–117

Type

kind : Kind
The kind says how the morph attaches.
form : String
The form is the bare segmental material, with no boundary notation.

Derives DecidableEq, Repr.

Built from

Used by Morph.bound, Morph.pref, Morph.suff, Morph.infixed, Morph.procl, Morph.encl, Morph.root, Morph.free, Morph.JoinsAt, Morph.JoinsAt.mono, Morph.wordsAt, Morph.flatten_wordsAt, Morph.wordsAt_singleton, Morph.flatMap_wordsAt, Morph.wordsAt_append_cons, Morph.wordsAt_append_of_eq_singleton, Morph.wordsAt_append, Morph.countP_le_one_of_isChain_joinsAt, Morph.countP_le_one_of_mem_wordsAt, Morph.instToString, Morph.surface, Morph.surface_singleton

Used in Fragments/Adyghe/Case, Fragments/Adyghe/Clause, Fragments/Arabic/ModernStandard/Negation, Fragments/Arabic/ModernStandard/Verbs, Fragments/Basque/Agreement and 113 more

Sides and positions

L127–130

L132

L134

s.attach a l attaches a on the side s of the sequence l.

def Morph.Side.attach L136–139

{α : Type u_1} :

Side → α → List α → List α

Morph.Side.before.attach x✝¹ x✝ = x✝¹ :: x✝
Morph.Side.after.attach x✝¹ x✝ = x✝ ++ [x✝¹]

Built from

Used by Morph.Side.attach_before, Morph.Side.attach_after

Kinds

k.position? is the position of a bound kind, and none for roots and free forms.

def Morph.Kind.position?L176–179

Kind → Option Position

(Morph.Kind.bound a a_1).position? = some a
Morph.Kind.root.position? = none
Morph.Kind.free.position? = none

Built from ,

Used by Morph.Kind.side?, Morph.Kind.position?_bound, Morph.Kind.position?_root, Morph.Kind.position?_free, Morph.Kind.position?_eq_some_iff, Morph.Kind.isSome_position?_iff, Morph.countP_le_one_of_isChain_joinsAt, Morph.countP_le_one_of_mem_wordsAt

k.attachment? is the attachment of a bound kind, and none for roots and free forms.

def Morph.Kind.attachment?L181–184

Kind → Option Attachment

(Morph.Kind.bound a a_1).attachment? = some a_1
Morph.Kind.root.attachment? = none
Morph.Kind.free.attachment? = none

Built from ,

Used by Morph.Kind.attachment?_bound, Morph.Kind.attachment?_root, Morph.Kind.attachment?_free, Morph.Kind.attachment?_eq_some_iff, Morph.Kind.isSome_attachment?_iff

k.side? is the side of a kind bound on a side, and none for infixes, endoclitics, roots and free forms.

def Morph.Kind.side?L186–188

(k : Kind) :

Option Side

k.side? = k.position?.bind Morph.Position.side?

Built from , , ,

Used by Morph.Kind.side?_bound, Morph.Kind.side?_root, Morph.Kind.side?_free, Morph.Kind.side?_eq_some_iff

Used in Morphology/Word/Tree, Baker1985, Haspelmath2007, Pater2001, Stassen2000

Morphs of each kind

L232–234

L233

pref s is the prefix of form s.

def Morph.pref L236–237

(s : String) :

Morph

Morph.pref s = { kind := Morph.Kind.bound Morph.Position.before Morph.Attachment.affix, form := s }

Built from

Used by Morph.pref_form, Morph.pref_kind

Used in Fragments/Adyghe/Clause, Fragments/Basque/Agreement, Fragments/Burmese/Negation, Fragments/Dargwa/Tanti/Verbs, Fragments/Georgian/Agreement and 25 more

L237

suff s is the suffix of form s.

def Morph.suff L239–240

(s : String) :

Morph

Morph.suff s = { kind := Morph.Kind.bound Morph.Position.after Morph.Attachment.affix, form := s }

Built from

Used by Morph.suff_form, Morph.suff_kind

Used in Fragments/Adyghe/Case, Fragments/Adyghe/Clause, Fragments/Basque/Pronouns, Fragments/Burmese/Negation, Fragments/Buryat/Complementizers and 80 more

L240

infixed s is the infix of form s.

def Morph.infixed L242–243

(s : String) :

Morph

Morph.infixed s = { kind := Morph.Kind.bound Morph.Position.inside Morph.Attachment.affix, form := s }

Built from

Used by Morph.infixed_form, Morph.infixed_kind

L243

procl s is the proclitic of form s.

def Morph.procl L245–246

(s : String) :

Morph

Morph.procl s = { kind := Morph.Kind.bound Morph.Position.before Morph.Attachment.clitic, form := s }

Built from

Used by Morph.procl_form, Morph.procl_kind

Used in Fragments/Mayan/Mam/Agreement, Fragments/Romance/French/Negation, Haspelmath2021c, Haspelmath2023, Scott2023

L246

encl s is the enclitic of form s.

def Morph.encl L248–249

(s : String) :

Morph

Morph.encl s = { kind := Morph.Kind.bound Morph.Position.after Morph.Attachment.clitic, form := s }

Built from

Used by Morph.encl_form, Morph.encl_kind

Used in Fragments/Dargwa/Tanti/Agreement, Fragments/Dargwa/Tanti/Coordination, Fragments/Dargwa/Tanti/FocusParticles, Fragments/Farsi/Coordination, Fragments/Farsi/FocusParticles and 29 more

L249

root s is the root of form s.

def Morph.root L251–252

(s : String) :

Morph

Morph.root s = { kind := Morph.Kind.root, form := s }

Built from

Used by Morph.root_form, Morph.root_kind

Used in Fragments/Adyghe/Clause, Fragments/Arabic/ModernStandard/Negation, Fragments/Buryat/Complementizers, Fragments/Cantonese/Verbs, Fragments/Chichewa/Verbs and 51 more

L252

free s is the free non-root morph of form s.

def Morph.free L254–255

(s : String) :

Morph

Morph.free s = { kind := Morph.Kind.free, form := s }

Built from

Used by Morph.free_kind, Morph.free_form

Used in Fragments/Arabic/ModernStandard/Negation, Fragments/Dargwa/Tanti/Coordination, Fragments/Dutch/Adpositions, Fragments/English/Adjectives, Fragments/English/Adpositions and 79 more

L255

Words

L261–264

L266

L268

Adjacent morphs of kinds k₁ k₂ are in one word at the attachment l when the first is bound before its host or the second after or inside it, no more loosely than l.

def Morph.Kind.JoinsAt L274–277

(l : Attachment) (k₁ k₂ : Kind) :

Prop

The definition is too large to print here; read it in the source.

Built from ,

Used by Morph.instDecidableRelKindJoinsAt, Morph.Kind.JoinsAt.mono, Morph.JoinsAt

Used in Phonology/Hiatus/Elision

The words of a sequence of morphs at the attachment l are its maximal runs of morphs joined at l.

def Morph.wordsAt L295–298

(l : Attachment) (ms : List Morph) :

List (List Morph)

Morph.wordsAt l ms = List.splitBy (fun (m₁ m₂ : Morph) => decide (Morph.JoinsAt l m₁ m₂)) ms

Built from , ,

Used by Morph.flatten_wordsAt, Morph.wordsAt_nil, Morph.wordsAt_singleton, Morph.flatMap_wordsAt, Morph.wordsAt_append_cons, Morph.wordsAt_append_of_eq_singleton, Morph.wordsAt_append, Morph.countP_le_one_of_mem_wordsAt

Used in Fragments/Korean/Verbs, Bobaljik2012, Haspelmath2023

L300–302

L304

L306

Words at a tighter attachment nest in the words at a looser one.

theorem Morph.flatMap_wordsAt L308–311

{l l' : Attachment} (h : l ≤ l') (ms : List Morph) :

List.flatMap (wordsAt l) (wordsAt l' ms) = wordsAt l ms

Built from , ,

A host with morphs bound before it on one side and after or inside it on the other, none more loosely than l, is one word at l.

theorem Morph.wordsAt_append_cons L313–329

{l : Attachment} {P S : List Morph} (h : Morph) (hP : ∀ p ∈ P, ∃ a ≤ l, p.kind = Kind.bound Position.before a) (hS : ∀ s ∈ S, ∃ (q : Position), q ≠ Position.before ∧ ∃ a ≤ l, s.kind = Kind.bound q a) :

wordsAt l (P ++ h :: S) = [P ++ h :: S]

Built from , , ,

A word at l followed by morphs bound after or inside their hosts, none more loosely than l, is one word at l.

theorem Morph.wordsAt_append_of_eq_singleton L331–347

{l : Attachment} {ms S : List Morph} (h : wordsAt l ms = [ms]) (hS : ∀ s ∈ S, ∃ (q : Position), q ≠ Position.before ∧ ∃ a ≤ l, s.kind = Kind.bound q a) :

wordsAt l (ms ++ S) = [ms ++ S]

Built from , , ,

Two sequences of morphs whose junction joins no morphs at l have the words of each.

theorem Morph.wordsAt_append L349–353

{l : Attachment} {ms ns : List Morph} (h : ∀ x ∈ ms.getLast?, ∀ y ∈ ns.head?, ¬JoinsAt l x y) :

wordsAt l (ms ++ ns) = wordsAt l ms ++ wordsAt l ns

Built from , , ,

L369–380

Every word has at most one morph that is not bound, a root or a free form hosting the rest.

theorem Morph.countP_le_one_of_mem_wordsAt L382–386

{l : Attachment} {ms w : List Morph} (hw : w ∈ wordsAt l ms) :

List.countP (fun (m : Morph) => decide (m.kind.position? = none)) w ≤ 1

Built from , , ,

Boundary notation

L390–397

The surface form of a sequence of morphs writes each word in boundary notation and separates the words by spaces.

def Morph.surface L399–404

(ms : List Morph) :

String

The definition is too large to print here; read it in the source.

Built from

Used by Morph.surface_nil, Morph.surface_singleton

Used in Fragments/Japanese/Conditionals, Fragments/Korean/Clause, Fragments/Korean/Verbs, Fragments/Swahili/Possession, Semantics/Conditionals/Typology and 5 more

L406

A single morph surfaces as itself, so an unanalysed form is the surface form of its root.

@[simp] theorem Morph.surface_singleton L408–409

(m : Morph) :

surface [m] = toString m

Built from ,

The boundaries between the morphs of a word in the notation surface writes are the affix boundary -, the clitic boundary = and the brackets of an infix.

def Morph.IsBoundary L411–413

(c : Char) :

Prop

Morph.IsBoundary c = (c = '-' ∨ c = '=' ∨ c = '<' ∨ c = '>')

Used by Morph.instDecidablePredCharIsBoundary

L415–416

The words of a text in the notation surface writes, each as the characters of its morph forms: words are separated by spaces, and the morphs of a word by boundaries.

def Morph.wordsOf L418–428

(s : String) :

List (List (List Char))

The definition is too large to print here; read it in the source.

Used in Miestamo2005

L426–428