Re: [isabelle] Some Remarks to Code Generation
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Some Remarks to Code Generation
- From: Christian Sternagel <c-sterna at jaist.ac.jp>
- Date: Wed, 01 Aug 2012 11:12:25 +0900
- In-reply-to: <op.wibki8x0ule2fv@douda-yannick>
- References: <234E321B-095C-4FBC-9DBC-CD3E5693D8D6@pbmichel.de> <op.wibki8x0ule2fv@douda-yannick>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120717 Thunderbird/14.0
On 08/01/2012 01:38 AM, Yannick Duchêne (Hibou57) wrote:
Just to clarify. There is nothing "erroneous" going on here. There are
just two different perspectives:
Le Tue, 31 Jul 2012 18:13:12 +0200, Patrick Michel <uni at pbmichel.de> a
As it turns out it is quite easy to prove a code equation that
obviously leads to non-terminating execution.
I've not reached that point (still learning Isabelle and HOL), but I'm
already interested in this, as I will generate SML programs from proofs.
Can you please, provide a concrete example of an erroneous proof of a
1) In HOL only functions that are provably total are accepted (but being
total does not mean that the same function when executed as a functional
program is terminating, since in HOL there is nothing like an evaluation
strategy). Consider, e.g.,
definition ite where
"ite b x y == if b then x else y"
lemmas ite_cong [fundef_cong] = if_cong [folded ite_def]
fun f :: "nat => nat" where
"f x = ite (x = 0) 1 (f (x - 1) * x)"
The call relation of f is well-founded (since in every recursive call
the argument is decreased by one). However when exporting code in any
language with strict evaluation, the result will loop on any input.
2) The only guarantee code-generation gives (and that is quite a strong
one) is that the generated code is a sound rewriting engine for the
function defined in the logic (assuming that every tool in the typical
chain -- e.g., compiler, OS -- is correct). Being a sound rewriting
engine means that every equation that can be derived by evaluation in
the programming language is also an equation of HOL.
See also "Code Generation via Higher-Order Rewrite Systems" by Haftmann
and Nipkow, where they state:
[...] partial correctness of the generated programs w.r.t. the
original equational theorems is guaranteed.
No claims are stated for aspects which have no explicit
representation in the logic, in particular termination or
This archive was generated by a fusion of
Pipermail (Mailman edition) and