[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Choose and TLC

For the common case, in which there is a single element in the set satisfying the CHOOSE, this change would decrease the expected execution time of CHOOSE by a factor of two.  However, if you think about how TLC is probably written, it would require a separate version of the code to evaluate a set-valued _expression_ for use in CHOOSE.  Moreover, this is one of any number of optimizations that one can think of.  For example, evaluating the common _expression_ S = {} is probably now done by computing the value of  S  and comparing it to {}.  We need more than anecdotes to determine what optimizations are worth making.  In particular, changes to the costs of various parts of the computation have made _expression_ evaluation an ever smaller part of the execution time of a TLC execution.  I believe that the biggest gains per programming hour are now obtainable by optimizing parallel execution and maintenance of the fingerprint graph.


On Saturday, January 30, 2016 at 6:39:45 AM UTC-8, fl wrote:
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.