Friday, December 11, 2009

converting recursive to iterative computations

A recursive definition of length of a list is..
fun {Length Xs}
case Xs of nil then 0
[] _|Xr then 1+{Length Xr}
In general, to convert a recursive computation into iterative one we'll have to formulate the problem as a sequence of state transformations. That is, we start with a state S0 and transform it successively, giving S1, S2, ... untill we reach the final state S-final, which contains the answer.

To calculate the list length, we can take state as pair of (i, Ys) where i is the length of the list already seen and Ys is the part of the list not seen yet. We can put this state into the function argument and can rewrite iterative definition of length calculation as follow..
fun {IterLength I Ys}
case Ys
of nil then I
[] _|Yr then {IterLength I+1 Yr}

In general, we can prove correctness of any iterative computation by finding a state invariant property. That is, a property which remains same across state transformations.
In case of the Length example, state invariant property is the sum of i + Length(Ys).. this will always be equal to length of the original list.

Ref: Section of CTM

No comments:

Post a Comment