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

Re: [tlaplus] Choose and TLC

On 30.01.2016 15:39, fl wrote:
> "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.

Hi Frederic,

I added your idea to the Codeplex issue tracker [1] to look into it
later. I personally don't have the necessary bandwidth in the
foreseeable future though.


[1] https://tlaplus.codeplex.com/workitem/24