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
header {* Unconstrained Fixpoint Evaluation of @{text wfrec} Is Inconsistent *}
theory Wfrec_Codegen_Inconsistency
imports Main
begin
consts_code
"wfrec" ("\<module>wfrec?")
attach {*
fun wfrec f x = f (wfrec f) x;
*}
definition
"F f x = (case x of
0 \<Rightarrow> True
| Suc 0 \<Rightarrow> False
| Suc (Suc n) \<Rightarrow> (f 0 = f (Suc 0)))"
definition "f = wfrec {} F"
lemma LFalse: "f 2 = False" by evaluation
lemma wfrec_empty: "wfrec {} H a = H (\<lambda>x. undefined) a"
proof -
from wfrec[OF wf_empty]
have "wfrec {} H a = H (cut (wfrec {} H) {} a) a" .
also have "\<dots> = H (\<lambda>x. undefined) a"
unfolding cut_def by simp
finally show ?thesis .
qed
lemma LTrue: "f 2 = True"
unfolding f_def
unfolding wfrec_empty
by (simp add: F_def)
lemma "False"
by (fold LFalse) (simp add: LTrue)
end
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
