When trying to apply supercompilation to problem solving we naturally come to
the idea of multi-result supercompilation: instead of trying to guess, which
residual graph of configurations is "the best" one, a multi-result supercompiler
(mrsc) produces a collection of residual graphs.
However, the main problem with multi-result supercompilation is that it can produce millions of residual graphs!
Luckily, filtering can be performed before producing final results of supercompilation...
How? This is explained in the preprint
- Sergei A. Grechanik, Ilya G. Klyuchnikov, Sergei A. Romanenko.
Staged multi-result supercompilation: filtering before producing.
Keldysh Institute Preprints, (70), 2013.
http://library.keldysh.ru//preprint.asp?lg=e&id=2013-70
The wiki pages are, on the one hand, a draft of the preprint, but, on the other hand, they contain some additional stuff, omitted in the preprint for the lack of space.
The paper
- Sergei Grechanik, Ilya Klyuchnikov, and Sergei Romanenko.
Staged Multi-Result Supercompilation: Filtering by Transformation.
In Fourth International Valentin Turchin Workshop on Metacomputation
(Proceedings of the Fourth International Valentin Turchin Workshop
on Metacomputation. Pereslavl-Zalessky, Russia, June 29 -
July 3, 2014).
A.V. Klimov and S.A. Romanenko, Ed. - Pereslavl-Zalessky: Publishing House "University of Pereslavl", 2014, 256 p. ISBN 978-5-901795-31-6, pages 54-78.
link PDF slides
is an extended version of the preprint.
- Is it possible to filter results that have not yet been produced?
- A model of big-step multi-result supercompilation in Agda.
- Staging big-step multi-result supercompilation.
- Cleaning lazy graphs.
- Codata and corecursion: cleaning before whistling.
- Counting without generation.
- An example: big-step supercompilation for counter systems.
- Conclusions and references.
- Source code in Agda. (Usable with Agda 2.5.2 and stdlib 0.13.)