339 lines
13 KiB
Coq
339 lines
13 KiB
Coq
(** * 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)) [ bostem ]) ->
|
||
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)) [ pastem ]) ->
|
||
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 : syncat
|
||
| V_fut_3 : syncat
|
||
| V_fut_part : syncat
|
||
| V_fut_part_aux_1 : syncat
|
||
| V_fut_part_aux_3 : syncat.
|
||
|
||
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.
|
||
|
||
(** ** An explanation of the syntactic categories
|
||
|
||
In reality, a verbal syntactic category is generally of the form NP -o
|
||
S for an intransitive and NP -o NP -o S for a transitive. Since the
|
||
transitivity of the periphrase should be determined by what I am
|
||
calling the participal, the actual scheme looks like the following:
|
||
|
||
|- \lambda t s.s(t)·kebopa;(NP -o V.fut.part) -o NP.1 -o S;\lambda x
|
||
P.fut(P(x))
|
||
|
||
This lexical entry for kebopa says that it takes an intransitive
|
||
future participle and then feeds it a first person argument NP.1.
|
||
|
||
|- boto;NP.1;first
|
||
|
||
This is the lexical entry of a first person pronoun.
|
||
|
||
|- epe;NP;water
|
||
|
||
The above is the lexical entry for water.
|
||
|
||
|- \lambda u v.u·v·beke;NP -o NP -o V.fut.part;\lambda w z.drink(z w)
|
||
|
||
The above is the lexical entry for beke.
|
||
|
||
First beke is combined with epe using modus ponens resulting in the
|
||
following:
|
||
|
||
|- \lambda u.u·epe·beke;NP -o V.fut.part;\lambda w.drink(water, w)
|
||
|
||
This is now of the right type to combine with kebopa resulting in:
|
||
|
||
|- \lambda t.t·epe·beke·kebopa;NP.1 -o S;\lambda x.fut(drink(water,
|
||
x))
|
||
|
||
The expression can now be combined with the first person:
|
||
|
||
|- boto·epe·beke·kebopa;S;fut(drink(water first))
|
||
|
||
The basic notion is that any participal can be made intransitive by
|
||
applying one arguement. Agreement can be handled completely by the
|
||
auxiliary, which absorbs the subject argument of the participal when
|
||
it combines with it.
|
||
|
||
*) |