% ===============================================================
% ===============================================================
% ===============================================================
\begin{frame}
\titleslide{Recursion}
\end{frame}

\begin{frame}
\frametitle{Example of Recursion}

For simplicity assume no parameters 
(we can simulate them using global variables)

\begin{minipage}{4cm}
\lstinputlisting{recur1.scala}
\end{minipage}
\begin{minipage}{4cm}
\[\begin{array}{l}
E(r_f) = \\
\Delta_{\pset{x>0}} \circ \big( \\
\ \ (\Delta_{x \% 2 = 0} \circ \\
\ \ \rho(x=x/2) \circ \\
\ \ r_f \circ \\
\ \ \rho(y = y * 2)) \\
\cup \\
\ \ (\Delta_{x \% 2 \ne 0} \circ \\
\ \ \rho(x = x - 1) \circ \\
\ \ \rho(y = y + x) \circ \\
\ \ r_f ) \\
\big) \cup \Delta_{\pset{x \le 0}}
\end{array}\]
\end{minipage}

Assume recursive function call denotes some relation $r_f$

Need to find relation $r_f$ such that $r_f = E(r_f)$
\end{frame}

\begin{frame}
\frametitle{Simpler Example of Recursion}

\begin{minipage}{4cm}
\lstinputlisting{recur2.scala}
\end{minipage}
\begin{minipage}{4cm}
\[
E(r) = \begin{array}[t]{l}
(\Delta_{\pset{x>0}} \circ \big( \\
\ \ \rho(x=x-1) \circ \\
\ \  r \ \circ \\
\ \ \rho(y=y+2)) \\
\big) \cup \Delta_{\pset{x \le 0}}
\end{array}
\]
\end{minipage}

\ \\

\pause
What is $E(\emptyset)$?

\pause
What is $E(E(\emptyset))$?

\pause $E^k(\emptyset)$?

\end{frame}

\begin{frame}
\frametitle{Omega Monotonicity}

The law
\[
   E(\bigcup_{i \in I} r_i) = \bigcup_{i \in I} E(r_i)
\]
holds when $E$ is built from constant relations, $r$, $\circ$ and $\cup$ and if

$I$ is a set of natural numbers
and $r_i$ is an increasing sequence:
$r_1 \subseteq r_2 \subseteq r_3 \subseteq \ldots$

\

In other words: $E$ is $\omega$-monotonic

\

Hence, its least fixpoint is
\[
  \bigcup_{k \ge 0} E^k(\emptyset)
\]

\end{frame}


\begin{frame}
\frametitle{Define Meaning of Recursion as the Least Fixpoint}

A recursive program is a recursive definition of a relation $E(r)=r$

\ \\

We define the intended meaning as $s = \bigcup_{i \ge 0} E(\emptyset)$, which satisfies
$E(s)=s$ and also is the least among all relations $r$ such that $E(r) \subseteq r$ \\
(therefore, also the least among $r$ for which $E(r)=r$)

\ \\

We picked \textbf{least} fixpoint, so if the execution cannot terminate
on a state $x$, then there is no $x'$ such that $(x,x') \in s$.

This model is simple (just relations on states) though it has some 
limitations: let $q$ be a program that \emph{never} terminates and $c$ one that always does:
\begin{itemize}
\item $\rho(q) = \emptyset$ and 
$\rho(\ndchoice{c}{q}) = \rho(c) \cup \emptyset = \rho(c)$  \\
(program that sometimes does not terminate has the same meaning as $c$)
\item $\rho(q) = \rho(\Delta_{\emptyset})$ (assume(false)), so the
absence of results due to path conditions and infinite loop are represented in the same way
\end{itemize}

\pause
Alternative: error states for non-termination (we will not pursue this approach)
\end{frame}

\begin{frame}
\frametitle{Procedure Meaning is the Least Relation}

\begin{minipage}{4cm}
\lstinputlisting{recur2.scala}
\end{minipage}
\begin{minipage}{4cm}
\[
E(r_f) = \begin{array}[t]{l}
(\Delta_{\pset{x>0}} \circ \big( \\
\ \ \rho(x=x-1) \circ \\
\ \  r_f \circ \\
\ \ \rho(y=y+2)) \\
\big) \cup \Delta_{\pset{x \le 0}}
\end{array}
\]
\end{minipage}

What does it mean that $E(r) \subseteq r$ ?

\pause

Plugging $r$ instead of the recursive call
results in something that conforms to $r$

\ \\

Justifies modular reasoning for recursive functions

\ \\

To prove that recursive procedure with body $E$ satisfies
specification $r$, show
\begin{itemize}
\item $E(r) \subseteq r$
\item Because procedure meaning $s$ is least, conclude $s \subseteq r$
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Proving that recursive function meets specification}

Prove that if $s$ is the relation denoting the recursive function below,
then 
\[
    ((x,y),(x',y')) \in s \rightarrow y' \ge y
\]

\ \\

\begin{minipage}{4cm}
\lstinputlisting{recur2.scala}
\end{minipage}
\begin{minipage}{4cm}
\[
E(r_f) = \begin{array}[t]{l}
(\Delta_{\pset{x>0}} \circ \big( \\
\ \ \rho(x=x-1) \circ \\
\ \  r_f \circ \\
\ \ \rho(y=y+2)) \\
\big) \cup \Delta_{\pset{x \le 0}}
\end{array}
\]
\end{minipage}

\ \\
\pause Solution: let specification relation be
$q = \{((x,y),(x',y')) \mid y' \ge y \}$


\pause Prove $E(q) \subseteq q$ - given by a quantifier-free formula

\end{frame}

\begin{frame}
\frametitle{Formula for Checking Specification} 

\lstinputlisting{recur2.scala}
Specification: $q = \{((x,y),(x',y')) \mid \alert{y' \ge y} \}$

Formula to prove, generated by representing $E(q) \subseteq q$:
\[\begin{array}{l}
   \big(
     (x > 0 \land x_1 = x - 1 \land y_1 = y \land \alert{y_2 \ge y_1} \land y' = y_2 + 2) 
\\
\lor (\lnot(x > 0) \land x' = x \land y' = y) \big)
    \ \rightarrow \ \alert{y' \ge y}
\end{array}
\]
\begin{itemize}
\item Because $q$ appears as $E(q)$ and $q$, the condition appears twice. 
\item Proving $f \subseteq q$ by $E(q) \subseteq q$ is always sound, whether or not function $f$ terminates; the meaning of $f$ talks only about
properties of terminating executions (relations can be partial)
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Multiple Procedures: Functions on Pairs of Relations}

Two mutually recursive procedures
$r_1 = E_1(r_1,r_2), \ \ \  r_2 = E_2(r_1,r_2)$

We extend the approach to work on pairs of relations:
\[
    (r_1,r_2) = (E_1(r_1,r_2), E_2(r_1,r_2))
\]
Define $\bar E(r_1,r_2) = (E_1(r_1,r_2), E_2(r_1,r_2))$, let $\bar r = (r_1,r_2)$.
We define semantics of procedures as the least solution of
\[
    \bar E(\bar r) = \bar r
\]
where $(r_1,r_2) \sqsubseteq (r'_1, r'_2)$ means
$r_1 \subseteq r'_1$ and $r_2 \subseteq r'_2$

Even though pairs of relations are not sets but pairs of sets, we can define
set-like operations on them, e.g.
\[
     (r_1,r_2) \sqcup (r'_1, r'_2) = (r_1 \cup r'_1,\ r_2 \cup r'_2)
\]
The entire theory works when we have a partial order $\sqsubseteq$ with
some ``good properties''.
(\textbf{Lattice} elements are a generalization of sets.)

\end{frame}

\begin{frame}
  \frametitle{Multiple Procedures: Least Fixedpoint and Consequences}

Two mutually recursive procedures
$r_1 = E_1(r_1,r_2), \ \ \  r_2 = E_2(r_1,r_2)$

For $E(r_1,r_2) = (E_1(r_1, r_2), E_2(r_1, r_2))$, semantics is 
\[
   (s_1,s_2) = \bigsqcup_{i \ge 0} \bar E^i(\emptyset, \emptyset)
\]
It follows that for any $c_1,c_2$ if
\[
E_1(c_1,c_2) \subseteq c_1   \ \mbox{ and } \
E_2(c_1,c_2) \subseteq c_2 
\]
then $s_1 \subseteq c_1$ and $s_2 \subseteq c_2$.

\ \\

\textbf{Induction-like principle:}
To prove that mutually recursive relations satisfy
two contracts, prove those contracts for the relation body definitions in which
recursive calls are replaced by those contracts.
  
\end{frame}

\begin{frame}
  \frametitle{Replacing Calls by Contracts: Example}

\small
  
\begin{minipage}{6cm}
  \lstinputlisting{mutualrec1.scala}
\end{minipage}
\begin{minipage}{4cm}
  \lstinputlisting{mutualrec2.scala}
\end{minipage}

\pause Reduces to checking these two non-recursive procedures:

\begin{minipage}{6cm}
  \lstinputlisting{mutualrec1h.scala}
\end{minipage}
\begin{minipage}{4cm}
  \lstinputlisting{mutualrec2h.scala}
\end{minipage}

\end{frame}
