[CakeML-dev] Iterated bootstrap theorem?

[Yong Kiam]

Hi dev,

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
speed though.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170211/25eaa9bf/attachment.html>