Skip to content

Instantly share code, notes, and snippets.

@codedot
Created Dec 30, 2011
Embed
What would you like to do?
Extensional Optimal Reduction
\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}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment