Module 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 Aliases

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.