Expand description
Functional programming as propositions
Model is derived from PSQ, PSI and HOOO EP.
Types
A type x : T uses Ty<X, T> from the path_semantics module (PSI).
A function type f : X -> Y uses Ty<F, Pow<Y, X>> from the hooo module (HOOO EP).
Imaginary Inverse
The syntax ~x uses Qu<X> from the qubit module,
and the syntax x ~~ y uses Q<X, Y> from the quality module.
This model uses imaginary inverse
inv(f) with ~inv(f) as a proof of bijective inverse.
Here, ~ means the path semantical qubit operator, such that:
(inv(f) ~~ g) => ~inv(f)
It means that one uses path semantical quality instead of equality for inverses.
Path semantical quality inv(f) ~~ g also implies inv(f) == g,
which is useful in proofs.
The inv_val_qu axiom makes it possible to compute using the inverse:
(~inv(f) ⋀ (f(x) == y)) => (inv(f)(y) == x)
The reason for this design is that inv(f) == inv(f) is a tautology,
and Rust’s type system can’t pattern match on 1-avatars with inequality in rules like in
Avatar Logic.
By using a partial equivalence operator ~~ instead of ==,
one can not prove inv(f) ~~ inv(f) without any assumptions.
This solves the problem such that axioms can be added,
only for functions that have inverses.
If a function f has no inverse, it is useful to prove false^(inv(f) ~~ g).
Modules
Structs
Functions
g(f(x)) => (g . f)(x).(g . f) ⋀ (g == h) => (h . f).(g . f) ⋀ (f == h) => (g . h).(inv(f) . inv(g)) => inv(g . f).(inv(f) . f) => id.(f . inv(f)) => id.(g . f)(x) => g(f(x)).inv(id) ~~ id.inv(g . f) => (inv(f) . inv(g)).(f : x -> y) => (inv(f) : y -> x).f if there exists a proof g.f by g.f if there exists a proof ~inv(f).(a -> b) : type(0).(f : A -> B) ⋀ (inv(f) ~~ g) => ((f ~~ g) : ((A -> B) ~~ (B -> A))).(f : A -> B) => ((f ~~ inv(f)) : ((A -> B) ~~ (B -> A))).type(n) : type(n+1).