[CakeML-dev] Iterated bootstrap theorem?
tanyongkiam at gmail.com
Sat Feb 11 21:06:19 UTC 2017
Thanks for clarifying, I was thinking of:
1) There is a compiler in the logic, e.g. compile :ast -> bytes (ignoring
2) Translate this compiler, to get some cakeml AST (in HOL) [..., val
compile = ... ]
3) Add new FFI/IO decls to the AST (as we do now) to get the full compiler
[..., val compile = ..., val main = ... ]
4) Define a new constant for the AST in 3), |- cml_ast = [..., val
compile = ..., val main = ... ]
5) Translate cml_ast to get the deeply embedded version of the AST: ``val
cml_ast = [ ... ]``
6) Stick cml_ast onto the back of 2): [ ..., val compile = ..., val cml_ast
= [ ...], val main = print (compile cml_ast)]
7) Run the in-logic compiler on 6 (doesn't need to be the same as 1)
I think Q2 would be 4) and Q1 would be 2).
How does it speed things up (maybe?): 7) would run a "fast" version of the
compiler in the logic, but it produces a program that runs a "slow" version
of the bootstrap outside the logic.
RE: translation bottleneck, it won't get past it, because we still need to
translate the whole compiler anyhow. The main purpose would be to speedup
bootstrap compilation, but I am not sure if the "fast" in-logic compiler
On Sat, Feb 11, 2017 at 6:56 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
> 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
> 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,
> 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.
> > 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
> > 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
> > what we have now (replace cml_ast with the appropriate n-1 th
> > The corresponding top-level correctness theorem would have some weird
> > assumptions about each time the bootstrap is ran.
> > One possible use of 2-fold bootstrap: one could evaluate in HOL using a
> > (but less optimizing) version of the compiler, then turn on all the
> > optimizations inside cml_ast. It probably doesn't matter for our
> > speed though.
> > _______________________________________________
> > Developers mailing list
> > Developers at cakeml.org
> > https://lists.cakeml.org/listinfo/developers
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Developers