dependent types, phi to theta

encodings/lhol.lp

@@ -3,29 +3,29 @@ symbol Kind: TYPE
 symbol Set: TYPE
 symbol Bool: TYPE
 
-set declared "ϕ"
+set declared "θ"
 set declared "η"
 set declared "ε"
 set declared "∀"
-injective symbol ϕ: Kind → TYPE
+injective symbol θ: Kind → TYPE
 injective symbol η: Set → TYPE
 injective symbol ε: Bool → TYPE
 
-symbol {|set|}: Kind
-symbol bool: Set
+constant symbol {|set|}: Kind
+constant symbol bool: Set
 
-rule ϕ {|set|} ↪ Set
+rule θ {|set|} ↪ Set
 rule η bool ↪ Bool
 
-symbol ∀ {x: Set}: (η x → Bool) → Bool
-symbol impd {x: Bool}: (ε x → Bool) → Bool
-symbol arrd {x: Set}: (η x → Set) → Set
+constant symbol ∀ {x: Set}: (η x → Bool) → Bool
+constant symbol impd {x: Bool}: (ε x → Bool) → Bool
+constant symbol arrd {x: Set}: (η x → Set) → Set
 
 rule ε (∀ {$X} $P) ↪ Πx: η $X, ε ($P x)
 with ε (impd {$H} $P) ↪ Πh: ε $H, ε ($P h)
 with η (arrd {$X} $T) ↪ Πx: η $X, η ($T x)
 
-symbol arr: Set → Set → Set
+constant symbol arr: Set → Set → Set
 rule η (arr $X $Y) ↪ (η $X) → (η $Y)
 set infix right 6 "~>" ≔ arr
 

encodings/pvs_more.lp

+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+
+// Dependent type
+// FIXME: quantification on types must be restricted to a prenex form
+set declared "ι"
+symbol ι: Kind → TYPE
+symbol dt_arr: Kind → Kind → Kind
+set infix right 7 "*>" ≔ dt_arr
+rule ι ({|set|} *> {|set|}) ↪ θ {|set|} → θ {|set|}

paper/equal.lp

@@ -2,4 +2,4 @@ require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.prenex
 
-symbol eq: χ (∀S (λT: ϕ {|set|}, scheme (T ~> T ~> bool)))
+symbol eq: χ (∀S (λT: θ {|set|}, scheme (T ~> T ~> bool)))

prelude/logic.lp

@@ -64,9 +64,8 @@ definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))
 // Defined types
 //
 // FIXME: needs another prenex polymorphism to be encoded,
-// ∀K (λt, ? (t ~> {|set|})) ≔ λt: ϕ {|set|}, t ~> bool
-// definition pred : χ (∀S (λt, scheme (t ~> {|set|}))) ≔ λt: ϕ {|set|}, t ~> bool
-definition pred t ≔ t ~> bool
+require open personoj.encodings.pvs_more
+definition pred : ι ({|set|} *> {|set|}) ≔ λt: θ {|set|}, t ~> bool
 definition PRED ≔ pred
 definition predicate ≔ pred
 definition PREDICATE ≔ pred

prelude/numbers.lp

@@ -7,7 +7,7 @@ require open personoj.prelude.logic
 //
 // Theory numbers
 //
-constant symbol number: ϕ {|set|}
+constant symbol number: θ {|set|}
 
 //
 // Theory number_fields