Recursively Defined Functions

Take the following function:

CONSTANTS parity
PROPERTIES
 parity : (NATURAL --> {0,1}) & 
 parity(0) = 0 & 
 !x.(x:NATURAL => parity(x+1) = 1 - parity(x))

Here, ProB will complain that it cannot find a solution for parity. The reason is that parity is a function over an infinite domain, but ProB has to represent the function as a finite set of maplets.

There are basically three solutions to this problem:

• Write a finite function:

parity : (NAT --> {0,1}) & 
parity(0) = 0 & 
!x.(x:NAT & x<MAXINT => parity(x+1) = 1 - parity(x))

• Rewrite your function so that in the forall you do not refer to values

of parity greater than x:
parity : (NATURAL --> {0,1}) & 
parity(0) = 0 & 
!x.(x:NATURAL1 => parity(x) = 1 - parity(x-1))

• Use symbolic animation (turn on Lazy expansion of lambdas & set comprehensions and lazy expansion of Recursive set comprehensions and lambdas in the Animation Preferences). You then need to rewrite your function using set comprehension or lambdas. Also, you are only allowed to apply the function, you cannot use any other set/function operation (otherwise the function will be expanded).

Note: this only works in version 1.2.7 of ProB; this feature has not yet been enabled in 1.3.0.