noah
/
morphexamples
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

elaboration and improvement of lexical meaning relation

This commit is contained in:
Noah Diewald 2021-06-04 01:20:28 -04:00
parent f184db67d2
commit 98a4164dbd
No known key found for this signature in database
GPG Key ID: EC2BAE1E100A5509
1 changed files with 11 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
Wao.v
View File

@ -136,13 +136,20 @@ Semantics. *)
Axiom big : e → prop.
Inductive meaning : ∀ s, Sns s → lₗ → mₘ → Prop :=
| meaning₁ : ∀ s (big : Sns s) l m, l = ñeneₗ → m = baseₘ → meaning s big l m.
Axiom tall : e → prop.
(** A relation for providing proofs of lexical meanings *)
Axiom small : e → prop.
Definition sense := { s : statterm & Sns s}.
Inductive meaning : sense → lₗ → mₘ → Prop :=
| m₁ : ∀ l m, l = ñeneₗ → m = baseₘ → meaning (existT Sns (func ent prp) big) l m
| m₂ : ∀ l m, l = ñeneₗ → m = baseₘ → meaning (existT Sns (func ent prp) tall) l m
| m₃ : ∀ l m, l = giitaₗ → m = baseₘ → meaning (existT Sns (func ent prp) small) 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 *)
@ -156,7 +163,7 @@ Definition ruleₛₚ (m : mₘ) (k : kₖ) (t : τ) (s : statterm) :=
(γ : Sns sₗₑₓ → Sns s)
(proofₘ : (fst α) ≤ₘ m)
(proofₖ : fₗₖ l ≤ₖ k)
(proofₛ : meaning sₗₑₓ β l (fst α)), (η (snd α), t, existT Sns s (γ β)).
(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 *)