Module prop::fun

Functional programming as propositions

Model is derived from PSQ, PSI and HOOO EP.

Introduction to Functional Programming

In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. For more information, see wikipedia article.

Foundational Path Semantics (PSI/PSQ/HOOO EP) is lower level than functional programming.

For example, a : T in functional programming is a primitive notion, which can not be reduced to something else. However, in foundational Path Semantics, a : T might be modelled as (a => T) ⋀ (a < T) where < is path semantical order.

Notice that in Rust, a : T is built into the language itself. The problem is that Rust does not support e.g. dependent types. This is why foundational Path Semantics is needed, to prove properties of higher level languages with more complex type systems than Rust. The motivation is to use a small set of axioms, powerful enough to develop some intuition in isolation, but also can be used as a starting point for more advanced logical frameworks.

There are many theorems that are provable in foundational Path Semantics, which are not provable in normal functional programming. Therefore, one should think about foundational Path Semantics as a more general model of mathematics.

Normal functional programming can be thought of as a “library” written in foundational Path Semantics. New operators and definitions are made using new axioms. However, these new axioms work in harmony with existing axioms.

For example, function composition g . f is not a primitive notion that is built into foundational Path Semantics. This operator needs to be defined and axioms introduced that describe mathematical properties of function composition. When these new axioms are defined, one can use them to prove theorems about function composition.

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

For information about the imaginary inverse, see the fun::inv module.

Function Extensionality

For information about function extensionality, see the fun::fun_ext module.

Dependent Types

For information about dependent types, see the fun::dep module.

Category Theory Perspective

This model seen from a Category Theory perspective produces an ∞-groupoid.

• Object: A: Prop as generic argument is an object A in the ∞-groupoid
• Morphism: Ty<F, Pow<B, A>> is a morphism F from A to B, f : A -> B
• Identity: Id<A> is the identity morphism id{A} : A -> A
• Composition: Comp<G, F> is the composition g . f
• Inverse: Inv<F> is the imaginary inverse inv(f)

The imaginary inverse adds an inverse for every morphism in the category, which results in a groupoid. However, since the inverse is imaginary, the groupoid is category realizable.

Any expression constructed from these operations can be used where A: Prop is allowed. Therefore, morphisms and higher morphisms are also objects, hence this form an ∞-groupoid.

Qubit Truths

For information about qubit truths, see the fun::id module.

Re-exports

• pub use dep::*;
• pub use feq::*;
• pub use id::*;
• pub use inv::*;

Modules

• bool_alg
  Boolean algebra
• dep
  Dependent Types
• eqx
  Equality helper macro.
• feq
  Equality
• fin
  Finite sets.
• fun_ext
  Function Extensionality
• id
  Identity function.
• inv
  Imaginary Inverse
• list
  List.
• natc
  Closed natural numbers
• natp
  Natural numbers.
• phott
  Propositional Homotopy Type Theory
• real
  Real numbers.

Structs

• App
  Applied function.
• Dup
  Duplicate function.
• FComp
  Composition.
• Fst
  Fst.
• IsConst
  Whether some symbol is a constant.
• Lam
  Lambda.
• Norm1
  f[g1 -> g2].
• Norm2
  f[g1 x g2 -> g3].
• ParTup
  Parallel tuple.
• Snd
  Snd.
• Subst
  Substitute in expression e[a := b].
• Tup
  Tuple.
• Type
  Cumulative type hierarchy.

Traits

• VProp
  Implemented by variable propositions.

Functions

• and_is_const
  is_const(a) ⋀ is_const(b) => is_const(a ⋀ b).
• app2_fun_ty
  (f : x -> y -> z) ⋀ (a : x) ⋀ (b : y) => f(a)(b) : z.
• app2_lam_ty
  (f : x => y => z) ⋀ (a : x) ⋀ (b : y) => f(a)(b) : z.
• app_eq
  (x == y) => (f(x) == f(y)).
• app_fun_ext
  (f : (x -> y)) ⋀ (g : (x -> y)) ⋀ (f(a) == g(a))^(a : x) => ∃ a : x { f == g }.
• app_fun_swap_ty
  (f(a) : y)^(a : x) => (f(b) : y)^(b : x).
• app_fun_ty
  (f : (x -> y)) ⋀ (a : x) => (f(a) : y).
• app_fun_unfold
  (f(a)^a : x -> y)^true => (f : x -> y).
• app_is_const
  is_const(f) ⋀ is_const(x) => is_const(f(x)).
• app_lam_ty
  (f : (x => y)) ⋀ (a : x) => (f(a) : y).
• app_lift_ty_lam
  (f(a) == b) ⋀ (a : x) ⋀ (b : y) => (\(a : x) = f(a)) : (x => y).
• app_map_eq
  (f == g) => (f(x) == g(y)).
• app_rev_fun_ty
  (f(a) : y)^(a : x) => (f : (x -> y)).
• app_rev_lam_ty
  (a : x) ⋀ (f(a) : y) => (f : (x => y)).
• app_tauto_lam_to_tauto_fun_ty^⚠
  (f(a)^a : x => y)^true => (f : x -> y).
• app_theory
  theory(f(x)).
• app_to_comp
  g(f(x)) => (g . f)(x).
• comp_app
  (f(a) == b) ⋀ (g(b) == c) => g(f(a)) == c.
• comp_app_def
  (f(a) == b) ⋀ (g(b) == c) ⋀ (h == (g . f)) => h(a) == c.
• comp_assoc
  h . (g . f) == (h . g) . f.
• comp_eq_left
  (f == h) => (f . g) == (h . g).
• comp_eq_right
  (g == h) => (f . g) == (f . h).
• comp_id_left
  (f : a -> b) => (id{b} . f == f).
• comp_id_right
  (f : a -> b) => (f . id{a} == f).
• comp_in_left_arg
  (g . f) ⋀ (g == h) => (h . f).
• comp_in_right_arg
  (g . f) ⋀ (f == h) => (g . h).
• comp_is_const
  is_const(f) ⋀ is_const(g) => is_const(g . f).
• comp_qu
  ~f ⋀ ~g => ~(g . f).
• comp_to_app
  (g . f)(x) => g(f(x)).
• comp_ty
  (f : x -> y) ⋀ (g : y -> z) => (g . f) : x -> z.
• const_eq
  (a == b) => (is_const(a) == is_const(b)).
• const_in_arg
  is_const(a) ⋀ (a == b) => is_const(b).
• const_tup
  is_const(a) ⋀ is_const(b) => is_const((a, b)).
• cover
  (a : b) ⋀ ((a == x) ⋁ (a == y))^(a : b) ⋀ c^(a == x) ⋀ c^(a == y) => c.
• dup_def
  dup(a) = (a, a).
• dup_is_const
  is_const(dup).
• dup_ty
  dup : a -> (a, a).
• eq_app_comp
  (g . f)(x) == g(f(x)).
• eq_app_norm1
  g2(f(inv(g1)(x))) == f[g1 -> g2](x).
• eq_app_norm2
  g3(f(inv(g1 x g2)(x))) == f[g1 x g2 -> g3](x).
• eq_norm2_norm1
  f[g1 x g2 -> g3] == f[(g1 x g2) -> g3].
• eq_norm2_norm1_comp
  f[g1 x g2 -> g3][g4 x g5 -> g6] == f[(g1 x g2) -> g3][(g4 x g5) -> g6].
• fcomp_is_const
  is_const(comp).
• fst
  t : (a, b) => fst(t) : a.
• fst_def
  fst((a, b)) = a.
• fst_is_const
  is_const(fst).
• fst_lower
  t : (x : a, b) => fst(t) == x.
• fst_ty
  fst : (a, b) -> a.
• fun_to_lam_ty^⚠
  f : x -> y => f : x => y.
• fun_ty
  (a : x) ⋀ (b : y) => (a -> b) : (x -> y).
• fun_type0
  (a : type(n)) ⋀ (b : type(m)) => (a -> b) : type(0).
• fun_type_ty
  (type(n) -> type(m)) : type(0).
• imply_is_const
  is_const(a) ⋀ is_const(b) => is_const(a => b).
• judgement_ty
  (b : type(n)) => (a : b) : type(n).
• lam
  (c : x) => ((\(a : x) = b)(c) == b[a := c]).
• lam_app_nop
  (a : x) => ((\(a : x) = b)(a) == b.
• lam_app_trivial
  (b : x) => ((\(a : x) = b)(b) == b.
• lam_app_ty
  (a : x) ⋀ (b : y) ⋀ (c : x) => ((\(a : x) = b)(c) : y).
• lam_app_ty_trivial
  (b : x) => (\(a : x) = b)(b) : x.
• lam_eq_lift
  (a : x) ⋀ (b == c) => (\(a : x) = b) == (\(a : x) = c).
• lam_fst
  (c : x) => (\(a : x) = \(b : y) = a)(c) == (\(b : y[a := c]) = c).
• lam_fst_ty
  (a : x) ⋀ (b : y) => (\(a : x) = \(b : y) = a) : x
• lam_id
  (x : type(n)) ⋀ (b : x) => (\(a : x) = a)(b) = b.
• lam_id_app_ty
  (a : x) ⋀ (b : x) => (\(a : x) = a)(b) : x.
• lam_id_eq
  (\(a : x) = a) == id{a}.
• lam_id_q
  (\(a : x) = a) ~~ id{x}.
• lam_id_ty
  (a : x) => (\(a : x) = a) : (x => x).
• lam_lift
  (a : x) ⋀ b => (\(a : x) = b).
• lam_snd
  (c : x) => (\(a : x) = \(b : y) = b)(c) == (\(b : y[a := c]) = b).
• lam_snd_ty
  (a : x) ⋀ (b : y) => (\(a : x) = \(b : y) = b) : y.
• lam_ty
  (a : x) ⋀ (b : y) => (\(a : x) = b) : (x => y).
• norm1_comp
  f[g1 -> g2][g3 -> g4] == f[(g3 . g1) -> (g4 . g2)].
• norm1_def
  f[g1 -> g2] == (g2 . f) . inv(g1).
• norm1_eq
  (f == h) => f[g1 -> g2] == h[g1 -> g2].
• norm1_eq_in
  (g1 == h) => f[g1 -> g2] == f[h -> g2].
• norm1_eq_out
  (g2 == h) => f[g1 -> g2] == f[g1 -> h].
• norm1_id
  (f : a -> b) => (f[id{a} -> id{b}] == f) for 1 argument.
• norm1_inv
  (f : a -> a) => id{a}[f -> id{a}] == inv(f).
• norm1_ty
  (f : a -> b) ⋀ (g1 : a -> c) ⋀ (g2 : b -> d) => f[g1 -> g2] : c -> d.
• norm2_app
  (inv(g1) ~~ h1) ⋀ (inv(g1) ~~ h2) ⋀ (g1(b1) = a1) ⋀ (g2(b2) = a2) ⋀ (f(b1, b2) = c) ⋀ (g3(c) = d) => f[g1 x g2 -> g3](a1, a2) = d.
• norm2_comp
  f[g1 x g2 -> g3][g4 x g5 -> g6] == f[(g4 . g1) x (g5 . g2) -> (g6 . g3)].
• norm2_def
  f[g1 x g2 -> g3] == (g3 . f) . (inv(g1) x inv(g2)).
• norm2_eq
  (f == h) => f[g1 x g2 -> g3] == h[g1 x g2 -> g3].
• norm2_ty
  (f : (a1, a2) -> b) ⋀ (g1 : a1 -> c1) ⋀ (g2 : a2 -> c2) ⋀ (g3 : b -> d) => f[g1 x g2 -> g3] : (c1, c2) -> d.
• or_is_const
  is_const(a) ⋀ is_const(b) => is_const(a ⋁ b).
• par_tup_app_is_const
  is_const(f) ⋀ is_const(g) => is_const(f x g).
• par_tup_comp
  (g1 x g2) . (f1 x f2) == ((g1 . f1) x (g2 . f2)).
• par_tup_def
  (f(i0) == o0) ⋀ (g(i1) == o1) => (f x g)(i0, i1) == (o0, o1).
• par_tup_fun_ty
  (f : (x1 -> y1)) ⋀ (g : (x2 -> y2)) => (f x g) : ((x1, x2) -> (y1, y2)).
• par_tup_id
  (id{a} x id{b}) == id{(a, b)}.
• par_tup_inv
  inv(f x g) == inv(f) x inv(g).
• par_tup_is_const
  is_const(par_tup).
• par_tup_lam_ty
  (f : (x1 => y1)) ⋀ (g : (x2 => y2)) => (f x g) : ((x1, x2) => (y1, y2)).
• pord_is_const
  is_const(a) ⋀ is_const(b) => is_const(pord(a, b)).
• q_inv_ty
  (f : A -> B) ⋀ (inv(f) ~~ g) => ((f ~~ g) : ((A -> B) ~~ (B -> A))).
• snd
  t : (a, b) => snd(t) : a.
• snd_def
  snd((a, b)) = b.
• snd_is_const
  is_const(snd).
• snd_lower
  t : (a, x : b) => snd(t) == x.
• snd_ty
  snd : (a, b) -> b.
• subst_app
  f(a)[b := c] == f[b := c](a[b := c]).
• subst_const
  is_const(a) => (a[b := c] == a).
• subst_eq
  a[c := d] == b => a[c := d][e := f] == b[e := f].
• subst_eq_lam_body
  a[c := d] == b => (\(e) = a[c := d]) == (\(e) = b).
• subst_lam
  (\(a : x) = b)[a := c] == b[a := c].
• subst_lam_const
  (\(a : x) = b)[a := c] == b[a := c].
• subst_nop
  a[b := b] == a.
• subst_trivial
  a[a := b] == b
• subst_tup
  (a, b)[c := d] == (a[c := d], b[c := d]).
• subst_ty
  (a : b) => (b[c := a] == b).
• sym_norm1_comp
  f[g1][g2] == f[g2 . g1] for 1 argument.
• sym_norm1_id
  (f : a -> a) => (f[id{a}] == f) for 1 argument.
• sym_norm1_ty
  (f : a -> a) ⋀ (g : a -> b) => f[g] : b -> b.
• sym_norm2_app
  (inv(g) ~~ h) ⋀ (g(b1) = a1) ⋀ (g(b2) = a2) ⋀ (f(b1, b2) = c) ⋀ (g(c) = d) => f[g](a1, a2) = d.
• sym_norm2_comp
  f[g1][g2] == f[g2 . g1] for 2 arguments.
• sym_norm2_id
  (f : (a, a) -> a) => f[id{a}] == f for 2 arguments.
• sym_norm2_ty
  (f : (a, a) -> a) ⋀ (g : a -> b) => f[g] : (b, b) -> b.
• tauto_lam_to_tauto_fun_ty^⚠
  (f : x => y)^true => (f^true : x -> y).
• tup3_eq_fst
  (a == b) => (a, c, d) == (b, c, d).
• tup3_eq_snd
  (a == b) => (c, a, d) == (c, b, d).
• tup3_eq_trd
  (a == b) => (c, d, a) == (c, d, b).
• tup3_fst
  (a, b, c) : (x, y, z) => (a : x).
• tup3_rev_eq_fst
  (c : x) ⋀ (d : y) ⋀ ((a, c, d) == (b, c, d)) => (a == b).
• tup3_rev_eq_snd
  (c : x) ⋀ (d : y) ⋀ ((c, a, d) == (c, b, d)) => (a == b).
• tup3_rev_eq_trd
  (c : x) ⋀ (d : y) ⋀ ((c, d, a) == (c, d, b)) => (a == b).
• tup3_snd
  (a, b, c) : (x, y, z) => (b : y).
• tup3_trd
  (a, b, c) : (x, y, z) => (c : z).
• tup_const
  is_const((a, b)) => is_const(a) ⋀ is_const(b).
• tup_eq
  (a == b) ⋀ (c == d) => (a, c) == (b, d).
• tup_eq_fst
  (a == b) => (a, c) == (b, c).
• tup_eq_fst_snd
  (a, b) == (fst((a, b)), snd((a, b))).
• tup_eq_snd
  (a == b) => (c, a) == (c, b).
• tup_fst
  (a, b) : (x, y) => (a : x).
• tup_fst_const
  is_const((a, b)) => is_const(a).
• tup_in_left_arg
  (a, b) ⋀ (a == c) => (c, b).
• tup_in_right_arg
  (a, b) ⋀ (b == c) => (a, c).
• tup_is_const
  is_const(a) ⋀ is_const(b) => is_const((a, b)).
• tup_rev_eq_fst
  (c : d) ⋀ ((a, c) == (b, c)) => (a == b).
• tup_rev_eq_snd
  (c : d) ⋀ ((c, a) == (c, b)) => (a == b).
• tup_snd
  (a, b) : (x, y) => (b : y).
• tup_snd_const
  is_const((a, b)) => is_const(b).
• tup_ty
  (a : x) ⋀ (b : y) => (a, b) : (x, y).
• tup_type_ty
  (type(n), type(m)) : type(0).
• ty_is_const
  is_const(a) ⋀ is_const(b) => is_const(a : b).
• type_imply
  type(n) => type(n+1).
• type_is_const
  is_const(type(n)).
• type_ty
  type(n) : type(n+1).

Type Definitions

• App2
  Apply 2 function arguments using function currying.
• Comp
  f . g.
• IsVar
  A proof that some symbol is not a constant.
• LamFst
  \(a : x) = \(b : y) = a.
• LamId
  \(a : x) = a.
• LamSnd
  \(a : x) = \(b : y) = b.
• Par
  Apply parallel tuple to two functions.
• ParInv
  Apply parallel tuple to two inverted functions.
• SymNorm1
  f[g] of 1 argument.
• SymNorm2
  f[g] of 2 arguments.
• Tup3
  Tuple of 3 elements.