Downcasing SetsQuick index:
1. Main idea: lifting archetypal proofs ======================================= Take a proof of some general statement. Now specialize it to a particular case. ``Specializing'' is somehow like doing a projection - some distinctions collapse, some details are lost - Here we are concerned with the opposite of specializing proofs. We start with an ``archetypal proof'' - a proof of a certain very particular case, done in a certain language - and then we /change our dictionary a bit/ - and some terms change meaning; and the same proof becomes a proof of the general case - We call this ``lifting''. Archetypal proofs /lift/ to more general proofs, and when this happens we get general proofs done in a language inherited from the archetypal cases. My favorite examples of such liftings of proofs are for proofs in Categorical Semantics. The fist significant example will be this one (we call it ``CCC<->λ1''): The Cartesian-Closed Categories (CCCs) are exactly the categories where we can interpret the simply-typed λ-calculus (``System λ1''). After ``CCC<->λ1'' we will see ``Hyp<->LPCE'': The hyperdoctrines are exactly the categories in which we can interpret (a certain system of intuitionistic, typed) first-order logic (``LPCE''). 2. Lifting set-like notation ============================ Our approach: `Set' is our archetypal CCC. Sets are also our archetypal model for λ1. Most of the proof - even most of the details of the statement of the theorem! - will appear more or less naturally from taking the diagrams below, done in the language of ``downcased types'' (DNC) and translating them in several ways. --| a |-- a a,b <==== a / - \ - - - / | \ | | <--> | v v v v v v b <---| b,c |---> c * c ===> b|->c --| P |-- P P&Q <==== P / - \ - - - / | \ | | <--> | v v v v v v Q <---| Q&R |---> R ⊤ R ====> Q⊃R Later, Set (or, more precisely, the fibration Set^>->), we will also be our archetypal hyperdoctrine. 3. Starting point: the Curry-Howard Isomorphism =============================================== There is a correspondence between Natural Deduction trees and terms of the simply-typed λ-calculus (λ1). Example: P&Q d:A×B --- ----- P&Q Q Q⊃R d:A×B π'd:B f:B->C --- ---------- ----- --------------- P R πd:A f(π'd):C ----------- ------------------ P&R <πd,f(π'd)>:A×C Sometimes the usual notation for type theory/ λ-calculus feels too verbose. The DNC notation started as an informal reasoning tool - I used it in my private notes as a system of abbreviations for λ-calculus. DNC grew with time and started to look more formal... It got special arrow symbols (a.k.a. ``connectives'' - `=>' and `-.>') to represent functors and natural transformations. In 2001 I found that `=>' and `-.>' had introduction rules besides the obvious elimination rules (think in introd and elim of `&', `⊃', `\or', etc in Natural Deduction) - so DNC could be the basis for a system of natural deduction for categories. DNC never became formal enough to be a ``system'', and nowadays it lives a more unpretentious existence as an auxiliary language for type theory and category theory (esp. categorical semantics). I changed the meaning for ``DNC'' - from a sytem for ``Natural Deduction for Categories'' to a notation of ``DowNCased types''. 4. Main ideas ============= Long names for variables ------------------------ In {(n,r)∈N×R | r^2=n} the (n,r) is the name of a variable - N×R is the space of pairs made of a natural number and a real. A dictionary ------------ Define n := π (n,r) r := π'(n,r) (r,n) := <r,n> The syntactical distinction between variables and terms ------------------------------------------------------- We've sacrificed it. Also, without the dictionary there is no way to tell from (n,r), n, r, (r,n) which of them are more primitive than the others. Downcasing ---------- The default name for a variable ranging over A is `a'. The default (long!) name for a variable ranging over A×B is `(a,b)'. Spaces of functions ------------------- In f:A->B we will read ``A->B'' as B^A and the ``:'' as the `:' of Type Theory. (For mathematicians: `:' is roughly like `∈', but ``f:A->B'' means also ```f' is of type `A->B''', and each term has a single type. We are not interesting in `\subset', `\subseteq', etc). Notation for functions ---------------------- An `a|->b' is an element of A->B. An `a|->b' is a function that takes each `a' to a `b'. Reconstructing the types and the dictionary from trees ------------------------------------------------------ d:A×B ----- d:A×B π'd:B f:B->C ----- --------------- πd:A f(π'd):C ------------------ <πd,f(π'd)>:A×C a,b --- a,b b b|->c a := π (a,b) --- ---------- b := π'(a,b) a c c := (b|->c)(b) ----------- a,c := <a,c> a,c Now add ``a,b := d'' and ``b|->c := f'' and we get the λ-calculus terms back from the DNC tree. Note that we obtain the types back by uppercasing the DNC ``terms'' - `|->' is uppercased to `->', `,' to `×', etc. 5. Contexts and discharges -------------------------- Each subtree of a Natural Deduction tree/derivation/proof corresponds to a smaller proof contained in a bigger one. For each node of a tree let's look at the tree above the node, and make its hypotheses explicit. P&Q P&Q|-P&Q --- -------- P&Q Q Q⊃R P&Q|-P&Q P&Q|-Q Q⊃R|-Q⊃R --- ---------- -------- -------------------- P R P&Q|-P Q⊃R,P&Q|-R ----------- ------------------------- P&R Q⊃R,P&Q|-P&R Now we can understand the ``⊃-introduction'' rule; it involves a discharge. [P&Q]^1 P&Q|-P&Q ------- -------- [P&Q]^1 Q Q⊃R P&Q|-P&Q P&Q|-Q Q⊃R|-Q⊃R ------- --------- -------- -------------------- P R P&Q|-P Q⊃R,P&Q|-R ------------- ------------------------- P&R Q⊃R,P&Q|-P&R -------1 ------------ P&Q⊃P&R Q⊃R|-P&Q⊃P&R Below the bar marked with ``1'' the hypotheses marked with ``[·]^1'' should no longer be in the list of hypotheses - they've been ``discharged'' (into the conclusion). Let's look at the functional side of this (Curry-Howard): [a,b]^1 (a,b)|-(a,b) ------- ------------ [a,b]^1 b b|->c (a,b)|-(a,b) (a,b)|-b (b|->c)|-(b|->c) ------- ----------- ------------ --------------------------- a c (a,b)|-a (b|->c),(a,b)|-c --------------- --------------------------------------- a,c (b|->c),(a,b)|-(a,c) ---------1 -------------------- a,b|->a,c (b|->c)|-(a,b|->a,c) [p]^1 p|-p ----- ------ [p]^1 π'p f p|-p p|-π'p f|-f ----- --------- ----- --------------- πp f(π'p) p|-πp f,p|-f(π'p) ----------------- ---------------------- <πp,f(π'p)> f,p|-<πp,f(π'p)> --------------1 -----------------1 λp.<πp,f(π'p)> f|-λp.<πp,f(π'p)> The ``⊃-introduction'' rule (last bar) corresponds to introducing a `λ'; one variable ceases to be free, and is removed from the list if hypotheses. One way of reading ``f,p|-<πp,f(π'p)>'' - or ``f:B->C,p:A×B|-<πp,f(π'p)>:A×C'' - is: if we know the value of f and p (points of B->C and A×B) we know the value of <πp,f(π'p)> (a point of A×C). 6. Expanding trees ================== a,b a,b:A×B --- |--------------> ------- a a:A - - - - | \ | \ | v | v | a,b|-a,b | a,b:A×B|-a,b:A×B | -------- |---------> ---------------- | a,b|-a | a,b:A×B|-a:A | - | - - | | | | \ | | | | v | | | | (a,b|-a,b):A×B->A×B | | | | ------------------- p | p:A×B | (a,b|-a):A×B->A -- |- - - | - - - -> ----- | - πp | πp:A | | - | - | | \ | \ | | v v v v | p|-p p:A×B|-p:A×B | ----- |- - - - - - -> ------------ | p|-πp p:A×B|-πp:A | - - | \ \ | v v v id id_{A×B}:A×B->A×B --- |- - - - - - - -> ----------------- π_0 π_{0\,A,B}:A×B->A L 7. Theorems for Free ==================== From the ``Theorems for Free'' paper (Wadler 1989): * All closed terms of type ∀A.∀B.(A×B->B×A) obey a certain theorem * Corollary: all terms of type ∀A.∀B.(A×B->B×A) are the flip function. Something similar (but much looser) happens in DNC: `a,b|->b,a' has a ``natural definition'' - apply Curry-Howard, prove P&Q⊃Q&P, translate the proof to λ-calculus in DNC notation - [P&Q]^1 [P&Q]^1 [a,b]^1 [a,b]^1 [p]^1 [p]^1 ------- ------- ------- ------- ----- ----- Q P b a π'p πp ----------- ----------- ---------- Q&P b,a <π'p,πp> -------1 ---------1 -----------1 P&Q⊃Q&P a,b|->b,a λp.<π'p,πp> and an argument using normalization of ND proofs can be used to show that all other ND proofs (= λ-terms) are equivalent to that one. In DNC we won't be interested in the ``uniqueness'' part very often, though. L 8. Ambiguity plays on our side (usually) ======================================== a,b a,b p p --- --- -- --- a := π (a,b) a b πp π'p b := π'(a,b) ------- -------- a,b := <a,b> a,b <πp,π'p> Apparently the DNC tree on the left, above introduces a ``secondary definition'' for a,b and a circularity in the dictionary, and such things have to be avoided at all costs - But we can be careful and interpret each tree as a term, and in a,b a,b p p --- --- -- --- a b πp π'p ------- -------- a,b = a,b <πp,π'p> = p what happens is that we have two different ``natural constructions'' for a,b from a,b, and we're saying that the two ``must give the same result'', i.e., <πp,π'p> = p... In many contexts we will have two different natural constructions for a DNC ``term'' with a certain name, and we will want to say that the two constructions give the same result (sometimes this will be an axiom, sometimes a theorem, sometimes a hypothesis) - We will sometimes use the expression ``is well defined'' (notation: ``wd[·]'') in a funny sense: ``wd[a,b]'' will mean ``the two obvious natural constructions for a,b give the same result''. L 9. Downcasing functors ====================== A functor F:\catC->\catD is composed of two operations: F_0 - its action on objects, and F_1 - its action of morphisms. Fix a set B, and look at these diagrams, for the functors (×B):Set->Set and (B->):Set->Set: A×B <---| A a,b <==== a - - - - f×B| <-| |f | <-| | v v v v A'×B <---| A' a',b <==== a' C |----> B->C c ====> b|->c - - - - g| |-> |B->g | |-> | v v v v C' |---> B->C' c' ===> b|->c' Functors act on two levels, so we will use a double arrow - `=>' - to denote them. Their names in DNC will come from their action on objects: A|->A×B a=>a,b C|->B->C c=>b|->c Their ``syntactical actions'' on morphisms can be derived from their names: a=>a,b adds a ``,b'' to the name of each object, so it takes a|->a' to a,b|->a',b; same for c=>b|->c. To find the ``real action'' of (×B)=(a=>a,b) on morphisms, look for a natural construction of a,b|->a',b from a|->a; f×B = a,b|->a',b = λp.<f(πp),π'p>. Note that a functor a=>a,b does not take `a's into `a,b's, like an arrow a|->a,b would do; instead, it takes the whole space of `a's, E[a]=A, into the space of `a,b's, E[a,b]=A×B - (×B)_0 = λA:Sets.A×B. 10. Products via natural transformations ======================================== Any diagram b <--| p |--> c induces an operation that takes any object A to a map of sets (A->P) -> (A->B)×(A->C) / a \ / a \ | - | | - - | | | | |--> | / \ | | v | | v v | \ p / \ b c / 11. Downcasing Natural Transformations ====================================== (...) Between two contravariant functors, Hom(-,P): Set^op -> Set A |-> A->P a^op => a|->p Hom(-,B)×Hom(-,C): Set^op -> Set A |-> (A->B)×(A->C) a^op => (a|->b),(a|->c) The natural transformation T: Hom(-,P) -> Hom(-,B)×Hom(-,C) takes each object A of Set (or: an object of Set^op) to a function: TA: (A->P) -> ((A->B)×(A->C)) We will represent this natural transformation T in DNC by just downcasing the triangle: A - - - / | \ v v v (A->P) -> ((A->B)×(A->C)) 12. Translating bigger trees ============================ a,b a,b|-a,b --- -------- a,b a a|-b|->c a,b|-a,b a,b|-a a|-b|->c --- -------------- |---> -------- ------------------- b b|->c a,b|-b a,b|-b|->c -------------- ------------------------ c a,b|-c - - | | v v p a|-f(a) p|-p a|-f(a) -- ---------ren ----- ---------ren p πp πp|-f(πp) p|-p p|-πp πp|-f(πp) --- --------------- |---> ------ ------------------ π'p f(πp) p|-π'p p|-f(πp) ---------------- --------------------- f(πp)(π'p) p|-f(πp)(π'p) id -- id π f -- ------- π' π;f ----------- <π;f,π'>;ev = f^v |