Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
[lua: PAREN3 = lambda("one, two, three", undollar [["\n($one,\n $two,\n $three)\n"]]) TABLE = lambda("text", undollar [["<table>$text\n</table>\n"]]) TR = lambda("text", undollar [["<tr>$text\n</tr>\n"]]) TD = lambda("bg, text", undollar [["<td>$text\n</td>\n"]]) TDBG = lambda("bg, text", undollar [["<td bgcolor=\"$bg\">$text\n</td>\n"]]) FG = lambda("bg, text", undollar [["<font bgcolor=\"$fg\">$text</font>\n"]]) BGBLOCK = lambda("bg, text", [[TABLE(TR(TDBG(bg, text)))]]) QUO = lambda("text", undollar [["\n<blockquote>\n$text\n</blockquote>\n"]]) MATHL = lambda("fname, text", [[HREF("math/"..fname, fname).." "..text]]) mathL = lambda("fname, text", [[HREF("math/"..fname, fname)]]) setgetargs(vargs1, "QUO") setgetargs(vargs2, "TABLE TR TD TDBG FG BGBLOCK MATHL mathL") -- print(2802, mathL, _GETARGS["mathL"]) -- (find-zsh "cd ~/LUA/; lua blogme.lua -o ~/TH/L/math-b.html -i math.blogme") -- (find-shttpfile "www.schemers.org/index.html" "<font color=GREEN>") -- (find-fline "~/TH/L/e/gtk.e.html" "td bgcolor") --22FF22 -- (eev "edrxnetscape ~/TH/L/math.html &" nil) -- (find-es "page" "math.th-files") ] [htmlize [J Eduardo Ochs - Academic Research - Categories, NSA, the "Typical Point Notation", and a language for skeletons of proofs] [J (...quick notes added in 2001dec26; I still haven't had time to glue the pieces together and make a coherent whole. The rest of the page is older.) [HLIST1 [J Some important online texts:] [HLIST2 [J On Category Theory, plus some unclassified things:] [HLIST2 [J Barr/Wells: Toposes, Triples, and Theories (1985):] [LR http://www.cwru.edu/artsci/math/wells/pub/ttt.html] ] [J Phil Scott: [LR http://linear.di.fc.ul.pt/handbook.ps Some Aspects of Categories in Computer Science] (1998/2000; a chapter of the "Handbook of Algebra")] [HLIST2 [J [LR http://www.cl.cam.ac.uk/~amp12/ Pitts]: Categorical Logic (2001):] [LR http://citeseer.nj.nec.com/pitts01categorical.html] [LR http://www.cl.cam.ac.uk/~amp12/papers/] [LR ftp://ftp.cl.cam.ac.uk/papers/amp12/catl.ps.gz] ] [J [LR http://www.mathematik.tu-darmstadt.de/~streicher/ Thomas Streicher]'s notes on [LR http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/fib.ps.gz Fibered Categories à là Jean Bénabou] (1999)] [J Wesley Phoa: [LR http://www.lfcs.informatics.ed.ac.uk/reports/92/ECS-LFCS-92-208/ECS-LFCS-92-208.ps.gz An Introduction to Fibrations, Topos Theory, the Effective Topos and Modest Sets]] [HLIST2 [J Caccamo/Hyland/[LR http://www.cl.cam.ac.uk/~gw104/ Winskel]:] [J [LR http://www.brics.dk/~mcaccamo/catnotes.ps.gz Lecture Notes in Category Theory [' [Draft]] (2001)] [J [LR http://www.brics.dk/RS/01/27/BRICS-RS-01-27.dvi.gz A Higher-Order Calculus for Categories]] ] [LR http://www.math.unipd.it/~maietti/ Milly Maietti's home page] [HLIST2 [J [LR http://www.tcs.informatik.uni-muenchen.de/~mhofmann/papers.html Martin Hofmann]: Syntax and Semantics of Dependent Types (1997):] [LR http://citeseer.nj.nec.com/hofmann97syntax.html] ] [HLIST2 [Q Nordström/Petersson/Smith: Martin-Löf's Type Theory:] [LR http://citeseer.nj.nec.com/1666.html] ] [HLIST2 [J Mark P. Jones: First Class Polymorphism with Type Inference (1997):] [LR http://www.cse.ogi.edu/~mpj/pubs/popl97-fcp.dvi.gz] ] ] [HLIST2 [J On Type Theory (mainly on the Calculus of Constructions):] [HLIST2 [LR http://www.cs.kun.nl/~herman/pubs.html Herman Geuvers]'s... [J PhD thesis, [LR http://www.cs.kun.nl/~herman/Proefschrift.ps.gz "Logics and Type Systems"] (1993), and] [LR http://www.cs.kun.nl/~herman/BRABasSNCC.ps.gz "A Short and Flexible Proof of Strong Normalization for the Calculus of Constructions"] ] [HLIST2 [J Barendregt: Lambda Calculi with Types (1992):] [LR http://citeseer.nj.nec.com/barendregt92lambda.html] [LR ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z] ] [J [LR http://www.dur.ac.uk/zhaohui.luo/ Zhaohui Luo]'s PhD thesis: "[LR http://www.dur.ac.uk/~dcs0zl/THESIS90.dvi.gz An Extended Calculus of Constructions]" (1990).] [J [LR http://home.uleth.ca/~jonathan.seldin/publications.html Jonathan Seldin]'s homepage] [J [LR http://www.cs.chalmers.se/~coquand/ Thierry Coquand]'s homepage] [J Barbanera/[LR http://www.di.unito.it/~stefano/ Berardi]: [LR http://www.di.unito.it/~stefano/Barbanera-ProofIrrelevanceOutOf.ps Proof-Irrelevance out of Excluded Middle and Choice in the Calculus of Constructions]] ] [HLIST2 [J On Parametricity:] [HLIST2 [J Phil Wadler:] [LR http://www.research.avayalabs.com/user/wadler/topics/parametricity.html Theorems for Free! (1989), The Girard-Reynolds Isomorphism (2001)] [LR http://www.research.avayalabs.com/user/wadler/topics/history.html Proofs are Programs: 19th Century Logic and 21st Century Computing] ] [HLIST2 [J John Reynolds:] [LR http://www-2.cs.cmu.edu/~jcr/ On Functors Expressible in the Polymorphic Typed Lambda Calculus] ] [HLIST2 [J Izumi Takeuti:] [J [LR http://www.sato.kuis.kyoto-u.ac.jp/~takeuti/abs-e.html#param An Axiomatic System of Parametricity] (1998)] [J [LR http://www.sato.kuis.kyoto-u.ac.jp/~takeuti/abs-e.html#cube The Theory of Parametricity in Lambda Cube] (draft)] ] [HLIST2 [J Harry Mairson:] [LR http://www.cs.brandeis.edu/~mairson/Papers/para.ps.gz Outline of a Proof Theory of Parametricity] ] ] [HLIST2 [J On Non-standard Analysis, SDG and friends:] [LR http://members.tripod.com/PhilipApps/nonstandard.html A page with many links on Non-Standard Analysis] [HLIST2 [LR http://www.acsu.buffalo.edu/~wlawvere/ William Lawvere]: [J [LR http://www.acsu.buffalo.edu/~wlawvere/SDG_Outline.pdf Outline of Synthetic Differential Geometry] (1998)] [J [LR http://www.acsu.buffalo.edu/~wlawvere/ToposMotion.pdf Toposes of Laws of Motion] (1997)] ] [J [LR http://www.math.uu.se/~jonase/ Jonas Eliasson] seems to be working on the relation between toposes of filters and toposes of ultrafilters; he makes reference to some [LR http://www.math.uu.se/~palmgren/publicat.html papers by Erik Palmgren] that are not on-line.] [J [LR http://iml.univ-mrs.fr/~ehrhard/pub.html Thomas Ehrhard]: [LR ftp://iml.univ-mrs.fr/pub/ehrhard/difflamb.ps.gz The Differential Lambda-Calculus] (2001).] [HLIST2 [LR http://home.imf.au.dk/kock/ Anders Kock]: [J [LR http://www.tac.mta.ca/tac/volumes/1999/n10/n10.ps Aspects of Fractional Exponent Functors] (1999, with G. Reyes)] [J [LR ftp://ftp.imf.au.dk/pub/kock/ODE5.ps Fractional Exponent Functors and Categories of Differential Equations] (1998, with G. Reyes)] ] [J [LR http://www.brics.dk/~butz/ Carsten Butz]: [LR http://www.brics.dk/~butz/public_ftp/new_stuff/filter.ps.gz The filter construction revisited] ] ] ] [P Citeseer search: [LR http://citeseer.nj.nec.com/cs/]] [P HPSearch: [LR http://hpsearch.uni-trier.de/]] [P [LR http://www.cs.uu.nl/people/franka/ref Frank Atanassow's list of online Programming Language Theory texts]] [RULE] [P News, 2002may17: I'm not having enough time to update this page -- I'm spending 8 months doing research at [LR http://www.math.mcgill.ca/ McGill University], working with [LR http://www.math.mcgill.ca/~rags/ Robert Seely], with a [LR http://www.capes.gov.br/ CAPES]'s [LR http://www.capes.gov.br/Bolsas/Exterior/Doutorando.htm "Sandwich PhD"] grant, and besides the academic side there are also hundreds of things happening wite my on a personal level, I'm sort of leaving my tadpole stage -- and my newest sets of notes are too messy, and many important parts of them are not TeXed yet... but, just to give an idea of what I've been working on, here's the abstract for a presentation that I'll be giving at the [LR http://cs.colgate.edu/faculty/mulry/FMCS2002/Web/FMCS2002.html FMCS2002] in early June:] [P --snip--snip--] [P Title: A System of Natural Deduction for Categories] [P We will present a logic (system DNC) whose terms represent categories, objects, morphisms, functors, natural transformations, sets, points, and functions, and whose rules of deduction represent certain constructive operations involving those entities. Derivation trees in this system only represent the "T-part" (for "terms" and "types") of the constructions, not the "P-part" ("proofs" and "propositions"): the rules that generate functors and natural transformations do not check that they obey the necessary equations. So, we can see derivations in this system either as constructions happening in a "syntactical world", that should be related to the "real world" in some way (maybe through meta-theorems that are yet to be found), or as being just "skeletons" of the real constructions, with the P-parts having been omitted for briefness.] [P Even though derivations in DNC tell only half of the story, they still have a certain charm: DNC terms represent "types", but a tree represents a construction of a lambda-calculus term; there's a Curry-Howard isomorphism going on, and a tree can be a visual help for understanding how the lambda-calculus term works -- how the data flows inside a given categorical construction. Also, if we are looking for a categorical entity of a certain "type" we can try to express it as a DNC term, and then look for a DNC "deduction" having it as its "conclusion"; the deduction will give us a T-part, and we will still have to go back to the standard language to supply a P-part, but at least the search has been broken in two parts...] [P The way to formalize DNC, and to provide a translation between terms in its "logic" and the usual notations for Category Theory, is based on the following idea. Take a derivation tree D in the Calculus of Constructions, and erase all the contexts and all the typings that appear in it; also erase all the deduction steps that now look redundant. Call the new tree D'. If the original derivation, D, obeys some mild conditions, then it is possible to reconstruct it -- modulo exchanges and unessential weakenings in the contexts -- from D', that is much shorter. The algorithm that does the reconstruction generates as a by-product a "dictionary" that tells the type and the "minimal context" for each term that appears in D'; by extending the language that the dictionary can deal with we get a way to translate DNC terms and trees -- and also, curiously, with a few tricks more, and with some minimal information to "bootstrap" the dictionary, categorical diagrams written in a DNC-like language.] [P --snip--snip--] [P I'll also be giving a slightly shorter version of that talk at the [LR http://www.cms.math.ca/Events/summer02/ CMS Summer 2002 Meeting], in mid-June.] [P I believe that the essential details (i.e., the "T-part") of a certain construction of a categorical model of the Calculus of Constructions fit in a few DNC diagrams, but my work on that is far from finished :(.] [RULE] [P I am currently finishing the second year of my PhD on Mathematics, at PUC-Rio, in Rio de Janeiro, Brazil. My work revolves around trying to explain two "facts":] [P 1) Some Calculus proofs involving infinitesimals, that apparently would need either Non-Standard Analysis or Synthetical Differential Geometry ("NSA" and "SDG", from now on) to be formalized, can be translated into completely formal standard proofs --- where the arguments about infinitesimals become standard arguments about limits and continuity --- via a ridiculously simple trick whose central step is to reread the "skeleton" of the proof in a certain filter-power of the standard universe, instead of using a ultrafilter-power. These proofs are certainly happening in a fragment of the usual logic; but which fragment?] [P 2) Proofs in category theory often also admit "skeletons"; VERY roughly, the "skeleton" of a proof is a tree or diagram that encodes the way of constructing the intermediate objects used in the proof; by squeezing these trees or diagrams just a bit we can derive some "natural properties" of the intermediate objects, and the original statement we wanted to prove turns out to be an easy consequence of these natural properties... That is, each such proof can be reduced to a construction plus some trivial checkings; once the construction is given it is possible to say "then it is obvious that xxx happens", and a reader (or an automated reasoning system, working on a small search space) should be able to fill up the missing details very quickly; that is, we will have a language where certain uses of "it is obvious that ..." will have a formal meaning, and in this language the skeletons of proofs [IT are], modulo the last "it is obvious that", real proofs. Moreover: if we define an "easy" proof as being a proof that admits a "decent" skeleton (this must be formalized, of course) then what I hope to be able to claim is this: [IT a significant part of topos theory is "easy"]. Corollary: a topos semantics for the language with infinitesimals mentioned above is "easy to understand", and basic topos theory can be presented in a much simpler way; it certainly doesn't need to be the bugaboo that students usually think it is.] [P I know that these topics may sound at the same time too pretentious and too basic -- especially the language for proofs in categories --, but I think that I have a pretty good reason to work on that: I'm using the typical point notation to simplify category theory for myself... many important objects of topos theory can be named in typical point notation just by their types, without having to be preceded by long chains of definitions, and many questions about natural objects become even more natural; for example, if we are told that there is an adjunction between the functors L and R we may try to write down the "names" of two morphisms aL->b and a->bR and then try to see if they "carry the same information", i.e., if regarding them as programs (think in lambda-calculus) we can convert one into another, and back. Also, it must be possible to construct the units and counits a->aLR and bRL->b of the adjunction "from nothing", and so on. Note: I still don't have a good notation for terms (only for types right now) and so it is generally better to use the standard notation to reason about reductions; however in my notes (links below) I have some examples of translations between TP and standard notations, and of using the TP notation to draw diagrams.] [P An example of a diagram extracted from the proof in TP notation that a functor that is a right adjoint preserves limits (pullbacks in this case, and yes, the explanations [IT are] missing).] [IMAGE IMAGES/preslim.png (right adjoints preserve limits)] [P [Q [J You can pick a copy of my notes on the "typical point notation" from the links below (2001a was last updated in 2001jan30, 2001b in 2001mar07, 2001c in 2001may07):]]] [P Be warned that these notes are in a quite preliminary form: some sections end abruptly, others do not exist, and the formatting is very bad. Nevertheless, the main ideas are quite clear (I hope!), at least in 2001a and 2001c.] [LIST1 [J [L math/2001a-dvi.tgz 2001a-dvi.tgz] (dvi plus .eps files)] [J [L math/2001a-dvi.zip 2001a-dvi.zip] (dvi plus .eps files)] [J [L math/2001a.ps.gz 2001a.ps.gz] (postscript, 600dpi)] [J [L math/2001a-ps.zip 2001a-ps.zip] (postscript, 600dpi)] ] [P You almost certainly don't want to download 2001b: it contains some early notes about "basic topos theory being easy" and about natural deduction in arbitrary categories and in topoi, but everything is messy, obscure and wrong. If you print it I'll have to deny that I wrote it; previewing is OK, though, but will probably be a waste of time.] [LIST1 [J [L math/2001b-dvi.tgz 2001b-dvi.tgz] (dvi plus .eps files)] [J [L math/2001b-dvi.zip 2001b-dvi.zip] (dvi plus .eps files)] [J [L math/2001b.ps.gz 2001b.ps.gz] (postscript, 600dpi)] [J [L math/2001b-ps.zip 2001b-ps.zip] (postscript, 600dpi)] ] [P 2001c contains the "real" notes about a system of natural deduction for categories, and how we can use this system to define what is a "syntactical" (or "easy") categorical proof; some examples of things that have syntactical proofs are the Yoneda lemma and the fact that a Set^C has exponentials and a classifier object.] [LIST1 [J [L math/2001c-dvi.tgz 2001c-dvi.tgz] (dvi plus .eps files)] [J [L math/2001c-dvi.zip 2001c-dvi.zip] (dvi plus .eps files)] [J [L math/2001c.ps.gz 2001c.ps.gz] (postscript, 600dpi)] [J [L math/2001c-ps.zip 2001c-ps.zip] (postscript, 600dpi)] ] [P I'll be presenting a (much cleaner!) version of these ideas in July 5, at a meeting called [L http://www.inf.puc-rio.br/nd/program_i.html Natural Deduction Rio 2001]. Here is the abstract (3 pages and a bit):] [LIST1 [J [L math/2001nd-abs.dvi.gz 2001nd-abs.dvi.gz] (dvi)] [J [L math/2001nd-abs-dvi.zip 2001nd-abs-dvi.zip] (dvi)] [J [L math/2001nd-abs.ps.gz 2001nd-abs.ps.gz] (postscript, 600dpi)] [J [L math/2001nd-abs-ps.zip 2001nd-abs-ps.zip] (postscript, 600dpi)] ] [P Coming soon: a bibliography and many more translations between the typical point notation and the more usual ones (MacLane, [LR http://www.cwru.edu/artsci/math/wells/pub/ttt.html Barr and Wells], Goldblatt, Lambek and Scott). Some months ago I translated most of chapter 0 of Lambek and Scott's book into an older form of the TP notation and TeXed the diagrams; the result is mostly unreadable but I'm hoping to reuse some diagrams later, especially from the part on monads. If you are me then you may want the links: [mathL tp-dvi.tar.gz]/[mathL tp-dvi.zip], [mathL tp-ps600.ps.tar.gz]/[mathL tp-ps600.ps.zip].] [RULE] [P [IT (This is the older informal abstract; I will soon cannibalize the good parts of it into the other and delete the rest.)]] [QUO [P [Q There is a class of proofs involving infinitesimals -- and this class is large enough to be interesting, as it contains most "straightforward calculations with infinitesimals" -- that can be translated to standard proofs in terms of continuity and limits via a surprisingly simple trick: reread these proofs in $Set^F$ (the power of the standard universe by a filter, instead of using an ultrafilter), with $F$ being a filter of (maybe punctured) neighbourhoods of the "zero" point of a certain topological space; then instead of choosing arbitrary infinitesimals where the statements say "for all infinitesimals $epsilon_1$, $epsilon_2$, ...", take only the "natural" (or "universal") infinitesimals induced by the filter $F$; then reread that in $Set$, which is trivial because a filter-power by a filter of neighbourhoods can be easily described in elementary terms. ]] [P [Q This works because these proofs are happening in a fragment of the logic of $Set^F$ that "doesn't notice" the non-two-valuedness of the logic of $Set^F$; and what is even more interesting is that we can put these proofs in a form --- a sort of Curry-Howard isomorphism for calculus with infinitesimals --- that depicts in a nice way and in tree form the constructions and logical steps involved, and that can be considered as the "skeletons" of the proofs; these skeletons can be not only used to translate the proofs to several more usual languages, but also to discover how to relax hypotheses ("this function can be just $C^4$ instead of $C^infty$", for example) and also lets us suppress most parameters of functions (as they can be inferred from the tree) and discuss coherence questions for Calculus and Differential Geometry (like "in this situation all natural ways to obtain $dw/dx$ are equivalent"); if this system can be made to work in full strength then we should hope to be able someday to devise an algorithm that would understand the notation that physicists and applied mathematicians use, and to convert it to skeleton form or to put back the omitted variables. ]] [P [Q Then comes the categorical side of these ideas. ]] [P [Q What are the precise syntax, the logical properties and the interesting semantics of the system where these proofs with infinitesimals lie? I don't have any good answer for these questions right now, but it seemed that the natural way to go was to pick some interesting examples and try to interpret them on a topos; I started to create a sort of notation of typical points for categories -- mainly to let me get more intuition about how things work on a topos -- and it turned out that many categorical concepts could be expressed very elegantly in this notation, as the language is built from the start to make easy to express things like "then there is exactly one natural arrow from x to y"; also, statements in that language lead to diagrams quite easily, and I have a strong impression (based on tests with friends) that this language is very good for dydactical purposes; an algorithm to translate from this language to the usual ones and back would then be useful not only to formalize skeletons of proofs with infinitesimals via a categorical setting, but also to discuss skeletons of categorical proofs. ]] ] [RULE] [P (Sorry for any incorrections, I will fix them as soon as I can...)] [P] [J The next block contains links to older texts in portuguese.] [RULE] [P (Aviso: [Q eu gerei os ".ps"s em 600 dpi e só usei gzip e tar pra comprimir e empacotar, se alguém precisar de outra resolução ou de pacotes feitos de outra maneira, mande um mail.])] [P Minha [MYLBYTES math/tese-mestr.tgz tese de mestrado] (apresentada e defendida em abril de 99) [Q é sobre formalizar "demonstrações-rabisco" envolvendo infinitesimais; em termos mais conhecidos, ela trata de lambda-cálculo, categorias, dedução natural, intuicionismo, isomorfismo de Curry-Howard... enfim, tudo o que é necessário para levar um matemático a entender análise não-standard através de sistemas de tipos, e a ver o que está por trás de uma certa tradução entre uma versão de análise não-standard que usa filtros no lugar de ultrafiltros e análise convencional. Como eu não consegui completar a tempo os últimos capítulos (ambiciosíssimos - eu ainda estou pesquisando parte do material que eu imaginava que iria pôr neles), que são sobre topoi, sobre "onde nós gostaríamos de chegar" e sobre análise não-standard, eles tiveram que virar umas espécies de apêndices com anotações informais, mas mesmo assim a tese foi muito bem aceita. Dê uma olhada pra entender por quê!]] [P [MYLBYTES math/slides-mestr.tgz [Q As transparências que eu usei na defesa da tese de mestrado.]]] [P [MYLBYTES math/00feb24.dvi [Q As transparências que eu usei na minha apresentação no Encontro de Lógica da UFF, em 24 de fevereiro de 2000, sobre o mesmo assunto, mas com ênfase na tradução de contas semi-standard (i.e., "não-standard com filtros") para standard.]]] [P [MYLBYTES math/99sep25.dvi [Q Notação mais curta para as regras de lógica linear, abreviando os contextos muito mais do que o normal.]] [Q (Usei os símbolos do Troelstra pros conectivos)]] [RULE] [HLIST1 [Q A few links:] [LR http://xxx.lanl.gov/] [LR http://hypatia.dcs.qmw.ac.uk/] [LR http://citeseer.nj.nec.com/] [LR http://theory.stanford.edu/~selinger/people.html] [LR http://saturn.umh.ac.be/~maesa/nicolas.htm [Q Le petit Nicolas en thèse]] ] ]]] [# # [P I've been writing some notes in English about all that I've been # studying on the \"Typical Point Notation\" -- a system that started as # a sort of Curry-Howard isomorphism for differential calculus, and that # gave as by-products: 1) a fragment of non-standard analysis where # filters suffice (instead of requiring ultrafilters) and where # translation to standard analysis is immediate, and 2) a notation for # categories in which coherence conditions become very easy to state and # many important concepts can be expressed very elegantly.] # # [P I have split my notes in two parts: one part is about the # \"Calculus\" side (which includes non-standard analysis with filters) # and the other is about the \"Categories\" side. You can get them (both # parts) by downloading any one of the four files below:] # # [LIST2 # [MATHL tp-dvi.tar.gz (~ 69720 bytes)] # [MATHL tp-dvi.zip (~ 128041 bytes)] # [MATHL tp-ps600.ps.tar.gz (~ 163027 bytes)] # [MATHL tp-ps600.ps.zip (~ 162774 bytes)] # ] # # [P They correspond to the version of [FG purple November 6, 2000]]. # # [P Be aware that this material is not yet ready to be announced at any # serious place: there are some sections that have been fully written # and that should be very clear (I hope) but there are others that at # this moment are just horrible drafts. Please preview on your screen # before printing.] ]