To generate images like this, see Quantum Propagation Explorer.

Path Semantics

A research project in path semantics, a re-interpretation of functions for expressing mathematics

Join us on Discord!

For an experimental implementation of a small subset of Path Semantics, see Poi.

Transcript of Talk "Introduction to Path Semantics" - This lecture was given to the Category Theory Study Group on the Applied Category Theory server (Discord).

Path Semantics is for people who want to develop deep intuition about mathematics. This means you learn to understand mathematics well enough to build your own languages for theorem proving, e.g. from scratch. The intuition of how to do this, comes from studying semantics of functions and programming by using functions.

• The semantics of functions is the fundament which programming is built upon.
• In mathematics, the functions modeled by Set Theory are pure (without side-effects and deterministic).
• Dependent Type languages uses pure functions to prove some properties of programs.

Path Semantics goes beyond Dependent Types to arbitrary sub-types, embraces undecidability and non-determinism. The notation is designed to be used with point-free theorem proving (see Poi) and can be used for analysis when a type system is not sufficient to capture all the properties of mathematical objects.

"Let's go quantum" - (2020 slogan)

Here you will find lots of papers on ideas related to mathematics, logic, language and artificial intelligence.
The common theme is to express mathematics in a way that is easier to read and understand for programmers.

• Logi - A simplified overview of our research
• Introduction to Path Semantics for Computer Scientists
• Tutorial
• Visualizing Path Semantics Using LEGO Bricks
• A brief history of Path Semantics - illustrated with stick figures
• How to think Abstractly with Path Semantics - illustrated
• Reading sequences for learning Path Semantics
• Reading sequences for Artificial Intelligence and Safety Research
• Mathematical Workflow Visualized
• About Publishing Path Semantics
• Frequently Asked Questions

Notice: This work has not yet been peer-reviewed,
except informally and partially checked by automated theorem provers.

Blog posts:

• 2021-04-04 Deriving Path Semantics from First Principles
• 2020-08-20 Improving Brute Force Theorem Proving
• 2020-04-26 The Core Axiom
• 2020-01-18 The Secret Behind 2019 Logo
• 2018-12-09 Five Things You Should Know About Path Semantics
• 2017-08-25 Homotopy and Geometry
• 2017-07-20 Generalizing Path Semantics to Probability Theory
• 2017-06-28 Standardizing Path Semantics
• 2017-06-25 Progress on Existential Paths
• 2017-06-03 Perfect Intelligence
• 2017-05-29 Golden Rationality
• 2017-04-23 Existential Paths
• 2017-04-20 Slot Lambda Calculus
• 2017-03-24 Proving Non-Existence of Monoid Symmetric Paths
• 2017-02-20 New Algorithm for Inferring Equations
• 2015-07-03 Path Semantics

What is path semantics?

Here is a cheat sheet to show how it looks like: Path Semantics Cheat Sheet

Functional programming has been an active research area for dependent types. In this notation, a new semantics that re-interprets functions takes a step beyond dependent types.

Very briefly, path semantics is about things like:

• How functions are constructed and connected
• How to express relationships between functions in a more strict way than equations
• What can be predicted about output of functions from something about the input
• What it means to refer to a function (function identity)
• What you can do with functions, given some class of knowledge about them is available
• What kind of structures are related to some class of functions

See the wiki for more information.

Why use path semantics?

Some problems require more powerful mathematical tools than others, e.g. AI safety research.
Path semantics grounds meaning in "intrinsic complexity" of functions, similar to computational type theory,
but builds up higher order concepts that stretches into the domain of philosophy.
Therefore, path semantics offers an integrated understanding of semantics spanning a wide area of applications.

An advantage of path semantics is that one can translate to and from other languages.
There are many such "bridges", from Logic to Lojban.
Among the most important connections is one between probability theory and computation,
which is formalized in path semantics.

Is this a new programming language?

A new kind of programming language, but for mathematical thinking.

Mathematical ideas are expressed in terms of functions, which are easier to program than e.g. sets. The purpose is to make mathematics more accessible and understandable in a way that relates to programming.

programming <------ path semantics ------> mathematics

Since programming and mathematis are very powerful tools on their own, it is often easier to use them to design domain specific languages for problem solving. However, doing so correctly, is easier by learning what mathematics can mean in terms of programming.

Goals:

• Create efficient algorithms that find paths
• Find deductive rules
• Find rules for well formed expressions
• Find applicable areas (machine learning etc.)
• Find generalizations (probability theory etc.)

Previous work

Some ideas are taking from unpublished work. I have been asked to publish it but have not gotten time to do it yet.

Earlier, I explored ways to encode information into a generalized version of Adinkra diagrams to model states of discrete systems. The idea is since Adinkra diagrams are constructed by labeling the edges after specific rules, one could extract rules from edges of similar diagrams representing systems.

These diagrams have a reflective property that allows related concepts to be expressed with variations in a systematic way, intuitively described as "context modelling". This background knowledge, together with dependent type experiments, served as rationale for developing the notation.

While suitable to model context in various applications, a problem is super exponential growth in memory usage. Path semantics constructs a space that appear similar to the structure of such diagrams, but compresses the information in a human readable form.

The diagrams have some important properties:

• Can be described fully using only an array of integers [a, b, c, ...]
• Uses direct group product as building block [a, b] x [c, b] = [a, b, c, d]
• The class with lowest complexity, [2, 2, ...], are edges of hypercubes, as in Adinkra diagrams
• All diagrams are subset of itself in a single dimension [N], which has the highest complexity

For algorithms to compute with these diagrams, see Context in the discrete library.