Missing parts in documetation

[trsh]

Hi! I'm big fan of this work and have read every blog article, docs, etc. I kind of understand the philosophy behind it and the theory.., but what I miss is are REAL LIFE application examples. I mean.., if you could show as some tiny/small useful example (a code) with a real life application (not just theoretical), it would be probably much easier to understand the whole POINT. The example should answer questions like: "What existing problem does't it solve?" or "What new possibilities it opens?"..

It's like Physics. The lectures can go on and on, but the real knowlage and interest, in my option, comes from practical examples- when you see the connection- have to apply it to our inner/outer world.

[bvssvni]

I understand perfectly what you mean, since the research is at the meta level while practical applications are at the concrete level. So far I have put a lot of effort into understanding the meta level to obtain algorithms and insight that can be exploited in practical applications. Bit by bit I am expanding this toolbox, so it becomes a more powerful framework of reasoning over time.

In mathematics and physics, you use matrices a lot, right? Here is an example when dealing with matrices:

// The determinant of the product of two matrices is the product of their determinants.
mul_mat[det] <=> mul

Symmetric paths are properties that are preserved under some operations on elements. They are very common in many areas, but people are not used to think of them. Path semantics teaches you to go looking for them.

In logic, you would write:

∀ a, b: mat { det(a * b) = det(a) * det(b) }

It is harder to see in logic that this got something to do with the * operator (mul_mat). Path semantics makes it possible to state directly which operator we are thinking about, and it does not allow arbitrary equations. If an equation is true but not expressible in path semantics, then that's an interesting observation on its own, because most "natural" equations are equivalent to some form of path semantics. Path semantics teaches you to classify equations by their shape, whether they tell something about a function or not.

So, are path semantics limiting then, since it can't describe all equations? No!

There is no problem reasoning with path semantics at a meta level of equations:

is_expressible_in_path_semantics(equation) -> bool

Yet, this is not the only way path semantics is useful. When you have a partially understood problem, you can reason about it the way programmers do, and then go directly into proving things about it.

Here are two examples from Eco PistonDevelopers/eco#16 and PistonDevelopers/eco#34.

Path semantics is used often used for problems that are not fully understood, for example:

1. Define your problem as a system of functions (start with types, then make it more concrete, but it doesn't have to be fully implemented)
2. Describe the properties of the functions in path semantics (the more you know, the better)
3. Iterate on the design (make the parts fit together more nicely)
4. Decide how to approach finding a solution, e.g. translate to equations, traits etc.
5. Start coding (alternatively, start here if you don't know where to begin)

Path semantics is equivalent to logic, but it is constrained to talk about functions. This is something I find very valuable. If I am working with functions, then I automatically start thinking about what properties these functions have. When working with equations or logic, I don't know how to measure progress. With functions this becomes much easier.

Example: Gaussian curvature and physical simulations of soft bodies

Some concepts are also hard to understand if you don't describe them as functions. For example, the Gaussian curvature (a real number) of a physical shape in 3D is defined for any point on a surface, but what does it mean that this number is conserved when the shape is deformed? You can define points on a surface any way you like! How do we know which points are the same when deforming the shape?

• I was not aware of my ignorance of how this worked, until I started analyzing it with path semantics
• When I figured out how it worked, it was enlightened of how this could be used in practical applications

The answer is that if you create a uv-map, like in 3D programs, then you can store the Gaussian curvature in a floating point texture. The distances to neighborhood points on the surface are in equilibrium as a spring force, and Gaussian curvature describes this equilibrium in a compact way. When you deform a shape, you create tension in the curvature and this affects the soft body motion in physical simulations.

Therefore, if you model e.g. clothing in 3D with springs, you get the conservation of Gaussian curvature for free, because springs hide these laws. Intuitively:

spring_constraints_on_surface[tension_equilibrium] <=> surface_curvature

[bvssvni]

Here is another example where path semantics makes things easier to notice https://en.wikipedia.org/wiki/Triangular_matrix.

• The sum of two upper triangular matrices is upper triangular.
• The product of two upper triangular matrices is upper triangular.
• The inverse of an invertible upper triangular matrix is upper triangular.
• The product of an upper triangular matrix by a constant is an upper triangular matrix.

Notice that the descriptions from Wikipedia are only partial knowledge. They don't cover all the cases.

Written like this:

add_mat[upper_tri] <=> eq           (I'm not sure)
mul_mat[upper_tri] <=> and         (I'm not sure)
inv_mat[upper_tri] <=> id
scale_mat[upper_tri x unit -> upper_tri] <=> id     (I'm not sure)

A path semantics algorithm that searches for these connections would infer the total knowledge easily.

[bvssvni]

It's very nice to have somebody to talk about practical applications of path semantics. Feel free to ask questions and come up with ideas for what can show off the power of path semantics.

[bvssvni]

One point I made that could be clearer:

is_expressible_in_path_semantics(equation) -> bool

In path semantics, when you define a function, you are halfway through figuring out how to approach solving the problem. Instead of being this abstract problem that is hard to wrap your head around, you can write this like this:

x : [is_expressible_in_path_semantics] true
y : [is_expressible_in_path_semantics] false

It gets pretty clear what the goals are, because we are missing the piece of knowledge that determine whether an equation belongs to the set x or the set y. This does not mean the problem is hard, it is just that nobody have yet thought much about it. One also need to find a good encoding of equations, one that is easy to reason about.

I like the way path semantics makes goals clearer and more intuitive. It feels like I am just writing down what I know, and the next logical step seems to follow automatically. The notation guides me toward better understanding, filling in the gaps of knowledge that I lack.

It is also easy to notice subtle things, that you take for granted when trying to solve a problem. For example, that is_expressible_in_path_semantics should return true sometimes and false otherwise. This is not self-evident when you write down a function. As a result of recent progress on the research, I can express this precisely:

∃∃is_expressible_in_path_semantics <=> id

This is true for all surjective functions (those that outputs all values of the return type).

Now I see that since is_expressible_in_path_semantics returns a bool, there can only be one function for ∃is_expressible_in_path_semantics:

∃is_expressible_in_path_semantics <=> true_1

This is an example of how you can clarify more subtle things about a function, that is often taken as a hidden assumption.

[trsh]

@bvssvni thanks for the long input. Really appreciate it & will try to get my brain around it :))

[bvssvni]

Feel free to ask questions!

[trsh]

Can I already play with some code?

[bvssvni]

There are some experiments here: https://github.com/bvssvni/path_semantics/tree/master/dyon_experiments

These are techniques for finding paths using existing functions.