text:
\documentclass{beamer}
%
% Choose how your presentation looks.
%
% For more themes, color themes and font themes, see:
% http://deic.uab.es/~iblanes/beamer_gallery/index_by_theme.html
%
\mode<presentation>
{
  \usetheme{default}      % or try Darmstadt, Madrid, Warsaw, ...
  \usecolortheme{default} % or try albatross, beaver, crane, ...
  \usefonttheme{default}  % or try serif, structurebold, ...
  \setbeamertemplate{navigation symbols}{}
  \setbeamertemplate{caption}[numbered]
  \setbeamertemplate{footline}[frame number]
  \setbeamertemplate{itemize items}[circle]
  \setbeamertemplate{theorems}[numbered]
  \setbeamercolor*{structure}{bg=white,fg=blue}
  \setbeamerfont{block title}{size=\normalsize}
}

% \newtheorem{proposition}[theorem]{Proposition}
% \theoremstyle{definition}
% \newtheorem{algorithm}[theorem]{Algorithm}
% \newtheorem{idea}[theorem]{Idea}

\usepackage[english]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{aligned-overset}
\usepackage{alltt}
\usepackage{amsmath}
\usepackage{csquotes}
% \usepackage{multicol}
% \usepackage{stmaryrd}
\usepackage{tabularx}

% \renewcommand\tabularxcolumn[1]{m{#1}}
% \newcolumntype{R}{>{\raggedleft\arraybackslash}X}=

\newcommand\logeq{\mathrel{\vcentcolon\Leftrightarrow}}
\def\code#1{\texttt{\frenchspacing#1}}
\def\padding{\vspace{0.5cm}}
\def\spadding{\vspace{0.25cm}}
\def\b{\textcolor{blue}}
\def\r{\textcolor{red}}
\def\g#1{{\usebeamercolor[fg]{block title example}{#1}}}

% fix for \pause in align
\makeatletter
\let\save@measuring@true\measuring@true
\def\measuring@true{%
  \save@measuring@true
  \def\beamer@sortzero##1{\beamer@ifnextcharospec{\beamer@sortzeroread{##1}}{}}%
  \def\beamer@sortzeroread##1<##2>{}%
  \def\beamer@finalnospec{}%
}
\makeatother

\title[Theoretical Computer Science]{Theoretical Computer Science \\ Regular Languages}
\author{Jonas Hübotter}
\date{}

\begin{document}

\begin{frame}
  \titlepage
\end{frame}

\begin{frame}[allowframebreaks]{Outline}
 \tableofcontents[subsubsectionstyle=hide]
\end{frame}
% \AtBeginSection[]
%   {
%      \begin{frame}[allowframebreaks]{Plan}
%      \tableofcontents[currentsection, sectionstyle=show/hide, hideothersubsections]
%      \end{frame}
%   }

\section{Overview}

\begin{frame}{Overview}
    \begin{block}{Representations of regular languages}\pause
        \begin{itemize}
            \item Right-Linear Grammar (RLG)\pause
            \item Deterministic Finite Automaton (DFA)\pause
            \item Nondeterministic Finite Automaton (NFA)\pause
            \item $\epsilon$-NFA\pause
            \item Regular Expression (Regex)
        \end{itemize}
    \end{block}
\end{frame}

\section{Automata}

\subsection{Deterministic Finite Automaton (DFA)}

\begin{frame}{DFA}
    \begin{definition}
        A \b{deterministic finite automaton (DFA)} $M = (Q, \Sigma, \delta, q_0, F)$\pause\ consists of
        \begin{itemize}
            \item a finite set of \b{states} $Q$\pause;
            \item a (finite) \b{alphabet} $\Sigma$\pause;
            \item a total \b{transition function} $\delta: Q \times \Sigma \to Q$\pause;
            \item an \b{initial state} $q_0 \in Q$\pause; and
            \item a set of \b{terminal (accepting) states} $F \subseteq Q$.
        \end{itemize}
    \end{definition}
\end{frame}

\begin{frame}{DFA}
    \begin{definition}
        The \b{induced transition function} $\hat{\delta}$ of a DFA $M$ is defined by\pause
        \begin{align*}
            \hat{\delta}(q, \epsilon) &= q\pause\\
            \hat{\delta}(q, aw) &= \hat{\delta}(\delta(q,a),w), a \in \Sigma, w \in \Sigma^*.
        \end{align*}\pause
        The language \b{accepted} by $M$ is $L(M) = \{w \in \Sigma^* \mid \hat{\delta}(q_0, w) \in F\}$.
    \end{definition}
\end{frame}

\subsection{Nondeterministic Finite Automaton (NFA)}

\begin{frame}{NFA}
    \begin{definition}
        A \b{nondeterministic finite automaton (NFA)} $N = (Q, \Sigma, \delta, q_0, F)$\pause\ consists of
        \begin{itemize}
            \item $Q, \Sigma, q_0, F$ as defined for DFAs\pause; and
            \item a (partial) \b{transition function} $\delta: Q \times \Sigma \to 2^Q$.
        \end{itemize}
    \end{definition}
\end{frame}

\begin{frame}{NFA}
    \begin{definition}
        The \b{induced transition function} $\hat{\bar{\delta}}$ of a NFA $N$ is defined analogously to $\hat{\delta}$ where\pause
        \begin{align*}
            \bar{\delta}: 2^Q \times \Sigma \to 2^Q, (S, a) \mapsto \bigcup_{q \in S} \delta(q, a).
        \end{align*}\pause
        The language \b{accepted} by $N$ is $L(N) = \{w \in \Sigma^* \mid \hat{\bar{\delta}}(\{q_0\}, w) \cap F \neq \emptyset\}$.
    \end{definition}
\end{frame}

\subsection{NFA $\to$ DFA (determinization)}

\begin{frame}{NFA $\to$ DFA (determinization)}
    \begin{block}{Idea}
        Interpret every reachable subset $S \subseteq 2^Q$ in the NFA $N$ as its own state in the new DFA $M$.\pause\par
        Every state $S$ of $M$ where $S \cap F_N \neq \emptyset$ is an accepting state of $M$.
    \end{block}\pause\padding
    \r{Worst-case exponential growth!}
\end{frame}

\subsection{$\epsilon$-NFA}

\begin{frame}{$\epsilon$-NFA}
    \begin{definition}
        An \b{$\epsilon$-NFA} $N = (Q, \Sigma, \delta, q_0, F)$ is an NFA with a special symbol $\epsilon \neg\in \Sigma$ where
        \begin{align*}
            \delta : Q \times (\Sigma \cup \{\epsilon\}) \to 2^Q.
        \end{align*}\pause
        $\epsilon$-transitions can be executed at any time without reading a symbol.
    \end{definition}
\end{frame}

\subsection{$\epsilon$-NFA $\to$ NFA}

\begin{frame}{$\epsilon$-NFA $\to$ NFA}
    \begin{block}{Idea}
        Given $\epsilon$-NFA $N = (Q, \Sigma, \delta, q_0, F)$\pause\ construct NFA $N' = (Q, \Sigma, \delta', q_0, F')$\pause\ where
        \begin{align*}
            \delta' : Q \times \Sigma \to 2^Q : (q, a) \mapsto \bigcup_{i, j \geq 0} \hat{\delta}(\{q\}, \epsilon^i a \epsilon^j)\pause;
        \end{align*}
        if $\epsilon \in L(N)$ then $F' = F \cup \{q_0\}$ else $F' = F$.
    \end{block}
\end{frame}

\subsection{Product-Construction}

\begin{frame}{Product-Construction}
    \begin{block}{Idea}
        Given DFAs $M_1 = (Q_1, \Sigma, \delta_1, s_1, F_1)$ and $M_2 = (Q_2, \Sigma, \delta_2, s_2, F_2)$\pause\ the \b{product automaton} is $M = (Q_1 \times Q_2, \Sigma, \delta, (s_1, s_2), F_1 \times F_2)$\pause\ where
        \begin{align*}
            \delta &: (Q_1 \times Q_2) \times \Sigma \to Q_1 \times Q_2 \pause\\
                   &: ((q_1, q_2), a) \mapsto (\delta_1(q_1, a), \delta_2(q_2, a)).
        \end{align*}\pause\padding
        For the product automaton $L(M) = L(M_1) \cap L(M_2)$ holds.
    \end{block}
\end{frame}

\subsection{Minimal Automaton}

\begin{frame}{Minimal Automaton}
    For any regular language $L$ there exists a DFA $D$ of minimal size such that $L(D) = L$.\pause
    \begin{block}{Algorithm ($\mathcal{O}(|Q|^2)$ for constant $|\Sigma|$)}
        \begin{enumerate}
            \item remove unreachable states from $q_0$\pause
            \item determine equivalent states\pause
            \item merge equivalent states
        \end{enumerate}
    \end{block}
\end{frame}

\begin{frame}{Equivalent States}
    \begin{definition}
        States $p, q \in Q$ are
        \begin{itemize}
            \item \b{equivalent} if $\forall w \in \Sigma^*.\ \hat{\delta}(p, w) \in F \iff \hat{\delta}(q, w) \in F$\pause;
            \item \b{distinguishable} if they are not equivalent.
        \end{itemize}
    \end{definition}\pause
    \begin{columns}
    \column{0.6\textwidth}
        \begin{block}{Algorithm for finding equivalent states}
            Idea: mark distinguishable states step-by-step.\pause
            \begin{enumerate}
                \item mark all pairs $p, q \in Q$ if $p \in F$ and $q \in Q \setminus F$\pause
                \item while $\exists \text{ unmarked } \{p, q\} \text{ and } \exists a \in \Sigma, \text{ if } \{\delta(p, a), \delta(q, a)\} \text{ is marked, mark } \{p, q\}$
            \end{enumerate}
        \end{block}
    \column{0.4\textwidth}
        \centering
        \includegraphics[width=\textwidth]{materials/images/equivalent_states.png}
    \end{columns}
\end{frame}

\subsection{Interlude: Equivalence Relations}

\begin{frame}{Interlude: Equivalence Relations}
    \begin{definition}
        A relation $\sim\ \subseteq A \times A$ is an \b{equivalence relation} if\pause
        \begin{itemize}
            \item $\forall a \in A.\ a \sim a.$ (\b{reflexivity})\pause
            \item $\forall a, b \in A.\ a \sim b \implies b \sim a.$ (\b{symmetry})\pause\ and
            \item $\forall a, b, c \in A.\ a \sim b \land b \sim c \implies a \sim c.$ (\b{transitivity})
        \end{itemize}\pause\par\padding
        $[a]_\sim = \{b \mid a \sim b\}$ is called the \b{equivalence class} of $a$ under $\sim$.\pause\par\padding
        The set of equivalence classes $A/{\sim} = \{[a]_\sim \mid a \in A\}$ is called the \b{quotient set} of $\sim$.
    \end{definition}
\end{frame}

\subsection{Quotient Automaton}

\begin{frame}{Quotient Automaton}
    Observation: the equivalence of states defines an equivalence relation.\pause\par\spadding
    We say $p \equiv_M q$ iff $p$ and $q$ are equivalent states in $M$.\pause\padding
    \begin{definition}
        The collapsed automaton relative to $\equiv_M$ is called \b{quotient automaton}.\pause
        \begin{align*}
            M/{\equiv_M} = (Q/{\equiv_M}, \Sigma, \delta', [q_0]_{\equiv_M}, F/{\equiv_M})
        \end{align*}\pause
        with $\delta'([p]_{\equiv_M}, a) = [\delta(p, a)]_{\equiv_M}$ for $p \in Q, a \in \Sigma$.
    \end{definition}
\end{frame}

\subsection{Canonical Minimal Automaton}

\begin{frame}{Canonical Minimal Automaton}
    \begin{definition}
        The \b{canonical minimal automaton} $M_L$ is a unique minimal automaton for any regular language $L$.\pause
        \begin{align*}
            M_L = (\Sigma^*/{\equiv_L}, \Sigma, \delta_L, [\epsilon]_{\equiv_L}, F_L)
        \end{align*}\pause
        with
        \begin{align*}
            \delta_L([w]_{\equiv_L}, a) &= [wa]_{\equiv_L}\pause \\
            F_L &= \{[w]_{\equiv_L} \mid w \in L\}
        \end{align*}\pause
        It follows that $\hat{\delta}([\epsilon]_{\equiv_L}, w) = [w]_{\equiv_L}$ for $w \in \Sigma^*$,\pause\par
        hence $L(M_L) = L$.
    \end{definition}
\end{frame}

\subsection{Theorem of Mihill-Nerode}

\begin{frame}{Theorem of Mihill-Nerode}
    \begin{theorem}[Theorem of Mihill-Nerode]
        $L \subseteq \Sigma^*$ is regular $\iff$ $\equiv_L$ has finitely many equivalence classes.
    \end{theorem}
\end{frame}

\section{Right-Linear Grammar (RLG)}

\subsection{DFA $\to$ RLG}

\begin{frame}{DFA $\to$ RLG}
    \begin{block}{Idea}
        Given DFA $M = (Q, \Sigma, \delta, q_0, F)$\pause\ define RLG $G = (Q, \Sigma, P, q_0)$\pause\ with productions $P$:\pause
        \begin{itemize}
            \item $(q_1 \to a q_2) \in P$ iff $\delta(q_1, a) = q_2$\pause;
            \item $(q_1 \to a) \in P$ iff $\delta(q_1, a) \in F$\pause; and
            \item $(q_0 \to \epsilon) \in P$ iff $q_0 \in F$.
        \end{itemize}\pause\padding
        Then, $L(G) = L(M)$.
    \end{block}
\end{frame}

\subsection{RLG $\to$ NFA}

\begin{frame}{RLG $\to$ NFA}
    \begin{block}{Idea}
        Given RLG $G = (V, \Sigma, P, S)$ without the production $S \to \epsilon$\pause,\ define the NFA $N = (V \cup \{q_f\}, \Sigma, \delta, S, \{q_f\})$\pause\ with:
        \begin{itemize}
            \item $Y \in \delta(X, a)$ iff $(X \to aY) \in P$\pause; and
            \item $q_f \in \delta(X, a)$ iff $(X \to a) \in P$.
        \end{itemize}\pause\padding
        Then, $L(N) = L(G)$.
    \end{block}
\end{frame}

\section{Regular Expressions}

\subsection{Definition}

\begin{frame}{Regular Expressions}
    \begin{block}{Syntax}
        \begin{itemize}
            \item $\boldsymbol{\emptyset}$ is a regular expression\pause;
            \item $\epsilon$ is a regular expression\pause;
            \item $\forall a \in \Sigma$, $a$ is a regular expression\pause; and
            \item given regular expressions $\alpha, \beta$, the following are regular expressions:\pause
                \begin{itemize}
                    \item $\alpha \beta$ (\b{concatenation})\pause;
                    \item $\alpha | \beta$ (\b{disjunction})\pause; and
                    \item $\alpha^*$ (\b{repetition}).
                \end{itemize}
        \end{itemize}
    \end{block}
\end{frame}

\begin{frame}{Regular Expressions}
    \begin{block}{Semantics}
        \begin{itemize}
            \item $L(\boldsymbol{\emptyset}) = \emptyset$\pause;
            \item $L(\epsilon) = \{\epsilon\}$\pause;
            \item $L(a) = \{a\}$\pause;
            \item $L(\alpha \beta) = L(\alpha) L(\beta)$\pause;
            \item $L(\alpha | \beta) = L(\alpha) \cup L(\beta)$\pause; and
            \item $L(\alpha^*) = L(\alpha)^*$.
        \end{itemize}
    \end{block}
\end{frame}

\subsection{Interlude: Structural Induction}

\begin{frame}{Interlude: Structural Induction}
    To prove a statement $P$ for an object $\gamma$ that is defined inductively, we use \b{structural induction}.\pause\padding

    Let $\gamma$ be defined by base cases $\alpha_1, \dots, \alpha_k$ and inductive cases $\beta_1, \dots, \beta_l$ with assumptions $a_{i1}, \dots, a_{im_i}$ for $i \in \{1, \dots, l\}$.\pause\padding

    To prove $P$ for all $\gamma$, prove:
    \begin{itemize}
        \item $P(\alpha_i)$ for $i \in \{1, \dots, k\}$\pause; and
        \item $P(a_{i1}) \land \dots \land P(a_{im_i}) \implies P(\beta_i)$ for $i \in \{1, \dots, l\}$.
    \end{itemize}
\end{frame}

\subsection{Regex $\to$ $\epsilon$-NFA (Kleene)}

\begin{frame}{Regex $\to$ $\epsilon$-NFA (Kleene)}
    \begin{columns}
        \column{0.1\textwidth}
        $\boldsymbol{\emptyset}$
        \column{0.6\textwidth}
        \includegraphics[width=2cm]{materials/images/regex_to_nfa_emptyset.png}
    \end{columns}\pause
    \begin{columns}
        \column{0.1\textwidth}
        $\epsilon$
        \column{0.6\textwidth}
        \includegraphics[width=2cm]{materials/images/regex_to_nfa_epsilon.png}
    \end{columns}\pause
    \begin{columns}
        \column{0.1\textwidth}
        $a$
        \column{0.6\textwidth}
        \includegraphics[width=3.5cm]{materials/images/regex_to_nfa_symbol.png}
    \end{columns}\pause
    \begin{columns}
        \column{0.1\textwidth}
        $\alpha \beta$
        \column{0.6\textwidth}
        \includegraphics[width=8cm]{materials/images/regex_to_nfa_concatenation.png}
    \end{columns}
\end{frame}

\begin{frame}{Regex $\to$ $\epsilon$-NFA (Kleene)}
    \begin{columns}
        \column{0.1\textwidth}
        $\alpha \mid \beta$
        \column{0.6\textwidth}
        \includegraphics[width=5cm]{materials/images/regex_to_nfa_alternative.png}
    \end{columns}\pause
    \begin{columns}
        \column{0.1\textwidth}
        $\alpha^*$
        \column{0.6\textwidth}
        \includegraphics[width=5.5cm]{materials/images/regex_to_nfa_repetition.png}
    \end{columns}
\end{frame}

\subsection{DFA/NFA $\to$ Regex (Kleene)}

\begin{frame}{DFA/NFA $\to$ Regex (Kleene)}
    Given $M = (Q, \Sigma, \delta, q_1, F)$ with $Q = \{q_1, \dots, q_n\}$ define
    \begin{align*}
        R_{ij}^k = \{w \in \Sigma^* \mid &\text{ input } w \text{ transitions from } q_i \text{ to } q_j \\
        &\text{ and all states in between have an index  } \leq k\}.
    \end{align*}\pause
    Idea: for all $i, j \in [n]$ and $k \in [n]_0$\par
    a regex $\alpha_{ij}^k$ can be constructed with $L(\alpha_{ij}^k) = R_{ij}^k$.
\end{frame}

\begin{frame}{DFA/NFA $\to$ Regex (Kleene)}
    Induction over $k$.
    \begin{itemize}
        \item $k = 0$:\pause\ Let
            \begin{align*}
                R_{ij}^0 &= \begin{cases}
                    \{a \in \Sigma \mid \delta(q_i, a) = q_j\} & i \neq j \\
                    \{a \in \Sigma \mid \delta(q_i, a) = q_j\} \cup \{\epsilon\} & i = j
                \end{cases}\pause \\
                \alpha_{ij}^0 &= \begin{cases}
                    a_1 \mid \dots \mid a_l & i \neq j \\
                    a_1 \mid \dots \mid a_l \mid \epsilon & i = j
                \end{cases}
            \end{align*}\pause
            where $\{a_1, \dots, a_l\} = \{a \in \Sigma \mid \delta(q_i, a) = q_j\}$.\pause
        \item $k \implies k + 1$:\pause
            \begin{align*}
                R_{ij}^{k+1} &= R_{ij}^k\pause \cup \r{R_{i(k+1)}^k (R_{(k+1)(k+1)}^k)^* R_{(k+1)j}^k} \\
                \onslide<8->{\alpha_{ij}^{k+1}} &\onslide<8->{= a_{ij}^k \mid a_{i(k+1)}^k (a_{(k+1)(k+1)}^k)^* a_{(k+1)j}^k.
                }
            \end{align*}
            \r{New paths using $q_{k+1}$ in terms of the already built subpaths.}
    \end{itemize}
    \onslide<9->{We now have, $L(M) = L(\alpha_{1i_1}^n \mid \dots \mid \alpha_{1i_r}^n)$ where $\{q_{i_1}, \dots, q_{i_r}\} = F$.}
\end{frame}

\subsection{Arden's Lemma}

\begin{frame}{Arden's Lemma}
    \begin{theorem}[Arden's Lemma for regular languages]
        Let $A, B, X$ be regular languages and $\epsilon \not\in A$, then:
        \begin{align*}
            X = AX \cup B \implies X = A^* B.
        \end{align*}
    \end{theorem}\pause
    \begin{theorem}[Arden's Lemma for regular expressions]
        Let $\alpha, \beta, X$ be regular expressions and $\epsilon \not\in L(\alpha)$, then:
        \begin{align*}
            X = \alpha X \mid \beta \implies X = \alpha^* \beta.
        \end{align*}
    \end{theorem}
\end{frame}

\section{Closure Properties}

\begin{frame}{Closure Properties}
    \begin{theorem}
        Given the regular languages $R, R_1, R_2$, then the following are also regular languages:\pause
        \begin{itemize}
            \item $R_1 R_2$\pause;
            \item $R_1 \cup R_2$\pause;
            \item $R^*$\pause;
            \item $\bar{R}$\pause;
            \item $R_1 \cap R_2$\pause; and
            \item $R_1 \setminus R_2$.
        \end{itemize}
    \end{theorem}
\end{frame}

\section{Pumping Lemma}

\begin{frame}{Pumping Lemma}
    \begin{lemma}[Pumping Lemma for regular languages]
        Let $R \subseteq \Sigma^*$ be regular.\pause\ Then there exists some $n > 0$ such that every $z \in R$ with $|z| \geq n$ can be decomposed into $z = uvw$\pause\ such that
        \begin{itemize}
            \item $v \neq \epsilon$\pause;
            \item $|uv| \leq n$\pause; and
            \item $\forall i \geq 0.\ uv^iw \in R$.
        \end{itemize}
    \end{lemma}\pause
    \r{A necessary condition for regular languages.}
\end{frame}

\begin{frame}{Pumping Lemma}
    \begin{example}[proof structure]
        Assume $L$ is regular.\par
        Let $n > 0$ be a Pumping Lemma number.\pause\par
        Choose $z \in L$ with $|z| \geq n$.\par
        Define $z = uvw$ with $v \neq \epsilon$ and $|uv| \leq n$.\pause\par
        Then, $\forall i \geq 0.\ uv^iw \in L$.\pause\par
        Now, use the last statement to find a contradiction.
    \end{example}
\end{frame}

\end{document}

max_stars_repo_name: jonhue/teaching-theo

max_issues_repo_name: jonhue/teaching-theo

max_forks_repo_name: jonhue/teaching-theo


text:
\chapter{Finite Precision Arithmetic}

\footnote{For more on this see a text book on numerical methods such as Bradie~\cite{Bra06}.} Because computers have a fixed amount of memory, floating point numbers can only be stored with a finite number of digits of precision. This limits the accuracy to which the solution to a numerical problem can be obtained in finite time. Most computers use binary IEEE 754 arithmetic to perform numerical calculations. There are other formats, but this will be the one of most relevance to us.

%subsubsection
\section{Exercises}
\begin{enumerate}
\item[1)] Download the most recent IEEE 754 standard. \url{http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=2355}, see also \url{http://grouper.ieee.org/groups/754/} -- unfortunately the links to the official standard requires either IEEE membership or a subscription. If you do not have this please see the wikipedia page (\url{http://en.wikipedia.org/wiki/IEEE_754-2008}) for the information you will need to answer the questions below\footnote{These links are correct as of 1 April 2012, should they not be active, we expect that the information should be obtained by a search engine or by referring to a numerical analysis textbook such as Bradie~\cite{Bra06}.}.
\begin{enumerate}
\item[a)] In this standard what is the range and precision of numbers in:
\begin{enumerate}
\item[i)] Single precision
\item[ii)] Double precision
\end{enumerate}
\item[b)] What does the standard specify for quadruple precision?
\item[c)] What does the standard specify about how elementary functions should be computed? How does this affect the portability of programs?
\end{enumerate}
\item[2)] Suppose we discretize a function for $x\in[-1,1]$. For what values of $\epsilon$ is
$$\epsilon\log\left(\cosh\left(\frac{x}{\epsilon}\right)\right)=\lvert x \rvert$$
in
\begin{enumerate}
\item[i)] Single precision?
\item[ii)] Double precision?
\end{enumerate}
\item[3)] Suppose we discretize a function for $x\in[-1,1]$. For what values of $\epsilon$ is
\begin{align*}
&{}\tanh\left(\frac{x}{\epsilon}\right)
=\left\{{1 \quad x\geq0}\atop{-1 \quad x < 0}\right.
\end{align*}
in
\begin{enumerate}
\item[i)] Single precision?
\item[ii)] Double precision?
\end{enumerate}
\item[4)]
\begin{enumerate}
\item[a)] What is the magnitude of the largest  4 byte integer in  the IEEE 754  specification that can be stored?
\item[b)] Suppose you are doing a simulation with $N^3$ grid points and need to calculate $N^3$. If $N$ is stored as a 4 byte integer, what is the largest value of $N$ for which $N^3$ can also be stored as a 4 byte integer?
\end{enumerate}
\end{enumerate}

ext: tex

max_stars_repo_name: bcloutier/PSNM

max_issues_repo_name: bcloutier/PSNM

max_forks_repo_name: bcloutier/PSNM


text:
\begin{figure*}[!t] \center
	\includegraphics[width=0.88\textwidth]{./fig/cnn_network.pdf}
\caption{An illustration of our deep convolutional neural field model for depth estimation.
The input image is first over-segmented into superpixels.
In the unary part, for a superpixel $p$, we crop the image patch centred around its centroid,
%
then resize and feed it to a \cnn which is composed of 5 convolutional and 4 fully-connected layers (details refer to Fig. \ref{fig:cnn_unary}).
In the pairwise part,
for a pair of neighbouring superpixels $(p, q)$, we consider $K$ types of similarities, and feed them into a fully-connected layer.
The outputs of unary part and the pairwise part are then fed to the \crf structured loss layer, which minimizes the negative log-likelihood.
Predicting the depths of a new image $\x$ is to maximize the conditional probability $\Pr(\y|\x)$, which has closed-form solutions (see Sec. \ref{sec:learning} for details).
}  \label{fig:cnn_ccrf}
\end{figure*}

%
\section{Deep convolutional neural fields}

%
We present the details of our deep convolutional neural field model for depth estimation in this section. Unless otherwise stated, we use boldfaced uppercase and lowercase letters to denote matrices and column vectors respectively.
%

%
\subsection{Overview}
The goal here is to infer the depth of each pixel in a single image depicting general scenes.
Following the work of \cite{make3d_pami09,Liu_cvpr12,Miaomiao_cvpr14},
we make the common assumption that an image is composed of small homogeneous regions (superpixels)
and consider the graphical model composed of nodes defined on superpixels.
Kindly note that our framework is flexible that can work on pixels or superpixels.
Each superpixel is portrayed by the depth of its centroid.
Let $\x$ be an image and $\y=[y_1,\ldots, y_n]^{\T} \in \Real^n$ be
%
a vector of continuous depth values corresponding to
 all $n$ superpixels in $\x$.
 %
 Similar to conventional CRF,
 we model the conditional probability distribution of the data with the following density function:
%
\begin{equation}\label{eq:prob}
\begin{aligned}
\Pr(\y|\x) = \frac{1}{\mathrm{Z(\x)}} \exp (- E(\y, \x)),
\end{aligned}
\end{equation}
where $E$ is the energy function; $\mathrm{Z}$ is the partition function  defined as:
\begin{equation}\label{eq:partition}
\mathrm{Z}(\x) = \int_{\y} \exp \{ -E(\y, \x) \}\mathrm{d}\y.
\end{equation}
Here, because $\y$ is continuous, the integral in Eq. \eqref{eq:prob} can be analytically calculated under certain circumstances, which we will show in Sec. \ref{sec:learning}.
This is different from the discrete case, in which approximation methods need to be applied.
To predict the depths of a new image, we solve the maximum a posteriori (MAP) inference problem:
\begin{align} \label{eq:inference}
\y^{\star}&=\argmax_{\y} \Pr(\y|\x).
\end{align}

\begin{figure*}[!t] \center
	\includegraphics[width=0.85\textwidth]{./fig/cnn_unary.pdf}
\caption{Detailed network architecture of the unary part in Fig. \ref{fig:cnn_ccrf}. }  \label{fig:cnn_unary}
\end{figure*}

We formulate the energy function as a typical combination of unary potentials $U$ and pairwise potentials $V$ over the nodes (superpixels) $\cal N$ and edges $\cal S$ of the image $\x$:
\begin{equation}\label{eq:energy}
E(\y, \x) = \sum_{p \in {\cal N} } U(y_{p}, \x)
	 + \sum_{(p,q) \in {\cal S}} V(y_{p}, y_{q}, \x).
\end{equation}
The unary term $U$ aims to regress the depth value from a single superpixel.
The pairwise term $V$ encourages neighbouring superpixels with similar appearances to take similar depths.
We aim to jointly learn $U$ and $V$ in a unified \cnn framework.

In Fig. \ref{fig:cnn_ccrf}, we show a sketch of our
%
deep convolutional neural field model
for depth estimation.
As we can see, the whole network is composed of a unary part, a pairwise part and a \crf loss layer.
For an input image, which has been over-segmented into $n$ superpixels,
we consider image patches centred around each superpxiel centroid.
%
The unary part then takes  all the image patches as input and feed each of them to a \cnn
and output an $n$-dimentional vector containing regressed depth values of the $n$ superpixels.
The network for the unary part is composed of $5$ convolutional and $4$ fully-connected layers with details in Fig. \ref{fig:cnn_unary}. Kindly note that the \cnn parameters are shared across all the superpixels.
The pairwise part %
takes similarity vectors (each with $K$ components)  of all neighbouring superpixel pairs as input and feed each of them to a fully-connected layer (parameters are shared among different pairs), then output a vector containing all the $1$-dimentional similarities for each of the neighbouring superpixel pair.
The \crf loss layer takes as input the outputs from the unary and the pairwise parts to minimize the negative log-likelihood.
Compared to the direct regression method in \cite{dcnn_nips14},
%
our model possesses two potential advantages:
1) We achieve translation invariance as we construct unary potentials irrespective of the superpixel's coordinate (shown in Sec. \ref{sec:potentials});
2) We explicitly model the relations of neighbouring superpixels through pairwise potentials.

In the following, we describe the details of potential functions involved in the energy function in Eq. \eqref{eq:energy}.

\subsection{Potential functions}
\label{sec:potentials}

\paragraph{Unary potential}
The unary potential is constructed from the output of a \cnn by considering the least square loss:
\begin{equation}\label{eq:unary}
U(y_{p}, \x;\btheta) = (y_p - \regress_p (\btheta))^2, \;\; \forall p=1,...,n.
\end{equation}
Here $\regress_p$ is the regressed depth of the superpixel $p$ parametrized by the \cnn parameters $\btheta$.
%

The network architecture for the unary part is depicted in Fig. \ref{fig:cnn_unary}.
Our \cnn model in Fig. \ref{fig:cnn_unary} is mainly based upon the well-known network architecture of Krizhevsky \etal \cite{AlexNet12} with modifications.
It is composed of $5$ convolutional layers and $4$ fully connected layers.
The input image is first over-segmented into superpixels, then for each superpixel, we consider the image patch centred around its centroid. Each of the image patches is resized to $ 224 \times 224$ pixels and then fed to the convolutional neural network.
Note that the convolutional and the fully-connected layers are shared across all the image patches of different superpixels.
Rectified linear units (ReLU) are used as activiation functions for the five convolutional layers and the first two fully connected layers.
For the third fully-connected layer, we use the logistic function ($f(x)=(1+e^{-x})^{-1}$) as activiation function.
%
The last fully-connected layer plays the role of model ensemble with no activiation function followed.
The output is an $1$-dimentional real-valued depth for a single superpixel.

\paragraph{Pairwise potential}
We construct the pairwise potential from $K$ types of similarity observations, each of which enforces smoothness by exploiting consistency information of neighbouring superpixels:
\begin{align} \label{eq:pairwise}
&V(y_{p}, y_{q}, \x; \bbeta) = \half \pws_{pq} (y_p - y_q)^2, \;\forall p,q=1,...,n.
%
\end{align}
Here $\pws_{pq}$ is the output of the network in the pairwise part (see  Fig. \ref{fig:cnn_ccrf}) from a neighbouring superpixel pair $(p,q)$.
We use a fully-connected layer here:
\begin{align}  \label{eq:def_R}
\pws_{pq} = \bbeta^{\T} [S_{pq}^{(1)},\ldots,S_{pq}^{(K)}]^{\T} = \sum_{k=1}^K \beta_k S_{pq}^{(k)},
\end{align}
where $\S^{(k)}$ is the $k$-th similarity matrix whose elements are $S_{pq}^{(k)}$ ($\S^{(k)}$ is symmetric);
$\bbeta=[\beta_1, \ldots, \beta_k]^{\T}$
are the network parameters.
From Eq. \eqref{eq:def_R}, we can see that we don't use any activiation function.
However, as our framework is general, more complicated networks can be seamlessly incorporated for the pairwise part.
In Sec .\ref{sec:learning}, we will show that we can derive a general form for calculating the gradients with respect to $\bbeta$ (see Eq. \eqref{eq:derive_beta_final}).
%
%
%
%
To guarantee
%
$Z(x)$ (Eq. \eqref{eq:partition}) is integrable, we require $\beta_k \geq 0$ \cite{ccrf_nips08}.
%

We consider $3$ types of pairwise similarities, measured by the color difference, color histogram difference and texture disparity in terms of local binary patterns (LBP) \cite{LBP_icpr94}, which take the conventional form:
%
$S_{pq}^{(k)} = e^{-\gamma \norm{s_p^{(k)} - s_q^{(k)}}}, k=1,2,3$,
where $s_p^{(k)}$, $s_q^{(k)}$ are the observation values of the superpixel $p$, $q$ calculated from color, color histogram and LBP;
$\norm{\cdot}$ denotes the $\ell_2$ norm of a vector and $\gamma$ is a constant.

%
%
%

%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%

\subsection{Learning}
\label{sec:learning}
With the unary and the pairwise pontentials defined in Eq. \eqref{eq:unary}, \eqref{eq:pairwise}, we can now write the energy function as:
\begin{equation}\label{eq:feature}
E(\y, \x) = \sum_{p \in {\cal N} } (y_p - \regress_p)^2
+ \sum_{(p,q) \in {\cal S}} \half \pws_{pq} (y_p - y_q)^2.
\end{equation}
For ease of expression, we introduce the following notation:
\begin{align} \label{eq:def_Amat}
 \A = \I+ \D - \bpws,
\end{align}
%
%
%
where $\I$ is the $ n \times n$ identity matrix; $\bpws$ is the matrix composed of $\pws_{pq}$;  $\D$ is a diagonal matrix with $\D_{pp} = \sum_q \pws_{pq}$.
Expanding Eq. \eqref{eq:feature}, we have:
\begin{align} \label{eq:feature_expand}
E(\y, \x) = \y^\T \A \y - 2\bregress^\T \y + \bregress^\T \bregress.
\end{align}
Due to the quadratic terms of $\y$ in the energy function in Eq. \eqref{eq:feature_expand} and the positive definiteness of $\A$, we can analytically calculate the integral in the partition function (Eq. \eqref{eq:partition}) as:
\begin{align} \label{eq:partition_expand}
Z(\x) &= \int_{\y} \exp \{ -E(\y, \x) \}\mathrm{d}\y  \notag \\
 	&=\frac{{(\pi)}^{\frac{n}{2}}}{{|\A|}^{\frac{1}{2}}} \exp \{{ \bregress ^\T \A^{-1} \bregress} - \bregress^\T \bregress \}.
\end{align}
From Eq. \eqref{eq:prob}, \eqref{eq:feature_expand},  \eqref{eq:partition_expand},  we can now write the probability distribution function as (see supplementary for details):
\begin{align} \label{eq:prob_final}
\Pr(\y|\x) =\frac{ |\A|^{\half}} {{\pi^{\frac{n}{2}}}} \exp \Big\{ - \y^\T \A \y + 2\bregress^\T \y -  \bregress ^\T \A^{-1} \bregress \Big\},
\end{align}
where $\bregress=[\regress_1, \ldots, \regress_n]^{\T}$; $|\A|$ denotes the determinant of the matrix $\A$, and $\A^{-1}$ the inverse of $\A$.
Then the negative log-likelihood can be written as:
\begin{align} \label{eq:log-likelihood}
-\log\Pr(\y|\x)&= \y^\T \A \y - 2\bregress^\T \y + \bregress ^\T \A^{-1} \bregress  \\ \notag
& - \half\log(|\A|) + \frac{n}{2}\log(\pi).
\end{align}

%
%
%
%
%
%
%
%
%
%
%
%
%
During learning, we minimizes the negative conditional log-likelihood of the training data. Adding regularization to $\btheta$, $\bbeta$, we then arrive at the final optimization:
\begin{align} \label{eq:ccrf_final}
\min_{\btheta, \bbeta \geq \zeros} &-\sum_{i=1}^N \log\Pr(\y^{(i)} | \x^{(i)}; \btheta, \bbeta) \\ \notag
&+ \frac{\lambda_1}{2} \fnorm \btheta + \frac{\lambda_2}{2} \fnorm \bbeta,
\end{align}
where $\x^{(i)}$, $\y^{(i)}$ denote the $i$-th training image and the corresponding depth map; $N$ is the number of training images; $\lambda_1$ and $\lambda_2$ are weight decay parameters.
We use stochastic gradient descent (SGD) based back propagation to solve the optimization problem in Eq.  \eqref{eq:ccrf_final} for learning all parameters of the whole network.
%
We project the solutions to the feasible set when the bounded constraints $\beta_k \geq 0$ is violated.
In the following, we calculate the partial derivatives of $-\log\Pr(\y|\x)$ with respect to the network parameters $\theta_l$ (one element of $\btheta$) and $\beta_k$ (one element of $\bbeta$) by using the chain rule (refer to supplementary for details):
%
\begin{align}
\frac{\partial \{ -\log\Pr(\y|\x)\} }{\partial \theta_l}
%
%
%
& = 2 (\A^{-1} \bregress - \y)^{\T} \frac{\partial \bregress}{\partial \theta_l}, \label{eq:derive_z} \\
%
%
\frac{\partial \{ -\log\Pr(\y|\x)\} }{\partial \beta_k}
& = \y^{\T} \J \y - \bregress^{\T} \A^{-1} \J \A^{-1}\bregress \notag \\
& \; - \half \trace \Big( \A^{-1} \J \Big),  \label{eq:derive_beta_final}
\end{align}
%
%
%
%
%
%
%
where $\trace(\cdot)$ denotes the trace of a matrix; $\J$ is an $n \times n$ matrix with elements:
\begin{align}  \label{eq:def_J}
J_{pq}& =  - \frac{\partial  \pws_{pq} }{\partial \beta_k}
+ \delta(p=q) \sum_q \frac{\partial  \pws_{pq} }{\partial \beta_k},
\end{align}
where $\delta(\cdot)$ is the indicator function, which equals 1 if $p=q$ is true and 0 otherwise.
From Eq. \eqref{eq:def_J}, we can see that our framework is general and more complicated networks for the pairwise part can be seamlessly incorporated.
Here, in our case, with the definition of $\pws_{pq}$ in Eq. \eqref{eq:def_R}, we have $\frac{\partial  \pws_{pq} }{\partial \beta_k}=S_{pq}^{(k)}$.
%
%
%
%
%
%
%
%
%
%
%
%

\paragraph{Depth prediction}
Predicting the depths of a new image is to solve the MAP inference in Eq. \eqref{eq:inference}, in which closed form solutions exist here (details refer to supplementary): %
\begin{align} \label{eq:inf_solution}
\y^{\star}&=\argmax_{\y} \Pr(\y|\x)  \\ \notag
&= \argmax_{\y} -\y^\T \A \y + 2\bregress^\T \y  \\  \notag
&= \A^{-1} \bregress.
\end{align}
If we discard the pairwise terms, namely $\pws_{pq}=0$, then Eq. \eqref{eq:inf_solution} degenerates to $\y^{\star}=\bregress$, which is a conventional regression model (we will report the results of this method as a baseline in the experiment).

%
%

%

\subsection{Implementation details}
We implement the network training based on the efficient CNN toolbox: VLFeat MatConvNet\footnote{VLFeat MatConvNet: http://www.vlfeat.org/matconvnet/} \cite{matconvnet}.
Training is done on a standard desktop with an NVIDIA GTX 780 GPU with 6GB memory.
%
%
During each SGD iteration, around $\sim 700$ superpixel image patches need to be processed.
The 6GB GPU may not be able to process all the image patches at one time.
We therefore partition the superpixel image patches of one image into two parts and process them successively.
%
%
%
%
Processing one image takes around $10$s (including forward and backward) with $\sim 700$ superpixels when training the whole network.

During implementation, we initialize the first 6 layers of the unary part in Fig. \ref{fig:cnn_unary} using a \cnn model trained on the ImageNet from \cite{vgg_bmvc14}.
First, we do not back propagate through the previous 6 layers by keeping them fixed and train the rest of the network (we refer this process as pre-train) with the following settings:
%
momentum is set to $0.9$, and weight decay parameters $\lambda_1, \lambda_2$ are set to $0.0005$.
During pre-train, the learning rate is initialized at $0.0001$,
and decreased by 40\% every 20 epoches.
%
%
We then run 60 epoches to report the results of pre-train (with learning rate decreased twice).
The pre-train is rather efficient, taking around $1$ hour to train on the Make3D dataset, and inferring the depths of a new image takes less than $0.1$s.
Then we train
%
the whole network with the same momentum and weight decay.
%
We apply dropout with ratio $0.5$ in the first two fully-connected layers of Fig. \ref{fig:cnn_unary}.
Training the whole network takes around $16.5$ hours on the Make3D dataset, and around $33$ hours on the NYU v2 dataset. Predicting the depth of a new image from scratch takes $\sim 1.1$s.


text:
\toclesssection{Divide and Conquer}

\toclesssubsection{Concept}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Introduction}
  \textbf{Concept:}
  \begin{itemize}
    \item<2->
      {\color{MainA}Divide} the problem into smaller subproblems
    \item<3->
      {\color{MainA}Conquer} the subproblems through recursive solving.\\
      If subproblems are small enough solve them directly
    \item<4->
      {\color{MainA}Connect} all subsolutions to solve the overall problem
    \item<5->
      {\color{MainA}Recursive} application of the algorithm on smaller
      subproblems
    \item<6->
      {\color{MainA}Direct} solving of small subproblems
  \end{itemize}
\end{frame}

%-------------------------------------------------------------------------------

\subsection{Maximum Subtotal}

\begin{frame}{Divide and Conquer}{Maximum Subtotal}
  \textbf{Input:}
  \begin{itemize}
    \item<2->
      Sequence {\color{MainA}$X$} of {\color{MainA}$n$} integers
  \end{itemize}
  \textbf{Output:}
  \begin{itemize}
    \item<3->
      Maximum sum of an uninterrupted subsequence of
      {\color{MainA}$X$} and its index boundary
  \end{itemize}
  \vspace{-1em}
  \onslide<4->
  \begin{table}[!t]
    \caption{input values}
    \begin{tabular}{c|c|c|c|c|c|c|c|c|c|c}
      Index & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9\\
      \midrule
      Value & 31 & -41 & 59 & 26 & -53 & 58 & 97 & -93 & -23 & 84
    \end{tabular}
    \label{tab:divide_and_conquer:max_subtotal_example_values}
  \end{table}
  \vspace{1em}
  %TODO: Hand-Drawings here (Free space) or no free space?
  \textbf{Output:} Sum: 187, Start: 2, End: 6
\end{frame}

%-------------------------------------------------------------------------------

%% \begin{frame}{Divide and Conquer}{Maximum Subtotal}
%%   \begin{example}[Maximum Subtotal]
%%     \vspace{-1em}
%%     \begin{table}[!t]
%%       \caption{Input values}
%%       \begin{tabular}{c|c|c|c|c|c|c|c|c|c|c}
%%         Index & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9\\
%%         \midrule
%%         Value & 31 & -41 & 59 & 26 & -53 & 58 & 97 & -93 & -23 & 84
%%       \end{tabular}
%%       \label{tab:divide_and_conquer:max_subtotal_example_values}
%%     \end{table}
%%     \vspace{6em}
%%     %TODO: Hand-Drawings here (Free space) or no free space?
%%     \textbf{Output:} Sum: 187, Start: 2, End: 6
%%   \end{example}
%% \end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal}
  \textbf{Idea:}
  \begin{figure}
    \begin{adjustbox}{width=\linewidth}
      \input{Images/DivideAndConquer/MaxSubTotal_idea.tikz}
    \end{adjustbox}
    \label{fig:divide_and_conquer:max_sub_total_divide}
  \end{figure}
  \vspace{-1.5em}
  \begin{itemize}
    \item<2->
      Solve the left / right half of the problem {\color{MainA}recursively}
    \item<3->
      Combine both solutions into an overall solution
    \item<4->
      The maximum is located in the {\color{MainA}left~half~($A$)}
      or the {\color{MainA}right~half~($B$)}
    \item<5->
      The maximum interval can {\color{MainA} overlap with the border ($C$)}
  \end{itemize}
\end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal}
  \textbf{Principle:}
  \begin{figure}[!h]
    \begin{adjustbox}{width=\linewidth}
      \input{Images/DivideAndConquer/MaxSubTotal_Divide.tikz}
    \end{adjustbox}
    \label{fig:divide_and_conquer:max_sub_total_divide2}
  \end{figure}
  \vspace{-1.5em}
  \begin{itemize}
    \item<2->
      Small problems are solved directly:
      {\color{MainA}$n = 1 \Rightarrow \max = X[0]$}
    \item<3->
      Big problems are decomposed into two subproblems and solved recursively.
      Subsolutions {\color{MainA}$A$} and {\color{MainA}$B$}
      are returned.
    \item<4->
      To solve {\color{MainA}$C$} we have to calculate
      {\color{MainA}rmax} and {\color{MainA}lmax}
    \item<5->
      The overall solution is the maximum of {\color{MainA}$A$},
      {\color{MainA}$B$} and {\color{MainA}$C$}
  \end{itemize}
\end{frame}

%-------------------------------------------------------------------------------

\codeslide{python}{
\begin{frame}{Divide and Conquer}{Maximum Subtotal - Python}
  \vspace{-0.5em}
  \lstinputlisting[
    language=Python,
    basicstyle=\small,
    tabsize=4,
    style={python-idle-code},
    escapechar={@},
    emph={maxSubArray,lmax,rmax},
    emphstyle=\color{blue},
    breaklines=false
  ]{Code/DivideAndConquer/MaxSubTotal_DivideAndConquer.py}
\end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal - Python}
  \vspace{-0.5em}
  \lstinputlisting[
    language=Python,
    basicstyle=\small,
    tabsize=4,
    style={python-idle-code},
    escapechar={@},
    emph={maxSubArray},
    emphstyle=\color{blue}
  ]{Code/DivideAndConquer/MaxSubTotal_SecondTrivialCase.py}
\end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal - Python}
  \vspace{-0.5em}
  \lstinputlisting[
    language=Python,
    basicstyle=\small,
    tabsize=4,
    style={python-idle-code},
    escapechar={@},
    emph={maxSubArray},
    emphstyle=\color{blue}
  ]{Code/DivideAndConquer/MaxSubTotal_Max.py}
\end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal - Python}
  \vspace{-0.5em}
  \lstinputlisting[
    language=Python,
    basicstyle=\small,
    tabsize=4,
    style={python-idle-code},
    escapechar={@},
    emph={maxSubArray},
    emphstyle=\color{blue}
  ]{Code/DivideAndConquer/MaxSubTotal_Max2.py}
\end{frame}
%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal - Python}
  \vspace{-0.5em}
  \lstinputlisting[
    language=Python,
    basicstyle=\small,
    tabsize=4,
    style={python-idle-code},
    escapechar={@},
    emph={lmax},
    emphstyle=\color{blue}
  ]{Code/DivideAndConquer/MaxSubTotal_LMax.py}
\end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal - Python}
  \vspace{-0.5em}
  \lstinputlisting[
    language=Python,
    basicstyle=\small,
    tabsize=4,
    style={python-idle-code},
    escapechar={@},
    emph={rmax},
    emphstyle=\color{blue}
  ]{Code/DivideAndConquer/MaxSubTotal_RMax.py}
\end{frame}
}

%TODO: Implement for Java / C++

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal}
  \begin{table}
    \caption{\textit{lmax} example}
    \label{fig:divide_and_conquer:lmax_example}
    \begin{tabular}{c|cccccc}
      index & $i$ & $i+1$ & $\cdots$ & $\cdots$ & $j-1$ & $j$\\
      %\midrule
      $X$ & 58 & -53 & 26 & 59 & -41 & 31\\
      %\midrule
       {\color{MainA}$sum$} & 58 & 5 & 31 & 90 & 49 & 80\\
      {\color{MainA}$lmax$} & 58 & 58 & 58 & 90 & 90 & 90\\
    \end{tabular}
  \end{table}
  \begin{itemize}
    \item<2->
      The {\color{MainA}$sum$} and {\color{MainA}$lmax$} are initialized with $X[i]$
    \item<3->
      We iterate over {\color{MainA}$X$} from {\color{MainA}$i+1$} to {\color{MainA}$j$} and update {\color{MainA}$sum$}
    \item<4->
      If {\color{MainA}$sum > lmax$}, then {\color{MainA}$lmax$}
      gets updated
  \end{itemize}
\end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal}
  \begin{tabular}{l}
\onslide<1>{\rlap{\includegraphics[width=1\textwidth]{Images/DivideAndConquer/maxsubarray-o1.pdf}}}%
\onslide<2>{\rlap{\includegraphics[width=1\textwidth]{Images/DivideAndConquer/maxsubarray-o2.pdf}}}%
\onslide<3>{\rlap{\includegraphics[width=1\textwidth]{Images/DivideAndConquer/maxsubarray-o3.pdf}}}%
\onslide<4>{\rlap{\includegraphics[width=1\textwidth]{Images/DivideAndConquer/maxsubarray-o4.pdf}}}%
\onslide<5->{\rlap{\includegraphics[width=1\textwidth]{Images/DivideAndConquer/maxsubarray-o5.pdf}}}%
  \end{tabular}
\end{frame}

%-------------------------------------------------------------------------------

% \begin{frame}{Divide and Conquer}{Maximum Subtotal}
%   \begin{figure}
%     \begin{adjustbox}{width=\linewidth}
%       \input{Images/DivideAndConquer/MaxSubTotal_Example.tikz}
%     \end{adjustbox}
%     \caption{\textit{maxSubArray} with $X = [-3, 9, -4, 7]$}
%     \label{fig:divide_and_conquer:max_sub_array_example}
%   \end{figure}
% \end{frame}

%-------------------------------------------------------------------------------

\codeslide{python}{
\begin{frame}{Divide and Conquer}{Maximum Subtotal - Python}
  \vspace{-0.5em}
  \lstinputlisting[
    language=Python,
    basicstyle=\small,
    tabsize=4,
    style={python-idle-code},
    breaklines=false,
    escapechar={@},
    emph={maxSubArray,lmax,rmax},
    emphstyle=\color{blue}
  ]{Code/DivideAndConquer/MaxSubTotal_Runtime.py}
\end{frame}
}

%TODO: Implement for Java / C++

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal - Number of steps $T(n)$}
  \textbf{Recursion equation:}
  \begin{displaymath}
    T(n) = \begin{cases}
      \hfill \underbrace{\Theta(1)}_\text{trivial case} & n = 1\\
      \underbrace{2 \cdot T\left(\frac{n}{2}\right)}_\text{
        solving of subproblems
      } + \underbrace{
        \Theta(n)
        \vphantom{\left(\frac{n}{2}\right)}
      }_\text{combination of solutions} & n > 1
    \end{cases}
  \end{displaymath}
    \begin{itemize}
    \item<2->
      There exist two constants {\color{MainA}$a$} and {\color{MainA}$b$} with:
      \begin{displaymath}
        T(n) \leq \begin{cases}
          \hfill {\color{MainA}a} & n = 1\\
          2 \cdot T\left(\frac{n}{2}\right) + {\color{MainA}b} \cdot n & n > 1
        \end{cases}
      \end{displaymath}
    \item<3->
      We define {\color{MainA}$c := \max(a,b)$}:
      \begin{displaymath}
        T(n) \leq \begin{cases}
          \hfill {\color{MainA}c} & n = 1\\
          2 \cdot T\left(\frac{n}{2}\right) + {\color{MainA}c} \cdot n & n > 1
        \end{cases}
      \end{displaymath}
  \end{itemize}
\end{frame}

%-------------------------------------------------------------------------------

%% \begin{frame}{Divide and Conquer}{Maximum Subtotal - Number of steps $T(n)$}
%%   \begin{itemize}
%%     \item
%%       There exist two constants $a$ and $b$ with:
%%       \begin{displaymath}
%%         T(n) \leq \begin{cases}
%%           \hfill a & n = 1\\
%%           2 \cdot T\left(\frac{n}{2}\right) + b \cdot n & n > 1
%%         \end{cases}
%%       \end{displaymath}
%%     \item
%%       We define $c := \max(a,b)$:
%%       \begin{displaymath}
%%         T(n) \leq \begin{cases}
%%           \hfill c & n = 1\\
%%           2 \cdot T\left(\frac{n}{2}\right) + c \cdot n & n > 1
%%         \end{cases}
%%       \end{displaymath}
%%   \end{itemize}
%% \end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal - Illustration of $T(n)$}
  \begin{figure}
    \begin{adjustbox}{width=\linewidth}
      \input{Images/DivideAndConquer/MaxSubTotal_Runtime.tikz}
    \end{adjustbox}
    \caption{illustration of the runtime}
    \label{fig:divide_and_conquer:max_sub_array_runtime}
  \end{figure}
\end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal - Illustration of $T(n)$}
  \begin{figure}
    \begin{adjustbox}{width=\linewidth}
      \input{Images/DivideAndConquer/MaxSubTotal_Runtime_Tree.tikz}
    \end{adjustbox}
    \caption{recursion tree method}
    \label{fig:divide_and_conquer:max_sub_array_runtime_tree}
  \end{figure}
\end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal - Illustration of $T(n)$}
  \textbf{Depth:}
  \begin{itemize}
    \item<2->
      Top level with depth {\color{MainA}$i = 0$}
    \item<3->
      Lowest level with {\color{MainA}$2^i = n$} elements
      \begin{displaymath}
        {\color{MainA}\Rightarrow i = \log_2 n}
      \end{displaymath}
  \end{itemize}
  \onslide<4->
  \textbf{Runtime:}
  \begin{itemize}
    \item<5->
      A total of {\color{MainA}$\log_2 n + 1$} levels costing
      {\color{MainA}$c \cdot n$} each\\
      \color{gray}
      The costs of merging the solutions and solving the trivial
      problems are the same in this case
  \end{itemize}
  \onslide<6->
  \begin{displaymath}
    {\color{MainA}
    T(n) = c \cdot n \log_2 n + c \cdot n \in \Theta(n\,\log n)}
  \end{displaymath}
\end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal - Summary}
  \textbf{Summary:}
  \begin{itemize}
    \item<2->
      Direct solution is slow with {\color{MainA}$\mathcal{O}(n^3)$}
    \item<3->
      Better solution with incremental update of sum was
      {\color{MainA}$\mathcal{O}(n^2)$}
    \item<4->
      Divide and conquer approach results in
      {\color{MainA}$\mathcal{O}(n\,\log n)$}
    \item<5->
      There is an approach running in {\color{MainA}$\mathcal{O}(n)$},
      under the assumption that all subtotals are positive
  \end{itemize}
\end{frame}

%-------------------------------------------------------------------------------

\begin{frame}{Divide and Conquer}{Maximum Subtotal}
  \begin{figure}
    \begin{adjustbox}{width=\linewidth}
      \input{Images/DivideAndConquer/MaxSubTotal_LinearRuntime.tikz}
    \end{adjustbox}
    \caption{scanning the array in linear time}
    \label{fig:divide_and_conquer:max_sub_total_linear}
  \end{figure}
\end{frame}

\codeslide{python}{
\begin{frame}{Divide and Conquer}{Maximum Subtotal - Python}
  \vspace{-0.5em}
  \lstinputlisting[
    language=Python,
    basicstyle=\small,
    tabsize=4,
    style={python-idle-code},
    breaklines=false,
    escapechar={@},
    emph={maxSubArray},
    emphstyle=\color{blue}
  ]{Code/DivideAndConquer/MaxSubTotal_LinearRuntime.py}
\end{frame}
}

%TODO: Implement for Java / C++

max_stars_repo_name: TobiOnline/AlgoDat

max_issues_repo_name: TobiOnline/AlgoDat

max_forks_repo_name: TobiOnline/AlgoDat


text: \section{Estimation and Simulation}

max_stars_repo_name: Randl/GMAT


text:
% intro.tex - What we did and did not do, and a hint of why, with forward refs
%------------------------------------------------------------------------------

\section{Introduction}
\label{intro}

%%% Godmar/Pat draft 1:
%%% McQ draft 1:
%%% Godmar revisions
%%% McQ revisions
%%% Godmar revisions 2 (mostly threw stuff out)

Fluke is a microkernel implemented in an object-based spirit.
Fluke operations are made available as methods on a collection of
primitive {\it Fluke objects} such as threads, ports, memory regions,
mutexes, condition variables, and others.  Fluke's high-level organizing
pattern is that of {\em recursive virtual machines\/}
or {\em nested processes\/}\cite{ford+:osdi96}. Nested processes
communicate via the low-level Fluke inter-thread communications facility,
called {\it Fluke IPC}, to provide a virtual machine abstraction.

Fluke allows the kernel state of an object to be exported {\em at any time}
\cite{Tullmann+:iwooos96}. This even holds for long-running kernel operations
in which an object may be involved. Therefore, these operations must
be decomposable into smaller units that leave each object in a
consistent state which can be exported. A checkpointer may extract
an object's state, pickle it and use the exported state to reconstruct
and restart these objects at a later time.

For instance, the Fluke IPC mechanism is designed to allow suspension
and resumption of long-lived IPC operations.  The operations are broken
into smaller pieces. Objects enter and leave these smaller primitives
in a consistent state. Since the Fluke thread objects of the participating
threads are used to keep track of the IPC operation's progress,
these consistent states must be valid restart-points for these threads.

Our work thus far has focused on model-checking the Fluke IPC subsystem,
in particular the Fluke {\it reliable IPC} mechanism, which is the most
complex, subtle and important of the three flavors of Fluke IPC.

The achievements of this effort are threefold.  First, we have
reverse-engineered a descriptive model of the Fluke IPC subsystem from
the current C implementation.  Second, we used this descriptive
model to develop a checkable model of the reliable IPC subsystem in
Promela \cite{Spin-book} which we present in sections \ref{ipc} and
\ref{core}.  Lastly, we have begun evaluating the performance of this
model under various realistic scenarios with encouraging results, as
presented in section \ref{results}.  This section we also
describe our experiences with SPIN and list some perceived shortcomings.
We conclude with an evaluation of the prospects of using
the SPIN model-checker as the basis for a larger-scale formal
verification effort of the Fluke kernel.

max_stars_repo_name: PimW/spins

max_issues_repo_name: PimW/spins

max_forks_repo_name: PimW/spins


text:
\documentclass[letterpaper]{article}

\usepackage{fullpage}
\usepackage{nopageno}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[utf8]{inputenc}
\allowdisplaybreaks

\newcommand{\abs}[1]{\left\lvert #1 \right\rvert}

\begin{document}
\title{Notes}
\date{November 5, 2014}
\maketitle
\section*{5.4 compactness and extreme values}
$y=x^2$ has min but no max and no supremum

$y=e^{-||\vec{x}||^2}$ has max at $x=0$, no minimum, infimum at 0

when the domain $D\subseteq \mathbb{R}^n$ is unbounded a function need not attain it's max or min

$y=\frac{1}{x}$, $x\in(0,1]$. domain is bounded, but not closed.

we like compact sets for domains, because this is when functions are guaranteed to obtain max and min (if they are continuous).

$f(x)=\begin{cases}x&x\in[0,1)\\0&x=1\end{cases}$
\subsection*{thm 5.4.4}
let $C\subseteq \mathbb{R}^n$ be compact and let $f:C\to\mathbb{R}$ be continuous. then $\exists \vec{a},\vec{b}\in C$ such  that $\forall \vec{x}\in C$ $f(\vec{a})\le f(\vec{x}\le f(\vec{b})$. ie f attains its min at $\vec{a}$ and it's max at $\vec{b}$.

we need something to prove this
\subsubsection*{5.4.3}
Let $C$ be a compact subset of $\mathbb{R}^n$ and let $f$ be a continuous function from $C$ into $\mathbb{R}^m$. then the image set $f(C)$ is compact.

a conintous function sends compact sets to compact sets.

pick a sequence $\{z_k\}$ such that $z_k\in f(C)$ for each $k$. we need to prove that this sequence has a convergent subsequence.

$z_k\in f(C)\Leftrightarrow z_k=f(c_k)$ for some $c_k\in C$ now $\{c_k\}$ has a convergent subsequence $\{c_{k_n}\}$ because $C$ is compact. let $\lim c_{k_n}=x$, note that $x\in C$. since $f$ is continuous, $\lim f(c_{k_n}=\lim z_{k_n}=f(x)$. so $\{z_{k_n}\}$ converges to $f(x)\in f(C)$ and so $f(C)$ is compact.

now to prove 5.4.4

\subsubsection*{proof 5.4.4}
so $f(C)\subseteq\mathbb{R}$ is closed and bounded by $5.4.3$. beccause it it bounded, then it has a supremum and an infimum. let $M=\sup f(C)\in \mathbb{R}, m=\inf f(C)\in \mathbb{R}$. given $\varepsilon=\frac{1}{n}\exists a_n\in f(C)$ such that $|a_n-M|<\varepsilon=\frac{1}{n}$. $\{a_n\}$ is a sequence of poins in $f(C)$ that converges to $M$. but $f(C)$ is closed so $M\in f(C)$ so $\exists b\in C$ such that $f(b)=M$. same proof for infimum.

\subsection*{5.5.9}
let $f:C\to\mathbb{R}^m$ where $C\subseteq\mathbb{R}^n$ is compact. then $f$ is uniformally continuous.

$f$ is uniformly continuous if $\forall\varepsilon>0\exists r>0$ such that $||f(x)-f(y)||<\varepsilon$ whenever $||x-y||<r$ for any $x,y\in$ domain of $f$.

\subsubsection*{proof}
assume that $f$ is not uniformly continuous then $\exists \varepsilon>0$ such that $\forall r>0$, we have some points $x,y$ with $||x-y||<r$ but $||f(x)-f(y)||\ge \varepsilon$. in particular, let $r=\frac{1}{n}$, for each $n\in \mathbb{N}$. for each $r=\frac{1}{n}\exists x_n,y_n\in C$ such that $||x_n-y_n||<\frac{1}{n}$ but $||f(x_n)-f(y_n)||>\varepsilon$. $\{x_n\}$ is a sequence in $C$. there is a convergent subsequence $x_{n_k}$ of $\{x_n\}$. let $a=\lim x_{n_k}$ then $||y_{n_k}-a||\le||y_{n_k}-x_{n_k}||+||x_{n_k}-a||$. so $\{y_{n_k}\}$ also converges to $a$. so $f(x_n)$ and $f(y_n)$ converge to $f(a)$ and so $||f(x_n)-f(y_n)||$ converges to $||f(a)-f(a)||=0$ and so it is not possible for $x_{n_k}-y_{n_k}||<\frac{1}{n_k}$ and $||f(x_{n_k}-f(y_{n_k}||\ge \varepsilon$ for a fixed $\varepsilon$.

\section*{exercises}
\subsection*{5.3.I}
let $f$ be a continuous real function defined on an open subset $U$ of $\mathbb{R}^n$. show that $\{(\boldsymbol{x},y):\boldsymbol{x}\in U,y>f(\boldsymbol{x})\}$ is an open subset of $\mathbb{R}^{n+1}$.

two ways, prove that ball $B(x,r)$ exists for each $x\in A$ where $B(x,r)\subseteq A$

we could also prove that $A^C$ is closed

let $(\vec{x},y)\in A$. we know that $\vec{x}\in U$ and $U$ is open. so $\exists r_1>0$ such that $B(\vec{x},r_1)\subseteq U$. and $y\in (f(\vec{x}),\infty+)\in \mathbb{R}$. so $\exists r_2$ such that $(y-r_2,y+r_2)\in (f(\vec{x}),\infty+)$ and so $B(\vec{x},r_1)\times(y-r_2,y+r_2)\supseteq U\times ($

\subsection*{know this for friday}
$f$ is continuous $\leftrightarrow$ $\forall U$ open in $\mathbb{R}^m$ $f:S\to\mathbb{R}^{m}$, $f^{-1}(U)$ is open in $S$ prove that this is equivalent to $\forall K$ closed in$\mathbb{R}^n$ $f^{-1}(K)$ is closed in $S$

\subsection*{5.4.G}
fix $M\in\mathbb{N}$

$f(\overline{B(0,M)})$ then $f$ is restricted to $\overline{B(0,M}$
\end{document}

max_stars_repo_name: ylixir/school

max_issues_repo_name: ylixir/school

max_forks_repo_name: ylixir/school


text:
\documentclass[12pt,a4paper]{article}
\usepackage{microtype}
\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{graphicx}

\newcommand{\dpar}[1]{\left(#1\right)}

\newcommand{\N}{\mathbb{N}}
\newcommand{\R}{\mathbb{R}}

\theoremstyle{definition}
\newtheorem{ex}{Exercise}[section]

\title{Physics 1: Class 5}
\author{Max Jauregui}

\begin{document}
\maketitle

\section{Constant acceleration (continuation)}

Figure~\ref{fig:mruv} shows the $v$ vs $t$ and $x$ vs $t$ graphs for a motion of a particle with constant acceleration.

\begin{figure}[ht]
  \centering
  \includegraphics[width=0.5\textwidth,keepaspectratio]{figures/mruv.pdf}
  \caption{$v$ vs $t$ and $x$ vs $t$ graphs for the motion of a particle eith constant acceleration.}
  \label{fig:mruv}
\end{figure}

\begin{ex}
  A car moves with a constant velocity of $90\,\mathrm{km/h}$. In a
  certain instant the driver of the car puts the brakes on and the car
  travels $60\,\mathrm{m}$ until it stops. Assuming constant
  acceleration, find the acceleration of the car? \emph{Answer:}
  $-5{,}21\,\mathrm{m/s^2}$.
\end{ex}

\begin{ex}
  A plane initially at rest has a uniform acceleration and travels
  $800\,\mathrm{m}$ in order to take off, which it does with a
  velocity of $360\,\mathrm{km/h}$. How much time does the plane take
  to take off? \emph{Answer:} $16\,\mathrm{s}$.
\end{ex}

\begin{ex}
  A car moves with a constant velocity of $36\,\mathrm{km/h}$. When
  the car is at a distance of $60\,\mathrm{m}$ from traffic lights,
  the traffic lights turn yellow and the driver presses on the
  accelerator in order to run it. Taking into account that the
  reaction time of the driver is $0{,}6\,\mathrm{s}$, calculate the
  minimum value of the acceleration of the car in order to run the
  yellow traffic light, knowing that it lasts $4\,\mathrm{s}$. \emph{Answer:} $1{,}75\,\mathrm{m/s^2}$.
\end{ex}

\section{Free fall}

In this case $|a|=g=9{,}8\,\mathrm{m/s}$. Usually we use the $y$ axis
instead of$x$ axis. If the $y$ axis point upwards, $a=-g$; otherwise
$a=g$.

\begin{ex}
  A particle is initially at rest at height $h$ from the ground. How
  much time it will take to reach the ground? What will be its
  velocity in this moment?
\end{ex}

\end{document}

max_stars_repo_name: maxjaure/UEM-DFI

max_issues_repo_name: maxjaure/UEM-DFI

max_forks_repo_name: maxjaure/UEM-DFI


text:
% ---- The rntz class ----
% Based on extarticle, and supports most of its options. Notable differences:
%
% 1. Section & sub-section numbers go into the left margin. Option `nomarginums'
%    disables this. Option `ribbons' puts these numbers on purple-colored
%    ribbons extending from page left.
%
% 2. Sections & sub-sections headings are smaller.
%
% 3. Sub-sub-sections are unnumbered.
%
% 4. Redefines \maketitle and the `abstract' environment.
%
% It also has a somewhat random grab-bag of other features I happen to use:
%
% 5. Requires and configures hyperref, url, and cleveref.
%
% 6. Requires amsmath & amsthm, and defines theorem, conjecture, lemma,
% definition, and corollary environments. It sets them to share a single running
% counter.
%
% 7. Defines some colors, taken from acmart.cls:
% ACM{Blue,Yellow,Orange,Red,LightBlue,DarkBlue,Green,Purple}.
\documentclass{rntz}

%% %% Alternatively, the following suffices for this document, if you just wish
%% %% to see the effect of the other packages in this repo:
%% \documentclass{article}
%% \usepackage{amsmath,amsthm}
%% \usepackage{hyperref,cleveref}
%% \theoremstyle{definition}
%% \newtheorem{theorem}{Theorem}
%% \newtheorem{conjecture}[theorem]{Conjecture}
%% \newtheorem{lemma}[theorem]{Lemma}
%% \theoremstyle{definition}
%% \newtheorem{definition}[theorem]{Definition}
%% \theoremstyle{remark}
%% \newtheorem*{corollary}{Corollary}
%% \theoremstyle{plain}            %back to default

% ---- rntzgeometry and narrow ----
%
% \usepackage{rntzgeometry} chooses a paper size and sets up reasonable margins
% for it. Options: a5, b5, a4, and letter.
%
% \usepackage{narrow} produces a single narrow column of text. The figure* and
% fullwidth environments expand to a larger width. Options:
%
% width=LEN
%   Text width. Default is 345pt.
% fullwidth=LEN
%   Width for figure* and fullwidth environments. Default is \textwidth, i.e.
%   whatever the text width was before you used narrow.sty.
\usepackage[b5]{rntzgeometry}
\usepackage{narrow}

% ---- rntzfont ----
%
% rntzfont chooses from a set of paired fonts, with appropriate scalings and
% line spacings.
%
% Text font options are alegreya, baskervald, charter, cochineal, libertine,
% librebaskerville, palatino, pt, and source. Math font options are euler,
% newmath, and nomath (which doesn't change the math font). Default is charter
% with euler.
\usepackage{rntzfont}

% Some small typographic improvements.
\usepackage[T1]{fontenc}
\usepackage[spacing,tracking,letterspace=20]{microtype}
\frenchspacing

\usepackage{lipsum} % for example text.

\title{Towards Better Typography in \LaTeX{}}
\author{Lore M. Ipsum}
\date{\today}

\begin{document}
\maketitle

\begin{abstract}
  Nam dui ligula, fringilla a, euismod sodales, sollicitudin vel, wisi. Nam
  lacus libero, pretium at, lobortis vitae, ultricies et, tellus. Donec aliquet,
  tortor sed accumsan bibendum, erat ligula aliquet magna, vitae ornare odio
  metus a mi. And on the \emph{n}\textsuperscript{th} day, Knuth created \TeX,
  and all was woe.
\end{abstract}

\section{Mostly fonts}\label{sec:one}

\newcommand{\testtext}{\textsc{This text} is ``meaningless''. \emph{[Quite
      `thoroughly' so! \textsc{-Ed.}]} {\bfseries \{Do you \textsc{disagree}?\}} I
  know 18--57 (\textsc{count 'em}) badgers --- who'd like a 9"
  {\bfseries\itshape rather \textsc{long}} word.}

\begingroup
\testtext\setlength\parskip{1em}\setlength\parindent{0em}

{\sffamily\testtext}

{\ttfamily It's "meaningless". \textbf{But it's monospace!}
  {\itshape
    Is it italic?} \textsc{Unlikely.}\\
  (Braces) [are] \{rather\} <important> \& so 'are' "quotes".
  Il1, O0.}
\endgroup

\subsection{Some mathematics, with references}

Nulla malesuada porttitor diam. Donec felis erat, congue non, volutpat at,
tincidunt tristique, libero.\footnote{Latin latin latin, latin latin latin.
  Greek.} Morbi auctor lorem non justo.\footnote{Another footnote, much like the
  first, a little bit longer --- okay, a lot longer --- and consequently more
  likely to wrap.\par Also, multiple paragraphs! How about that.}

\begin{theorem}[Binomial]\label{thm:binomial}
  Lorem ipsum dolor sit amet, consectetuer:
  %
  \[ (x+y)^n = \sum_{k=0}^n \binom{n}{k} x^{n-k} y^k \]
\end{theorem}

\begin{corollary} Adipiscing $n=4$, elit
  \( (x+y)^4 = x^4 + 4x^3y + 6x^2y^2 + 4xy^3 + y^4 \). Moreover, if $f(x) =
  x^2$, then it follows that $f = \mathit{id} \cdot \mathit{id}$, et cetera, et
  cetera.
\end{corollary}

Vivamus viverra fermentum felis. Donec nonummy pellentesque ante. Pha\-sellus
adipiscing semper elit. Proin fermentum \cref{thm:binomial} massa ac quam:
\nopagebreak[2]
\[ \sum_{i=1}^n n = \frac{n(n+1)}{2} \]

%% %
%% \begin{eqnarray}
%%   e^{i\tau} &=& 0\\
%%   (x+y)^n &=& \sum_{k=0}^n \binom{n}{k} x^{n-k} y^k
%% \end{eqnarray}

Sed diam turpis, molestie vitae, placerat a, molestie nec, leo. Maecenas
lacinia. \Cref{sec:two} nam ipsum ligula, eleifend at, accumsan nec, suscipit a,
ipsum. Morbi blandit ligula feugiat magna. Nunc eleifend consequat lorem. Sed
lacinia nulla vitae enim. Pellentesque tincidunt purus vel magna. Integer non
enim. Praesent euismod nunc eu purus. Donec bibendum quam in tellus. Nullam
cursus pulvinar lectus. Donec et mi. Nam vulputate metus eu enim. Vestibulum
pellentesque felis eu massa.

\section{Another section}\label{sec:two}
\subsection{Immediately followed by a subsection}\label{sec:two-one}

\lipsum[6]

\begin{conjecture}
  Morbi luctus, wisi viverra faucibus pretium, nibh est placerat odio, nec
  commod wisi enim egat quam \cref{sec:two-one}.
\end{conjecture}

\subsubsection{Sub-subsections (like this one) are always unnumbered}

\lipsum[7]

\section{Many sections of lorem ipsum}
\lipsum[8]

\section{Many sections of lorem ipsum}
\lipsum[9]

\section{Many sections of lorem ipsum}
\lipsum[10]

\section{Many sections of lorem ipsum}
\lipsum[11]

\section{Many sections of lorem ipsum}
\lipsum[12]

\section{Many sections of lorem ipsum}
\lipsum[13]

\section{Many sections of lorem ipsum}
\lipsum[14]

\section{Many sections of lorem ipsum}
\lipsum[15]

\subsection{Many subsections}
\lipsum[16]

\subsection{Many subsections}
\lipsum[17]

\subsection{Many subsections}
\lipsum[18]

\subsection{Many subsections}
\lipsum[19]

\subsection{Many subsections}
\lipsum[20]

\subsection{Many subsections}
\lipsum[21]

\subsection{Many subsections}
\lipsum[22]

\subsection{Many subsections}
\lipsum[23]

\subsection{Many subsections}
\lipsum[24]

\subsection{Many subsections}
\lipsum[25]

\subsection{Many subsections}
\lipsum[26]

\section{Unbroken lorem ipsum for many pages}
\lipsum\lipsum[1]\lipsum\lipsum[2]\lipsum\lipsum[3]\lipsum\lipsum[4]
\lipsum\lipsum[5]\lipsum\lipsum[6]\lipsum\lipsum[7]\lipsum\lipsum[8]
\lipsum\lipsum[1]\lipsum\lipsum[2]\lipsum\lipsum[3]\lipsum\lipsum[4]
\lipsum\lipsum[5]\lipsum\lipsum[6]\lipsum\lipsum[7]\lipsum\lipsum[8]

\end{document}

max_stars_repo_name: rntz/rntztex

max_issues_repo_name: rntz/rntztex

max_forks_repo_name: rntz/rntztex


text:
\documentclass[../butidigress.tex]{subfiles}
\begin{document}
\chapter{The Void}\label{chap:thevoid}
\epi{Can one be a saint without God?, that's the problem, in fact the only problem I'm up against today.}{\attrib{Albert Camus}{The Plague}{1947}}
\newpage

\lettrine{T}{he} values and lessons presented in this chapter stem pretty directly from my partial embrace of Albert Camus' absurdism.\ftnote{This is the new introduction to this chapter, much of it adapted from the original.}
Taken directly from \book{The Myth of Sisyphus}, the \say{principles of the absurd man} have some problematic elements, not the least of which is the fact that the phrase \say{absurd man} is widely used throughout that essay.
That being said, I don't really have much experience with the philosophy, basically \book{Sisyphus}, a video about \movie{Synecdoche, New York}, some fragmented high school memories, and various Wikipedia/Stanford Encyclopedia readings.

I first came into contact with Camus in high school, in Mrs.~Nye's, whom I've mentioned before, sophomore year\ftnote{I think.} English class.
We were reading \book{L'\'{E}tranger} (\book{The Outsider} or \book{The Stranger}), a pretty standard high school reading.
Not much attention was paid in that class, I vaguely remember her mentioning absurdism and Sisyphus and his boulder, but I didn't rediscover the philosophy until later, until college\ftnote{I'm not exactly sure when, but somewhere around there.}.

\todobrak{the paragraph below is the old introduction}

This comes pretty clearly from my (partial) embrace of the absurd.\foottodo{this is crazy wrong, absurdism doesn't require the \textit{a priori} recognition of a god}
I struggle with Camus' absurd, caveat that I have read \book{The Myth of Sisyphus} but once; my difficulty stems from the acknowledgment of some form of higher power and the extremely gendered terminology in \book{Sisyphus}.
Intellectually I cannot really brook any consideration of \say{God} in any real form.
In normal conversation I tend to describe myself as agnostic, partially for the sake of expediency, partially out of my fear of certainty\ftnote{Partially out of a fear of nothingness.}, but in reality I am an atheist.
I'm not even really anti-religion, people are free to believe what they believe, and if it doesn't infringe on me, then more power to them.
Religion, for all its faults, has made some great things in the world, and getting a huge swath of humanity to conform to some morality is a good, even if most people don't follow exactly.\ftnote{This partial embrace of religion feels almost like a betrayal to my liberal, academic sensibility.}

I originally titled this section \textit{Fight the Void}, which is not necessarily inappropriate; the current title reflects a broadening of scope.\ftnote{And I just like it better, feels cleaner.}
While the fight against oblivion is important, some might say the most important, conceptually, it is necessary to understand what one is up against.
So this chapter title is meant to be about the fight, but also about the enemy.

The other reason for the title change is that I'm not trying to constrain myself to Camus' absurd, which has a relatively specific definition.
I want to discuss living in the face of the absolute knowledge of one's death, dealing with bleak circumstances\ftnote{One might say that absolute knowledge of one's death is bleak.}, and perseverance through unimaginable hardship.
That's the broader theme of the chapter, the nobility of the struggle; I get that that sounds like absurdism.

\digsec{Camus' Absurd}{6}{8}{18}{camusabsurd}

\begin{somenotes}{Camus' Absurd}
    \item lots of people called Camus an existentialist, he didn't call himself that\foottodo{seems pretty self-evident; give an introduction to the \say{canonical} form of absurdism}
\end{somenotes}

Here I'll give a brief introduction to what the fuck absurdism even is\ftnote{I don't consider myself an \say{absurd man} in the way Camus puts forth; I do however, consider myself a man willing to yell at hurricanes, so to speak}\ldots

As I may have mentioned a couple times\ftnote{Kinda not sure what's above this paragraph, lots of rewriting.}, absurdism is most frequently associated with Albert Camus, the \nth{20} century French-Algerian author and philosopher.
The seminal work in this school of though is \book{The Myth of Sisyphus} an essay, written by Camus in 1942, which outlines the virtues of the \say{absurd man.}
Again, this work had some seriously gendered terminology, a kind of implicit belief that only the male mind is capable of such rich philosophical sight.
This dated way of thinking is easily reconcilable, just imagine \say{people.}

What it really boils down to\ftnote{Or at least, this is the succinct way of thinking about it I just thought of.} is that life, existence as a whole, is about the journey, because that's all there is.\autocite{mythofsisyphus}

\digsec{Expounding on the Infinite}{5}{9}{18}{voidexpounding}
\epi{One must imagine Sisyphus happy.}{\attrib{Albert Camus}{The Myth of Sisyphus}{1942}}
As previously asserted, I don't subscribe fully to Absurdism.\foottodo{this is just rambling at this point}
Conceptually it is appealing to me.

Maybe the higher power thing is not as integral as I thought.
It's more about the nobility of the fight, of not giving in.
I'll talk more about some specifics in the section on \tvshow{The 100},\ftnote{Appendix~\ref{chap:justrandom}, \fref{sec:thehundred}} but I'll cover some generalities right now.

\todobrak{some generalities}

In the \say{scheme of things} every single human life is entirely meaningless. Without fully unpacking what \say{scheme} this refers to we can take it for the titular \say{void}. Such a truth (i.e., the opening sentence to this paragraph) is pretty unavoidable. Logically, most everybody can come to this conclusion, yet we all continue to live.\par Why? Well the simple answer is that most people just ignore it. And why not? it's so easy and it makes life livable. I confess to intentional ignorance on most days.\foottodo{integrate this better}

\digsec{Case Study: \tvshow{The 100}}{5}{9}{18}{thehundred}
\tvshow{The~100} is a television show, currently\ftnote{As of this writing.} airing on \textit{The~CW}.
Set in a dystopian future in which civilization, destroyed by global nuclear war, is kept alive by around 500 people aboard a space station, the Ark, orbiting Earth; the series starts around 100 years after the war.
In order to maintain discipline, all crimes are treated as capital offenses, except for those under eighteen, who are imprisoned.
There are, at the beginning of the series, exactly 100\ftnote{Somehow\ldots} of said young offenders.
These reprobates\ftnote{Some are actually bad people, others are locked up for more innocuous crimes or for getting caught being altruistic, like stealing medicine for sick loved ones and the like.} are sent to the surface to test survivability of the radiation levels.

As one might expect, sending a group of raucous youths, unsupervised, to a, theoretically, uninhabited planet, leads to some hijinks, and a certain amount of attempted murder.
People to whom I've talked about the show tend to dismiss it as \say{just another young adult show,} and I'll admit that it does look like that upon first glance and upon viewing the first episode.
Once the series gets going, however, it gets dark, and starts becoming a compelling exploration of the dangers of tribalism, faith vs.\ pragmatism, and man's true nature.

Here's a little example of how gosh darn intense the show gets; this little scene is from season four, episode three\ftnote{I think, may be earlier or later.}.
So there's this crazy radiation wave coming to kill everybody\ftnote{Because of nuclear reactors that are breaking down; turns out the bad guy in season three genuinely thought she was saving humanity.} and this family of \say{grounders}\ftnote{What the people from the Ark call the descendants those who managed to survive on Earth after the nuclear war.} shows up at the space people's camp.
There's the dad (who was actually a pretty established character, which was weird) and the mom (who ends up being pretty important to the story) and a couple kids (or maybe just one, I don't remember for sure).
They're a cute family and one of the kids has pretty bad radiation poisoning.
Anyways, long story short the kid dies in her parents arms; like, she takes her last, strained and shuddering breaths, her breathing slowing until it stops.
Her parents, go from comforting their child, to the most abject grief anyone could possibly imagine.
That ain't normal, run-of-the-mill young adult fare; that's some hardcore stuff.
From here, we'll talk about some individual characters and overarching plot-lines as they relate to \say{The Void.}

One of the options available to a person who considers the universe's lack of feeling is to basically say \say{fuck it} and pretty much give up on life.
In fact, that may be the only real choice that we make in life, whether or not to live once our eyes have opened.\autocite{mythofsisyphus}
Having chosen the \say{throw it all away} route, there are additional forks; one can simply commit suicide\ftnote{I've always found the fact that we say \say{commit suicide} kinda weird, like it feels weirdly formal} or one can throw any sense of human decency to the wind and live a hedonistic, Caligula-esque life.
In \tv{The 100}, the character Jasper has taken these two paths; Earth was not friendly to him and he lost at every turn.

\end{document}

max_stars_repo_name: mvwicky/ButIDigress

max_issues_repo_name: mvwicky/ButIDigress

max_forks_repo_name: mvwicky/ButIDigress


text:
\section{Future Work}
\label{sec:future_work}

Despite all the accomplishments achieved through the AdaptUI platform, there are
still several areas and features in which more efforts are required to improve
the presented results. Consequently, in this section several ideas about future
research actions are presented and, in some cases, an explanation of the steps
that should be taken.

\begin{enumerate}[label=\alph*)]
  \item Dynamic self-generation adaptive rules. Although AdaptUI provides three
  different sets of rules, these rules are static, and they always depend on
  the corresponding developer to be designed. This means that rules have to
  be added in a previous stage, when users are still not present. In the near
  future we aim to provide to AdaptUI an extra module capable of generating and
  adapting at runtime different rules considering several context change
  triggers. Thus, from a default set of rules, these rules could be personalized
  taking into account the user experience.

  \item Further \textit{Pellet4Android} evaluation and tests are needed. Although
  it provides promising results running in Android devices, deeper processing
  experiments are needed. More specialized datasets should be used to compare
  the results.

  \item AdaptUI basically covers disabilities related to visual and hearing
  sensory limitations. A further study and analysis of these and more
  disabilities, based on the \ac{icf}, would include more users and better
  adaptations of the user interfaces.

  \item Use users with actual enduring disabilities.

  \item Translate the models to JSON-LD~\citep{jsonld}, which is a JSON based
  Linked Data format.

  \item Adapt the \ac{api}, reaching a more object oriented paradigm. For instance,
  declaring an individual and being able to modify it with class methods would
  be desirable than the current approach, in which there is just a method to
  declare it through the AdaptUI object. Listing~\ref{lst:api_adaptation} shows
  an example of the mentioned changes.

  \inputminted[linenos=true, fontsize=\footnotesize, frame=lines]{java}{6_conclusion/api_adaptation.java}
\captionof{listing}{Projected changes in the \ac{api}.\label{lst:api_adaptation}}

  \item Including the usability metrics in the Modelling Layer might help to
  identify the user needs in the current context. This will also allow to avoid
  the necessity of using the Capabilities Collector. In the current version it
  is mandatory to use it to collect several user preferences. By anticipating
  the intervention of the usability metrics the interaction monitoring process
  might produce significant preferences results.

%   \item Managing more than one possible configuration for the same view for the
%   same context. For instance, combining the functionality of a button with a
%   specific configuration.

  \item Integrate the proposed framework with the paradigm followed by
  \citet{marmolin_medium_1995}, through which it would be possible to distinguish
  between superficial and deep customizations depending on the context situation.
  This could be used to enrich the functionalities of the Adaptation Polisher
  module.
\end{enumerate}

max_stars_repo_name: edlectrico/dissertation

max_issues_repo_name: edlectrico/dissertation

max_forks_repo_name: edlectrico/dissertation


text:
%%% -*- mode: LaTeX; TeX-master: "main.tex"; -*-

\ifx\master\undefined
\documentclass[a4paper]{easychair}
\usepackage{submission}
\begin{document}
{\let\master\relax\input{frontmatter}}
\fi
%%%% PLEASE DO NOT EDIT ABOVE THIS LINE

\section{Introduction}
\label{sec:intro}

\tlaplus\ is a language for specifying the behaviour of concurrent and
distributed systems and asserting properties of those
systems~\cite{lamport03tla}.  However, it provides no way to write
proofs of those properties.  We have designed an extended version of
the language that allows writing proofs, and we have begun
implementing a system centered around a \textit{Proof Manager} (\PM)
that invokes existing automated and interactive proof systems to check
those proofs. For now, the new version of \tlaplus\ is called \tlatwo\
to distinguish it from the current one.  We describe here the \tlatwo
proof constructs and the current state of the proof system.

The primary goal of \tlatwo\ and the proof system is the mechanical
verification of systems specifications. The proof system must not only
support the modal and temporal aspects of TLA needed
to reason about system properties, but must also support
ordinary mathematical reasoning in the underlying logic. Proofs in
\tlatwo are natural deduction proofs written in a hierarchical style
that we have found to be good for ordinary
mathematics~\cite{lamport93amm} and crucial for managing the
complexity of correctness proofs of systems~\cite{gafni:disk-paxos}.

The \PM\ computes proof obligations that establish the correctness of
the proof and sends them to one or more back-end provers to be
verified.  Currently, the back-end provers are Isabelle/\tlaplus, a
faithful axiomatisation of \tlaplus\ in Isabelle/Pure, and
Zenon~\cite{bonichon07lpar}, a tableau prover for classical
first-order logic with equality.  The \PM\ first sends a proof
obligation to Zenon.  If Zenon succeeds, it produces an Isar script
that the \PM\ sends to Isabelle to certify.  Otherwise, the \PM
directs Isabelle to try to find a proof with its automated tactics.
In both cases, the proofs are certified by Isabelle/\tlaplus.
%%
%% SM: I changed the following sentence because its original
%% formulation seems to defeat certifiability, an issue that we
%% highlight.
%%
%This system
%architecture allows us in the future to add other back-end provers
%whose proofs need not be certified by Isabelle/\tlaplus.
The system architecture easily accomodates other back-end provers; if
these are proof-producing, certification by Isabelle/\tlaplus\ gives
us high high confidence in the overall correctness.

The \tlatwo\ proof constructs are described in
Section~\ref{sec:proof-language}.  Section~\ref{sec:obligations}
describes the proof obligations generated by the \PM, and
Section~\ref{sec:backend} describes how the \PM\ uses Zenon and
Isabelle to verify them.  The conclusion summarizes what we have done
and not yet done and briefly discusses related work.

%%%% PLEASE DO NOT EDIT BELOW THIS LINE
\ifx\master\undefined
{\let\master\relax\input{rearmatter}}
\end{document}
\fi

max_stars_repo_name: damiendoligez/tlapm

max_issues_repo_name: damiendoligez/tlapm

max_forks_repo_name: damiendoligez/tlapm