Re: [PVS-Help] TCC Question (Stack followup)

[David Coppit <sri@coppit.org>]

On Mon, 3 Oct 2005, Jeff Maddalon wrote:

> Now back to the version with TCCs.  Since the TCCs arise in the definition of
> multiple_add_sub, you cannot "expand" multiple_add_sub.  In the same way as
> trying to prove gt0, you will need more information about the return type.

First, thanks to jeff and Bruno for helping me to understand the issue.

One final question: What do I do in cases where the value of the return
type cannot be easily expressed in terms of the arguments?

e.g. This works:

   multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | u=x } =
     IF y=0 THEN
       x
     ELSE
       multiple_add_sub(x+1,y-1)-1
     ENDIF
   MEASURE y

but this does not:

   multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | y>0 => u>0 } =
     IF y=0 THEN
       x
     ELSE
       multiple_add_sub(x+1,y-1)-1
     ENDIF
   MEASURE y

In the above I was trying to just provide the type information and not
x=u. If I have to provide x=u, I wonder what I would do for a nasty
function whose value isn't easily expressed in terms of the arguments:

   complex(x:nat, y:nat): RECURSIVE { u: nat | u=??? } =
     IF y=0 THEN
       x
     ELSE
       complex( (x+1) * y * complex(x+2,y-1), y-1)-1
     ENDIF
   MEASURE y

Thanks,
David

_____________________________________________________________________
David Coppit                           david@coppit.org
The College of William and Mary        http://coppit.org/

"They have computers, and they may have other weapons of mass destruction."
Former Attorney General Janet Reno, speaking at LLNL of modern criminals