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

Re: [PVS-Help] Mutual recursive functions

Sjaak Smetsers writes:
   F (. )(g) = . g(.).
   and to replace the application of F in G's body by
   G (.) = . F( .)(G) .

You need to put more information into the type, eg

   F(x)(g : [(below_measure_of(x)) -> ... ]) = ...

Similarly to what you have to do for double recursion, see
f91.pvs in the Examples directory in the pvs 2.4 distribution. To
say more I need to have the sources of your problem.

A different approach for mutual recursive function is to combine
domain and codomain with the union datatype:

FG : [union[domain(F),domain(G)] -> union[codomain(F),codomain(G)]] = 
  lambda xy : cases xy of
    inl(x) : F(x),
    inr(y) : G(y)