Assignment 4

2 files changed, 141 insertions, 0 deletions

diff --git a/assignment4.tex b/assignment4.tex
new file mode 100644
index 0000000..81d5a95
--- /dev/null
+++ b/assignment4.tex
@@ -0,0 +1,136 @@
+\documentclass[a4paper]{article}
+
+\usepackage[bottom=2cm]{geometry}
+\usepackage[english]{babel}
+
+\usepackage{enumitem}
+\setenumerate[1]{label=(\alph*)}
+
+\usepackage{fancyhdr}
+\renewcommand{\headrulewidth}{0pt}
+\renewcommand{\footrulewidth}{0pt}
+\fancyhead{}
+\fancyfoot[C]{Copyright {\textcopyright} 2016 Camil Staps}
+\pagestyle{fancy}
+
+\usepackage{sv}
+
+\title{Software Verification - assignment 4}
+\author{Camil Staps}
+
+\usepackage{rotating}
+\usepackage{amsmath}
+\usepackage{mathpartir}
+
+\def\List#1{\mathbf{List}(#1)}
+\def\Nil{\mathbf{Nil}}
+\def\Cons#1#2{\mathbf{Cons}\;#1\;#2}
+\def\empt#1{\text{empty}(#1)}
+\def\hd#1{\text{hd}(#1)}
+\def\tl#1{\text{tl}(#1)}
+\def\xs{\mathit{xs}}
+\def\ys{\mathit{ys}}
+\def\true{\mathbf{true}}
+\def\false{\mathbf{false}}
+\def\tapp{\tau_{\mathit{app}}}
+
+\begin{document}
+
+\maketitle
+\thispagestyle{fancy}
+
+\setcounter{section}{1}
+\section{Lists for ML}
+\begin{enumerate}
+  \item \begin{align*}
+      %\tau &::=\enspace \dots\\
+      %  &\enspace\enspace|\quad\, \List{\tau}\\
+      l &::=\enspace \Nil\\
+        &\enspace\enspace|\quad\, \Cons{e}{l}\\
+      e &::=\enspace \dots\\
+        &\enspace\enspace|\quad\, l\\
+        &\enspace\enspace|\quad\, \empt{e}\\
+        &\enspace\enspace|\quad\, \hd{e}\\
+        &\enspace\enspace|\quad\, \tl{e}\\
+    \end{align*}
+
+  \item \begin{mathpar}
+      \inferrule*[right=list]
+        {\xs \in l} {\xs \eval \xs} \qquad
+      \inferrule*[right=hd]
+        {\xs \eval \Cons{e}{l}} {\hd\xs \eval e} \qquad
+      \inferrule*[right=tl]
+        {\xs \eval \Cons{e}{l}} {\tl\xs \eval l} \\
+      \inferrule*[right=empty\_true]
+        {\xs \eval \Nil} {\empt\xs \eval \true} \qquad
+      \inferrule*[right=empty\_false]
+        {\xs \eval \Cons e l} {\empt\xs \eval \false}
+    \end{mathpar}
+
+  \item $$\mathit{append}=\lambda \xs \ys.\mlif{(\xs=\Nil)}{\ys}{(\Cons{\hd\xs}{\mathit{append}(\tl\xs)(\ys)})}.$$
+
+  \item \begin{mathpar}
+      \inferrule*[right=nil]
+        {l=\Nil}{\Gamma\vdash l:\List{\sigma}} \qquad
+      \inferrule*[right=cons]
+        {\Gamma\vdash e:\sigma \quad \Gamma\vdash l:\List{\sigma}}{\Gamma\vdash\Cons{e}{l}:\List{\sigma}} \\
+      \inferrule*[right=hd]
+        {\Gamma\vdash l:\List\sigma}{\hd{l}:\sigma} \qquad
+      \inferrule*[right=tl]
+        {\Gamma\vdash l:\List\sigma}{\tl{l}:\List\sigma} \qquad
+      \inferrule*[right=empty]
+        {\Gamma\vdash l:\List\sigma}{\empt{l}:\Bool} \qquad
+    \end{mathpar}
+
+  \item 
+    \begin{sidewaysfigure}\begin{mathpar}\scriptsize
+      \inferrule*[right=Lambda]
+        {
+          \inferrule*[right=If]
+            {
+              \inferrule*[right=Bin Op]
+                {
+                  = : (\List\sigma, \List\sigma)\to\Bool \\\\
+                  \Gamma \vdash \xs:\List\sigma \and
+                  \inferrule*[right=nil]{}{\Gamma \vdash \Nil:\List\sigma}
+                }
+                {\Gamma \vdash (\xs=\Nil):\Bool}
+              \and
+              \Gamma \vdash \ys:\List\sigma
+              \and
+              \inferrule*[right=cons]
+                {
+                  \inferrule*[right=hd]{\Gamma\vdash\xs:\List\sigma}{\Gamma \vdash \hd\xs:\sigma}
+                  \and
+                  \inferrule*[right=App]
+                    {
+                      \inferrule*[right=App]
+                        {
+                          \Gamma \vdash \mathit{a}:\tapp \and
+                          \inferrule*[right=tl]
+                            {\Gamma \vdash \xs:\List\sigma}
+                            {\Gamma \vdash \tl\xs:\List\sigma}
+                        }
+                        {\Gamma \vdash \mathit{a}(\tl\xs):\List\sigma\to\List\sigma}
+                      \and
+                      \Gamma \vdash \ys:\List\sigma
+                    } %todo
+                    {\Gamma \vdash \mathit{a}(\tl\xs)(\ys):\List\sigma}
+                }
+                {\Gamma \vdash \Cons{\hd\xs}{\mathit{a}(\tl\xs)(\ys)}:\List\sigma}
+            } %todo
+            {\Gamma \vdash \mlif{(\xs=\Nil)}{\ys}{(\Cons{\hd\xs}{\mathit{a}(\tl\xs)(\ys)})} : \List\sigma}
+        }
+        {\mathit{a}:\tapp \vdash \lambda \xs \ys.\mlif{(\xs=\Nil)}{\ys}{(\Cons{\hd\xs}{\mathit{a}(\tl\xs)(\ys)})} : \tapp} \\
+
+        \setlength\arraycolsep{1pt}
+        \begin{array}{rl}
+          \text{where}\qquad a & \stackrel{\text{def}}{=} \mathit{append}, \\
+                    \tapp & \stackrel{\text{def}}{=} \List\sigma\;\List\sigma\to\List\sigma, \\
+                        \Gamma & \stackrel{\text{def}}{=} \xs:\List\sigma, \ys:\List\sigma, \mathit{a}:\tapp.
+        \end{array}
+      \end{mathpar}\end{sidewaysfigure}
+\end{enumerate}
+
+\end{document}
+
diff --git a/sv.sty b/sv.sty
index d28ca47..6be0b3d 100644
--- a/sv.sty
+++ b/sv.sty
@@ -40,3 +40,8 @@
 
 \let\next\Circle
 
+\let\eval\Downarrow
+\def\mlif#1#2#3{\mathbf{if}\;#1\;#2\;#3}
+\def\mllet#1#2#3{\mathbf{let}\;\mathit{#1}=#2\;\mathbf{in}\;#3}
+\def\Bool{\mathbf{Bool}}
+