Formal Semantics in Modern Type Theories

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). ...