\documentclass{article}
\usepackage{latexsym}
\usepackage{lcom}
\usepackage{cdsty}
\input{minml-defns}

\newcommand{\apply}{\mbox{\textbf{apply}}}
\newcommand{\pair}[1]{\langle #1 \rangle}
\newcommand{\ep}{\pair{}}
\newcommand{\inl}[1]{\mbox{\textbf{inl}}^{#1}}
\newcommand{\inlt}{\mbox{\textbf{inl}}^{\tau_1+\tau_2}}
\newcommand{\inrt}{\mbox{\textbf{inr}}^{\tau_1+\tau_2}}
\newcommand{\inr}[1]{\mbox{\textbf{inr}}^{#1}}
\newcommand{\fun}[3]{\mbox{\textbf{fun }} {#1} {#2} \mbox{\textbf{ is }}
 { #3}\mbox{ \textbf{end} }}
\newcommand{\case}[5]{\mbox{\textbf{case }} {#1}\mbox{\textbf{ of }}
  {#2}\Rightarrow {#3}\mid {#4} \Rightarrow  {#5}} 
\newcommand{\caset}{\mbox{\textbf{case }} e \mbox{\textbf{ of }}
  \inl{} \ x_1\hastype\tau_1\Rightarrow e_1\mid \inr{} \ x_2\hastype\tau_2 \Rightarrow  e_2}
\newcommand{\recordt}{\{l_1\hastype \tau_1\mdots l_n\hastype \tau_n\}}
\newcommand{\variantt}{[l_1\hastype \tau_1\mdots l_n\hastype \tau_n]}
\newcommand{\record}{\{l_1=e_1\mdots l_n=e_n\}}
\newcommand{\varexp}{\mbox{\textbf{case} $e$ \textbf{of }}
  l_1=x_1\Rightarrow e_1\mid \mdots\mid l_n=\tau_n\Rightarrow e_n}
\newcommand{\varex}[1]{\mbox{\textbf{case} $#1$ \textbf{of }}
  l_1=x_1\Rightarrow e_1\mid \mdots\mid l_n=\tau_n\Rightarrow e_n}
\begin{document}

\section{Records and variants}
\label{sec:rv}

\emph{Records} are tuples whose components, called \emph{fields} have labels;
given a record we can access one of its component via one of its
labels. For example \texttt{type id
  =\{name:string,born:int\} }; if \texttt{oneid} is of type \texttt{id},
you can access the \texttt{name} field with \texttt{oneid.name}.
 Analogously \emph{variants} are $n$-ary
labeled sums. They come equipped with a $n$-ary injection operator and
a correspondent case destructor. We make the convention to use the
notation $S_i$ such that $1\leq i\leq n$. We assume a
denumerable set of labels.
\[
\begin{array}{rrcl}
\mathit{Types} & \tau &  \bnfas &\dots\bnfalt\recordt\bnfalt\variantt\\
\mathit{Expressions}& e & \bnfas &
\dots\bnfalt\record\bnfalt e.l\bnfalt[l=e]_{[l_i\hastype\tau_i]_i}\bnfalt \\
& & &\varexp\\
\mathit{Values} & v &\bnfas & \dots \bnfalt \{l_1=v_1\mdots
l_n=v_n\}\bnfalt [l=v]_{[l_i\hastype\tau_i]_i}
\end{array}
\]
 
Give typing and SOS evaluation rules for this language:

\[
\begin{array}{c}
\ianc{\GG\vd e_i\hastype \tau_i}{\GG\vd\record\hastype\recordt}{\forall i. 1\leq
  i\leq n}\vsk
\ianc{\GG\vd e\hastype\recordt}{\GG\vd e.{l_i}\hastype\tau_i}{\exists i. 1\leq
  i\leq n }\vsk
\ianc{\GG\vd e_i\hastype
  \tau_i}{\GG\vd[l=e]_{[l_i\hastype\tau_i]_i}\hastype \variantt }{\exists i.1\leq
  i\leq n}\vsk
\ianc{\GG[x_i\oftp\tau_i]\vd e_i\hastype\tau}{\GG\vd\varexp\hastype\tau}{\forall i. 1\leq
  i\leq n}\vsk\vsk
\ianc{\mbox{for some} 1\le j\leq n}{ \{l_1=v_1\mdots l_n=v_n\}.{l_j}\mapsto v_j}{[EvalField]}\qquad
\ianc{e\mapsto e'}{ \{\dots  l=e\dots\}\mapsto\{\dots  l=e'\dots\}}
{[SearchField]} \vsk
\ianc{e\mapsto e'}{\varexp\mapsto\varex{e'}}{[CaseSearch]}\vsk
\ianc{}{\varex{[l_i=v_i]}\mapsto [v_i/x_i]e_i}{[CaseEval]}
\end{array}
\]


\section{DeBruin indices}
\label{sec:dbr}
\newcommand{\up}{\uparrow}
Db indices are used to enforce the bound variable convention:
variables are replaced with pointers to the correspondent binding
occurrence, implemented as the number of \textbf{fun} it needs
to traverse to reach the place where it is bound. For example, if we
abbreviate $\fun {} {x} {e}$ in $\lx e$ and \apply with
justapposition:
\beq
\l x. \l y. x(\l z.yz) & = & \l(\l(2(\l (2\ 1))))
\eneq
Rather than using integers we use a \emph{shift} operator analogous to
a postfix successor:
\beq
\l x. \l y. x(\l z.yz) & = & \l(\l(1\up(\l ((1\up) \ 1))))
\eneq
This yields the following language:
\[
\begin{array}{rrcl}
\mathit{Expressions}& e & \bnfas & x\bnfalt \lx e\bnfalt e\ e'\\
\mathit{Db Expressions}& F & \bnfas & 1\bnfalt \l F\bnfalt F\
F'\bnfalt F\up
\end{array}\]

Give rules to transform an expression into its Db format.
\[
\begin{array}{c}
\ianc{\GG,x\vd e = F}{\GG\vd\lx e = \l F}{\l}\qquad
\ibnc{\GG\vd e_1 = F_1}{\GG\vd e_2  = F_2}{\GG\vd e_1\ e_2 = F_1 \ F_2}{app}
\vsk
\ianc{}{\GG,x\vd x=1}{Var}\qquad
\ianc{\GG\vd e = F}{\GG,x\vd e = F\up}{\up}
\end{array}\]
\end{document}

