% -*- mode: LaTeX; compile-command: "mk" -*-
\documentclass{tufte-handout}
%include polycode.fmt
% \arrayhs
% \usepackage[stable]{footmisc} % for putting footnotes in section headings
\usepackage{../../hshw}
\usepackage{mathpartir}
\title{\thecourse\ problem set 2}
\date{\small Revision 1: compiled \today\ at \currenttime}
\author{Due Tuesday 2 February, 2016}
\begin{document}
\maketitle
\section{Trees}
\begin{marginfigure}[6em]
\begin{center}
\begin{diagram}[width=75]
import TreeDia
dia = vcat' (with & sep .~ 2)
[ subtree
, text' 4 "="
, square 1.5
, text' 3 "or"
, treeDef
]
# frame 0.5
\end{diagram}
\end{center}
\caption{Definition of a binary tree $T$} \label{fig:binary-tree-defn}
\end{marginfigure}
\begin{marginfigure}
\begin{center}
\begin{diagram}[width=75]
import TreeDia
import Diagrams.TwoD.Layout.Tree
import Data.Maybe (fromJust)
import Diagrams.Prelude hiding (Empty)
t :: BTree Integer
t = BNode 6 (leaf 4) (BNode 0 (BNode 1 (leaf (-3)) Empty) (leaf 15))
exampleTree
= renderTree node (~~)
. fromJust
. symmLayoutBin' (with & slVSep .~ 4 & slHSep .~ 4)
$ t -- $
dia = exampleTree # frame 0.5 # lwO 0.7
\end{diagram}
\end{center}
\caption{An example binary tree} \label{fig:binary-tree-ex}
\end{marginfigure}
For the purposes of this problem set, a \term{binary tree} containing
values of type |a| is defined as being either
\begin{itemize}
\item empty; or
\item a node containing a value of type |a| and (recursively) two
binary trees, referred to as the ``left'' and ``right'' subtrees.
See the illustration in \pref{fig:binary-tree-defn}, and an example
binary tree in \pref{fig:binary-tree-ex}.
\end{itemize}
\exercise Define a recursive, polymorphic algebraic data type |Tree|
which corresponds to the above definition.
\exercise Define a function \[ |incrementTree :: Tree Integer -> Tree
Integer| \] which adds one to every |Integer| contained in a tree.
\exercise Define a function \[ |treeSize :: Tree a -> Integer| \] which
computes the \term{size} of a tree, defined as the number of nodes.
For example, the tree in \pref{fig:binary-tree-ex} has size $6$.
% \exercise Implement an \emph{inorder traversal} with type \[
% |inorder :: Tree -> [Integer]|. \] For example, the inorder
% traversal of the tree in \pref{fig:binary-tree-ex} is $[4,6,-3,1,0,15]$.
\bigskip
\hrule \bigskip
A \term{binary search tree} (BST) is a binary tree of |Integer|s in
which the |Integer| value stored in each node is larger than all the
|Integer| values in its left subtree, and smaller than all the values
in its right subtree. (For the purposes of this problem set, assume
that all the values in a binary search tree must be distinct.) For
example, the binary tree shown in \pref{fig:binary-tree-ex} is not a
BST, but the one in \pref{fig:BST-ex} is.
\begin{marginfigure}
\begin{center}
\begin{diagram}[width=100]
import TreeDia
import Diagrams.TwoD.Layout.Tree
import Data.Maybe (fromJust)
import Diagrams.Prelude hiding (Empty)
t :: BTree Integer
t = BNode 6 (BNode 4 (BNode 1 Empty (leaf 3)) (leaf 5)) (BNode 12 (BNode 8 Empty (leaf 9)) Empty)
exampleTree
= renderTree node (~~)
. fromJust
. symmLayoutBin' (with & slVSep .~ 4 & slHSep .~ 4)
$ t -- $
dia = exampleTree # frame 0.5 # lwO 0.7
\end{diagram}
\end{center}
\caption{An example binary search tree} \label{fig:BST-ex}
\end{marginfigure}
The following problems ask you to implement some basic binary search
tree algorithms. If you don't remember how they work, you can ask me,
or consult a reference such as \citet[Chapter
13]{cormen2001introduction}.
\exercise Implement a function \[ |bstInsert :: Integer -> Tree
Integer -> Tree Integer|. \] Given an integer |i| and a valid BST,
|bstInsert| should produce another valid BST which contains |i|. If
the input BST already contains |i|, it should be returned
unchanged.\footnote{It does not matter what |bstInsert| does when
given an input |Tree| which is not a valid BST. Later in the course
we will talk about ways to use the type system to help enforce
invariants such as this.}
% \exercise Implement a function \[ |bstMember :: Integer -> Tree ->
% Bool| \] which returns |True| if and only if the given integer is
% contained in the given BST.
\exercise Implement
\[ |bstDelete :: Integer -> Tree Integer -> Tree Integer|. \]
When given an integer |i| and a valid BST, it should return another
valid BST containing all the same integers except for
|i|.\footnote{Ideally, this should require only $O(\log n)$
operations and leave the output BST as similar as possible to the
input BST.}
% That is, it
% should satisfy
% \begin{itemize}
% \item |bstMember i (bstDelete i t) == False|
% \item |inorder t \\ [i] == inorder (bstDelete i t)|\footnote{The
% |\\| operator takes two lists as arguments and deletes the
% contents of the second from the first.}
% \end{itemize}
\exercise Write a function \[ |isBST :: Tree Integer -> Bool| \] which
checks whether the given |Tree| is a valid BST.
\exercise \ec Ensure that your |isBST| function runs in $O(n)$ time.
% \exercise \opt |bstMember| leaves a bit to be desired; it only tells
% you \emph{whether} a certain integer occurs in a tree, but not
% \emph{where} in the tree it can be found. Make a better version of
% |bstMember| by filling in the definitions below.
% \begin{spec}
% type Path = ...
% followPath :: Path -> Tree -> Maybe Integer
% followPath ...
% bstMember' :: Integer -> Tree -> Maybe Path
% bstMember' ...
% \end{spec}
\section{Proof trees}
Consider the following Haskell definitions, which encode the simple
proof system we considered as a first example in class, with only
propositional variables. For example, a rule of this system might
look like
\[
\inferrule{A \\ B}{C}.
\]
Since everything is a tree, we can easily encode these proof trees as
values of an algebraic data type in Haskell.
\marginnote{These definitions are available in |Proof.hs|. If you
download |Proof.hs| and put it in the same folder as your |.hs| or
|.lhs| file, you can add |import Proof| at the top of your |.hs|
file in order to make use of the types it defines.}
\marginnote[1in]{Note that the |type| keyword creates a \emph{type
synonym}, \ie\ |Prop| and |String| can now be used completely
interchangeably (and similarly for |System| and |[Rule]|).}
\begin{spec}
-- Prop represents arbitrary propositional variables,
-- like A, B, C in the example above
type Prop = String
-- An inference rule is a list of premises and a conclusion.
data Rule where
R :: [Prop] -> Prop -> Rule
-- A rule system is a list of rules.
type System = [Rule]
-- A proof is a tree where each node contains a rule and
-- a list of proofs of the rule's premises.
data Proof where
PNode :: Rule -> [Proof] -> Proof
\end{spec}
\exercise Write a function
\[ |checkProof :: Proof -> Prop -> Bool|, \]
which, given a purported proof and a proposition, checks whether the
given proof is actually a valid proof of the given proposition. (A
proof might not be valid because, \eg, the final conclusion is not the
requested proposition, or because some node contains proofs whose
conclusions do not match the stated premises of its rule.) You may
assume that in a valid proof node, the premises of the rule match up
with the given proofs \emph{in order}, that is, the first proof should
be a proof of the first premise of the rule, the second proof of the
second premise, and so on (this makes your job a bit easier, and is
a not unreasonable requirement).
\exercise \ec Write a function \[ |findProof :: System -> Prop -> Maybe
Proof|. \] Given a rule system and a goal proposition, it should
either return a valid proof of the proposition using only rules from
the system, or |Nothing| if there is no valid proof.
\section{Propositional logic}
\exercise Give formal derivations (proof trees) for each of the
following judgments. \marginnote{You will probably want to draw these
by hand and then turn them in on paper. If you are a really
hard-core \LaTeX\ user and want to typeset them, try the
\texttt{mathpartir} package, available from
\url{http://cristal.inria.fr/~remy/latex/mathpartir.sty}, with
documentation at
\url{http://cristal.inria.fr/~remy/latex/mathpartir.html}. You might
also want to use the \texttt{lscape} or \texttt{pdflscape} packages
to put individual pages in landscape mode, since the proof trees
tend to be much wider than they are tall.}
\begin{enumerate}[label=(\alph*)]
\item $(P \implies (Q \implies R)) \vdash (Q \implies (P
\implies R))$
\item $((P \land Q) \implies R) \vdash (P \implies (Q
\implies R))$
\item $((P \lor Q) \implies R) \vdash ((P \implies R) \land
(Q \implies R))$
\end{enumerate}
\exercise \opt This is just for fun. Take each of the above three
judgments and replace $\land$ by multiplication, $\lor$ by addition,
and replace $\implies$ by (backwards) exponentiation, \ie replace $P
\implies Q$ by $Q^P$. What do you notice?
\exercise We did not talk about negation $(\lnot P)$ in class, since
it turns out that for our purposes, it is possible to encode negation
using other logical connectives. In particular, consider defining \[
\lnot P := (P \implies \bot). \]
Using this definition, for each of the following judgments, either
give a formal derivation (\ie\ a proof tree), or explain why it is not
possible.
\begin{enumerate}[label=(\alph*)]
\item $\vdash P \land \lnot P \implies \bot$
\item $\vdash P \lor \lnot P$
\item $\vdash P \implies \lnot (\lnot P)$
\item $\vdash \lnot (\lnot P) \implies P$
\item $\lnot (P \lor Q) \implies (\lnot P \land \lnot Q)$
\end{enumerate}
\bibliographystyle{plainnat}
\bibliography{ADTs-proof}
\end{document}