Email Gateway (Aug 19 2022 at 14:26): Email Gateway (Aug 19 2022 at 14:26):From: Omar Montano Rivas <omarmrivas@gmail.com>
Hi,
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.
Thanks,
Omar.
Email Gateway (Aug 19 2022 at 14:26):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 14:26):From: Aleks Kissinger <aleks0@gmail.com>
Hi Omar,
Last year a student of mine implemented some parallel collection types
(including lazy sequences) on top of isaplib which is a small ML library
that is (mostly) source compatible with Isabelle/ML. You may find that code
useful:
https://github.com/iislucas/isaplib/tree/master/Concurrent
Best,
Aleks
Last updated: Nov 21 2024 at 12:39 UTC