\documentclass[11pt]{article}

\renewcommand{\thepage}{}

\input{pset-defs}

\begin{document}
\begin{center}\large\bf
  CS 516---Software Foundations via Formal Languages---Spring 2022
\end{center}
\begin{center}\Large\bf
Problem Set 1
\end{center}
\begin{center}\large\bf
Due by 5pm on Friday, February 4 \\
Submission via Gradescope
\end{center}

\section*{Problem 1 (25 points)}

Suppose $X$ is a set, and $x\in X$.  What are the elements of
$\emptyset\fun X$, $X\fun\emptyset$, $\{x\}\fun X$ and $X\fun\{x\}$?
Prove that your answers are correct.

\section*{Problem 2 (25 points)}

Use mathematical induction (Theorem~1.2.1) to prove that, for all
$n\in\nats$, if $n\geq 4$, then $2^n < n!$. Here $n!$ is
the factorial of $n$, defined recursively by:
\begin{enumerate}[\quad(1)]
\item $0! = 1$;

\item $(n + 1)! = (n + 1) * n!$, for all $n\in\nats$.
\end{enumerate}

\section*{Problem 3 (25 points)}

Use strong induction (Theorem~1.2.4) to prove that, for all
$n\in\nats$, if $n\geq 1$, then there are $i,j\in\nats$ such that
$n=2^i(2j + 1)$.

\section*{Problem 4 (25 points)}

Define $f\in\ints\fun\ints$ by:
\begin{displaymath}
f\,n =
\left\{ \begin{array}{ll}
0 & \eqtxtr{if} n = 0 , \\
1 - n & \eqtxtr{if} n\geq 1, \\
-n - 1 & \eqtxtr{if} n\leq -1 .
\end{array} \right.
\end{displaymath}
Given $n\in\ints$, define the $l$-th \emph{iteration of} $f$ \emph{on}
$n$ ($f^l(n)\in\ints$), for $l\in\nats$, by recursion:
\begin{align*}
f^0(n) &= n , \\
f^{l + 1}(n) &= f(f^l(n)) .
\end{align*}
Then we have that:
\begin{enumerate}[\quad(1)]
\item For all $n\in\ints$, $f^1(n) = f\,n$.

\item For all $n\in\ints$ and $l, m\in\nats$, $f^{l+m}(n)=f^m(f^l(n))$.
\end{enumerate}

\bigskip\noindent Let $R$ be the relation on $\ints$ defined by: for
all $n,m\in\ints$, $n\mathrel{R}m$ iff $|n|<|m|$. Here $|n|$ is the
absolute value of $n$: $n$, if $n\geq 0$; and $-n$, if $n\leq -1$.  We
have the following properties of absolute value, where $n,m\in\ints$:
\begin{enumerate}[\quad(1)]
\item if $n\leq m$, then $|n - m| = m - n$;
\item if $m\leq n$, then $|n - m| = n - m$.
\end{enumerate}
Because $|\cdot|\in\ints\fun\nats$ and $<$ is well-founded on $\nats$,
Proposition~1.2.10 tells us that $R$ is well-founded on $\ints$.

\bigskip\noindent Use well-founded induction on $R$ (Theorem~1.2.8) to
show that, for all $n\in\ints$, there is an $l\in\nats$ such that
$f^l(n) = 0$.
\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: