|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008typesystems.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008typesystems.tex && latex 2008typesystems.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008typesystems.tex && pdflatex 2008typesystems.tex"))
% (eev "cd ~/LATEX/ && Scp 2008typesystems.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008typesystems.dvi")
% (find-pspage "~/LATEX/2008typesystems.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008typesystems.ps 2008typesystems.dvi")
% (find-pspage "~/LATEX/2008typesystems.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% TODO: borrow more from:
% (find-LATEX "2002fmcs.tex")
% (find-LATEXdvi "2002fmcs.dvi")
% «.intro-to-bhk» (to "intro-to-bhk")
% «.witnesses-vs-proofs» (to "witnesses-vs-proofs")
% «.intro-to-ptss» (to "intro-to-ptss")
% «.notation-space-of» (to "notation-space-of")
% «.dependent-types» (to "dependent-types")
% «.spaces-of-witnesses-set» (to "spaces-of-witnesses-set")
% «.typing-categories-1» (to "typing-categories-1")
% «.typing-categories-2» (to "typing-categories-2")
% «.typing-categories-3» (to "typing-categories-3")
\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\begin{document}
\input 2008typesystems.dnt
%*
% (eedn4-51-bounded)
Index of the slides:
\msk
% To update the list of slides uncomment this line:
\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\tocline {Introduction to BHK} {2}
\tocline {Spaces of witnesses as spaces of proofs, collapsed} {3}
\tocline {Pure Type Systems} {4}
\tocline {Notation (temporary) for ``the space of''} {5}
\tocline {Dependent types} {6}
\tocline {Spaces of witnesses in Set} {7}
\tocline {Typing categories (1)} {8}
\tocline {Typing categories (2)} {9}
\tocline {Typing categories (3)} {10}
\setlength{\parindent}{0em}
\newpage
% --------------------
% «intro-to-bhk» (to ".intro-to-bhk")
% (s "Introduction to BHK" "intro-to-bhk")
\myslide {Introduction to BHK} {intro-to-bhk}
{\myttchars
\footnotesize
\begin{verbatim}
Suppose that for atomic propositions P, Q, R(4,2), etc,
we know how to characterize what constitutes a ``proof''
of P, Q, R(4,2), etc.
Write W[P] for the ``space of proofs of P'',
W[R(4,2)] for the ``space of proofs of R(4,2)'',
and so on.
The BHK (Brouwer-Heyting-Kolmogorov) interpretation
tells us how to build the ``spaces of (constructive)
proofs'' for all (bigger) formulas whose atomic
formulas are just P, Q, R(4,2), etc... the rules are:
W[P&Q] := W[P]×W[Q]
W[P⊃Q] := W[P]->W[Q]
W[P∨Q] := {0}×W[P] þ {1}×W[Q]
W[§] := {*}
W[®] := \emptyset
W[ýa¨A.P(a)] := åa¨A.W[P(a)]
W[Îa¨A.P(a)] := Æa¨A.W[P(a)]
Note that this is different from just saying that
``the space of witnesses of P is a singleton when
P is true, and the empty set when P is false'' -
because W[§∨§] = {(0,*),(1,*)}
and W[În¨\N.§] = {(0,*),(1,*),(2,*),...} -
`∨' and `Î' take us out of the realm of sets
of size 0/1.
\end{verbatim}
}
\newpage
% --------------------
% «witnesses-vs-proofs» (to ".witnesses-vs-proofs")
% (s "Spaces of witnesses as spaces of proofs, collapsed" "witnesses-vs-proofs")
\myslide {Spaces of witnesses as spaces of proofs, collapsed} {witnesses-vs-proofs}
{\myttchars
\footnotesize
\begin{verbatim}
Our (archetypical) space of truth-values:
Ø = {0, 1} = {{}, {*}}
A ``space of witnesses'' for us is a set
that is ``at most a singleton'' (size=0/1).
a:A:Þ A is a set, a is an element of A
P:Ï[P]:Ø Ï[P] is a space of witnesses,
P is a witness for the proposition P.
Interpreting BHK categorically is hard, and uncommon
(see Palmgren 2002; it refers to Makkai/Reyes 1977).
Interpreting propositions using this Ø
(like BHK, but collapsing the spaces of proofs into
sets that are ``at most singletons'') is easy,
and that's what we will do.
In BHK we start from W[P], W[Q], W[R(4,2)], ...
and we build all the spaces of proofs for propostions
whose atomic propositions are just these.
Here we will also start from spaces of witnesses
for the atomic propositions, and build all other
spaces of witnesses from them.
In the archetypical model - Set - these spaces of
witnesses will be exactly what we expect
(classical logic).
In some toposes the logic will be intuitionistic,
not classical - for example, we may have
Ï[P] \subsetneq Ï[¬¬P].
\end{verbatim}
}
\newpage
% --------------------
% «intro-to-ptss» (to ".intro-to-ptss")
% (s "Pure Type Systems" "intro-to-ptss")
\myslide {Pure Type Systems} {intro-to-ptss}
{\myttchars
\footnotesize
\begin{verbatim}
PTSs generalize the type system for ð-calculus
that we've seen (``ð1'') and other systems that
we will see.
We have supposed that we knew sets A, B, C
to derive:
b|->c
=========
a,b|->a,c
In a PTS we don't have any constants besides the
``sorts'', that typically are Ø:Þ:ñ, whose intended
semantics are, VERY roughly:
ñ (the class of all) classes
Þ (the class of all) sets
Ø the set of truth-values
(Ø has two elements, ``true'' and ``false'')
Constants - like:
A,B,C:Þ
\R:Þ
+:\R×\R->\R
assoc:Ï[ýx,y,z:\R.(x+y)+z=x+(y+z)]:Ø
can be added later, as ``impurities''.
The idea is that Pure Type Systems are flexible enough
to let us declare the constants that we need as
variables in the beginning of a context.
In a PTS we can derive:
A:Þ,B:Þ,C:Þ,f:(B->C) |- (ðp:A×B.<p,f('p)>):A×B->A×C
which, in DNC notation, shrinks to:
A,B,C,(b|->c)|-(a,b|->a,c)
\end{verbatim}
}
\newpage
% --------------------
% «notation-space-of» (to ".notation-space-of")
% (s "Notation (temporary) for ``the space of''" "notation-space-of")
\myslide {Notation (temporary) for ``the space of''} {notation-space-of}
{\myttchars
\footnotesize
\begin{verbatim}
{a,b|P(a,b)} {a,b|P(a,b)}
v v
| becomes: |
v v
A×B {a,b}
We will write ``{a,b}'' for A×B.
``{a,b}'' will stand for ``the set of all
possible values for (a,b)''.
Note that this conflicts with the
set-theoretical usage - ``the set with
two elements, a and b''...
(I used to use \E[a,b] for {a,b}, but
many people felt that that was too weird...)
The same notation - {a,b} - will also work
for ``dependent types'' (next slides), where
a:A,b:B_a, and B_a depends on a...
\end{verbatim}
}
\newpage
% --------------------
% «dependent-types» (to ".dependent-types")
% (s "Dependent types" "dependent-types")
\myslide {Dependent types} {dependent-types}
{\myttchars
\footnotesize
\begin{verbatim}
Suppose that we have:
A a set: the space of `a's
(B_a)_{a:A} a family of sets/spaces (of `b's)
(C_a)_{a:A} another family of sets
(D_abc)_{(a,b,c):\{a,b,c\}} another family
Note that
{a:A,b:B_a,c:C_a} ----> {a:A,c:C_a}
| __| |
| |
v v
{a:A,b:B_a} ----------> {a:A}
is a pullback.
Alternative notations:
{a,b,c} ----> {a,c} a,b,c |----> a,c
| __| | - __| -
| | | |
v v v v
{a,b} ------> {a} a,b |------> a
Maps (between ``contexts'') that just drop
the last variable - all but the top one in
the squares above - are called ``one-step
projections''.
What are ``generalized projections''?
We will see that later...
\end{verbatim}
}
\newpage
% --------------------
% «spaces-of-witnesses-set» (to ".spaces-of-witnesses-set")
% (s "Spaces of witnesses in Set" "spaces-of-witnesses-set")
\myslide {Spaces of witnesses in Set} {spaces-of-witnesses-set}
{\myttchars
\footnotesize
\begin{verbatim}
More families:
(\P_ab)_{(a,b):\{a,b\}} a family of spaces of witnesses,
(\Q_a)_{a:A} another,
(\R_ab)_{(a,b):\{a,b\}} another.
We can use spaces of witnesses to represent propositions:
a proposition is false when its space of witnesses is empty,
true when it is non-empty.
{a,b||P(a,b)} |---> {a||Îb.P(a,b)}
{a,b||R(a,b)} |---> {a||ýb.R(a,b)}
\end{verbatim}
}
\newpage
% --------------------
% «typing-categories-1» (to ".typing-categories-1")
% (s "Typing categories (1)" "typing-categories-1")
\myslide {Typing categories (1)} {typing-categories-1}
{\myttchars
\footnotesize
\begin{verbatim}
A category is a 7-uple,
(Objs, Hom, id, ¢, idL, idR, assoc)
where the first four components are ``structure''
and the last three are ``properties''.
They can by typed like this:
(this looks indirect, but can be formalized...
note that this is a locally small category -
its hom-sets are sets, not classes)
|-Objs:ñ
A:Objs,B:Objs|-Hom(A,B):Þ
A:Objs|-id_A:Hom(A,A)
A:Objs,B:Objs,C:Objs,f:Hom(A,B),g:Hom(B,C)
|-(g¢f):Hom(A,C)
A:Objs,B:Objs,f:Hom(A,B)|-idL_f:W[f¢id_A=f]
A:Objs,B:Objs,f:Hom(A,B)|-idR_f:W[id_B¢f=f]
A:Objs,B:Objs,C:Objs,D:Objs,
f:Hom(A,B),g:Hom(B,C),h:Hom(C,D)
|-assoc(f,g,h):W[h¢(g¢f)=(h¢g)¢f]
We are using some shorthands...
The constants that we are declaring are actually
Objs,(Hom),(id),(¢),(idL),(idR),assoc:
Hom(A,B) := (Hom) A B
id_A := (id) A
(g¢f) := (¢) A B C f g
idL_f := (idL) A B f
idR_f := (idR) A B f
assoc(f,g,h) := (assoc) A B C D f g h
and we are using ``identity types'':
X:Þ,x:X,x':X|-W[x=x']:Ø
W[x=x'] := Eq X x x'
and we should imagine that we also have terms that
assert that this ``equality'' is reflexive, symmetric,
transitive, and stable by substitutions - but these
terms will not be used in the spefication of the
typing of a category.
\end{verbatim}
}
\newpage
% --------------------
% «typing-categories-2» (to ".typing-categories-2")
% (s "Typing categories (2)" "typing-categories-2")
\myslide {Typing categories (2)} {typing-categories-2}
{\myttchars
\footnotesize
\begin{verbatim}
Let's make this typing less indirect.
Instead of:
|-Objs:ñ
A:Objs,B:Objs|-(Hom)AB:Þ
A:Objs|-(id)A:(Hom)AA
A:Objs,B:Objs,C:Objs,f:(Hom)AB,g:(Hom)BC
|-(¢)ABCfg:(Hom)AC
This:
|-Objs:ñ
|-(Hom):(åA:Objs.åB:Objs.Þ)
|-(id):(åA:Objs.(Hom)AA)
|-(¢):(åA:Objs.åB:Objs.åC:Objs.
åf:(Hom)AB.åg:(Hom)BC.(Hom)AC)
The exact typing of (Hom), (id), (¢), etc is immaterial -
for example, (Hom) can be either :(Objs->(Objs->Þ)) or
:(Objs×Objs->Þ), it doesn't matter.
Problems:
(1) The domains of these functions are too big.
(2) We need dependent types.
Let's examine one particular case: \Set.
|-Þ:ñ
|-(ðA:Þ.ðB:Þ.A->B):(åA:Þ.åB:Þ.Þ)
|-(ðA:Þ.ða:A.a):(åA:Þ.(ðA:Þ.ðB:Þ.A->B)AA)
rewriting:
|-Þ:ñ
|-(ðA:Þ.ðB:Þ.A->B):(Þ->(Þ->Þ))
|-(ðA:Þ.ða:A.a):(åA:Þ.A->A)
Some domains of functions are Þ - a class, not a set -
and, in (id) - the ``polymorphic identity'' -
the space where ða:A.a lives - A->A - depends on A...
\end{verbatim}
}
\newpage
% --------------------
% «typing-categories-3» (to ".typing-categories-3")
% (s "Typing categories (3)" "typing-categories-3")
\myslide {Typing categories (3)} {typing-categories-3}
{\myttchars
\footnotesize
\begin{verbatim}
Some of these terms can only be declared after others have
been declared: (Hom) after Objs, (id) and (¢) after Hom...
``Earlier'' terms and variables appear higher at
derivation trees than ``later'' terms and variables...
Here's a diagram showing the dependencies:
Objs
|
Hom
/ \
id ¢
| / \
idL,idR assoc
It is possible to build the ``space of all categories'',
but it will depend on the order that we will choose for
the components - and then we would define Objs, Hom, etc,
as certain components of these 7-uples...
(Objs,Hom,id,¢,idL,idR,assoc):(Æ_.Æ_.Æ_.Æ_.Æ_.Æ_._)
(Objs,Hom,¢,id,assoc,idL,idR):(Æ_.Æ_.Æ_.Æ_.Æ_.Æ_._)
(Actually the first `Æ' - ÆObjs:ñ._ - is problematic, as
it would require a sort above ñ - but this is not
important now)
\end{verbatim}
}
% Add:
% Propositions as dependent types
% ÎÏ[P].P satisfiable
% ýÏ[P].P⊃P tautology
% (and theorem)
%
% Blob diagram
% (find-es "tex" "ovals")
% Doctrinal diagram
% Smashing operator
% PTSs with minimal contexts
% Category of contexts
% Projections form a preorder
% Products are pullbacks
% What are the conditions on sections?
% They can only be added after their
% inverses; they must commute with what?
% An a|->a,b says that a,b has as much information as a.
% Comparison with quotients (on HAs) and equations (a<->a,b)
% Display maps
% Projections, generalized projections, proper projections,
% one step projections; unit types; the formal way to see
% variables
% Diagram for a,b`->a,b,b',(b=b')
% A magic rule says that this is not just a section
% LCCCs
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: