main.tex

\documentclass{beamer}
% \documentclass[handout]{beamer}
\usetheme{metropolis}           % Use metropolis theme
\setbeamertemplate{footline}[frame number]
\title{Formalising Modal Embeddings of Call-by-Name and Call-by-Value}
\date{\today}
\author[Floris Reuvers]{Floris Reuvers \\[1ex]
  \small Supervisor: dr. N.M. van der Weide \\
  \small Second Reader: dr. E.G.M. Hubbers
}
\institute{Radboud University} % What is actually the institute?

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage{array}
\usepackage{listings}
\usepackage{rutitlepage}
\usepackage{hyperref}
\usepackage{enumitem}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{xspace}
\usepackage{tabularx}
\usepackage{multicol}
\usepackage{multirow}
\usepackage{float}
\usepackage{cmll}
\usepackage{lipsum}
\usepackage{amsthm}
\usepackage{thmtools}
\usepackage{booktabs}
\usepackage{caption}
\usepackage{cleveref}
\usepackage{amsthm}
\usepackage{enumitem}
\usepackage{latexsym}
\usepackage{newunicodechar}
\usepackage{code/latex/agda} % path to generated agda.sty

\newcommand{\lambdabar}{\lambda\!\!\raisebox{0.6ex}{\scalebox{0.8}{--}}}

\newunicodechar{□}{\ensuremath{\mathnormal\square}}
\newunicodechar{⇒}{\ensuremath{\mathnormal\Rightarrow}}
\newunicodechar{λ}{\ensuremath{\mathnormal\lambda}}
\newunicodechar{↝}{\ensuremath{\mathnormal\leadsto}}
\newunicodechar{₁}{\ensuremath{_1}}
\newunicodechar{₂}{\ensuremath{_2}}
\newunicodechar{ₙ}{\ensuremath{_n}}
\newunicodechar{ν}{\ensuremath{\mathnormal\nu}}
\newunicodechar{ζ}{\ensuremath{\mathnormal\zeta}}
\newunicodechar{ξ}{\ensuremath{\mathnormal\xi}}
\newunicodechar{μ}{\ensuremath{\mathnormal\mu}}
\newunicodechar{β}{\ensuremath{\mathnormal\beta}}
\newunicodechar{⊢}{\ensuremath{\mathnormal\vdash}}
\newunicodechar{Γ}{\ensuremath{\mathnormal\Gamma}}
\newunicodechar{Δ}{\ensuremath{\mathnormal\Delta}}
\newunicodechar{∀}{\ensuremath{\mathnormal\forall}}
\newunicodechar{ƛ}{\ensuremath{\lambda\mkern-8mu\raisebox{0.45ex}{\rotatebox{15}{\scalebox{0.8}{--}}}}}

\newcolumntype{Y}{>{\centering\arraybackslash}X}

\RequirePackage{defs}
\RequirePackage{bussproofs}
\RequirePackage{formalgrammars}

\theoremstyle{definition}
% \newtheorem{theorem}{Theorem}[chapter] %QUESTION, SECTION OR CHAPTER?
% \newtheorem{definition}[theorem]{Definition}
% \newtheorem{lemma}[theorem]{Lemma}
% \newtheorem{proposition}[theorem]{Proposition}
% \newtheorem{example}[theorem]{Example}

% \crefname{definition}{Definition}{Definitions}
% \Crefname{definition}{Definition}{Definitions}

\begin{document}
  \maketitle
  
  \section{Introduction}

  \begin{frame}{Context}
    \begin{block}{Functional Programming Languages}
      \begin{itemize}
        \item[\textbullet] OCaml, F\#, SML, Haskell, Clean
      \end{itemize}
    \end{block} \pause

    \begin{block}{Evaluation Strategies}
      \begin{itemize}
        \item[\textbullet] \alert{Call-by-value} (\textsf{cbv})
          \begin{itemize}
            \item[--] Evaluate the argument first, then substitute
            \item[--] OCaml, F\#, SML 
          \end{itemize} \pause
        \item[\textbullet] \alert{Call-by-name} (\textsf{cbn}) / lazy
          \begin{itemize}
            \item[--] Substitute the argument, evaluate only when needed
            \item[--] Haskell, Clean
          \end{itemize}
      \end{itemize}
    \end{block}
  \end{frame}

  \begin{frame}{Example \textsf{cbn} and \textsf{cbv}}
    \begin{block}{Let f be defined as}
      \begin{flalign*}
        & f (x) = x * x &
      \end{flalign*}
    \end{block} \pause
    
    \begin{block}{\alert{\textsf{cbn}} and \alert{\textsf{cbv}} evaluation of f (3 + 3)}
      \begin{align*}
        \onslide<2->{& \textbf{\alert{\textsf{cbn}:}} &                    & \textbf{\alert{cbv:}} &           } \\
        \onslide<3->{f (3 + 3)    & \to (3 + 3) * (3 + 3) & f (3 + 3)     & \to f (6) } \\
        \onslide<4->{             & \to 6 * (3 + 3)       &               & \to 6 * 6 } \\
        \onslide<5->{             & \to 6 * 6             &               & \to 36 }    \\
        \onslide<6->{             & \to 36}
      \end{align*}
    \end{block} \pause
  \end{frame}
  
  \begin{frame}{Reasons to Unify \textsf{cbn} and \textsf{cbv}}
    \begin{block}{Pros and Cons of \alert{\textsf{cbn}} and \alert{\textsf{cbv}}}
      \begin{itemize}
        \item Sometimes arguments are used:
        \begin{itemize}
          \item[--] \alert{zero} times: \alert{cbn} is more efficient
          \item[--] \alert{multiple} times: \alert{cbv} is more efficient
        \end{itemize}
      \end{itemize}
    \end{block} \pause

    \begin{block}{Unification}
      \begin{itemize}
        \item[\textbullet] Best of both worlds
        \item[\textbullet] Universal Framework
      \end{itemize}
    \end{block}

    \end{frame}

  \begin{frame}{Some approaches to Unification}

  \begin{block}{\alert{Thunks} and \alert{CPS} Translation (Hatcliff et al.)}
    \begin{itemize}
      \item[\textbullet] Wrappers around expressions to delay evaluation
      \item[\textbullet] Continuous Passing Style translation 
    \end{itemize}
    
  \end{block}\pause

  \begin{block}{\alert{Linear} Logic (Maraist et al. and Ehrhard et al.)}
    \begin{itemize}
      \item[\textbullet] Explicit control over resources
      \item[\textbullet] Arguments correspond to resource usage
    \end{itemize}
  \end{block} \pause

  \begin{block}{\alert{Modal} Logic (Espírito Santo et al.)}
    \begin{itemize}
      \item[\textbullet] Adds box modality
      \item[\textbullet] Boxed terms are treated as values
    \end{itemize}
  \end{block}

  \end{frame}

  \begin{frame}{Formalisation in Agda}
    \begin{itemize}
      \item[\textbullet] \alert{Agda}: programming language and proof assistant
      \item[\textbullet] Unification of \alert{\textsf{cbn}} and \alert{\textsf{cbv}} into a universal framework  
      \item[\textbullet] Formalise this framework in \alert{Agda}
      \item[\textbullet] Proof of the main properties of the framework
    \end{itemize}
  \end{frame}

  \begin{frame}{Main Contribution}
    \Large
    We formalised the unification of call-by-name and call-by-value using modal logic in Agda
  \end{frame}

  \section{Background}
  \begin{frame}{Lambda Calculus (\lc)}
    Simple and formal \alert{model of computation}
    \begin{block}{\boldmath${\lambda}$-terms and types}
      % \vspace{7pt}
      \begin{align*}
        \begin{grammar}{
          \pr{$M, N, P, Q$}{$x \gors \lambda x.M \gors M N$}
        }
        \end{grammar}
        \quad 
        \begin{grammar}{
          \pr{$A$}{$X \gors A \fa A'$}
        }
        \end{grammar}
      \end{align*}
    \end{block} \pause
    \begin{block}{Example \alert{terms} and \alert{types}} \pause
      \begin{columns}
        \begin{column}{0.48\textwidth}
          \begin{itemize}
            \item $x$ \pause
            \item $\lamb{x}{x}$ \pause
            \item $\lamb{y}{y} z$ \pause
            \item $(\lamb{y}{y}) z$ \pause
            \item $\lamb{x}{\lamb{t}{x t (\lamb{s}{w})}wy}$ \pause
          \end{itemize}
        \end{column}
        \begin{column}{0.48\textwidth}
          \begin{itemize}
            \item $X$ \pause
            \item $X \fa X$\pause
            \item $(X \fa X) \fa X$\pause
            \item $(X \fa X) \fa (X \fa X)$
          \end{itemize}
        \end{column}
      \end{columns}
    \end{block}
  \end{frame}

  \begin{frame}{Call-by-name \lc (\lan)}
    \begin{block}{\boldmath${\beta}$-reduction}
      \begin{align*}
        (\lamb{x}{M})N \red M \subst{x}{N} \quad \quad (\bn)
      \end{align*}
    \end{block} \pause
    \begin{block}{Closure rule}
      \begin{prooftree}
        \def\extraVskip{5pt}
        \AxiomC{$M \red M'$}
        \RightLabel{($\mu$)}
        \UnaryInfC{$M N \red M' N$}
      \end{prooftree}
    \end{block} \pause
    \begin{block}{\textsf{cbn} evaluation}
      \begin{itemize}
        \item \alert{\br} together with the \alert{$\mu$} closure rule
      \end{itemize}
    \end{block}
  \end{frame}

  \begin{frame}{Call-by-box \lc (\lab)}
    \begin{block}{\boldmath${\lambda}$-terms}
      \begin{align*}    
        \begin{grammar}{
          \pr{$M, N, P, Q$}{$\boxe{x} \gors \lambda x.M \gors M N \gors \boxi{N}$}
        }
        \end{grammar}
      \end{align*}
    \end{block} \pause
    \begin{block}{Idea}
      \begin{itemize}
        \item[\textbullet] $\varepsilon$: \alert{unbox} operator
        \item[\textbullet] \textsf{box}: \alert{box} operator
        \item[\textbullet] paramters of abstractions are \alert{boxed}
        \item[\textbullet] \alert{box} gives control over what to evaluate 
      \end{itemize}
    \end{block} \pause
    \begin{block}{Types}
      \begin{align*}
        \begin{grammar}{
          \pr{$A$}{$X \gors B \fa A \gors B$}
        } \quad \quad
        \end{grammar}
        \begin{grammar}{
          \pr{$B$}{$\boxit{A}$}
        }
        \end{grammar}
      \end{align*}
    \end{block}
  \end{frame}

  \begin{frame}{Call-by-box evaluation}
    \begin{block}{\boldmath${\beta}$-reduction}
      \begin{align*}
        (\lamb{x}{M})\boxi{N} \red M \subst{\boxe{x}}{N} \quad \quad (\bb)
      \end{align*}
    \end{block} \pause
    \begin{block}{Closure rules}
      \vspace{-15pt} % Adjust this value as needed (e.g. -1mm to -4mm)
      \begin{tabularx}{\textwidth}{YY}
        \begin{prooftree}
          \AxiomC{$M \rightarrow M'$} % Conclusion
          \RightLabel{$(\mu)$}
          \UnaryInfC{$M N \rightarrow M' N$}
        \end{prooftree}
        & \quad
        \begin{prooftree}
          \AxiomC{$N \rightarrow N'$} % Conclusion
          \RightLabel{$(\nu)$}
          \UnaryInfC{$M N \rightarrow M N'$}
        \end{prooftree}
      \end{tabularx}
      \vspace{10pt}
    \end{block} \pause
    \begin{block}{\alert{Call-by-box} (cbb) evaluation}
      \begin{itemize}
        \item \alert{\br} together with the \alert{$\mu$} and \alert{$\nu$} closure rule
      \end{itemize}
    \end{block}
  \end{frame}

  \section{\texorpdfstring{Embeddings into \lab}{Embeddings into the boxed lambda calculus}}
  \begin{frame}{Girard's and Gödel's Translation}
    \begin{itemize}
      \item[\textbullet] Translate standard \lc into \lab
      \item[\textbullet] \alert{Girard's} translation: \lan into \lab
      \item[\textbullet] \alert{Gödel's} translation: \lav into \lab
      \item[\textbullet] \alert{Cbb} simulates
        \begin{itemize}
          \item[--] \alert{\textsf{cbn}} under \alert{Girard's} embedding
          \item[--] \alert{\textsf{cbv}} under \alert{Gödel's} embedding
        \end{itemize}
      \item[\textbullet] Notation: $\girard{M}$ is the Girard translation of $\lambda$-term $M$
    \end{itemize}
  \end{frame}
    
  \begin{frame}{Girard's Embedding}
    \begin{block}{Translation from \textsf{cbn} $\lambda$-terms to \lab}
      \begin{align*}
        \girard{X}                 & = X                                          & \girard{x}             & = \boxe{x} \\
        \girard{(A_1 \fa A_2)}     & = \boxt{\girard{A_1}} \fa \girard{A_2}       & \girard{(\lamb{x}{M})} & = \lamb{x}{\girard{M}} \\
                                   &                                              & \girard{(M N)}         & = \girard{M} \boxi{\girard{N}}
      \end{align*}
    \end{block} \pause
    \begin{block}{Embedding of \boldmath${(\lamb{x}{x}) y}$}
      \begin{align*}
        \onslide<2-> { \girard{\alert{((\lamb{x}{x}) y)}} & = \girard{(\lamb{x}{x})} \boxi{\girard{\alert{y}}} } \\
                                  \onslide<3-> { & = \girard{\alert{(\lamb{x}{x})}} \boxi{\boxe{y}} }   \\
                                  \onslide<4-> { & = (\lamb{x}{\girard{\alert{x}}}) \boxi{\boxe{y}} }   \\
                                  \onslide<5-> { & = (\lamb{x}{\boxe{x}}) \boxi{\boxe{y}} }
      \end{align*}
    \end{block}
  \end{frame}

  \begin{frame}{Example of cbb under Girard's embedding}
    \begin{block}{\boldmath${\beta}$-reduction}
      \begin{align*}
        (\lamb{x}{M})\boxi{N} \red M \subst{\boxe{x}}{N} \quad \quad (\bb)
      \end{align*}
    \end{block} \pause
    \begin{block}{Example \alert{cbb} evaluation}
      \begin{align*}
        \onslide<2-> { \alert{((\lamb{x}{\boxe{x}}) \ \boxi{\lamb{y}{\boxe{y}}})} \ \boxi{\boxe{z}} & \redbn \alert{(\lamb{y}{\boxe{y}}) \boxi{\boxe{z}}}} \\
        \onslide<3-> { & \redbn \boxe{z} }
      \end{align*}
    \end{block}
  \end{frame}

  \begin{frame}{Girard's Image}
    \begin{block}{Well-typed terms after translation}
      \vspace{7pt}
      \begin{grammar}{
        \pr{$M, N$}{$\boxe{x} \gors \lambda x.M \gors M \boxi{N}$}
      }
      \end{grammar}
    \end{block} \pause
    \vspace{5pt}
    \begin{itemize}
      \item[\textbullet] Eliminates the \alert{$\nu$} closure rule
      \item[\textbullet] Only the \alert{$\mu$} rule remains
      \item[\textbullet] Call-by-box becomes \alert{deterministic}
      \item[\textbullet] If $M$ evaluates to $N$ with \alert{\textsf{cbn}}, then $\girard{M}$ evaluates to $\girard{N}$ with \alert{\textsf{cbb}} 
    \end{itemize}
  \end{frame}

  \section{Agda}

  \begin{frame}{What is Agda?}
    \begin{itemize}
      \item \includegraphics[width=0.5\textwidth]{Agda.png}
      \item[\textbullet] Functional programming language
      \item[\textbullet] Inspired by Haskell
      \item[\textbullet] Proof assistant
      \item[\textbullet] Dependently typed
      \item[\textbullet] Hole-based programming
    \end{itemize}
  \end{frame}

  \begin{frame}{Some Agda code}
    \begin{block}{Girard's Embedding for Types}
      \begin{align*}
        \girard{(A_1 \fa A_2)}     & = \boxt{\girard{A_1}} \fa \girard{A_2}      \\                                         
        \girard{X}                 & = X                                         
      \end{align*}
    \end{block} \pause
    \begin{block}{Embedding in Agda}
      \input{code/latex/embedCBNIntoCBB1.tex}
    \end{block}
  \end{frame}

  \begin{frame}{Challenges}
    \begin{itemize}
      \item[\textbullet] Variables
        \begin{itemize}
          \item[--] Use of \alert{de Bruijn indices}
          \item[--] Variables represented as natural numbers
        \end{itemize} \pause
      \item[\textbullet] Ill-typed terms
        \begin{itemize}
          \item[--] \lterm $y (\lamb{x}{x})$ is not typeable
          \item[--] Solution: restrict to \alert{well-typed} \lterms
        \end{itemize} \pause
      \item[\textbullet] Formal definition of \alert{substitution}
      \item[\textbullet] Formal definition of \alert{\raiseembn} in Gödel's translation %do I have time for this??? Probably not, so I'll probably skip this
    \end{itemize}
  \end{frame}

  \begin{frame}{Experience Working with Agda}
    \begin{itemize}
      \item[\textbullet] Intersting learning experience
      \item[\textbullet] High learning curve
      \item[\textbullet] Hole based programming is amazing
      \item[\textbullet] Error message are not always helpful
      \item[\textbullet] But give it a try! \pause
        \begin{itemize}
          \item[--] Follow the online \alert{PLFA} book (Programming Language Foundations in Agda)
          \item[--] \alert{\url{https://plfa.github.io/}} 
        \end{itemize}  
    \end{itemize}
  \end{frame}

  \section{Conslusions}
  
  \begin{frame}{Conclusion}
    \begin{itemize}
      \item[\textbullet] Recap of the \lc
      \item[\textbullet] Explained \alert{\lab}
      \item[\textbullet] Defined the unifying relation \alert{\textsf{cbb}}
      \item[\textbullet] \alert{Girard's} translation
      \item[\textbullet] Formally proved the main properties of the translations    
    \end{itemize}
  \end{frame}

  \section{Questions?}

  % \begin{frame}{Questions?}
  %   test
  % \end{frame}

  % \section{Challenges of Formalisation}
  % \begin{frame}{Overview Challenges}
  %   \begin{itemize}
  %     \item[\textbullet] Variables
  %     \item[\textbullet] Ill typed terms
  %     \item[\textbullet] Formal definition of \raiseembn
  %   \end{itemize}
  % \end{frame}
  % \begin{frame}{De Bruijn Indices}
  %   Lorem ipsum
  % \end{frame}
  % \begin{frame}{Restriction to well-typed terms}
  %   Lorem ipsum
  % \end{frame}
  % \begin{frame}{Formal definition of \raiseembn}
  %   Lorem ipsum
  % \end{frame}

  % \section{Propositions}
  % \begin{frame}{Girard's Translation}
  %   Lorem ipsum
  % \end{frame}
  % \begin{frame}{Gödel's Translation}
  %   Lorem ipsum
  % \end{frame}

  % \section{Conclusion}
  % \begin{frame}{Conclusion}
  %   Lorem ipsum
  % \end{frame}
  % \begin{frame}{Boxed Lambda Calculus}
  %   \small
  %   \begin{block}{\textsf{cbn} \lc (\lan)}
  %     \begin{grammar}{
  %       \pr{$M, N, P, Q$}{$x \gors \lambda x.M \gors M N$}
  %     }
  %     \end{grammar}
  %     \begin{align*}
  %       (\lamb{x}{M})N \red M \subst{x}{N} \quad \quad (\bn)
  %     \end{align*}
  %   \end{block}
  %   \small
  %   \begin{block}{Boxed \lc (\lab)}
  %     \begin{grammar}{
  %       \pr{$M, N, P, Q$}{$\boxe{x} \gors \lambda x.M \gors M N \gors \boxi{N}$}
  %     }
  %     \end{grammar}
  %     \begin{align*}
  %       (\lamb{x}{M})\boxi{N} \red M \subst{\boxe{x}}{N} \quad \quad (\bb)
  %     \end{align*}
  %   \end{block}
  %   \small
  %   \begin{block}{Girard's Translation}
  %     \begin{align*}
  %       \girard{X}                 & = X                                          & \girard{x}             & = \boxe{x} \\
  %       \girard{(A_1 \fa A_2)}     & = \boxt{\girard{A_1}} \fa \girard{A_2}       & \girard{(\lamb{x}{M})} & = \lamb{x}{\girard{M}} \\
  %                                   &                                              & \girard{(M N)}         & = \girard{M} \boxi{\girard{N}}
  %     \end{align*}
  %   \end{block}
  % \end{frame}
  % \section{Research Results}
  % \begin{frame}[fragile]{Research Results}
  %   \begin{block}{Preservation of Reduction}
  %     \center  
  %     If $M \rednb N$ then $\girard{M} \redbbox \girard{N}$.
  %   \end{block}
  %   \tiny
  %   \begin{block}{Agda Proof}
  %     \input{code/latex/pres-red.tex}
  %   \end{block}
  % \end{frame}
  % \begin{frame}[fragile]{Research Results}
  %   \begin{block}{Preservation of Evaluation}
  %     If $M \redn N$ then $\girard{M} \redbn \girard{N}$.
  %   \end{block}
  %   \small
  %   \begin{block}{Agda Proof}
  %     \input{code/latex/pres-eval.tex}
  %   \end{block}
  % \end{frame}
\end{document}