text:
\section{Introduction}
\label{sec:lts-transformation:intro}
Model-driven software development (MDSD)~\cite{mdsd} entails creating implementations on a low level of abstraction from designs represented by models on a high level of abstraction.
Implementation details are added to these abstract models by means of refining model transformations.
By applying one or more of such transformations to a model that represents the high-level design of a software system, a model on a low level of abstraction can be generated that can be transformed to an implementation for this system straightforwardly.
In case a sequence of transformations is applied, also a number of intermediate models is produced.
Usually, an implementation must satisfy a number of requirements that can be expressed as properties of the model that forms its design.
To ensure that the implementation satisfies its requirements, these properties should also hold for the models that result from model transformations.
In other words, these transformations should preserve properties.
In this chapter, we address research question~\RQ{6}, where a model transformation is considered to be correct if the desirable properties of the input model are preserved in the refined model.
We present a technique to automatically verify the correctness of model transformations.

\RQSix

\noindent
Here, we deal with a modeling formalism with a more restricted expressiveness in comparison to the formalism discussed in Chapter~\ref{chap:reusable-correct-transformations}.
Additionally, the model transformations considered below are of a more abstract nature than those presented in Chapter~\ref{chap:reusable-correct-transformations}.

Traditionally, model checking~\cite{Clarke1999} is applied to verify whether models satisfy certain properties.
The models that form the design of a system are often relatively small, which means that properties of such models can easily be verified using traditional techniques such as explicit state-space exploration.
Unfortunately, however, iteratively refining these models by adding implementation details quickly results in models that suffer from the state-space explosion problem.
This makes it practically unfeasible to perform verification on the resulting refined models by traversing their complete state space.
To overcome this problem, we introduce a model checking technique that can be used to determine whether a transformation preserves properties.
Using this technique, the fact that the properties that hold for the initial model also hold for the refined model can be inferred from the fact that the transformation is property preserving.
In this way, only the initial model needs to be model checked using the traditional technique.

\begin{figure}[hbt]
\centering
\includegraphics[scale=0.6]{lts-transformation/figs/rechecking-overview}
\caption{Avoiding rechecking intermediate models by checking transformations}
\label{fig:lts-transformation:rechecking}
\end{figure}

The technique presented in this chapter can assert whether a transformation is property preserving for all possible models provided as input.
However, if a transformation cannot be shown to preserve properties for all input models, it may still preserve some properties for particular input.
In such cases, verification of refined models using traditional techniques may still show that the given properties hold for these models.
Figure~\ref{fig:lts-transformation:rechecking} illustrates the application of our technique.
It sketches the refinement of model~\Model{1}, which is transformed to model~\Model{n} through a sequence of refinement steps.
When a property holds for a model, which is indicated by a black check mark, and this model is transformed using a transformation that preserves this property, which is also indicated by a black check mark, then the property is guaranteed to hold for the resulting model.
A white check mark is used to indicate that this is established without rechecking the property for the new model.
If a transformation is not guaranteed to preserve a property, the property needs to be rechecked.
Transformation~\Transformation{m}, for example, does not preserve the property at hand.
Therefore, the property needs to be checked again for model~\Model{m}.

In this chapter, labeled transition systems~(LTSs) are used to represent individual processes.
By combining these processes with synchronization rules, networks of LTSs~\cite{lang05} are obtained, which represent models.
The synchronization rules define how the processes in a network synchronize with each other.
A model is refined by transforming its processes using transformation rules and possibly adding additional synchronization rules.
Each transformation rule defines how a part of the behavior of a process should be refined.
To check whether a refinement step is property preserving, only the transformation rules, a subset of the synchronization rules of the model provided as input, and the newly introduced synchronization rules need to be examined.
However, to be able to reason about property preservation of transformations, a number of reasonable conditions are formulated that must hold for the networks and transformations under consideration.
The technique presented here is applicable to any modeling language whose semantics can be expressed in terms of networks of LTSs.

Mateescu and Wijs~\cite{mateescu.wijs.propred} identified a fragment of the modal $\mu$-calculus~\cite{Kozen-83} that is compatible with divergence-sensitive branching bisimilarity (DSBB)~\cite{GlaLutTrc09}.
Because of this compatibility, if a certain property expressed using this fragment of the modal $\mu$-calculus holds for a given model, it also holds for all bisimilar models.
The identified fragment is sufficiently expressive to capture the vast majority of practical safety, liveness, and fairness properties.
In the same paper, the technique of maximal hiding is introduced.
Given a property, maximal hiding enables automatically abstracting away from all behavior that is not relevant for the property.
We use both of these results for our preservation check as follows.
First, networks of transformation rules are constructed based on the synchronization rules before and after the application of a transformation.
Then, the LTSs corresponding to these networks of transformation rules are computed.
Each of these networks leads to a pair of LTSs, where one LTS represents the relevant behavior before transformation and the other the behavior after transformation.
Finally, property preservation is checked by applying maximal hiding to all the LTSs and checking whether each pair of LTSs is divergence-sensitive branching bisimilar.

The remainder of this chapter is structured as follows.
Section~\ref{sec:lts-transformation:background} introduces the preliminaries.
In Section~\ref{sec:lts-transformation:transformations}, we formalize LTS transformation.
Next, in Section~\ref{sec:lts-transformation:proppres}, we discuss our technique for determining whether transformations preserve properties.
Experimental results are given in Section~\ref{sec:lts-transformation:experiments}.
Section~\ref{sec:lts-transformation:related} discusses related work, and Section~\ref{sec:lts-transformation:conclusions} contains conclusions and pointers to future work.

ext: tex

max_stars_repo_name: ljpengelen/latex-phd-thesis

max_issues_repo_name: ljpengelen/latex-phd-thesis

max_forks_repo_name: ljpengelen/latex-phd-thesis


text:
\documentclass[11pt]{article}
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage[utf8]{inputenc}

\begin{document}

\section{ECC Summer School 2015}
\subsection{Intro - Software and Hardware implementation of Elliptic Curve Cryptography}
Presentation by Jérémie Detrey.
Reminders on elliptic curves over finite fields, associated operations, ECDH and ElGamal. \newline
Jérémie then states the design goals of ECC implementations: efficient and secure.

Efficiency can have multiple meanings. Does it refer to:
\begin{itemize}
	\item fast? $\to$ low latency or high throughput?
	\item small? $\to$ low memory / code / silicon usage?
	\item low power? ... or low energy?
\end{itemize}
Constraints are going to depend to the application and target platform.

The other design goal was security, but secure against which attack:
\begin{itemize}
	\item protocol attacks? (FREAK, LogJam, etc) [More in N. Heninger's talk]
	\item curve attacks? (weak curves, twist security, etc.)
	\item timing attacks? [More in P. Schwabe's talk]
	\item fault attacks? [More in J. Krämer's talk]
	\item cache attacks?
	\item branch-prediction attacks?
	\item power or electromagnetic analysis?
\end{itemize}

A list of possible target platforms is enumerated to highlight the discrepancy in resources between them.

The layer of ECC implementations are usually:
\begin{itemize}
	\item protocol (OpenPGP, TLS, SSH, etc)
	\item cryptographic primitives (ECDH, ECDSA, etc)
	\item scalar multiplication
	\item elliptic curve arithmetic (point addition, point doubling, etc.)
	\item finite field arithmetic (addition, multiplication, inversion ...)
	\item native integer arithmetic (CPU instruction set)
\end{itemize}

For hardware implementations, there are additional layers:
\begin{itemize}
	\item logic circuits (registers, multiplexers, adders, etc.)
	\item logic gates (NOT, NAND, etc.) and wires
	\item transistors
\end{itemize}

All (top) layers might lead to critical vulnerabilities if poorly implemented! ECC is no more secure than its weakest link.

Jérémie concludes introduction with some references. Most books are already quite old. He suggests to read proceedings of recent crypto conferences such as CHES.

Elliptic curve points multiplication methods are then covered (Double-and-add, windowed method, wNAF method, GLV curves ...). The double-and-add algorithm is easily vulnerable to timing analysis (by revealing the hamming weight of secret k) and a power analysis will leak bits of k. An counter-measure to this attack could be to "double-and-add-always" but this is still vulnerable to fault-attacks. A better alternative is the Montgomery ladder since it has the following properties:
\begin{itemize}
	\item performs one addition and one doubling at each step
	\item ensure that both results are used in the next step
	\item loop invariant: $T_1$ = $T_0$ + $P$ (See slides)
\end{itemize}

But the conditional branches depend on the value of a secret bit $k_i$. Hence, it might be vulnerable to branch prediction attacks. We can compute indices for $T_0$ and $T_1$ from $k_i$? Issue is that memory access to $T_0$ or $T_1$ depend on secret bit $k_i$, hence might be vulnerable to cache attacks.

Solution: use bit masking to avoid secret-dependent memory access patterns.

\subsection{The group of rational points of an elliptic curve over a finite field}
Presentation by Damien Robert. He starts his presentation by defining an elliptic curves over complex numbers and defining classes of isomorphisms of elliptic curves. Two elliptic curves $E$ and $E'$ are isomorphic over $\bar{k} \iff j_{E} = j{\bar{E}}$ where $j$ is the $j-invariant$.

A twist of an elliptic curve $E/k$ is an elliptic curve $E'/k$ isomorphic to $E$ over $\bar{k}$ but not over $k$.

Why look at the complex numbers? For cryptography we work with elliptic curves over finite fields. Everything that is true over $\mathbb{C}$ is true over other fields except when it is not true (non algebraically closed fields, characteristic $p$ ...). Example: "there are $n^2$ points of $N$-torsion."
How can we transfer results from $\mathbb{C}$ to other fields?
Damien then goes back to $\mathbb{C}$ and defines the Weil pairing over $\mathbb{C}$.
For more notes on this session, refer to slides.

\subsection{Algorithms for discrete logarithms in finite fields and elliptic curves}
Presentation by Emmanuel Thomé. Introduction to ECDLP. This presentation does not address here the DH-related problems, but really the computation of DL.
\subsubsection{Hardness}
What does it mean for:
\begin{itemize}
	\item DLP to be hard on EC
	\item DLP to be moderately hard on finite fields
	\item DLP to be easy on small characteristic finite fields.
\end{itemize}

We want the cost of computing DL by most efficient
means known to grow fast.

So, what groups shall we avoid?
\begin{itemize}
	\item Easy DL: $(\mathbb{Z}/N\mathbb{Z}, +)$
	\item Not-so-hard DL: finite fields, curves of very large genus, class
groups of number fields
	\item Hard DL: elliptic curves, curves of genus 2
\end{itemize}

Claim: since finite fields are not-so-hard, why not ditch them and just use EC hardness?

Why finite fields are still interesting
\begin{itemize}
	\item Some protocols prefer them
	\item Pairings! Some cryptographic protocols use pairings:
\[
	e: \mathbb{G} \times \mathbb{G} \to K^\star
\]
	\item Tricks with subgroups of the multiplicative group. \begin{itemize}
		\item we are not necessarily interested in the DLP in the whole
multiplicative group per se
		\item we shall not be annoyed by some uninteresting prime factors
behaving oddly
		\item DL modulo small primes can be handled differently anyway
	\end{itemize}
\end{itemize}

Known generic solutions to DLP. All of the following algorithms are exponential in the bit-size of G:
\begin{itemize}
	\item Enumeration
	\item Baby-step–Giant-step
	\item Pollard $\rho$
	\item Parallel collision search
\end{itemize}

In Nechaev-Shoup [Nec94,Sho97], lower-bound for a generic (black-box) group $G$ with $n = \sqrt{G}$, no discrete logarithm algorithm succeeds in time less than $\mathcal{O}(\sqrt(n))$.

As it turns out, finite fields have faster DLP algorithms than generic groups. First algorithm of this kind: Adleman [Adl79], based on the combination of congruences idea. \newline
Smoothness: a polynomial of degree at most $n$ is $k$-smooth if all its irreducible factors have degree at most $k$. The smoothness is a construction kit situation. Works fine for finite fields, much less for EC.

Overview of Adleman's algorithm (See slides/online). Thanks to the smoothness probability, we can find an optimal choice for the B factor. The overall complexity of Adleman's algorithm is sub-exponential complexity, L(1/2). Consequence, the key size is roughly the square of time.

\subsubsection{L(1/3) Algorithms}

What makes Adleman's algorithm so slow?

\begin{itemize}
	\item Elements created as $g^r \pmod p$ are as large as $p$
	\item For computing individual logarithms, we have no way to take advantage of the fact that $h$ might perhaps have not-so-large bit size.
\end{itemize}

If we could take advantage of $h$ might have a not-so-large bit size, we might imagine a recursive procedure. Getting to the NFS-DL via the FFS.

Outline of algorithm:
\begin{itemize}
	\item Do the setup. Choose a factor base bound $B$
	\item Relation search. Pick pairs $a, b$ for coprime integers $a$ and $b$. Expect $a - bm$ to be a smooth integer. Expect also the ideal $(a-b\alpha)$ to be smooth. Compute Schirokauer maps. Do linear algebra to compute virtual logarithms of factor base elements. Compute individual logarithms.
\end{itemize}

Analysis of runtime of NFS gives $L_p[1/3]$ where $p$ is a prime. Not all $p$ are born equal. Some exceptionally easy $p$ conspicuous. But disguising an easy $p$ as an honest random-looking $p$ is easy: pick $f$ and $g$ to our liking; publish $p$ = Res($f$ , $g$ ). Improvements since NFS. The complexity depends much on how $n$ compares to log $p$ for $\mathbb{F}_{p^n}$.

Covers $L(1/3)$ on large genus curves.

\subsubsection{Benefits of Sieving}
\begin{itemize}
	\item Forced factor in the norm improves the smoothness probability
	\item Reduced lattice basis limits the expense of this constraint on the size of $(a,b)$.
	\item Sieved areas are smaller, each is typically manageable on a single node.
	\item Special-q [DH84] provide an easy division (reduces sieving space), with (almost) stable yield. (Gives reasonable expectations of time computation will take)
\end{itemize}

Implementation tricks such as sieving by vectors and bucket sieving can improve performance.

Black box algorithms favorable for performance reasons. State of the art:
\begin{itemize}
	\item Block Wiedemann algorithm: offers more distribution opportunities
	\item Block Lanczos algorithm: needs fewer matrix operations
\end{itemize}

Current record in $\mathbb{F}_p$: Bouvier, Gaudry, Imbert, Jeljeli, T.: 180dd (600 bits), 2014\newline
Records over binary fields: \begin{itemize}
	\item Record for $\mathbb{F}_{2^p}$ : 1279 bits [Kleinjung14]
	\item Record for $\mathbb{F}_{2^n}$ : 9234 bits (9234 = 2 · 35 · 19) [GKZ14]
\end{itemize}

\subsubsection{Quasi-polynomial DLP in small characteristic} [See Slides]

Conclusion: New algorithm Quasi-polynomial complexity. Relies on heuristic, experimentally checked. RIP small characteristic pairings. This does not affect RSA, nor large characteristic DLP.

\end{document}


text:
\documentclass[masterthesis]{fer}
% Add the option upload to generate the final version which is uploaded to FERWeb
% Dodaj opciju upload za generiranje konačne verzije koja se učitava na FERWeb

\usepackage{blindtext}

%--- THESIS INFORMATION / PODACI O RADU ----------------------------------------

% Title in English / Naslov na engleskom jeziku
\title{Uncomputable Computablity}

% Title in Croatian / Naslov na hrvatskom jeziku
\naslov{Neizračunljiva izračunljivost}

% Thesis number / Broj rada
\brojrada{1234}

% Author / Autor
\author{Ferko Ferovac}

% Mentor
\mentor{Prof.\@ Baltazar}

% Date in English / Datum rada na engleskom jeziku
\date{June, 2021}

% Date in Croatian / Datum rada na hrvatskom jeziku
\datum{lipanj, 2021.}

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

\begin{document}

% Titlepage is automatically generated / Naslovnica se automatski generira
\maketitle

%--- THESIS ASSIGNMENT / ZADATAK -----------------------------------------------

% Thesis assignment is included from external file / Zadatak se ubacuje iz vanjske datoteke
% Enter the filename of the PDF downloaded from FERWeb / Upiši ime PDF datoteke preuzete s FERWeb-a
\zadatak{filename.pdf}

%--- ACKNOWLEDGMENT / ZAHVALE --------------------------------------------------

\begin{zahvale}
  % Write in the acknowledgment / Ovdje upišite zahvale
  Thanks for the tea...
\end{zahvale}

% Page numbering starts from here / Odovud započinje numeriranje stranica
\mainmatter

% Table of contents is automatically generated / Sadržaj se automatski generira
\tableofcontents

%--- INTRODUCTION / UVOD -------------------------------------------------------
\chapter{Introduction}
\label{chp:introduction}

Some of the works we will quote are \cite{6248073,6247753,ghiglia_pritt_phase_unwrapping,hartley2003multiple,4250461,123DCatch}.
The works are quoted here to test the referencing of a conference paper, of a journal paper, of a book, and of a webpage.

\begin{figure}[htb]
  \centering
  \includegraphics[width=0.38\linewidth]{Figures/lenovo_yoga_tab3_pro_front.png}
  \caption{My first figure}
  \label{fig:firstfigure}
\end{figure}

Reference to the first figure \ref{fig:firstfigure} in the middle of a sentence, then before a comma \ref{fig:firstfigure}, and then at the end of a sentence \ref{fig:firstfigure}.
We have just tested if the command \verb|\ref| handles the following interpunction properly.

Now typeset one equation:
\begin{equation}
  \label{eq:firstequation}
  \int_{-\infty}^{+\infty}f(t)\,dt=F(\omega)
\end{equation}
The equation \eqref{eq:firstequation} is my first equation which defines a transform pair $f(t)\ufrek F(\omega)$ or $F(\omega)\uvrem f(t)$.

%-------------------------------------------------------------------------------
\chapter{Materials and Methods}
\label{sec:materialsandmethods}

\Blindtext

%-------------------------------------------------------------------------------
\chapter{Results and Discussion}
\label{sec:results_and_discussion}

\Blindtext

%--- CONCLUSION / ZAKLJUČAK ----------------------------------------------------
\chapter{Conclusion}
\label{chp:conclusion}

\blindtext

%--- REFERENCES / LITERATURA ---------------------------------------------------

% References are automatically generated from the supplied .bib file / Literatura se automatski generira iz zadane .bib datoteke
% Enter the name of the BibTeX file without .bib extension / Upiši ime BibTeX datoteke bez .bib nastavka
\bibliography{references}

%--- ABSTRACT / SAŽETAK --------------------------------------------------------

% Abstract in English
\begin{abstract}
  Enter the abstract in English.

  \blindtext
\end{abstract}

\begin{keywords}
  the first keyword; the second keyword; the third keyword
\end{keywords}

% Sažetak na hrvatskom
\begin{sazetak}
  Unesite sažetak na hrvatskom.

  \blindtext
\end{sazetak}

\begin{kljucnerijeci}
  prva ključna riječ; druga ključna riječ; treća ključna riječ
\end{kljucnerijeci}

%--- APPENDIX / PRIVITCI -------------------------------------------------------

% All following chapters will be denoted with an appendix and a letter / Sva poglavlja koja slijede će biti označena slovom i riječi privitak
\backmatter

\chapter{The Code}

\Blindtext

\end{document}

max_stars_repo_path: Quickstart Examples/master_thesis.tex

max_issues_repo_path: Quickstart Examples/master_thesis.tex

max_forks_repo_path: Quickstart Examples/master_thesis.tex


text:
\section*{Observed mutations table}
\input{Tables/TNFR1mutations}

\newpage
\section*{Tables with applicable missense mutations to TNFRSF1A}
\input{Tables/RelevantTNFR1mutationsTNFA}

\newpage
\input{Tables/RelevantTNFR1mutationsTNFB}

\newpage

\section*{SPVAA Backrub density plots}
\includegraphics[width=\linewidth]{Rosetta_Backrub_Relax_Density_Plots/backrub_Alpha_plot.pdf}
\newpage
\includegraphics[width=\linewidth]{Rosetta_Backrub_Relax_Density_Plots/backrub_Beta_plot.pdf}

\section*{HOPE reports}
\includepdf[pages=-]{Figures/HOPE_results/CYS62GLY.pdf}
\includepdf[pages=-]{Figures/HOPE_results/GLU138ALA.pdf}
\includepdf[pages=-]{Figures/HOPE_results/PHE141ILE.pdf}
\newpage
\section*{R packages}
\input{Tables/R_packages}

max_stars_repo_name: Sylt-CSI/variant-protein-prediction

max_issues_repo_name: Sylt-CSI/variant-protein-prediction

max_forks_repo_name: Sylt-CSI/variant-protein-prediction


text:
\section*{\Large{\textbf{Lecture 1B - Parallel Programming Models and Architectures}} \small{(March 15, 2021)}}
\label{sec:lecture-1B}

\subsection*{\large{\textbf{1B.1. Introduction}}}
\label{ssec:lecture-1B1}

\noindent All \emph{Classical Computers} are now \textbf{parallel}, specially, the modern ones, which support \textbf{parallelism} in \emph{hardware}, through, at least, one \emph{parallel feature}:
\begin{itemize}
    \vspace{-0.1cm}
    \item \emph{Vector Instructions};
    \vspace{-0.1cm}
    \item \emph{Multi-threaded Cores};
    \vspace{-0.1cm}
    \item \textbf{\emph{Multicore Processors}};
    \vspace{-0.1cm}
    \item \emph{Multiple Processors};
    \vspace{-0.1cm}
    \item \emph{Graphics Engines};
    \vspace{-0.1cm}
    \item \emph{Parallel Co-Processors};
\end{itemize}

\noindent This statement does not apply only to \emph{supercomputers}, but even the \emph{smallest} computers, such as \emph{phones}, support many of these features, where, it is necessary to use explicit \textbf{\emph{parallel programming}} to get the most of them.

The \emph{automatic approaches} to \emph{parallelizing} \emph{serial code} \textbf{\emph{cannot}} deal with the shifts in the \emph{algorithm's structures} required for effective \emph{parallelization}.

A \emph{programmer}, in a \emph{modern computing environment}, should not just take advantage of \emph{processors} with \emph{multi-cores}, but, must be able to write \textbf{\emph{scalable}} \emph{applications}, that can take advantage of \textbf{any} amount of \textbf{\emph{parallel hardware}}.

\vspace{0.35cm}

\noindent The feature of \textbf{\emph{scaling}} requires attention to many factors:
\begin{itemize}
    \vspace{-0.2cm}
    \item \emph{Minimization of Data Movement};
    \vspace{-0.2cm}
    \item \emph{Serial Bottlenecks} (including \emph{Locking});
    \vspace{-0.2cm}
    \item Other forms of \emph{Overhead};
\end{itemize}

\noindent Some \textbf{\emph{Parallel Patterns}} can help with this factors, but ultimately, is a responsibility of the \emph{software developer} to produce a \textbf{\emph{good}} \emph{algorithm design}.

In the recent years, it were also made some progress in other \emph{paradigm} of \emph{computing}, known as, \textbf{\emph{Quantum Computing}}, which is also, \emph{inherently} \textbf{\emph{parallel}}, taking advantage of the \textbf{quantum parallelism} offered on the \emph{atomic} and\emph{sub-atomic} levels of \textbf{\emph{elementary particles}}, such as, \textbf{photons}.

\newpage

\subsection*{\large{\textbf{1B.2. Think Parallel}}}
\label{ssec:lecture-1B2}

\noindent The \textbf{\emph{Parallelism}} is an \emph{intuitive} and \emph{common} \emph{human experience}, where, \emph{programmers} naturally accept the concept of \emph{parallel work} via a \emph{group of workers}, often with \emph{specializations}, in order to achieve a \emph{major goal}.

\vspace{0.35cm}

\noindent Some \emph{important} and \emph{relevant} notions are:
\begin{itemize}
    \vspace{-0.2cm}
    \item \textbf{\emph{Serialization}}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item Act of putting some set of operations into a specific order;
    \end{itemize}
    \vspace{-0.2cm}
    \item \textbf{\emph{Serial Semantics}}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item \emph{Semantics} used even though the \emph{hardware} was naturally \emph{parallel};
    \end{itemize}
    \vspace{-0.2cm}
    \item \textbf{\emph{Serial Illusion}}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item \emph{Mental model} of a \emph{computer} executing operations, \emph{sequentially};
        \item Has the problem of programmers came to depend on it too much;
    \end{itemize}
\end{itemize}

\noindent The \textbf{\textit{Serialization}} has its own \emph{benefits}, such as, if someone reads a piece of \emph{serial code} from top to bottom, will also be able to understand the \emph{temporal order} of operations from the structure of the \emph{source code}.

It helps that modern \emph{programming languages} have evolved to use some \emph{structured} \emph{control flow} to emphasize this aspect of \emph{serial semantics}.

Unless it was intentionally injected \emph{randomness}, the \emph{serial programs} are \textbf{\emph{deterministic}}, doing always the same operations in the same order, giving the \emph{same answer}, every time you run them with the \emph{same inputs}.

The \textbf{\emph{Determinism}} is useful for \emph{debugging}, \emph{verification}, and \emph{testing}, but the \emph{deterministic behavior} is not a natural characteristic of \emph{parallel programs}.

Generally speaking, the \emph{timing} of \emph{task execution} in \emph{parallel programs}, in particular the \emph{relative timing}, is often \textbf{\emph{Non-Deterministic}}.

Given that \emph{parallelism} is necessary for \emph{performance}, it would be useful to find an effective approach to \emph{parallel programming} that retains as many of the benefits of \emph{serialization} as possible, yet is also similar to existing practice.

Some of the known \textbf{\emph{Parallel Patterns}} provide \emph{structure} but they can also avoid the existing \textbf{Non-Determinism}, with a few easily visible exceptions where it is \emph{unavoidable} or \emph{necessary} for a better \emph{performance}.

When eliminating \emph{unnecessary} \emph{serialization}, leading to \emph{poor performance}, the current \emph{programming tools} may have many \textbf{\emph{serial traps}} built into them.

\newpage

\noindent The \textbf{\emph{serial traps}} are constructs that make, often \emph{unnecessary}, their \emph{serial assumptions} and they can also exist in the \emph{design} of \emph{algorithms} and in the abstractions used, to estimate the respective \emph{complexity} and \emph{performance}.

\vspace{0.35cm}

\noindent Often, there are two main steps to \emph{think} and \emph{program} in \emph{parallel}:
\begin{enumerate}
    \vspace{-0.2cm}
    \item Learning to recognize \textbf{\emph{serial traps}};
    \vspace{-0.2cm}
    \item Programming in terms of \textbf{\emph{Parallel Patterns}} that capture their best practices and using \emph{efficient} implementations of these \emph{patterns};
\end{enumerate}

\noindent The most difficult part of learning to \emph{program} in \emph{parallel} is \emph{recognizing} and \emph{avoiding} \textbf{\emph{serial traps}} (i.e., \emph{assumptions} of \emph{serial ordering}).

These assumptions are so \emph{common} that, their existence is unnoticed and most of the \emph{programming languages} \emph{unnecessarily} overconstrain the \emph{execution order}, making the \emph{parallel execution} of their \emph{programs} to be difficult.

\emph{Parallelizing} \emph{serial} \emph{programs} written using \emph{iteration} \emph{constructs}, requires to be \emph{recognized} the \emph{semantics} used and \emph{convert} them to the appropriate \emph{parallel structure} and even better would be to \emph{design} \emph{programs} using them.

\vspace{0.5cm}

\subsection*{\large{\textbf{1B.3. Vocabulary and Notation}}}
\label{ssec:lecture-1B3}

\noindent The two fundamental components of algorithms are \textbf{\emph{tasks}} and \textbf{\emph{data}}, where a \textbf{\emph{task}} operates on \textbf{\emph{data}}, either \emph{modifying} it in place or \emph{creating} new \textbf{\emph{data}}.

In a \emph{parallel computation}, the \emph{multiple tasks} need to be \emph{managed} and \emph{coordinated}, where, in particular, \textbf{\emph{dependencies}} between \textbf{\emph{tasks}} need to be \emph{respected}, regarding their particular \emph{ordering} of \emph{execution}.

\vspace{0.35cm}

\noindent The \textbf{\emph{dependencies}} are often but not always associated with the transfer of \textbf{\emph{data}}, between \textbf{\emph{tasks}} and can be categorised as the following two kinds:
\begin{itemize}
    \vspace{-0.2cm}
    \item \textbf{\emph{Data Dependency}}:
    \begin{itemize}
        \vspace{-0.2cm}
        \item \textbf{\emph{Tasks}} that \textbf{\emph{cannot}} be executed, before some of its required \textbf{\emph{data}} be ready, which can be generated by other \textbf{\emph{tasks}};
    \end{itemize}
    \vspace{-0.2cm}
    \item \textbf{\emph{Control Dependency}}:
    \begin{itemize}
        \vspace{-0.2cm}
        \item \emph{Events} or \emph{side effects}, such as, the ones happening due to some \emph{I/O operations}, which need to be \emph{ordered}, in time;
    \end{itemize}
\end{itemize}

\newpage

\noindent For the \emph{task management}, there is the \textbf{\emph{fork-join}} \emph{pattern}, where can exist:
\begin{itemize}
    \vspace{-0.2cm}
    \item \textbf{Fork Points}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item New \emph{serial} \emph{control flows} are created, by \emph{splitting} an existing \emph{serial} \emph{control flow}, previously executed;
    \end{itemize}
    \vspace{-0.2cm}
    \item \textbf{Join Points}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item Two \emph{separate} executed \emph{serial} \emph{control flows} which are \emph{synchronized}, by \emph{merging} them together in one \emph{serial} \emph{control flow};
    \end{itemize}
\end{itemize}

\noindent In a \emph{single} \emph{serial} \emph{control flow}, the \textbf{\emph{tasks}} are \emph{ordered}, according to the \emph{serial semantics}, and due to the implicit \emph{serial} \emph{control flow} before and after these \emph{points}, the \textbf{\emph{control dependencies}} are also needed between \textbf{\emph{fork}} and \textbf{\emph{join}} \textbf{\emph{points}} and the \textbf{\emph{tasks}} that \emph{precede} and \emph{follow} them, respectively.

\vspace{0.5cm}

\subsection*{\large{\textbf{1B.4. Simple Approaches to Parallelization}}}
\label{ssec:lecture-1B4}

\noindent Some simple approaches for \emph{parallelization} are:
\begin{itemize}
    \item \textbf{\emph{Distributed Memory}}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item \emph{Parallel system} based on \emph{processors} \textbf{\emph{linked}} with a \emph{fast network};
        \item The \emph{processors} \textbf{\emph{communicate}} with each other, via \emph{messages};
    \end{itemize}
    \item \textbf{\emph{Owner Computes}}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item \emph{Distribute} the \textbf{\emph{data}} \emph{elements} to \emph{processors};
        \item Each \emph{processor} \emph{updates} its own \textbf{\emph{data}} \emph{elements};
    \end{itemize}
    \item \textbf{\emph{Single Program, Multiple Data}} (\textbf{\emph{SPMD}}):
    \vspace{-0.2cm}
    \begin{itemize}
        \item All \emph{machines} run the \textbf{\emph{same}} \emph{program} on \emph{independent} \textbf{\emph{data}};
        \item The \emph{dominant} form of \emph{parallel computing};
    \end{itemize}
\end{itemize}

\noindent For \textbf{\emph{Shared Memory}}, the \emph{latency} of \emph{communication} between the \emph{processors} is \emph{low}, while, for the \textbf{\emph{Distributed Systems}}, occurs the opposite, with \emph{high} \emph{latencies} on the \emph{communications} between the \emph{processors}, where this \emph{drawback} can be solved, by keeping some \textbf{\emph{data}} \emph{elements} of other \emph{processors} \emph{locally}, with what is called \textbf{\emph{ghost cells}}, \emph{decreasing} a \emph{latency} of its \emph{communications}.

\newpage

\subsection*{\large{\textbf{1B.5. Flynn's Characterization}}}
\label{ssec:lecture-1B5}

\noindent The \emph{parallel processors} can be divided into categories based on whether they have \emph{multiple} \textbf{\emph{flows of control}}, \emph{multiple} \textbf{\emph{streams of data}}, or on both:
\begin{itemize}
    \vspace{-0.2cm}
    \item \textbf{\emph{Single Instruction, Single Data}} (\textbf{\emph{SISD}}):
    \begin{itemize}
        \vspace{-0.2cm}
        \item \emph{Standard} \emph{non-parallel} \emph{processor}, often referred as \emph{scalar processor};
        \item The \emph{individual} \emph{performance} of \emph{scalar processing} is important, since if it is slow, it can end up \emph{dominating} the \emph{global performance};
    \end{itemize}
    \item \textbf{\emph{Single Instruction, Multiple Data}} (\textbf{\emph{SIMD}}):
    \begin{itemize}
        \vspace{-0.2cm}
        \item \emph{Single} \emph{task} \emph{executing} simultaneously on \emph{multiple} \emph{elements} of \emph{data};
        \item The number of \emph{data elements} in a \emph{SIMD}'s \emph{operation} can vary from a small number, such as the 4 to 16 elements in short \emph{vector instructions}, to thousands, as in \emph{streaming vector processors};
        \item The \emph{SIMD processors} are also known as \emph{array processors}, since consist on an \emph{array} of \emph{functional units} with a \emph{shared controller};
    \end{itemize}
    \item \textbf{\emph{Multiple Instruction, Single Data}} (\textbf{\emph{MISD}}):
    \begin{itemize}
        \vspace{-0.2cm}
        \item Not particularly useful and is not used;
    \end{itemize}
    \item \textbf{\emph{Multiple Instruction, Multiple Data}} (\textbf{\emph{MIMD}}):
    \begin{itemize}
        \vspace{-0.2cm}
        \item Separated \emph{streams} of \textbf{\emph{instructions}} and \textbf{\emph{tasks}}, each one with its own \emph{flow of control}, operating on separated \textbf{\emph{data}} \emph{elements};
        \item Defines \emph{multiple cores} in a \emph{single processor}, \emph{multiple processors} in a \emph{single computer}, and \emph{multiple computers} in a \emph{single cluster};
        \item Represents a \textbf{\emph{heterogeneous computer}}, as \emph{multiple processors} using \emph{different} \emph{architectures}, present in the \emph{same} \emph{computer system};
        \item An example would be a \emph{host processor} and a \emph{co-processor} with \emph{different} sets of \textbf{\emph{instructions}} and \textbf{\emph{tasks}};
    \end{itemize}
\end{itemize}

\newpage

\subsection*{\large{\textbf{1B.7. Software Taxonomies}}}
\label{ssec:lecture-1B7}

\noindent Some commonly used \emph{Software Taxonomies} are the following ones:
\begin{itemize}
    \vspace{-0.2cm}
    \item \textbf{\emph{Data Parallel}} (\textbf{\emph{SIMD}}):
    \vspace{-0.2cm}
    \begin{itemize}
        \item \emph{Parallelism} that is a result of \emph{identical} \emph{operations} being applied \emph{concurrently} on \emph{different} \emph{data elements} (e.g., \emph{matrix algorithms});
        \item Difficult to apply it to some \emph{complex problems};
    \end{itemize}
    \vspace{-0.2cm}
    \item \textbf{\emph{Single Program, Multiple Data}} (\textbf{\emph{SPMD}}):
    \vspace{-0.2cm}
    \begin{itemize}
        \item A \emph{single} \emph{application} is executing across \emph{multiple} \emph{processes/threads} on a \emph{MIMD} \emph{architecture};
        \item Most processes execute the same code but do not work in \emph{lock-step};
        \item \emph{Dominant} form of \emph{parallel programming};
    \end{itemize}
\end{itemize}

\subsection*{\large{\textbf{1B.8. Shared Memory (SM)}}}
\label{ssec:lecture-1B8}

\begin{itemize}
    \item \textbf{\emph{Attributes}}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item Has \emph{global} \emph{memory space};
        \item A \emph{processor} use its own \emph{cache} for a part of \emph{global} \emph{memory space};
        \item The \emph{consistency} of the \emph{cache} is maintained by \emph{hardware};
    \end{itemize}
    \item \textbf{\emph{Advantages}}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item \emph{User-friendly} \emph{programming} techniques (\emph{OpenMP} and \emph{OpenACC});
        \item Has \emph{low} \emph{latency} for \emph{data sharing} between \textbf{\emph{tasks}};
    \end{itemize}
    \item \textbf{\emph{Disadvantages}}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item Has \emph{global} \emph{memory} \emph{space-to-CPU} path may be a \emph{bottleneck};
        \item Has \emph{Non-Uniform Memory Access} (\emph{NUMA});
        \item The \emph{programmer} is responsible for the details of \emph{synchronization};
    \end{itemize}
\end{itemize}

\newpage

\subsection*{\large{\textbf{1B.9. Distributed Memory (DM)}}}
\label{ssec:lecture-1B9}

\begin{itemize}
    \item \textbf{\emph{Attributes}}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item The \emph{memory} is \emph{shared} amongst \emph{processors} via \emph{message passing};
    \end{itemize}
    \item \textbf{\emph{Advantages}}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item The \emph{memory} \emph{scales} based on the number of \emph{processors};
        \item The access to a \emph{processor}'s own \emph{memory} is \emph{fast};
        \item Is \emph{cost effective};
    \end{itemize}
    \item \textbf{\emph{Disadvantages}}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item Is \emph{error prone};
        \item The \emph{programmer} is responsible for the details of \emph{communication};
        \item The \emph{complex} \emph{data structures} may be difficult to \emph{distribute};
    \end{itemize}
\end{itemize}

\subsection*{\large{\textbf{1B.10. Software/Hardware Models}}}
\label{ssec:lecture-1B10}

\noindent The \emph{Software} and \emph{Hardware} models \textbf{\emph{do not}} need to match:

\vspace{-0.2cm}
\begin{itemize}
    \item \textbf{\emph{Distributed Memory}} \emph{software} on \textbf{\emph{Shared Memory}} \emph{hardware}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item \textbf{\emph{Message Passing Interface}} (\textbf{\emph{MPI}}), which is designed for \textbf{\emph{Distributed Memory}} (\textbf{\emph{DM}}) \emph{hardware} but is also available on \textbf{\emph{Shared Memory}} (\textbf{\emph{SM}}) \emph{systems};
    \end{itemize}
    \item \textbf{\emph{Shared Memory}} \emph{software} on \textbf{\emph{Distributed Memory}} \emph{hardware}:
    \vspace{-0.2cm}
    \begin{itemize}
        \item \textbf{\emph{Remote Memory Access}} (\textbf{\emph{RMA}}) included within \textbf{\emph{MPI-3}};
        \item \textbf{\emph{Partitioned Global Address Space}} (\textbf{\emph{PGAS}}) \emph{languages}:
        \begin{itemize}
            \item \textbf{\emph{Unified Parallel C}} (extension to \textbf{ISO C 99});
            \item \textbf{\emph{Coarray Fortran}} (\textbf{Fortran 2008});
        \end{itemize}
    \end{itemize}
\end{itemize}

\newpage

\subsection*{\large{\textbf{1B.11. Difficulties of Parallelization}}}
\label{ssec:lecture-1B11}

\noindent There are some common difficulties on \textbf{\emph{Parallelization}}, such as:

\vspace{-0.2cm}
\begin{itemize}
    \item The \textbf{\emph{serialization}} causes \textbf{\emph{bottlenecks}};
    \item The \textbf{\emph{workload}} is not \emph{distributed};
    \item The \textbf{\emph{debugging}} is \textbf{\emph{hard}};
    \item The \textbf{\emph{serial}} approach \textbf{does not} \textbf{\emph{parallelize}};
\end{itemize}

\subsection*{\large{\textbf{1B.12. Performance}}}

\noindent Often, one of the most common \textbf{\emph{serial traps}} is the habit of discussing the \emph{performance} of the \emph{algorithms}, focusing only on the \emph{minimization} of the \emph{total amount} of \emph{computational work} to be done, in \emph{parallel programming}.

\vspace{0.35cm}

\noindent From this common habit, comes two main problems, such as:
\vspace{-0.2cm}
\begin{itemize}
    \item The \emph{computation} itself, may not be the \textbf{\emph{bottleneck}}, since, the \emph{access} to \emph{memory} or its \emph{communication} may constrain the \emph{performance};
    \vspace{-0.1cm}
    \item The \emph{potential} for \emph{scaling performance} on a \emph{parallel computer} is always constrained by the \emph{algorithm's span}, which is the \emph{execution time} needed for the longest \emph{chain of tasks} that, must be performed \emph{sequentially};
\end{itemize}


text:
\section{Related and Future Work}
\label{sec:final}

\textbf{Related Work}.  Our work builds upon the well-known Schnorr-Euchner
algorithm for solving the closest vector problem.  Prior to developing BLT, we
used the closest-vector solver in
\texttt{fplll}~\cite{DBLP:conf/codcry/HanrotPS11} to solve problems.  It uses
the $L^2$ norm, and thus is not a decision procedure.  However, we found that
it could often find satisfying assignments at quality levels greater than $60$
despite the lack of completeness.

\texttt{LattE} is a program for enumerating lattice points in a rational
polytope \cite{DeLoera2004}. This is asking strictly more than the question
we've discussed. \texttt{LattE} is competitive with commercial branch-and-bound
solvers, the same solvers which perform poorly on the DCT problems in section
\ref{sec:jpeg}. We attempted to evaluate \texttt{LattE} on our DCT problems,
but found that it would crash given a 16 GB memory limit.

\textbf{Future Development}.
We are still working on developing BLT, and have plans to continue
testing it on a wider variety of challenge problems.  We plan to
enable the $\linf$ distance calculation to use exact arithmetic.  We
also plan to explore ways to solve problems with one-sided bounds via
heuristics, and ways to infer unsatisfiable subsets of constraints so
that BLT can be integrated into an SMT solver.  Finally, we would like
to integrate techniques from SAT community such as
conflict-driven-clause learning into the ILP search performed by BLT.
The later should help improve its performance on hard problem instances.

More broadly, it also seems interesting to explore how the calculus and
heuristics that BLT uses can be integrated into other ILP solvers, such as those
based on cutting planes (e.g.~\cite{DBLP:journals/jar/JovanovicM13}).  Those algorithms
are able to work on more general problems as they do not require explicit upper
and lower bounds for all linear expressions.  On the other hand, BLT appears
to be more effective at making effective decisions within the search.

\textit{Acknowledgements}. The authors would like to thank Dejan Jovanovi\'{c},
Grant Passmore, and the reviewers for comments that helped improve this paper.

max_stars_repo_name: benjaminfjones/blt

max_issues_repo_name: benjaminfjones/blt

max_forks_repo_name: benjaminfjones/blt


text:
\documentclass{article}
\usepackage{amsmath}
% if you need to pass options to natbib, use, e.g.:
% \PassOptionsToPackage{numbers, compress}{natbib}
% before loading nips_2017
%
% to avoid loading the natbib package, add option nonatbib:
% \usepackage[nonatbib]{nips_2017}

%\usepackage{nips_2017}

% to compile a camera-ready version, add the [final] option, e.g.:
\usepackage[final]{nips_2017}

\usepackage[utf8]{inputenc} % allow utf-8 input
\usepackage[T1]{fontenc}    % use 8-bit T1 fonts
\usepackage{hyperref}       % hyperlinks
\usepackage{url}            % simple URL typesetting
\usepackage{booktabs}       % professional-quality tables
\usepackage{amsfonts}       % blackboard math symbols
\usepackage{nicefrac}       % compact symbols for 1/2, etc.
\usepackage{microtype}      % microtypography
\usepackage{subfig}
\usepackage{cleveref}
\usepackage{graphicx}
\usepackage{siunitx}

\graphicspath{ {hw3/imgs/} }

\title{Computer Vision 1: Harris Corner Detector and Optical Flow}

\author{
	Gabriele Bani \\
	11640758 \\
  \texttt{gabriele.bani@student.uva.nl} \\
  %% examples of more authors
  \And
  	Andrii Skliar \\
  11636785 \\
  \texttt{andrii.skliar@student.uva.nl} \\
}

\begin{document}
\maketitle

\section*{Introduction}

In this homework we explore various algorithms for corner detection and optical flow estimation.

\section{Harris Corner Detector}

\begin{figure}[h]
    \centering
    \caption{Results for Harris Corner detection}
    \subfloat[Image derivatives along $x$ direction $I_x$]{{
    	\includegraphics[width=0.5\textwidth]{toy_harris_Ix.png}
    }}\\
    \subfloat[Image derivatives along $y$ direction $I_y$]{{
    	\includegraphics[width=0.5\textwidth]{toy_harris_Iy.png}
    }}\\
    \subfloat[Detected corners (marked by red points)]{{
    	\includegraphics[width=0.5\textwidth]{toy_harris_corners.jpg}
    }}
\label{fig:harris1}
\end{figure}

\begin{figure}[h]
    \centering
    \caption{Results for Harris Corner detection}
    \subfloat[Image derivatives along $x$ direction $I_x$]{{
    	\includegraphics[width=0.5\textwidth]{ping_harris_Ix.png}
    }}\\
    \subfloat[Image derivatives along $y$ direction $I_y$]{{
    	\includegraphics[width=0.5\textwidth]{ping_harris_Iy.png}
    }}\\
    \subfloat[Detected corners (marked by red points)]{{
    	\includegraphics[width=0.5\textwidth]{ping_harris_corners.jpg}
    }}
\label{fig:harris2}
\end{figure}

\begin{figure}[h]
    \centering
    \caption{Results for Harris Corner detection rotation}
    \subfloat[No rotation]{{
    	\includegraphics[width=0.4\textwidth]{toy_harris_corners.jpg}
    }}
    \subfloat[90 degree rotation]{{
    	\includegraphics[width=0.4\textwidth]{toy_harris_corners_rot.jpg}
    }}\\
    \subfloat[No rotation]{{
    	\includegraphics[width=0.4\textwidth]{ping_harris_corners.jpg}
    }}
    \subfloat[90 degree rotation]{{
    	\includegraphics[width=0.4\textwidth]{ping_harris_corners_rot.jpg}
    }}
\label{fig:harris_rot}
\end{figure}

\begin{figure}[h]
    \centering
    \caption{Harris corners with varying sigma and threshold}
    \subfloat[$\sigma$ 0.5, $\threshold$ 100]{{
    	\includegraphics[width=0.5\textwidth]{harris_corners_05_100.jpg}
    }}
    \subfloat[$\sigma$ 0.5, $\threshold$ 400]{{
    	\includegraphics[width=0.5\textwidth]{harris_corners_05_400.jpg}
    }}\\
    \subfloat[$\sigma$ 1, $\threshold$ 100]{{
    	\includegraphics[width=0.5\textwidth]{harris_corners_1_100.jpg}
    }}
    \subfloat[$\sigma$ 1, $\threshold$ 400]{{
    	\includegraphics[width=0.5\textwidth]{harris_corners_1_400.jpg}
    }}
\label{fig:harris_params}
\end{figure}

You can observe obtained results in \cref{fig:harris1} and \cref{fig:harris2}. We have tried different values of sigma and threshold and, as we found out, they influence the final result quite heavily. You can see results with different parameters in \cref{fig:harris_params}.

Lowering the threshold makes more points to be considered as corners and in many cases we would like to avoid it, because this makes results noisy. We have found out, that with larger $\sigma$ algorithm tends to detect more points and we need larger threshold to filter them out.

After searching for perfect threshold, we have concluded, that for $pingpong$ images threshold should be fairly low - $10$, while for $person\_toy$ images it should be larger - $400$ worked out pretty well for us. In both cases, we were using value of $\sigma=1$, which works out pretty well for us.

Also, as you can see in \cref{fig:harris_rot}, Harris algorithm is indeed rotation-invariant (it will also be discussed in the next question).
\begin{enumerate}
    \item Is the algorithm rotation-invariant?\\
    Yes, it is rotation-invariant, because we are not looking at the whole image, but detecting corners using eigenvalue-decomposition of the patch, which means, that when image is rotated, patches will change their orientation, and this will change the shape of the neighbourhood, but eigenvalues will stay the same and this makes algorithm rotation invariant. If we would look at the whole image at one to detect corners, that would make it sensitive to rotation, but as long as we don't, it is invariant.

    \item How do Shi and Tomasi define cornerness?\\
    $H = min(\lambda_1, \lambda_2)$, which according to their experiments, is supposed to be a better criteria for cornerness.

    \item Do we need to calculate the eigen decomposition of the image or the patches?\\
    We need to calculate the eigen decomposition of the patches, because to do so, we need to calculate convolution between Gaussian filter and window centered at the current pixel. Also, we could do it with the whole image as a window, but this way we would only be able to calculate cornerness for one pixel right in the center of the image and that wouldn't make sense, because we need to find pixels, for which cornerness is largest in a certain window.

    \item In the following scenarios, what could be the relative cornerness values assigned by Shi and Tommasi?
    \begin{itemize}
        \item (a) Both eigenvalues are near 0.\\
        Cornerness value will be 0. This pixel is not corner.
        \item (b) One eigenvalue is big and the other is near zero.\\ Cornerness value will be near 0. This pixel is not corner.
        \item (c) Both eigenvalues are big.\\
        Cornerness value will be large. This pixel has a high chance of being corner.
    \end{itemize}

\end{enumerate}

\section{Optical Flow with Lucas-Kanade Algorithm}
You can observe obtained results in \cref{fig:lucas}.

\begin{itemize}
    \item At what scale those algorithms operate; i.e local or global? \\
    Lukas-Kanade operates on a local scale, because it is based on the asumption regarding that pixel being examined has approximately constant optical flow in a neighbourhood and that allows for optical flow equation to hold in that neighbourhood.\\
    Horn-Schunck operates on a global scale, because it uses the assumption about that flow over the whole image is smooth and minimizes flow as a global energy functional.

    \item How do they behave on ﬂat regions?
    \\
    Lukas-Kanade will perform worse due to the fact, that it is operating in a local neighborhood, which is flat and therefore has small gradient. However, Horn-Schunck should perform much better, because it operates on a global scale and can therefore overcome the problem of a region being flat by taking information about changes in the whole image into account.

\end{itemize}

\begin{figure}[h]
    \centering
\caption{Optical flow in sphere and synthetic image}
\subfloat{{
	\includegraphics[width=0.9\textwidth]{sphere.png}
}}\\
\subfloat{{
	\includegraphics[width=0.9\textwidth]{synth.png}
}}
\label{fig:lucas}
\end{figure}

\section{Feature Tracking}

\begin{enumerate}
    \item Why do we need feature tracking while we can detect features for each and every frame?\\
    In most of the cases, feature detection is much more expensive, than tracking, which can be done in real-time, and that might be the first reason. The other reason is that, for example, for object detection, tracking is much more robust to changes in viewpoint and therefore might perform better. Also, tracking can be more robust to overlapping objects and can predict the movement of the points in the image.
\end{enumerate}

\section*{Conclusion}

In this homework we have explored various algorithms for corner detection and optical flow estimation.

\end{document}

max_stars_repo_name: askliar/computer-vision

max_issues_repo_name: askliar/computer-vision

max_forks_repo_name: askliar/computer-vision


text:
\documentclass{beamer}
\usepackage[latin1]{inputenc}
\usepackage{ifthen}
\usepackage{alltt}
\usepackage{MnSymbol}
\usepackage[style=philosophy-modern]{biblatex}
% Package biblatex: '\bibliography' must be given in preamble.
\bibliography{../cites}

\usecolortheme{dove}
\definecolor{Red}{rgb}{1,0,0}
\definecolor{Blue}{rgb}{0,0,1}
\definecolor{Green}{rgb}{0,1,0}
\definecolor{magenta}{rgb}{1,0,.6}
\definecolor{lightblue}{rgb}{0,.5,1}
\definecolor{lightpurple}{rgb}{.6,.4,1}
\definecolor{gold}{rgb}{.6,.5,0}
\definecolor{orange}{rgb}{1,0.4,0}
\definecolor{hotpink}{rgb}{1,0,0.5}
\definecolor{newcolor2}{rgb}{.5,.3,.5}
\definecolor{newcolor}{rgb}{0,.3,1}
\definecolor{newcolor3}{rgb}{1,0,.35}
\definecolor{White}{rgb}{1,1,1}
\definecolor{darkgreen1}{rgb}{0, .35, 0}
\definecolor{darkgreen}{rgb}{0, .6, 0}
\definecolor{darkblue}{rgb}{0, 0, .6}
\definecolor{darkred}{rgb}{.75,0,0}
\newcommand{\putat}[3]{\begin{picture}(0,0)(0,0)\put(#1,#2){#3}\end{picture}}
\newcommand{\gnm}[1]{\text{\gntermfont{#1}}}

\newcommand{\mapstos}[0]{\stackrel{\star}{\mapsto}}
\newcommand{\mapstoc}[0]{\stackrel{!}{\mapsto}}

\newcommand*{\newblock}{}
\newcommand{\pred}[2]{{#1}\;\mathit{#2}}
\newcommand{\rel}[2]{{#1}\;\longleftrightarrow\;{#2}}
\newcommand{\predand}[2]{{#1}\;\mathit{#2}\quad}
\newcommand{\Inf}[3][!*NEVER USED ARGUMENT*!]{%
  \ifthenelse{\equal{#1}{!*NEVER USED ARGUMENT*!}}{%
    \dfrac{#2}{#3}
  }{%
    \dfrac{#2}{#3}(#1)
  }%
}
\newcommand{\subst}[3]{\{{#2}/{#1}\}#3}
\newcommand{\te}[1]{{\textnormal{\texttt{#1}}}}
\newcommand{\tearg}[2]{{\texttt{#1(}#2{\texttt{)}}}}
\newcommand{\vdasharrow}[0]{\vdash\!\!\!\!\filledtriangleright}
\newcommand{\ok}[1]{{#1}\;\small{\textbf{ok}}}
\newcommand{\decs}[2]{\small{{#1}\;\textbf{decs}}\;{#2}}
\newcommand{\iftc}[3]{\texttt{if(}{#1}\texttt{) then }{#2}\texttt{ else }{#3}}
\newcommand{\whiletc}[2]{\texttt{while(}{#1}\texttt{)}{#2}}
\newcommand{\returntc}[1]{\texttt{return(}{#1}\texttt{);}}
\newcommand{\blocktc}[1]{\texttt{\{}{#1}\texttt{\}}}
\newrobustcmd*{\footlessfullcite}{\AtNextCite{\renewbibmacro{title}{}\renewbibmacro{in:}{}}\footfullcite}
\xdefinecolor{olive}{cmyk}{0.64,0,0.95,0.4}
\useoutertheme[subsection=false]{smoothbars}
\usetheme{Singapore}
\title[OutsideIn(X) Formalised in Agda]{\textbf{Formalising GHC's Type System}\\$\textsc{OutsideIn}(X)$ encoded in Agda}
\author{Thesis A Presentation \\ Liam O'Connor (z3253158)}
\institute{CSE, UNSW (also NICTA)}
\date{Tue 24 April 2012}
\begin{document}
\begin{frame}
\titlepage
\end{frame}
\section{The Problem}
\subsection{Introduction}
\begin{frame}{Haskell}

\putat{210}{-70}{\includegraphics[width=5em]{haskell_logo.pdf}}
	\begin{itemize}
		\item Strongly, statically typed purely functional language\footcite{Anonymous:2010we}

		\medskip

		\item Getting stronger all the time:
		\begin{itemize}
		   \item GADTs \footcite{Schrijvers:2009jg}
		   \item Type Families  \footcite{citeulike:9320233}
		   \item $n$-Rank Types \footcite{Jones:2007dr}
		   \item Data Kinds, Polymorphic Kinds  \footcite{Yorgey:2012:GHP:2103786.2103795}
		\end{itemize}
	\end{itemize}

\end{frame}

\subsection{Problem}
\begin{frame}{The Problem}
	\begin{itemize}
	\item These type system extensions are formalised in isolation.
	\pause
	\item Implementing them \emph{together} in the one compiler can be difficult, and can also lead to many problems (inference, soundness etc.)
	\pause

	\medskip

	$\Longrightarrow$ we need a unified formalisation for all of them!
	\end{itemize}
\end{frame}
\begin{frame}{Partial Solution}
	\begin{itemize}
	\item $\textsc{OutsideIn}(X)$ is a (mostly rigorous) formalisation of the type checking and inference system currently in use for GHC.\footcite{Vytiniotis:2011:OMT:2139531.2139533}
	\pause
	\item \textbf{It's not enough}.

     New extensions are already being developed that ignore it! \footcite{Yorgey:2012:GHP:2103786.2103795}
	\end{itemize}
\end{frame}

\subsection{Agda}
\begin{frame}{Agda}
	Agda is a programming language that is:
	\begin{itemize}
		\item \textbf{Dependently Typed}\footcite{MartinLof:1984tr}
		\pause
		\item \textbf{Total} - missed pattern cases, general recursion not allowed.
		\pause

		$\therefore$ doubles as a proof assistant!\footcite{Howard:1980vs}
	\end{itemize}
\end{frame}
\subsection{Related Work}
\begin{frame}{Related Work}
	Unfortunately, not much.
	\begin{itemize}
		\item ML's (similar) type system was formalised for soundness proofs in Coq. \footcite{Dubois00provingml}
		\pause
		\item Nothing notable in Agda
		\item $\textsc{OutsideIn}(X)$ is new research $\Rightarrow$ not much work on it.
	\end{itemize}
\end{frame}
\section{Initial Steps}
\subsection {Rest of the Semester}
\begin{frame}{Initial Steps}
	\begin{itemize}
		\item Experiment with different encodings in Agda
		\item Not based on all of $\textsc{OutsideIn}(X)$, but a subset that is similar to $\textsc{HM}$.
		\item Starting with the \emph{constraint generation} part of type \emph{inference.}
		\item Constraints are generated, \emph{then} solved. No interleaving.
	\end{itemize}
\end{frame}
\begin{frame}{Parameterisation}
\textbf{Problem:} \textsc{OutsideIn}(X) is parameterised by the language/constraint system used.
			\pause
		$\Longrightarrow$ Ignoring this for now
\end{frame}
\subsection {Representing Names}
\begin{frame}{Representing Names}
	\pause
	\begin{center}
		\textbf{De Bruijn Indices}
		\begin{displaymath}
			(\Lambda x.\ \Lambda y.\ x\ y) \leadsto (\Lambda.\ \Lambda.\ 0\ 1 ) \; \color{white}{\checkmark}
		\end{displaymath}\pause
		or
		\begin{displaymath}
			(\Lambda x.\ \Lambda y.\ x\ y) \leadsto (\Lambda.\ \Lambda.\ 1\ 0 ) \; \pause \color{darkgreen}{\checkmark}
		\end{displaymath}
	\end{center}
\end{frame}
\begin{frame}{Dealing with Fresh Variables}
	\begin{displaymath}
		\Inf{\predand{\alpha}{\textbf{fresh}} \Gamma, (x : \alpha) \vdasharrow e : \tau \leadsto C}{\Gamma \vdasharrow \lambda x.\ e : \alpha \rightarrow \tau \leadsto C}{\textsc{Abs}}
	\end{displaymath}
\end{frame}
\begin{frame}{Dealing with Fresh Variables}
	View type as input, only constraint as output:
	\begin{displaymath}
		\Inf{\predand{\alpha}{\textbf{fresh}}  {\color{darkred}\predand{\beta}{\textbf{fresh}}} \Gamma, (x : \alpha) \vdasharrow e : {\color{darkred}\beta} \leadsto C}{\Gamma \vdasharrow \lambda x.\ e : {\color{darkred}\tau} \leadsto C \land {\color{darkred} \tau \sim (\alpha \rightarrow \beta) }}{\textsc{Abs}}
	\end{displaymath}
\end{frame}
\begin{frame}{Dealing with Fresh Variables}	Extend the constraint language to include quantifiers for ``fresh'' variables \footcite{Pottier:2005ue}:
	\begin{displaymath}
		\Inf{\Gamma_{\color{darkred}{\uparrow\uparrow}}, (x : {\color{darkred}{0}} ) \vdasharrow e : {\color{darkred} 1} \leadsto C}{\Gamma \vdasharrow \lambda x.\ e : \tau \leadsto {\color{darkred}{\exists.\ \exists.\ }}C \land \tau \sim {\color{darkred}(0 \rightarrow 1)}}{\textsc{Abs}}
	\end{displaymath}
\end{frame}
\subsection {Indexing Constraint Types}
\begin{frame}
	\begin{displaymath}
		\Inf{C : \text{Constraint}}{\exists. C : \text{Constraint}}{\exists\textsc{-Con}}
	\end{displaymath}
\end{frame}
\begin{frame}
	Index by number of available variables\footcite{Morris04exploringthe} \footcite{McBride:2003bg}:
	\begin{displaymath}
		\Inf{C : \text{Constraint}(s(n))}{\exists. C : \text{Constraint}(n)}{\exists\textsc{-Con}}
	\end{displaymath}
	\pause
	\begin{displaymath}
		\Inf{\tau_1 : \text{TypeTerm}(n)\quad\tau_2 : \text{TypeTerm}(n)}{\tau_1 \sim \tau_2 : \text{Constraint}(n)}{\textsc{Eq-Con}}
	\end{displaymath}
	\pause
	\begin{displaymath}
		\Inf{x : \text{Fin}(n)}{ \mathtt{Var}(x) : \text{TypeTerm}(n)}{\textsc{TVar-Con}}
	\end{displaymath}
	\pause
		\color{darkblue}
	\begin{displaymath}
		\Inf{}{\mathtt{zero} : \text{Fin}(s(n))}{\textsc{Zero}} \quad \Inf{x : \text{Fin}(n)}{ s(x) : \text{Fin}(s(n)) }{\textsc{Succ}}
	\end{displaymath}
\end{frame}
\begin{frame}{Generalising}
	Parameterise by a type used for names:
	\begin{displaymath}
		\Inf{C : \text{Constraint}({\color{darkred}\mathcal{S}(\tau)})}{\exists. C : \text{Constraint}({\color{darkred} \tau})}{\exists\textsc{-Con}}
	\end{displaymath}

	\begin{displaymath}
		\Inf{\tau_1 : \text{TypeTerm}({\color{darkred}\tau})\quad\tau_2 : \text{TypeTerm}({\color{darkred}\tau})}{\tau_1 \sim \tau_2 : \text{Constraint}({\color{darkred}\tau})}{\textsc{Eq-Con}}
	\end{displaymath}

	\begin{displaymath}
		\Inf{\color{darkred} x : \tau}{ \mathtt{Var}(x) : \text{TypeTerm}({\color{darkred}\tau})}{\textsc{TVar-Con}}
	\end{displaymath}
	\pause
	\color{darkgreen}
	\begin{displaymath}
		\Inf{}{\mathtt{zero} : \mathcal{S}(\tau)}{\textsc{Zero}}\quad\Inf{x : \tau}{s(x) : \mathcal{S}(\tau)}{\textsc{Succ}}
	\end{displaymath}
\end{frame}
\subsection{coincidence}
\begin{frame}{Just by Coincidence}
	TypeTerm forms a monad:
	\begin{displaymath}
		\gg\!= : \text{TypeTerm}(\alpha) \rightarrow (\alpha \rightarrow \text{TypeTerm}(\beta)) \rightarrow \text{TypeTerm}(\beta)
	\end{displaymath}
	\begin{displaymath}
		\mathtt{unit} : \alpha \rightarrow \text{TypeTerm}(\alpha) = \mathtt{Var}
	\end{displaymath}
	Kleisli arrows are substitutions $\alpha \rightarrow \text{TypeTerm}(\beta)$.

	\pause
	These substitutions are, by definition, \emph{capture avoiding} \footcite{Bellegarde:1994:SFM:202774.202788} \footcite{Bird:1999:DBN:968699.968702}

\end{frame}
\begin{frame}{Monad Laws}
	Kleisli composition forms a category ({\color{darkred}The Monad Laws}):
	\begin{itemize}
		\item {\tt unit} (i.e {\tt Var}) is an identity substitution:

		$$\mathtt{Var} \circ g \stackrel{\cdot}{=} g \qquad f \circ \mathtt{Var} \stackrel{\cdot}{=} f$$
		\item Substitution composition is associative:

		$$(a \circ b) \circ g \stackrel{\cdot}{=} a \circ (b \circ g)$$
    \end{itemize}
	 (Where $a \circ b$ is $\lambda x.\ a\ x \gg\!= b$)
	\end{frame}
	\begin{frame}{Functors!}
		Since TypeTerm is a monad, Environment can be indexed by the name type, and therefore form a functor:
		\pause
		\begin{displaymath}
			fmap : (\alpha \rightarrow \beta) \rightarrow Environment(\alpha) \rightarrow Environment(\beta)
		\end{displaymath}
		\begin{displaymath}
			\Gamma_\uparrow = {\tt fmap}\ s\ \Gamma
		\end{displaymath}
		(We also get functor instances for Constraint)
	\end{frame}
	\section{Thesis B}
	\subsection{Generating Constraints}
	\begin{frame}{Generating Constraints}
		With the new quantifiers added, constraints can be generated in a simple structural, syntax-directed way much like the original $\textsc{OutsideIn}(X)$ formalisation.
	\end{frame}
	\begin{frame}{Existential Quantifiers}
		\pause
		Rewrite to prenex normal form:
		\begin{displaymath}
			\begin{array}{lll}
				\phi \land \exists.\ \psi & \mapsto & \exists.\ \phi_\uparrow \land \psi \\
				& \cdots &
			\end{array}
		\end{displaymath}
			Termination measure: Depth of $\exists$-nesting.
			\pause

			\textbf{Possible Problem}:
			\begin{itemize}
				\item $\textsc{OutsideIn}(X)$ defines its own existential quantifiers for local assumptions (which should not be globalised).
				\item $\textsc{OutsideIn}(X)$ defines implication constraints for local assumptions.
			\end{itemize}
	\end{frame}
	\subsection{Proofs}
	\begin{frame}{Proofs}
		Once the constraint generation phase is complete, we can adapt the proofs of \emph{soundness} and \emph{principality} of the inference algorithm.

		We can do this without full knowledge of the constraint system, entailment relation or solver being used.

		\medskip

		\textbf{N.B: } $\textsc{OutsideIn}(X)$ does not guarantee completeness.

				\medskip
		\pause

		$\Longrightarrow$ virtually impossible to gauge how long this will take.
	\end{frame}
	\subsection{Solving}
	\begin{frame}{Solving Constraints}
		\textbf{If/When proofs are complete}, the next step is encoding the solver used by GHC's constraint system and plugging it into the $\textsc{OutsideIn}(X)$ formalisation in Agda.

		\medskip

		The solver is complicated, and specified as a rewrite system.

		\medskip

		Termination of the rewrite system is not proven, or even discussed: Even getting Agda to accept it may be a major source of pain.
		\pause

		\bigskip

		$\Longrightarrow$ Solver added to the ``nice to have'' pile.
	\end{frame}
	\begin{frame}{Unification}
		McBride's ``First-order unification by structural recursion'', a JFP paper that describes the use of terms indexed by available variables to provide a structural termination argument for first-order unification.

		\medskip

		Andrea Vezzozi has written an Agda version of the Epigram in the paper (a fairly straightforward translation).
	\end{frame}
	\section{Timeline}
	\subsection{Thesis A}
	\begin{frame}{Rest of Thesis A}
		\begin{itemize}
			\item Finish the basic language formalisation (without local assumptions)
			\item Investigate and, if time, resolve issues with the local assumption constraints.
		\end{itemize}
				\putat{20}{-90}{\includegraphics[width=2.5em]{determined.png}}
	\end{frame}
	\subsection{Thesis B}
	\begin{frame}{Thesis B Weeks 1-3}
		\begin{itemize}
			\item Finalise the formalisation of $\textsc{OutsideIn}(X)$, without the language parameterisation.
			\item Make a start on proof work.
		\end{itemize}
		\putat{20}{-96}{\includegraphics[width=2.5em]{concentrating2.png}}
	\end{frame}
	\begin{frame}{Thesis B Weeks 3-6}
		\begin{itemize}
			\item Keep working on soundness, principality proofs.
			\item Avoid going insane.
		\end{itemize}
		\putat{20}{-104}{\includegraphics[width=2.5em]{concentrating.png}}
	\end{frame}
	\begin{frame}{Thesis B Weeks 6-9}
		\begin{itemize}
			\item Finish proofs.
			\item Figure out how to add the solver
		\end{itemize}
		\putat{15}{-104}{\includegraphics[width=4.5em]{jackiechan.png}}
	\end{frame}
	\begin{frame}{Thesis B Weeks 9-12}
		\begin{itemize}
			\item Finalise documents
			\item If lucky, complete solver.
		\end{itemize}
		\putat{15}{-104}{\includegraphics[width=4.5em]{angry-desk-flip.png}}
	\end{frame}
	\begin{frame}[allowframebreaks]{Bibliography}
		\small
		\setlength{\parskip}{1cm}

		\printbibliography
		\end{frame}

\end{document}

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
\documentclass[12pt]{exam}
\usepackage[utf8]{inputenc}

\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb}
\usepackage{multicol}
\usepackage{upquote}
\usepackage{url}
\newcommand{\class}{miniHive}
\newcommand{\term}{}
\newcommand{\examnum}{Milestone 4}
\newcommand{\examdate}{}
\usepackage{paralist}
\usepackage{fancyvrb}
\usepackage{graphicx}

\pagestyle{head}
\firstpageheader{}{}{}
\runningheader{\class}{\examnum\ - Page \thepage\ of \numpages}{}
\runningheadrule

\begin{document}

\noindent
\begin{tabular*}{\textwidth}{l @{\extracolsep{\fill}} r @{\extracolsep{6pt}} l}
\textbf{\class} & \\
\textbf{\term} &&\\
\textbf{\examnum} &&\\
\textbf{\examdate} &&\\
\end{tabular*}\\
\rule[2ex]{\textwidth}{2pt}

\noprintanswers

\noindent

\section*{Optimizing {\em miniHive}\/}

In the fourth milestone, we optimize {\em miniHive}\/.
 The goal is to reduce the total amount of data stored in intermediary files within HDFS.

We have considered various options in class, and it is up to you which optimization(s) you implement. Chain folding is a good bet. You may also implement more than one idea.

In case  you need to adapt the LUIGI workflow, there is a chapter from the book ``Hadoop with Python'' with an introduction to LUIGI in Moodle.

\section{Evaluation Data}

We use data from the TPC-H benchmark, describing customers and their orders. This is a famous benchmark, where synthetic data can be generated based on a scale factor (SF).

The ER-like diagram in Figure~\ref{tpch} describes the schema, and has been taken from the official benchmark description. We assume that all  data adheres to this schema.

\begin{figure}[t]
\centering
    \includegraphics[scale=.3]{tpch.png}
    \caption{The TCP-H benchmark data [Source: {\tt www.tpc.org}.]}
    \label{tpch}
\end{figure}

The parentheses following each table name contain the prefix of the column names for that table.
The arrows point in the direction of the one-to-many relationships between tables.
The number/formula below each table name represents the cardinality (number of rows) of the table. Some are factored by SF, the scale factor.

\section{Calling {\em miniHive}\/}

For evaluating a single query, {\em miniHive} gets

\begin{compactitem}
    \item an optional flag telling miniHive to switch optimization on,
    \item the optional scale factor, allowing you to derive the
 {\em approximate}\/ sizes of tables,
    \item the input files, already stored in HDFS or available as local files,

    \item the optional execution environment (LOCAL or HDFS), set to HDFS by default,
        \item the SQL query over TPC-H data  to evaluate.
\end{compactitem}

\noindent
This is how we  call the optimized {\em miniHive}\/ for execution on local files:

\begin{Verbatim}[frame=single]
miniHive.py --O --SF 1 --env LOCAL "select distinct N_NAME from NATION"
\end{Verbatim}

If called in \verb!LOCAL! mode, this outputs an approximation of the HDFS storage costs (more on this later).
{\bf Make sure your submitted version does not write any other information to standard out, as this will confuse the test scripts.}

\section{Material in Moodle}

\begin{compactitem}

\item
A sample dataset that was generated with scale factor~0.01 (\verb!data_0_01.zip!).

\item
The  file \verb!miniHive.py!. You may alter this file.

\item
The file \verb!costcouter.py!. You must not alter this file.

\item
A list of SQL test queries in \verb!miniHive.q!.

\end{compactitem}

\section{What to Submit}

Submit a flat ZIP file (without any subfolders) containing

\begin{compactitem}
    \item a README file mentioning any additional Python modules that need to be installed via \verb!pip!, and a 1-paragraph description of the optimization(s) that you have implemented. The README must have this format:

    \begin{Verbatim}[frame=single,fontsize=\small]
# Author: <your lastname>, <your firstname>
# TODO install <comma-separated list of modules to install, or empty>

# My approach:
<1-paragraph description of your optimizations>
    \end{Verbatim}

    \item Further, all Python files required to run {\em miniHive}.

\end{compactitem}

\end{document}

max_stars_repo_name: miniHive/assignment

max_issues_repo_name: miniHive/assignment

max_forks_repo_name: miniHive/assignment


text:
\subsubsection{9.1 Covariant Differentiation}

\begin{definition}
affine connection or covariant differentiation is operator $\nabla (X,v) \mapsto \nabla_X v$ \quad \, $\begin{aligned} & \quad \\
       & \text{ vector $X$ at $p$ } \\
       & \text{ vector field $v$ at $p$ } \end{aligned}$

\begin{equation}
\begin{gathered}
\nabla_X (av+ bw) = a\nabla_X v + b \nabla_X w \\
         \nabla_{ aX + bY} v = a\nabla_X v + b\nabla_Y v
\end{gathered} \quad \quad \quad (9.2)
\end{equation}

\[
\begin{gathered}
\nabla_X (fv) = X(f)v + f\nabla_X v  \quad \quad \, \text{(``Leibniz rule'')}
\end{gathered}
\]

demand if $X$ smooth, $\nabla_X v$ smooth vector field.
\end{definition}

in our work up until now, we have always used local coordinates $x$ to yield a basis $\frac{ \partial}{ \partial x^i}$ for tangent vectors in a patch $U$.

For many purposes, however, it is advantageous to use a more general basis.

frame of vector fields in $U$ - $n$ linearly independent smooth vector fields
\[
\mathbf{e} = (e_1 \dots e_n)
\]
coordinate frame = special case, $e_i = \frac{ \partial }{ \partial x^i}$ for some coordinate system $x$ in $U$

frame $\mathbf{e}$ usually not coordinate frame, since $[e_i, e_j]$ usually not 0 while $[\partial_i, \partial_j] =0$

\begin{theorem}[9.3] frame $\mathbf{e}$ is locally a coordinate frame iff
\[
[e_i , e_j] = 0 \quad \, \forall \, i,j
\]
\end{theorem}

% \begin{proof} (proof environment not defined)
Proof:

We need only show that $[e_i, e_j]=0$ implies $\exists \, $ functions $(x^i)$ such taht
\[
e_i = \frac{ \partial }{ \partial x^i }
\]

Let $\sigma$ be the dual form basis.  From (4.25)

\begin{equation}
d\sigma^i(e_j, e_k) = -\sigma^i([e_j, e_k]) \quad \quad \quad \, (9.4)
\end{equation}

% \end{proof} (proof environment not defined)

Let $e = (e_1 \dots e_n)$ frame in $U$.  Then $X=e_j X^j$
\begin{equation}
\begin{aligned}
        \xrightarrow{ (9.2)} \nabla_X(e_k v^k) & = X(v^k) e_k + v^k \nabla_X e_k = X^j e_j v^k e_k + v^k X^j \nabla_{e_j} e_k = X^j e_j(v^k)e_k + X^j e_i \omega^i_{jk} v^k = \\
        & = X^j e_i \omega^i_{jk} v^k + X^j e_j(v^k)e_k
\end{aligned} \quad \quad \quad (9.5)
\end{equation}

where $\omega^i_{jk}$ defined

\begin{equation}
        \nabla_{e_j} e_k = e_i \omega^i_{jk} \quad \quad \quad (9.6)
\end{equation}

when $e_j = \partial_j$ coordinate frame, $\omega^i_{jk} = \Gamma^i_{jk}$

since $X(v^k) = dv^k(X)$

\[
\nabla_X v = e_i \lbrace dv^i(X) + X^j\omega^i_{jk} v^k \rbrace
\]

$\omega^i_{jk}$ coefficients of affine connection.  \\

using dual basis $\sigma$ of 1-forms,

\begin{equation}
        \nabla_X v = e_i \lbrace dv^i(X) + \omega^i_{jk} \sigma^j(X) v^k \rbrace = e_i \lbrace dv^i + \omega^i_{jk} \sigma^j v^k \rbrace(X) \quad \quad \quad (9.7)
\end{equation}

i.e.

\begin{equation}
\boxed{ \nabla_X v = dv(X) + \omega^i_{jk} + \omega^i_{jk} \sigma^j(X) v^ke_i }
\end{equation}

when frame $e$ is coordinate frame $e_i = \partial_i = \frac{ \partial }{ \partial x^i}$, \, $\sigma^i = dx^i$

\[
\nabla_X v = \partial_i \lbrace \frac{ \partial v^i}{ \partial x^j} + \omega^i_{jk} v^k \rbrace dx^j(X)
\]

i.e.

\begin{equation}
        (\nabla_X v)^i = \left[ \frac{ \partial v^i}{ \partial x^j} + \omega^i_{jk} v^k \right] X^j \quad \quad \quad (9.8)
\end{equation}

since $\nabla_X v$ assumed to be vector, conclude

\begin{equation}
        \nabla_j v^i = \left. v^i \right|_j \equiv \frac{ \partial v^i}{ \partial x^j} + \omega^i_{jk} v^k \quad \quad \quad (9.9)
\end{equation}

form the components of a mixed tensor, covariant derivative of vector $v$.

\subsubsection{9.3 Cartan's Exterior Covariant Differential}

\subsubsection{9.3c. Cartan's Structural Equations}

denote \\
row matrix  $ e \equiv (e_1 \dots e_n) $ \\
column $\sigma \equiv (\sigma^1 \dots \sigma^n )^T$ \\

$n \times n$ matrix of connection 1-forms $\omega = (\omega^i_{ \, \, j} )$ \\

column vector of torsion 2-forms $\tau = (\tau^1 \dots \tau^n)^T$

\subsubsection{9.3d. The Exterior Covariant Differential of a Vector-Valued Form}

$\alpha$ vector-valued $p$-form \\
locally,
$\alpha = e_i \otimes \alpha^i$, $\forall \, \alpha^i = a^i_{\, \, \underline{J}}(x) \sigma^J$ locally defined $p$-form \\

\textbf{exterior covariant differential}, vector-valued $(p+1)$ form $\nabla \alpha$ \\
\phantom{\quad } defined by Leibniz rule
\[
\nabla \alpha = \nabla (e_i \otimes \alpha^i) = (\nabla e_i) \otimes_{\wedge} \alpha^i + e_i \otimes d\alpha^i
\]
where
\[
(\nabla e_i)\otimes_{\wedge} \alpha^i = (e_k \otimes \omega^k_{\, \, i} ) \otimes_{\wedge} \alpha^i \equiv e_k \otimes (\omega^k_{\, \, i} \wedge \alpha^i)
\]

column of $p$ forms $\alpha = (\alpha^1 \dots \alpha^n)^T$

\begin{equation}
\nabla \alpha = e\otimes (d\alpha + \omega \wedge \alpha ) \quad \quad \quad \, (9.31)
\end{equation}

\paragraph{9.3(1) Basis expansion of the curvature form}
\beq{
	\tensor\theta{^i_j}
	&= \d\tensor\omega{^i_j} + \tensor\omega{^i_r}\wedge\tensor\omega{^r_j}
	 = \d\left(\tensor\omega{^i_{\ell j}}\d u^\ell\right) + \left(\tensor\omega{^i_{kr}}\d u^k\right)\wedge \left(\tensor\omega{^r_{\ell j}}\d u^\ell\right) \\
	&= \underbrace{\left(\partial_k\tensor\omega{^i_{\ell j}} + \tensor\omega{^i_{kr}}\tensor\omega{^r_{\ell j}}\right)}_{\identical\, \text{``}(_{k\ell})\text{''}} \underbrace{\d u^k\wedge\d u^\ell}_{\identical\, \d u^{k\ell}}
	 = \frac12 \left((_{k\ell})\d u^{k\ell} + (_{k\ell})\d u^{k\ell}\right) \\
	 	&\qquad\text{(In the second summand, commute the wedge product,} \\
	 	&\qquad\text{ afterwards rename }k\leftrightarrow \ell\text{)} \\
	 &= \frac12 \left((_{k\ell})\d u^{k\ell} - (_{\ell k})\d u^{k\ell}\right) \\
	 &= \frac12 \underbrace{\left(\partial_k\tensor\omega{^i_{\ell j}} - \partial_\ell\tensor\omega{^i_{kj}} + \tensor\omega{^i_{kr}}\tensor\omega{^r_{\ell j}} - \tensor\omega{^i_{\ell r}}\tensor\omega{^r_{kj}}\right)}_{=\tensor R{^i_{jk\ell}}} \d u^k\wedge\d u^\ell \\
	&= \frac12\tensor R{^i_{jk\ell}} \d u^k\wedge\d u^\ell
}

\paragraph{9.3(2) Covariant derivative of the identity form}
\beq{
	\vec\nabla\text{``}\d\vec r\text{''}
	&= \vec\nabla\left(\vec e_i \otimes \sigma^i\right)
	 = \vec e_i \otimes \underbrace{\left(\d\sigma^i + \tensor\omega{^i_j}\wedge\sigma^j\right)}_{=\tau^i}
	 = \vec e_i \otimes \tau^i
}
\emph{Remark:} The reason for calling \ieq{\vec e_i\otimes\sigma^i} the identity form is because
\beq{
	\vec e_i\otimes\sigma^i(\vec v)
	&= \vec e_i\otimes\sigma^i(v^j\vec e_j)
	 = \vec e_iv^j\underbrace{\sigma^i(\vec e_j)}_{=\delta^i_j}
	 = \vec e_iv^i
	 = \vec v
}

\subsubsection{9.4 Change of Basis and Gauge Transformations}

\paragraph{9.4(1) Transformation of the curvature form}\ \\
For readability, let \ieq{\bar P \equiv P^{-1}}.
\beq{
	   \theta'
	&= \d\omega' + \omega'\wedge\omega' \\
	&= \d(\bar P\omega P + \bar P\d P) \\
		&\qquad + (\bar P\omega P + \bar P\d P)\wedge(\bar P\omega P + \bar P\d P) \\
	&= \d(\bar P\omega P) + \d(\bar P\d P) \\
		&\qquad + \bar P\omega P\wedge\bar P\omega P + \bar P\omega P\wedge\bar P\d P + \bar P\d P\wedge\bar P\omega P + \bar P\d P\wedge\bar P\d P \\
	&= \d\bar P\wedge\omega P + \bar P\d\omega P - \bar P\omega\wedge\d P + \d\bar P\wedge\d P + \cancel{\bar P\d^2P} \\
		&\qquad + \bar P\omega P\wedge\bar P\omega P + \bar P\omega P\wedge\bar P\d P + \bar P\d P\wedge\bar P\omega P + \bar P\d P\wedge\bar P\d P \\
		&\qquad\text{(Use }0 = \d\unity = \d(\bar P P) = \d\bar P P + \bar P\d P \Leftrightarrow \d\bar P = -\bar P\d P\bar P \text{;} \\
		&\qquad\text{Also, the matrices ``commute'' with the wedge product, i.e. ``}A\wedge B=AB\wedge\text{'')} \\
	&= -\bar P\d P\wedge\bar P\omega P + \bar P\d\omega P - \bar P\omega\wedge\d P - \bar P\d P\wedge\bar P\d P \\
		&\qquad + \bar P\omega\wedge\omega P + \bar P\omega\wedge\d P + \bar P\d P\wedge\bar P\omega P + \bar P\d P\wedge\bar P\d P \\
	&= \bar P\d\omega P + \bar P\omega\wedge\omega P \\
	&= \bar P(\d\omega + \omega\wedge\omega) P \\
	&= \bar P\theta P
}

And this dear children is why indices should be left away. (Yes, it's the same exercise.)

\beq{
	   \theta'^i{}_j
	&= \d\omega'^i{}_j + \omega'^i{}_k\wedge\omega'^k{}_j \\
	&= \d(\bar P^i{}_l\omega^l{}_m P^m{}_j + \bar P^i{}_l\d P^l{}_j) \\
		&\qquad + (\bar P^i{}_l\omega^l{}_m P^m{}_k + \bar P^i{}_l\d P^l{}_k)\wedge(\bar P^k{}_n\omega^n{}_o P^o{}_j + \bar P^k{}_n\d P^n{}_j) \\
	&= \d(\bar P^i{}_l\omega^l{}_m P^m{}_j) + \d(\bar P^i{}_l\d P^l{}_j) \\
		&\qquad + \bar P^i{}_l\omega^l{}_m P^m{}_k\wedge\bar P^k{}_n\omega^n{}_o P^o{}_j + \bar P^i{}_l\omega^l{}_m P^m{}_k\wedge\bar P^k{}_n\d P^n{}_j \\
		&\qquad + \bar P^i{}_l\d P^l{}_k\wedge\bar P^k{}_n\omega^n{}_o P^o{}_j + \bar P^i{}_l\d P^l{}_k\wedge\bar P^k{}_n\d P^n{}_j \\
	&= \d\bar P^i{}_l\wedge\omega^l{}_m P^m{}_j + \bar P^i{}_l\d\omega^l{}_m P^m{}_j - \bar P^i{}_l\omega^l{}_m\wedge\d P^m{}_j + \d\bar P^i{}_l\wedge\d P^l{}_j + \cancel{\bar P^i{}_l\d^2P^l{}_j} \\
		&\qquad + \bar P^i{}_l\omega^l{}_m P^m{}_k\wedge\bar P^k{}_n\omega^n{}_o P^o{}_j + \bar P^i{}_l\omega^l{}_m P^m{}_k\wedge\bar P^k{}_n\d P^n{}_j \\
		&\qquad + \bar P^i{}_l\d P^l{}_k\wedge\bar P^k{}_n\omega^n{}_o P^o{}_j + \bar P^i{}_l\d P^l{}_k\wedge\bar P^k{}_n\d P^n{}_j \\
		&\qquad\text{(Use }0 = \d\delta^i{}_j = \d(\bar P^i{}_k P^k{}_j) = \d\bar P^i{}_k P^k{}_j + \bar P^i{}_k\d P^k{}_j \Leftrightarrow \d\bar P^i{}_j = -\bar P^i{}_k\d P^k{}_l\bar P^l{}_j \text{;} \\
		&\qquad\text{Also, the matrices ``commute'' with the wedge product, i.e. ``}A^i{}_k\wedge B^k{}_j=A^i{}_kB^k{}_j\wedge\text{'')} \\
	&= -\bar P^i{}_r\d P^r{}_s\wedge\bar P^s{}_l\omega^l{}_m P^m{}_j + \bar P^i{}_l\d\omega^l{}_m P^m{}_j - \bar P^i{}_l\omega^l{}_m\wedge\d P^m{}_j - \bar P^i{}_r\d P^r{}_s\wedge\bar P^s{}_l\d P^l{}_j \\
		&\qquad + \bar P^i{}_l\omega^l{}_m\wedge\omega^m{}_o P^o{}_j + \bar P^i{}_l\omega^l{}_m\wedge\d P^m{}_j \\
		&\qquad + \bar P^i{}_l\d P^l{}_m\wedge\bar P^m{}_n\omega^n{}_o P^o{}_j + \bar P^i{}_l\d P^l{}_k\wedge\bar P^k{}_n\d P^n{}_j \\
	&= \bar P^i{}_l\d\omega^l{}_m P^m{}_j + \bar P^i{}_l\omega^l{}_m\wedge\omega^m{}_n P^n{}_j \\
	&= \bar P^i{}_l(\d\omega^l{}_m + \omega^l{}_n\wedge\omega^n{}_m) P^m{}_j \\
	&= \bar P^i{}_l\theta^l{}_m P^m{}_j
}

\paragraph{9.4(2) Transformation of the curvature form}\ \\
The Transformation rule for basis vectors is
\beq{
	\vec e'=\vec eP \Leftrightarrow e'_i = e_j \tensor P{^j_i}
}
The transformation from cartesian to polar coordinates is given by
\beq{
	\matrixp{x\\y} &= \matrixp{x(r,\varphi)\\y(r,\varphi)} = \matrixp{r\cos\varphi\\r\sin\varphi} \\
	P &= \pdq{(x,y)}{(r,\varphi)} = \matrixp{\pdq xr & \pdq x\varphi \\ \pdq yr & \pdq y\varphi} = \matrixp{\cos\varphi & -r\sin\varphi \\ \sin\varphi & r\cos\varphi}
}
Using Mathematica to skip the annoying 2nd semester homework assignment parts of finding the inverse and calculating derivatives,
\beq{
	\d P &= \matrixp{-\sin\varphi\d\varphi & -\sin\varphi\d r-r\cos\varphi\d\varphi \\ \cos\varphi\d\varphi & \cos\varphi\d r-r\sin\varphi\d\varphi} \\
	P^{-1} &= \matrixp{\cos\varphi & \sin\varphi \\ -\frac1r\sin\varphi & \frac1r\cos\varphi}
}
Multiplying these two expressions yields, as desired,
\beq{
	\omega' = \cancel{P^{-1}\omega P} + P^{-1}\d P = \matrixp{0 & -r\d\varphi \\ \frac1r\d\varphi & \frac1r\d r}
}
Since \ieq{\theta=0}, \ieq{\theta'} vanishes as well. This is obvious from the transformation behavior of \ieq{\theta}; direct computation confirms this, as
\beq{
	   \theta'
	&= \d\omega'+\omega'\wedge\omega' \\
	&= \d\matrixp{0 & -r\d\varphi \\ \frac1r\d\varphi & \frac1r\d r} + \matrixp{0 & -r\d\varphi \\ \frac1r\d\varphi & \frac1r\d r}\wedge\matrixp{0 & -r\d\varphi \\ \frac1r\d\varphi & \frac1r\d r} \\
	&= \matrixp{\cancel{\d0} & \d(-r\d\varphi) \\ \d\left(\frac1r\d\varphi\right) & \cancel{\d\left(\frac1r\d r\right)}} + \matrixp{\cancel{0\wedge0} - \cancel{r\d\varphi\wedge\frac1r\d\varphi} & \cancel{0\wedge(-r\d\varphi)}-r\d\varphi\wedge\frac1r\d r \\ \cancel{\frac1r\d\varphi\wedge0} + \frac1r\d r\wedge\frac1r\d\varphi & \cancel{\frac1r\d\varphi\wedge(-r\d\varphi)} + \cancel{\frac1r\d r\wedge\frac1r\d r}} \\
	&= \matrixp{0 & -\d r\wedge\d\varphi \\ -\frac1{r^2}\d r\wedge\d\varphi & 0} + \matrixp{0 & \d r\wedge\d\varphi \\ \frac1{r^2}\d r\wedge\d\varphi & 0} \\
	&= \matrixp{0&0\\0&0}
}
This exercise made the advantage of the matrix notation clear: use the connection coefficients like normal matrices, only that you put a wedge in between their components' differential form ``factors''.

\subsubsection{}

\subsubsection{ Parallel Displacement and Curvature on a Surface}

When is parallel displacement independent of path?

We saw in Section 8.7 that parallel displacement of a vector between 2 pts. of a surface is path-dependent;  \\
This phenomenon is referred to as holonomy.

\begin{theorem}[9.61]
        Let $U\subset M^2$ compact in Riemannian surface with piecewise smooth boundary $\partial U$ \\
Assume $U$ covered by single orthonormal frame field $e$ (e.g. $U$ contained in coordinate patch) \\
Let unit vector $\mathbf{v}$ parallel translated around $\partial U$ \\
\quad $\mathbf{e}$ defined orientation.

Then angle $\Delta \alpha$ between $\mathbf{v}_0, \mathbf{v}_f$ is
\[
\Delta \alpha = \iint K dS = \iint_U K \sigma^1 \wedge \sigma^2
\]
\end{theorem}

Proof. parametrize $\partial U$, let $T$ tangent, let $\alpha = \arccos{ \langle e_1, v \rangle }$ \\
Although $\alpha$ (like $\mathbf{v}$) is not single-valued on $\partial U$, $d\alpha = \left( \frac{ d\alpha}{ds} \right) ds$ well-defined.
\[
\Delta \alpha = \arccos{ \langle v_0, v_f \rangle } = \oint_{ \partial U} d\alpha
\]

For
\[
\mathbf{v} = \mathbf{e}_1 \cos{\alpha} + \mathbf{e}_2 \sin{\alpha}
\]

then

\[
\begin{gathered}
        \nabla v = e(dv + \omega v) = e_1 (dv^1 + \omega_{12} v^2 ) + e_2 ( dv^2 + \omega_{21} v^1 ) = e_1 (-\sin{\alpha} d\alpha + \omega_{12} \sin{\alpha} ) + e_2 ( \cos{\alpha} d\alpha + \omega_{21} \cos{\alpha} ) = \\
        = (-e_1 \sin{\alpha} + e_2 \cos{\alpha} )( d\alpha - \omega_{12})
\end{gathered}
\]

To say that $v$ parallel displaced around $\partial U$ is to say \\
\quad $\nabla v(T) =0$, i.e. $d\alpha - \omega_{12} =0$ along $\partial U$  \quad (9.62)

\[
d \alpha(T) = \omega_{12}(T)
\]

Then
\[
\begin{gathered}
        \Delta \alpha = \oint_{\partial U} d\alpha = \oint_{\partial U} \omega_{12} = \iint_U d\omega_{12} = \\
        = \iint_U \theta_{12} = \iint_U K \sigma^1 \wedge \sigma^2
\end{gathered}
\]

max_stars_repo_path: LaTeX_and_pdfs/the geometry of physics problems/09covariantdifferentiation.tex


text:
% This is part of the TFTB Reference Manual.
% Copyright (C) 1996 CNRS (France) and Rice University (US).
% See the file refguide.tex for copying conditions.

\markright{tfrqview}
\section*{\hspace*{-1.6cm} tfrqview}

\vspace*{-.4cm}
\hspace*{-1.6cm}\rule[0in]{16.5cm}{.02cm}
\vspace*{.2cm}

{\bf \large \sf Purpose}\\
\hspace*{1.5cm}
\begin{minipage}[t]{13.5cm}
Quick visualization of a time-frequency representation.
\end{minipage}
\vspace*{.5cm}

{\bf \large \sf Synopsis}\\
\hspace*{1.5cm}
\begin{minipage}[t]{13.5cm}
\begin{verbatim}
tfrqview(tfr)
tfrqview(tfr,sig)
tfrqview(tfr,sig,t)
tfrqview(tfr,sig,t,method)
tfrqview(tfr,sig,t,method,p1)
tfrqview(tfr,sig,t,method,p1,p2)
tfrqview(tfr,sig,t,method,p1,p2,p3)
tfrqview(tfr,sig,t,method,p1,p2,p3,p4)
tfrqview(tfr,sig,t,method,p1,p2,p3,p4,p5)
\end{verbatim}
\end{minipage}
\vspace*{.5cm}

{\bf \large \sf Description}\\
\hspace*{1.5cm}
\begin{minipage}[t]{13.5cm}
        {\ty tfrqview} allows a quick visualization of a time-frequency
        representation. {\ty tfrqview} is called by any time-frequency
        representation of the toolbox ({\ty tfr*} functions) when these
        functions are called without any output argument.\\

\hspace*{-.5cm}\begin{tabular*}{14cm}{p{1.5cm} p{8.5cm} c}
Name & Description & Default value\\
\hline
        {\ty tfr}     & time-frequency representation {\ty (MxN)}\\
        {\ty sig}     & signal in time. If unavailable, put {\ty sig=[]} as input
                  parameter                    & {\ty []}\\
        {\ty t}       & time instants                 & {\ty (1:N)}\\
        {\ty method}  & name of chosen representation (see the {\ty tfr*}
		files for authorized names) & {\ty 'type1'} \\
                  &  {\ty type1} : the representation {\ty tfr} goes in normalized
                        frequency from {\ty -0.5} to {\ty 0.5} \\
                  &  {\ty type2} : the representation {\ty tfr} goes in normalized
                        frequency from {\ty 0} to {\ty 0.5}\\
        {\ty p1..p5} & optional parameters of the representation : run the
                  file {\ty tfrparam(method)} to know the meaning of {\ty p1..p5}
                  for your method\\
\hline
\end{tabular*}
\end{minipage}

\newpage

\hspace*{1.5cm}
\begin{minipage}[t]{13.5cm}
        When you use the {\ty 'save'} option in the main menu, you save all
        your variables as well as two strings, {\ty TfrQView} and {\ty
        TfrView}, in a mat file. If you load this file and do {\ty
        eval(TfrQView)}, you will restart the display session under {\ty
        tfrqview} ; if you do {\ty eval(TfrView)}, you will obtain the
        exact layout of the screen you had when clicking on the {\ty
        'save'} button.
\end{minipage}
\vspace*{.5cm}

{\bf \large \sf Example}
\begin{verbatim}
         sig=fmsin(128);
         tfr=tfrwv(sig);
         tfrqview(tfr,sig,1:128,'tfrwv');
\end{verbatim}
\vspace*{.5cm}

{\bf \large \sf See Also}\\
\hspace*{1.5cm}
\begin{minipage}[t]{13.5cm}
\begin{verbatim}
tfrview, tfrsave, tfrparam.
\end{verbatim}
\end{minipage}

max_stars_repo_name: sangyoonHan/extern

max_issues_repo_name: sangyoonHan/extern

max_forks_repo_name: sangyoonHan/extern