Re: [isabelle] Some Remarks to Code Generation



On 08/01/2012 01:38 AM, Yannick Duchêne (Hibou57) wrote:
Le Tue, 31 Jul 2012 18:13:12 +0200, Patrick Michel <uni at pbmichel.de> a
écrit:
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
non‑terminating function?
Just to clarify. There is nothing "erroneous" going on here. There are just two different perspectives:

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
  runtime complexity.

cheers

chris





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.