215 lines
7.0 KiB
Coq
215 lines
7.0 KiB
Coq
(** * 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. *)
|
||
|
||
Require Import Coq.Strings.String.
|
||
Require Import Coq.Unicode.Utf8.
|
||
Require Import Coq.Lists.List.
|
||
|
||
Open Scope type_scope. Open Scope string_scope.
|
||
|
||
(** The quasi phonological representation of morphological forms use
|
||
the string definition from the standard library. *)
|
||
|
||
Inductive mₘ : Set :=
|
||
| baseₘ
|
||
| poₘ
|
||
| concatₘ : mₘ → mₘ → mₘ.
|
||
|
||
Infix "⊙" := concatₘ (at level 60, right associativity).
|
||
|
||
(** mₘ are basic symbols used to form category names. Associated
|
||
types, functions and relations will have ₘ in their name. *)
|
||
|
||
Inductive Mₘ : mₘ → Prop :=
|
||
| baseM : Mₘ baseₘ
|
||
| poM : Mₘ poₘ.
|
||
|
||
(** Using mₘ instances, a finite number of category names Mₘ are
|
||
licensed. *)
|
||
|
||
Inductive leₘ : mₘ → mₘ → Prop :=
|
||
| reflₘ : ∀ α, Mₘ α → leₘ α α
|
||
| transₘ : ∀ α β γ, Mₘ α → Mₘ β → Mₘ γ → leₘ α β → leₘ β γ → leₘ α γ.
|
||
|
||
Axiom antisymₘ : ∀ α β : mₘ, leₘ α β → leₘ β α → α = β.
|
||
|
||
Infix "≤ₘ" := leₘ (at level 60, right associativity).
|
||
|
||
(** A partial order is defined over mₘ instances, where only Mₘ
|
||
instances are ordered. *)
|
||
|
||
Inductive lₗ : Set :=
|
||
| ñeneₗ (* big *)
|
||
| giitaₗ. (* small *)
|
||
|
||
(** Lexemes are defined as a simple inductive type lₗ. The ₗ is used
|
||
in names of types, functions and relations associated with lexemes. *)
|
||
|
||
Inductive kₖ : Set :=
|
||
| adjₖ
|
||
| anyₖ.
|
||
|
||
(** 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ₖ. *)
|
||
|
||
Inductive leₖ : kₖ → kₖ → Prop :=
|
||
| topₖ : ∀ α β, α = anyₖ → leₖ α β
|
||
| reflₖ : ∀ α, leₖ α α
|
||
| transₖ : ∀ α β γ, leₖ α β → leₖ β γ → leₖ α γ.
|
||
|
||
Axiom antisymₖ : ∀ α β, leₖ α β → leₖ β α → α = β.
|
||
|
||
Infix "≤ₖ" := leₖ (at level 60, right associativity).
|
||
|
||
(** Form classes are ordered with anyₖ as a top. *)
|
||
|
||
Definition fₗₖ (α : lₗ) : kₖ :=
|
||
match α with
|
||
| ñeneₗ => adjₖ
|
||
| giitaₗ => adjₖ
|
||
end.
|
||
|
||
(** 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. *)
|
||
|
||
Definition poₜ (stem : string) : string :=
|
||
stem ++ "po".
|
||
|
||
(** poₜ is a simple rule for suffixing the sting "po" to a base. *)
|
||
|
||
Definition mpₘₚ := (mₘ * string).
|
||
|
||
(** This type is named with ₘₚ instead of ₘₜ because it stands for
|
||
morphological paradigm. *)
|
||
|
||
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. *)
|
||
|
||
Load extensions.
|
||
|
||
(** Using Jordan Needle's formalization of Agnostic Hyper-intentional
|
||
Semantics. *)
|
||
|
||
Axiom big : e → prop.
|
||
|
||
Axiom tall : e → prop.
|
||
|
||
Axiom small : e → prop.
|
||
|
||
Axiom boat : e → prop.
|
||
|
||
Axiom hand : e → prop.
|
||
|
||
Definition sense := { s : statterm & Sns s}.
|
||
|
||
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 (β γ).
|
||
|
||
Inductive meaning : sense → lₗ → mₘ → Prop :=
|
||
m₁ : ∀ s l m, m = baseₘ → In (l, s) lexmeaning → meaning s l m
|
||
| 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.
|
||
|
||
(** A relation for providing proofs of lexical meanings. This is at
|
||
the proof of concept stage. *)
|
||
|
||
Definition spₛₚ := (ϕ * τ * sense).
|
||
|
||
(** A type alias for a lexical sign *)
|
||
|
||
Definition ruleₛₚ (m : mₘ) (k : kₖ) (t : τ) (s : statterm) :=
|
||
λ (α : mpₘₚ)
|
||
(l : lₗ)
|
||
(mp : MPₘₚ α l)
|
||
(sₗₑₓ : statterm)
|
||
(β : Sns sₗₑₓ)
|
||
(γ : Sns sₗₑₓ → Sns s)
|
||
(proofₘ : (fst α) ≤ₘ m)
|
||
(proofₖ : fₗₖ l ≤ₖ k)
|
||
(proofₛ : meaning (existT Sns sₗₑₓ β) l (fst α)),
|
||
(η (snd α), t, existT Sns s (γ β)).
|
||
|
||
(** The above is a constructor for a mapping rule between form entries
|
||
and sign entries *)
|
||
|
||
Definition e₁_identity (x : e → prop) := x.
|
||
|
||
Inductive SPₛₚ : spₛₚ → lₗ → Prop :=
|
||
simp_adjₛₚ : ∀ α l mp (sₗₑₓ : statterm) β proofₘ proofₖ proofₛ,
|
||
SPₛₚ ((ruleₛₚ baseₘ adjₖ (N ⊸ N) (func ent prp))
|
||
α 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))
|
||
α l mp (func ent prp) β e₁_identity proofₘ proofₖ proofₛ) l.
|
||
|
||
(** A SPₛₚ is a well-formed lexical sign plus a lexeme reference used
|
||
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. *)
|
||
|
||
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. *)
|
||
|