path_semantics_std

A Rust type checked implementation of the standard dictionary of path semantics using constrained functions

Notice! This library is in early stage of development and might contain bugs and missing features!

Example: Proving addition of even numbers

```// Prove `add[even] <=> eq`, which is equal to
// `even(add(a, b)) = eq(even(a), even(b))`.
let even: Even<u32> = Even::default();

The Rust type checker proves equivalence of existential paths when calling `.path`. It is based on a neat theory of path semantics called "constrained functions". All you need to do is expressing the theorem directly in Rust code!

The example above can be shortened down to a single line:

`let path: Eq<bool> = Add::<u32>::default().path(Even::default());`

To change the constrains, use the `.i` method (using variable names for readability):

`let path: Eq<bool, (Id<bool>, Not)> = add.i((even, odd)).path(even);`

This changes the `add` function into a partial function, and it propagates the constraint such that you can see the constraint on the predictor function.

The `.ex_path` method returns an output function:

`let res: Not = add.i((even, odd)).path(even).ex_path();`

In this case we proved that if you add an even number and an odd number, you don't get an even number!

What is path semantics?

Path semantics is an attempt to make deep ideas in mathematics more accessible and theorem proving more understandable for programmers. It is an extension and unification of dependently types and guarded commands, that are used today to reason about and verify software. The major difference from existing work is that path semantics is very high level (more expressive) and allows arbitrary constraints and properties defined by functions. This makes path semantics in general undecidable, but it has rules that allows checking for consistency for specific problems, plus the strict concept of function identity that is used when extending the theory to new domains.

The syntax and notation of path semantics is designed to be concise and easily adapted to source code.

• `f{g}` means "constrain `f : A -> B` with `g : A -> bool`".
• `∀f` means "get the constraint of input of `f`".
• Existential path: `∃f : B -> bool` means "what does `f : A -> B` outputs? This depends on the constraint.
• Path: `f[g] <=> h` means "the property `g : A -> B` of `f : A -> A` is predicted by `h : B -> B`.
• Composition: `g . f` outputs `∃g{∃f}`.
• Sub-type: `x : [g] a` where `g : X -> A`, is consistent if `a : [∃g] true`.
• Naming of functions: `false_1, not, id, true_1: bool -> bool` (`id` is generic `A -> A`).
• Surjective xor non-surjective: All "normal" functions has `∃∃f => {id, true_1}`.
• Reduction of proof: `a : [f] b ∧ [g] c` is equal to `a : [f{[g] c}] b` or `a : [g{[f] b}] c`.
• Transform to equations: `f[g] <=> h` gives `g(f(a, b)) = h(g(a), g(b))` (example is for binary functions).
• Propagation of constraints to paths: Used for complain-when-wrong type checking.
• Probabilistic existential path: Like existential path, but for probability theory.
• Probabilistic path: A way to predict properties of output probabilistically from properties of input.

The theory of path semantics reveals that functions are related to each other in a natural occuring space called "path semantical space", which precisely defines the identity of all functions. Because the space is organized in a way closely related to the concept of prediction, the research has lot of overlap with artificial intelligence and machine learning. Path semantics is a field that studies how this space is organized and higher order algorithms for extracting and applying knowledge related to perfect and probabilistic prediction. It is not so much about finding solutions to a single problem, but for studying and understanding higher order reasoning to solve large classes of problems.

Features

All objects in this library are higher order representations of constrained functions. This means they do not "compute" but merely construct types of each other, in a way that Rust can type check.

• `Constrain` trait (type `.i(<constrain>)`, `.i_force` skips existential path check)
• `ExPath` trait (type `.ex_path()`)
• `Path` trait (type `.path()`, `.path_force` skips existential path check)
• Complete Boolean algebra (all paths checked with all constraints)
• Some work on natural numbers

One problem is combinatorial explosion because of the complexity of functional spaces. To work around this issue, there are some tricks applied to reduce the number of building blocks, such as using `If` and `IfK` for many non-trivial functions.

• `If` has a condition that depends on the argument that is dependend on in the branches
• `IfK` has a condition that is decided at higher order, and therefore not depended on in the branches

The `()` type is used instead of a `True1` because this looks nicer in Rust.

Structs

 Add AddK And Eq EqK Even Exc False1 GeK `(>= k)` Id If `\(x) = if co(x) {tr(x)} else {fa(x)}` IfK `\(x) = if co(k) {tr(x)} else {fa(x)}` Technically this could reduce the condition to a `bool`, but preserving the `k` makes it easier to debug. LtK `(< k)` Nand Nexc Nor Not Nrexc Odd Or Rexc Xor

Traits

 Constrain Implemented by higher order representations of constrained functions. ExPath Path