#import "template/lib.typ": *
#import "template/math.typ": *
#import "@preview/fletcher:0.5.8" as fletcher: diagram, node, edge
#import "@preview/curryst:0.6.0": rule, prooftree
#import "@preview/pinit:0.2.2": *

#let scheme = dark
#let edge = edge.with(stroke: scheme.fg, crossing-fill: scheme.bg)
#let prooftree = prooftree.with(stroke: stroke(thickness: 0.05em, paint: scheme.fg))

#show: paper.with(scheme: scheme, title: "SEMPL", subtitle: "Lesson 1")

#let environment = environment.with(scheme: scheme)
#let environment_ = environment_.with(scheme: scheme)
#let theorem = environment.with(name: "Theorem")
#let proposition = environment.with(name: "Proposition")
#let definition = environment.with(name: "Definition")
#let remark = environment.with(name: "Remark", counter: none)
#let exercise = environment.with(name: "Exercise")
#let proof = environment_.with(name: "Proof of", follows: true)
#let solution = environment_.with(name: "Solution of", follows: true)
#let example = environment_.with(name: "Example")
#let notation = environment_.with(name: "Notation", counter: none)

`guillaume.geoffroy@irif.fr`

#outline()

= (Some) Universal algrebra with binders

E.g. monoid = "Structure" over signature $(⋅, 1)$ satisfying some equations

Idea :
- Model of the $lambda$-calculus
- Structure over signature $("Lambda", "App")$ satisfying
  $
    &beta : "App"("Lambda"(x . t), u) = t[x := u]\
    &eta : "Lambda"(x . "App"(t, x)) = t
  $

== Algrebraic syntax with binders

For a formal and abstract presentation
- #link("https://lics.siglog.org/archive/1999/GabbayPitts-ANewApproachtoAbstr.html")[Gabbay & Pitts (LICS 1999)]
- #link("https://lics.siglog.org/1999/FiorePlotkinTuri-AbstractSyntaxandVa.html")[Fiore, Plotkin & Tury (LICS 1999)]

An algebraic signature with binders is a pair $Sigma = ("Op"_Sigma, "Ar"_Sigma)$ with
- $"Op"_Sigma$ is a set (operations)
- $"Ar"_Sigma$ is $in "Op"_Sigma --> "List"(NN)$ (arity)

#example[
  $
    Sigma_1 = ({"Lam", "App"}, cases("Lam" mapsto (1), "App" mapsto (0, 0))})
  $
]

#definition[
  Let $Sigma$ be an algebraic signature.

  The set of terms over $Lambda$ is defined by the following grammar, modulo
  $alpha$-renaming.

  $
    t := &x " (variable)"\
         &alpha((x_(1, 1), ..., x_(1, n_1))⋅t_1, ..., (x_(k, 1), ..., x_(k, n_k))⋅t_k)\
         &"Where " alpha in "Op"_Sigma " and " (n_1, ..., n_k) = "Ar"_Sigma (alpha)
         &"and " forall i, x_(i, 1), ..., x_(i, n_i) " are pairwise " eq.not
  $
]

#example[
  $"Term"(Sigma_Lambda)$ is the set of pure $lambda$-terms (modulo $alpha$)
]

#exercise[
  Find a construction in an actual programming language that has arity $(1, 2)$.

]
#solution[
  ```
  function [] -> e
           | h::t -> f      -> (0, 2)
  function Leaf(x) -> e
           | Node(l, r) -> f
  ```
]

#notation[
  Let $Sigma$ be a signature, $x_1, ..., x_n$ pairwise $eq.not$ variables and
  t, u_1, ..., u_n terms over $Lambda$.

  We write $t[x_1 := u_1, ..., x_n := u_1]$ for the simultaneous capture-avoiding
  (#sym.arrow.l.r.double compatible with $eq.not$) substitution of each free
  occurrence of $x_i$ with $u_i$.
]

#let Lam = $"Lam"$
#let App = $"App"$
#let Op = $"Op"$
#let Ar = $"Ar"$
#let Type = $"Type"$
#let Rule = $"Rule"$

#exercise[
  - $(Lam(x ⋅ App(x, y)))[x := a, y := b] = Lam(x ⋅ App(x, b))$
  - $(App(x, y))[x := y, y := x] = App(y, x)$
  - $(Lam(x ⋅ App(y, x)))[y := x] = Lam(z ⋅ App(x, z))$
]

#exercise[
  $Sigma$ signature, $t$, $u$, $v$ terms, $x$, $y$ variables.

  If $y$ not free in $t$, prove $t[x := u[y := v]] = t[x := u][y := v]$
]

#solution[
  $
    y[x := u[y := z]] := y\
    y[x := u][y := z] := z
  $
]

#proposition[
  Let $Sigma$ signature, $t, u_1, ..., u_n, v_1, ..., v_n$ terms over $Sigma$
  $x_1, ..., x_n, y_1, ..., y_n$ variables. If no $y_i$ is free in $t$ then

  $t[x_1 := u_1[overline(y) := overline(v)], ..., x_n := u_m [overline(y) := overline(v)]]
  = t[overline(x) := overline(u)][overline(y) := overline(v)]$
]

#remark[
  Also true if the list $overline(x)$ contains all of the free variables of $t$,
  regardless of whether any $y_i$ is free in $t$.
]

#definition[
  Given a signature $Sigma$, a simple type system over $Sigma$ is a pair
  $tau = ("Type"_tau, "Rule"_tau)$ where :
  - $"Type"_tau$ is a set
  - $"Rule"_tau in product_cases(delim: #none, alpha in "Op"_Sigma, (n_1, ..., n_k)=Ar_Sigma(alpha))$
]

Intuitively :
#prooftree(
  rule(
    $Gamma, x_(1, 1) : A_(1, 1), ..., x_(1, n_1) : A_(1, n_1) tack t_1 : B_1$,
    $...$,
    $Gamma, x_(k, 1) : A_(k, 1), ..., x_(k, n_k) : A_(k, n_k) tack t_k : B_k$,
    $Gamma tack alpha((overline(x_1))⋅t_1, ..., (overline(x_k))⋅t_k) : C$
  ),
)
$
  <=> Rule_tau (alpha) = (overline(A_1), B_1, ..., overline(A_k), B_k, C)
$

#example[
  Let $Type_tau_(S T)$ be generated by
  $
    A, b ::= &a | b | ... " (atomic types)"\
             | &A -> B
  $
  $
    Sigma_S T = (union_(A, B) {Lam_(A, B), App_(A, B)}, cases(Lam_(A, B) mapsto (1), App_(A, B) mapsto (0, 0))})
  $

  $Rule_tau_(S T) (App_(A, B)) = (A -> B, A, B)$
  #prooftree(
    rule(
      $Gamma tack t : A -> B$,
      $Gamma tack u : B$,
      $Gamma tack App_(A, B)(t, u) : B$
    ),
  )

  $Rule_tau_(S T) (Lam_(A, B)) = (A, B, A -> B)$
  #prooftree(
    rule(
      $Gamma tack t : A$,
      $Gamma tack u : B$,
      $Gamma tack Lam(A, B)(x⋅t) : A -> B$
    ),
  )
]

#definition[
  Let $Sigma, tau$ be a simply typed algebraic signature (STAS).
  - A context is a tuple $((x_1 : A_1), ..., (x_n : A_n))$ (written $x_1 : A_1, ..., x_n : A_n$) when the $x_i$ are
    pairwise $eq.not$ variables and the $A_i$ are types.
  - The context $Gamma = x_i : A_i, ..., x_n : A_n$ binds the variables $x_1, ..., x_n : B_k$
  - A context $Gamma$ _closes_ a term $t$ if it binds all its free variables
  - A _term with context_ is a pair $(Gamma, t)$ (written $Gamma tack t$) where
    $t$ is a term and $Gamma$ is a context that closes $t$.
  - A _typing judgement_ is a triple $(Gamma, t, B)$ (written $Gamma tack t : B$)
    where $Gamma tack t$ is a term with context and $B$ is a type.
]

#let ol = overline

#definition[
  Let $(Sigma, tau)$ be a STAS. The set of (intuistionistically) valid judgements
  for $(Sigma, tau)$ is the least set of typing judgements s.t :
  - $forall x, A quad x : A tack x : A$ is valid
  - $forall alpha in Op_Sigma$ with $(n_1, ..., n_k) = Ar_Sigma(alpha)$ and
    $(overline(A_1), B_1, ..., overline(A_k), ..., B_k, C) = Rule_Sigma (alpha)$
    $
      forall Gamma, overline(x_1) : overline(A_1) tack t_1, B_1, ..., Gamma, ol(x_k) : ol(A_k) tack t_k : B_k "valid"\
      forall Gamma tack alpha((ol(x_1))⋅t_1, ..., (ol(x_k))⋅t_k) : C "is valid"
    $
  - permutation
    $ &forall m in NN quad forall sigma : {1, ..., m} --> {1, ..., m} "bijection"\
      &forall A_1, ..., A_m "types"\
      &forall x_1 : A_(sigma(1)), ..., x_m : A_(sigma(m)) tack t : B "valid"\
      &forall y_1, ..., y_m "pairwise" eq.not "variables"
      y_1 : A_1, ..., y_m : A_m tack t[x_1 := y_(sigma(1)), ..., x_m := y_(sigma(m))] : B "is valid"
    $
  - contraction
    $ &forall m in NN quad forall sigma : {1, ..., m} --> {1, ..., n}\
      &forall A_1, ..., A_n "types"\
      &forall x_1 : A_(sigma(1)), ..., x_m : A_(sigma(m)) tack t : B "valid"\
      &forall y_1, ..., y_n "pairwise" eq.not "variables"
      y_1 : A_1, ..., y_n : A_n tack t[x_1 := y_(sigma(1)), ..., x_m := y_(sigma(m))] : B "is valid"
    $
]

#exercise[
  State the cut rule
]

== Cartesian models

Intuition :
$
  A &~> [[A]] "Set with structure"\
  t: A &~> [[t : A]] in [[A]]
$

2 paths :
- « Objects = Types, Morphims = Terms »
  $
    "(valid)" x_1 : A_1, ..., x_n : A_n tack t : B ~> [[Gamma tack t : B]] in space ??? [[A_1]], ..., [[A_n]]; [[B]] eq.not cal(C)([[A]], [[B]])
  $
- « Objects = Contexts = Lists of types, Morphisms = Substitutions = Lists of terms »
  $
    "(valid)" underbrace(underbrace(x_1 : A_1\, ...\, x_n : A_n, Gamma) tack t_1 : B_B ... Gamma tack t_n : B_n, Gamma : overline(A) tack Delta : overline(B))
     ~> cases(
          delim: "|",
          overline(A) |-> [|overline(A)|],
          Gamma : overline(A) |- Delta : overline(B) |->
          [|Gamma |- Delta|] in ???_[|overline(A), overline(B)|]
        )
  $

#let List = "List"

#let lA = $overline(A)$
#let lB = $overline(B)$
#let lC = $overline(C)$
#let lD = $overline(D)$
#let lx = $overline(x)$
#let ly = $overline(y)$
#let lz = $overline(z)$
#let cC = $cal(C)$
#let lC = $overline(cC)$
#let lt = $overline(t)$
#let lu = $overline(u)$
#let lv = $overline(v)$
#let pair(r, l) = $chevron.l #r, #l chevron.r$
#let Types = $"Types"$

#exercise[
  Let $(Sigma, tau)$ be a simply typed algebraic signature.\

  - For all $overline(A), overline(B)$ list of types, let $cal(C)(overline(A), overline(B))$ be a set.\

  - For all $Gamma : overline(A) |- Delta : overline(B)$ valid,
    let $[|Gamma |- Delta|] in cal(C)(overline(A), overline(B))$

  - For all $overline(A), overline(B), overline(C)$ and all
    $b in cal(C)(overline(A), overline(B)),
    c in cal(C)(overline(B), overline(C))$,
    let $c[b] in cal(C)(overline(A), overline(C))$
  Assume that
  - $
      &forall overline(A), overline(B), overline(C),\
      &forall
      Gamma_1 : overline(A) |- Delta_1 : overline(B) "and" Gamma_2 : overline(B) |- Delta_2 : overline(C) "valid",\
      &[|Gamma_1 |- Delta_1|][[|Gamma_2 |- Delta_2|]] = [|Gamma_1 |- Delta_1[Gamma_2 |- Delta_2]|]
    $
  - $forall overline(A) overline(B), [| - |]_(overline(A), overline(B))$ is surjective
  - $
      forall "types" lA, B_1, ..., B_n\
      forall "valid judgements"\
      cases(delim: "(",
        lz : lA tack t_1 : B_1,
        lz : lA tack t_n : B_n
      )\
      cases(delim: "(",
        lz : lA tack u_1 : B_1,
        lz : lA tack u_n : B_n
      )
    $
  - $[| lz |- alpha(lx_1 ⋅ t_1, ..., lx_n ⋅ t_n) |]$ depends only on $[| |- t_1 |], ..., [| |- t_n |]$
  Prove that:
  - $(List(Type), cal(C))$ defines a category with all finite products
  - It is cartesian
  - each $alpha in Op_Sigma$ is interpreted by a natural transformation (natural wrt the context)
]

#environment(name: "Erratum", counter: none)[
  Terms in context are defined up to renaming :
  $
    x: A, y: B &tack t\
    x': A, y': B &tack t[x := x', y := y']
  $
]

#solution[
  $"Id"$ morphism : $A_1, ..., A_n = overline(A)$
  $
    id_overline(A) = [[ overline(x) : overline(A) tack x_1 : A_1 ]], ..., [[ overline(x) : overline(A) tack x_n : A_n ]]
  $

  Composition : $overline(A), overline(B), overline(C)$
  $
    b in cal(C)(overline(A), overline(B)) quad c in cal(C)(overline(B), overline(C))\
    c compose b = ? quad c[b]
  $

  Associativity : $overline(A), overline(B), overline(C), overline(D)$
  $
    b in cal(C)(overline(A), overline(B)) quad c in cal(C)(overline(B), overline(C)) quad d in cal(C)(overline(C), overline(D))\
    "surjective : " b = [[overline(x) tack overline(t)]] quad c = [[overline(y) tack overline(u)]] quad d = [[overline(z) tack overline(v)]]\
    d compose (c compose b) &= d[c[b]] \
        &= [|overline(z) |- overline(v)|][[|overline(y) |- overline(u)|][[|overline(x) |- overline(t)|]]] \
        &= [|overline(z) |- overline(v)|][[|overline(x) |- overline(u)[overline(y) := overline(t)]|]] \
        &= [|overline(x) |- overline(v)[overline(z) := overline(u)[overline(y) := overline(t)]]|] \
        &= [|overline(x) |- overline(v)[overline(z) := overline(u)][overline(y) := overline(t)]|] \
        &= d[c][b] quad #[by unrolling in the other way]\
        &= (d compose c) compose b
  $

  Unit : $overline(A), overline(B) quad b = [|overline(x) tack overline(t) in cal(C)(overline(A), overline(B))|]$
  $
    id_overline(B) &= [| overline(y) tack overline(y) |]\
    id_overline(B) compose b &= [| overline(y) tack overline(y) |] compose [| overline(x) tack overline(t) |]\
                             &= [| overline(x) tack overline(y)[ overline(y) := overline(t) ]|]
                             &= [| overline(x) tack overline(t) |]
                             &= b
    id_overline(A) &= [| overline(x') tack overline(x') |]\
    b compose id_overline(A) &= [| overline(x) tack overline(t) |] compose [| overline(x') tack overline(x') |]\
                             &= [| overline(x') tack overline(t)[ overline(x) := overline(x') ]|]
                             &= [| overline(x) tack overline(t) |]
                             &= b
  $


  It is cartesian
  - Terminal object : $[]$
  - Product of $lA, lB$:
    $
      lA times lB & := [lA, lB] && quad ("concatenation") \
      pi_lA & := [|lx : lA, ly : lB |- lx : lA|] \
      pi_lB & := [|lx : lA, ly : lB |- ly : lB|] \
    $
    For $f := [|lz |- lt|] in cC(lC, lA), g := [|lz |- lu|] in cC(lC, lA)$,
    $
      pair(f, g) := [|z |- lt, lu|] quad (= [| [lz |- t_1, ..., lz |- t_m, lz |- u_1, ..., lz |- u_n] |])
    $
    Uniqueness:
    Let $h = [|lz |- lv : lA, lB|] in cC(lC, [lA, lB])$.
    $
      lv &= [lv_lA, lv_lB] \
      f &= pi_A compose h = [|lx, ly |- lx|] compose [|lz |- lv_lA, lv_lB|] \
      &= [|lz |- lx[lx := lv_lA, ly := lv_lB]|] \
      &= [|lz |- lv_lA|] \
      g &= [|lz |- lv_lB|]
    $
    $h = pair(f, g)$ now follows from (3)

  Prove that for all $alpha in Op_Sigma$ where $Rule(alpha) = (lA_1, B_1..., lA_n, B_n, C)$
  the map $lD in List(Types) t-> cases(delim: "(",
    b_1 = [| lz, lx_1 in cC((lD, lA_1), B_1) |],
    ...,
    b_n = [| lz, lx_n in cC((lD, lA_n), B_n) |],
  ) t-> [| lz |- alpha(lx_1 ⋅ t_1, ..., lx_n ⋅ t_n) |]$ is a natural transformation (wrt $lD$).

  $
    cC((-, lA_1), B_1) times ... times cC((-, lA_n), B_n) => cC(-, C)
  $

  $
    underbrace([| ly : lE |- lu : lD |], d) in cC(lE, lD)\

    [| ly |- alpha(lx_1 ⋅ t_1[lz := lu], ..., lx_n ⋅ t_n[lz := lu]) |]
    = [| lz |- alpha(lx_1 ⋅ t_1, ..., lx_n ⋅ t_n) |] compose [| ly |- lu |]
  $
]

#show "STAS": "Simply Typed Algebraic Signature (STAS)"

#let Ob = $"Ob"$
#let Set = $"Set"$

#definition[
  Let $(Sigma, tau)$ be a STAS.
  A structure on $(Sigma, tau)$ is :
  - A locally small#footnote[$forall A, B, cC(A, B) "is a set"$] cartesian category $cC$. Notation :
    - $(A times B, pi_1 "or" pi_A, pi_2 "or" pi_B)$ product
    - $pair(f, g) in cC(C, A times B)$ universal map
    - $T$ terminal object
    - $T_A in cC(A, T)$
  - A function $[| ... |] : Types --> Ob(cC)$
  - $forall alpha in Op_Sigma$ with $Rule(alpha) = (lA_1, B_1, ..., lA_n, B_n, C)$
    a natural transformation (wrt $D$)
    $[| alpha |] : D in Ob(cC) t-> [| alpha |]_D in Set(cC(D times [| lA_1 |], [[B_1]]) times ... times cC(D times [| lA_n |], [[B_n]]), cC(D, [|C|]))$ ($[|A_1|]$ meaning $[|A_(1, 1)|] times ... times [|A_(1, m_1)|]$)
]

#example[
  $AA$ set of atomic types $~> Lambda_("ST", AA) = (Sigma_(Lambda_("ST", AA)), tau_(Lambda_("ST", AA)))$.
  $cC = Set$. $forall a in AA "choose" [|a|] "set"$. Let $[| A --> B |] = cC([|A|], [|B|])$.

  $
    [|Lam_(A, B)|]_D = f t-> (x t-> y t-> f(x, y)) in Set(cC(D times [|A|], [|B|]), cC(D, cC([|A|], [|B|])))
  $
]

#exercise[
  Given $Gamma : lA |- lt : lB$ valid typing judgements.

  Define $[| Gamma : lA |- lt : lB |] in tau([|lA|], [|lB|])$.

  Such that $[| Gamma_1 |- Delta_2[Gamma_2 := Delta_1] |] = [| Gamma_2 |- Delta_2 |] compose [| Gamma_1 |- Delta_1 |] in cC(D, A) => cC(D, B)$

  $cC(A, B)$
]

== Models of the Simply-Typed $lambda$-Calculus

#let ST = "ST"
#let app = "app"
#let lam = "lam"

Interpret $Lambda_(ST, AA)$ so that
$beta : [| lz : D |- app_(A, B)(lam_(A, B)(x⋅t), u) : B |] = [| z |- t[x := u] |]$
and $eta : [| lz : D |- lam_(A, B)(x ⋅ app_(A, B)(t, x)) : A -> B |] = [| lz : D |- t : A -> B |]$

Equivalently, so that $t =_(beta, eta) u => [| Gamma |- t |] = [| Gamma |- u |]$.

Take $cC$ locally small category.

Let $A -> B in Ob(cC), forall A, B in Ob(cC)$.

Let $cC(D times A, B) <--_(lam_(A, B, D)) cC(D, A -> B)$,
$cC(D, A -> B) times cC(D, A), -->_(app_(A, B, D)) cC(D, B)$ be a natural
transformation wrt D.

Assume that $forall t in cC(D times A, B), forall u in cC(D, u)$.

$beta : app(lam(t), u) = t compose pair(id_D, u)$

$eta : forall t e cC(D, A -> B)$

$t = lam(app(t compose pi_D, pi_A))$

Then $cC$ is cartesian closed (and this is equivalent).

#exercise[
  Given $Gamma : lA |- lt : lB$ valid typing judgements.

  Define $[| Gamma : lA |- lt : lB |] in tau([|lA|], [|lB|])$.
]

In Ocaml, is it true that $("fun" x -> t) u eq.triple t[x := u]$ ?
- find a sufficient condition on $f$ : if $f$ "uses $x$ exactly once"
- find a sufficient condition on $e$ : if $e$ has no side-effects

Attention : Non-commutative side-effects

== Interlude : Yoneda's Lemma

#let Cat = $cal("C")"at"$

#definition[
  Let $cC$, $cD$ be locally small categories.
  The category of functions $Cat(cC, cD)$ defined by:
]

#proposition[
  Let $cC$ be a locally small category.
  Then $Cat(cC^"op", Set)$ is a Grothendieck topos, in particular:
  - It has all small limits and colimits
  - It is cartesian closed
]

#let yo = $よ$

#definition(subtitle: "The Yoneda embedding")[
  Let $cC$ a locally small category, we define a functor:
  $
    よ : cC --> Cat(cC^op, Set)
  $

  - On objects : $forall A in Ob(cC)$, $yo(A) : cC^"op" --> Set$ is defined by :
    - $forall B in Ob(cC), yo(A)(B) = cC(B, A)$
    - $forall f in cC(B_2, B_1), yo(A)(f) = cases(cC(B_1, A) &--> cC(B_2, A), g &t--> g compose f)$
    $
      yo(A)(f_1)(y(A)(f_2)(g)) &= (g compose f_2) compose f_1\
                               &= g compose (f_2 compose f_1)\
                               &= yo(A) (f_2 compose f_1) (g)
    $
  - On morphisms : $forall h in cC(A_1, A_2), yo(h) : yo(A_1) => y(A_2)$ is defined by :
    $
      forall B in Ob(cC), yo(h)(B) = cases(underbrace(yo(A_1)(B), cC(B, A_1)) &-->^(Set) underbrace(yo(A_2)(B), cC(B, A_2)),
                                           g &t--> h compose g)
    $
]

#exercise[
  Prove that $forall h, yo(h)$ is natural : $forall f in cC^(B_1, B_2) = cC(B_2, B_1)$
  #align(center, diagram({
  	node((-1, -1), [$cC(B_1, A_1)$])
  	node((-1, 1), [$cC(B_1, A_2)$])
  	node((3, -1), [$cC(B_2, A_1)$])
  	node((3, 1), [$cC(B_2, A_2)$])
  	edge((-1, -1), (-1, 1), [$h compose -$], label-side: right, "->")
  	edge((-1, -1), (-1, 1), [$yo(h)(B_1)$], label-side: left, " ")
  	edge((-1, -1), (3, -1), [$- compose f$], label-side: left, "->")
  	edge((3, -1), (3, 1), [$h compose -$], label-side: left, "->")
  	edge((3, -1), (3, 1), [$yo(h)(B_2)$], label-side: right, " ")
  	edge((-1, 1), (3, 1), [$- compose f$], label-side: right, "->")
  	edge((-1, 1), (3, 1), [$yo(A_2)(f)$], label-side: left, "->")
  	edge((-1, -1), (3, -1), [$yo(A_1)(f)$], label-side: right, " ")
  }))
]

#theorem(subtitle: "Yoneda")[
  For all $F in Cat(cC^"op", Set)$, the natural transformation :
  $
    cases(
      Cat(cC^"op", Set)(yo(-), F) &==> F(-),
      underbrace(A, in Ob(cC)) t-> underbrace(alpha, in yo(A) => F = Cat(cC^"op", Set)(yo(A), F)) &t--> underbrace(underbrace(alpha_A, in Set(yo(A)(A), F(A)))(underbrace(id_A, in cC(A, A) = yo(A)(A))), in F(A)),
    )
  $

  is a bijection.
]

#exercise[
  - Prove naturality
  - Prove Yoneda (i.e. bijection)
  - Prove that $yo : cC --> Cat(cC^"op", Set)$ which is full & faithful (Apply
    yoneda to $F = yo(B)$)
  - Prove that $yo$ is continuous (= preserves all small limits that exists in $cC$)
]

= Models of linear logic

== Nomenclature the various fragments of linear logic

$
  #pin(1)&(times) quad &-o quad &1 quad &    quad &par quad &bot quad &"multiplicative"\
  &(+)     quad &\& quad &0 quad &top quad &    quad &&"additive"\
  &!       quad &   quad &  quad &    #pin(2) quad &    quad &&"exponential"\
$
$
  "intuitionistic fragment"
$

// #pinit-highlight(1, 2)

- MALL : $(times) (+) \& par 1 space 0 space top bot -o$
- ILL : $(times) (+) \& space 1 space 0 space top -o !$
- MEILL : $(times) (+) \& par 1 space 0 space top bot -o ! space ?$

== Standard notions of models for fragments of MALL

$(times) 1$ : Symmetric monoidal category
- adding $-o$ : Symmetrict monoidal closed category
  - adding $par bot$ : \*-autonomous
- adding $& top$ : Finite products
- adding $(+) 0$ : Finite coproducts

#definition[
  Let $cC$ be a category and $A, B in Ob(cC)$.

  A coproduct of A and B is:
  - An object $A (+) B$
  - Two morphisms $i_A in cC(A, A (+) B), i_B in cC(B, A(+) B)$
    such that $forall C in Ob(cC), forall f in cC(A, C), forall g in cC(B, C)$

    $exists ! [f, g] in cC(A (+) B, C)$ such that
    #align(center, diagram({
    	node((-1, -1), [$A (+) B$])
    	node((0, -1), [$B$])
    	node((-2, -1), [$A$])
    	node((-1, 0), [$C$])
    	edge((0, -1), (-1, -1), [$iota_B$], label-side: right, "->")
    	edge((-2, -1), (-1, -1), [$iota_A$], label-side: left, "->")
    	edge((-1, -1), (-1, 0), [$[f, g]$], label-side: right, "->")
    	edge((0, -1), (-1, 0), [$g$], label-side: left, "->", bend: 18deg)
    	edge((-2, -1), (-1, 0), [$f$], label-side: right, "->", bend: -18deg)
    }))
]

#let FinBan = $"FinBan"$

#example[
  Let $FinBan$ (finite Banard) be the category defined by :
  - $Ob(FinBan)$ : All finite-dimensional normed ($RR$-)vector spaces 
  - $FinBan(A, B)$ =
    ${ &f : A --> B "linear"\ &"s.t." forall ||f(a)|| <= ||a|| }$ 
  - $FinBan(A_1, ..., A_n, B)$ =
    ${ &f : A_1 times ... times A_n --> B space n"-linear (linear wrt each variable)"\ &"s.t." forall ||f(a_1, ..., a_n)|| <= ||a_1|| ... ||a_n|| }$ 
  - $top = 0 = { 0 }$
  - $A & B = A times B space (= A + B)$, $||(a, b)|| = max(||a||, ||b||)$\
    Exercise : Prove that product\
    $||pi_A(a, b)||  = ||a|| <= max(||a||, ||b||)$\
    $||pi_B(a, b)||  = ||b|| <= max(||a||, ||b||)$

    Let $f in FinBan(C, A)$, $g in FinBan(C, B)$.

    $<f, g>$ must be defined by $<f, g>(c) = (f(c), g(c))$

    let $c in C$, $underbrace(||f(c)|| <= c quad ||g(c)|| <= c, ||(f(c), g(c))|| <= c)$

  - $A (+) B = A + B space (= A times B)$\
    $||inj_A(a, b)||  = ||(a, 0)|| "and" ||(a, 0)||, ||a||$\
    $||inj_B(a, b)||  = ||(0, b)|| "and" ||(0, b)||, ||b||$

    Let $f in FinBan(A, C)$, $g in FinBan(B, C)$.

    $exists ! h : A (+) B --> C$ linear s.t $h compose inj_1 = f$ ($h(a, 0) = f(a)$) and $h compose inj_2 = g$ ($f(0, b) = g(b)$)

    So, $h(a, b) = h((a, 0) + (0, b)) = f(a) + g(b)$.

    $||h(a, b)|| = ||f(a) + g(b)|| <= ||f(a)|| + ||g(b)|| <= ||a|| + ||b||$
  - $A -o B$ = Linear maps $A -> B$
    $||f|| = sup_"max" {||f(a)||, ||a|| <= 1}$
  - $bot = 1 = (RR, |.|)$

    $
      1 -o B &arrow.r.double^~ B\
      underbrace(f, ||f|| = ||f(1)|| = ||f(-1)||) &t-> f(1) quad quad (|r| <= 1)
    $

    $((a -o bot) -o bot) tilde.eq A$
  - $(A (*) B, (a, b) t-> a (*) b)$ is characterised by the following universal property.
    #align(center, diagram({
    	node((-2, -1), [$(A, B)$])
    	node((0, -1), [$FinBan(A, B\; C)$])
    	node((-1, -1), [$C$])
    	node((-2, 0), [$A (times) B$])
    	node((-2, 1), [$FinBan(A, B\; A (times) B)$])
    	edge((-2, 0), (-1, -1), [$exists !$], label-side: right, "-->")
    	edge((-2, -1), (-1, -1), [$forall$], label-side: left, "->")
    	edge((-2, -1), (-2, 0), [$(a, b) t-> a (times) b$], label-side: right, "->")
    	edge((-2, 1), (-2, 0), [$in$], label-side: center, " ")
    	edge((-1, -1), (0, -1), [$in$], label-side: center, " ")
    	edge((-2, -1), (-2, -1), "->", bend: 140deg, loop-angle: 135deg)
    }))
]

#exercise[
  Find a symmetrical monoidal category $(cC, (*), 1)$
  s.t. $cC$ has finite coproducts but $(*)$ does not distribute over them.
  i.e., in general :
  - $A (*) (B (+) C) tilde.eq.not (A (*) B) (+) (B (*) C)$
  - $A (*) 0 tilde.eq.not 0$
]

#solution[
  $cC = FinBan$

  $(*) = \&$

  $I = top$

  $(1 (+) 1) \& 1 tilde.eq.not (1 \& 1) (+) (1 \& 1)$
]

== Interpreting $!$ Linean/Non-Linear adjunctions

#definition[
  Let $(cC, ⋅, I) space (cD, (x), 1)$ be symmetric monoidal categories.

  A _symmetric lax monoidal functor_ from $cC$ to $cD$ is a functor
  $F : cC --> cD$ equipped with :
  - A natural transformation (wrt $A, B$) :
    $m^2_(A, B) in cD(F A (*) F B, F (A ⋅ B)), forall A, B in Ob(cC)$
  - A morphism $m^0 in cD(1, F I)$

  Such that :
  1.
    #align(center, diagram({
    	node((0, 0), [$(F A (*) F B) (*) F C$])
    	node((1, 0), [$F A (*) (F B (*) F C)$])
    	node((0, 1), [$F(A⋅B) (*) F C$])
    	node((0, 2), [$F((A⋅B)⋅C)$])
    	node((1, 1), [$F A (*) F (B ⋅ C)$])
    	node((1, 2), [$F (A ⋅ (B ⋅ C))$])
    	edge((0, 0), (1, 0), [$"assoc"^cD$], label-side: left, "->")
    	edge((0, 2), (1, 2), [$"assoc"^cD$], label-side: left, "->")
    	edge((0, 0), (0, 1), [$m^2_(A, B) (*) F C$], label-side: right, "->")
    	edge((0, 1), (0, 2), [$m^2_(A⋅B, C)$], label-side: right, "->")
    	edge((1, 0), (1, 1), [$F A (*) m^2_(B, C)$], label-side: left, "->")
    	edge((1, 1), (1, 2), [$m^2_(A, B⋅C)$], label-side: left, "->")
    }))
  2.
    // https://q.uiver.app/#r=typst&q=WzAsNCxbMCwwLCJGIEEgKCopIDEiXSxbMSwwLCJGIEEiXSxbMCwxLCJGIEEgKCopIEYgSSJdLFsxLDEsIkYgKEEg4ouF4oCvSSkiXSxbMCwxLCJcInVuaXRcIl5jRCJdLFswLDIsImlkXyhGIEEpICgqKSBtXjAiLDJdLFszLDEsIkYgKFwidW5pdFwiXmNDKSIsMl0sWzIsMywibV4yIiwyXV0=
    #align(center, diagram({
    	node((-2, -2), [$F A (*) 1$])
    	node((-1, -2), [$F A$])
    	node((-2, -1), [$F A (*) F I$])
    	node((-1, -1), [$F (A ⋅ I)$])
    	edge((-2, -2), (-1, -2), [$"unit"^cD$], label-side: left, "->")
    	edge((-2, -2), (-2, -1), [$id_(F A) (*) m^0$], label-side: right, "->")
    	edge((-1, -1), (-1, -2), [$F ("unit"^cC)$], label-side: right, "->")
    	edge((-2, -1), (-1, -1), [$m^2$], label-side: right, "->")
    }))
  3.
    // https://q.uiver.app/#r=typst&q=WzAsNCxbMCwwLCJGIEEgKCopIEYgQiJdLFsxLDAsIkYgQiAoKikgRiBBIl0sWzAsMSwiRiAoQSDii4UgQikiXSxbMSwxLCJGIChCIOKLhSBBKSJdLFswLDIsIm1fMiJdLFsxLDMsIm1eMiJdLFswLDEsIlwiU3dhcFwiXmNEIiwxXSxbMiwzLCJGIChcIlN3YXBcIl5jQykiLDFdXQ==
    #align(center, diagram({
    	node((-2, -1), [$F A (*) F B$])
    	node((-1, -1), [$F B (*) F A$])
    	node((-2, 0), [$F (A ⋅ B)$])
    	node((-1, 0), [$F (B ⋅ A)$])
    	edge((-2, -1), (-2, 0), [$m^2$], label-side: right, "->")
    	edge((-1, -1), (-1, 0), [$m^2$], label-side: left, "->")
    	edge((-2, -1), (-1, -1), [$"Swap"^cD$], label-side: center, "->")
    	edge((-2, 0), (-1, 0), [$F ("Swap"^cC)$], label-side: center, "->")
    }))

  A _strong monoidal functor_ is a lax monoidal functor (F, m) s.t. $m^2$ and
  $m^0$ are isomophisms.
]

#definition[
  A _symmetric monoidal adjunction_ :
  #align(center, diagram({
  	node((-1, 0), [$(cal(C), dot, I)$])
  	node((1, 0), [$(cal(D), (*), 1)$])
  	node((0, 0), [$bot_(underline(m), underline(eta), underline(epsilon))$])
  	edge((-1, 0), (1, 0), [$L$], label-side: left, "->", bend: 40deg)
  	edge((1, 0), (-1, 0), [$B$], label-side: left, "->", bend: 40deg)
  }))

  Is the data of :
  - A strong monoidal functor $(L, m) : (cC, ⋅, I) --> (cD, (*), 1)$
  - A functor $R : cD --> cC$
  - An adjunction $L attach(tack.l, br:(eta, epsilon)) R$
    $
    // https://q.uiver.app/#r=typst&q=WzAsMixbMCwwLCJjQyJdLFsxLDAsImNEIl0sWzAsMSwiTCIsMCx7Im9mZnNldCI6LTN9XSxbMSwwLCJSIiwwLHsib2Zmc2V0IjotM31dLFswLDEsImJvdF8oZXRhLCBlcHNpbG9uKSIsMSx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dXQ==
    #align(center, diagram({
    	node((0, 0), [$cC$])
    	node((1, 0), [$cD$])
    	edge((0, 0), (1, 0), [$L$], label-side: left, shift: 0.3, "->")
    	edge((1, 0), (0, 0), [$R$], label-side: left, shift: 0.3, "->")
    	edge((0, 0), (1, 0), [$bot_(eta, epsilon)$], label-side: center, " ")
    }))
    $
]

#definition[
  A _linear/non-linear adjunction_ is a summetric monoidal adjunction
  #align(center, diagram({
  	node((-1, 0), [$(VV, times, I)$])
  	node((1, 0), [$(LL, (*), 1)$])
  	node((0, 0), [$bot_(m, eta, epsilon)$])
  	edge((-1, 0), (1, 0), [$L$], label-side: left, "->", bend: 40deg)
  	edge((1, 0), (-1, 0), [$V$], label-side: left, "->", bend: 40deg)
  }))
]

=== The exponential comonoad $!$

Let $! = L compose V : bb(L) -> bb(L)$.
$forall a in "OB" bb(L), $ let $mu_A = L(  eta_(V A)) in bb(L)(L V A, L V L V A)$ \
($L V A "is" !A$, $L V L V A "is" !!A$,) \
Then $(!, epsilon, mu)$ is a comonad.
We then have

#diagram({
  node((0, 0), [$(LL_!, par, T)$])
  node((2, 0), [$(LL, (*), 1)$])
  node((1, 0), [$bot$])
  edge((0, 0), (2, 0), [$!$], label-side: left, "->", bend: 18deg)
  edge((2, 0), (0, 0), [$id$], label-side: left, "->", bend: 18deg)
})

where $bb(L)_!(A,B) := bb(L)(!A, B)$

#let big_adjunction(L, R, f, g, a: $bot$) = diagram({
	node((-1, 0), L)
	node((1, 0), R)
	node((0, 0), a)
	edge((-1, 0), (1, 0), f, label-side: left, "->", bend: 18deg)
	edge((1, 0), (-1, 0), g, label-side: left, "->", bend: 18deg)
})

#big_adjunction($(LL^!, (*), 1)$, $(LL, (*), 1)$, $"forget"$, $!$)

#definition[
  Let $cC$ be a category and $(!, epsilon, nu)$ a command on $cC$
  - The Kleisli category $cC_!$ is defined by
    $ &Ob(cC_!) = Ob(cC)\
      &cC_! (A, B) = cC(!A, B)\
      &"for" f in cC_! (A, B), g in cC_! (B, C)\
      &g << f in cC_!(A, C) "is defined by"\
      &g << f = f compose !f compose nu_A
    $
]

#exercise[
  Prove this defines a category.
]

#solution[
  - Identity is $epsilon$
  - $f << epsilon_A = f compose !epsilon_A compose eta_A = f$
  - $epsilon_B << f = epsilon_B compose !f compose eta_A = f compose epsilon_(!A) compose eta_A = f$
  - $
      h << (g << f) &= h compose !(g compose !f compose nu_A) compose nu_A = h compose !g compose !!f compose !nu_A compose nu_A \
      (h << g) << f &= (h compose !g compose nu_B) compose !f compose nu_A = h compose !g compose !!f compose nu_(!A) compose nu_A
    $

  Axioms of comonads
  // https://q.uiver.app/#r=typst&q=WzAsNCxbMSwwLCIhQSJdLFsxLDEsIiEhQSJdLFswLDEsIiFBIl0sWzIsMSwiIUEiXSxbMCwyLCJpZF8oIUEpIiwyXSxbMCwzLCJpZF8oIUEpIl0sWzEsMiwiIWVwc2lsb25fQSJdLFsxLDMsImVwc2lsb25fKCFBKSIsMl0sWzAsMSwibnVfQSIsMl1d
  - #align(center, diagram({
    	node((0, 0), [$!A$])
    	node((0, 1), [$!!A$])
    	node((-1, 1), [$!A$])
    	node((1, 1), [$!A$])
    	edge((0, 0), (-1, 1), [$id_(!A)$], label-side: right, "->")
    	edge((0, 0), (1, 1), [$id_(!A)$], label-side: left, "->")
    	edge((0, 1), (-1, 1), [$!epsilon_A$], label-side: left, "->")
    	edge((0, 1), (1, 1), [$epsilon_(!A)$], label-side: right, "->")
    	edge((0, 0), (0, 1), [$nu_A$], label-side: right, "->")
    }))
  // https://q.uiver.app/#r=typst&q=WzAsNCxbMCwwLCIhQSJdLFsxLDAsIiEhQSJdLFsxLDEsIiEhIUEiXSxbMCwxLCIhIUEiXSxbMCwxLCJudV9BIl0sWzEsMiwibnVfKCFBKSJdLFszLDIsIiFudV9BIiwyXSxbMCwzLCJudV9BIiwyXV0=
  - #align(center, diagram({
    	node((0, 0), [$!A$])
    	node((1, 0), [$!!A$])
    	node((1, 1), [$!!!A$])
    	node((0, 1), [$!!A$])
    	edge((0, 0), (1, 0), [$nu_A$], label-side: left, "->")
    	edge((1, 0), (1, 1), [$nu_(!A)$], label-side: left, "->")
    	edge((0, 1), (1, 1), [$!nu_A$], label-side: right, "->")
    	edge((0, 0), (0, 1), [$nu_A$], label-side: right, "->")
    }))
]

=== The Seely isomorphisms

Let $A, B in Ob(LL)$. Assue the cartesian product $A \& B$ exists in $LL$.

$V$ is the right adjoint $=>$ preserves limits.

$V ( A \& B ) tilde.eq V A times V B$

$L$ is strongly monoidal so $L (V A times V B) tilde.eq underbrace(L V A, !A) (*) underbrace(L V B, !B)$

So $underbrace(L V (A \& B), !(A \& B)) tilde.eq L V A (*) L V B tilde.eq !A (*) !B$

Similarly, if $LL$ has a terminal object $top$, $!top tilde.eq 1$.

== A model of Linear Logic : Probabilistic coherence spaces

#definition(subtitle: [Duality in $RR^X_+$])[
  Let $X$ be a countable set :
  - For all $x in X$, define $Pi_x : cases(RR^X_+ -> RR_+, a space t-> space a_x)$

    define $e_x in RR^X_+$ by $pi_x(e_x) = 1$
  - For all $a, b in RR^X_+$, let $a ⋅ b = sum_(x in X) a_x b_x in [0, +infinity[]$
  - For all $P subset.eq RR^X_+$, let
    $
      P^bot = { b in RR^X_+; forall a in P, underbrace((a⋅b <= 1), R(A, b)) } subset.eq RR^X_+
    $
    In particular $P^(bot bot) subset.eq P$
]

#definition([
  A probabilistic coherent space is a pair
  $X = (|X|, P X)$ where $|X|$ is a countable set, and $P X subset.eq RR^(|X|)_+$ such that
  - $P X ^(bot bot) = P X$ (equivalent to $P X ^(bot bot) subset.eq P X$)
  - $forall x in |X|$, 
    - $exists lambda > 0, lambda e_X in P X$  
    - $exists lambda > 0, lambda e_x in P X ^bot$
])


#example[
  $
    ({*}, [0, 1]) &=: 1\
                  &=: bot\
    (emptyset, {0}) &=: top\
                    &=: 0\
    (|X|, [0, 1]^(|X|))\
    ({0, 1}, ([0, 1]^2)^bot &= {binom(x, y) | (binom(1, 1) dot binom(x, y)) = x + y <= 1 }) \
  $
  Given $X = (|X|, P X)$ a pcoh,
  $X^bot := (|X|, P X^bot)$ is a pcoh.
]

#definition([
  Let $X, Y$ be pcohs. 
  A _linear morphism_ from $X$ to $Y$ is a map \
  #align(center)[$f in "Set"(P X, P Y)$]
  such that there exists a (necessarily unique) matrix $tilde(f) in RR^(|X| times |Y|)_+$ such that 
  for all $a in P X$, \ 
  #align(center)[$f(a) = (sum_(x in X) tilde(f)_(x,y) a_x)_(y in |Y|)$]
  pcohs and linear morphisms form a category PCoh.
])

#remark([ \
  $ tilde(id) = (delta_(x_1, x_2))_(cases(x_1 in  |X|, x_2 in |X|)) 
  #h(1cm) (delta_(x,y) = cases(1 #h(.2cm) & x = y, 0 & x eq.not y)) $ 
  $ tilde(g compose f) = tilde(g) tilde(f) = (sum_(y in |Y|) tilde(g)_(y,z) tilde(f)_(x, y))_(cases(x in |X|, z in |Z|)) $
])

#definition([
  Let $X_1, ..., X_n, Y$ be pcohs. A n-linear (or multilinear) map from $X_1, ..., X_n$ to $Y$ is a map 
  $ f in "Set"(P X_1  times ... times P X_n, P Y) $
  such that there exists a (necessarily unique) tensor 
  $ tilde(f) in RR^(|X_1| times ... times | X_n | times | Y |) $
  such that $forall (a_i) in (P X_i)$,
  $ f(a_1, ..., a_n) = (sum_(cases(x_1 in |X_1|, ..., x_n in |X_n|)) tilde(f)_(x_1, ... x_n, y) dot a_x_1 ... dot a_x_n )_(y in |Y|) $

])

#definition([
  $X (*) Y$ is defined by 
  $| X (*) Y| = |X| times |Y|$ and,
  $ P (X (*) Y)^bot = {tilde(f), f in "PCoh"(X, Y, 1)} $ ($f$ bilinear from $X, Y$ to 1)
])

#remark[
  For every $X, Y$ PCohs,
  $
    "PCoh"(X (*) Y, 1) & -> "PCoh"(X, Y\; 1) \
                  f & |-> ((a, b) |-> f(a (*) b))
  $
  is a bijection where
  $
    a (*) b = (a_x b_y)_(x, y) in P(X (*) Y)
  $
]
#proposition[
  For every PCohs $X, Y, Z$,
  $
    "PCoh"(X (*) Y, Z) & -> "PCoh"(X, Y\; Z) \
                  f & |-> ((a, b) |-> f(a (*) b))
  $
  is a bijection
]

#proposition[
  For every PCohs $W_1, ..., W_n, X, Y, Z$,
  $
    "PCoh"(W_1, ..., W_n, X (*) Y\; Z) & -> "PCo"h(W_1, ..., W_n, X, Y\; Z) \
    f & |-> ((w_1, ..., w_n, x, y) |-> f(w_1, ..., w_n, a (*) b))
  $
  is a bijection
]

#proposition[
  For every PCohs $W_1, ..., W_n, Z$,
  $
    "PCoh"(W_1, ..., W_n, 1\; Z) & -> "PCo"h(W_1, ..., W_n, X, Y\; Z) \
    f & |-> ((w_1, ..., w_n) |-> f(w_1, ..., w_n, 1))
  $
  is a bijection
]

#exercise[
  $("PCoh", **, 1)$ is symmetric monoidal.
]