[INCLUDE TH/speedbar.blogme] [SETFAVICON dednat4/dednat4-icon.png] [lua: LR = R ] [# (defun c () (interactive) (find-blogme3-sh0-if "2007semantics")) ;; http://angg.twu.net/2007semantics.html ;; file:///home/edrx/TH/L/2007semantics.html #] [lua: -- (eev-math-glyphs-edrx) eev_math_glyphs_edrx() ] [htmlize [J Basic Semantics] [WITHINDEX [# # «.cats-with-finite-prods» (to "cats-with-finite-prods") # «.a-ring-in-a-CFP» (to "a-ring-in-a-CFP") # «.CCC-diagrams» (to "CCC-diagrams") # «.CCCs-in-half-DNC» (to "CCCs-in-half-DNC") # «.CCCs-to-L1:products» (to "CCCs-to-L1:products") # «.CCCs-to-L1:products-eqs» (to "CCCs-to-L1:products-eqs") # «.deleted-diagrams» (to "deleted-diagrams") # «.new-diagrams» (to "new-diagrams") #] [RULE ----------------------------------------] [# (find-2005oct20seminar "" "lings-internas-CFPs") (find-2005oct20seminarpage 39) ð(a,a',(b, c)):A×A×(B×C).(c,a'),a' #] [tsec «cats-with-finite-prods» (to ".cats-with-finite-prods") [++N]. Categories with finite products ====================================== Categories with finite products (CFPs) are categories in which we can interpret tuples and projections. Our archetypal CFP is Set. An example of the translation: a,a',(b,c) |---------------> (c,a'),a' becomes: <<_3;_2,_1>,_1> A×A×(B×C) ------------------> (C×A)×A How? Let's look at how we construct (c,a'),a' from a,a',(b,c): a,a',(b,c) ----------_3 b,c a,a',(b,c) ---_2 ----------_2 c a' a,a',(b,c) ----------------<,> ----------_2 c,a' a' -------------------------<,> (c,a'),a' Now let's make the contexts explicit (p := a,a',(b,c), for typographical reasons): p|-a,a',(b,c) -------------_3 p|-b,c p|-a,a',(b,c) ------_2 -------------_2 p|-c p|-a' p|-a,a',(b,c) -----------------------<,> -------------_2 p|-c,a' p|-a' -------------------------------<,> p|-(c,a'),a' Translating: id --- _3 id ------- --- _3;_2 _2 id ---------------- --- <_3;_2,_2> _2 --------------------- <<_3;_2,_2>,_2> Notation: 1={*} is the 0-ary product. Example: a,b|->* (``!'') is the only morphism from A×B to 1. It's not important to differentiate the ``*''s - for example, *,*' |-> *,*' and *,*' |- *',* are the same morphism from 1×1 to 1×1 - we can write it just as *,* |-> *,*. ] [tsec «a-ring-in-a-CFP» (to ".a-ring-in-a-CFP") [++N]. A ring in a CFP ====================== A ring in a CFP is an object R equipped with five morphisms, z s 1 ----> R <----- R×R * |---> 0 1 ----> R <----- R×R * |---> 1 u m a+b <----| a,b n ab <----| a,b R -----> R a |---> -a These morphisms must obey certain equations, one for each ring axiom. For example, ýa,b,c. a(b+c) = ab+ac becomes the following equation on morphisms: (a,b,c |-> a(b+c)) = (a,b,c |-> ab+ac) t|-b t|-c t|-a t|-b t|-a t|-c ---------- ---------- ---------- t|-b,c t|-a,b t|-a,c ------ ------ ----- t|-a t|-b+c t|-ab t|-ac -------------- ------------------ t|-a,(b+c) t|-ab,ac ---------- -------- t|-a(b+c) = t|-ab+ac _1 _2 _0 _1 _0 _2 --------- --------- --------- <_1,_2> <_0,_1> <_0,_2> ----------- ----------- ----------- _0 <_1,_2>;s <_0,_1>;m <_0,_2>;m ------------------ ------------------------- <_0,<_1,_2>;s> <<_0,_1>;m,<_0,_2>;m> ------------------- --------------------------- <_0,<_1,_2>;s>;m = <<_0,_1>;m,<_0,_2>;m>;s ] [RULE ------------------------------------------------------------] [tsec «CCC-diagrams» (to ".CCC-diagrams") [++N]. CCC Diagrams =================== Note (1): these diagrams function as a ``skeleton'' for the whole proof - we take the diagram, add layers of meat and skin, and we reconstruct the whole animal. As far as I know, the standard proofs for CCC<->ð1 don't have a ``center'' that is as clear as we have here. Note (2): our idea of ``dictionaries'' is related to the idea of ``internal languages'' in Categorical Semantics. It is common in, e.g., Topos Theory, to take a set-theoretical proof, then check that it is well-behaved enough, and then say that ``this proof works in any topos''. This corresponds to our liftings; but internal languages assign precise meanings to all well-formed expressions of a certaing language, while our dictionaries will only attribute meanings to those expressions that are mentioned, directly or indirectly, in our proofs. /Internal languages induce infinite dictionaries/; and our way of building dictionaries from proofs will let us deal with arising ambiguities one by one, in organic (and ad-hoc) ways... ] [tsec «CCCs-in-half-DNC» (to ".CCCs-in-half-DNC") [++N]. CCCs in half-DNC ======================= This diagram expresses the structure in a CCC: A CCC is a category plus this "structure": --| a |-- a a,b <==== a / - \ - - - / | \ | | <--> | v v v v v v b <--| b,c |--> c * c ===> b|->c The product diagram comprises two operations on morphisms, and the adjunction diagram four: (we'll forget the terminal for the moment) / a \ / a \ | - | | - - | | | | |-> | / \ | | v | | v v | \ b,c / \ b c / / a \ / a \ | - - | | - | | / \ | |-> | | | | v v | | v | \ b c / \ b,c / a',b <==== a' - - | <--| | v v a,b <==== a - - | <--| | | |--> | v v c ===> b|->c - - | |--> | v v c' ==> b|->c' a',b <==== a' - - p|- | <--| | a'|-a(a') v v a,b <==== a - - p|-f(p)('p) | <--| | a|-f(a) p|-c(p) | |--> | a|-ðb.c() v v c ===> b|->c - - c|-c'(c) | |--> | f|-ðb.c'(fb) v v c' ==> b|->c' ] [tsec «CCCs-to-L1:products» (to ".CCCs-to-L1:products") [++N]. From CCCs to ð-calculus: products ======================================== From diagrams to natural deduction: propositional calculus / P \ / P \ P P | - | | - - | : : | | | |-> | / \ | P|-Q&R P|-Q&R Q&R Q&R | v | | v v | ====== ====== --- --- \ Q&R / \ Q R / P|-Q P|-R Q R / P \ / P \ P P | - - | | - | : : | / \ | |-> | | | P|-Q P|-R Q R | v v | | v | =========== ------- \ Q R / \ Q&R / P|-Q&R Q&R / a \ / a \ a a | - | | - - | : : | | | |-> | / \ | a|-b,c a|-b,c b,c b,c | v | | v v | ====== ====== --- --- \ b,c / \ b c / a|-b a|-c b b / a \ / a \ a a | - - | | - | : : | / \ | |-> | | | a|-b a|-c b c | v v | | v | =========== ------- \ b c / \ b,c / a|-b,c a,c In half-DNC: / a \ / a \ a a | - | | - - | : : | | | |-> | / \ | a|-p(a) a|-p(a) p(a) p(a) | v | | v v | ======== ========= ----- ------ \ p(a) / \p(a) 'p(a)/ a|-p(a) a|-'p(a) p(a) 'p(a) / a \ / a \ a a | - - | | - | : : | / \ | |-> | | | a|-b(a) a|-c(a) b(a) c(a) | v v | | v | ================= ----------- \ b(a) c(a) / \/ a|- ] [tsec «CCCs-to-L1:products-eqs» (to ".CCCs-to-L1:products-eqs") [++N]. From CCCs to ð-calculus: equations for products ====================================================== The two arrows (coming from the natural transformations) are inverses, so their two composites must be identites: / a \ / a \ / a \ | - | | - - | | - | | | | |-> | / \ | |-> | | | = id | v | | v v | | v | \ p(a) / \p(a) 'p(a)/ \<p(a),'p(a)>/ / a \ / a \ / a \ | - - | | - | | - - | | / \ | |-> | | | |-> | / \ | = id | v v | | v | | v v | \ b(a) c(a) / \/ \ '/ ýp:B×C. p=<p,'p> ýb:B,c:C. b= ýb:B,c:C. c=' ] [tsec «deleted-diagrams» (to ".deleted-diagrams") [++N]. Deleted diagrams ======================= a,b <==== a - - | <--| | v v a',b <==== a' a,b <==== a a,b <==== a - - - - | <--| | | |--> | v v v v c ===> b|->c c ===> b|->c c ===> b|->c - - | |--> | v v c' ==> b|->c' If we translate these six operations to half-DNC we get: / a \ / a \ | - | | - - | | | | |-> | / \ | | v | | v v | \ p(a) / \ p(a) 'p(a) / / a \ / a \ | - - | | - | | / \ | |-> | | | | v v | | v | \ b(a) c(a) / \ / p <=========== a - - | <--| | v v <=== a'(a) p <========= a p <========== a - - - - | <--| | | |--> | v v v v f(p)('p) ===> f(a) c(p) ====> ðb.c() c ===========> f - - | |--> | v v c'(c) =====> ðb.c'(fb) ] [tsec «new-diagrams» (to ".new-diagrams") [++N]. New diagrams =================== An adjunction has 4 operations on morphisms =========================================== P'&Q <==== P' - - | <--| | v v P&Q <==== P - - | <--| | | |--> | v v R ====> Q¶R - - | |--> | v v R ====> Q¶R Translating categorical operations to ð-calculus ================================================ P'&Q ---- P'&Q <==== P' P' P'&Q - - : ---- P'&Q|-P&Q | <--| | P'|-P P'|-P P Q v v ========= ------ P&Q <==== P P'&Q|-P&Q P&Q a',b p ---- -- a',b <==== a' a' a',b p p - - : : : --- p|- | <--| | a'|-a(a') a(a') b a(p) 'p v v ---------- ----------- a,b <==== a a',b <==== a' - - p|- | <--| | a'|-a(a') v v a,b <==== a - - p|-f(p)(pi'p) | <--| | a|-f(a) p|-c(p) | |--> | a|-ðb.p() v v c ===> b|->c - - c|-c'(c) | |--> | f|-ðb.c'(fb) v v c' ==> b|->c' The product and the terminal ============================ Translating ð-calculus rules to categorical constructions ========================================================= ] ] ] [# # Local Variables: # coding: raw-text-unix # modes: (fundamental-mode blogme-mode) # End: #]