Redefining VDM recursive measures as well-founded lexicographic tuples

[leouk]

Ever since the discussion with Peter about translating to Isabelle recursive (and mutually recursive) functions I started to dig into the limits of VDM and how to address them.

In a nutshell, to have lexicographic tuples for measures that operate as reductive well-founded relations.

For example, VDM recursive measures work well for multiple call sites, so long as they remain direct. That is, no inner calls or complicated parameter arrangements. Concretely, the recursive measure for a the Ackerman function is hard to grasp:

ack: nat * nat -> nat 
ack(m,n) ==
    (if m = 0 then
        n+1
    else if n = 0 then
        ack(m-1, 1)
    else 
        ack(m-1, ack(m, (n-1)))
    )
measure 
    --@IsaMeasure( pair_less_VDMNat )
    --@doc where pair_less_VDMNat = lex_prod(less_than_VDMNat, less_than_VDMNat)
    --           less_than_VDMNat = transitive_closure({(z', z) | z' : int, z: int . 0 <= z' ∧ z' < z})
    --           lex_prod(ra,rb)  = { ((a,b), (a', b')) | a, b, 'a, b': int & (a,a') in set ra or a = a' and (b,b') in set rb}
is not yet specified;

Does anyone know or can suggest a good measure for something like Ackerman? I tried with variations (e.g. say from a PVS definition), but didn’t quite worked. Any suggestions?

The definition in comments is what I am using for the Isabelle translation, which uses well founded relations instead of functions (e.g., it wants to get both the callee (i.e. function parameters) and call sites (i.e. recursive calls).

Isabelle’s solution to these is the most general, yet the most difficult (to my mind). I looked into PVS and a few other provers, yet found the one for the language Dafny the easiest (and closest) to what we have.

In Dafny, they have recursive measures as a lexicographic tuple for any type (not just nat-results) that “reduce”, where reduction forms a well-founded relation:

• irreflexive: not a > a
• transitive: a > b and b > c => a > c
• no infinite descending chain: there is some value a, such that d > …. > a. (i.e. a minimal value)

They then define this ordering operator for various default types (i.e. akin to what we can do in VDM with the “ord” predicate), e.g.:

* bool: “y < x == x and not y”
* int : “y < x == y < x and 0 <= x”
* set of T: “y < x == y psubset x”
* seq of T: “y < x == y psubseq x” etc.

Finally, they define a notion of lexicographic ordering between the callee and recursive call sites, for every call site, using this operator as the “measure” test. Again, this is not dissimilar to what we would do with VDM tuples in ord predicates, like:

T == nat * nat 
ord mk_(x1, y1) < mk_(x2, y2) == x1 < x2 or (x1 = x2 and y1 < y2) 

So, for Ackerman above, using lexicographic tuples for measures and the Dafny reduction order trick, Ackerman’s measure is just:

measure
    m, n        -- or if you like, mk_(m, n) 

this will impose the checks that:

* first recursive call  :   ack(m-1, 1) == “m - 1, 1” < “m, n”, which is true given “m -1  < m”
* second call       :   ack(m-1, X) == “m - 1, X” < “m, n”, which is true for m and will depend then on “X < n”, but that’s okay from 3rd:
* third call        : X= ack(m, n-1) == “m, n-1” < “m, n”, which is true given “n - 1" 

All this is in the Dafny recent book (Sect. 3.2 and 3.3).

PS: Another topic of interest is measures for recursive (record) types, which are impossible to define I think.

[tomooda]

Leo,

Does anyone know or can suggest a good measure for something like Ackerman? I tried with variations (e.g. say from a PVS definition), but didn’t quite worked. Any suggestions?

measure mk_(m, n) looks working fine. :smile:

Another topic of interest is measures for recursive (record) types, which are impossible to define I think

Peter also threw this question at me years ago, and I couldn't make a clear answer. Maybe we need a kind of size of operator that counts the number of all values in a compound value. In the case of SL, this operator should be safe because all values are in the form of a tree while PP and RT may have a cyclic reference and thus unsafe to perform the "size-of" operator.

[leouk]

Leo,

Does anyone know or can suggest a good measure for something like Ackerman? I tried with variations (e.g. say from a PVS definition), but didn’t quite worked. Any suggestions?

measure mk_(m, n) looks working fine. 😄

Another topic of interest is measures for recursive (record) types, which are impossible to define I think

Peter also threw this question at me years ago, and I couldn't make a clear answer. Maybe we need a kind of size of operator that counts the number of all values in a compound value. In the case of SL, this operator should be safe because all values are in the form of a tree while PP and RT may have a cyclic reference and thus unsafe to perform the "size-of" operator.

Ah, wow... That's interesting. It never occurred to me to try that! That's because if you ask the type of the measure function it returns as

p measure_ack = (nat nat +> (nat nat))

as opposed to ( (nat nat) +> (nat nat)), but then I was equally surprised by the result type! I didn't know that VDM already used lexicographic measure types for complicated recursion. Neat! That's great. I never read it on the manual or in examples. Would have been quite useful to know.

In any case, isn't the measure expression betraying the expected type of ack? That is, you cannot call

p ack(mk(3, 2)) Error 3060: Too few arguments in 'RecursiveVDM' (console) at line 1:1 Args: mk(3, 2) Params: (nat, nat)

actually, worse: the call to the measure_ack function throws a type error if called with a tuple, yet accepts the measure expression? This can't be right.

p measureack(mk(3, 2)) Error 3060: Too few arguments in 'RecursiveVDM' (console) at line 1:1 Args: mk_(3, 2) Params: (nat, nat)

I guess it touches upon another point I made about VDM curried / parameter passing, as in parenthesis in the parameter calls have a curious semantic meaning! Here is the full example

ack': (nat * nat) -> nat 
    ack'(mk_(m,n)) ==
        (if m = 0 then
            n+1
        else if n = 0 then
            ack'(mk_(m-1, 1))
        else 
            ack'(mk_(m-1, ack'(mk_(m, (n-1)))))
        )
    measure 
        mk_(m, n);

p ack' = ((nat nat) -> nat) Executed in 0.001 secs. p measure_ack' = ((nat nat) +> (nat * nat)) Executed in 0.0 secs. p ack'(mk_(3,2)) = 29 Executed in 0.023 secs. p measureack'(mk(3,2)) = mk_(3, 2) Executed in 0.002 secs.

[nickbattle]

I didn't know that VDM already used lexicographic measure types for complicated recursion. Neat! That's great. I never read it on the manual or in examples. Would have been quite useful to know.

It's mentioned on pages 46/47 of the LRM, where the Ackermann function is used as an example :-)

[nickbattle]

Incidentally, the recursive PO generated for Ackermann with a lexical measure is as follows. But for some reason, it doesn't generate obligations for the second pair of recursive calls. Hmm... will investigate...

(forall m:nat, n:nat &
  (not (m = 0) =>
    ((n = 0) =>
      (let lhs = measure_ack(m, n), rhs = measure_ack((m - 1), 1) in if lhs.#1 <> rhs.#1 then lhs.#1 > rhs.#1 else lhs.#2 > rhs.#2))))

[nickbattle]

But for some reason, it doesn't generate obligations for the second pair of recursive calls

It was reporting them all at the same location sigh. Fixed. So now you get three obligations, one of which can't be evaluated :-(

Proof Obligation 3: (Unproved)
ack: recursive function obligation in 'DEFAULT' (test.vdm) at line 7:13
(forall m:nat, n:nat &
  (not (m = 0) =>
    ((n = 0) =>
      (let lhs = measure_ack(m, n), rhs = measure_ack((m - 1), 1) in if lhs.#1 <> rhs.#1 then lhs.#1 > rhs.#1 else lhs.#2 > rhs.#2))))

Proof Obligation 5: (Unproved)
ack: recursive function obligation in 'DEFAULT' (test.vdm) at line 9:13
(forall m:nat, n:nat &
  (not (m = 0) =>
    (not (n = 0) =>
      (let lhs = measure_ack(m, n), rhs = measure_ack((m - 1), ack(m, (n - 1))) in if lhs.#1 <> rhs.#1 then lhs.#1 > rhs.#1 else lhs.#2 > rhs.#2))))

Proof Obligation 7: (Unproved)
ack: recursive function obligation in 'DEFAULT' (test.vdm) at line 9:22
(forall m:nat, n:nat &
  (not (m = 0) =>
    (not (n = 0) =>
      (let lhs = measure_ack(m, n), rhs = measure_ack(m, (n - 1)) in if lhs.#1 <> rhs.#1 then lhs.#1 > rhs.#1 else lhs.#2 > rhs.#2))))

> qc
PO #1, MAYBE in 0.018s
PO #2, MAYBE in 0.007s
PO #3, MAYBE in 0.001s
PO #4, MAYBE in 0.002s
PO #5, FAILED in 1.08s: Counterexample: n = 1, m = 7
Causes Error 4174: Stack overflow in 'DEFAULT' (test.vdm) at line 11:13
----
ack: recursive function obligation in 'DEFAULT' (test.vdm) at line 9:13
(forall m:nat, n:nat &
  (not (m = 0) =>
    (not (n = 0) =>
      (let lhs = measure_ack(m, n), rhs = measure_ack((m - 1), ack(m, (n - 1))) in if lhs.#1 <> rhs.#1 then lhs.#1 > rhs.#1 else lhs.#2 > rhs.#2))))

PO #6, MAYBE in 0.003s
PO #7, MAYBE in 0.008s
> 

[leouk]

Ah! I see. I missed an important trick here.

Okay, I returned to my other more complicated examples and got a couple of surprises.

1) parameter permutation

the measure signature (as a lexicographic tuple) depends on the measure expression, not the measure definition!

   perm: int * int * int -> int --nat
   perm(m,n,r) == 
        if 0 < r then 
            perm(m, r-1, n) 
        else if 0 < n then 
            perm(r, n-1, m)
        else --if 0 <= m then 
            m
    pre 
        ((0 < r or 0 < n) => m+n+r > 0)
    measure
        max(m+n+r, 0);      

has measure_perm as (int int int +> nat). This was a "lucky" scenario (i.e. no inner calls), but what would the tuple-based measure be would be tricky? I mean, I had to add the precondition for the measure I with max. I wasn't sure how to define the measure (assuming no precondition); i.e., VDM has lexicographic order, yet no "reduction" relation but fixed to nat results.

2) Takegushi's function

An easier case with respect to measure, but harder with respect to the measure expression.

    tak: int * int * int -> int
    tak(x,y,z) == 
        if x <= y then
            y
        else    
            tak(tak(x-1,y,z), tak(y-1,z,x), tak(z-1,x,y))
   measure 
      mk_(x, y ,z)

Here the "easy" measure works neatly for nat parameters, but I couldn't immediately see (beyond a complicated if-then-else of choices for nat results) how to define it for inputs like say tak(-3,2,1).

Okay, is it then right to say that VDM does have lexicographic tuple ordering, yet not quite type-orderng beyond nat as a result? I mean, here the type of Takegushi's function result in "int int int +> (nat nat nat)" which will fail the invariant

> p tak(-3,2, 1)
Error 4065: Measure: Value -3 is not a nat in 'RecursiveVDM' (console) at line 1:1
MainThread> o
Runtime: Error 4065: Measure: Value -3 is not a nat in 'RecursiveVDM' (console) at line 1:1

I don't know about the consequence regarding ord-types about POs though. Ah! If inputs were structural, then I see Tomo's point now about size_of! You ould need a size_of for all inputs to map to nat. Humm.

Interesting. Thanks for the comments!