I have been asked the question about what partial evaluation is. Partial evaluation is one of the core components behind the Tau Meta Language. In order to understand Tauchain and TML we have to do a little digging to understand not just partial evaluation but in specific the partial fixed point logic.
Self interpretation and self definition are the core of what makes Tauchain unique, and no other crypto or really any technology outside of academia will have that. Partial fixed point logic will be discussed in this blog post along with Futamura's paper on partial evalulation.
Partial Evaluation of Computation Process--An Approach to a Compiler-Compiler
Futamura's paper discusses partial evaluation as an approach to a compiler compiler. A compiler as many programmers know, is a lot like a translator. A compiler translates "source code" written in a high level formal language into "machine code" which is a lower level language. This translation process is what allows human "programmers" to communicate in a language which the machine can understand without having to speak directly in the machine code at the lowest level. With this in mind we can now understand that a compiler-compiler allows humans to describe, define, and compile a compiler, in essence allowing humans to create new programming languages.
Partial evaluation is a means of building a compiler compiler allowing this. A partial evaluation of a computation is based upon taking the formal description of the semantics of a programming language which is known as an "interpreter", allowing for description of the "evaluation procedure" which is the interpreter, to be used for defining the semantics of a programming language. So to simplify it down, the interpreter allows the advanced users of TML to define the semantics also known as the "meaning" of a programming language. This gives the user of TML a lot of flexibility, to in essence define their own programming language and then compile it (compiler-compiler). A meta compiler is what the paper describes as the ability to compile a particular language, where the partial evaluation process is where the meaning behind the semantics is defined.
A programming language is both syntax and semantics. So for future reference, after parsing is complete (syntax analysis) the meaning comes from the semantics through "semantic analysis". Partial evaluation is a process pertaining to the semantic analysis portion which takes place after syntax analysis otherwise called parsing. So we start with source code, which is input into a parser, which outputs into the generator, which at this point receives input from the partial evaluator just prior to the final stage of compilation into "machine code".
The significance of partial evaluation in Tauchain and the interesting features of partial fixed point logic
Partial evaluation is a bit of a tweak on what is usually called a compiler-compiler or parser generator. Partial fixed point logic is where the magic of TML is supposed to happen and by magic I mean the main selling points such as self defining, decidable, etc. A quick Google search of fixed point logic shows that fixed point logic has a role in model checking which is a critical design feature for Tauchain. We also learn that partial fixed point logic is more expressive on infinite structures than inflationary fixed point logic.
The critical paper comes from Imhof titled "logics that define their own semantics". It is almost magical in that in this paper we are presented with the logic which is self definable by it's nature as well as decidable. So the literature is clearly showing that theory backs TML. TML likey will be used to produce a partial fixed point logic solver which through the unique properties of this logic we will gain the magical properties promised for Tauchain. To understand partial fixed point logic fully requires a lot more in depth study, but this blog post will point potential developers in the right direction so that the most basic questions are answered.
- TML is a compiler-compiler utilizing partial evaluation.
- TML will likely be utilizing partial fixed point logic because that is the only logic in the literature which allows for self interpretation, self defining, and decidability.
- TML if implemented will represent a major technological breakthrough.
What is the significance of this breakthrough? This is the part which is hardest for me because it opens the door to so many opportunities and so much potential. For example what can developers do with the ability to inject any logic they wish, whether partial fixed point logic or some other? What does this mean for Tauchain which can now support multiple logics? What does this mean for Agoras which can be built using a decidable logic yet be expressive? PSPACE complexity, what will this allow for developers?
I'm unable to answer those questions sufficiently, but I think this is a much bigger deal than mere "Turing complete" status which we see common with the current state of the art blockchain tech. In a way this represents the next level, which is a state of the art meta language and compiler-compiler where flexibility is in the ability to communicate from human to machine.
References
Futamura, Y. (1999). Partial evaluation of computation process—an approach to a compiler-compiler. Higher-Order and Symbolic Computation, 12(4), 381-391.
Kreutzer, S. (2002, September). Partial fixed-point logic on infinite structures. In CSL (pp. 337-351).
Imhof, H. (1999). Logics that define their own semantics. Archive for Mathematical Logic, 38(8), 491-513.