283
edits
Syntax sugar (Pipe-calculus): Difference between revisions
→Arrow Syntax
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 50: | Line 50: | ||
</math> | </math> | ||
Informally, '''positive arrows''' denote outward directed operations while '''negative arrows''' denote inward directed ones. | |||
<ref> | <ref> | ||
The arrow syntax is unambiguous because variables can always be distinguished from atoms and an atom without polarity does not occur anywhere else in the syntax. | The arrow syntax is unambiguous because variables can always be distinguished from atoms and an atom without polarity does not occur anywhere else in the syntax. | ||
| Line 56: | Line 56: | ||
Both arrows are right associative. | Both arrows are right associative. | ||
When it is clear from context, we can call a negative arrow simply an arrow. | When it is clear from context, we can call a negative arrow simply an arrow. | ||
Using arrow syntax and recursion we can write <code>passNat</code> from the [[Pipe-calculus#An_example|introductory example]] like this. | |||
<math>\mathsf{rec}~ p . (\mathsf{1} \nto \mathsf{1} \pto p \mid \mathsf{end} \nto \mathsf{end} \pto \textbf{succeed})</math> | |||
== Notes == | == Notes == | ||
<references /> | <references /> | ||