From c97a981b2529358fd87889590eb4da792d854e42 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Tue, 5 Dec 2023 11:34:05 +0100 Subject: [PATCH] Added thesis, changed folder structure --- .gitignore | 45 ++++++++++ .envrc => src/.envrc | 0 Agda.css => src/Agda.css | 0 Makefile => src/Makefile | 0 bsc.agda-lib => src/bsc.agda-lib | 0 flake.lock => src/flake.lock | 0 flake.nix => src/flake.nix | 0 shell.nix => src/shell.nix | 0 thesis/.vscode/settings.json | 25 ++++++ thesis/Makefile | 20 +++++ thesis/README.adoc | 42 +++++++++ thesis/agda/motivation.agda | 75 ++++++++++++++++ thesis/bib.bib | 52 +++++++++++ thesis/main.tex | 110 ++++++++++++++++++++++++ thesis/src/00_introduction.tex | 2 + thesis/src/01_preliminaries.tex | 4 + thesis/src/02_agda-categories.tex | 4 + thesis/src/03_iteration.tex | 3 + thesis/src/04_partiality-monads.tex | 4 + thesis/src/05_monadK.tex | 1 + thesis/src/10_conclusion.tex | 1 + thesis/src/A1_contributions.tex | 5 ++ thesis/src/examples.tex | 129 ++++++++++++++++++++++++++++ thesis/src/titlepage.tex | 50 +++++++++++ 24 files changed, 572 insertions(+) rename .envrc => src/.envrc (100%) rename Agda.css => src/Agda.css (100%) rename Makefile => src/Makefile (100%) rename bsc.agda-lib => src/bsc.agda-lib (100%) rename flake.lock => src/flake.lock (100%) rename flake.nix => src/flake.nix (100%) rename shell.nix => src/shell.nix (100%) create mode 100644 thesis/.vscode/settings.json create mode 100644 thesis/Makefile create mode 100644 thesis/README.adoc create mode 100644 thesis/agda/motivation.agda create mode 100644 thesis/bib.bib create mode 100644 thesis/main.tex create mode 100644 thesis/src/00_introduction.tex create mode 100644 thesis/src/01_preliminaries.tex create mode 100644 thesis/src/02_agda-categories.tex create mode 100644 thesis/src/03_iteration.tex create mode 100644 thesis/src/04_partiality-monads.tex create mode 100644 thesis/src/05_monadK.tex create mode 100644 thesis/src/10_conclusion.tex create mode 100644 thesis/src/A1_contributions.tex create mode 100644 thesis/src/examples.tex create mode 100644 thesis/src/titlepage.tex diff --git a/.gitignore b/.gitignore index 4d47fdc..e218ad9 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +# agda *.agdai *.pdf *.log @@ -5,3 +6,47 @@ Everything.agda public/ .direnv .DS_Store + +# latex +# put this to .git/info/exclude in git repos managing latex +# +# git ls-files --others --exclude-from=.git/info/exclude +# Lines that start with '#' are comments. +# For a project mostly in C, the following would be a good set of +# exclude patterns (uncomment them if you want to use them): +# *.[oa] +.*.swp +.#* +*~ +*.pdf +# AUTOGENERATED +# All wildcards below this marker are used to remove generated files in +# 'make clean' +*.aux +*.fdb_latexmk +*.log +*.out +*.pdf +*.synctex.gz +*.toc +*.bbl +*.blg +*.idx +*.ilg +*.fls +*.ind +*.zip +*.dvi +*.eps +*.bcf +*.run.xml +*.nav +*.snm +*.vrb +*.vtc +*.spl +*.nlo +*.nls +*.auxlock +.auctex-auto/ +_region_.tex diff --git a/.envrc b/src/.envrc similarity index 100% rename from .envrc rename to src/.envrc diff --git a/Agda.css b/src/Agda.css similarity index 100% rename from Agda.css rename to src/Agda.css diff --git a/Makefile b/src/Makefile similarity index 100% rename from Makefile rename to src/Makefile diff --git a/bsc.agda-lib b/src/bsc.agda-lib similarity index 100% rename from bsc.agda-lib rename to src/bsc.agda-lib diff --git a/flake.lock b/src/flake.lock similarity index 100% rename from flake.lock rename to src/flake.lock diff --git a/flake.nix b/src/flake.nix similarity index 100% rename from flake.nix rename to src/flake.nix diff --git a/shell.nix b/src/shell.nix similarity index 100% rename from shell.nix rename to src/shell.nix diff --git a/thesis/.vscode/settings.json b/thesis/.vscode/settings.json new file mode 100644 index 0000000..89f774e --- /dev/null +++ b/thesis/.vscode/settings.json @@ -0,0 +1,25 @@ +{ +"latex-workshop.latex.tools" : [ + { + "name": "latexmk-main", + "command": "latexmk", + "args": [ + "-synctex=1", + "-interaction=nonstopmode", + "-file-line-error", + "-pdf", + "-outdir=%OUTDIR%", + "main.tex" + ], + "env": {} + } +], +"latex-workshop.latex.recipes": [ + { + "name": "latexmk-main", + "tools": [ + "latexmk-main" + ] + }, +] +} \ No newline at end of file diff --git a/thesis/Makefile b/thesis/Makefile new file mode 100644 index 0000000..b934397 --- /dev/null +++ b/thesis/Makefile @@ -0,0 +1,20 @@ +src = $(wildcard *.tex) +pdf = $(src:.tex=.pdf) +imgpdf = $(wildcard img/*.pdf) + +.PHONY: all clean install + +all: $(pdf) $(imgpdf) + +%.pdf: %.tex $(wildcard src/*.tex) $(wildcard *.bib) $(imgpdf) + latexmk -file-line-error -synctex=1 -halt-on-error -pdf $< + +fast: + # enforce tex execution + pdflatex -synctex=1 $(src) + +clean: + latexmk -C $(src) + rm -f $(wildcard *.out *.nls *.nlo *.bbl *.blg *-blx.bib *.run.xml *.bcf *.synctex.gz *.fdb_latexmk *.fls *.toc) + rm -f $(wildcard src/*.aux) + diff --git a/thesis/README.adoc b/thesis/README.adoc new file mode 100644 index 0000000..42f1802 --- /dev/null +++ b/thesis/README.adoc @@ -0,0 +1,42 @@ +README +====== + +About +----- +The present collection of files offers a template for a final thesis (no matter +whether project, bachelor, or master thesis). You are welcome to modify anything +to your personal needs. In case of any ambiguity, consult your supervisor on +formal aspects of the document, instead of just relying of my design choices for +the present template. + +Also see the content of template-master-thesis.pdf for some more suggestions. + +Usage +----- +It is strongly recommended to use a latex wrapper like latexmk (or rubber), in +order to build it. You can find a Makefile in the toplevel directory providing +a nice interface to latexmk: + +Type `make` In order to build the PDF, type `make clean` to remove all +automatically generated files (including the PDF). + +License of this Template +------------------------ +You can freely use the present template for your final thesis (i.e. master or bachelor or project thesis). +It is not mandatory at all to use this template for your final thesis. +It is just a suggestion! You are also allowed to change anything you would like to change in order to fit your needs/taste/... + +License for your Thesis +----------------------- +The template includes a http://creativecommons.org/licenses/by-sa/4.0/[Creative Commons Attribution-ShareAlike 4.0 International License] license remark as suggested license for your thesis. +We suggest you keep this license although you are free to choose a different license. + +License for your Implementation +------------------------------- +For implementations you write as part of your thesis we recommend to use a different repository and license this code under an Open Source license like GPL-3 or Apache. +When choosing a license for your implementations keep in mind that containing/modifying previous implementations licensed under GPL-3 requires you to use GPL-3 for your code as well. + +It is common to indicate the license of your code via a file called LICENSE in the folder of your repository. +If such a file does not exist already, GitLab displays a button "Add LICENSE" where you can select from common licenses as a template. + +// vim: tw=80 ft=asciidoc diff --git a/thesis/agda/motivation.agda b/thesis/agda/motivation.agda new file mode 100644 index 0000000..c6f15bf --- /dev/null +++ b/thesis/agda/motivation.agda @@ -0,0 +1,75 @@ +{-# OPTIONS --guardedness #-} + +-- Take this example as motivation: +-- https://stackoverflow.com/questions/21808186/agda-reading-a-line-of-standard-input-as-a-string-instead-of-a-costring + +open import Level +open import Agda.Builtin.Coinduction +module thesis.motivation where + +module old-delay where + private + variable + a : Level + data _⊥ (A : Set a) : Set a where + now : A → A ⊥ + later : ∞ (A ⊥) → A ⊥ + + never : ∀ {A : Set a} → A ⊥ + never = later (♯ never) + +module ReverseInput where + open import Data.Char + open import Data.Nat + open import Data.List using (List; []; _∷_) + open import Data.String + open import Data.Unit.Polymorphic + open import Codata.Musical.Costring + open import Codata.Musical.Colist using ([]; _∷_) + -- open import IO using (IO; seq; bind; return; Main; run; putStrLn) + open import IO.Primitive + open import IO.Primitive.Infinite using (getContents) + open import Agda.Builtin.IO using () + + open old-delay + -- IDEA: start in haskell, then motivate in agda and define delay type + -- next talk about bisimilarity. + -- idea for slide title: dlrowolleh.hs and dlrowolleh.agda + + private + variable + a : Level + + -- reverse : Costring → String ⊥ + -- reverse = go [] + -- where + -- go : List Char → Costring → String ⊥ + -- go acc [] = now (fromList acc) + -- go acc (x ∷ xs) = later (♯ go (x ∷ acc) (♭ xs)) + + -- putStrLn⊥ : String ⊥ → IO {a} ⊤ + -- putStrLn⊥ (now s) = putStrLn s + -- putStrLn⊥ (later s) = seq (♯ return tt) (♯ putStrLn⊥ (♭ s)) + + -- main : Main + -- main = run (bind (♯ {! getContents !}) {! !}) --(λ c → ♯ putStrLn⊥ (reverse c))) + +-- NOTE: This is not very understandable... Better stick to the outdated syntax +module delay where + mutual + data _⊥ (A : Set) : Set where + now : A → A ⊥ + later : A ⊥' → A ⊥ + + record _⊥' (A : Set) : Set where + coinductive + field + force : A ⊥ + open _⊥' + + mutual + never : ∀ {A : Set} → A ⊥ + never = later never' + + never' : ∀ {A : Set} → A ⊥' + force never' = never diff --git a/thesis/bib.bib b/thesis/bib.bib new file mode 100644 index 0000000..dde4d9e --- /dev/null +++ b/thesis/bib.bib @@ -0,0 +1,52 @@ +@inproceedings{10.1145/3437992.3439922, + author = {Hu, Jason Z. S. and Carette, Jacques}, + title = {Formalizing Category Theory in Agda}, + year = {2021}, + isbn = {9781450382991}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/3437992.3439922}, + doi = {10.1145/3437992.3439922}, + abstract = {The generality and pervasiveness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization of category theory. We document our work on solving this dilemma. The formalization revealed a number of potential design choices, and we present, motivate and explain the ones we picked. In particular, we find that alternative definitions or alternative proofs from those found in standard textbooks can be advantageous, as well as "fit" Agda's type theory more smoothly. Some definitions regarded as equivalent in standard textbooks turn out to make different "universe level" assumptions, with some being more polymorphic than others. We also pay close attention to engineering issues so that the library integrates well with Agda's own standard library, as well as being compatible with as many of supported type theories in Agda as possible.}, + booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs}, + pages = {327–342}, + numpages = {16}, + keywords = {formal mathematics, Agda, category theory}, + location = {Virtual, Denmark}, + series = {CPP 2021} +} + +@incollection{Altenkirch_2017, + doi = {10.1007/978-3-662-54458-7_31}, + url = {https://doi.org/10.1007%2F978-3-662-54458-7_31}, + year = {2017}, + publisher = {Springer Berlin Heidelberg}, + pages = {534--549}, + author = {Thorsten Altenkirch and Nils Anders Danielsson and Nicolai Kraus}, + title = {Partiality, Revisited}, + booktitle = {Lecture Notes in Computer Science} +} + +@article{delay2005, + doi = {10.2168/lmcs-1(2:1)2005}, + url = {https://doi.org/10.2168%2Flmcs-1%282%3A1%292005}, + year = {2005}, + month = {jul}, + publisher = {Centre pour la Communication Scientifique Directe ({CCSD})}, + volume = {Volume 1, Issue 2}, + author = {Venanzio Capretta}, + title = {General Recursion via Coinductive Types}, + journal = {Logical Methods in Computer Science} +} + +@inproceedings{uni-elgot2021, + doi = {10.4230/LIPICS.ICALP.2021.131}, + url = {https://drops.dagstuhl.de/opus/volltexte/2021/14200/}, + author = {Goncharov, Sergey}, + keywords = {Elgot monad, partiality monad, delay monad, restriction category, Theory of computation → Categorical semantics, Theory of computation → Constructive mathematics}, + language = {en}, + title = {Uniform Elgot Iteration in Foundations}, + publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, + year = {2021}, + copyright = {Creative Commons Attribution 4.0 International license} +} diff --git a/thesis/main.tex b/thesis/main.tex new file mode 100644 index 0000000..6a5387d --- /dev/null +++ b/thesis/main.tex @@ -0,0 +1,110 @@ +\documentclass[a4paper,11pt,numbers=noenddot]{scrbook} + +\usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry} +\usepackage[utf8]{inputenc} +\usepackage[ngerman,english]{babel} +\babeltags{german=ngerman} +\usepackage{amssymb} +\usepackage{amsthm} +\usepackage{thmtools} +\usepackage{fancyvrb} +\usepackage{mathtools} +\usepackage{amsmath} +\usepackage{ifthen} +\usepackage{xspace} +\usepackage{hyperref} +\usepackage{makeidx} +\usepackage{graphicx} +\usepackage[style=ieee, sorting=ynt]{biblatex} %advanced citations +\usepackage[english=british]{csquotes} %biblatex recommended to load this +\addbibresource{bib.bib} +%\usepackage[right]{showlabels} +%\usepackage[justific=raggedright,totoc]{idxlayout} +\usepackage[type=CC, modifier=by-sa,version=4.0]{doclicense} + + +\addto\extrasenglish{% + \renewcommand{\chapterautorefname}{Section} + \renewcommand{\sectionautorefname}{Section} + \renewcommand{\subsectionautorefname}{Subsection} + } + +\newcommand\chap[1]{% + \chapter*{#1}% + \chaptermark{#1}% + \addcontentsline{toc}{chapter}{#1}} + +\declaretheorem[name=Definition,style=definition,numberwithin=chapter]{definition} +\declaretheorem[name=Example,style=definition,sibling=definition]{example} +\declaretheorem[style=definition,numbered=no]{exercise} +\declaretheorem[name=Remark,style=definition,sibling=definition]{remark} +\declaretheorem[name=Assumption,style=definition,sibling=definition]{assumption} +\declaretheorem[name=Observation,style=definition,sibling=definition]{observation} +\declaretheorem[name=Theorem,sibling=definition]{theorem} +\declaretheorem[sibling=definition]{corollary} +\declaretheorem[name=Fact,sibling=definition]{fact} +\declaretheorem[sibling=definition]{lemma} +\declaretheorem[sibling=lemma]{proposition} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % +% Spacing settings % +% % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\setlength{\parindent}{0pt} +\setlength{\parskip}{6pt} +\setlength{\marginparsep}{0cm} + +\title{Implementing Notions of Partiality and Delay in Agda} + +\author{Leon Vatthauer} + +\makeatletter +\hypersetup{ + pdfauthor={\@author}, + pdftitle={\@title}, + % kill those ugly red rectangles around links + hidelinks, +} +\newcommand*{\theauthor}{\@author} +\makeatother + +\begin{document} +\pagestyle{plain} +\input{src/titlepage}% +\chapter*{Disclaimer} +\begin{german} +Ich versichere, dass ich die Arbeit ohne fremde Hilfe und ohne Benutzung anderer als der angegebenen Quellen angefertigt habe und dass die Arbeit in gleicher oder ähnlicher Form noch keiner anderen Prüfungsbehörde vorgelegen hat und von dieser als Teil einer Prüfungsleistung angenommen wurde. +Alle Ausführungen, die wörtlich oder sinngemäß übernommen wurden, sind als solche gekennzeichnet. + +\vspace{5em} +Erlangen, \today{} \rule{7cm}{1pt}\\ +\phantom{Erlangen, \today{}} \theauthor{} +\end{german} + +\chapter*{Licensing} +\doclicenseThis{} +\tableofcontents +% \include{src/examples} +\include{src/00_introduction} + +%% IDEA: swap chapter 01 and 02, first introduce category theory in agda and then subsequently explain every notion in preliminaries with agda code. +%% This is a major design decision..., there are two alternatives: +%%% - introduce notions in latex and later give agda code (maybe in appendix) +%%% - introduce notions in agda directly (maybe unreadable, maybe duplication with appendix) +\include{src/01_preliminaries} +\include{src/02_agda-categories} +\include{src/03_iteration} +\include{src/04_partiality-monads} +\include{src/05_monadK} +\include{src/10_conclusion} + +\appendix +\include{src/A1_contributions} + +\medskip + +\printbibliography[heading=bibintoc]{} +\end{document} + +% vim: tw=80 nospell spelllang=en nocul diff --git a/thesis/src/00_introduction.tex b/thesis/src/00_introduction.tex new file mode 100644 index 0000000..80c5521 --- /dev/null +++ b/thesis/src/00_introduction.tex @@ -0,0 +1,2 @@ +\chapter{Introduction} +citing elgot~\cite{uni-elgot2021} diff --git a/thesis/src/01_preliminaries.tex b/thesis/src/01_preliminaries.tex new file mode 100644 index 0000000..0c2fc92 --- /dev/null +++ b/thesis/src/01_preliminaries.tex @@ -0,0 +1,4 @@ +\chapter{Preliminaries} +\section{Stable Natural Numbers Object} +\section{Extensive and Distributive Categories} +\section{Strong and Commutative Monads} \ No newline at end of file diff --git a/thesis/src/02_agda-categories.tex b/thesis/src/02_agda-categories.tex new file mode 100644 index 0000000..c002f41 --- /dev/null +++ b/thesis/src/02_agda-categories.tex @@ -0,0 +1,4 @@ +\chapter{Formalizing Category Theory in Agda} +% IDEAS: +%% - why agda? talk about other approaches i.e. HOTT, coq, ... +%% - show some basic definitions like category and functor \ No newline at end of file diff --git a/thesis/src/03_iteration.tex b/thesis/src/03_iteration.tex new file mode 100644 index 0000000..b5531ab --- /dev/null +++ b/thesis/src/03_iteration.tex @@ -0,0 +1,3 @@ +\chapter{Iteration Algebras and Monads} +\section{Elgot Algebras} +\section{Pre-Elgot Monads} \ No newline at end of file diff --git a/thesis/src/04_partiality-monads.tex b/thesis/src/04_partiality-monads.tex new file mode 100644 index 0000000..bdfdd48 --- /dev/null +++ b/thesis/src/04_partiality-monads.tex @@ -0,0 +1,4 @@ +\chapter{Partiality Monads} +\section{Classifying Partiality Monads} +\section{The Maybe Monad} +\section{The Delay Monad} \ No newline at end of file diff --git a/thesis/src/05_monadK.tex b/thesis/src/05_monadK.tex new file mode 100644 index 0000000..cd10f96 --- /dev/null +++ b/thesis/src/05_monadK.tex @@ -0,0 +1 @@ +\chapter{The K monad} \ No newline at end of file diff --git a/thesis/src/10_conclusion.tex b/thesis/src/10_conclusion.tex new file mode 100644 index 0000000..3533e97 --- /dev/null +++ b/thesis/src/10_conclusion.tex @@ -0,0 +1 @@ +\chapter{Conclusion} \ No newline at end of file diff --git a/thesis/src/A1_contributions.tex b/thesis/src/A1_contributions.tex new file mode 100644 index 0000000..4ca1852 --- /dev/null +++ b/thesis/src/A1_contributions.tex @@ -0,0 +1,5 @@ +\chapter{Open Source Contributions} +% IDEA: Include formalization of kleisli-triple, distributive category and PNNO in appendix. +\section{Kleisli Triple} +\section{Distributive Categories} +\section{Stable Natural Numbers Object} \ No newline at end of file diff --git a/thesis/src/examples.tex b/thesis/src/examples.tex new file mode 100644 index 0000000..7509528 --- /dev/null +++ b/thesis/src/examples.tex @@ -0,0 +1,129 @@ +\chapter{Some Introduction and Examples} +You can freely use the present template for your final thesis (i.e.~master or +bachelor or project thesis). + +This template was made from the following theses: +\begin{itemize} +\item \url{http://thorsten-wissmann.de/theses/ma-wissmann.pdf} +\item \url{http://thorsten-wissmann.de/theses/project-wissmann.pdf} +\item \url{http://thorsten-wissmann.de/theses/bachelor-thesis-wissmann.pdf} +\end{itemize} + +\section{Meaning} +It is not mandatory at all to use this template for your final thesis. It is +just a suggestion! You are also allowed to change anything you would like to +change in order to fit your needs/taste/$\ldots$. + +Of course, you should adjust some places when using it for your final thesis: +\begin{enumerate} +\item In the parameters to the \texttt{hyperref}-package, you should adjust the +fields \texttt{pdfauthor} and \texttt{pdftitle} to your name and the title of +your thesis. + +\item In \texttt{src/titlepage.tex} you should adjust the title and (possibly +the) subtitle of your thesis, the degree of your thesis (Masters degree? +Bachelor?), your name and the name of your advisors. + +\end{enumerate} + +\section{Some hints} +\subsection{Macros} + +% some macros only needed for these hints here +\newcommand{\C}{\ensuremath{\mathcal{C}}\xspace} +\newcommand{\preview}[2]{ +\begin{center} +\fbox{\begin{minipage}[t]{.47\textwidth} +#1 +\end{minipage}}% +\hspace{.02\textwidth}% +\fbox{\begin{minipage}[t]{.47\textwidth} +#2 +\end{minipage}}% +\end{center}} + +When using certain mathematical symbols very often, it makes sense to define +macros for them, e.g.~ +\begin{verbatim} +\newcommand{\C}{\ensuremath{\mathcal{C}}\xspace} +\end{verbatim} +The \texttt{ensuremath} enforces mathmode and the \texttt{xspace} inserts a +space if necessary: +\preview{ +\Verb|Some \textbackslash C in the midle of the sentence| +\Verb|and at the end: \textbackslash C.| +}{ +Some \C in the midle of the sentence +and at the end: \C. +} + +\subsection{UTF-8} + +I strongly recommend exploiting the utf8 capability of \LaTeX: + +\begin{verbatim} +\usepackage{newunicodechar} +\newunicodechar{∀}{\ensuremath{\forall}} +\newunicodechar{∃}{\ensuremath{\exists}} +\newunicodechar{×}{\ensuremath{\times}} +\newunicodechar{ø}{\ensuremath{\emptyset}} +\newunicodechar{≤}{\ensuremath{\le}} +\newunicodechar{∈}{\ensuremath{\in}} +\newunicodechar{→}{\ensuremath{\to}} +\newunicodechar{⊆}{\ensuremath{\subseteq}} +\newunicodechar{⊗}{\ensuremath{\otimes}} +\newunicodechar{∧}{\ensuremath{\wedge}} +\end{verbatim} + +with that, you can write: +\begin{verbatim} + \begin{definition}[Transitivity] + A relation $\text{``}≤\text{''} ⊆ X×X$ has upper bounds if + \[ + ∀a,b ∈ X\ ∃ c ∈ X: a ≤ c ∧ b ≤ c + \] + \end{definition} +\end{verbatim} + +It will result in the following: + + \begin{definition}[Transitivity] + A relation $\text{``}≤\text{''} ⊆ X×X$ has upper bounds if + \[ + ∀a,b ∈ X\ ∃ c ∈ X: a ≤ c ∧ b ≤ c + \] + \end{definition} + +In order to input unicode characters, just configure a compose key, e.g.: +\begin{itemize} +\item \url{https://en.wikipedia.org/wiki/Compose_key} +\item +\url{https://wiki.archlinux.org/index.php/Keyboard_configuration_in_Xorg#Configuring_compose_key} + +\end{itemize} + +\subsection{Autoref} + +Let \LaTeX~include whether something references is a definition or what else +using the \texttt{\textbackslash autoref} command: + +\begin{verbatim} + \begin{definition}[label={relation},name={Relation}] + A relation $R$ between sets $X$ and $Y$ is just a subset of $X×Y$. + \end{definition} + We have just seen \autoref{relation}. +\end{verbatim} + +This results in: + + + \begin{definition}[label={relation},name={Relation}] + A relation $R$ between sets $X$ and $Y$ is just a subset of $X×Y$. + \end{definition} + We have just seen \autoref{relation}. + +\subsection{Further Comments} +For even more convenience while writing, you should look at the following: +synctex, git (for managing your \TeX-sources). + +% vim: tw=80 nospell spelllang=en nocul diff --git a/thesis/src/titlepage.tex b/thesis/src/titlepage.tex new file mode 100644 index 0000000..62e0063 --- /dev/null +++ b/thesis/src/titlepage.tex @@ -0,0 +1,50 @@ +\begin{titlepage} +\newcommand{\drop}{0.07\textheight} +\begin{center} +\begingroup% +\vfill +{\LARGE\textsc{% +Friedrich-Alexander-Universität\\[2mm] +Erlangen-Nürnberg% +}}\\[\drop] +{% +% trim= left bottom right top +\includegraphics[height=1.8cm,trim=0cm 0mm 0 0mm]{img/tcs}\\ +\textsc{\large Chair for Computer Science 8}\\ +\textsc{\large Theoretical Computer Science}}%\\[\drop] +\vfill +\rule{\textwidth}{1pt}\par +\vspace{0.5\baselineskip} +{% maybe \itshape? + \Huge\bfseries + \makeatletter + \@title \\[1cm] + \makeatother +\large\bfseries +An exploration of \ldots % TODo +\\ and \ldots +\\[1cm] +\textbf{\large Bachelor Thesis in Computer Science} +}\\[0.5\baselineskip] +\rule{\textwidth}{1pt}\par +\vfill +{\Large{\makeatletter\@author\makeatother} + %\\ {\large\normalsize{maybe-ur-mail@example.org}} +} +\vfill +\large Advisor: +\vfill +\begin{tabular}{ccc} + \large + Sergey Goncharov +\end{tabular} +\vfill +% trim= left bottom right top +\includegraphics[height=1.8cm,trim=0cm -5mm 0 0mm]{img/fau} +\vfill +{\large Erlangen, \today} +\endgroup +\end{center} +\end{titlepage} + +% vim: tw=80 spell spelllang=en nocul