2021-06-01 02:37:03 -04:00
|
|
|
|
(** * Wao Tededo Fragment
|
|
|
|
|
|
|
|
|
|
The purpose of this file is to eventually lay out a significant
|
|
|
|
|
grammatical fragment of Wao Tededo, beginning with a simple treatment
|
|
|
|
|
of adjectival classifiers. It is also a place where I plan to
|
|
|
|
|
implement various innovations of the underlying formalism. *)
|
|
|
|
|
|
2021-05-26 02:18:30 -04:00
|
|
|
|
Require Import Coq.Strings.String.
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Require Import Coq.Unicode.Utf8.
|
2021-06-04 03:00:03 -04:00
|
|
|
|
Require Import Coq.Lists.List.
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
|
|
|
|
Open Scope type_scope. Open Scope string_scope.
|
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
(** The quasi phonological representation of morphological forms use
|
|
|
|
|
the string definition from the standard library. *)
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Inductive mₘ : Set :=
|
|
|
|
|
| baseₘ
|
|
|
|
|
| poₘ
|
|
|
|
|
| concatₘ : mₘ → mₘ → mₘ.
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Infix "⊙" := concatₘ (at level 60, right associativity).
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
(** mₘ are basic symbols used to form category names. Associated
|
|
|
|
|
types, functions and relations will have ₘ in their name. *)
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Inductive Mₘ : mₘ → Prop :=
|
|
|
|
|
| baseM : Mₘ baseₘ
|
|
|
|
|
| poM : Mₘ poₘ.
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
(** Using mₘ instances, a finite number of category names Mₘ are
|
2021-06-01 02:37:03 -04:00
|
|
|
|
licensed. *)
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Inductive leₘ : mₘ → mₘ → Prop :=
|
|
|
|
|
| reflₘ : ∀ α, Mₘ α → leₘ α α
|
|
|
|
|
| transₘ : ∀ α β γ, Mₘ α → Mₘ β → Mₘ γ → leₘ α β → leₘ β γ → leₘ α γ.
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Axiom antisymₘ : ∀ α β : mₘ, leₘ α β → leₘ β α → α = β.
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Infix "≤ₘ" := leₘ (at level 60, right associativity).
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
(** A partial order is defined over mₘ instances, where only Mₘ
|
2021-06-01 02:37:03 -04:00
|
|
|
|
instances are ordered. *)
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Inductive lₗ : Set :=
|
|
|
|
|
| ñeneₗ (* big *)
|
|
|
|
|
| giitaₗ. (* small *)
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
(** Lexemes are defined as a simple inductive type lₗ. The ₗ is used
|
|
|
|
|
in names of types, functions and relations associated with lexemes. *)
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Inductive kₖ : Set :=
|
|
|
|
|
| adjₖ
|
|
|
|
|
| anyₖ.
|
2021-06-04 00:52:26 -04:00
|
|
|
|
|
|
|
|
|
(** kₖ are names of form classes, similar in concept to inflection
|
|
|
|
|
classes. The k is for the beginning sound of /klæs/ and like ₘ the ₖ
|
|
|
|
|
is used for names of types, functions and relations associated with
|
|
|
|
|
kₖ. *)
|
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Inductive leₖ : kₖ → kₖ → Prop :=
|
|
|
|
|
| topₖ : ∀ α β, α = anyₖ → leₖ α β
|
|
|
|
|
| reflₖ : ∀ α, leₖ α α
|
|
|
|
|
| transₖ : ∀ α β γ, leₖ α β → leₖ β γ → leₖ α γ.
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Axiom antisymₖ : ∀ α β, leₖ α β → leₖ β α → α = β.
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Infix "≤ₖ" := leₖ (at level 60, right associativity).
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
(** Form classes are ordered with anyₖ as a top. *)
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Definition fₗₖ (α : lₗ) : kₖ :=
|
|
|
|
|
match α with
|
|
|
|
|
| ñeneₗ => adjₖ
|
|
|
|
|
| giitaₗ => adjₖ
|
|
|
|
|
end.
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
(** Each lexeme has a form class. Hypothetically, this could
|
|
|
|
|
eventually be defined as a relation. Not much hinges on the functional
|
|
|
|
|
nature of the relation. *)
|
2021-05-26 02:18:30 -04:00
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Definition poₜ (stem : string) : string :=
|
2021-05-26 02:18:30 -04:00
|
|
|
|
stem ++ "po".
|
2021-06-01 02:37:03 -04:00
|
|
|
|
|
|
|
|
|
(** poₜ is a simple rule for suffixing the sting "po" to a base. *)
|
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
Definition mpₘₚ := (mₘ * string).
|
|
|
|
|
|
|
|
|
|
(** This type is named with ₘₚ instead of ₘₜ because it stands for
|
|
|
|
|
morphological paradigm. *)
|
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Definition ruleₘₚ (m : mₘ) (k : kₖ) (newₘ : mₘ) (t : string → string) :=
|
|
|
|
|
λ (α : mpₘₚ)
|
|
|
|
|
(l : lₗ)
|
|
|
|
|
(proofₘ : fst α ≤ₘ m)
|
|
|
|
|
(proofₖ : fₗₖ l ≤ₖ k), (newₘ, t (snd α)).
|
|
|
|
|
|
|
|
|
|
Inductive MPₘₚ : mpₘₚ → lₗ → Prop :=
|
|
|
|
|
| ñeneMP : MPₘₚ (baseₘ, "ñene") ñeneₗ
|
|
|
|
|
| giitaMP : MPₘₚ (baseₘ, "giita") giitaₗ
|
|
|
|
|
| poMP : ∀ α l proofₘ proofₖ,
|
|
|
|
|
MPₘₚ α l → MPₘₚ ((ruleₘₚ baseₘ adjₖ poₘ poₜ) α l proofₘ proofₖ) l.
|
|
|
|
|
|
|
|
|
|
(** MPₘₚ is a predicate for determining form paradigm entries. *)
|
|
|
|
|
|
|
|
|
|
Inductive Pₘₚ : mpₘₚ → mpₘₚ → Prop :=
|
|
|
|
|
| inₘₚ : ∀ α β l, MPₘₚ α l → MPₘₚ β l → Pₘₚ α β
|
|
|
|
|
| reflₘₚ : ∀ α l, MPₘₚ α l → Pₘₚ α α
|
|
|
|
|
| transₘₚ : ∀ α β γ, Pₘₚ α β → Pₘₚ β γ → Pₘₚ α γ
|
|
|
|
|
| symₘₚ : ∀ α β, Pₘₚ α β → Pₘₚ β α.
|
|
|
|
|
|
|
|
|
|
(** The form paradigm for some lexeme is an equivalence class *)
|
|
|
|
|
|
|
|
|
|
Inductive ϕ : Set :=
|
|
|
|
|
| ε
|
|
|
|
|
| η : string → ϕ
|
|
|
|
|
| concatϕ (α β : ϕ).
|
|
|
|
|
|
|
|
|
|
Infix "•" := concatϕ (at level 60, right associativity).
|
|
|
|
|
|
|
|
|
|
(** The pheno is simplified. *)
|
|
|
|
|
|
|
|
|
|
Inductive τ : Set :=
|
|
|
|
|
| NP
|
|
|
|
|
| N
|
|
|
|
|
| Fin
|
|
|
|
|
| infτ (α β : τ).
|
|
|
|
|
|
|
|
|
|
Notation "x ⊸ y" := (infτ x y) (at level 60, right associativity).
|
|
|
|
|
|
|
|
|
|
(** The tecto is simplified. *)
|
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
Load extensions.
|
2021-06-01 02:37:03 -04:00
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
(** Using Jordan Needle's formalization of Agnostic Hyper-intentional
|
|
|
|
|
Semantics. *)
|
2021-06-01 02:37:03 -04:00
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
Axiom big : e → prop.
|
2021-06-01 02:37:03 -04:00
|
|
|
|
|
2021-06-04 01:20:28 -04:00
|
|
|
|
Axiom tall : e → prop.
|
2021-06-01 02:37:03 -04:00
|
|
|
|
|
2021-06-04 01:20:28 -04:00
|
|
|
|
Axiom small : e → prop.
|
2021-06-01 02:37:03 -04:00
|
|
|
|
|
2021-06-04 03:00:03 -04:00
|
|
|
|
Axiom boat : e → prop.
|
|
|
|
|
|
|
|
|
|
Axiom hand : e → prop.
|
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
Definition sense := { s : statterm & Sns s}.
|
|
|
|
|
|
2021-06-04 03:00:03 -04:00
|
|
|
|
Definition lexmeaning : list (lₗ * sense) :=
|
|
|
|
|
cons (ñeneₗ, existT Sns (func ent prp) big)
|
|
|
|
|
(cons (ñeneₗ, existT Sns (func ent prp) tall)
|
|
|
|
|
(cons (giitaₗ, existT Sns (func ent prp) small) nil)).
|
|
|
|
|
|
|
|
|
|
Definition catmeaning : list (mₘ * sense) :=
|
|
|
|
|
cons (poₘ, existT Sns (func ent prp) boat)
|
|
|
|
|
(cons (poₘ, existT Sns (func ent prp) hand) nil).
|
|
|
|
|
|
|
|
|
|
Definition conjmeaning (α β : e → prop) : (e → prop) :=
|
|
|
|
|
λ γ,(α γ) and (β γ).
|
|
|
|
|
|
2021-06-04 01:20:28 -04:00
|
|
|
|
Inductive meaning : sense → lₗ → mₘ → Prop :=
|
2021-06-04 03:00:03 -04:00
|
|
|
|
m₁ : ∀ s l m, m = baseₘ → In (l, s) lexmeaning → meaning s l m
|
2021-06-04 03:01:48 -04:00
|
|
|
|
| m₂ : ∀ (s₁ : e → prop) (s₂ : e → prop) l m,
|
|
|
|
|
m = poₘ →
|
|
|
|
|
In (l, existT Sns (func ent prp) s₁) lexmeaning →
|
|
|
|
|
In (m, existT Sns (func ent prp) s₂) catmeaning →
|
|
|
|
|
meaning (existT Sns (func ent prp) (conjmeaning s₁ s₂)) l m.
|
2021-06-04 01:20:28 -04:00
|
|
|
|
|
|
|
|
|
(** A relation for providing proofs of lexical meanings. This is at
|
|
|
|
|
the proof of concept stage. *)
|
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
Definition spₛₚ := (ϕ * τ * sense).
|
|
|
|
|
|
|
|
|
|
(** A type alias for a lexical sign *)
|
|
|
|
|
|
|
|
|
|
Definition ruleₛₚ (m : mₘ) (k : kₖ) (t : τ) (s : statterm) :=
|
2021-06-01 02:37:03 -04:00
|
|
|
|
λ (α : mpₘₚ)
|
|
|
|
|
(l : lₗ)
|
|
|
|
|
(mp : MPₘₚ α l)
|
2021-06-04 00:52:26 -04:00
|
|
|
|
(sₗₑₓ : statterm)
|
|
|
|
|
(β : Sns sₗₑₓ)
|
|
|
|
|
(γ : Sns sₗₑₓ → Sns s)
|
2021-06-01 02:37:03 -04:00
|
|
|
|
(proofₘ : (fst α) ≤ₘ m)
|
|
|
|
|
(proofₖ : fₗₖ l ≤ₖ k)
|
2021-06-04 03:14:35 -04:00
|
|
|
|
(proofₛ : meaning (existT Sns sₗₑₓ β) l (fst α)),
|
|
|
|
|
(η (snd α), t, existT Sns s (γ β)).
|
2021-06-01 02:37:03 -04:00
|
|
|
|
|
|
|
|
|
(** The above is a constructor for a mapping rule between form entries
|
|
|
|
|
and sign entries *)
|
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
Definition e₁_identity (x : e → prop) := x.
|
|
|
|
|
|
2021-06-01 02:37:03 -04:00
|
|
|
|
Inductive SPₛₚ : spₛₚ → lₗ → Prop :=
|
2021-06-04 03:14:35 -04:00
|
|
|
|
simp_adjₛₚ : ∀ α l mp (sₗₑₓ : statterm) β proofₘ proofₖ proofₛ,
|
2021-06-04 00:52:26 -04:00
|
|
|
|
SPₛₚ ((ruleₛₚ baseₘ adjₖ (N ⊸ N) (func ent prp))
|
2021-06-04 03:14:35 -04:00
|
|
|
|
α l mp (func ent prp) β e₁_identity proofₘ proofₖ proofₛ) l
|
|
|
|
|
| po_adjₛₚ : ∀ α l mp (sₗₑₓ : statterm) β proofₘ proofₖ proofₛ,
|
|
|
|
|
SPₛₚ ((ruleₛₚ poₘ adjₖ (N ⊸ N) (func ent prp))
|
2021-06-04 00:52:26 -04:00
|
|
|
|
α l mp (func ent prp) β e₁_identity proofₘ proofₖ proofₛ) l.
|
2021-06-01 02:37:03 -04:00
|
|
|
|
|
2021-06-04 00:52:26 -04:00
|
|
|
|
(** A SPₛₚ is a well-formed lexical sign plus a lexeme reference used
|
2021-06-04 03:14:35 -04:00
|
|
|
|
to simplify the identification of paradigms. The first constructor is
|
|
|
|
|
for basic adjective with no classifier. The second is for an adjective
|
|
|
|
|
with a classifier that takes a syntactic argument. *)
|
2021-06-01 02:37:03 -04:00
|
|
|
|
|
|
|
|
|
Inductive Pₛₚ : spₛₚ → spₛₚ → Prop :=
|
|
|
|
|
| inₛₚ : ∀ α β l, SPₛₚ α l → SPₛₚ β l → Pₛₚ α β
|
|
|
|
|
| reflₛₚ : ∀ α l, SPₛₚ α l → Pₛₚ α α
|
|
|
|
|
| transₛₚ : ∀ α β γ, Pₛₚ α β → Pₛₚ β γ → Pₛₚ α γ
|
|
|
|
|
| symₛₚ : ∀ α β, Pₛₚ α β -> Pₛₚ β α.
|
|
|
|
|
|
|
|
|
|
(** A sign paradigm is an equivalence class. *)
|
|
|
|
|
|