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

[PVS-Help] Mutual recursive functions



Hi,

 

Although PVS does not support mutual recursive function, I thought that maybe the following trick would work:

 

Suppose I want to define a two (mutual recursive) functions

 

F (…) =

            … G(…)…

 

G (…) =

            … F( …) …

 

The idea is to lift G in the body of F as follows

 

F (… )(g) =

            … g(…)…

 

and to replace the application of F in G’s body by

 

G (…) =

            … F( …)(G) …

 

Unfortunately, this produces an unprovable termination TCC. How can I fix this? If necessary, I can send you the complete program.

 

 

Regards,

 

Sjaak Smetsers