The first instance of Tau MetaLanguage (TML) has appeared on Github!

in crypto-news •  2 years ago  (edited)

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 <algorithm>

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.

References

  1. https://github.com/idni/tau
  2. https://en.wikipedia.org/wiki/Partial_evaluation
  3. https://gist.github.com/tomykaira/3159910
Authors get paid when people like you upvote their post.
If you enjoyed what you read here, create your account today and start earning FREE STEEM!
Sort Order:  

This project is very different from anything else out there

A self defining, decidable logic under pspace that acts as a compiler-compiler is very non trivial and took years of research, and now he's achieved the centerpiece that will allow for a lot of extraordinary features to come

Ohad will be releasing a set of explanations soon that will detail this and I'm looking forward to it.

This guy is truly something else, he's the smartest person with whom I've ever interacted and I'm glad I found out about the project through your posts.

·

It Works! https://github.com/IDNI/tau/blob/master/example

This is what it computes:

The version TML computes is a slight variation but based on the same concepts.

·

Also we cannot forget Henrik Imhof's work on partial fixed point logic which seems very relevant for TML. The logic is something I'm unfamiliar with so I don't discuss it in detail in this post but it is something critical for the self defining property of TML. This is something for Ohad to describe best in my opinion because logic is not standard knowledge common for programmers.

The fact that the code works represents a breakthrough because it's a practical implementation where "the proof is in the pudding" as they say.

Congratulations @dana-edwards, this post is the eighth most rewarded post (based on pending payouts) in the last 12 hours written by a Hero account holder (accounts that hold between 10 and 100 Mega Vests). The total number of posts by Hero account holders during this period was 378 and the total pending payments to posts in this category was $7073.03. To see the full list of highest paid posts across all accounts categories, click here.

If you do not wish to receive these messages in future, please reply stop to this comment.

Tau-Chain always looked verry interesting and seems they are going in a good direction. They do have this explainer video wich lookz like an LSD trip

damn it I tried to snap up some Agoras but they already skyrocketed +51%
thanks for the heads up anyway, I'll keep an eye out for a better entry.

I totally don't understand the coding or technical aspects of this, but your earlier summaries of Tauchain's potentials sold me on the investment - great news hearing the code has finally come out. A wonderful early Xmas present. :-)

·

Well if you know how a compiler works, where you take a document as input, parse it and it outputs as an o file or exe? In the case of TML you will be able to input a document defining the programming language, so this means Tau will be like an Internet of Languages. To explain in depth will require Ohad but the breakthrough of TML is that unlike what you have with Ethereum or Tezos where you have to basically work within the box, in Tau you define the box using TML.

·
·

Thanks for the analogy. However, I agree with rok-sivante that the implications of such a breakthrough are difficult to grasp, our brains being so familiar with using programming langages, not create them.

Congratulations, your post received one of the top 10 most powerful upvotes in the last 12 hours. You received an upvote from @trafalgar valued at 101.06 SBD, based on the pending payout at the time the data was extracted.

If you do not wish to receive these messages in future, reply with the word "stop".

Thanx you so much dear @dana-adwards for sharing this crypto news.

After long years of waiting, finally! Yes! Now we wait for the explanation included in the whitepaper.

Excellent attempt at explaining Tau. Continue working on making it simple, with metaphor too. "A true leader does not seek to enlighten the people, but help them achieve simplicity" - A wise dude.

The only word I recognised was 'Futurama'.
My favourite is zoidberg.

Thank you for this post, it really helped to answer some of the questions I had when looking at the github code. I am very much looking forward to see how it pans out, and hope that eventually I too will be able to contribute to the project in a meaningful manner. Have a great day!