Re: [PVS-Help] recursive functions calling each other

[Cesar Munoz <munoz@xxxxxxxxxx>]

PVS doesn't directly support mutually recursive functions. However,
there is a way to encode mutual recursion using ordinary recursion. The
following simple example illustrates how to do that for a mutual
recursive definition of even and odd:

evenf(oddf:[nat->bool])(x:nat): bool =
  if x=0 then true
  else oddf(x-1)
  endif

odd(x:nat) : RECURSIVE bool =
  if x=0 then false
  elsif x=1 then true
  else evenf(odd)(x-1)
  endif
  MEASURE x

even : [nat->bool] = evenf(odd)

Cesar

Lucian M. Patcas wrote:
> Hi there,
> 
> I have two recursive functions that call each other:
> 
> a(x: nat): RECURSIVE bool =
> ...
> b(x)
> ...
> MEASURE x
> 
> b(y: nat): RECURSIVE bool =
> ...
> a(y)
> ...
> MEASURE y
> 
> I don't know how to do this without getting resolution errors.
> 
> Thanks for your help,
> Lucian
> 

-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@xxxxxxxxxx
National Institute of Aerospace         mailto:Cesar.A.Munoz@xxxxxxxx
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4