documentation.tex

\documentclass[11pt]{article}

\marginparwidth0.5in 
\oddsidemargin0.25in 
\evensidemargin0.25in 
\marginparsep0.25in
\topmargin 0.25in 
\textwidth 6in \textheight 8 in

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{upgreek}
\usepackage{enumerate}
\usepackage{verbatim}
\usepackage{stmaryrd}
\usepackage{listings}

\newcommand*{\br}[1]{\llbracket{#1}\rrbracket}


\begin{document}
\title{Linear Lambda Calculus Compiler Documentation}
\author{CS 4999: Anna Yesypenko Supervised by Professor Nate Foster}
\maketitle

\section*{Overview:}

We compile the source language, linear lambda calculus programs $e$
\begin{align*}
    b\ &::=\ +\ |\ -\ |\ /\ |\ *\\
    e\ &::=\ n\ |\ x\ |\ e_1\ b\ e_2\ |\ \text{let}\ x\ =\ e_1\ \text{in}\ e_2\\
    &|\ \lambda\ x.\ e\ |\ e_1\ e_2
\end{align*}
to the target language, stack machine programs $\rho$
\begin{align*}
    binop\ &::=\ \text{Add $|$ Subt $|$ Mult $|$ Div}\\
    funop\ &::= \text{Save\_Function ($fun\_id, k$) $|$ Form\_Closure ($fun\_id$) $|$ Apply}\\
    rollop\ &::= \text{Roll $k$ $|$ Unroll $k$}\\
    tupleop\ &::= \text{Construct\_Tuple $k$ $|$ Deconstruct\_Tuple $k$}\\
    instr\ &::=\ binop\ |\ funop\ |\ rollop\ |\ tupleop\ |\ \text{Push $n$}\\
    \rho &::=\ instr\ \text{list}
\end{align*}
which operate on stacks $\sigma$ and $\sigma_f$
\begin{align*}
    \sigma_f\ &::=\ (fun\_id, \rho)\ \text{list}\\
    tup\ &::=\ \text{Tuple $(v_1, \dots, v_k)$}\\
    v\ &::=\ \text {Int $n\ |\ tup\ |$ Closure ($\rho, tup$)}\\
    \sigma &::=\ v\ \text{list}
\end{align*}

\break{}

\section*{Defunctionalization:}

Given a lambda-calculus program $p$, defunctionalization produces a first-order language. That is, functions are no longer considered to be values. Instead, $l\ ::=\ (\lambda x.\ e)$ is represented as $C_l(v_1, \dots, v_n)$, where $C_l$ uniquely identifies the function $l$, and $v_1, \dots, v_n$ are the values of the variables $x_1, \dots, x_n$ which are free in $l$.

We define the translation from lambda-calculus program to first-order program.
\begin{align*}
        \br{x} &= x\\
            \br{\lambda x.\ e} &= C_{\lambda x.\ e} (x_1, \dots, x_n),\ \text{where $x_1, \dots, x_n$ are free in $\lambda x.\ e$}\\
                \br{e_1\ b\ e_2} &= \br{e_1}\ b\ \br{e_2}\\
                    \br{\text{let}\ x = e_1\ \text{in}\ e_2} &= \br{(\lambda x.\ e_2)\ e_1}\\
                        \br{e_1\ e_2} &= \text{apply}(\br{e_1}, \br{e_2})
\end{align*}

Thus a lambda calculus program $p$ is translated to a first-order program as such:
\begin{lstlisting}[mathescape = true]
let rec apply_defunc (f, arg) = 
    match f with
        | C$_{\lambda x.\ e} (x_1, \dots, x_n)$ -> let $x = \arg$ in $\br{e}$
        | $\dots$ in
        $\br{p}$
\end{lstlisting}

\section*{Analogue to Defunctionalization:}

The values Closure ($fun\_id$, Tuple $(v_1, \dots, v_k)$) on stack $\sigma$ are analogous to the constructors $C_{fun\_id} (v_1, \dots, v_k)$.\\

The function stack $\sigma_f$ stores the programs $\hat{\rho}$ corresponding to each case of the dispatch function `apply\_defunc'. At the beginning of a program $\rho$, there will be a series of Save\_Function instructions to initialize $\sigma_f$.

\break{}

\section*{Executing and Reversing a Program:}

The rules we present below show the reversibility for each instruction using the following tuple: $$(\rho, \sigma, \sigma_f, \sigma_h \in \text{int list}, \rho_h).$$

\textbf{Binomial arithmetic operations:}
\begin{gather*}
    (\text{(Add $|$ Subt $|$ Mult $|$ Div as $b$)}::\rho, \text{Int $n_1$}::\text{Int $n_2$}::\sigma, \sigma_f, \sigma_h, b::\rho_h)\\
    \Longleftrightarrow (\rho, n_1 \star n_2::\sigma, \sigma_f, n_1::\sigma_h, b::\rho_h)
\end{gather*}

\textbf{Function operations:}
\begin{gather*}
    (\text{Save\_Function ($fun\_id, k$) as $sf$}::\hat{\rho}\ @\ \rho, \sigma, \sigma_f, \sigma_h, \rho_h), \text{where $|\hat{\rho}| = k$}\\
    \Longleftrightarrow (\rho, \sigma, (fun\_id, \hat{\rho})::\sigma_f, \sigma_h, sf::\rho_h)\\ \\
    (\text{Form\_Closure ($fun\_id$) as $fc$}::\rho, \text{Tuple $(v_1, \dots, v_k)$ as $tup$}::\sigma, \sigma_f, \sigma_h, \rho_h)\\ \text{where List.assoc $fun\_id\ \sigma_f = \hat{\rho}$}\\
    \Longleftrightarrow (\rho, \text{Closure ($\hat{\rho}, tup$)}::\sigma, \sigma_f, \sigma_h, fc::\rho_h)\\ \\ 
    (\text{Apply}::\rho, \text{Closure ($\hat{\rho}$, Tuple $(v_1, \dots, v_k)$ as $tup$)}::\arg::\sigma, \sigma_f, \sigma_h, \rho_h),\\     
    \Longleftrightarrow (\hat{\rho}\ @\ \rho, tup::\arg::\sigma, \sigma_f, |\hat{\rho}|::\sigma_h, fc::\rho_h)
\end{gather*}


\textbf{Roll, Tuple, and Integer Pushing operations:}
\begin{gather*}
    (\text{Roll $k$}::\rho, v_1::v_2::\dots::v_k::\sigma, \sigma_f, \sigma_h, \rho_h)\\
    \Longleftrightarrow (\rho, v_k::v_1::\dots::v_{k-1}::\sigma, \sigma_f, \sigma_h, \text{Roll $k$}::\rho_h)\\ \\
    (\text{Unroll $k$}::\rho, v_1::v_2::\dots::v_k::\sigma, \sigma_f, \sigma_h, \rho_h)\\
    \Longleftrightarrow (\rho, v_2::\dots::v_k::v_1::\sigma, \sigma_f, \sigma_h, \text{Unroll $k$}::\rho_h)\\ \\
    (\text{Compose\_Tuple $k$}::\rho, v_1:: \dots:: v_k::\sigma, \sigma_f, \sigma_h, \rho_h)\\
    \Longleftrightarrow (\rho, \text{Tuple}(v_1, \dots, v_k)::\sigma, \sigma_f, \sigma_h, \text{Compose\_Tuple $k$}::\rho_h)\\ \\
    (\text{Decompose\_Tuple $k$}::\rho, \text{Tuple}(v_1, \dots, v_k)::\sigma, \sigma_f, \sigma_h, \rho_h)\\
    \Longleftrightarrow (\rho, v_1::\dots::v_k::\sigma, \sigma_f, \sigma_h, \text{Decompose\_Tuple $k$}::\rho_h)\\ \\
    (\text{Push $n$}::\rho, \sigma, \sigma_f, \sigma_h, \rho_h)\\
    \Longleftrightarrow (\rho, \text{Int $n$}::\sigma, \sigma_f, \sigma_h, \text{Push $n$}::\rho_h)
\end{gather*}

\section*{Reversability of Apply:}

Define $\vec{\rho} = (\hat{\rho}, \rho)$ and $\vec{\sigma} = (\text{Tuple}(v_1, \dots, v_n), \arg, \sigma)$.
\begin{align*}
    \textbf{Well-Formed Closure Property}: \\
    \text{wf} (\vec{\rho}, \vec{\sigma})\ &\triangleq\ (\text{Apply::$\rho$, Closure ($\hat{\rho}$, Tuple $(v_1, \dots, v_k)$ as $tup$)::$\arg::\sigma, \dots$})\\
    &\Longrightarrow (\hat{\rho}\ @\ \rho, tup::\arg::\sigma, \dots) \Longrightarrow^* (\rho, result::\sigma, \dots)
\end{align*}

All the operations change the size of the stack $\sigma$. We define the function $\delta$ which gives the change in the size of $\sigma$ after executing an instruction.
\begin{align*}
    \delta(\text{Add $|$ Subt $|$ Mult $|$ Div})\ &=\ -1\\
    \delta(\text {Save\_Function \_})\ &=\ +0\\
    \delta(\text {Form\_Closure \_})\ &=\ +0\\
    \delta(\text {Apply})\ &=\ -1\\
    \delta(\text{Roll \_ $|$ Unroll \_})\ &=\ +0\\
    \delta(\text {Compose\_Tuple $k$})\ &=\ -k + 1\\
    \delta(\text {Decompose\_Tuple $k$})\ &=\ +k - 1\\
    \delta(\text {Push \_})\ &=\ +1\\
\end{align*}

Let us define the following property.
\begin{align*}
        \textbf{Grow-Shrink Property}:\\ 
        \text{gs ($\rho$ where $|\rho| > 0$)}\ \triangleq\ \exists \rho_g,\ \rho_s.\ \rho = \rho_g\ @\ \rho_s
\end{align*}

Recall that to reverse Apply, we must split the program such that we restore the instructions in the original closure. Currently, we must store the length of the instructions in the closure body to reverse Apply. We define this split as follows.
\begin{align*}
    \text{splits}\ (\vec{\rho},\vec{\sigma})\ \triangleq\ \rho' = \hat{\rho}\ @\ \rho\ \wedge : \ \texttt{wf}\ (\vec{\rho}, \vec{\sigma})
\end{align*}
If the following proposition holds, then Apply would be injective.
\begin{align*}
    \text{InjApply}: \quad \forall \rho', \vec{\sigma}.\ \exists\ \vec{\rho^a}.\ \text{splits}\ (\vec{\rho^a}, \sigma) \wedge \exists\ \vec{\rho^b}.\ \text{splits}\ (\vec{\rho^b}, \vec{\sigma}) \Longrightarrow \vec{\rho^a} = \vec{\rho^b}
\end{align*}

\textbf{More definitions:}

Let $\Phi(\rho)$ = \text{List.fold\_left (fun sum instr.\ acc + $\delta$ (instr)) 0 $\rho$}. Note that for $\hat{\rho}$ the body of a well formed closure, $$\Phi(\hat{\rho}) = -1.$$

Furthermore, for any  any $\hat{\rho} = \hat{\rho}_g\ @\ \hat{\rho}_s$, $$\Phi(\hat{\rho}_g) = \alpha \ge 0, \qquad \Phi(\hat{\rho}_s) = - \alpha - 1.$$

\textbf{Proof of InjApply:}

Let $\vec{\sigma}$. Suppose, for a contradiction, there exist $\vec{\rho^a} \neq \vec{\rho^b}$ such that splits $(\vec{\rho^a}, \vec{\sigma})$ and splits $(\vec{\rho^b}, \vec{\sigma})$. Assuming the grow shrink property holds for $\hat{\rho}^a$ and $\hat{\rho}^b$, $$\hat{\rho}^a = \hat{\rho}_g^a\ @\ \hat{\rho}_s^a, \qquad \hat{\rho}^b = \hat{\rho}_g^b\ @\ \hat{\rho}_s^b.$$

TODO $\hat{\rho}_g^a = \hat{\rho}_g^b$.\\

Assume $\Phi(\hat{\rho}_g^a) = \alpha$. Then $\Phi(\hat{\rho}_s^a) = \Phi(\hat{\rho}_s^b) = - \alpha - 1$.

Then $\hat{\rho}_s^b = \hat{\rho}_s^a\ @\ \rho^*$, and $\Phi(\rho^*) = 0$ (more clearly, the instructions in $\rho^*$ do not change the size of the stack). \\

TODO guarantee that our compiler will not produce closure body programs with end with instructions that do not change the size of the stack.








\end{document}