# 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/

```