From c932c70a68672346cc1bb9472596aa41508f2362 Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Fri, 1 Apr 2016 09:51:56 -0400
Subject: [PATCH] quick writeup of unification judgementally

---
 unification.tex | 112 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 112 insertions(+)
 create mode 100644 unification.tex

diff --git a/unification.tex b/unification.tex
new file mode 100644
index 0000000..af36103
--- /dev/null
+++ b/unification.tex
@@ -0,0 +1,112 @@
+
+\documentclass{amsart}
+\usepackage{amssymb,amsmath,latexsym,stmaryrd,mathtools}
+\usepackage{cleveref}
+\usepackage{mathpartir}
+\let\types\vdash % turnstile
+\def\cb{\mid} % context break
+\def\op{^{\mathrm{op}}}
+\def\p{^+} % variances on variables
+\def\m{^-}
+\let\mypm\pm
+\let\mymp\mp
+\def\pm{^\mypm}
+\def\mp{^\mymp}
+\def\jdeq{\equiv}
+\def\cat{\;\mathsf{cat}}
+\def\type{\;\mathsf{type}}
+\def\ctx{\;\mathsf{ctx}}
+\let\splits\rightrightarrows
+\def\flip#1{#1^*} % reverse the variances of all variables
+\def\mor#1{\hom_{#1}}
+\def\id{\mathrm{id}}
+\def\ec{\cdot} % empty context
+\def\psplit{\overset{\mathsf{pair}}{\splits}}
+\def\iso{\cong}
+\def\tpair#1#2{#1\otimes #2}
+\def\cpair#1#2{\langle #1,#2\rangle}
+\def\tlet#1,#2:=#3in{\mathsf{let}\; \tpair{#1}{#2} \coloneqq #3 \;\mathsf{in}\;}
+\def\clet#1,#2:=#3in{\mathsf{let}\; \cpair{#1}{#2} \coloneqq #3 \;\mathsf{in}\;}
+\def\mix#1,#2 with #3 in{\mathsf{mix} {\scriptsize \begin{array}{c} \check{#1} \coloneqq \check{#3} \\ \hat{#2} \coloneqq \hat{#3} \end{array}  }\mathsf{in}\;}
+\newcommand{\coend}{\begingroup\textstyle\int\endgroup}
+\newcommand{\Set}{\mathrm{Set}}
+\def\yielding{\mid}
+\def\unif{\doteq}
+
+\begin{document}
+
+This is for a cartesian language.  I'm not sure how quadraticality plays
+into the unification algorithm.
+
+First-order terms consist of variables and constants applied to lists of
+terms.  A list of terms is either empty ($\cdot$) or a cons.  
+
+\begin{mathpar}
+\inferrule{x \in \Gamma}
+          {\Gamma \types x}
+
+\inferrule{\Gamma \types \vec{M}}
+          {\Gamma \types F(\vec{M})}
+
+\inferrule{ }
+          {\Gamma \types \cdot}
+
+\inferrule{\Gamma \types M \\ \Gamma \types \vec{M}}
+          {\Gamma \types M,\vec{M}}
+\end{mathpar}
+
+A context is $\cdot$ or $\Gamma,x$.  A substitution is 
+\begin{mathpar}
+\inferrule{ }
+          {\Gamma \vdash \cdot : \cdot}
+
+\inferrule{\Gamma \types \theta : \Gamma' \\ 
+            \Gamma \types M }
+          {\Gamma \types \theta,M/x : \Gamma',x}
+\end{mathpar}
+
+Identity and composition are admissible:
+\begin{mathpar}
+\inferrule{ }
+          {\Gamma \vdash 1_\Gamma : \Gamma}
+
+\inferrule{\Gamma \types \theta : \Gamma' \\ 
+            \Gamma' \types \theta'' : \Gamma'' }
+          {\Gamma \types \theta'' [ \theta' ] : \Gamma''}
+\end{mathpar}
+
+
+The unification judgements have the form 
+\begin{itemize}
+\item $M \unif N \yielding \theta$ where $\Gamma \types M$ and $\Gamma
+  \types N$ and $\Gamma' \types \theta : \Gamma$.  Operationally, we
+  think of $M$ and $N$ and $\Gamma$ as inputs and $\Gamma'$ and $\theta$
+  as outputs, so unification produces a new context and a substitution
+  for the original variables from it.  
+
+\item $\vec{M} \unif \vec{N} \yielding \theta$ where $\Gamma \types
+  \vec{M}$ and $\Gamma \types \vec{N}$ and $\Gamma' \types \theta :
+  \Gamma$.  
+\end{itemize}
+
+Here are the rules (I put in some type annotations that might be helpful):
+\begin{mathpar}
+
+\inferrule{ }
+           {\cdot \unif \cdot \yielding 1_\Gamma}
+
+\inferrule{ M \unif N \yielding (\Gamma' \types \theta : \Gamma) \\
+             \vec{M}[\theta] \unif \vec{N}[\theta] \yielding (\Gamma'' \types \theta' : \Gamma') \\
+           }
+           {M,\vec{M} \unif N,\vec{N} \yielding \theta[\theta']}
+
+\inferrule{\Gamma \vdash M}
+          {x \unif M \yielding (\Gamma \vdash (1_\Gamma,M/x) : \Gamma,x)}
+
+
+\inferrule{\vec{M} \unif \vec{N} \yielding \theta}
+          {F(\vec{M}) \unif F(\vec{N}) \yielding \theta}
+\end{mathpar}
+
+
+\end{document}