[CakeML-dev] Iterated bootstrap theorem?

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Sat Feb 11 11:56:30 UTC 2017


This looks like an interesting idea. I haven't understood it fully.
Let me try to clarify.
Here are 2 questions I have about your 2-fold example, which I'll copy below:

val prog2fold = process_topdecs`
val (compile,conf) = ^Q1;
val cml_ast = ^Q2;
val main = print(compile conf cml_ast);`

My questions are about what Q1 and Q2 should be.

I assume the above program, prog2fold, is going to be used as input
for proof-grounded evaluation of the compiler, i.e., we will produce a
theorem like this by EVAL: |- compile ^prog2fold = <... some bytes
...>

I guess Q2 is produced by translator (i.e., what is currently in
compiler/bootstrap/translation). I understand that part, if so.

Is Q1 also produced by the translator? i.e., we roughly have Q1 = Q2?
Or what is it?

I think this would be interesting if it provided a principled way to
substantially increase the speed for bootstrapping. It also seems like
it would interact interestingly with the eval primitive. It seems to
have no effect on the translation-time bottleneck for bootstrap speed,
though.

On 11 February 2017 at 16:34, Yong Kiam <tanyongkiam at gmail.com> wrote:
> 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.
>
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>



More information about the Developers mailing list