Pipe-calculus - Revision history

KalmanKeri: /* Normal forms */

2023-07-08T16:35:03Z

Normal forms

← Older revision		Revision as of 16:35, 8 July 2023
Line 348:		Line 348:
	\\		\\
	(s \alt t) \alt u \rew & s \alt (t \alt u) \\		(s \alt t) \alt u \rew & s \alt (t \alt u) \\
	a^+ . s \alt a^+ ~~\seq~~ t \rew & a^+ . (s \alt t) \\		a^+ . s \alt a^+ . t \rew & a^+ . (s \alt t) \\
	a^- . s \alt a^- ~~\seq~~ t \rew & a^- . (s \alt t) \\		a^- . s \alt a^- . t \rew & a^- . (s \alt t) \\
	\bot \alt s \rew & s \\		\bot \alt s \rew & s \\
	s \alt \bot \rew & s \\		s \alt \bot \rew & s \\
Line 356:		Line 356:
	\end{alignat}		\end{alignat}
	</math>		</math>

			('''Todo''': these rules don't implement idempotence of <math>\|</math> because commutativity is left out from the rules so equal terms don't always have a chance to "meet" on sides of <math>\|</math>.)

	While all other rules are syntax directed, rules for <math>\pipe</math> have to be attempted in the listed order for the following reasons.		While all other rules are syntax directed, rules for <math>\pipe</math> have to be attempted in the listed order for the following reasons.

KalmanKeri: /* Normal forms */

2023-07-08T16:26:37Z

Normal forms

← Older revision		Revision as of 16:26, 8 July 2023
Line 330:		Line 330:
	Normal form of pipe-calculus terms is defined by a term rewriting system<ref name="Fokkink"/>.		Normal form of pipe-calculus terms is defined by a term rewriting system<ref name="Fokkink"/>.
	Rewrite rules can be applied to any matching subterm of a term.		Rewrite rules can be applied to any matching subterm of a term.
	A term is in normal form if no rewrite rule applies to it.		A term is in normal form if no rewrite rule applies to any of its subterms.

	<math>		<math>

KalmanKeri: /* Normal forms */

2023-07-08T16:19:21Z

Normal forms

← Older revision		Revision as of 16:19, 8 July 2023
Line 328:		Line 328:
	=== Normal forms ===		=== Normal forms ===

	Normal form of pipe-calculus terms is defined by a term rewriting system<ref name="Fokkink"/>. A term is in normal form if no rewrite rule applies to it.		Normal form of pipe-calculus terms is defined by a term rewriting system<ref name="Fokkink"/>.
			Rewrite rules can be applied to any matching subterm of a term.
			A term is in normal form if no rewrite rule applies to it.

	<math>		<math>

KalmanKeri: /* Pipe-calculus as a process calculus */

2023-06-25T08:07:39Z

Pipe-calculus as a process calculus

← Older revision		Revision as of 08:07, 25 June 2023
Line 412:		Line 412:

	* The most outstanding difference is the lack of channels. Pipe-calculus processes only have a conceptual input and output, however one can simulate channels with synchronisation where atoms stand for channel names.		* The most outstanding difference is the lack of channels. Pipe-calculus processes only have a conceptual input and output, however one can simulate channels with synchronisation where atoms stand for channel names.
	* Communication primitives in mainstream process calculi often inseparably unite two conceptual steps: the selection of a communication channel and the act of message sending. For example [[wikipedia:pi-calculus\|Π-calculus]] <ref> Joachim Parrow: [https://courses.cs.vt.edu/~cs5204/fall05-kafura/Papers/PICalculus/parrow~2.pdf An Introduction to the π-Calculus], chapter to appear in Handbook of Process Algebra, ed. Bergstra, Ponse and Smolka,		* Communication primitives in mainstream process calculi often inseparably unite two conceptual steps: the selection of a communication channel and the act of message sending. For example [[wikipedia:pi-calculus\|π-calculus]] <ref> Joachim Parrow: [https://courses.cs.vt.edu/~cs5204/fall05-kafura/Papers/PICalculus/parrow~2.pdf An Introduction to the π-Calculus], chapter to appear in Handbook of Process Algebra, ed. Bergstra, Ponse and Smolka,
	Elsevier</ref> defines ''input prefixing'' <math>c\left(x\right).P</math> and ''output prefixing'' <math>\overline{c} \langle y \rangle.P</math> to denote receiving a name via channel <math>c</math> and sending a name via channel <math>c</math> respectively, before proceeding as <math>P</math>. Although one can introduce as convention ''synchronization'' where the communicated message is ignored, and ''broadcast'' where a group of processes are receiving messages on the same channel. In pipe-calculus these steps are separated by design.		Elsevier</ref> defines ''input prefixing'' <math>c\left(x\right).P</math> and ''output prefixing'' <math>\overline{c} \langle y \rangle.P</math> to denote receiving a name via channel <math>c</math> and sending a name via channel <math>c</math> respectively, before proceeding as <math>P</math>. Although one can introduce as convention ''synchronization'' where the communicated message is ignored, and ''broadcast'' where a group of processes are receiving messages on the same channel. In pipe-calculus these steps are separated by design.
	* In pipe-calculus there is no counterpart of ''name hiding'' that prevents interference between two groups of processes using the same channel name for communication. Since there is no general, bidirectional parallel composition, we don't need a hiding primitive. The pipe operation naturally restricts communication to a pipeline.		* In pipe-calculus there is no counterpart of ''name hiding'' that prevents interference between two groups of processes using the same channel name for communication. Since there is no general, bidirectional parallel composition, we don't need a hiding primitive. The pipe operation naturally restricts communication to a pipeline.

KalmanKeri at 08:07, 25 June 2023

2023-06-25T08:07:11Z

← Older revision		Revision as of 08:07, 25 June 2023
Line 2:		Line 2:
	One of its distinctive features is the inclusion of syntactic symbols, so it is easy to express program structure and complex data types using only the built-in constructs.		One of its distinctive features is the inclusion of syntactic symbols, so it is easy to express program structure and complex data types using only the built-in constructs.

	The name of the calculus refers to the ''pipe'' operator of Unix shells, and also alliterates with π-calculus, a popular process calculus, however they are not closely related.		The name of the calculus refers to the ''pipe'' operator of Unix shells, and also alliterates with [[wikipedia:pi-calculus\|π-calculus]], a popular process calculus, however they are not closely related.

	Pure pipe-calculus is untyped. Construction of a [[ideas_for_a_type_system\|type system]] is in the exploration phase, placing the focus on well-typed communication of programs.		Pure pipe-calculus is untyped. Construction of a [[ideas_for_a_type_system\|type system]] is in the exploration phase, placing the focus on well-typed communication of programs.

KalmanKeri at 08:02, 25 June 2023

2023-06-25T08:02:30Z

← Older revision		Revision as of 08:02, 25 June 2023
Line 2:		Line 2:
	One of its distinctive features is the inclusion of syntactic symbols, so it is easy to express program structure and complex data types using only the built-in constructs.		One of its distinctive features is the inclusion of syntactic symbols, so it is easy to express program structure and complex data types using only the built-in constructs.

	The calculus ~~was named after~~ the ''pipe'' operator of Unix shells, and also alliterates with π-calculus, a popular process calculus, however they are not ~~directly~~ related.		The name of the calculus refers to the ''pipe'' operator of Unix shells, and also alliterates with π-calculus, a popular process calculus, however they are not closely related.

	Pure pipe-calculus is untyped. Construction of a [[ideas_for_a_type_system\|type system]] is in the exploration phase, placing the focus on well-typed communication of programs.		Pure pipe-calculus is untyped. Construction of a [[ideas_for_a_type_system\|type system]] is in the exploration phase, placing the focus on well-typed communication of programs.

KalmanKeri: /* An example */

2023-06-24T21:28:14Z

An example

← Older revision		Revision as of 21:28, 24 June 2023
Line 26:		Line 26:
	* <code>match s</code> expects that the next symbol of the input stream is <code>s</code>. On failure the current branch of the program is aborted.		* <code>match s</code> expects that the next symbol of the input stream is <code>s</code>. On failure the current branch of the program is aborted.
	* <code>write s</code> appends the symbol <code>s</code> to the output stream.		* <code>write s</code> appends the symbol <code>s</code> to the output stream.
	* <code>run x</code> runs a ~~program~~ given its name.		* <code>run x</code> recursively runs a routine given its name.
	* <code>p ; q</code> runs <code>p</code> then runs <code>q</code> unless <code>p</code> fails.		* <code>p ; q</code> runs <code>p</code> then runs <code>q</code> unless <code>p</code> fails.
	* <code>p \| q</code> forks the execution of the program so that one branch runs <code>p</code>, another branch runs <code>q</code>, sharing the same input stream.		* <code>p \| q</code> forks the execution of the program so that one branch runs <code>p</code>, another branch runs <code>q</code>, sharing the same input stream.

KalmanKeri: /* An example */

2023-06-24T20:23:28Z

An example

← Older revision		Revision as of 20:23, 24 June 2023
Line 28:		Line 28:
	* <code>run x</code> runs a program given its name.		* <code>run x</code> runs a program given its name.
	* <code>p ; q</code> runs <code>p</code> then runs <code>q</code> unless <code>p</code> fails.		* <code>p ; q</code> runs <code>p</code> then runs <code>q</code> unless <code>p</code> fails.
	* <code>p \| q</code> forks the execution of the program so that one branch runs <code>p</code>, another branch runs <code>q</code>, sharing the same input ~~and output~~ stream.		* <code>p \| q</code> forks the execution of the program so that one branch runs <code>p</code>, another branch runs <code>q</code>, sharing the same input stream.

	Start by writing a routine that copies a natural number from the input to the output.		Start by writing a routine that copies a natural number from the input to the output.

KalmanKeri: /* Prefixes */

2023-06-24T20:16:40Z

Prefixes

← Older revision		Revision as of 20:16, 24 June 2023
Line 117:		Line 117:
	\|}		\|}

	~~In some applications it is useful to think of positive prefixes as data and negative prefixes as programs.~~		Prefixes are the basic units of interaction. Prefixes of the same kind and opposite polarity can interact.
	Prefixes are ~~also~~ the basic units of interaction. Prefixes of the same kind and opposite polarity can interact.		Intuitively, positive prefixes are outbound, while negative ones are inbound.
			It is also useful to think of positive prefixes as data and negative prefixes as programs.
	In the zeroth-order calculus only synchronisation is present.		In the zeroth-order calculus only synchronisation is present.

KalmanKeri: /* Terms */

2023-06-24T20:08:45Z

Terms

← Older revision		Revision as of 20:08, 24 June 2023
Line 89:		Line 89:
	** ''positive literal prefixing'' <math>a^+ \dot s</math> is a process that signals an atom <math>a</math> on its output before proceeding as <math>s</math>.		** ''positive literal prefixing'' <math>a^+ \dot s</math> is a process that signals an atom <math>a</math> on its output before proceeding as <math>s</math>.
	* ''communication'', where		* ''communication'', where
	** ''input prefixing'' <math>?x \dot s</math> is a process that receives a term ~~on its input~~. On success, it proceeds as <math>s</math> binding the name <math>x</math> to the received term.		** ''input prefixing'' <math>?x \dot s</math> is a process that receives a term. On success, it proceeds as <math>s</math> binding the name <math>x</math> to the received term.
	** ''output prefixing'' <math>!s \dot t</math> is a process that sends a term <math>s</math> ~~to its output~~ before proceeding as <math>t</math>.		** ''output prefixing'' <math>!s \dot t</math> is a process that sends a term <math>s</math> before proceeding as <math>t</math>.
	* ''sequence'' <math>s \seq t</math> is a composite process that executes <math>s</math> before proceeding as <math>t</math> unless <math>s</math> fails.		* ''sequence'' <math>s \seq t</math> is a composite process that executes <math>s</math> before proceeding as <math>t</math> unless <math>s</math> fails.
	* ''choice'' <math>s \alt t</math> is a forking process where one branch executes <math>s</math> while the other branch executes <math>t</math>. Failure of one branch does not affect the other branch.		* ''choice'' <math>s \alt t</math> is a forking process where one branch executes <math>s</math> while the other branch executes <math>t</math>. Failure of one branch does not affect the other branch.
	* ''pipeline'' <math>s \pipe t</math> is a composite process that enforces unidirectional, left to right data flow between its components.		* ''pipeline'' <math>s \pipe t</math> is a composite process that enforces unidirectional, left to right data flow between its components.
	* ''top'' <math>\top</math> is a process that successfully terminated.		* ''top'' <math>\top</math> is a process that is successfully terminated.
	* ''bottom'' <math>\bot</math> is also a terminated process. In certain contexts it denotes failure.		* ''bottom'' <math>\bot</math> is also a terminated process. In certain contexts it denotes failure.