[CakeML-dev] Iterated bootstrap theorem?
tanyongkiam at gmail.com
Sat Feb 11 05:34:34 UTC 2017
This is more of a random question than anything. I was wondering if it is
possible to get a theorem about k-fold bootstrap of the compiler, i.e.
using the compiler to iterate compilation on itself once in the logic and
k-1 times (outside the logic).
Concretely, 1-fold bootstrap would be what we have right now, so the code
being compiled in the logic looks like:
val main str = print (compile conf str);
A 2-fold bootstrap could look like:
val cml_ast = ... //from an iterated translation of the compiler AST in HOL
into a translated AST
val main = print(compile conf (cml_ast));
i.e. the output is a program, that when run, compiles the compiler AST.
My sense is that such a k-fold bootstrap theorem could probably be done
with what we have now (replace cml_ast with the appropriate n-1 th
translation). The corresponding top-level correctness theorem would have
some weird nested assumptions about each time the bootstrap is ran.
One possible use of 2-fold bootstrap: one could evaluate in HOL using a
fast (but less optimizing) version of the compiler, then turn on all the
optimizations inside cml_ast. It probably doesn't matter for our bootstrap
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Developers