fun {Length Xs}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.

case Xs of nil then 0

[] _|Xr then 1+{Length Xr}

end

end

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}

end

end

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 3.4.2.4 of CTM

## No comments:

## Post a Comment