# Difference between revisions of "Concurrency with oracles"

(References finally added) |
m (Formatting changes; added section regarding concurrency) |
||

Line 1: | Line 1: | ||

+ | == Oracles, defined == |
||

+ | |||

An ''oracle'' is a value that "knows", by magic predictive power, which of two computations will finish first or which input event will arrive first, or whether a computation will finish before an input event arrives. In practice the predictive power is unnecessary, but the oracle, by seeming to contain the prediction, will preserve the [[Referential transparency|referential transparency]] of a language while allowing expression of computations whose outcomes depend on execution time and arrival time. |
An ''oracle'' is a value that "knows", by magic predictive power, which of two computations will finish first or which input event will arrive first, or whether a computation will finish before an input event arrives. In practice the predictive power is unnecessary, but the oracle, by seeming to contain the prediction, will preserve the [[Referential transparency|referential transparency]] of a language while allowing expression of computations whose outcomes depend on execution time and arrival time. |
||

Solutions tend to involve infinite trees of oracles, so you can pull one out whenever you need one, and pass an infinite subtree to future computations. Of course once an oracle has been used, it can't be reused. [[Referential transparency]] demands that the outcome of applying the oracle is fixed. |
Solutions tend to involve infinite trees of oracles, so you can pull one out whenever you need one, and pass an infinite subtree to future computations. Of course once an oracle has been used, it can't be reused. [[Referential transparency]] demands that the outcome of applying the oracle is fixed. |
||

⚫ | |||

+ | == Connections to concurrency == |
||

+ | |||

+ | On page 32 of 60 in ''Tackling the Awkward Squad'', Simon Peyton Jones introduces non-determinism as a result of adding concurrency to the ''operational semantics'' he provides for I/O. As shown by |
||

+ | Peter Dybjer, Herbert Sander and Mieke Massink, the throughtful use of oracles can help to recover |
||

+ | referential transparency in models of concurrency despite them being non-deterministic. |
||

+ | |||

⚫ | |||

* [http://www.cse.chalmers.se/~peterd/papers/FACS1989.pdf A Functional Programming Approach to the Specification and Verification of Concurrent Systems], Peter Dybjer and Herbert Sander. |
* [http://www.cse.chalmers.se/~peterd/papers/FACS1989.pdf A Functional Programming Approach to the Specification and Verification of Concurrent Systems], Peter Dybjer and Herbert Sander. |
||

Line 12: | Line 20: | ||

[[Category:Concurrency]] |
[[Category:Concurrency]] |
||

+ | [[Category:Nondeterminism]] |

## Revision as of 05:33, 18 March 2021

## Oracles, defined

An *oracle* is a value that "knows", by magic predictive power, which of two computations will finish first or which input event will arrive first, or whether a computation will finish before an input event arrives. In practice the predictive power is unnecessary, but the oracle, by seeming to contain the prediction, will preserve the referential transparency of a language while allowing expression of computations whose outcomes depend on execution time and arrival time.

Solutions tend to involve infinite trees of oracles, so you can pull one out whenever you need one, and pass an infinite subtree to future computations. Of course once an oracle has been used, it can't be reused. Referential transparency demands that the outcome of applying the oracle is fixed.

## Connections to concurrency

On page 32 of 60 in *Tackling the Awkward Squad*, Simon Peyton Jones introduces non-determinism as a result of adding concurrency to the *operational semantics* he provides for I/O. As shown by
Peter Dybjer, Herbert Sander and Mieke Massink, the throughtful use of oracles can help to recover
referential transparency in models of concurrency despite them being non-deterministic.

## References

- A Functional Programming Approach to the Specification and Verification of Concurrent Systems, Peter Dybjer and Herbert Sander.

- Functional Techniques in Concurrency, Mieke Massink.