\RequirePackage[l2tabu, orthodox]{nag} \documentclass[10pt,fleqn,a4paper]{article} \usepackage{amsmath} \usepackage{stmaryrd} \usepackage{tikz} \usepackage{tikz-cd} \usepackage[bookmarks]{hyperref} \usepackage{savetrees} \newcommand{\ite}[3]{\mathbf{if}\; #1 \;\mathbf{then}\; #2 \;\mathbf{else}\; #3} \newcommand{\lbd}[2]{\lambda #1 \,.\, #2} \newcommand{\fnp}[2]{\text{#1}\;(#2)} \newcommand{\fnw}[2]{\text{#1}\;#2} \newcommand{\fns}[2]{(\text{#1}\;#2)} \DeclareMathOperator{\snd}{snd} \DeclareMathOperator{\fst}{fst} \DeclareMathOperator{\inl}{inl} \DeclareMathOperator{\inr}{inr} \DeclareMathOperator{\id}{id} \title{MBProg Summary} \date{2022-03-28} \author{ Florian Guthmann\\\texttt{florian.guthmann@fau.de} \and } \begin{document} \maketitle{} \section*{Semantics for Computation} \subsection*{Evaluation Strategies} \paragraph{$\alpha$ -conversion} $C[\lbd{x}{t}] \to_\alpha C[\lbd{y}{t[y/x]}]$ \paragraph{$\beta$ -reduction} $C[(\lbd{x}{t}) s] \to_\beta C(t[s/x])$ \paragraph{$\eta$ -reduction} $C[\lbd{x}{f\,x} \to_\eta C[f]]$ \paragraph{Confluence (Church-Rosser)} Independent reductions starting from the same term can always be joined. \paragraph{Church Numerals} \begin{align*} 0 &= \lbd{f}{\lbd{z}{z}}\\ 1 &= \lbd{f}{\lbd{z}{f\,z}}\\ 2 &= \lbd{f}{\lbd{z}{f\,f\,z}}\\ \end{align*} \subsubsection*{Standard} We impose a \emph{left-most-outermost} evaluation order. \paragraph{Standardization Theorem} If $s \to_{\alpha\beta}^* t$ and $t$ is $\alpha\beta$ -normal, then $s\to_{\text{so}}^* t$ and $t$ is so-normal. \subsubsection*{Call-by-Name (lazy)} \paragraph{small-step} \begin{itemize} \item no more rewriting under $\lambda$ \item all terms are closed \end{itemize} \[ \frac{}{(\lbd{x}{p}) q \to p[q/x]}\\ \frac{p\to p'}{pq \to p'q} \] \paragraph{big-step} \[ \frac{}{\lbd{x}{p}\Downarrow \lbd{x}{p}}\\ \frac{q\Downarrow\lbd{x}{p'} \quad p'[q/x] \Downarrow v}{pq\Downarrow v} \] \subsubsection*{Call-by-Value (eager)} \paragraph{Value} A value is a term of the form $\lbd{x}{t}$ \paragraph{small-step} \[ \frac{p \to p'}{pq \to p'q}\\ \frac{q \to q' \quad p \text{ is a value}}{pq \to pq'}\\ \frac{q \text{ is a value}}{(\lbd{x}{p}) q \to p[q/x]} \] \paragraph{big-step} \[ \frac{}{\lbd{x}{p}\Downarrow\lbd{x}{p}}\\ \frac{p\Downarrow\lbd{x}{p'} \quad q\Downarrow q' \quad p'[q'/x]\Downarrow c}{pq\Downarrow c} \] \subsection*{PCF} \paragraph{Simply-Typed Lambda-Calculus} \[ \text{Type} := \underbrace{A,B,C,\dots}_{\text{base types}} | \underbrace{1}_{\text{unit type}} | A \times B | A \to B \] $\Omega = (\lbd{x}{xx})(\lbd{x}{xx})$ is not typable. Thus, $\to_{\alpha\beta}$ is strongly normalising for simply-typed lambda-calculus. We obtain \emph{PCF} by: \begin{itemize} \item adding the fixpoint combinator $Y_A :(A\to A) \to A$ for every type $A$ \item fixing $\mathrm{Nat}$ and $\mathrm{Bool}$ as the base types \item postulating the arithmetic and logical operations \end{itemize} \paragraph{Contextual Equivalence} A term context $C$ is of \emph{ground type} if its type is either $\mathrm{Nat}$, $\mathrm{Bool}$ or $1$. Two PCF terms $\Gamma \vdash s:A$ and $\Gamma \vdash t:A$ are \emph{contextually equivalent}, if for all contexts $C$ of ground type and for all values $v$, $C[s]\Downarrow v$ iff $C[t]\Downarrow v$ \subsubsection*{Operational Semantics} \paragraph{Call-by-Name} A value is \begin{itemize} \item a term of base or unit type \item a pair of closed terms \item a closed term of the form $\lbd{x}{t}$ \end{itemize} \paragraph{Call-by-Value} \begin{itemize} \item a term of base or unit type \item a pair of values \item a closed term of the form $\lbd{x}{t}$ \end{itemize} \subsection*{Denotational Semantics} \paragraph{Partial Order} A partial order $(A, \sqsubseteq)$ is a relation, such that: \begin{itemize} \item $a\sqsubseteq a$ (reflexivity) \item $a \sqsubseteq b \land b \sqsubseteq c \Rightarrow a \sqsubseteq c$ (transitivity) \item $a \sqsubseteq b \land b \sqsubseteq a \Rightarrow a = b$ (antisymmetry) \end{itemize} \paragraph{Complete Partial Order} A complete partial order (pre-domain) is a partial order $(A,\sqsubseteq)$ such that for any infinite chain \[ a_1 \sqsubseteq a_2 \sqsubseteq \dots \] there is a least upper bound $a$ such that \begin{itemize} \item $\forall i.\; a_i\sqsubseteq a$ \item $\forall i.\; a_i \sqsubseteq b \Rightarrow a\sqsubseteq b$ \end{itemize} We denote such a by $\bigsqcup_i a_i$ \paragraph{Domain} A pointed cpo (\emph{domain}) is a cpo that contains an element $\bot$ such that $\forall a\in A. \bot \sqsubseteq a$ \paragraph{Monotonicity} A function $f: A\to B$ between partial orders is \emph{monotone} if \[ a \sqsubseteq b \Rightarrow f(a) \sqsubseteq f(b) \] \paragraph{Scott-continuity} A monotone function $f : A\to B$ between cpos is continuous if for any chain $a_1 \sqsubseteq a_2 \sqsubseteq \dots$ \[ f\left(\bigsqcup_i a_i\right) = \bigsqcup_i f(a_i) \] \paragraph{Strictness} A function $f: a\to B$ is \emph{strict} if $f(\bot) = \bot$ \paragraph{Products of Predomains} \[ A\times B = \{(a,b) | a\in A, b\in B\}\\ (a_1,b_1) \sqsubseteq (a_2,b_2) \text{if} a_1 \sqsubseteq a_2 \land b_1 \sqsubseteq b_2 \] Pairing is continuous: $\bigsqcup_i(a_i,b_i) = \left(\bigsqcup_ia_i, \bigsqcup_jb_j\right)$ \paragraph{Lifting predomains and functions} \[ A_\bot = A \uplus {\bot} = {(\star,a)| a\in A} \cup {(\bot,\star)}\\ a\sqsubseteq b \text{ if } a =\bot \text{ or } a\in A,b\in A \text{ and } a\sqsubseteq b\\ \] \[ f^*(x) = \begin{cases} f(y) & \text{if } x = \lfloor y \rfloor\\ \bot & \text{if } x = \bot \end{cases} \] \paragraph{Function Spaces} Let $(A,\sqsubseteq)$, $(B,\sqsubseteq)$ be predomains. $(A \to B,\sqsubseteq)$ is the function space predomain where: \[ A\to B = \{f: A\to B \mid f \text{ is continuous}\}\\ f\sqsubseteq g \Leftrightarrow \forall x. f(x) \sqsubseteq g(x) \] We define: \begin{align*} \text{curry} &: (A\times B \to C)\to (A\to (B \to C))\\ \text{uncurry} &: (A\to (B \to C))\to (A \times B \to C)\\ \text{ev} &: (A\to B) \times A \to B\\ \end{align*} If $B$ is a domain, so is $A\to B$ with the bottom element being $\lbd{x}{\bot}$ \paragraph{Kleene`s Fixpoint Theorem} Let f be a continuous function $f: D\to D$ over a domain $D$ \begin{itemize} \item least fixpoint: $\exists \mu f \in D$ such that $f(\mu f) = \mu f$ and $\forall x \in D. f(x) = x \Rightarrow \mu\;f \sqsubseteq x$ \item $\mu\;f = \bigsqcup_if^i(\bot)$, where $f^0(x) = \bot, f^{i+1}(x) = f(f^i(x))$ \item least prefixpoint: $f(\mu\;f) \sqsubseteq \mu\;f$ and $\forall x \in D. f(x) \sqsubseteq x \Rightarrow \mu\;f \sqsubseteq x$ \end{itemize} \subsubsection*{CBN} \paragraph{Soundness} A denotational semantics is \emph{sound} if \[ p\Downarrow v \Rightarrow \llbracket p \rrbracket = v \] \paragraph{Adequacy} A denotational semantics is \emph{adequate} if for $p$ of ground type \[ \llbracket p \rrbracket = v \Rightarrow p \Downarrow v \] for every \emph{value} $v$ \paragraph{Compositionality} \[ \llbracket C[t] \rrbracket =\llbracket C \rrbracket\left[\llbracket t \rrbracket\right] \] \begin{align*} \llbracket 1 \rrbracket &= 1_\bot\\ \llbracket \mathrm{Nat} \rrbracket &= \mathrm{Nat}_\bot\\ \llbracket \mathrm{Bool} \rrbracket &= \mathrm{Bool}_\bot\\ \llbracket A\times B \rrbracket &= \llbracket A \rrbracket \times \llbracket B \rrbracket\\ \llbracket A\to B \rrbracket &= \llbracket A \rrbracket \to \llbracket B \rrbracket\\ \end{align*} Given a term in context $\Gamma \vdash t: A$ where $\Gamma = x_1:A_1,\dots,x_n:A_n$ the semantics $\llbracket \Gamma \vdash t:A\rrbracket$ is a continuous function $\llbracket A_1\rrbracket \times \dots \times \llbracket A_n\rrbracket \to \llbracket A \rrbracket$ ($\llbracket\dots\rrbracket_\rho = \llbracket\dots\rrbracket(\rho)$) \begin{align*} \llbracket \Gamma \vdash x_i:A_i\rrbracket_\rho &= \mathrm{proj}_i(\rho)\\ \llbracket \Gamma \vdash \star:1\rrbracket_\rho &= \lfloor \star \rfloor\\ \vdots&\\ \llbracket \Gamma \lbd{x}{t} : A\to B\rrbracket_\rho &= (\mathrm{curry} \llbracket\Gamma,x:A \vdash t:B\rrbracket)(\rho)\\ \llbracket \Gamma st: B\rrbracket_\rho &= \mathrm{ev}(\llbracket\Gamma\vdash s: A\to B\rrbracket_\rho,\rrbracket\Gamma\vdash t: A\rrbracket_\rho\\ \llbracket\Gamma \vdash Y_A\rrbracket &=\mu \end{align*} \subsubsection*{CBV} \subsubsection*{Full Abstraction} The implication $p =_{ctx} q \Rightarrow \llbracket p \rrbracket = \llbracket q \rrbracket$ is called full abstraction. It would mean that operational semantics and denotational semantics agree as far as program equivalence. However consider the \texttt{por} function. It is not definable in PCF, but it is a continuous function and thus can be used in the denotational semantics. \begin{align*} \mathtt{por}(\mathrm{True},x) &= \mathrm{True}\\ \mathtt{por}(x,\mathrm{True}) &= \mathrm{True}\\ \mathtt{por}(\mathrm{False}, \mathrm{False}) &= \mathrm{False}\\ \mathtt{por}(x,y) &= \bot \end{align*} We can construct a function $t: \mathrm{Bool} \to (\mathrm{Bool} \to \mathrm{Bool} \to \mathrm{Bool}) \to \mathrm{Bool}$ in PCF that tests if a given function is $\mathtt{por}$. \section*{Category Theory} \paragraph{Category} A Category $\mathcal{C}$ consist of a collection of objects $\mathrm{Ob}(\mathcal{C})$ and a collection of morphisms $\mathrm{Hom}_{\mathcal{C}}(A,B)$ for any $A,B \in \mathrm{Ob}(\mathcal{C})$ such that: \begin{itemize} \item for every $A\in \mathrm{Ob}(\mathcal{C})$ there is an \emph{identity morphism} $id_A \in \mathrm{Hom}_{\mathcal{C}}(A,A)$ \item for any $f \in \mathrm{Hom}_{\mathcal{C}}(B,C)$ and $g \in \mathrm{Hom}_{\mathcal{C}}(A,B)$ we can form a \emph{composition} $f\circ g \in \mathrm{Hom}_{\mathcal{C}}(A,C)$ \item $\id\circ f = f$ (left identity) \item $f\circ \id = f$ (right identity) \item $(f\circ g) \circ h = f \circ (g \circ h)$ (associativity) \end{itemize} \paragraph{Terminal Object} A terminal object is an object $1\in \mathrm{Ob}(\mathcal{C})$ such that for any $A\in \mathrm{Ob}(\mathcal{C})$, there is a unique morphism $!_A : A \to 1$. \paragraph{Initial Object} An initial object is an object $0 \in \mathrm{Ob}(\mathcal{C})$ such that for any $A\in \mathrm{Ob}(\mathcal{C})$, there is a unique morphism $\mbox{!`}_A : 0 \to A$. \paragraph{Isomorphism} An \emph{isomorphism} between objects $A$ and $B$ in a category $\mathcal{C}$ is a pair of morphisms $f : A\to B,\;g : B \to A$ such that: \[ \begin{tikzcd} A \arrow[r, "f"] \arrow[rd, "\id_A"'] & B \arrow[d, "g"] \arrow[rd, "\id_B"] & \\ & A \arrow[r, "f"] & B \end{tikzcd} \] \paragraph{Cartesian Category} A \emph{cartesian category} is a category with a terminal object an binary products \subsection*{Products and Coproducts} \subsubsection*{Binary Products} A product of objects $A,B$ in a category $\mathcal{C}$ is a triple $(A\times B, \fst, \snd)$ such that for any $C\in \mathrm{Ob}(\mathcal{C})$ and $f: C\to A$ and $g : C\to B$ there is a \emph{unique} morphism $\langle f,g \rangle : C \to A \times B$: \[ \begin{tikzcd} & C \arrow[ld, "f"'] \arrow[rd, "g"] \arrow[d, "{\langle f,g\rangle}"', dashed] & \\ A & A\times B \arrow[r, "\snd"'] \arrow[l, "\fst"] & B \end{tikzcd} \] \subsubsection*{Coproducts} A coproduct of objects $A,B$ in a category $\mathcal{C}$ is a triple $(A+B, \inl, \inr)$ such that for any $f: A\to C$ and $g : B\to C$ there is a \emph{unique} morphism $[f,g] : A+B\to C$: \[ \begin{tikzcd} & C & \\ A \arrow[r, "\inl"'] \arrow[ru, "f"] & A+B \arrow[u, "{[f,g]}", dashed] & B \arrow[l, "\inr"] \arrow[lu, "g"'] \end{tikzcd} \] \subsection*{Functor} A covariant Functor $F$ between categories $\mathcal{C}$ and $\mathcal{D}$ is a correspondence sending any $A\in \mathrm{Ob}(\mathcal{C})$ to $FA\in \mathrm{Ob}(\mathcal{D})$ and any $f\in \mathrm{Hom}_{\mathcal{C}}(A,B)$ to $Ff\in \mathrm{Hom}_{\mathcal{D}}(FA,FB)$ such that: \[ F(\id_A) = \id_{FA}\\ F(f\circ g) = F(f) \circ F(g) \] \paragraph{Example: Forgetful Functor} \[ G: \mathrm{Cpo} \to \mathrm{Set}\\ G(A,\sqsubseteq) = A\\ G(f) = f \] \paragraph{Example: Endofunctor} An \emph{endofunctor} is a functor from a category into itself. \paragraph{Contravariant Functor} A functor $F: \mathcal{C}^{\mathrm{op}} \to D$ is a contravariant functor from $\mathcal{C}$ to $\mathcal{D}$. \paragraph{Bifunctor} A bifunctor is a functor $\mathcal{C}\times\mathcal{D}\to \mathcal{E}$. \subsection*{Natural Transformations} Let $\mathcal{C}, \mathcal{D}$ be categories and $F,G : \mathcal{C} \to \mathcal{D}$ be functors. A \emph{natural transformation} $\vartheta : F \to G$ is a family of morphisms \[ (\vartheta_C : FC \to GC)_{c\in \mathrm{Ob}(\mathcal{C})} \] such that $\forall f : C \to C'$ in $\mathcal{C}$: \[ \begin{tikzcd} FC \arrow[d, "\vartheta_C"] \arrow[r, "Ff"] & FC' \arrow[d, "\vartheta_{C'}"] \\ GC \arrow[r, "Gf"] & GC' \end{tikzcd} \] \subsection*{Monad} \subsubsection*{Kleisli Triple} A \emph{Monad} in a category $\mathcal{C}$ is given by a triple $(T,\eta, -^*)$ where: \begin{itemize} \item $T: \mathrm{Ob}(\mathcal{C}) \to \mathrm{Ob}(\mathcal{C})$ \item unit: $\eta$ is a family $(\eta_X : X \to TX)_{x\in \mathrm{Ob}(\mathcal{C})}$ \item Kleisli lifting: for any $f : A \to TB$, $f^* : TA \to TB$ \end{itemize} such that: \[ \eta^* = \id\\ f^* \eta = f\\ (f^*g)^* = f^*g^* \] \paragraph{Kleisli Category} \subsubsection*{From Endofunctor and Natural Transformation} A \emph{Monad} in a category $\mathcal{C}$ consists of an endofunctor $T: \mathcal{C} \to \mathcal{C}$ an natural transformations \begin{itemize} \item unit: $\eta : \mathrm{Id} \to T$ \item multiplication: $\mu : TT \to T$ \end{itemize} such that: \[ \mu\circ\mu_T = \mu\circ T\mu \\ \mu\circ\eta_T = \id = \mu\circ T\eta \] \[ \begin{tikzcd} TTTX \arrow[r, "\mu_{TX}"] \arrow[d, "T\mu_X"] & TTX \arrow[d, "\mu_X"] & & TX \arrow[r, "\eta_{TX}"] \arrow[rd, "\id_{TX}"'] & TTX \arrow[d, "\mu_X"] & TX \arrow[l, "T\eta_X"'] \arrow[ld, "\id_{TX}"] \\ TTX \arrow[r, "\mu_X"] & TX & & & TX & \end{tikzcd} \] \subsection*{Tensorial Strength} \paragraph{Cartesian Closure} A category $\mathcal{C}$ is \emph{cartesian closed}(CCC) if it is cartesian, and for any objects $B$ and $C$ there is an object $B^C$, called an exponential, for which \[ \text{curry}: \mathrm{Hom}(A\times B,C) \cong \mathrm{Hom}(A, C^B) \] which is natural in $A$ such that \[ \begin{tikzcd} {\mathrm{Hom}(A\times B,C)} \arrow[rr, "\text{curry}"] \arrow[d, "{\mathrm{Hom}(f\times B,C)}"] & & {\mathrm{Hom}(A,C^B)} \arrow[d, "{\mathrm{Hom}(f,C^B)}"] \\ {\mathrm{Hom}(A'\times B,C)} \arrow[rr, "\text{curry}"] & & {\mathrm{Hom}(A',C^B)} \end{tikzcd} \] We can generalize the CBV semantics of PCF by: \begin{itemize} \item replace $(-)_\bot$ with $T$ \item replace ``let'' with ``do'' \item replace $\lfloor - \rfloor$ with \texttt{return} \end{itemize} \paragraph{Strong Functor} A strong Functor is a functor $F: \mathcal{C}\to\mathcal{D}$ between cartesian categories $\mathcal{C}$ and $\mathcal{D}$, plus \emph{strength}, which is a natural transformation $\tau_{A,B}:A\times FB \to F(A\times B)$ such that \[ \begin{tikzcd} 1\times FX \arrow[rr, "\snd"] \arrow[d, "\tau"] & & FX \\ F(1\times X) \arrow[rru, "F(\snd)"] & & \end{tikzcd}\\ \begin{tikzcd} X\times Y \times FZ \arrow[rr, "\tau"] \arrow[d, "\mathrm{assoc}"] & & F((X\times Y)\times Z) \arrow[d, "{F\,\mathrm{assoc}}"] \\ X\times(Y\times FZ) \arrow[rd, "X\times\tau"] & & F(X\times (Y\times Z)) \\ & X\times F(Y\times Z) \arrow[ru, "\tau"] & \end{tikzcd} \] \subsubsection*{Strong Monads} A monad is \emph{strong} if it is strong as a functor and $\eta,\mu$ are strong natural transformations. \[ \begin{tikzcd} X\times Y \arrow[r, "\eta"] \arrow[d, "\id\times\eta"'] & T(X\times Y) \\ X\times TY \arrow[ru, "\tau"'] & \end{tikzcd}\\ \begin{tikzcd} X\times TTY \arrow[rr, "\id\times\mu"] \arrow[d, "\tau"] & & X\times TY \arrow[d, "\tau"] \\ T(X\times TY) \arrow[rd, "T\tau"] & & T(X\times Y) \\ & TT(X\times Y) \arrow[ru, "\mu"] & \end{tikzcd} \] \subsubsection*{Commutative Monads} A strong monad $T$ is commutative if \begin{tikzcd} TA\times TB \arrow[r, "\tau"] \arrow[d, "\hat{\tau}"] & T(TA\times B) \arrow[r, "T\hat{\tau}"] & TT(A\times B) \arrow[dd, "\mu"] \\ T(A\times TB) \arrow[d, "T\tau"] & & \\ TT(A\times B) \arrow[rr, "\mu"] & & T(A\times B) \end{tikzcd} In other words, \[ \text{do}\; x = p; \text{do}\; y = q; \text{return} \langle x,y\rangle == \text{do}\; y = q; \text{do}\; x = p; \text{return} \langle x,y\rangle \] \subsubsection*{Monoidal Categories} A category $\mathcal{C}$ is \emph{monoidal} if there exists: \begin{itemize} \item a bifunctor $C \times C \to C$ (tensor product) \item an object $I$ (unit object) \item natural transformations \[ \alpha_{A,B,C}: A \otimes (B\otimes C) \cong (A\otimes B) \otimes C\\ \lambda_{A}: I\otimes A \cong A\\ \rho_A:A\otimes I \cong A \] \end{itemize} A \emph{monoid} in a monoidal Category $\mathcal{C}$ is a triple $(M,\varepsilon, \odot)$ where $M$ is an object in $\mathcal{C}$, $\odot$ is a morphism $M\otimes M \to M$ and $\varepsilon$ is a morphism $I\to M$ such that: \[ \begin{tikzcd} M\otimes I \arrow[rd, "\rho_M"] \arrow[r, "\id_m\otimes\varepsilon"] & M\otimes M \arrow[d, "\odot"] & I\otimes M \arrow[ld, "\lambda_M"] \arrow[l, "\varepsilon\otimes \id_M"] \\ & M & \end{tikzcd}\\ \begin{tikzcd} M\otimes (M \otimes M) \arrow[rr, "{\alpha_{M,M,M}}"] \arrow[dd, "\id_M\otimes\odot"] & & (M\otimes M)\otimes M \arrow[dd, "\odot\otimes \id_M"] \\ & & \\ M\otimes M \arrow[r, "\odot"'] & M & M\otimes M \arrow[l, "\odot"] \end{tikzcd} \] \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: