funclang series2: Added report.

funclang-taddeus/series2/series2.tex

+\documentclass[10pt,a4paper]{article}
+
+\usepackage[english]{babel}
+\usepackage[utf8]{inputenc}
+\usepackage{amsmath,hyperref,graphicx,booktabs,float,listings}
+
+% Paragraph indentation
+\setlength{\parindent}{0pt}
+\setlength{\parskip}{1ex plus 0.5ex minus 0.2ex}
+
+\title{Functional Languages - Assignment series 2}
+\author{Tadde\"us Kroes (6054129)}
+
+\begin{document}
+
+\maketitle
+
+\section{Assignment 4}
+
+Assignment: \emph{Define the Boolean functions negation, disjunction and
+conjunction as $\lambda$-terms.}
+
+\newcommand{\s}{\hspace{2mm}}
+\newcommand{\true}{\lambda a.\lambda b.a}
+\newcommand{\truea}{\lambda u.\lambda v.u}
+\newcommand{\false}{\lambda a.\lambda b.b}
+\newcommand{\falsea}{\lambda u.\lambda v.v}
+
+\subsection{Negation}
+
+Negation flips the value of a boolean (TRUE becomes FALSE and vice versa).
+Consider $\neg = \lambda b.\lambda x.\lambda y.((b \s y) \s x)$.
+
+Given that $TRUE = \true$ and $FALSE = \false$, we can make the following
+derivations:
+
+\begin{table}[H]
+	\begin{tabular}{rl}
+		$\neg TRUE$ & $= (\lambda b.\lambda x.\lambda y.((b \s y) \s x) \s \true)$ \\
+		& $\rightarrow_{\beta} \lambda x.\lambda y.((\true \s y) \s x)$ \\
+		& $\rightarrow_{\beta} \lambda x.\lambda y.(\lambda b.y \s x)$ \\
+		& $\rightarrow_{\beta} \lambda x.\lambda y.y$ \\
+		& $\equiv_{\alpha} FALSE$ \\
+		& \\
+		$\neg FALSE$ & $= (\lambda b.\lambda x.\lambda y.((b \s y) \s x) \s \false)$ \\
+		& $\rightarrow_{\beta} \lambda x.\lambda y.((\false \s y) \s x)$ \\
+		& $\rightarrow_{\beta} \lambda x.\lambda y.(\lambda b.b \s x)$ \\
+		& $\rightarrow_{\beta} \lambda x.\lambda y.x$ \\
+		& $\equiv_{\alpha} TRUE$ \\
+	\end{tabular}
+\end{table}
+
+TRUE and FALSE are both flipped, so the function $\neg$ is correct.
+
+\pagebreak
+
+\subsection{Disjunction}
+
+The disjunction function $\vee$ should have the following properties: \\
+TRUE $\vee$ TRUE = TRUE \\
+TRUE $\vee$ FALSE = TRUE \\
+FALSE $\vee$ TRUE = TRUE \\
+FALSE $\vee$ FALSE = FALSE
+
+Consider $\vee = \lambda p.\lambda q.((p \s p) \s q)$. Given the functions for
+TRUE and FALSE, the combination of the following derivations proves that the
+function $\vee$ is correct:
+
+\begin{table}[H]
+	\begin{tabular}{rl}
+		$TRUE \s\vee\s TRUE$ & $= (\lambda p.(\lambda q.((p \s p) \s q) \s \true) \s \true)$ \\
+		& $\rightarrow_{\beta} (\lambda q.((\true \s \true) \s q) \s \true)$ \\
+		& $\rightarrow_{\beta} ((\true \s \true) \s \true)$ \\
+		& $\rightarrow_{\alpha,\beta} (\lambda b.\truea \s \true)$ \\
+		& $\rightarrow_{\beta} \truea$ \\
+		& $\equiv_{\alpha} TRUE$ \\
+		& \\
+		$TRUE \s\vee\s FALSE$ & $= (\lambda p.(\lambda q.((p \s p) \s q) \s \false) \s \true)$ \\
+		& $\rightarrow_{\beta} (\lambda q.((\true \s \true) \s q) \s \false)$ \\
+		& $\rightarrow_{\beta} ((\true \s \true) \s \false)$ \\
+		& $\rightarrow_{\alpha,\beta} (\lambda b.\truea \s \false)$ \\
+		& $\rightarrow_{\beta} \truea$ \\
+		& $\equiv_{\alpha} TRUE$ \\
+		& \\
+		$FALSE \s\vee\s TRUE$ & $= (\lambda p.(\lambda q.((p \s p) \s q) \s \true) \s \false)$ \\
+		& $\rightarrow_{\beta} (\lambda q.((\false \s \false) \s q) \s \true)$ \\
+		& $\rightarrow_{\beta} ((\false \s \false) \s \true)$ \\
+		& $\rightarrow_{\beta} (\lambda b.b \s \true)$ \\
+		& $\rightarrow_{\beta} \true$ \\
+		& $\equiv_{\alpha} TRUE$ \\
+		& \\
+		$FALSE \s\vee\s FALSE$ & $= (\lambda p.(\lambda q.((p \s p) \s q) \s \false) \s \false)$ \\
+		& $\rightarrow_{\beta} (\lambda q.((\false \s \false) \s q) \s \false)$ \\
+		& $\rightarrow_{\beta} ((\false \s \false) \s \false)$ \\
+		& $\rightarrow_{\beta} (\lambda b.b \s \false)$ \\
+		& $\rightarrow_{\beta} \false$ \\
+		& $\equiv_{\alpha} FALSE$ \\
+	\end{tabular}
+\end{table}
+
+\pagebreak
+
+\subsection{Conjunction}
+
+The disjunction function $\wedge$ should have the following properties: \\
+TRUE $\wedge$ TRUE = TRUE \\
+TRUE $\wedge$ FALSE = FALSE \\
+FALSE $\wedge$ TRUE = FALSE \\
+FALSE $\wedge$ FALSE = FALSE
+
+Consider $\wedge = \lambda p.\lambda q.((p \s q) \s p)$. Given the functions for
+TRUE and FALSE, the combination of the following derivations proves that the
+function $\wedge$ is correct:
+
+\begin{table}[H]
+	\begin{tabular}{rl}
+		$TRUE \s\wedge\s TRUE$ & $= (\lambda p.(\lambda q.((p \s q) \s p) \s \true) \s \true)$ \\
+		& $\rightarrow_{\beta} (\lambda q.((\true \s q) \s \true) \s \true)$ \\
+		& $\rightarrow_{\beta} ((\true \s \true) \s \true)$ \\
+		& $\rightarrow_{\alpha,\beta} (\lambda b.\truea \s \true)$ \\
+		& $\rightarrow_{\beta} \truea$ \\
+		& $\equiv_{\alpha} TRUE$ \\
+		& \\
+		$TRUE \s\wedge\s FALSE$ & $= (\lambda p.(\lambda q.((p \s q) \s p) \s \false) \s \true)$ \\
+		& $\rightarrow_{\beta} (\lambda q.((\true \s q) \s \true) \s \false)$ \\
+		& $\rightarrow_{\beta} ((\true \s \false) \s \true)$ \\
+		& $\rightarrow_{\alpha,\beta} (\lambda b.\falsea \s \true)$ \\
+		& $\rightarrow_{\beta} \falsea$ \\
+		& $\equiv_{\alpha} FALSE$ \\
+		& \\
+		$FALSE \s\wedge\s TRUE$ & $= (\lambda p.(\lambda q.((p \s q) \s p) \s \true) \s \false)$ \\
+		& $\rightarrow_{\beta} (\lambda q.((\false \s q) \s \false) \s \true)$ \\
+		& $\rightarrow_{\beta} ((\false \s \true) \s \false)$ \\
+		& $\rightarrow_{\beta} (\lambda b.b \s \false)$ \\
+		& $\rightarrow_{\beta} \false$ \\
+		& $\equiv_{\alpha} FALSE$ \\
+		& \\
+		$FALSE \s\wedge\s FALSE$ & $= (\lambda p.(\lambda q.((p \s q) \s p) \s \false) \s \false)$ \\
+		& $\rightarrow_{\beta} (\lambda q.((\false \s q) \s \false) \s \false)$ \\
+		& $\rightarrow_{\beta} ((\false \s \false) \s \false)$ \\
+		& $\rightarrow_{\beta} (\lambda b.b \s \false)$ \\
+		& $\rightarrow_{\beta} \false$ \\
+		& $\equiv_{\alpha} FALSE$ \\
+	\end{tabular}
+\end{table}
+
+\section{Assignment 5}
+
+See appendix \ref{appendix:ass5} (file \emph{ass5.ml}) for my implementation
+of the functions \texttt{isLeapYear}, \texttt{date2str}, \texttt{digitRoot}
+and \texttt{isPalindrome}.
+
+\pagebreak
+
+\appendix
+
+\section{ass5.ml}
+\label{appendix:ass5}
+\lstinputlisting{ass5.ml}
+
+\end{document}