Re: [isabelle] Parallel sequences



On Mon, 12 May 2014, Omar Montano Rivas wrote:

I am currently working with sequences in Isabelle/ML (src/Pure/General/seq.ML) and I was wondering if there is any support for parallel execution of functions such as exists or forall for sequences, e.g. ('a -> bool) -> 'a seq -> bool. I can see there is a library for parallel lists (src/Pure/Concurrent/par_list.ML) but can not find something similar for sequences.

The sequences of structure Seq are unbounded and lazy, and usually explored only to a certain point and then abandonned.

It is not immediately obvious what should happen in parallel here, i.e. you need to determine more clearly what you need, and then it is probably feasible to imitate the Par_List implementation.

The regular sequences are at the bottom of tactics and tacticals in Isabelle. In http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/goal.ML#l339 there are a few parallel combinators for that, but I avoided the above questions by restricting to result sequence to zero or one result (via DETERM / SINGLE).


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.