Skip to content

Instantly share code, notes, and snippets.

Created Dec 30, 2011
What would you like to do?
Extensional Optimal Reduction
\tikzset{close/.style={node distance=0pt},
every to/.style={rounded corners, draw},
every edge/.style={draw}}
\title{Extensional Optimal Reduction}
\author{Anton Salikhmetov}
\newcommand{\fan}[3]{\node (#1) [label=#2:$+$, #3] {};
\path (#1.west) to (#1.east)}
\node (#1) [outer sep=0pt, inner sep=0pt, #2] {#3};
\node (#1 in) [close, above=of #1] {};
\node (#1 out) [close, below=of #1] {}}
\section{Encoding $\lambda$-expressions}
\node (root) {};
\context{lambda}{below=of root}{$G(\lambda x.C[x])$};
\foreach \side in {west, east}
\path (root.\side) to (lambda in.\side);
\node (root) {};
\fan{lambda}{above left}{below=of root};
\context{c}{below left=of lambda}{$G(C[x])$;};
\node (bottom) [below right=of c] {};
\node (right) [right=of c] {};
\foreach \side in {west, east}
\path (lambda.\side) edge (root.\side) edge (c in.\side)
to (right.\side) to (bottom.\side) to (c out.\side);
\end{tikzpicture} \tag{$\lambda$} \\
\node (root) {};
\context{apply}{below=of root}{$G(C_1[x]\ C_2[x])$};
\node (bottom) [below=of apply] {};
\foreach \side in {west, east}
\path (root.\side) to (apply in.\side)
(bottom.\side) to (apply out.\side);
\context{c2}{right=of c1}{$G(C_2[x])$.};
\fan{apply}{below right}{above=of c1};
\node (root) [above=of apply] {};
\node (right) [above=of c2] {};
\node (top) [above=of right] {};
\node (left) [below=of c1] {};
\node (below) [below=of c2] {};
\fan{share}{below left}{below=of below};
\node (bottom) [below=of share] {};
\foreach \side in {west, east}
\path (apply.\side) edge (root.\side) edge (c1 in.\side)
to (top.\side) to (c2 in.\side)
(share.\side) edge (c2 out.\side) edge (bottom.\side)
to (left.\side) to (c1 out.\side);
\end{tikzpicture} \tag{$@$}
\section{Graph rewriting rules}
\section{Example: $\Omega$}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment