Recursively Defined Functions: Difference between revisions

No edit summary
No edit summary
Line 21: Line 21:
  parity(0) = 0 &  
  parity(0) = 0 &  
  !x.(x:NATURAL1 => parity(x) = 1 - parity(x-1))
  !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).
* Write your function constructively using a single recursive equation using set comprehensions, lambda abstractions, finite sets and set union. This requires ProB 1.3.5-beta7 or higher and you need to declare <tt>parity</tt> as <tt>ABSTRACT_CONSTANT</tt>. Here is a possible equation:
 
parity : INTEGER <-> INTEGER &
Note: this only works in version 1.2.7 of ProB; this feature is currently being re-developed for ProB 1.3.5.
parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1))
 
* Another solution is try and write your function constructively and non-recursively, ideally using a lambda abstraction:
* Another solution is try and write your function constructively and non-recursively, ideally using a lambda abstraction:
   parity : (NATURAL --> {0,1}) &  
   parity : (NATURAL --> {0,1}) &  

Revision as of 06:35, 17 March 2012

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))
  • Write your function constructively using a single recursive equation using set comprehensions, lambda abstractions, finite sets and set union. This requires ProB 1.3.5-beta7 or higher and you need to declare parity as ABSTRACT_CONSTANT. Here is a possible equation:
parity : INTEGER <-> INTEGER & 
parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1))
  • Another solution is try and write your function constructively and non-recursively, ideally using a lambda abstraction:
  parity : (NATURAL --> {0,1}) & 
  parity = %x.(x:NATURAL|x mod 2)
  • Here ProB detects that parity is an infinite function and will keep it symbolic (if possible). With such an infinite function you can:
    • apply the function, e.g., parity(10001) is the value 1
    • compute the image of the function, e.g., parity[10..20] is {0,1}
    • compose the function with a finite relation, e.g., (id(1..10) ; parity) gives the value [1,0,1,0,1,0,1,0,1,0]
    • sometimes compute the domain of the function, here, dom(parity) is determined to be NATURAL. But this only works for simple infinite functions represented.
    • sometimes check that you have a total function, e.g., parity: NATURAL --> INTEGER can be checked by ProB. However, if you change the range (say from INTEGER to 0..1), then ProB will try to expand the function.

You can experiment with those by using the Eval console of ProB, experimenting for example with the following complete machine. Note, you should use ProB 1.3.5-beta2 or higher.

MACHINE InfiniteParityFunction
CONSTANTS parity
PROPERTIES
  parity : NATURAL --> INTEGER & 
  parity = %x.(x:NATURAL|x mod 2)
VARIABLES c
INVARIANT
c: NATURAL
INITIALISATION c:=0
OPERATIONS
 Inc = BEGIN c:=c+1 END;
 r <-- Parity = BEGIN r:= parity(c) END;
 r <-- ParityImage = BEGIN r:= parity[0..c] END;
 r <-- ParityHistory = BEGIN r:= (%i.(i:1..c+1|i-1) ; parity) END
END

You may also want to look at the tutorial page on modeling infinite datatypes.