241 lines
7.4 KiB
TeX
241 lines
7.4 KiB
TeX
\documentclass[a4paper,10pt,numbers=noenddot,twocolumn]{scrbook}
|
|
|
|
\KOMAoptions{twoside=false}
|
|
\usepackage[top=2cm,lmargin=0.5in,rmargin=0.5in,bottom=3cm,hmarginratio=1:1]{geometry}
|
|
\usepackage[ngerman, english]{babel}
|
|
\usepackage[moderate, title=tight, bibliography=tight, margins=tight]{savetrees}
|
|
\babeltags{german=ngerman}
|
|
% \usepackage{mathabx}
|
|
% \usepackage{amssymb}
|
|
\usepackage[dvipsnames]{xcolor} % Coloured text etc.
|
|
\usepackage{amsthm}
|
|
\usepackage{thmtools}
|
|
\usepackage{fancyvrb}
|
|
\usepackage{anyfontsize}
|
|
% \usepackage{mathtools}
|
|
% \usepackage{amsmath}
|
|
\usepackage{mathpartir}
|
|
% packages for draft version
|
|
\usepackage{lineno}
|
|
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
|
|
\usepackage{unicode-math}
|
|
|
|
% mathpartir uses \atop, amsmath overrides it to throw a warning tho, so we override it back to the original!
|
|
\makeatletter
|
|
\let\atop\@@atop % chktex 1
|
|
\makeatother
|
|
|
|
\usepackage{tikz}
|
|
\usetikzlibrary{cd, babel, quotes}
|
|
\usepackage{quiver}
|
|
% \usepackage{stmaryrd} % for \llbracket and \rrbracket
|
|
\usepackage{ifthen}
|
|
\usepackage{xspace}
|
|
\usepackage{makeidx}
|
|
\usepackage{graphicx}
|
|
\usepackage{fvextra}
|
|
\usepackage[style=ieee, sorting=ynt, language=british]{biblatex} % advanced citations, british to make dates DD-MM-YYYY
|
|
\usepackage[english=british]{csquotes} % biblatex recommended to load this
|
|
\usepackage{etoolbox,xpatch}
|
|
|
|
\makeatletter
|
|
\AtBeginEnvironment{minted}{\dontdofcolorbox}\def\dontdofcolorbox{\renewcommand\fcolorbox[4][]{##4}}\xpatchcmd{\inputminted}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{}\xpatchcmd{\mintinline}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{} % see https://tex.stackexchange.com/a/401250/
|
|
\makeatother
|
|
\usepackage{scrhack}
|
|
|
|
\usepackage{multicol}
|
|
\usepackage[final]{hyperref}
|
|
|
|
|
|
\addbibresource{bib.bib}
|
|
%\usepackage[right]{showlabels}
|
|
%\usepackage[justific=raggedright,totoc]{idxlayout}
|
|
\usepackage[type=CC, modifier=by-sa,version=4.0]{doclicense}
|
|
|
|
% Listings package supporting unicode and agda highlighting
|
|
\usepackage{minted}
|
|
\setminted[agda]{
|
|
linenos=true,
|
|
breaklines=true,
|
|
encoding=utf8,
|
|
fontsize=\small,
|
|
frame=lines,
|
|
autogobble
|
|
}
|
|
% autoref for minted listings
|
|
\providecommand*{\listingautorefname}{Listing}
|
|
|
|
|
|
\addto\extrasenglish{
|
|
\renewcommand{\chapterautorefname}{Chapter}
|
|
\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\parskip{\baselineskip}
|
|
\setlength{\marginparsep}{0cm}
|
|
\AtBeginEnvironment{minted}{\setlength{\parskip}{0pt}}
|
|
|
|
\title{Implementing Categorical 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
|
|
|
|
|
|
\usepackage[scale=.85]{noto-mono}
|
|
|
|
\usepackage{mathrsfs}
|
|
\usepackage{xargs}
|
|
\usepackage{xstring}
|
|
|
|
\newcommand*{\dbtilde}[1]{\tilde{\raisebox{0pt}[0.85\height]{\(\tilde{#1}\)}}}
|
|
|
|
% https://unicodeplus.com/U+3016
|
|
\newcommand*{\lbparen}{〖}
|
|
\newcommand*{\rbparen}{〗}
|
|
|
|
% category C
|
|
\newcommand*{\C}{\ensuremath{\mathscr{C}}}
|
|
\newcommand*{\D}{\ensuremath{\mathscr{D}}}
|
|
% objects of category
|
|
\newcommand*{\obj}[1]{\ensuremath{\vert #1 \vert}}
|
|
% category of elgot algebras on #1
|
|
\newcommand*{\elgotalgs}[1]{\ensuremath{\mathit{ElgotAlgs}(#1)}}
|
|
% category of monads on #1
|
|
\newcommand*{\coalgs}[1]{\ensuremath{\mathit{Coalgs}(#1)}}
|
|
\newcommand*{\monads}[1]{\ensuremath{\mathit{Monads}(#1)}}
|
|
\newcommand*{\strongmonads}[1]{\ensuremath{\mathit{StrongMonads}(#1)}}
|
|
% category of pre-Elgot monads on #1
|
|
\newcommand*{\preelgot}[1]{\ensuremath{\mathit{PreElgot}(#1)}}
|
|
\newcommand*{\strongpreelgot}[1]{\ensuremath{\mathit{StrongPreElgot}(#1)}}
|
|
\newcommand*{\setoids}{\ensuremath{\mathit{Setoids}}}
|
|
% free objects
|
|
\newcommand*{\freee}[1]{\ensuremath{#1^\star}}
|
|
\newcommand*{\free}[1]{
|
|
\ensuremath{
|
|
\IfSubStr{#1}{\circ}
|
|
{{\freee{(#1)}}}
|
|
{\IfSubStr{#1}{\;}
|
|
{\freee{(#1)}}
|
|
{\freee{#1}}
|
|
}
|
|
}
|
|
}
|
|
% right stability
|
|
\newcommand*{\rss}[1]{\ensuremath{#1^\blacktriangleright}}
|
|
\newcommand*{\rs}[1]{
|
|
\ensuremath{
|
|
\IfSubStr{#1}{\circ}{{\rss{(#1)}}}{\rss{#1}}
|
|
}
|
|
}
|
|
% left stability
|
|
\newcommand*{\lss}[1]{\ensuremath{#1^\blacktriangleleft}}
|
|
\newcommand*{\ls}[1]{
|
|
\ensuremath{
|
|
\IfSubStr{#1}{\circ}{{\lss{(#1)}}}{\lss{#1}}
|
|
}
|
|
}
|
|
% terminal coalgebra
|
|
\newcommand*{\coalg}[1]{\ensuremath{\lbparen#1\rbparen}}
|
|
|
|
% discretized setoids
|
|
\newcommand*{\disc}[1]{\ensuremath{\vert #1 \vert}}
|
|
|
|
% Defines the `mycase` environment, copied from https://tex.stackexchange.com/questions/251053/how-to-use-case-1-case-2-in-a-proof-ieee-confs
|
|
\newcounter{cases}
|
|
\newcounter{subcases}[cases]
|
|
\newenvironment{mycase}
|
|
{
|
|
\setcounter{cases}{0}
|
|
\setcounter{subcases}{0}
|
|
\newcommand{\case}
|
|
{
|
|
\par\indent\stepcounter{cases}\textbf{Case \thecases.}
|
|
}
|
|
\newcommand{\subcase}
|
|
{
|
|
\par\indent\stepcounter{subcases}\textit{Subcase (\thesubcases):}
|
|
}
|
|
}
|
|
{
|
|
\par
|
|
}
|
|
\renewcommand*\thecases{\arabic{cases}}
|
|
\renewcommand*\thesubcases{\roman{subcases}}
|
|
|
|
\begin{document}
|
|
\pagestyle{plain}
|
|
\input{src/titlepage}%
|
|
|
|
\twocolumn[\include{src/00_abstract}]
|
|
|
|
\tableofcontents
|
|
|
|
% \listoftodos\
|
|
|
|
\newcommand{\agda}{{\raisebox{-0.075cm}{\includegraphics[height=1em]{img/agda.pdf}}}}
|
|
\newcommand{\agdaref}[1]{\href{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/#1.html}{\agda}}
|
|
|
|
\newcommandx{\unsure}[2][1=]{\todo[inline,linecolor=red,backgroundcolor=red!25,bordercolor=red,#1]{#2}}
|
|
\newcommandx{\change}[2][1=]{\todo[linecolor=blue,backgroundcolor=blue!25,bordercolor=blue,#1]{#2}}
|
|
\newcommandx{\info}[2][1=]{\todo[inline,linecolor=OliveGreen,backgroundcolor=OliveGreen!25,bordercolor=OliveGreen,#1]{#2}}
|
|
\newcommandx{\improvement}[2][1=]{\todo[inline,linecolor=Plum,backgroundcolor=Plum!25,bordercolor=Plum,#1]{#2}}
|
|
|
|
|
|
% for creating custom labels like (Fixpoint)
|
|
\makeatletter
|
|
\newcommand{\customlabel}[2]{%
|
|
\protected@write \@auxout {}{\string \newlabel {#1}{{#2}{\thepage}{#2}{#1}{}} }% chktex 1
|
|
\hypertarget{#1}{#2}%
|
|
}
|
|
\makeatother
|
|
|
|
\include{src/01_introduction}
|
|
\include{src/02_preliminaries}
|
|
\include{src/03_agda-categories}
|
|
\include{src/04_partiality-monads}
|
|
\include{src/05_iteration}
|
|
\include{src/06_setoids}
|
|
\twocolumn[\include{src/07_conclusion}]
|
|
|
|
\appendix
|
|
|
|
\medskip
|
|
|
|
\emergencystretch=1em
|
|
\printbibliography[heading=bibintoc]{}
|
|
|
|
\end{document}
|