[isabelle-dev] consts_code wfrec (Re: Code generation in Isabelle)

[Alexander Krauss]

> Aside: On page 232 of the above-mentioned manual there is an example
> about const_code wfrec. The same is still used here in MicroJava:
> http://isabelle.in.tum.de/repos/isabelle/annotate/eee4fa79398f/src/HOL/MicroJava/J/TypeRel.thy#l100
>
> The source says "Code generator setup (FIXME!)".
>
> The changelog says: "no consts_code for wfrec, as it violates the "code
> generation = equational reasoning" principle" (before it was in
> src/HOL/Wellfounded.thy).

Here is the long version of eee4fa79398f:

Recall that our notion of "correctness of code generation" is that any 
evaluation in the generated code could theoretically be replayed by 
equational reasoning within the logic. This is the basis of the 
"evaluation oracle", which proves statements by evaluating them to true.

The attached theory shows that this is inconsistent with the above 
consts_code declaration for wfrec. I have this since 2007 and showed it 
to a bunch of people at that time. The present form uses neither recdef 
nor function, which clarifies the issue a bit. In a nutshell, the 
unconstrained evaluation lets us "prove" things that are not true in the 
logic.

> Does that mean there is something utterly wrong with MicroJava?

Not deeply, since MicroJava does not use the evaluation oracle, so it 
does not matter if code generation is sound or not. Nevertheless it 
would be good to get rid of it and to make MicroJava executable in some 
other way. Also note that this declaration (by coincidence) is not 
possible with the new code generator, since that does not seem to 
support the funny "question mark notation" for silently dropping the 
relation argument.

Alex
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: Wfrec_Codegen_Inconsistency.thy
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110724/d979d58f/attachment-0002.ksh>