976 lines
34 KiB
Typst
976 lines
34 KiB
Typst
#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: "Part 2", author: "Guillaume Geoffroy's Course\nNotes by Lyes Saadi")
|
||
|
||
#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.
|
||
]
|