Studying Tau Language source code (Aug 2 2024)

Tau Language Github code analysis

The lead developer David Castro is working on some of the final pieces to finish the puzzle which is Tau Language alpha. In some of his latest commits we can see he's working on the solver and in specific the minterm solver. A solver in computer science is a piece of software which uses an algorithm to search for a solution to your described problem. There are many kinds of solvers, but in our case the kind of problem is a logic problem represented in the economical minterm normal form. A normal form is how the information is represented, and there are many different normal forms which represent information in a manner which makes it easier for machines to work with it.

In the Tau Language code base you will see a normalizer, and strong normalization is a way of processing the data, simplifying it down to it's elements. In the code base for Tau Language there also has to be satisfiability. Satisfiability means there exists at least one interpretations that makes the formula true.

A formula is satisfiable if there exists an interpretation that makes the formula true. What do I mean by this?

Consider the Boolean formula: (A OR B) AND (NOT A)

This formula is satisfiable because we can make it true by assigning:
A = false
B = true

With these assignments, the formula evaluates to true:

(false OR true) AND (NOT false) = true AND true = true.

Tau Language is also decidable, and can speak about itself due to the NSO (nullary second order logic). In the code we can see that David is currently working on iterators (part of the C++ standard library), and he's implementing a version of the solution in Ohad's TABA manual. I won't go into the solution from that manual because it's beyond the scope of this post but it explains how to build a solver, how to essentially work the formulas.

Iterating on only non-trivial minterms seems to be a way to increase computational efficiency. Also David has added some tests, apparently to allow for debugging.

All of this progress was made possible by Lucca's implementation of splitters a few days ago. Before anyone asks me, I don't know exactly what a splitter is. Ohad invented the concept, but it seems to be a sort of mathematical trick to allow Tau Language to compute the necessary solutions.

With a solver, specifically a satisfiability solver, Tau can become self optimizing. Think of solve as search, and to solve is as to search. Optimization is also a matter of search, and for these reasons you can model a problem in such a way that the computer can mechanically search for or solve for the solution. As long as an algorithm exists to do it, it can be done.

I will do more Tau code analysis in the future, and in more detail if requested.