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).
A lambda/closure type f : X => Y uses Ty<F, Imply<X, Y>>.
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).
Function Extensionality
It is possible to prove the following (fun_ext):
(f == g)^true => fun_ext_ty(f, g)
However, the reverse is not possible to prove.
By using path semantical quality, the path axiom makes it possible to get the inverse map:
~inv(f) ⋀ (f : x -> y) ⋀ (x -> y) => f ⋀ inv(f)
Which proves (path_inv):
~inv(f) ⋀ (f : x -> y) ⋀ (x -> y) => (y -> x)
This means, only ~inv(fun_ext(f, g)) needs to be added,
together with declaration of the type of function extensionality:
fun_ext(f, g) : (f == g)^true -> fun_ext_ty(f, g)
The path axiom might be thought of as collapsing the proof space of all
tautology transforms with inverses, together with the proof space of inverses.
With other words, it leverages PSI to say that any proof of x -> y is identical to having a
proof of y -> x when there exists an inverse and a proof f : x -> y.
Modules
Structs
Functions
is_const(a) ⋀ is_const(b) => is_const(a ⋀ b).((\(a : x) = b) : (x => y)) ⋀ (a : x) ⋀ (b : y) ⋀ (c : x) => (f(a) : y[a := c]).is_const(f) ⋀ is_const(x) => is_const(f(x)).(f : (x => y)) ⋀ (a : x) => (f(a) : y).(f(a) == b) ⋀ (a : x) ⋀ (b : y) => (\(a : x) = f(a)) : (x => y).g(f(x)) => (g . f)(x).h . (g . f) == (h . g) . f.(f == h) => (f . g) == (h . g).(g == h) => (f . g) == (f . h).id . f == f.f . id == f.(g . f) ⋀ (g == h) => (h . f).(g . f) ⋀ (f == h) => (g . h).(inv(f) . inv(g)) == inv(g . f).(inv(f) . inv(g)) => inv(g . f).is_const(f) ⋀ is_const(g) => is_const(g . f).(inv(f) . f) => id.(f . inv(f)) => id.(g . f)(x) => g(f(x)).is_const(a) ⋀ is_const(b) => is_const((a, b)).(g . f)(x) == g(f(x)).f[g1 x g2 -> g3] == f[(g1 x g2) -> g3].f[g1 x g2 -> g3][g4 x g5 -> g6] == f[(g1 x g2) -> g3][(g4 x g5) -> g6].fst((a, b)) = a.is_const(fst).(f == g)^true => fun_ext_ty(f, g).(a : x) ⋀ (f == g) => ((\(a : x) = (f(a) == g(a))) . (snd . snd))((f, g, a)).(a : x) => ((\(a : x) = (f(a) == f(a))) . (snd . snd))((f, f, a)).fun_ext_ty(f, f).fun_ext_ty(f, g) => fun_ext_ty(g, f).fun_ext_ty(f, g) ⋀ fun_ext_ty(g, h) => fun_ext_ty(f, h).fun_ext_ty(f, g) => (f == g)^true.is_const(id).inv(id) ~~ id.id => (inv(f). f).id => (f . inv(f)).is_const(a) ⋀ is_const(b) => is_const(a => b).inv(g . f) => (inv(f) . inv(g)).inv(inv(f))(x) == f(x).(f == g) => inv(f) == inv(g).inv(inv(f)) => f.is_const(f) => is_const(inv(f)).~f => ~inv(f).(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).inv(inv(f)) == f.f => inv(inv(f)).(c : x) => ((\(a : x) = b)(c) == b[a := c]).(b : x) => ((\(a : x) = b)(b) == b.(a : x) ⋀ (b : y) ⋀ (c : x) ⋀ is_const(x) => ((\(a : x) = b)(c) : y).(a : x) ⋀ (b : x) => (\(a : x) = b)(b) : x.(a : x) ⋀ (b : y) ⋀ (c : x) => ((\(a : x) = b)(c) : y[a := c]).(a : x) ⋀ (b == c) => (\(a : x) = b) == (\(a : x) = c).(c : x) => (\(a : x) = \(b : y) = a)(c) == (\(b : y[a := c]) = c).(a : x) ⋀ (b : y) => (\(a : x) = \(b : y) = a) : x(\(a : x) = a)(b) = b.(a : x) ⋀ (b : x) => (\(a : x) = a)(b) : x.(\(a : x) = a) ~~ id.(a : x) => (\(a : x) = a) : (x => x).(a : x) ⋀ b => (\(a : x) = b).(c : x) => (\(a : x) = \(b : y) = b)(c) == (\(b : y[a := c]) = b).(a : x) ⋀ (b : y) => (\(a : x) = \(b : y) = b) : y.(a : x) ⋀ (b : y) => (\(a : x) = b) : (x => y).f[g1 -> g2][g3 -> g4] == f[(g3 . g1) -> (g4 . g2)].(f == h) => f[g1 -> g2] == h[g1 -> g2].(g1 == h) => f[g1 -> g2] == f[h -> g2].(g2 == h) => f[g1 -> g2] == f[g1 -> h].id[f -> id] == inv(f).f[g1 x g2 -> g3][g4 x g5 -> g6] == f[(g4 . g1) x (g5 . g2) -> (g6 . g3)].(f == h) => f[g1 x g2 -> g3] == h[g1 x g2 -> g3].is_const(a) ⋀ is_const(b) => is_const(a ⋁ b).is_const(f) ⋀ is_const(g) => is_const(f x g).(g1 x g2) . (f1 x f2) == ((g1 . f1) x (g2 . f2)).(f(i0) == o0) ⋀ (g(i1) == o1) => (f x g)(i0, i1) == (o0, o1).(f : (x1 -> y1)) ⋀ (g : (x2 -> y2)) => (f x g) : ((x1, x2) -> (y1, y2)).(id x id) == id.inv(f x g) == inv(f) x inv(g).is_const(par_tup).(f : (x1 => y1)) ⋀ (g : (x2 => y2)) => (f x g) : ((x1, x2) => (y1, y2)).~inv(f) ⋀ (f : x -> y) ⋀ (x -> y) => f ⋀ inv(f).~inv(f) ⋀ (f : x -> y) ⋀ (x -> y) => (y -> x).is_const(a) ⋀ is_const(b) => is_const(pord(a, b)).(a -> b) : type(0).inv(f) ~~ g == f ~~ inv(g).inv(f) ~~ g => f ~~ inv(g).f ~~ inv(g) => inv(f) ~~ g.f ~~ g => inv(f) ~~ inv(g).(f : A -> B) ⋀ (inv(f) ~~ g) => ((f ~~ g) : ((A -> B) ~~ (B -> A))).~f => ~inv(inv(f)).~inv(fun_ext(f, g)).~inv(f) ⋀ (f == g)^true => ~inv(g).~inv(inv(f)) => ~f.~f ⋀ (f == g)^true => f ~~ g.~inv(f) => (f(a) == b) == (inv(f)(b) == a).(inv(f) == f) => ((f . f) == id).(f : A -> B) => ((f ~~ inv(f)) : ((A -> B) ~~ (B -> A))).snd((a, b)) = b.is_const(snd).is_const(a) => (a[b := c] == d).a[c := d] == b => a[c := d][e := f] == b[e := f].a[c := d] == b => (\(e) = a[c := d]) == (\(e) = b).a[b := a] == a.(\(a : x) = b)[a := c] == b[a := c].(\(a : x) = b)[a := c] == b[a := c].a[b := b] == ba[a := b] == b(a, b)[c := d] == (a[c := d], b[c := d]).(a : b) => (b[c := a] == b).f[g1][g2] == f[g2 . g1] for 1 argument.f[id] == f for 1 argument.f[g1][g2] == f[g2 . g1] for 2 arguments.f[id] == f for 2 arguments.(a == b) => (a, c, d) == (b, c, d).(a == b) => (c, a, d) == (c, b, d).(a == b) => (c, d, a) == (c, d, b).(a, b, c) : (x, y, z) => (a : x).(c : x) ⋀ (d : y) ⋀ ((a, c, d) == (b, c, d)) => (a == b).(c : x) ⋀ (d : y) ⋀ ((c, a, d) == (c, b, d)) => (a == b).(c : x) ⋀ (d : y) ⋀ ((c, d, a) == (c, d, b)) => (a == b).(a, b, c) : (x, y, z) => (b : y).(a, b, c) : (x, y, z) => (c : z).is_const((a, b)) => is_const(a) ⋀ is_const(b).(a == b) => (a, c) == (b, c).(a == b) => (c, a) == (c, b).(a, b) : (x, y) => (a : x).is_const(a) ⋀ is_const(b) => is_const((a, b)).(c : d) ⋀ ((a, c) == (b, c)) => (a == b).(c : d) ⋀ ((c, a) == (c, b)) => (a == b).(a, b) : (x, y) => (b : y).(a : x) ⋀ (b : y) => (a, b) : (x, y).is_const(a) ⋀ is_const(b) => is_const(a : b).type(n) => type(n+1).is_const(type(n)).type(n) : type(n+1).Type Definitions
f : ((a : x) -> p(a)).(a : x) -> p(a).f : ((a : x) => p(a)).(a : x) => p(a).\(a : x) = (f(a) == g(a)).((f, g, a) : (x -> y, x -> y, x)) -> ((\(a : x) = (f(a) == g(a))) . (snd . snd))((f, g, a)).\(a : x) = \(b : y) = a.\(a : x) = a.\(a : x) = \(b : y) = b.f[g1 -> g2].f[g1 x g2 -> g3].f[g] of 1 argument.f[g] of 2 arguments.