tobast/L3-internship-report
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Linear lambda: started details

Browse source
This commit is contained in:
Théophile Bastian 2016-07-20 14:18:33 +01:00
parent df1e931494
commit a3ad301113
2 changed files with 25 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
concurgames.sty
View file

@ -5,6 +5,7 @@
\usepackage{MnSymbol} \usepackage{MnSymbol}
\usepackage{stmaryrd} \usepackage{stmaryrd}
\usepackage{tikz} \usepackage{tikz}
\usepackage{relsize}
\usetikzlibrary{shapes,arrows} \usetikzlibrary{shapes,arrows}
@ -28,6 +29,9 @@
\newcommand{\seman}[1]{\llbracket{} #1 \rrbracket} \newcommand{\seman}[1]{\llbracket{} #1 \rrbracket}
\newcommand{\tens}{\otimes}
\newcommand{\Tens}{\mathlarger\otimes}
\newcommand{\includedot}[2][]{% \newcommand{\includedot}[2][]{%
\begin{tikzpicture}[>=latex,line join=bevel,#1] \begin{tikzpicture}[>=latex,line join=bevel,#1]
\input{_build/dot/#2.tex} \input{_build/dot/#2.tex}

23
report.tex
View file

@ -301,12 +301,32 @@ and then computing the transitive reduction of the DAG\@.
%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Linear lambda-calculus} \section{Linear lambda-calculus}
Concurrent games can be used as a model of lambda-calculus \todo{ref Pierre~?}. Concurrent games can be used as a model of lambda-calculus.
To avoid non-determinism in the strategies, and to have a somehow easier To avoid non-determinism in the strategies, and to have a somehow easier
approach, one can use concurrent games as a model of \emph{linear} approach, one can use concurrent games as a model of \emph{linear}
lambda-calculus, that is, a variant of the simply-typed lambda-calculus where lambda-calculus, that is, a variant of the simply-typed lambda-calculus where
each variable in the environment can and must be used exactly once. each variable in the environment can and must be used exactly once.
\subsection{Definition}
The linear lambda calculus we use has the same syntax as the usual simply-typed
lambda calculus with type annotations and tensor product:
\begin{minipage}[t]{0.45\textwidth}
\begin{align*}
\text{Terms } t,u,\ldots ::=~&x \in \mathbb{V} \\
\vert~&t~u \\
\vert~&\lambda x^A \cdot t \\
\vert~&t \tens u
\end{align*}
\end{minipage} \hfill \begin{minipage}[t]{0.45\textwidth}
\begin{align*}
\text{Types } A,B,\ldots ::=~&\alpha \\
\vert~&A \linArrow B \\
\vert~&A \Tens B
\end{align*}
\end{minipage}
\begin{minipage}{0.4\textwidth} \begin{equation} \begin{minipage}{0.4\textwidth} \begin{equation}
\tag{\textit{Ax}} \tag{\textit{Ax}}
\frac{}{x : A \vdash x : A} \frac{}{x : A \vdash x : A}
@ -322,7 +342,6 @@ each variable in the environment can and must be used exactly once.
\label{typ:llam:app} \label{typ:llam:app}
\end{align} \end{minipage} \end{align} \end{minipage}
\todo{describe linear lambda-calculus?}
The implementation, which was supposed to be fairly simple, turned out to be The implementation, which was supposed to be fairly simple, turned out to be
not as trivial as expected due to technical details: while, in the theory, the not as trivial as expected due to technical details: while, in the theory, the