Extensional Optimal Reduction

optimal.tex

\documentclass[12pt,a4paper]{article}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{tikz}

\usetikzlibrary{arrows,positioning}
\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)}
\newcommand{\context}[3]{
\node (#1) [outer sep=0pt, inner sep=0pt, #2] {#3};
\node (#1 in) [close, above=of #1] {};
\node (#1 out) [close, below=of #1] {}}

\begin{document}

\maketitle

\section{Encoding $\lambda$-expressions}

\begin{align*}
\begin{tikzpicture}[baseline=(lambda.base)]
\node (root) {};
\context{lambda}{below=of root}{$G(\lambda x.C[x])$};
\foreach \side in {west, east}
\path (root.\side) to (lambda in.\side);
\end{tikzpicture}
&\equiv
\begin{tikzpicture}[baseline=(c.base)]
\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$} \\
\begin{tikzpicture}[baseline=(apply.base)]
\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);
\end{tikzpicture}
&\equiv
\begin{tikzpicture}[baseline=(c1.base)]
\context{c1}{}{$G(C_1[x])$};
\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{$@$}
\end{align*}

\section{Graph rewriting rules}

\section{Example: $\Omega$}

\end{document}