[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Recursive Functions with negative domain



Daniel Kroening writes:
 > I'd like to define a function with its domain containing negative
 > numbers, such as:
 > 
 > 
 > testtheorem: THEORY
 > 
 >   BEGIN
 > 
 >     ABC(i:integer | i>=-1): RECURSIVE integer = 
 >       IF i=-1 THEN
 >         0
 >       ELSE
 >         ABC(i-1)
 >       ENDIF
 >       MEASURE i
 > 
 >   END testtheorem
 > 
 > (not really reasonable)
 > 
 > The problem is that PVS generates a TCC, which can't be proven:

Daniel,

The simplest solution to your problem is to coerce your measure into
the natural numbers. 

       ABC(i:integer | i>=-1): RECURSIVE integer = 
       IF i=-1 THEN
         0
       ELSE
         ABC(i-1)
       ENDIF
       MEASURE i+1

In this case, PVS easily discharges the generated TCC.

Alternatively, you may define a well founded measure on the type
upfrom(-1).

       ABC(i:upfrom(-1)): RECURSIVE integer = 
       IF i=-1 THEN
         0
       ELSE
         ABC(i-1)
       ENDIF
       MEASURE i by (lambda (i,j:upfrom(-1)): i < j)

Here, PVS generates a TCC asking you to prove that (lambda
(i,j:upfrom(-1)): i < j) is well founded.  This can be proven with a
little effort using the axiom wf_nat from the prelude.  (The proof is
left as an exercise).

Regards,

-- 
-- Paul S. Miner                | phone: (757) 864-6201
-- 1 South Wright St. / MS 130  | fax:   (757) 864-4234
-- NASA Langley Research Center | mailto:p.s.miner@larc.nasa.gov
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/