I am doing Exercise 3.2 from Nipkow & Klein's Concrete Semantics book.

I arrived to a function definition that compiles at least at the covering all the cases level, but its termination is of question that I do not see through.

```
theory Minimal
imports Main
begin
type_synonym vname = string
datatype aexp = N int | V vname | Plus aexp aexp
text ‹In this exercise we verify constant folding for aexp where we
sum up all constants, even if they are not next to each other. For example, Plus
(N 1) (Plus (V x ) (N 2)) becomes Plus (V x ) (N 3). This goes beyond asimp.
Define a function full_asimp :: aexp ⇒ aexp that sums up all constants and
prove its correctness: aval (full_asimp a) s = aval a s.›
fun full_asimp :: "aexp ⇒ aexp" where
(* adding constants on top *)
"full_asimp (Plus (N i) (N j)) = N(i+j)"
(* adding constants on first and second level *)
| "full_asimp (Plus (N i) (Plus (N j) a2)) = full_asimp (Plus (N(i+j)) (full_asimp a2))"
| "full_asimp (Plus (N i) (Plus a2 (N j))) = full_asimp (Plus (N(i+j)) (full_asimp a2))"
| "full_asimp (Plus (Plus (N i) a2) (N j)) = full_asimp (Plus (N(i+j)) (full_asimp a2))"
| "full_asimp (Plus (Plus a2 (N i)) (N j)) = full_asimp (Plus (N(i+j)) (full_asimp a2))"
(* Keeping constants and variables *)
| "full_asimp (V n) = V n"
| "full_asimp (N i) = N i"
(* handling unhandled constant/variable + other cases recursively *)
| "full_asimp (Plus (V n) a2) = Plus (V n) (full_asimp a2)"
| "full_asimp (Plus a1 (V n)) = Plus (full_asimp a1) (V n)"
| "full_asimp (Plus (N i) a2) = full_asimp (Plus (N i) (full_asimp a2))"
| "full_asimp (Plus a1 (N i)) = full_asimp (Plus (full_asimp a1) (N i))"
(* handling the Plus (Plus Plus) case *)
| "full_asimp (Plus (Plus a1 a2) (Plus b1 b2)) =
full_asimp (Plus
(full_asimp (Plus a1 a2))
(full_asimp (Plus b1 b2))
)"
```

Do you have a hint what should be the next step? At all, is it possible to prove the termination of this, don't I have too much recursive calls?

```
"full_asimp (Plus a1 (N i)) = full_asimp (Plus (full_asimp a1) (N i))"
```

that line looks very suspicious.

For termination, you have to make sure that the arguments are smaller (in some sense of smaller). Esp. simpilification functions tend to not always change the argument. So look at all your calls assuming that the expression is already simplified.

The thing is, full_asimp a1 might bring up a new constant (N j) that full_asimp should take care of, combining with (N i). It might bring up a (Plus (V n) (N j)), ditto. I do not see how I could do this with less recursive calls.

The downloadable package of exercise templates on concrete-semantics.org seems to provide a bit more guidance for this exercise

Last updated: Aug 13 2022 at 06:26 UTC