-
-
Notifications
You must be signed in to change notification settings - Fork 11
What is path semantics
The difference between grammar and semantics is the following:
- Grammar describes how a language looks like.
- Semantics describes what a language means.
This notation is an attempt at constructing a new and more powerful semantics, using a building block called a "path". It extends traditional type theory where the mechanism used for type membership is a flexible construction.
Normally mathematics is a combination of formal languages and text describing the theorem proving process. In the later years, new formal languages for assisting with theorem proving has been developed. This way of doing mathematics can take advantage of computers. A program running on a computer can search for proofs between steps, such that the user can concentrate more on the idea behind the proof. The use of computer programs fill some of the roles that informal language does in mathematics to explain proofs.
The overall motivation of studying semantics is that once all rules are formalized, an implementation can be made in the computer. This makes it possible to "mine the idea space" having complex semantics built from simpler semantics. Studying of semantics is usually basic research and have no economic short term goals. However, in the long term a discovery of new semantics can have large consequences for the use of computers. Much of the software created for computers are based on sophisticated languages. The semantics of these languages describe what they mean when translated into machine instructions, which is what we care about. Exploring new semantics means new ways of translating meaning into actions.
Semantics can also play a role in transformations of symbolic relationships. The most common form of mathematical transformation is manipulating equations. For example, when moving a term from one side to another, a law describes whether the sign should change. If a number is positive on one side, it must be changed to negative when moved to the right side. This preserves the semantic relationships between the terms. The equation overall is a view into these relations.
Path semantics is all about related functions, where the relationships are also constructed by functions. When we express such relationships, we describe properties of some systems we would like to study. Ideas are formed about things that are true for the system, and then expressed in the notation. When looking at things written in the notation, we often discover new relations. Formalizing is to explain in detail what we mean when we express new ideas. The hope is that one day a computer can help with such exploration. To achieve this goal, the computer must also understand what we are looking for. If we can also express our goals in the same notation, the computer can assist with more and more sophisticated tasks. However, this will fail if the rules that govern the semantics are inconsistent. This is why it is important to find rules that behave nicely together the way we want.
The difficulty with expressing ideas is that the space of relations grows rapidly with the amount of objects. Therefore, the notation for expressing ideas must compress them into a short and understandable form. In a mathematical notation, we are interested in expressing ideas that appear frequently in mathematical thoughts. This is a big challenge because a mathematical thought is a compression of meaning in itself.
The idea of path semantics arrived from combining two advanced ideas. One was a generalized version of Adinkra diagrams which resemble an internal structure similar to direct group products. The other was investigating alternative ways to express type systems, as a computational problem. It was discovered that the information in the type system could be attached to edges in the diagrams. A compressed version of expressing such relations resulted in this notation. Since it was believed that the states of any discrete system could be fit into a diagram, and thereby representing perfect knowledge given some weak constraints, it was also believed that this knowledge could be connected to mathematics by finding axioms similar to Homotopy Type Theory.
What we are looking for in path semantics is a set of simple rules that govern the whole structure, but without loosing the expressiveness of narrowing down an idea to its essential components. It is also important to be able express incomplete formulations of ideas. Turns out that all the semantics has its root in very simple rules, but these are very hard to express computationally. This is because the rules can easily be understood when checking them against a simple problem, but when looking at the inference of global related concepts there are many possible interpretations that have less understood violations of the rules. For example, by introducing a new feature in a language, it suddenly requires complicated rules elsewhere. This is not something you can predict without a reflective understanding of the use of the language.