(* #FORMAT FormatSlides *)
(* #DIRECTORIES Format *)
(* #GRAMMAR Format/notations *)
(* #PACKAGES Typography.DriverCairo *)
(* #PACKAGES bibi *)
(* #DRIVER Pdf *)

\Caml(
open Diagrams
)
\Include{Preamble}
\Include{MoreFig}
\Include{Macros}


\begin{slide}
    \begin{center}
 \size(5.){Towards a theory of programming languages}

\vspaceBefore(5.)
Tom Hirschowitz

\vspaceBefore(5.)
\id(includeGraphics ~scale:0.05 "bare-lama.jpg") LAMA, CNRS et Université de Savoie

\end{center}
\end{slide}


\begin{slide}
\begin{center}
\begin{env}(fun env->{env with normalMeasure=env.normalMeasure/.2.})
    \TableOfContents
\end{env}
\end{center}
\end{slide}


== The question ==

\begin{slide}

\Title{The ladder of abstraction (© Brett Victor): level 1}

\alert{Formal reasoning} over practical things like
\begin{center}
\diagram(
let m,ms = array [`East;`West] [[
    <$\mathsText(<<counting:>>)$> ; <$\mathsText(<<integers,>>)$>
    ];[
    <$\mathsText(<<moving:>>)$> ; <$\mathsText(<<transformations of the plane,>>)$>
    ];[
    <$\mathsText(<<exchanging:>>)$> ; <$\mathsText(<<permutations.>>)$>
    ]]
    
)
\end{center}

\end{slide}

\begin{slide}

\Title{The ladder of abstraction: level 2}

Common properties of:
\begin{itemize}
\item integers,
\item rotations,
\item translations,
\item symmetries,
\item isometric,transformations.
\item permutations on a finite set…
\end{itemize}

\begin{block}{Abstraction}
Notion of \intro{group}.
\end{block}
\end{slide}


\begin{slide}
\Title{The ladder of abstraction: towards level 3}
\begin{block}{Neighbours}
\begin{itemize}
\item Generalisation: monoids (e.g., all transformations of the plane).
\item Specialisation: rings, modules, algebras, …
\end{itemize}
\end{block}
\begin{block}{Problem}
\begin{itemize}
\item Numerous \alert{abstract} notions.
\item A lot in common: \begin{itemize}
      \item free constructions (e.g., free monoid = words);
      \item notions of morphisms;
      \item downcasting (any ring is a group, at least).
\end{itemize}
\end{itemize}
\end{block}
\end{slide}

\begin{slide}
\Title{The ladder of abstraction: level 3}

\begin{block}{Abstraction over abstraction!}
Two proposals:
\begin{itemize}
\item Lawvere theories;
\item monads on sets.
\end{itemize}
Lawvere theories a little more general.
\end{block}

\vspaceBefore(4.)
Programming language theory: still at level 2!
\end{slide}

\begin{slide}
\Title{Level 1: calculi}
Programming languages $↝$ \intro{calculi}:
\begin{itemize}
\item pure $λ$-calculus,
\item $λ$-calculus in cbv, cbn, lazy, fully lazy, optimal, …
\item $λ$-calculus with \verb{let rec} / refs / \verb{call/cc}, …
\item $ζ$, $λσ$, $\oline{λ}μ\oline{μ}$, …
\item $π$, join, Ambients, Spy, …
\end{itemize}
\begin{block}{Analogy}
Reasoning over integers $≈$ Reasoning over programs in language $L$.
\end{block}
And that's only the \alert{untyped} tip of the iceberg!
\end{slide}

\begin{slide}
\Title{Level 2: denotational semantics}
\begin{itemize}
\item Denotational model of language $L$ $≈$ mathematical structure supporting the operations of $L$.
\item $L$ $≈$ `free' structure.
\end{itemize}
\begin{block}{Common use of denotational semantics}
Disprove a property of programs by finding a counter-model. 
\end{block}
\begin{center}
\diagram(
let m,ms = array [`East;`West;`West] [[
    <$\mathsText(<<Groups:>>)$> ; <$\mathsText(<<integers,permutations, …>>)$>
    ];[
    <$\mathsText(<<Rings:>>)$> ; <$\mathsText(<<integers, polynomials, …>>)$>
    ];[
    <$\mathsText(<< Models of simply-typed $λ$: >>)$> ; <$\mathsText(<<cartesian closed categories, … >>)$> ;
    ]]
    
)
\end{center}

Rk: not all calculi are at level 2 (i.e., equipped with a notion of model).


\end{slide}

\begin{slide}
\Title{Towards level 3?}

\begin{center}
\diagram(
let m,ms = array [`East;`West;`West] [[
    <$\mathsText(<<Groups:>>)$> ; <$\mathsText(<<integers,permutations, …>>)$>
    ];[
    <$\mathsText(<<Rings:>>)$> ; <$\mathsText(<<integers, polynomials, …>>)$>
    ];[
    <$\mathsText(<< $X$-calculus: >>)$> ; <$\mathsText(<<models of $X$, >>)$> ;
    ]]

let x,y = ms.(0).(1).Node.anchor `NorthEast
let x',y' = ms.(1).(1).Node.anchor `SouthEast
let xm = x +. 4.

let e = Edge.(edge [draw;bendLeft 30.] 
    (coordinate (x,y)) ~controls:[[(xm,y); (xm,y')]]
    (coordinate (x,y')))

let lt = node Node.([at (xm, 0.5 *. (y +. y')); anchor `West]) <<Lawvere theories>>

let _ = node Node.([at (xm,snd (ms.(2).(1).Node.anchor `East)); anchor `West]) <<\alert{Lawvere theory?}>>
)
\end{center}

No, for at least two reasons:
\begin{itemize}
\item variable binding ($λx.x ≡ λx'.x'$);
\item dynamics $(λx.M) N ↝ M [x ↦ N]$: need for `directed' equations.
\end{itemize}
\begin{block}{}
Need to generalise Lawvere theories!
\end{block}
\end{slide}

\begin{slide}
\Title{Hence the question}

\begin{itemize}
\item What is a programming language?
\item What is a translation between two programming languages?
\item General results?
\end{itemize}

\vspaceBefore(4.)
\begin{block}{}
Let us start with a (fake) poll…
\end{block}
\end{slide}

\begin{slide}
\Title{Fake poll: what is a programming language?}
\begin{block}{Low-level answer}
\begin{itemize}
\item a language on a finite alphabet,
\item a translation to \verb{x86} (…).
\end{itemize}
\end{block}

\begin{itemize}
\item Why definitely fix \verb{x86}?
\begin{itemize}
\item Low-level does evolve a lot (shit, it's \verb{amd64} already…). 
\item Sometimes overkill, e.g., language of regular expressions.
\item Not canonical. 
\item Limited: e.g., distributed computing.
\end{itemize}
\item Not won at the level of high-level reasoning on programs.
\end{itemize}

\end{slide}


\begin{slide}
\Title{Fake poll: what is a programming language?}
\begin{block}{Frequent answer by researchers in programming languages}
\alert{One} super complex language supposed to model all other languages.
\end{block}
\begin{itemize}
\item Illusory.
\item Adding features may change global properties: study of fragments.
\item Eludes the crucial question of what \alert{morphisms} should be.
\end{itemize}
\end{slide}


\begin{slide}
\Title{Fake poll: what is a programming language?}
\begin{block}{Other frequent answer mostly in the UK}
A \intro{structural operational semantics} (Plotkin, 1981), in a certain \intro{format}.
\end{block}

\begin{itemize}
\item Low-level notion of syntax with binding.
\item Morphisms: only starting to be investigated.
      \item Far from mainstream mathematics.
\end{itemize}
\end{slide}


\begin{slide}
\Title{Fake poll: what is a programming language?}
\begin{block}{Other frequent answer}
A \intro{higher-order rewrite system} (Nipkow, 1991).
\end{block}
Close answer: a \intro{combinatory reduction system} (Klop, 1980).
\begin{itemize}
\item Roughly, rewriting terms with variable binding.
\item \alert{No} notion of morphism, even google does not find anything.
\item Far from mainstream mathematics.
\end{itemize}
\end{slide}

\begin{slide}
\Title{}
About the last two,
\begin{itemize}
\item structural operational semantics (SOS) and
\item higher-order rewriting (HOR).
\end{itemize}
\begin{block}{}
\begin{itemize}
\item General results, but on \alert{one} language:
\begin{itemize}
\item congruence of bisimilarity (SOS),
\item confluence, finite developments, etc (HOR).
\end{itemize}
\item Better, hints at level 3:\begin{itemize}
\item \intro{mathematical operational semantics} (SOS, Turi and Plotkin),
\item \intro{cartesian closed 2-categories} (HOR, main subject here).
\end{itemize}
\end{itemize}

\end{block}\end{slide}


== Lawvere theories ==

\begin{slide}
\Title{Lawvere theories in 20 slides}
Starters: introduction to \intro{category theory}, then \intro{Lawvere theories}.
\end{slide}

\begin{slide}
\Title{Categories}

\begin{definitionstar}
Category:
	a (directed, multi) graph equipped with 
\begin{itemize}
\item	a \intro{composition} law on edges,
\item \intro{identities}.
\end{itemize}
\end{definitionstar}

\begin{center}
\diagram(

  let m,ms = simple_math_matrix ~style:Matrix.([centers 10. 30.]) [[
  [];  <$B$> ];[
  <$A$> ; [] ; <$C$> ]]

  let _ = sedges_matrix ms Edge.([
    ([labelal <<$f$>>],(1,0),(0,1));
    ([labelar <<$g$>>],(0,1),(1,2));
    ([bendRight 20.;labelb <<$g ∘ f$>>],(1,0),(1,2));
  ])

)
\end{center}

\end{slide}

\begin{slide}
\Title{Examples}

\begin{itemize}
\item 
The category $Grp$.\begin{itemize}
\item Vertices / \intro{objects}: groups.
\item Edges / \intro{morphisms}: morphisms of groups.
\end{itemize}

\item
\alert{Large category}.

\item
Similar examples: monoids, rings, etc.
\item Topological spaces and continuous functions: $Top$.
\item Graphs: $Gph$.
\item Even plain \alert{sets}: $Set$.
\end{itemize}
\end{slide}

(* \begin{slide} *)
(* \Title{Gros exemples 2} *)

(* \begin{itemize} *)
(* \item N'importe quel préordre.\begin{itemize} *)
(* \item Objets: éléments du préordre. *)
(* \item Morphismes $x → y$: \begin{itemize} *)
(* \item un seul si $x ≤ y$, *)
(* \item pas du tout sinon. *)
(* \end{itemize} *)
(* \end{itemize} *)
(* \end{itemize} *)

(* \begin{center} *)
(* \diagram( *)

(*   let m,ms = simple_math_matrix ~style:Matrix.([centers 10. 30.]) [[ *)
(*   [];  <$y$> ];[ *)
(*   <$x$> ; [] ; <$z$> ]] *)

(*   let _ = sedges_matrix ms Edge.([ *)
(*     ([labelal <<$≤$>>],(1,0),(0,1)); *)
(*     ([labelar <<$≤$>>],(0,1),(1,2)); *)
(*     ([bendRight 20.;labelb <<$≤$>>],(1,0),(1,2)); *)
(*   ]) *)

(* ) *)
(* \end{center} *)
(* \end{slide} *)

\begin{slide}
\Title{Cartesian product (\alert{in any category}!)}
\begin{itemize}
\item Consider any objects $A, B ∈ \cat$;
\item $A \xot{π} C \xto{π'} B$ is a \intro{product} of $A$ and $B$ iff
\begin{center}
\diagram(
let m,ms = simple_math_matrix [[
    [];    <${∀} D$> 
    ];[
    <$A$> ; <$C$> ; <$B$> 
    ]]

let _ = sedges_matrix ms Edge.([
        ([labelal <<${∀} f$>>],(0,1),(1,0)) ;
        ([labelar <<${∀} g$>>],(0,1),(1,2)) ;
        ([labelb <<$π$>>],(1,1),(1,0)) ;
        ([labelb <<$π'$>>],(1,1),(1,2)) ;
        ([dashed [2.];labell <<${∃} {!} h$>>],(0,1),(1,1)) ;
    ])
)
\end{center}
\item Notation: $C = A × B$ and $h = ⟨ f , g ⟩$.
\end{itemize}
\begin{examplestar}
\begin{itemize}
\item $Set$, $Grp$, $Top$,…
\item Graphs.
\end{itemize}
\end{examplestar}

\end{slide}

\begin{slide}
\Title{Terminal object}
\begin{itemize}
\item $A$ is a \intro{terminal} object in $\cat$ iff
\diagram(
let m,ms = simple_math_matrix [[
    <${∀} B$> ; <$A\textdot$>
    ]]

let _ = sedges_matrix ms Edge.([
        ([dashed [2.];labela <<${∃} {!} f$>>],(0,0),(0,1)) ;
    ])
)
\item Notation: $A = 1$, $f = {!}B$.
\end{itemize}

\begin{examplestar}
\begin{itemize}
\item Sets: singleton.
\item Graphs: what would you guess?
\end{itemize}
\end{examplestar}

\end{slide}

\begin{slide}
\Title{Finite products = products + terminal objects}

\begin{definitionstar}
Category with \intro{finite products}: \begin{itemize}
\item a product $(A × B, π, π')$ for all $A,B$,
\item a terminal object $1$.
\end{itemize}
\end{definitionstar}

\end{slide}

\begin{slide}
\Title{First insight of Lawvere theories}

\begin{observation_star}
Any model of an algebraic theory `is' a category with finite products.
\end{observation_star}

\begin{states}([0])
I.e.,
\begin{itemize}
\item Any monoid is a category with finite products.
\item Any ring is a category with finite products.
\item …
\end{itemize}
\end{states}
\begin{states}([1])
\begin{examplestar}
Category $\cat_ℕ$ for the monoid of natural numbers and $+$:\begin{itemize}
\item objects are finite `powers' of $ℕ$, e.g., $ℕ × ℕ × ℕ$;
\item morphisms are functions generated by\begin{itemize}
\item addition $ℕ × ℕ → ℕ$,
\item zero $1 → ℕ$ (the map picking $0$), 

\item identities and composition, \vspaceBefore(1.3)
\item pairing $⟨f₁,…,fₙ⟩ : ℕᵖ → ℕⁿ$, 
\item projections $π_{n,i} : ℕⁿ → ℕ$, 
\item the unique map $ℕᵖ → 1$.
\end{itemize}
\end{itemize}
\end{examplestar}
This is a subcategory of $Set$.
\end{states}
\end{slide}

\begin{slide}
\Title{The category $\cat_ℕ$ (looking closer)}

\begin{itemize}
\item Any morphism $f : ℕᵖ → ℕⁿ$ decomposes as 
$⟨f₁,…,fₙ⟩$.
\item Example morphism
$plus ∘ ⟨ π, plus ∘ ⟨π', (zero ∘ {!}(ℕ²))⟩ ⟩ : ℕ² → ℕ\textdot$
\item A.k.a. $plus (x, (plus (y, zero)))\textdot$

\item A.k.a. $\exmorphism{ℕ}{plus}{zero}(5.)(10.)$

$≈$ circuits with sharing restricted to inputs.
\item Variables: dealt with by projections.

\end{itemize}\end{slide}

\Caml(let blueX : math_macro = <$\alertm{X}$>
let bluem : math_macro = <$\alertm{m}$>
let bluee : math_macro = <$\alertm{e}$>
)

\begin{slide}
\Title{\alert{Any} monoid $\blueX$ `is' a category $\cat_\blueX$ with finite products}

\begin{block}{General construction}
Category $\cat_\blueX$ for the monoid $(\blueX,\bluem,\bluee)$:\begin{itemize}
\item objects are finite `powers' of $\blueX$, e.g., $\blueX × \blueX × \blueX$;
\item morphisms are functions generated by\begin{itemize}
\item $\bluem : \blueX × \blueX → \blueX$,
\item $\bluee : 1 → \blueX$ (the map picking $e$), 

\item identities and composition, \vspaceBefore(1.3)
\item pairing $⟨f₁,…,fₙ⟩ : \blueXᵖ → \blueXⁿ$, 
\item projections $π_{n,i} : \blueXⁿ → \blueX$, 
\item the unique map $\blueXᵖ → 1$.
\end{itemize}
\end{itemize}
\end{block}
Again a subcategory of $Set$.
\end{slide}


\begin{slide}
\Title{The Lawvere theory for monoids}
\begin{definitionstar}
The category $\cal{L}_{monoid}$ defined by:
\begin{itemize}
\item Objects: one object, say $t$, and its \alert{formal} finite powers $t × … × t$.
\item Morphisms \alert{$t × … × t → t$}: \intro{terms} generated by 
\begin{itemize}
\item binary $m$,
\item constant $e$,
\item in $n$ (ordered) variables,
\end{itemize}
up to a few equations.
\item Morphisms $tⁿ → tᵖ$: $p$-tuples of terms.
\item Composition = simultaneous substitution.
\end{itemize}
\end{definitionstar}
Not directly a subcategory of sets.
\end{slide}

\begin{slide}
\Title{The Lawvere theory for monoids}

In $\cal{L}_{monoid}$, example morphism

\begin{center}
$\exmorphism{t}{m}{e}(5.)(10.)$ cf. $\exmorphism{ℕ}{plus}{zero}(5.)(10.)$
\end{center}
\begin{block}{Observation}
There seems to be a `map' $\cal{L}_{monoid} → \cat_ℕ$.
\end{block}

\end{slide}

\begin{slide}
\Title{Generalised monoids}
\begin{definitionstar}
A \intro{generalised monoid} is \begin{itemize}
\item a category $\cat$ with finite products,
\item an object $X ∈ \cat$,
\item morphisms $comp : X × X → X$ and $unit : 1 → X$,
\item satisfying the obvious associativity and unitality equations.
\end{itemize}
\end{definitionstar}
\begin{examplestar}
\begin{itemize}
\item $\cat_ℕ$,
\item $\cat_X$, for any monoid $X$,
\item $\cal{L}_{monoid}$.
\item A bigger one: $Set$ with, e.g., $ℕ$ and addition.
\end{itemize}
\end{examplestar}
\end{slide}

\begin{slide}
\Title{Morphisms}
\begin{definitionstar}
A \intro{morphism of generalised monoids} is
\begin{itemize}
\item a \intro{functor} $F : \cat → \catD$ between underlying categories,
\end{itemize}
\end{definitionstar}
Wait wait, what's a functor?
\end{slide}

\begin{slide}\Title{Functors}
\begin{definitionstar}
A \intro{functor} $\cat → \catD$ is a `morphism of categories':\begin{itemize}
\item a map from objects of $\cat$ to objects of $\catD$,
\item a map between morphisms \size(3.){(preserving source and target)},
\end{itemize}
preserving composition and identities.
\end{definitionstar}

(* \begin{examplestar} *)
(* `Forgetful' functor $U : Grp → Set$ maps:\begin{itemize} *)
(* \item any group $G$ to its underlying set $|G|$, *)
(* \item any morphism of groups to its underlying function. *)
(* \end{itemize} *)
(* Does satisfy $U (g ∘ f) = U (g) ∘ U (f)$ and $U (id_G) = id_{|G|}$. *)
(* \end{examplestar} *)

\begin{examplestar}
The `map' $\cal{L}_{monoid} → \cat_ℕ$ determined by
\begin{center}
$\exmorphism{t}{m}{e}(3.)(5.) ↦ \exmorphism{ℕ}{plus}{zero}(3.)(5.)$
\end{center}
\end{examplestar}

\end{slide}


\begin{slide}\Title{Morphisms}
\begin{definitionstar}
A \intro{morphism of generalised monoids} is
\begin{itemize}
\item a \intro{functor} $F : \cat → \catD$ between underlying categories,
\item preserving products: $F (A × B) = F(A) × F(B)$ \size(3.){(subtlety here, who can guess?)},
\item mapping $X$, $comp$, and $unit$ in $\cat$ to their counterparts in $\catD$.
\end{itemize}
\end{definitionstar}
\begin{examplestar}
Again, the functor $\cal{L}_{monoid} → \cat_ℕ$ determined by
\begin{center}
$\exmorphism{t}{m}{e}(3.)(5.) ↦ \exmorphism{ℕ}{plus}{zero}(3.)(5.)$
\end{center}
In particular $t × t ↦ ℕ × ℕ$.
\end{examplestar}
\end{slide}



\begin{slide}
\Title{The Lawvere theory for monoids}

\begin{propositionstar}
\begin{center}
Generalised monoids 

$≃$ 

categories $\cat$ with a finite-product preserving functor $\cal{L}_{monoid} → \cat$.
\end{center}\end{propositionstar}
Intuitively, $\cal{L}_{monoid}$ serves as a \alert{definition} of monoids.

\end{slide}


\begin{slide}
\Title{Further example}
What should be the Lawvere theory $\cal{L}_{rings}$ for rings?
\begin{itemize}
\item Objects: one object, say $t$, and its formal finite powers $t × … × t$.
\item Morphisms $t × … × t → t$: terms generated by 
\begin{itemize}
\item \alert{binary $mult$ and $add$,}
\item \alert{constants $one$ and $zero$,}
\item in $n$ (ordered) variables,
\end{itemize}
up to a few \alert{equations.}
\item Morphisms $tⁿ → tᵖ$: $p$-tuples of terms.
\item Composition = simultaneous substitution.
\end{itemize}

\end{slide}

\begin{slide}
\Title{Lawvere theories: definition}
\begin{definitionstar}
\intro{Lawvere theory}: a category with
\begin{itemize}
\item finite products,
\item objects formally generated by a set of `sorts'.
\end{itemize}
\end{definitionstar}
E.g., $t × u × t$, for sorts $t$ and $u$.
\end{slide}


\begin{slide}
\Title{What has been gained (quick summary)}
\begin{itemize}
\item Signature + equations, i.e., theory $↦$ \alert{category of models}
\begin{center}
\diagram(
let m,ms = simple_math_matrix ~style:Matrix.([centers 30. 40.]) [[
    [];    <$\cal{L}_{theory}$> ];[
    <$\cat$> ; [] ; <$\catD$>
    ]]

let _ = sedges_matrix ms Edge.([
    ([labelal <<\size(2.7){model ₁}>>],(0,1),(1,0));
    ([labelar <<\size(2.7){model ₂}>>],(0,1),(1,2));
    ([labelb <<\size(2.7){functor preserving finite products}>>],(1,0),(1,2));
])
)
\end{center}
There are more general notions of morphisms…
\item A notion of morphism between Lawvere theories:
functors preserving finite-products; e.g.,
\begin{center}
$\cal{L}_{monoid} ↪ \cal{L}_{ring}$.
\end{center}
\end{itemize}
\end{slide}

\begin{slide}
\Title{What is missing?}

\begin{itemize}
\item Variable binding ($λx.x ≡ λx'.x'$).
\item Dynamics $(λx.M) N ↝ M [x ↦ N]$.
\end{itemize}
\begin{block}{}
Need to generalise Lawvere theories!
\end{block}

\end{slide}

== Generalising Lawvere theories == 

\begin{slide}
\Title{Variable binding}
We defined products by a \alert{property}.

\begin{itemize}
\item Consider any objects $A, B ∈ \cat$ with finite products;
\begin{states}([0])
\item $C × A \xto{ev} B$ is an \intro{exponential} of $A$ and $B$ iff ${∀} D ∈ \cat$,

\id{ }
\begin{center}
\diagram(
let m,ms = simple_math_matrix [[
    <$C × A$>;    <$B$> 
    ];[
    <$D × A$>
    ]]

let _ = sedges_matrix ms Edge.([
        ([labelbr <<${∀} f$>>],(1,0),(0,1)) ;
        ([labela <<$ev$>>],(0,0),(0,1)) ;
        ([dashed [2.];labell <<${∃} {!} h × id_A$>>],(1,0),(0,0)) ;
    ])
)
\end{center}
\end{states}
\begin{states}([1])
\item $Bᴬ × A \xto{ev} B$ is an \intro{exponential} of $A$ and $B$ iff ${∀} D ∈ \cat$,
\begin{center}
\diagram(
let m,ms = simple_math_matrix [[
    <$Bᴬ × A$>;    <$B$> 
    ];[
    <$D × A$>
    ]]

let _ = sedges_matrix ms Edge.([
        ([labelbr <<${∀} f$>>],(1,0),(0,1)) ;
        ([labela <<$ev$>>],(0,0),(0,1)) ;
        ([dashed [2.];labell <<${∃} {!} λf × id_A$>>],(1,0),(0,0)) ;
    ])
)
\end{center}
\end{states}
\item Notation: $C = Bᴬ$ and $h = λf$.
\item Intuition: $Bᴬ$ = function space, $λf$ = currying of $f$.
\end{itemize}

\end{slide}


\begin{slide}
\Title{Examples}
\begin{itemize}
\item $Set$: $Bᴬ$ = set of functions $A → B$.
\item $Gph$, graphs: some convoluted construction of rare use (to my knowledge). 
\item Not $Top$! Have to restrict to compactly generated spaces.
\item \intro{Scott domains}. Particular posets, important in denotational semantics.
\end{itemize}
\end{slide}

\begin{slide}
\Title{Cartesian closed categories = products + terminal object \alert{+ exponentials}}
\begin{definitionstar}
Cartesian closed category (CCC): \begin{itemize}
\item a product $(A × B, π, π')$ for all $A,B$,
\item a terminal object $1$,
\item an exponential $(Bᴬ,ev)$ for all $A,B$.
\end{itemize}
\end{definitionstar}

\end{slide}

\begin{slide}
\Title{Variable binding}
\begin{block}{Synopsis}
Models of theories with binding `are' cartesian closed categories.
\end{block}

\begin{examplestar}
The syntax for the pure $λ$-calculus yields a cartesian closed category $\cal{L}_{λ}$:
\begin{itemize}
\item objects are \alert{formal} powers and exponentials of $t$, e.g., $tᵗ × t$, $(t × t × t)^{t × tᵗ}$,…
\item morphisms are formally generated by\begin{itemize}
\item $lam : tᵗ → t$ and $app : t × t → t$,

\item stuff needed for $\cal{L}_λ$ to be a CCC.
\end{itemize}
\end{itemize}
\end{examplestar}
\begin{itemize}
\item Remark: $\cal{L}_λ$ contains more than the usual notion of syntax.
\item Morphisms = \alert{simply-typed} $λ$-terms up to $βη$-conversion.
\item E.g., $λx.M$ is here modelled as $lam (λ x : t. ⟦ M ⟧)$.
\end{itemize}
\end{slide}


\begin{slide}
\Title{Dynamics}
To model $$(λx.M) N ↝ M[x ↦ N]$$
we could add an equation
   $$app ⟨ lam (λ x : t. M), N⟩ = (λ x : t. M) N\textdot$$
We prefer adding a \intro{2-cell}:
\begin{center}
\diagram(
	let m,ms = simple_math_matrix ~style:Matrix.([centers 10. 30.]) [[
	[]; <$t × t$> ];[
	<$tᵗ × t$> ; [] ; <$t$> ]]

	let lam :: app :: res :: _ = sedges_matrix ms Edge.([
	([labelal <<$lam × idₜ$>>;bendLeft 10.],(1,0),(0,1));
	([labelar <<$app$>>;bendLeft 10.],(0,1),(1,2));
	([labelb <<$ev$>>;bendRight 20.],(1,0),(1,2));
	])

	let p = ms.(0).(1).Node.anchor `South
	let _ = Edge.(edge [double 0.5;arrow env;draw;labelr <<$β$>>] 
    		    	   (coordinate (Point.(p + (0.,-. 3.))))
    		    	   (coordinate (Point.(p + (0.,-. 10.))))
			   )

)
\end{center}
$↝$ \intro{Cartesian closed 2-categories}!
\end{slide}

\begin{slide}
\Title{Example reduction}

\begin{itemize}
\item In pure $λ$, if $M ↝ M'$ then $M N ↝ M' N$.
\item Here, assuming $α : M ⇒ N$, derive
\begin{center}
\diagram(
	let m,ms = simple_math_matrix ~style:Matrix.([centers 10. 30.]) [[
	<$Γ$> ; [] ; <$t × t$> ; <$t$> ]]

	let redex :: reactum :: app :: _ = sedges_matrix ms Edge.([
	([labela <<$⟨M,N⟩$>>;bendLeft 30.],(0,0),(0,2));
	([labelb <<$⟨M',N⟩$>>;bendRight 30.],(0,0),(0,2));
	([labela <<$app$>>],(0,2),(0,3));
	])

	let p = redex.Edge.anchor (`Temporal 0.5)
	let q = reactum.Edge.anchor (`Temporal 0.5)
	let _ = Edge.(edge [double 0.5;arrow env;draw;labelr <<$⟨α,id_N⟩$>>;shorten 3. 3.] 
	      		   (coordinate p) (coordinate q)
    		    	   (* (coordinate (Point.(p + (0.,-. 3.)))) *)
    		    	   (* (coordinate (Point.(p + (0.,-. 10.)))) *)
			   )

)
\end{center}

\end{itemize}
\begin{block}{Syntactically}
$app ⟨ α; id_N ⟩ : app ⟨ M; N ⟩ ⇒ app ⟨ M'; N ⟩$.
\end{block}

\end{slide}

\begin{slide}
\Title{Other example reduction}

\begin{itemize}
\item In pure $λ$, if $M ↝ M'$ then $λx.M ↝ λx.M'$.
\item Here, assuming 
\begin{center}
\diagram(
	let m,ms = simple_math_matrix ~style:Matrix.([centers 10. 30.]) [[
	<$Γ × t$> ; [] ; <$t$>]]

	let redex :: reactum :: _ = sedges_matrix ms Edge.([
	([labela <<$M$>>;bendLeft 30.],(0,0),(0,2));
	([labelb <<$M'$>>;bendRight 30.],(0,0),(0,2));
	])

	let p = redex.Edge.anchor (`Temporal 0.5)
	let q = reactum.Edge.anchor (`Temporal 0.5)
	let _ = Edge.(edge [double 0.5;arrow env;draw;labelr <<$α$>>;shorten 3. 3.] 
	      		   (coordinate p) (coordinate q)
    		    	   (* (coordinate (Point.(p + (0.,-. 3.)))) *)
    		    	   (* (coordinate (Point.(p + (0.,-. 10.)))) *)
			   )

)
\end{center}
derive
\begin{center}
\diagram(
	let m,ms = simple_math_matrix ~style:Matrix.([centers 10. 30.]) [[
	<$Γ$> ; [] ; <$tᵗ$> ; <$t$> ]]

	let redex :: reactum :: app :: _ = sedges_matrix ms Edge.([
	([labela <<$λx:t.M$>>;bendLeft 30.],(0,0),(0,2));
	([labelb <<$λx:t.M'$>>;bendRight 30.],(0,0),(0,2));
	([labela <<$lam$>>],(0,2),(0,3));
	])

	let p = redex.Edge.anchor (`Temporal 0.5)
	let q = reactum.Edge.anchor (`Temporal 0.5)
	let _ = Edge.(edge [double 0.5;arrow env;draw;labelr <<$λx : t.α$>>;shorten 3. 3.] 
	      		   (coordinate p) (coordinate q)
    		    	   (* (coordinate (Point.(p + (0.,-. 3.)))) *)
    		    	   (* (coordinate (Point.(p + (0.,-. 10.)))) *)
			   )

)
\end{center}
\end{itemize}
\begin{block}{Syntactically}
$λx:t.α : lam(λx:t.M) ⇒ lam(λx:t.M')$.
\end{block}
\end{slide}

\begin{slide}

\begin{propositionstar}
\begin{center}
2-cells $M ⇒ N$ 

$≅$ 

reductions up to \alert{permutation equivalence}() (Lévy, late 70's; Bruggink, 2003).
\end{center}
\end{propositionstar}
\end{slide}

==Perspectives==

\begin{slide}
\Title{Possible perspectives}
\begin{itemize}
\item More involved examples.
\item Dynamic properties of 2CCCs (following Hilken).
\item Dynamic properties of morphisms.
\item Formal links with other approaches.
\item Extensions, e.g., dependent types. 
\item Coq library?
\end{itemize}
\end{slide}