283
edits
Pipe-calculus: Difference between revisions
→Choice
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) (→Choice) |
||
| Line 135: | Line 135: | ||
=== Choice === | === Choice === | ||
Choice is a forking process. <math>s \mid t</math> has two branches that exist side by side. | |||
Both <math>s</math> and <math>t</math> are ready for interaction, however they can't communicate with each other. Both branches participate in the same interaction but they evolve independently. | |||
This is different from systems where alternatives are exclusive or they are examined one by one. We can say that choice is ''laid out in space''<ref>This suggestive phrasing is borrowed from Lennart Augustsson et al.: [https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf The Verse Calculus: a Core Calculus for Functional Logic Programming].</ref>. | |||
==== Rules ==== | |||
If one of the branches fail, the other remains active. | |||
<math>s \mid \bot = s</math> | |||
* laid out in space | |||
* fork - join | * fork - join | ||
* failure is local to forks | * failure is local to forks | ||
* forks may overlap | * forks may overlap | ||
* but identical forks cannot be distinguished | * but identical forks cannot be distinguished | ||
* choice and mathematical case | * choice and mathematical case analysis | ||
==== Analogies ==== | |||
Practical concepts that share some properties with choice are: | |||
* The Unix [[Wikipedia:Fork_(system_call)|fork system call]] - as both forks inherit the same environment and the failure of one fork does not affect the other one. | |||
* Branches in a version control system - branches are often created to explore solutions and successful solutions are merged with the main branch. | |||
In both analogies, branches may exist side by side. However branches of a choice combinator are all equal, there is no main branch between them. | |||
==== Exclusive choice ==== | ==== Exclusive choice ==== | ||