commit 7c78b560dabbd34606209dea3dbbf20a3f71b8fe Author: Noah Diewald Date: Thu Feb 25 06:42:04 2021 -0500 initial commit diff --git a/PotawatomiPoss.v b/PotawatomiPoss.v new file mode 100644 index 0000000..edbbead --- /dev/null +++ b/PotawatomiPoss.v @@ -0,0 +1,246 @@ +Require Import Coq.Lists.List. +Require Import Coq.Strings.String. +Import ListNotations. + +Open Scope type_scope. +Open Scope string_scope. + +(* First we define lexes, which are building blocks for lexemes. These +are not lexemes themselves because we require additional structure to +develop a notion of derivational relationships. *) + +Inductive lex : Set := +| OS : lex (* father *) +| NESHNABÉ : lex (* person *) +| BIWABEK : lex (* metal *) +| MOWECH : lex (* feces *) +| BAGJÉʔGEN : lex. (* pool cue *) + +(* Here we define the only derivational relationship that we are +concerned with for this fragment, IJ, which relates lexes to a lexeme +that is related by the function c to the class appropriate to +inalienably possessed nouns. *) + +Inductive rel : Set := +| IJ : rel. (* fellow *) + +(* Lexemes are either simple, in the case of root or have a +relationship to a class of likewise derived lexemes in the case of +cmplx. *) + +Inductive lexeme : Type := +| root (l : lex) +| cmplx (r : rel) (l : lex). + +(* The type mm is for atoms used in m-categories or mcats, which are +lists of mms. Here this is somewhat redundant because our fragment is +so simple. *) + +Inductive mm : Set := +| free : mm +| freem : mm +| bound : mm +| nposs : mm. + +(* I define fclasses that are not used in this fragment. These are +related to lexemes by the function c. *) + +Inductive fclass : Set := +| long : fclass +| short : fclass +| nosuffix : fclass +| msuffix : fclass +| LN : fclass +| LM : fclass +| SN : fclass +| SM : fclass +| LNM : fclass +| LSN : fclass +| LSM : fclass +| SNM : fclass +| LSNM : fclass +| none : fclass. (* This will exist outside the order. *) + +(* As stated above, mcat is a list of mms. An mform is a string. *) + +Definition mcat := list mm. +Definition mform := string. + +(* An mtrip is the data structure used to define Fentrys *) + +Definition mtrip := mcat * mform * lexeme. + +(* Note that the check below demonstrates why simply saying that we're +working with mtrips is not good enough. Non-grammatical triples +check. We need to be able to specify which are legal triples. *) + +Check ([ SNM ] , "walk" , root OS). + +(* To solve this I define a predicate Fentry, the use of which will be +seen below. Essentially, only grammatical mtrips will be Fentrys. *) + +Axiom Fentry : mtrip -> Prop. + +(* lem is the order over mcats. The axioms below define it as an +order. *) + +Axiom lem : mcat -> mcat -> Prop. +Axiom lem_refl : forall x : mcat, lem x x. +Axiom lem_antisym : forall x y : mcat, lem x y -> lem y x -> x = y. +Axiom lem_trans : forall x y z : mcat, lem x y -> lem y z -> lem x z. + +(* The order is not natural. We define, explicitly, the relation. *) + +Axiom free_lem_bound : lem [ free ] [ bound ]. +Axiom free_lem_freem : lem [ free ] [ freem ]. + +(* lef is the order over fclasses. The axioms below define it as an +order. *) + +Axiom lef : fclass -> fclass -> Prop. +Axiom lef_refl : forall x : fclass, lef x x. +Axiom lef_antisym : forall x y : fclass, lef x y -> lef y x -> x = y. +Axiom lef_trans : forall x y z : fclass, lef x y -> lef y z -> lef x z. + +(* The order is not natural. We define, explicitly, the relation. *) + +Axiom ln_lef_long : lef LN long. +Axiom lm_lef_long : lef LM long. +Axiom ln_lef_nosuffix : lef LN nosuffix. +Axiom sn_lef_nosuffix : lef SN nosuffix. +Axiom lm_lef_msuffix : lef LM msuffix. +Axiom sm_lef_msuffix : lef SM msuffix. +Axiom sn_lef_short : lef SN short. +Axiom sm_lef_short : lef SM short. +Axiom lnm_lef_ln : lef LNM LN. +Axiom lsn_lef_ln : lef LSN LN. +Axiom lnm_lef_lm : lef LNM LM. +Axiom lsm_lef_lm : lef LSM LM. +Axiom lsn_lef_sn : lef LSN SN. +Axiom snm_lef_sn : lef SNM SN. +Axiom lsm_lef_sm : lef LSM SM. +Axiom snm_lef_sm : lef SNM SM. +Axiom lsnm_lef_lnm : lef LSNM LNM. +Axiom lsnm_lef_lsm : lef LSNM LSM. + +(* Below we define c which relates lexemes to their fclass. We assume +that only cmplx IJ NESHNABÉ will have an fclass that allows for the +derivation from root NESHNABÉ as this is the only attested lexeme for +that derivation among the lexemes defined. *) + +Definition c (l:lexeme) : fclass := + match l with + | root OS => SN + | root NESHNABÉ => LM + | root BIWABEK => LSM (* We'd predict LSNM but these are attested. *) + | root BAGJÉʔGEN => SNM (* The same as above. *) + | root MOWECH => LSNM (* There are missing forms here too. *) + | cmplx IJ lx => match lx with + | NESHNABÉ => SN + | _ => none + end + end. + +(* Below I define the form building functions. These ignore the +intricacies of providing correct surface forms as a simplification and +due to a lack of the specification of a phonological interface. *) + +Definition suffix_m (s:mform) : mform := + s ++ "m". + +Definition prefix_n (s:mform) : mform := + "n" ++ s. + +Definition prefix_ned (s:mform) : mform := + "ned" ++ s. + +Definition prefix_ij (s:mform) : mform := + "ij" ++ s. + +(* These are definitions of basic stems for the lexemes above. Note +that I define the mtrips first and then specify that they are +Fentrys. *) + +Definition mowech_free := ([ free ], "mowech", root MOWECH) : mtrip. + +Definition os_bound := ([ bound ], "os", root OS) : mtrip. + +Axiom f_mowech_free : Fentry mowech_free. + +(* f_m is the rule for specifying that... *) + +Axiom f_m : forall (mt : mtrip), (Fentry mt) -> (lem (fst (fst mt)) [ freem ]) -> (lef (c (snd mt)) msuffix) -> Fentry ([ bound ], suffix_m (snd (fst mt)), (snd mt)). + +Axiom f_n : forall (mt : mtrip), (Fentry mt) -> (lem (fst (fst mt)) [ bound ]) -> (lef (c (snd mt)) short) -> Fentry ([ nposs ], prefix_n (snd (fst mt)), (snd mt)). + +Axiom f_ned : forall (mt : mtrip), (Fentry mt) -> (lem (fst (fst mt)) [ bound ]) -> (lef (c (snd mt)) long) -> Fentry ([ nposs ], prefix_ned (snd (fst mt)), (snd mt)). + +Definition glex (l:lexeme) := + match l with + | root lx => lx + | cmplx _ lx => lx + end. + +Axiom f_ij : forall (mt : mtrip), (Fentry mt) -> (lem (fst (fst mt)) [ freem ]) -> (lef (c (snd mt)) msuffix) -> Fentry ([ bound ], prefix_ij (snd (fst mt)), cmplx IJ (glex (snd mt))). + +Lemma walk_base_is_fentry: + Fentry mowech_free. +Proof. + apply f_mowech_free. +Qed. + +Lemma mowech_free_is_free: + lem (fst (fst mowech_free)) [ free ]. +Proof. + simpl. + apply lem_refl. +Qed. + +Lemma mowech_free_is_LSNM: + lef (c (snd mowech_free)) LSNM. +Proof. + simpl. + apply lef_refl. +Qed. + +Lemma LM_is_msuffix: + lef LM msuffix. +Proof. + apply lm_lef_msuffix. +Qed. + +Lemma LNM_is_msuffix: + lef LNM msuffix. +Proof. + assert (H1 : lef LNM LM). + { apply lnm_lef_lm. } + assert (H2 : lef LM msuffix). + { apply lm_lef_msuffix. } + apply (lef_trans LNM LM msuffix H1 H2). +Qed. + +Lemma mowech_free_is_msuffix: + lef (c (snd mowech_free)) msuffix. +Proof. + simpl. + assert (H1 : lef LSNM LNM). + { apply lsnm_lef_lnm. } + assert (H2 : lef LNM msuffix). + { exact LNM_is_msuffix. } + apply (lef_trans LSNM LNM msuffix H1 H2). +Qed. + +Example test_f_m: + Fentry ([ bound ], "mowechm", root MOWECH). +Proof. + assert (H1 : lem [ free ] [ freem ]). + { apply free_lem_freem. } + assert (H2 : lef LSNM msuffix). + { exact mowech_free_is_msuffix. } + apply (f_m mowech_free). + exact f_mowech_free. + simpl. + assumption. + simpl. + assumption. +Qed. diff --git a/QuechuaPlural.v b/QuechuaPlural.v new file mode 100644 index 0000000..1e8441a --- /dev/null +++ b/QuechuaPlural.v @@ -0,0 +1,325 @@ +(** * Cochabamba Quechua Plurals + +Below is a morphological fragment of in Lexical Proof Morphology of an +overabundant plural pattern found in Cochabamba Quechua. + +In some dialects of Cochabamba Quechua the borrowed Spanish plural -s +occurs on all nominal stems that end in a vowel. There is also a +native plural -kuna, that occurs on nominal stems generally. These +plural may also co-occur in varying order on the stem. So for a vowel +stem, like warmi, 'woman', warmi-s, warmi-kuna, warmi-s-kuna, +warmi-kuna-s are all predicted to occur, though not with equal +likelihood, necessarily. A stem that ends in a consonant, like sipas, +'young woman', is predicted to have the plural forms sipaskuna and +sipaskunas for some speakers. There is also a possible semantic +constraint on the distribution of the Spanish plural, where the -kuna +plural is more appropriate for contrastive subjects. Of course, there +are also other dialectal patterns and speaker variation. The fragment +below captures one observable pattern. *) + +Require Import Coq.Lists.List. +Require Import Coq.Strings.String. +Import ListNotations. + +Open Scope type_scope. +Open Scope string_scope. + +(** * Initial axioms of the fragment + +Below I introduce the basic lexemes and categories of the +morphological fragment. + +** Lexemes + +First I define some basic lexemes. Lexemes have no inherent +properties. They serve a role similar to foriegn keys in a relational +database. They are a key for retrieving and defining collections of +information. For instance ( LEXEME_1, x ), ( LEXEME_1, y ) puts both x +and y in the same collection, where the collection is defined in terms +of the second elements of tuples where the first element is the same +lexeme. + +The lexeme WARMI corresponds to a nominal with a stem ending in a +vowel. The lexeme SIPAS corresponds to a lexeme ending in a +consonant. *) + +Inductive lexeme : Set := +| WARMI : lexeme (* woman *) +| SIPAS : lexeme. (* young woman *) + +(** ** Morphological categories + +The type matom is for atoms used in m-category names or mcats, +which I compose like lists. Mcats are morphological categories, which +categorize observable analogical patterns in morphological form. For +instance, though warmis, warmikuna, warmiskuna and warmikunas +correspond to two syntactic categories, one for basic plural and one +for a contrastive subject, but there are, at minimum, four +morphological categories, one for each form. In practice, there are +more categories to capture the "morphotactics" or the allowable +patterns of affix coocurence within words of the system and to allow +for generalizations when mapping between syntactic categories. + +In fact, what one "sees" in this system are not the categories, +themselves, which are conceptually atomic but a means of referring to +them with names. Think of the name John Smith as a category name and +Smith as analogous to an matom. Just as the last name Smith can belong +to an entire family or even multiple people in multiple families, each +person with Smith in their name is an individual and could, +potentially be named something else. Likewise, having Smith as a last +name, one of the most frequent last names in the English language, +does not entail family membership. Despite this, the system of naming +children using their parents' last names does simplify the naming of +children. Therefore if it were a rule that every child needed to be +named as a composition of the last name of a particular parent and +some individuated name, the rules of naming are greatly simplified, +even if nothing can be said to be entailed about the properties of +that individual by having a particular last name. The category naming +scheme used here, where names are lists of matoms allows for +flexibility and simplification in naming categories using rules but, +at least at this time, no rule applies because it has a particular +sub-element or sub-list, i.e.\ nothing is entailed about the category +just because a sub-element of its name is one thing or another. This +is a fundamental difference between this scheme and a feature system, +for instance. *) + +Inductive matom : Set := +| nbase : matom +| mplural : matom +| s : matom +| kuna : matom +| kbase : matom +| sbase : matom +| ta : matom. + +(** As stated above, mcat is a list of matoms. *) + +Definition mcat := list matom. + +** Mcats for the fragment *) + +(* [ nbase ] is a basic noun stem. [ kbase ] is a stem that can take + a -kuna affix. [ sbase ] is a stem that can take a -s affix. [ + kuna ] is any form that contains -kuna. [ mplural ] is any form + with a plural affix. [ s , nbase ] is a basic stem with only an -s + affix. [ kuna, nbase ] is a basic stem with only a -kuna affix. + The other two mcats contain both suffixes in differing order. + +The kuna forms are hypothesized to have a different distribution than +the -s only form. They are (possibly) more compatible with focus +constructions in subject position. + +A take away for the above is that nearly every form type has its own +category, at least in this analysis of this phenomenon. Labeling form +types is not the only role of these categories. Some categories, such +as [ sbase ] and [ kbase ] are only directly relevant to +morphotactics. Other categories, such as [ kuna ] are more relevant to +the interface with the syntactic paradigm. *) + +(** ** Morphological forms + +An mform, or morphological form, is a string *) + +Definition mform := string. + +(** Below are some string functions to handle suffixation. *) + +Definition suffix_s (stem:mform) : mform := + stem ++ "s". + +Definition suffix_kuna (stem:mform) : mform := + stem ++ "kuna". + +Definition suffix_ta (stem:mform) : mform := + stem ++ "ta". + +(** ** The structure of morphological paradigm entries + +An mtrip is a data structure used to define Fentrys, which are +"form entries" aka morphological paradigm entries. There could +potentially be many non-Fentrys that have the type of an +mtrip. Nothing constrains this type to only be reasonable +entities. One of the purposes of the theory is to specify what +morphological forms are valid in a particular language. This is +similar to the formal language notion of defining the characteristic +function of a subset of all string combinations that correspond to a +grammar. + +Here the '*' corresponds to ×, for defining the types of pairs. *) + +Definition mtrip := mcat * mform * lexeme. + +(** The check below demonstrates why simply saying that we're working +with mtrips is not good enough. Non-grammatical triples check. We need +to be able to specify which are legal triples. *) + +Check ( [ kuna ] , "foot" , WARMI ). + +(** Here I define Fentry, which is a predicate that is proveable when +an mtrip is a valid lexical entity. *) + +Axiom Fentry : mtrip -> Prop. + +(** Here I define the mtrip for the "warmi" stem. I am not handling +the phonological dimension that "sipas" requires, where -s cannot be +suffixed to a stem that ends in a consonant because I haven't built a +phonological abstraction into this example, yet. I could specify the +needed categorical distinction with a predicate. Such a predicate +would be true for some specified set of mforms and false for others +but it is more interesting to do it correctly and pattern match on the +string. *) + +Definition warmi_nbase := ([ nbase ], "warmi", WARMI) : mtrip. + +(** This requires an explicit axiom to be treated like an +Fentry. Other Fentries will be derived from it. *) + +Axiom f_warmi_nbase : Fentry warmi_nbase. + +(** * Morpho-Lexical relations + +lem, for "less than or equal to morphological category" is the +order over morphological categories, or mcats. What you see below are +the basic properties of an order. These state the relation is +reflexive, meaning that x ≤ x; antisymmetric, meaning that if x ≤ y +and y ≤ x then x = y; transitive, meaning that if x ≤ y and y ≤ z then +x ≤ z. *) + +Axiom lem : mcat -> mcat -> Prop. +Axiom lem_refl : forall x : mcat, lem x x. +Axiom lem_antisym : forall x y : mcat, lem x y -> lem y x -> x = y. +Axiom lem_trans : forall x y z : mcat, lem x y -> lem y z -> lem x z. + +(** The order is not natural. There may be natural orders on the +underlying list type based on length but this is not how I use +mcats. As mentioned, though their structure is complex, they are +*names* of atomic categories. + +Due to the fact that the order is not natural, each relation must be +explicitly specified, except those that are predictable from the +properties of the order. Below I specify those needed for this +fragment. *) + +Axiom nbase_lem_kbase : lem [ nbase ] [ kbase ]. +Axiom s_nbase_lem_kbase : lem [ s ; nbase ] [ kbase ]. +Axiom nbase_lem_sbase : lem [ nbase ] [ sbase ]. +Axiom kuna_nbase_lem_sbase : lem [ kuna ; nbase ] [ sbase ]. +Axiom kuna_nbase_lem_kuna : lem [ kuna ; nbase ] [ kuna ]. +Axiom kuna_s_nbase : lem [ kuna ; s ; nbase ] [ kuna ]. +Axiom s_kuna_nbase : lem [ s ; kuna ; nbase ] [ kuna ]. +Axiom kuna_lem_mplural : lem [ kuna ] [ mplural ]. +Axiom s_nbase_lem_mplural : lem [ s ; nbase ] [ mplural ]. + +(** ** Morphotactic rules + +In using the word "morphotactic", it may imply an imperative form +building interpretation. Though rules in this system tend to take as +input simpler forms and output more complex forms, the opposite is +possible. Defining rules in a form building direction is done for +practical reasons. Longer more complex forms are often less +frequent. If one wishes to base the assumed forms of a fragment on +something that is independently observable and to be consistent about +which forms are assumed as axioms across lexemes, frequently used +forms are preferable -- or perhaps something like the principal parts +of a paradigm. The intended interpretation of these rules is that they +declare that if it is the case that Fentry x exists, then Fentry y +exists but x does not underly y in any sense. Nor is it necessarily +contained as a subpart of y. + +Below one can see the first morphotactic rule, which I call form-form +mappings. It specifies that anything within the category of [ sbase ] +can have its form suffixed with -s. The accessors that look like (fst +(fst mt)) are because the mtrip triple is actually a pair of a pair +and a lexeme, the structure is w=((x,y),z) so (fst (fst w)) is x. In +English the rule says, for any mtrip that is an Fentry, if the mcat is +less than or equal to [ sbase ] then there is a Fentry such that the +category is whatever was provided with matom s added to the front, an +mform with an affixed -s and an unchanged lexeme. *) + +Axiom add_s : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ sbase ]) -> + Fentry (cons s (fst (fst mt)), + suffix_s (snd (fst mt)), + (snd mt)). + +(** The rule below is very similar except that it is for the -kuna +containing forms. *) + +Axiom add_kuna : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ kbase ]) -> + Fentry (cons kuna (fst (fst mt)), + suffix_kuna (snd (fst mt)), + (snd mt)). + +(** The below specifies the morphological category for accusative +marked plurals. *) + +Axiom add_plta : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ mplural ]) -> + Fentry ([ s ; ta ], + suffix_ta (snd (fst mt)), + (snd mt)). + +(** The below specifies the morphological category for accusative +marked singulars. *) + +Axiom add_ta : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ nbase ]) -> + Fentry ([ ta ], + suffix_ta (snd (fst mt)), + (snd mt)). + +(** * Mock-up of the interface + +Below I define some types for syntactic categories but I do not supply +full entries. This is because for the purposes of this simple +exposition it doesn't make sense to embed the actual types and terms +needed for Linear Categorial Grammar, which is the syntactic theory +that I assume. + +In order to hold somewhat to the spirit of the complete theory, I +define Sentry which is the predicate for valid lexical entries. *) + +Inductive syncat : Set := +| nom : matom +| nom_pl : matom +| nom_foc_pl : matom +| acc : matom +| acc_pl : matom. + +Axiom Sentry : syncat -> Prop. + +(** ** Interface rules + +I call these form-sign mappings because the lexical entries are called +signs in LCG. + +The first maps uninflected forms to the unmarked nominative. The +second, assuming that the -kuna forms are not always focal, which is +consistent with corpora, maps all mplurals to nom_pl. The third maps +the kuna forms to nom_foc_pl. The last two map -ta marked forms to the +acc and acc_pl, respectively. *) + +Axiom nbase_to_nom : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ nbase ]) -> Sentry nom. + +Axiom mplural_to_nom_pl : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ mplural ]) -> Sentry nom_pl. + +Axiom kuna_to_foc : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ kuna ]) -> Sentry nom_foc_pl. + +Axiom ta_to_acc : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ ta ]) -> Sentry acc. + +Axiom s_ta_to_acc_pl : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ s ; ta ]) -> Sentry acc_pl. diff --git a/README.org b/README.org new file mode 100644 index 0000000..c5d3fe4 --- /dev/null +++ b/README.org @@ -0,0 +1,24 @@ +* Examples from talks + +The files in this directory are mostly more fleshed out examples from +talks. They still consitute incomplete fragments but provide details +that are otherwise missing in overviews. + +** Potawatomi possession PotawatomiPoss.v + +The phenomenon is described in: + +- [[https://noah.diewald.me/files/aimm4poster.pdf][The structure of Potawatomi hybrid-class overabundance]] + +** Quechua plurals QuechuaPlural.v + +The phenomenon is described in: + +- [[https://noah.diewald.me/files/diewald2018wp.pdf][WP for sign-based CGs: a focus on morphotactics]] + +** Wao Tededo future tense WaoFuture.v + +I have not uploaded the slides yet. + + + diff --git a/WaoFuture.v b/WaoFuture.v new file mode 100644 index 0000000..b846509 --- /dev/null +++ b/WaoFuture.v @@ -0,0 +1,293 @@ +(** * Wao Tededo Future + +Below is a morphological fragment of in Lexical Proof Morphology of an +overabundant future tense pattern found in Wao Tededo (Terero). + +In Wao Tededo there is a pattern where both a synthetic form bekebopa, +'I will drink' and an analytic construction beke kebopa, can be used +in the formation of the future tense. There is much to be learned +about this pattern but the two forms are considered replaceabl by some +native speakers when context is controlled for. This indicates a +shared category of the two constructions when used in syntax. *) + +Require Import Coq.Lists.List. +Require Import Coq.Strings.String. +Import ListNotations. + +Open Scope type_scope. Open Scope string_scope. + +(** * Initial axioms of the fragment + +Below I introduce the basic lexemes and categories of the +morphological fragment. + +** Lexemes + +First I define some basic lexemes. Lexemes have no inherent +properties. They serve a role similar to foriegn keys in a relational +database. They are a key for retrieving and defining collections of +information. For instance ( LEXEME_1, x ), ( LEXEME_1, y ) puts both x +and y in the same collection, where the collection is defined in terms +of the second elements of tuples where the first element is the same +lexeme. + +The lexeme BEKI corresponds to a verb meaning 'drink'. The lexeme +KEKI corresponds to an auxiliary used to form the future tense. *) + +Inductive lexeme : Set := +| BEKI : lexeme (* drink *) +| KEKI : lexeme. (* do *) + +(** ** Morphological categories + +The type matom is for atoms used in m-category names or mcats, which I +compose like lists. Mcats are morphological categories, which +categorize observable analogical patterns in morphological form. There +are categories used to capture the "morphotactics" or the allowable +patterns of affix coocurence within words of the system and to allow +for generalizations when mapping between syntactic categories. + +In fact, what one "sees" in this system are not the categories, +themselves, which are conceptually atomic but a means of referring to +them with names. Think of the name John Smith as a category name and +Smith as analogous to an matom. Just as the last name Smith can belong +to an entire family or even multiple people in multiple families, each +person with Smith in their name is an individual and could, +potentially be named something else. Likewise, having Smith as a last +name, one of the most frequent last names in the English language, +does not entail family membership. Despite this, the system of naming +children using their parents' last names does simplify the naming of +children. Therefore if it were a rule that every child needed to be +named as a composition of the last name of a particular parent and +some individuated name, the rules of naming are greatly simplified, +even if nothing can be said to be entailed about the properties of +that individual by having a particular last name. The category naming +scheme used here, where names are lists of matoms allows for +flexibility and simplification in naming categories using rules but, +at least at this time, no rule applies because it has a particular +sub-element or sub-list, i.e.\ nothing is entailed about the category +just because a sub-element of its name is one thing or another. This +is a fundamental difference between this scheme and a feature system, +for instance. *) + +Inductive matom : Set := +| base : matom +| ke : matom +| bo : matom +| pa : matom +| bostem : matom +| pastem : matom. + +(** As stated above, mcat is a list of matoms. *) + +Definition mcat := list matom. + +(** Mcats for the fragment + +[ base ] is a basic, uninflected, stem. [ ke, base ], [ bo, base ], +etc, will be stems with -ke and -bo suffixed respectively. To provide +a little more context, bo is associated with first person, pa with +assertive, a marker of something like the indicative. The ke is used +in various contexts including what I am calling the future. It is also +correlated to an 'in order to' meaning and a limitive 'just' or 'only' +meaning, more often when used with nominals. A take away is that +nearly every form type has its own category, at least in this analysis +of this phenomenon. Labeling form types is not the only role of these +categories they also play a role in morphotactics and the interface. [ +bostem ] and [ pastem ] are categories of stems that license stems +ending in bo and pa, respectively. *) + +(** ** Morphological forms + +An mform, or morphological form, is a string. *) + +Definition mform := string. + +(** Below are some string functions to handle suffixation. *) + +Definition suffix_ke (stem:mform) : mform := + stem ++ "ke". + +Definition suffix_bo (stem:mform) : mform := + stem ++ "bo". + +Definition suffix_pa (stem:mform) : mform := + stem ++ "pa". + +(** ** The structure of morphological paradigm entries + +An mtrip is a data structure used to define Fentrys, which are +"form entries" aka morphological paradigm entries. There could +potentially be many non-Fentrys that have the type of an +mtrip. Nothing constrains this type to only be reasonable +entities. One of the purposes of the theory is to specify what +morphological forms are valid in a particular language. This is +similar to the formal language notion of defining the characteristic +function of a subset of all string combinations that correspond to a +grammar. + +Here the '*' corresponds to ×, for defining the types of pairs. *) + +Definition mtrip := mcat * mform * lexeme. + +(** The check below demonstrates why simply saying that we're working +with mtrips is not good enough. Non-grammatical triples check. We need +to be able to specify which are legal triples. *) + +Check ( [ ke, base ] , "foot" , KEKI ). + +(** Here I define Fentry, which is a predicate that is proveable when +an mtrip is a valid lexical entity. *) + +Axiom Fentry : mtrip -> Prop. + +(** Here I define the mtrip for the beki and keki stems. *) + +Definition beki_base := ([ base ], "be", BEKI) : mtrip. + +Definition keki_base := ([ base ], "ke", KEKI) : mtrip. + +(** These require an explicit axiom to be treated like an +Fentry. Other Fentries will be derived from it. *) + +Axiom f_beki_base : Fentry beki_base. + +Axiom f_keki_base : Fentry keki_base. + +(** * Morpho-Lexical relations + +lem, for "less than or equal to morphological category" is the +order over morphological categories, or mcats. What you see below are +the basic properties of an order. These state the relation is +reflexive, meaning that x ≤ x; antisymmetric, meaning that if x ≤ y +and y ≤ x then x = y; transitive, meaning that if x ≤ y and y ≤ z then +x ≤ z. *) + +Axiom lem : mcat -> mcat -> Prop. +Axiom lem_refl : forall x : mcat, lem x x. +Axiom lem_antisym : forall x y : mcat, lem x y -> lem y x -> x = y. +Axiom lem_trans : forall x y z : mcat, lem x y -> lem y z -> lem x z. + +(** The order is not natural. There may be natural orders on the +underlying list type based on length but this is not how I use +mcats. As mentioned, though their structure is complex, they are +*names* of atomic categories. + +Due to the fact that the order is not natural, each relation must be +explicitly specified, except those that are predictable from the +properties of the order. Below I specify those needed for this +fragment. *) + +Axiom base_lem_bostem : lem [ base ] [ bostem ]. +Axiom ke_base_lem_bostem : lem [ ke ; base ] [ bostem ]. +Axiom bostem_lem_pastem : lem [ bostem ] [ pastem ]. +Axiom bo_lem_pastem : lem [ bo ; base ] [ pastem ]. +Axiom bo_ke_lem_pastem : lem [ bo ; ke ; base ] [ pastem ]. + +(** ** Morphotactic rules + +In using the word "morphotactic", it may imply an imperative form +building interpretation. Though rules in this system tend to take as +input simpler forms and output more complex forms, the opposite is +possible. Defining rules in a form building direction is done for +practical reasons. Longer more complex forms are often less +frequent. If one wishes to base the assumed forms of a fragment on +something that is independently observable and be consistent about +which forms are assumed as axioms across lexemes, frequently used +forms are preferable -- or alternately, something like the principal +parts of a paradigm. The intended interpretation of these rules is +that they declare that if it is the case that Fentry x exists, then +Fentry y exists. But x does not underly y in any sense. Nor is it +necessarily contained as a subpart of y. + +Below one can see the first morphotactic rule, which I call form-form +mappings. It specifies that anything within the category of [ base ] +can have its form suffixed with -ke. The accessors that look like (fst +(fst mt)) are because the mtrip triple is actually a pair of a pair +and a lexeme, the structure is w=((x,y),z) so (fst (fst w)) is x. In +English the rule says, for any mtrip that is an Fentry, if the mcat is +less than or equal to [ base ] then there is a Fentry such that the +category is whatever was provided with matom ke added to the front, an +mform with an affixed -ke and an unchanged lexeme. *) + +Axiom add_ke : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ base ]) -> + Fentry (cons ke (fst (fst mt)), + suffix_ke (snd (fst mt)), + (snd mt)). + +(** The rule below is very similar except that it is for the -bo +containing forms. *) + +Axiom add_kuna : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ bobase ]) -> + Fentry (cons bo (fst (fst mt)), + suffix_bo (snd (fst mt)), + (snd mt)). + +(** The below specifies the morphological category for assertives. *) + +Axiom add_plta : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ pabase ]) -> + Fentry (cons pa (fst (fst mt)), + suffix_pa (snd (fst mt)), + (snd mt)). + +(** * Mock-up of the interface + +Below I define some types for syntactic categories but I do not supply +full entries. This is because for the purposes of this simple +exposition it doesn't make sense to embed the actual types and terms +needed for Linear Categorial Grammar, which is the syntactic theory +that I assume. + +In order to hold somewhat to the spirit of the complete theory, I +define Sentry which is the predicate for valid lexical entries. *) + +Inductive syncat : Set := +| V_fut_1 : matom +| V_fut_3 : matom +| V_fut_part : matom +| V_fut_part_aux_1 : matom +| V_fut_part_aux_3 : matom. + +Axiom Sentry : syncat -> Prop. + +(** ** Interface rules + +I call these form-sign mappings because the lexical entries are called +signs in LCG. + +The first maps basic stems with -ke to the future participle +category. The second maps a basic stem with -pa to the category for +the auxiliary third person, which in a proper treatment would take a +participle as an argument. The third maps a basic stem with -bopa to a +similar category for the first person. The following rules map +morphological categories to the synthetic future tense. *) + +Axiom ke_base_to_v_fut_part : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ ke ; base ]) -> Sentry V_fut_part. + +Axiom kepa_to_v_fut_part_aux_3 : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ pa ; base ]) -> + Sentry V_fut_part_aux_3. + +Axiom kepa_to_v_fut_part_aux_1 : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ pa ; bo ; base ]) -> + Sentry V_fut_part_aux_1. + +Axiom pa_ke_to_v_fut_3 : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ pa ; ke ; base ]) -> + Sentry V_fut_3. + +Axiom pa_bo_ke_to_v_fut_1 : forall + (mt : mtrip), (Fentry mt) -> + (lem (fst (fst mt)) [ pa ; bo ; ke ; base ]) -> + Sentry V_fut_1.