Hi all,
"Choose x \in A : P" is a nice construct that allows to express ideas succinctly but
TLC evaluates it that way: it generates all the elements in A and then filter them using P.
If A is large, an exception is thrown.
A better way to evaluate the construct would be to generate an element of A, check that P is true,
if yes stop the algorithm in the other case continue. Obviously we can get too long a loop in that
case but in the better case we can have the opportunity to find the right element in a decent
time interval which cannot happen with the current algorithm. (Obviously if the loop is too
long we need a way to stop it.)
Generating one element at a time and then visiting it, is
the basic philosophy to evaluate combinatorial objects such as all trees or all permutations favored
by Knuth in TAOCP 4A.
--
FL