# 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
• 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:
```
```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
```
```
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.