Ohad Asor has kept his word and released the first iteration of TML for peer review on Github. This is exciting news and many people have been watching Tauchain for a very long time waiting for this. In this blog post I will try my best to analyze some portions of the code but be aware that this is a task which could take multiple blog posts and explanation from Ohad himself.
What is TML?
TML is the core component which will make Tauchain possible. TML is known as the Tau Meta Language. This technology is what will allow humans and machines to effectively communicate back and forth in an organized manner. Many people may be familiar with a compiler, but fewer are familiar with what is known as a compiler-compiler or parser generator. The approach taken by TML resembles that of a parser generator. To be specific, we have what is called partial evaluation.
This quote provides a brief description of what this means when applied for TML:
A particularly interesting example of the use of partial evaluation, first described in the 1970s by Yoshihiko Futamura,[1] is when prog is an interpreter for a programming language.
This is something Ohad will have to elaborate on because the theory is very complicated and hard to explain. My own understanding is that TML will be able to have the unique properties of self interpretation and self definition. So the two concepts to study to analyze the source code thoroughly are partial evaluation (particularly as Futamura describes), and self interpretation.
#include "tml.h"
#include
int32_t evaluate(int32_t v, env &e) {
if (v > 0) return v;
env::const_iterator it = e.find(v);
if (it == e.end()) return v;
int32_t u;
while ((it = e.find(u = it->second)) != e.end());
return e[v] = u;
}
literal::literal(const literal &l, env& e) {
// DEBUG(endl<<L"evaluating "<<(*this)<<L" with "<<e<<L" giving ");
resize(l.size()), (*this)[0] = l[0];
for (size_t i = 1; i < l.size(); ++i) (*this)[i] = evaluate(l[i], e);
// DEBUG(r << endl);
}
bool literal::unify(const literal &g, env &e) const {
DEBUG(endl<<L"unifying "<<*this<<L" with "<<g<<L" given "<<e);
size_t sz = size();
if (g.size() != sz) return false;
int v;
for (size_t i = 1; i < sz; ++i) // assuming same rel
if ((v = ::evaluate(at(i), e)) > 0 && v != g[i]) return false;
else if (v < 0) e[v] = g[i];
DEBUG(L" output " << e << endl);
return true;
}
bool literal::operator==(const literal &l) const{return ((base)*this)==(base)l;}
////////////////////////////////////////////////////////////////////////////////
clause::clause(const clause& c, env& e) {for(literal *l:c)*this+=literal(*l,e);}
bool clause::operator==(const clause &l) const {
size_t sz = size();
if (sz != l.size()) return false;
for (size_t n = 0; n < sz; ++n) if (*at(n) != *l[n]) return false;
return true;
}
clause& clause::operator+=(const literal &t) {
for (size_t n = 0, s = size(); n != s; ++n)
if (abs((*at(n))[0]) == abs(t[0]) &&
t.size() == at(n)->size() &&
!memcmp(&(*at(n))[1], &t[1], (t.size()-1)*sizeof(int32_t))){
if ((*at(n))[0] != t[0]) erase(begin() + n);
return *this;
}
push_back(new literal(t));
return *this;
}
////////////////////////////////////////////////////////////////////////////////
dlp& dlp::operator+=(clause *c) {
sort(c->begin(), c->end());
for (const clause *d : *this) if (*d == *c) return *this;
size_t n;
int v;
literal *l;
//DEBUG(L"clause_push called with " << *c << endl);
//DEBUG(L"program before new clause: " << endl << *this << endl);
for (size_t k = 0; k < c->size(); ++k) {
c->rels.emplace(v = (l = c->at(k))->at(0));
index[v][size()] = k;
for (n = 1; n < l->size(); ++n)
if ((v = l->at(n)) < 0)
l->vars.emplace(v), c->vars.emplace(v);
}
push_back(c);
//DEBUG(L"program after new clause: " << endl << *this << endl);
return *this;
}
void dlp::pe(dlp &q) {
typedef const pair<size_t, size_t> index_element;
const clause *d;
const literal *g;
size_t szp, szq, iter = 0;
do { ++iter, szp = size(), szq = q.size();
for (size_t n = 0; n < q.size(); ++n)
for (size_t k = 0; k < q[n]->size(); ++k) {
g = q.at(n)->at(k);
for(index_element& x : index[-g->at(0)])
d = at(x.first),
pe(d, d->at(x.second), g, q);
DEBUG(L"finished iteration "<<iter<< L" program len " << szp << endl);
}
} while (size() != szp || q.size() != szq);
}
void dlp::pe(const clause *c, const literal *l, const literal *g, dlp &q) {
env e;
clause *d;
// DEBUG(L"pe: c="<<*c<<L" l="<<*l<<L" g="<<*g<<endl);
if (l->unify(*g, e)) {
d = new clause(*c, e);
if ((*d += *g).size() == 1) q += d;
else *this += d;
}
}
dlp::~dlp() { for (const clause *c : *this) delete c; clear(); }
clause::~clause() { for (literal *l : *this) delete l; clear(); }
int32_t main() {
setlocale(LC_ALL, "");
dlp p, q;
p.program_read(wcin);
q.program_read(wcin);
p.index_write(wcout);
q.index_write(wcout);
p.pe(q);
wcout<<p<<endl;
wcout<<q<<endl;
}
My understanding of this code is that it allows you to do partial evaluation, which I will describe as a way of translating, where the interpreter and source code are both inputs. If my understanding is correct then we can see in the code the structure for taking in both inputs. The structure uses p and q which are familiar to me from logic used for proofs, and we see the partial evaluation at "p.pe(q);". Partial evaluation to my current understanding is to fix some variables in the given code prior to execution, exploiting the fact that certain variables are not likely to change and can be fixed. Specially TML utilizes the concept of partial fixed point evaluation which in theory has been shown to allow for the self definition property necessary to make Tauchain work as intended.
DLP stands for disjunctive logic program, which has interesting implementations for knowledge representation. This post was made to introduce the concepts of partial evaluation which is critical for making sense of this code base. There are other pieces of the code base which I have not reviewed, dealing with the parser, and disjunctive logic programming is something I am not familiar with. This code however gives programmers and researchers a place to start for deeper understanding and contribution to Tau.