Appendix 7Coq Codes

A7.1. Some basic ontology and subtyping declarations

Definition CN:= Set.
Parameters Mary Helen: Woman.
Parameters John George: Man.
(** Common Nouns as Types *)
Parameters Phy Info Institution Woman Delegate : CN.Parameters Man Object Surgeon Animal Human: CN.
(** Subtyping relations **)
Axiom sw: Surgeon -> Human. Coercion sw: Surgeon >-> Human. Axiom dh: Delegate -> Human. Coercion dh: Delegate >-> Human. Axiom mh: Man -> Human. Coercion mh: Man >-> Human.
Axiom wh: Woman -> Human. Coercion wh: Woman >-> Human.
Axiom ha: Human -> Animal. Coercion ha: Human>-> Animal.
Axiom ao: Animal -> Object. Coercion ao: Animal>-> Object.
Axiom bi: Bank -> Institution. Coercion bi: Bank >-> Institution.
(** Some quantifiers *)
Definition some:=   fun A: CN=> fun P :A -> Prop=> exists x: A, P(x).
Definition all:=   fun A: CN=> fun P: A -> Prop=> forall x: A, P(x).
Definition no:=   fun A: CN=> fun P: A->Prop=> forall x: A, not(P(x)).

A7.2. Simple homonymy by overloading in coercive subtyping

(* Simple Homonymy by Overloading in Coercive Subtyping *) Set Implicit Arguments.
(* Unit type for "run" -- Onerun *)
Inductive Onerun: Set:= run.
Definition T1:= Human -> Prop.
Definition T2:= Human -> Institution -> Prop.
Parameter run1: T1. Parameter run2: T2.
Definition r1 (r: Onerun): T1:= run1. Coercion r1: Onerun >-> T1. Definition r2 (r: Onerun): T2:= run2. Coercion r2: Onerun >-> T2.
(*John runs quickly*)
Parameter quickly: forall (A: CN), (A -> Prop) -> (A -> Prop). ...

Get Formal Semantics in Modern Type Theories now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.