During the Piston project, I (bvssvni) have developed a mathematical notation for reasoning about API design, which I figured out could be used for theorem proving. I have tried to understand the semantics and how it relates to dependently typed programming languages.
What is path semantics?
In a dependently typed language, you have to encode the “proofs” into the type:
append(vec(X), vec(Y)) -> vec(X+Y)
With path semantics, one can connect two function through another function to express the same relationship:
append(vec, vec) -> vec len(vec) -> usize append [len] (usize, usize) -> usize append [len] [:] (X, Y) -> X+Y
[:] treats members of a type as paths from the type to themselves.
0(u32) -> 0 1(u32) -> 1 2(u32) -> 2 ...
Formal definition of paths
A “path” is a function with one argument and one return value.
g(x) -> y
When a such function exists, there can possibly exist other functions, that can be inferred logically or experimentally to have the equality:
f [g] (g(x)) = g(f(x))
A such connection might exist partially or probabilistically.
Paths can also be used asymmetrically:
f([g] x, [h] y) -> [i] z
Because paths can be used asymmetrically, they can be computed with as values. This is possible to execute using a form of pattern matching stack machine, where operations are not encoded in a single instruction, but in a sequence of instructions on the stack. Verifying such programs is most likely to be undecidable.
In the pure version of path semantics where types and values emerges from the connections, an axiom of equality can be applied (analog to the univalence axiom):
F0(X0), F1(X1), F0 == F1 ------------------------ X0 == X1
This axiom states how equality is to be interpreted, for example
[g] x is not equal to
because the path
g changes the identity of the function that takes it as an argument.
In a pattern matching state machine, this causes the first match to fail so it looks for other
functions in the sub tree.
Semantics of pure paths
In a pure path theory, there are no “functions” in the normal sense, but only “terms” or “atoms”. Each term can have an associated function taking constant arguments and returning a constant. For example:
add [:] (1, 1) -> 2
Which is equal to
add( 1,  2) ->  2
To compute on numbers with pure paths, you would need one rule for every possible input. This is not practical in many applications, so a pattern matching and variable binding over multiple inputs can be used:
add [:] (X, Y) -> X + Y
The probabilistic version of a path can be interpreted as “any bit of information about an object can be used to infer some probabilistic knowledge about the object itself and its relations to other objects”. Even if this connection can not be computed exactly, it can be used as a general inference tool.
Alice is a person with red hair, Bob is a person with blue hair:
alice(person) -> alice bob(person) -> bob red_hair(person) -> bool red_hair([alice] alice) -> [true] true red_hair([bob] bob) -> [false] false
If there is a person with red hair, the probability it is Alice is 50%:
probability(bool) -> f64 is(person, person) -> bool is([red_hair] [true] true, [alice] alice) -> [probability] [0.5] 0.5
Or, written in short form:
alice: person bob: person red_hair(person) -> bool [:] (alice) -> true [:] (bob) -> false probability(bool) -> f64 is(person, person) -> bool ([red_hair] [:] true, [:] alice) -> [probability] [:] 0.5
Notice that there is no way to “type check” this connection without having saying what “probability” means. Path semantics does not tell how to model the world, but it implies there exists possibly a such connection. If there is a such connection, then there are some constraints or internal consistenty to follow relative to what is already said.
The key here is that when the function
[probability] [:] 0.5
this changes how the information gets computed later on.
We could define a logical
and gate operating on both
bool and for probability:
and(bool, bool) -> bool [:] (true, true) -> true [:] (_, _) -> false [probability] [:] (X, Y) -> X * Y
One might use path semantics to model “fuzzy” relationships between objects. The ability to verify such programs is probably an undecidable problem.
Why is this an interesting research project for Piston?
One big problem we have in the Piston project is to design APIs that satisfy some critera. These criteria change over time, and it is easy to forget what the original intentions were. Using a formal language helps guiding the design, and the ability to express “fuzzy” relationships might solve some tricky cases.
Otherwise, I think it is interesting to learn more about the internals of a such language should work. Perhaps some of these ideas might leak into some practical libraries?
I also keep an eye open to the OpenCog project, which seeks to build a human level artificial intelligence. This project uses a knowledge database called “AtomSpace”. It would be interesting if some of the patterns used in AtomSpace could be encoded with path semantics. One project currently going on in OpenCog is to make game characters smarter, which is very interesting. This project has done a lot of testing in this area, and perhaps the Piston project will explore some things in this direction.
This project has also been important for testing Piston-Meta, which might turn out to be very useful for other projects.