Re: [tlaplus] Choose and TLC

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

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.

Thanks
Markus

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