Crate path_semantics_std [−] [src]
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 add: Add<u32> = Add::default(); let even: Even<u32> = Even::default(); let path: Eq<bool> = add.path(even);
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?
A brief introduction is given here, since most people do not know what it is. For more information about path semantics, click here.
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 "constrainf : A > B
withg : A > bool
".∀f
means "get the constraint of input off
". Existential path:
∃f : B > bool
means "what doesf : A > B
outputs? This depends on the constraint.  Path:
f[g] <=> h
means "the propertyg : A > B
off : A > A
is predicted byh : B > B
.  Composition:
g . f
outputs∃g{∃f}
.  Subtype:
x : [g] a
whereg : X > A
, is consistent ifa : [∃g] true
.  Naming of functions:
false_1, not, id, true_1: bool > bool
(id
is genericA > A
).  Surjective xor nonsurjective: All "normal" functions has
∃∃f => {id, true_1}
.  Reduction of proof:
a : [f] b ∧ [g] c
is equal toa : [f{[g] c}] b
ora : [g{[f] b}] c
.  Transform to equations:
f[g] <=> h
givesg(f(a, b)) = h(g(a), g(b))
(example is for binary functions).  Propagation of constraints to paths: Used for complainwhenwrong 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 nontrivial functions.
If
has a condition that depends on the argument that is dependend on in the branchesIfK
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 

Id  
If 

IfK 

LtK 

Nand  
Nexc  
Nor  
Not  
Nrexc  
Odd  
Or  
Rexc  
Xor 
Traits
Constrain 
Implemented by higher order representations of constrained functions. 
ExPath  
Path 