Can I ask questions here?

[viclib]

This is supposed to be for learning purposes so I thought it would be OK to ask questions here. I am absolutely sorry if not! My doubts are:

1. What is the relationship between supercompilers and MTT composition? As far as my understanding goes, both accomplish very similar things: fusing recursive functions.
2. How wide/powerful is the idea of using supercompilation for proving? IE, could you, in theory, use it to do the same you would with Idris, but without the types?
3. Can supercompilation be used as a mean of checking function equality, in general? Even for large programs? Can you use it, say, to determine, for sure, if a function performs a sort, and then substitute it to a call to specialised sorting hardware? Or, say, to check if a function behaves like a "map" on a flat array, and redirect the computation to the GPU?
4. The language used on the paper is turing complete. Is there any benefits in making a supercompiler for a total language?

Thanks in advance and sorry again for any inconvenience.

[ilya-klyuchnikov]

Hello. Great questions, thanks for asking them.

1. I need some time to refresh my knowledge of MTT (Macro Tree Transducers, yes?) and then I will try to answer in details.
2. The idea of using supercompilation for proving in a sense appeals to two more general ideas: 1) proving via simplification and 2) proving via normalization. So, a supercompiler is just used as a simplifier/normalizer. This idea is quite wide/popular inside supercompilation community. The difference from proving via Idris is that proving in Idris is "manual proving" - you construct a proof directly (via Curry-Howard isomorphism) or you use some tactics (but this is also a manual way to construct a proof). Ideas of supercompilation may be used to code a tactic "prove by normalization via supercompilation". I and my some my colleagues have plans to implement such tactic for Coq. As for constructing proofs "without types" - it is possible, it just depends on what you consider to be a proof. If you are interested, I recommend to look into papers: "Verification as a parameterized testing (experiments with the SCP4 supercompiler)" by Lisitsa and Nemytykh http://link.springer.com/article/10.1134/S0361768807010033 - in this paper proofs are constructed informally. The second paper is "Automatic Verication of Counter Systems via Domain-Specic Multi-Result Supercompilation" by Klimov, Klyuchnikov, Romanenko - it uses the same idea, but finally proofs are done in Isabelle. Another project that exploits the idea of proving via normalization via supercompilation is TT Lite (https://github.com/ilya-klyuchnikov/ttlite).
3. The general answer is no. The problem of checking program equivalence in general is undecidable (as the halting problem). However, a supercompiler may be used to recognize that two functions (programs) are equivalent - a popular approach is to supercompile (normalize) two programs, and if supercompiled programs are the same syntactically (and supercompiler preserves equivalence) then original programs are equivalent. However, if supercompiled programs are not the same it doesn't mean that original programs are not equivalent. Moreover, there is a theorem (you can find it in "Turchin's supercompiler revisited" master's thesis by Sørensen) that a supercompiler for a call-by-name language can produce only linear improvement in performance. It means that if two programs are equivalent, but of different complexity (say, the first one is linear, while the second one is quadratic) then a traditional supercompiler is unable to recognize their equivalence.
4. Yes. Really this interesting question needs a deeper research - what are the benefits of making a supercompiler for a total language. One known technical benefit is that a supercompiler for a total language may exploits a normalizer (evaluator) to a great extent. An example is TT Lite supercompiler for a total language based on type theory. So, the obvious technical benefit from the "how to construct a supercompiler" point of view is that the fact that every expression is normalizable is valuable.

Feel free to ask other questions if something is not clear from these explanations.

[ilya-klyuchnikov]

As for the first question about MTT. Supercompilation is a general method, while MTT is a quite specific technique/algorithm for fusing functions with accumulating parameters. It is a known fact that (classical/standard) supercompilers in general are not very good at transforming functions with accumulating parameters. However, we need to distinguish supercompilation as a method and some certain supercompiler as an instantiation of this method. A supercompiler may use additional techniques/tricks to tame specific problems. So, MTT may be incorporated into a certain supercompiler.

[viclib]

Wow, thank you. You just answered questions that have been bothering me for so long, and that completely sets a new path to my work. I was already aware of it, but in the next days I will be exploring TT Lite further. I don't think I have many related questions by now, you covered pretty much everything. But if you let me ask: how mature is TT Lite (or other supercompile, maybe)? Given how performance lacking and difficult to compile are MLTT based languages today, could it be used to create a performant LLVM/JS backend now, or is it more of a research project?

Thanks again for the great work and answer.

[ilya-klyuchnikov]

TT Lite is a research project just to show that a certifying supercompiler is possible. Performance/backends are out of the scope of TT Lite at all. Try to look at Idris (it has LLVM and JS backends), Coq, Agda, etc...

[viclib]

I'm looking for a mature supercompiler for a simple functional language. I don't mind very much the language used, I just wish it was complete enough for me to use in a project. Do you know if there is any available?

PS: just reporting minor typing error on the paper, http://o7.no/1oDAkVx http://o7.no/SJaSTK

[ilya-klyuchnikov]

Hello. I suggest to look into SPSC project https://github.com/spsc/spsc-scala. It works with the same language as this project, but the full "classical" supercompilation with whistle (homeomorphic embedding) and generalization (MSG) is implemented. If you familiar with Scala, it is easy to look into details and (possibly) hack it. Also it has a working web demonstration - http://spsc.appspot.com/, so you can play with it right now.