Tauchain and the mysterious Futamura projections

Futamura Projections and Partial Evaluation

• Tauchain is based upon TML. TML being the partial evaluator allowing for the meta-language functionality.
• TML currently has implemented the BDD data structure (as discussed) and at this time is in the debugging phase.
• If TML works as intended with the BDD data structure efficiencies then Futamura projection is the next logical phase of development.

While we know Futamura projection is a planned and necessary feature it is also unlikely that most of us even know what Futamura projection is. In fact most people do not even fully understand what BDD can do in particular.

One video which can help for those who wish to study further is:

The distinction must be made between the topic of "Boolean Algebra" and "The Algebra of Boole". The Algebra of Boole is pertinent to the understanding of the BDD aspect of TML. Disclosure, I am not a mathematician so the information in the video above goes toward a level of detail which I am not qualified to express any expertise on. If you choose to take on the herculean task of carrying the cognitive load then please do so at your own risk. If you are really brave you can check out the work of Boole himself directly as well.

For all who have suffered through the cognitive workload presented in that video the next part of this discussion is on the capabilities and process of Futamura projection.

• Consider a program as a physical object. Software is physical.
• A partial evaluator can: compile, transform an interpreter into a compiler, or generate a compiler generator.
• We can have; a program specializer (spec), an interpreter (int), and a program (source).
• A specializer will specialize a program with regard to it's static input. Static inputs are command line inputs.

The formula below concisely represents exactly what partial evaluation is:

Given a program, p, static inputs SI, dynamic inputs DI, and outputs O,
we can write:

O = [ p ] ( SI,DI )

Given a partial evaluator, mix, we can write:

ps = [ mix ] ( p, SI )

where ps is the specialization of program p and:

O = [ ps ] ( DI )

We can input the description of our translator. Our translator can either be a compiler or an interpreter. What we want to describe is the process by which the defined language can translate to another language. Using an interpreter we can describe the semantics of our programming language.

How do you compile a compiler?

At the most simple and basic level we start with one input and one output. In the abstract you input your commands into the box and the box produces an output based on those commands. Most very simple software works in this way. A compiler basically takes input (source code) and produces output (a program). The source code are the acceptable commands for the compiler to produce the program with the appropriate behavior. In essence we can think of the box as nothing more than a translator device which takes one set of symbols and produces an output of another set of symbols.

Futamura offers three projections. This is a self referential process so what if instead of just one input into the box we now have two? With two inputs we can now not only send source code into the box and watch it translate into a program but now we can actually go even further and create an "interpreter". Using this second input we can now define the behavior of the box by sending a description of how you want the box to behave. In other words you can now rely on an interpreter which is distinct from a compiler in that it can only translate one statement at a time. Compilers, interpreters, and assemblers, are all translators so ultimately we have symbol manipulation at the core of all this activity.

To compile a compiler you must take an input as an interpreter and get an output as a compiler. Wikipedia provides the three projections:

1. Specializing an interpreter for given source code, yielding an executable
2. Specializing the specializer for the interpreter (as applied in #1), yielding a compiler
3. Specializing the specializer for itself (as applied in #2), yielding a tool that can convert any interpreter to an equivalent compiler

In other words Ohad will have to rely on TML to compile TML by using Futamura projection 3 in the list. In essence he will have to compile TML by using TML. This is the most confusing aspect to explain because it's a mode of self reference where TML essentially is used to create itself. The specializer is specialized for itself.

In my opinion this is a similar moment to when Satoshi Nakamoto mined the genesis block to prove Bitcoin could be built. If Ohad can achieve the feat of compiling TML using TML then we will know from this that TML is able to work. From this we can know at minimum that Tauchain on the most basic level is feasible. The question still remains on the question of logic of course. While in theory we know the logic is supposed to work it is also an area of theory which very few of us understand well. If it is demonstrated that this logic does in fact work as intended then we will know for certain that Tauchain is feasible.

Futamura projection is perhaps one of the most difficult parts of TML to explain conceptually due to the self referential nature. Excuse me if I made any errors in my attempt to explain it.

References

Boole, G. (1984). Analysis of Logic.

Web:

1. http://www.utdallas.edu/~gupta/courses/apl/peval.txt
2. http://wiki.c2.com/?ThirdFutamuraProjection
3. https://en.wikipedia.org/wiki/Partial_evaluation