\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}{\node (#1) [label=#2:$+$, #3] {}; \path (#1.west) to (#1.east)} \newcommand{\context}{ \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}