Stream: Beginner Questions

Topic: Termination of a complex recursive function

view this post on Zulip Gergely Buday (Jan 25 2021 at 12:16):

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?

view this post on Zulip Mathias Fleury (Jan 25 2021 at 12:22):

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

that line looks very suspicious.

view this post on Zulip Mathias Fleury (Jan 25 2021 at 12:26):

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.

view this post on Zulip Gergely Buday (Jan 25 2021 at 12:44):

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.

view this post on Zulip Jakub Kądziołka (Jan 25 2021 at 12:47):

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

Last updated: Apr 19 2024 at 08:19 UTC