funcprog: Added missing week 2, assignment 4 to repository.

parent 3647b016
TEXFLAGS := -halt-on-error -interaction=nonstopmode -file-line-error
all: ass4.pdf
clean:
rm *.out *.toc *.aux *.log *.pdf
%.pdf: %.tex
pdflatex $(TEXFLAGS) $< | grep -i ".*:[0-9]*:.*\|warning" || true
\documentclass[10pt,a4paper]{article}
\usepackage[english]{babel}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,hyperref,graphicx,booktabs,float}
% Paragraph indentation
\setlength{\parindent}{0pt}
\setlength{\parskip}{1ex plus 0.5ex minus 0.2ex}
\title{Functional programming: week 2, assignment 4}
\author{Sander Mathijs van Veen (6167969; smvv@kompiler.org)}
\begin{document}
\maketitle
\tableofcontents
\newcommand{\s}{\hspace{.3em}}
\newcommand{\la}{\lambda a}
\newcommand{\lb}{\lambda b}
\newcommand{\lp}{\lambda p}
\newcommand{\laq}{\lambda q}
\newcommand{\lu}{\lambda u}
\newcommand{\lv}{\lambda v}
\newcommand{\lx}{\lambda x}
\newcommand{\ly}{\lambda y}
\newcommand{\tb}[1]{\textbf{#1}}
\newcommand{\ra}{\rightarrow_\alpha}
\newcommand{\rb}{\rightarrow_\beta}
\newcommand{\ea}{\equiv_\alpha}
\newcommand{\true}{\la.\lb.a}
\newcommand{\false}{\la.\lb.b}
\newcommand{\truea}{\lu.\lv.u}
\newcommand{\falsea}{\lu.\lv.v}
\section{Negation}
\label{sec:Negation}
Negation inverts the value of a boolean: \texttt{true} becomes \texttt{false},
and \texttt{false} becomes \texttt{true}. In lambda calculi, negation can be
expressed as the $\lambda$-term $\neg x = \lb.\lx.\ly.((b \s y) \s x)$. By
applying $\alpha$-conversions and $\beta$-reductions, we can prove this
$\lambda$-term. First, $\neg \tb{true} \equiv \tb{false}$:
\begin{align*}
\neg \tb{true} & = (\lb.\lx.\ly.((b \s y) \s x) \s \la.\lb.a) \\
& \rb \lx.\ly.((\la.\lb.a \s y) \s x) \\
& \rb \lx.\ly.(\lb.y \s x) \\
& \rb \lx.\ly.y \\
& \ea \tb{false}
\end{align*}
And now $\neg \tb{false} \equiv \tb{true}$:
\begin{align*}
\neg \tb{true} & = (\lb.\lx.\ly.((b \s y) \s x) \s \la.\lb.b) \\
& \rb \lx.\ly.((\la.\lb.b \s y) \s x) \\
& \rb \lx.\ly.(\lb.b \s x) \\
& \rb \lx.\ly.x \\
& \ea \tb{false}
\end{align*}
\pagebreak
\section{Disjunction}
\label{sec:Disjunction}
Disjunction results in \tb{true} whenever one or more of its operands are
\tb{true}. Thus, only iff all operands are \tb{false}, the disjunction will
return \tb{false}.
\begin{align*}
\tb{true} \s\vee\s \tb{true} & = (\lp.(\laq.((p \s p) \s q) \s \true) \s \true) \\
& \rb (\laq.((\true \s \true) \s q) \s \true) \\
& \rb ((\true \s \true) \s \true) \\
& \ra ((\true \s \truea) \s \true) \\
& \rb (\lb.\truea \s \true) \\
& \rb \truea \\
& \ea \tb{true} \\
\end{align*}
\begin{align*}
\tb{true} \s\vee\s \tb{false} & = (\lp.(\laq.((p \s p) \s q) \s \false) \s \true) \\
& \rb (\laq.((\true \s \true) \s q) \s \false) \\
& \rb ((\true \s \true) \s \false) \\
& \ra ((\true \s \truea) \s \false) \\
& \rb (\lb.\truea \s \false) \\
& \rb \truea \\
& \ea \tb{true} \\
\end{align*}
\begin{align*}
\tb{false} \s\vee\s \tb{true} & = (\lp.(\laq.((p \s p) \s q) \s \true) \s \false) \\
& \rb (\laq.((\false \s \false) \s q) \s \true) \\
& \rb ((\false \s \false) \s \true) \\
& \rb (\lb.b \s \true) \\
& \rb \true \\
& \ea \tb{true} \\
\end{align*}
\begin{align*}
\tb{false} \s\vee\s \tb{false} & = (\lp.(\laq.((p \s p) \s q) \s \false) \s \false) \\
& \rb (\laq.((\false \s \false) \s q) \s \false) \\
& \rb ((\false \s \false) \s \false) \\
& \rb (\lb.b \s \false) \\
& \rb \false \\
& \ea \tb{false} \\
\end{align*}
\pagebreak
\section{Conjunction}
\label{sec:Conjunction}
Conjunction results in \tb{true} whenever all of its operands are \tb{true}.
Thus, only iff one or more of operands are \tb{false}, the disjunction will
return \tb{false}.
\begin{align*}
\tb{true} \s\wedge\s \tb{true} & = (\lp.(\laq.((p \s q) \s p) \s \true) \s \true) \\
& \rb (\laq.((\true \s q) \s \true) \s \true) \\
& \rb ((\true \s \true) \s \true) \\
& \ra ((\true \s \truea) \s \true) \\
& \rb (\lb.\truea \s \true) \\
& \rb \truea \\
& \ea \tb{true} \\
\end{align*}
\begin{align*}
\tb{true} \s\wedge\s \tb{false} & = (\lp.(\laq.((p \s q) \s p) \s \false) \s \true) \\
& \rb (\laq.((\true \s q) \s \true) \s \false) \\
& \rb ((\true \s \false) \s \true) \\
& \ra ((\true \s \falsea) \s \true) \\
& \rb (\lb.\falsea \s \true) \\
& \rb \falsea \\
& \ea \tb{false} \\
\end{align*}
\begin{align*}
\tb{false} \s\wedge\s \tb{true} & = (\lp.(\laq.((p \s q) \s p) \s \true) \s \false) \\
& \rb (\laq.((\false \s q) \s \false) \s \true) \\
& \rb ((\false \s \true) \s \false) \\
& \rb (\lb.b \s \false) \\
& \rb \false \\
& \ea \tb{false} \\
\end{align*}
\begin{align*}
\tb{false} \s\wedge\s \tb{false} & = (\lp.(\laq.((p \s q) \s p) \s \false) \s \false) \\
& \rb (\laq.((\false \s q) \s \false) \s \false) \\
& \rb ((\false \s \false) \s \false) \\
& \rb (\lb.b \s \false) \\
& \rb \false \\
& \ea \tb{false} \\
\end{align*}
\end{document}
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment