User:Drdiem/ProPro

ProPro is a tool for checking productivity of recursive stream specifications. Productivity captures the intuitive notion of unlimited progress, of `working' programs producing values indefinitely, programs immune to livelock and deadlock. A recursive specification is called productive if not only can the specification be evaluated continually to build up an infinite normal form, but this infinite expression is also meaningful in the sense that it represents an infinite object from the intended domain.

For example consider the following specification:

 M = 0 : zip(inv(M), tail(M))
 zip(x : xs, ys) = x : zip(ys, xs) 
 inv(x : xs) = i(x) : inv(xs) 
 tail(x : xs) = xs 
 i(0) = 1 
 i(1) = 0

This specification is productive and defines the well-known Thue-Morse sequence; indeed the constant M rewrites to 0 : 1 : 1 : 0 : 1 : 0 : 0 : 1 : ... in the limit.

Another productive specification of this sequence is the following:

 M = 0 : 1 : f(tail(M)) 
 tail(x : xs) = x
 f (0 : xs) = 0 : 1 : f(xs)
 f (1 : xs) = 1 : 0 : f(xs)

This one is the result of translating the D0L system for the Thue-Morse sequence to a stream specification.