initial commit
This commit is contained in:
commit
7c78b560da
|
|
@ -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.
|
||||
|
|
@ -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.
|
||||
|
|
@ -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.
|
||||
|
||||
|
||||
|
||||
|
|
@ -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.
|
||||
Loading…
Reference in New Issue