Syntax sugar (Pipe-calculus) - Revision history

KalmanKeri: /* Arrow Syntax */

2023-05-24T07:27:27Z

Arrow Syntax

← Older revision		Revision as of 07:27, 24 May 2023
Line 57:		Line 57:
	Using arrow syntax and recursion we can write <code>passNat</code> from the [[Pipe-calculus#An_example\|introductory example]] like this.		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>		<math>\mathsf{rec}~ p . (\mathsf{1} \nto \mathsf{1} \pto p \mid \mathsf{end} \nto \mathsf{end} \pto \top)</math>

	== Notes ==		== Notes ==

	<references />		<references />

KalmanKeri: /* Let ... in */

2023-05-24T07:24:17Z

Let ... in

← Older revision		Revision as of 07:24, 24 May 2023
Line 5:		Line 5:
	<math>		<math>
	\def\seq{\mathrel{;}}		\def\seq{\mathrel{;}}
	~~\def\succeed{\textbf{succeed}}~~
	\def\alt{\mid}		\def\alt{\mid}
	~~\def\fail{\textbf{fail}}~~
	\def\pipe{\rhd}		\def\pipe{\rhd}
	\def\pass{\textbf{pass}}		\def\pass{\textbf{pass}}
Line 22:		Line 20:

	<math>		<math>
	\mathsf{let}~x = s~\mathsf{in}~t \rew \out s . \~~fail~~ \pipe \in x . t		\mathsf{let}~x = s~\mathsf{in}~t \rew \out s . \bot \pipe \in x . t
	</math>		</math>

	~~According to~~ the defined [[Pipe-calculus#Normal_forms\|rewriting relation]], this can be rewritten as follows.		Using the defined [[Pipe-calculus#Normal_forms\|rewriting relation]], this can be rewritten as follows.

	<math>\out s . \~~fail~~ \pipe \in x . t \rew \~~fail~~ \pipe t[s/x] \rew t[s/x]</math>.		<math>\out s . \bot \pipe \in x . t \rew \bot \pipe t[s/x] \rew t[s/x]</math>.

	== Arrow Syntax ==		== Arrow Syntax ==

KalmanKeri: /* Arrow Syntax */

2023-05-23T07:14:26Z

Arrow Syntax

← Older revision		Revision as of 07:14, 23 May 2023
Line 50:		Line 50:
	</math>		</math>

	~~Intuitively~~ '''positive arrows''' denote outward directed operations while '''negative arrows''' denote inward directed ones.		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 />

KalmanKeri: /* Arrow Syntax */

2023-05-23T06:46:37Z

Arrow Syntax

← Older revision		Revision as of 06:46, 23 May 2023
Line 50:		Line 50:
	</math>		</math>

	Intuitively a '''positive ~~arrow~~''' ~~denotes~~ outward directed operations ~~and~~ '''negative ~~arrow~~''' ~~denotes~~ inward directed ones.		Intuitively '''positive arrows''' denote outward directed operations while '''negative arrows''' denote inward directed ones.
	<ref>		<ref>
	~~Notice that 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.
	</ref>		</ref>
	Both arrows are right associative.		Both arrows are right associative.

KalmanKeri at 06:43, 23 May 2023

2023-05-23T06:43:20Z

← Older revision		Revision as of 06:43, 23 May 2023
Line 1:		Line 1:
	Thoughtful application of syntax sugar makes programs easy to read, more compact and more familiar to programmers.		Thoughtful application of syntax sugar makes programs easy to read, more compact and more familiar to programmers. They can even reveal nice properties of the core calculus.
	~~The syntax extensions described here are lightweight and well-defined~~.

	== Let ... in ==		== Let ... in ==

KalmanKeri: /* Let ... in */

2023-05-10T07:11:28Z

Let ... in

← Older revision		Revision as of 07:11, 10 May 2023
Line 14:		Line 14:
	\def\out{!}		\def\out{!}
	\def\rew{\mathrel{\Rightarrow}\,}		\def\rew{\mathrel{\Rightarrow}\,}
	</math>		</math><math>\mathsf{let}</math> is a popular construct in functional languages that declares a lexically scoped local variable. It's usual form is <math>\mathsf{let}~x = s~\mathsf{in}~t</math> which denotes binding the name <math>x</math> to the term <math>s</math> in the term <math>t</math>.
	<math>\mathsf{let}</math> is a popular construct in functional languages that declares a lexically scoped local variable. It's usual form is <math>\mathsf{let}~x = s~\mathsf{in}~t</math> which denotes binding the name <math>x</math> to the term <math>s</math> in the term <math>t</math>.		In lambda calculus <math>\mathsf{let}</math> can be encoded as <math>(\lambda x . t)~s</math>. Using the ''<math>\beta</math>-rule'' we get <math>t[s/x]</math>, an instance of <math>t</math> where <math>s</math> is substituted for every free occurence of <math>x</math>.
	In lambda calculus <math>\mathsf{let}</math> can be encoded as <math>(\lambda x . t)~s</math>. ~~Applying~~ the ''<math>\beta</math>-rule'' we get <math>t[s/x]</math>, an instance of <math>t</math> where <math>s</math> is substituted for every free occurence of <math>x</math>.
	In pipe-calculus we can do similar encoding.		In pipe-calculus we can do similar encoding.

KalmanKeri: /* Arrow Syntax */

2023-05-09T22:38:22Z

Arrow Syntax

← Older revision		Revision as of 22:38, 9 May 2023
Line 54:		Line 54:
	Intuitively a '''positive arrow''' denotes outward directed operations and '''negative arrow''' denotes inward directed ones.		Intuitively a '''positive arrow''' denotes outward directed operations and '''negative arrow''' denotes inward directed ones.
	<ref>		<ref>
	Notice that the arrow syntax is unambiguous because variables can always be distinguished from atoms and an atom without a polarity does not occur anywhere else in the syntax.		Notice that 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.
	</ref>		</ref>
	Both arrows are right associative.		Both arrows are right associative.

KalmanKeri: /* Let ... in */

2023-05-09T22:34:48Z

Let ... in

← Older revision		Revision as of 22:34, 9 May 2023
Line 27:		Line 27:
	</math>		</math>

	According to the defined [[Pipe-calculus#Normal_forms\|rewriting relation]], this can be ~~brought to a normal form in two steps~~.		According to the defined [[Pipe-calculus#Normal_forms\|rewriting relation]], this can be rewritten as follows.

	<math>\out s . \fail \pipe \in x . t \rew \fail \pipe t[s/x] \rew t[s/x]</math>.		<math>\out s . \fail \pipe \in x . t \rew \fail \pipe t[s/x] \rew t[s/x]</math>.

KalmanKeri: /* Let ... in */

2023-05-09T22:33:28Z

Let ... in

← Older revision		Revision as of 22:33, 9 May 2023
Line 15:		Line 15:
	\def\rew{\mathrel{\Rightarrow}\,}		\def\rew{\mathrel{\Rightarrow}\,}
	</math>		</math>
	<math>\mathsf{let}</math> is a popular construct in functional languages that declares a lexically scoped local variable. It's usual form is <math>\mathsf{let}~x = t~\mathsf{in}~u</math> which denotes binding the name <math>x</math> to the term <math>t</math> in the term <math>u</math>.		<math>\mathsf{let}</math> is a popular construct in functional languages that declares a lexically scoped local variable. It's usual form is <math>\mathsf{let}~x = s~\mathsf{in}~t</math> which denotes binding the name <math>x</math> to the term <math>s</math> in the term <math>t</math>.
	In lambda calculus <math>\mathsf{let}</math> can be encoded as <math>(\lambda x . u)~t</math>. Applying the ''<math>\beta</math>-rule'' we get <math>u[t/x]</math>, an instance of <math>u</math> where <math>t</math> is substituted for every free occurence of <math>x</math>.		In lambda calculus <math>\mathsf{let}</math> can be encoded as <math>(\lambda x . t)~s</math>. Applying the ''<math>\beta</math>-rule'' we get <math>t[s/x]</math>, an instance of <math>t</math> where <math>s</math> is substituted for every free occurence of <math>x</math>.
	In pipe-calculus we can do similar encoding.		In pipe-calculus we can do similar encoding.

KalmanKeri at 22:30, 9 May 2023

2023-05-09T22:30:06Z

← Older revision		Revision as of 22:30, 9 May 2023
Line 1:		Line 1:
	Thoughtful application of syntax sugar makes programs easy to read, more compact and familiar to programmers.		Thoughtful application of syntax sugar makes programs easy to read, more compact and more familiar to programmers.
	The syntax extensions described here are lightweight and well-defined.		The syntax extensions described here are lightweight and well-defined.