From de8835078680572faad8eb87753d3140e6f62898 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 21 Oct 2020 01:24:08 +0100 Subject: [PATCH] Some scribbles on relations and functions. --- macros.tex | 5 ++ thesis.bib | 15 +++++ thesis.tex | 193 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 213 insertions(+) diff --git a/macros.tex b/macros.tex index d0968ed..a19a17a 100644 --- a/macros.tex +++ b/macros.tex @@ -5,6 +5,11 @@ \newcommand{\defnas}[0]{\mathrel{:=}} \newcommand{\simdefas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{\simeq}}} +%% +%% Some useful maths abbreviations +%% +\newcommand{\N}{\ensuremath{\mathbb{N}}} + %% %% Partiality %% diff --git a/thesis.bib b/thesis.bib index ce6bb86..13f57f5 100644 --- a/thesis.bib +++ b/thesis.bib @@ -1336,4 +1336,19 @@ author = {William Shakespeare}, title = {The {Tragedy} of {Hamlet}, {Prince} of {Denmark}}, year = {1564-1616} +} + +# Introductory PL books +@book{Pierce02, + author = {Benjamin C. Pierce}, + title = {Types and programming languages}, + publisher = {{MIT} Press}, + year = {2002} +} + +@book{Harper16, + author = {Robert Harper}, + title = {Practical Foundations for Programming Languages (2nd. Ed.)}, + publisher = {Cambridge University Press}, + year = {2016} } \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index 4a0d1bb..8de2141 100644 --- a/thesis.tex +++ b/thesis.tex @@ -254,6 +254,199 @@ Explain conventions\dots \part{Background} \label{p:background} +\chapter{Mathematical preliminaries} +\label{ch:maths-prep} + +Only a modest amount of mathematical proficiency should be necessary +to be able to wholly digest this dissertation. +% +This chapter introduces some key mathematical concepts that will +either be used directly or indirectly throughout this dissertation. +% + +I assume familiarity with basic programming language theory including +structural operational semantics~\cite{Plotkin04a} and System F type +theory~\cite{Girard72}. For a practical introduction to programming +language theory I recommend consulting \citeauthor{Pierce02}'s +excellent book \emph{Types and Programming + Languages}~\cite{Pierce02}. For the more theoretical inclined I +recommend \citeauthor{Harper16}'s book \emph{Practical Foundations for + Programming Languages}~\cite{Harper16} (do not let the ``practical'' +qualifier deceive you) --- the two books complement each other nicely. + +\section{Relations and functions} +\label{sec:functions} + +\begin{definition} + The Cartesian product of two sets $A$ and $B$, written $A \times B$, + is the set of all ordered pairs $(a, b)$, where $a$ is drawn from + $A$ and $b$ is drawn from $B$, i.e. + % + \[ + A \times B \defas \{ (a, b) \mid a \in A, b \in B \} + \] + % +\end{definition} +% +Since the Cartesian product is itself a set, we can take the Cartesian +product of it with another set, e.g. $A \times B \times C$. However, +this raises the question in which order the product operator +($\times$) is applied. In this dissertation the product operator is +taken to be right associative, meaning +$A \times B \times C = A \times (B \times C)$. +% +\dhil{Define tuples (and ordered pairs)?} +% +% To make the notation more compact for the special case of $n$-fold +% product of some set $A$ with itself we write +% $A^n \defas A \underbrace{\times \cdots \times}_{n \text{ times}} A$. +% + + +\begin{definition} + A relation $R$ is a subset of the Cartesian product of two sets $A$ + and $B$, i.e. $R \subseteq A \times B$. + % + An element $a \in A$ is related to an element $b \in B$ if + $(a, b) \in R$, sometimes written using infix notation $a\,R\,b$. + % + If $A = B$ then $R$ is said to be a homogeneous relation. +\end{definition} +% + +\begin{definition} + For any two relations $R \subseteq A \times B$ and + $S \subseteq B \times C$ their composition is defined as follows. + % + \[ + S \circ R \defas \{ (a,c) \mid (a,b) \in R, (b, c) \in S \} + \] +\end{definition} + +The composition operator ($\circ$) is associative, meaning +$(T \circ S) \circ R = T \circ (S \circ R)$. +% +For $n \in \N$ the $n$th relational power of a relation $R$, written +$R^n$, is defined inductively. +\[ + R^0 \defas \emptyset, \quad\qquad R^1 \defas R, \quad\qquad R^{1 + n} \defas R \circ R^n. +\] +% +Reflexive and transitive relations and their closures feature +prominently in the dynamic semantics of programming languages. +% +\begin{definition} + A homogeneous relation $R \subseteq A \times A$ is said to be + reflexive and transitive if its satisfies the following criteria, + respectively. + \begin{itemize} + \item Reflexive: $\forall a \in A$ it holds that $a\,R\,a$. + \item Transitive: $\forall a,b,c \in A$ if $a\,R\,b$ and $b\,R\,c$ + then $a\,R\,c$. + \end{itemize} +\end{definition} + +\begin{definition}[Closure operations] + Let $R \subseteq A \times A$ denote a homogeneous relation. The + reflexive closure $R^{=}$ of $R$ is the smallest reflexive relation + over $A$ containing $R$, i.e. + % + \[ + R^{=} \defas \{ (a, a) \mid a \in A \} \cup R + \] + % + The transitive closure $R^+$ of $R$ is the smallest transitive + relation over $A$ containing $R$, i.e. + % + \[ + R^+ \defas \displaystyle\bigcup_{n \in \N} R^n + \] + +\end{definition} +% +The reflexive and transitive closure $R^\ast$ of $R$ is defined as +$R^\ast \defas (R^+)^{=}$. + +\begin{definition} + A relation $R \subseteq A \times B$ is functional and serial if it + satisfies the following criteria, respectively. + % + \begin{itemize} + \item Functional: $\forall a \in A, b,b' \in B$ if $a\,R\,b$ and $a\,R\,b'$ then $b = b'$. + \item Serial: $\forall a \in A,\exists b \in B$ such that + $a\,R\,b$. + \end{itemize} +\end{definition} +% +The functional property guarantees that every $a \in A$ is at most +related to one $b \in B$. Note this does not mean that every $a$ +\emph{is} related to some $b$. The serial property guarantees that +every $a \in A$ is related to one or more elements in $B$. +% +We use these properties to define partial and total functions. +% +\begin{definition} + A partial function $f : A \pto B$ is a functional relation + $f \subseteq A \times B$. + % + A total function $f : A \to B$ is a functional and serial relation + $f \subseteq A \times B$. +\end{definition} +% +A total function is also simply called a `function'. +% +For a function $f : A \to B$ (or partial function $f : A \pto B$) we +write $f(a) = b$ to mean $(a, b) \in f$, and say that $f$ returns $b$ +when applied to $a$. +% +The domain of a function is a set, $\dom(-)$, consisting of all the +elements for which it is defined. Thus the domain of a total function +is its domain of definition, e.g. $\dom(f : A \to B) = A$. +% +For a partial function $f$ its domain is a proper subset of the domain +of definition. +% +\[ + \dom(f : A \pto B) \defas \{ a \mid a \in A,\, f(a) \text{ is defined} \} \subset A. +\] +% +The codomain of a total function $f : A \to B$ (or partial function +$f : A \pto B$) is $B$, written $\dec{cod}(f) = B$. A related notion +is that of \emph{image}. The image of a total or partial function $f$, +written $\dec{Im}(f)$, is the set of values that it can return, i.e. +% +\[ + \dec{Im}(f) \defas \{\, f(a) \mid a \in \dom(f) \} +\] + + +\begin{definition} + A function $f : A \to B$ is injective and surjective if it satisfies + the following criteria, respectively. + \begin{itemize} + \item Injective: $\forall a,a' \in A$ if $f(a) = f(a')$ then $a = a'$. + \item Surjective: $\forall b \in B,\exists a \in A$ such that $f(a) = b$. + \end{itemize} + If a function $f$ is both injective and surjective, then it is said + to be a bijective. +\end{definition} +% +A partial function $f : A \pto B$ is injective, surjective, and +bijective whenever the function $f' : \dom(A) \to B$ obtained by +restricting $f$ to its domain is injective, surjective, and bijective +respectively. + +\section{Universal algebra} +\label{sec:universal-algebra} + +\begin{definition}[Algebra]\label{def:algebra} +\end{definition} + +\section{Programming languages} +\label{sec:pls} +% +\dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness} + \chapter{The state of effectful programming} \label{ch:related-work}