Eduardo Ochs - Academic Research - Categorical Semantics, Downcasing Types, Skeletons of Proofs, and a bit of Non-Standard AnalysisQuick index:
On some missing diagrams in the ElephantAt this moment this is a 12-page extended abstract (also here with darker fonts) that I submitted to ACT2019, that will happen in Oxford in mid-july. The extended abstract's abstract is:
I presented it in the poster session on tuesday 16/jul.
See the "Planar Heyting Algebras for Children" series. Notes on the Yoneda Lemma
Slides. Work in
progress, about 90% ready.
I am trying to implement this in a proof assistant -
An introduction to type systems (and to the "Logic for Children" project)This is going to be a series of videos, but I am still
working on the slides... work in progress!
I almost gave a presentation about the part on types at IFCS in 2019jun18, but Jean-Yves Beziau forgot to pick up the projector from the secretary's drawer in the morning... she left everything locked, went out for lunch and only returned many, many hours later. Five applications of the "Logic for Children" project to Category TheoryA talk that I gave at the EBL2019 in 2019may09. Its abstract is here. My plans for this talk were very ambitious: I wanted to present the main ideas, motivations and constructions of PHAfC 1, 2 and 3 and Logic for Children in 20 minutes, with lots of figures... but when it was my turn to present all the people who knew a bit of Category Theory were in another room, attending a session with technical talks, and I did not have the 5 or 6 slides that I could have made my talk more accessible to an audience of philosophers. I failed miserably. Slides.Ensinando Matemática Discreta para calouros com português muito ruim I organized a round table about how to teach Logic
to undergraduates in the EBL2019.
How to almost teach Intuitionistic Logic to Discrete Mathematics Students *
A talk in the World Logic
Day - 2019jan14 - in Rio de
Janeiro, about:
Dednat6: an extensible (semi-)preprocessor for LuaLaTeX *
A talk at TUG2018, in Rio de
Janeiro, in 2018jul20 about
the package that I use to typeset several kinds of
diagrams.
Logic for Children (workshop at UniLog 2018) *
I organized (with Fernando Lucatelli) a workshop called "Logic for Children" that
happened at the UniLog 2018 in
Vichy, France, in june 24, 2018.
Visualizing Geometric Morphisms (talk at UniLog 2018)
A talk given at the workshop "Categories and Logic" in the
UniLog 2018 in june 22, 2018.
Planar Heyting Algebras for Children (2017-) *Finite planar Heyting Algebras ("ZHA"s) are very good tools for teaching Heyting Algebras and Intuitionistic Propositional Logic to "children"; "children" here means "people without mathematical maturity", in the sense that they are not able to understand structures that are too abstract straight away, they need particular cases first. This is going to be a series of three papers.
My submission to the ACT2019,
"On some missing diagrams in the
Elephant", is currently the best presentation of the material in
the third paper.
When I present this to "real" children who don't know lambda notation we go through this material first. The first paper (current working version).
Notes on notation (2017)"Different people have different measures for "mental space"; someone with a good algebraic memory may feel that an expression like [...] is easy to remember, while I always think diagramatically, and so what I do is that I remember this diagram [...] and I reconstruct the formula from it." (IDARCT) These are very informal notes showing my favourite ways to draw the "missing diagrams" in MacLane's CWM, and my favourite choice of letters for them. Work in progress changing often, contributions and chats welcome, etc. My plan is to do something similar for parts of the Elephant next. A skeleton for the Yoneda Lemma (PDF).
IPL For Children and Meta-Children, or: How Archetypal Are ZHAs? (2017)
This is a 20-minute talk that I gave in the
EBL2017 in 2017may09.
Lambda-calculus, logics and translations (course, 2016-)In 2016 I started giving a very introductory course on lambda-calculus, types, intuitionistic propositional logic, Curry-Howard, Categories, Lisp and Lua in the campus where I work. The course is 2hs/week, has no prerequisites at all, has no homework, and is usually attended by 2nd/3rd semester CompSci students; they spend most of their time in class discussing and doing exercises together in groups on a whiteboard. I have LaTeXed a part of the material; it's here. For bibliography, images of the whiteboards, etc, go here. Intuitionistic Logic for Children, or: Planar Heyting Algebras for Children (2015)
Seminar notes, with lots of figures (all drawn with Dednat6).
Logic and Categories, or: Heyting Algebras for Children (2015)
A tutorial presented at the UniLog 2015 conference (Istanbul), 20-22/jun/2015.
Sheaves for children (2014)A 20-minute talk - here are its slides - presented at the XIV EBL, on 2014apr09. Its abstract:
The second - and much longer - version of this talk (at the Seminário Carioca de Lógica, 2014may19, 15:00, IFCS) had these slides and these handouts, and was meant for much younger "children". The focus this time was a visual characterization of the subsets of N^{2} that are Heyting Algebras, and how can we treat their points as truth-values, and so how to interpret intuitionistic logic on them. I call these subsets "ZHAs", the definitions and main theorems for them are in the pages 20 to 27 of the slides, and also at the handouts. Sheaves on Finite DAGs may be Archetypal (2011)Can the ideas of my article about "internal diagrams" be used to present the basic concepts of toposes and sheaves starting from simple, "archetypal" examples? I believe so, but this is still a work in progress! Here are 7 pages of very nice handwritten notes (titled "Sheaves for Children"): pdf, djvu. They were written after discussions with Hugo Luiz Mariano and Claus Akira Matsushige Horodynski in feb/2012, during a minicourse on CT in Brasilia organized by Claus, with me and Hugo as lecturers... ...and here are some slightly older notes - I submitted them, in a admittedly incomplete form, to the XVI EBL, with this abstract - and then I did a bad job at presenting them; here are the slides, they cover only the first ideas =(. For the sake of completeness, here are some handwritten diagrams describing Kan extensions in an (hopefully) archetypal case, motivated by discussions with G.F. Lima: 1200dpi djvu, 600dpi djvu, 600dpi pdf. Internal Diagrams in Category Theory (2010/2013) *A paper submitted to Logica Universalis, and published in their special issue on Categorical Logic in 2013, with a longer name: "Internal Diagrams and Archetypal Reasoning in Category Theory". Its abstract:
The paper was produced from the material that I created for the talk below. The slides covers much more ground, but the paper explains the ideas much more clearly. The revised version (2013), that has more sections and more words in the title: "Internal Diagrams and Archetypal Reasoning in Category Theory" (if you prefer a .dvi, it needs this .eps). The original version (just "Internal Diagrams in Category Theory", 2010) is here. (2013) Internal Diagrams and
Archetypal Reasoning in Category Theory
Downcasing Types (at UniLog'2010)I gave a talk about Downcasing Types at the special session on Categorical Logic of UNILOG'2010, on 2010apr22. Very few people attended - because the volcanic ashes many people could not fly to Portugal, and from all these programmed talks only these ended up happening. The abstract was:
(A longer version of the abstract: pdf.) First official release of the slides (2010jun21, 100 pages): pdf. Latest version of the slides (109 pages): dvi, pdf. Some related posts at cat-dist:Natural infinitesimals in filter-powers (2008)"Purely calculational proofs" involving infinitesimals can be "lifted" from the non-standard universe (an ultrapower) to the "semi-standard universe" (a filter-power) through the quotient Set^{I}/F→Set^{I}/U; and after they've been moved to the right filter-power they can be translated very easily to standard proofs. I don't know how much of this idea is new, but I liked it so much that I wrote it down in some detail and asked for feedback in the Categories mailing list.
Preliminary version (2008jul13), including the message to the mailing list: pdf, dvi, source. A (long-ish) abstract for a presentation intended for undergrads:
pdf,
source.
(News: Reinhard Boerger pointed me to later (post-1958) work by Laugwitz and Schmieden, and I got a copy of the "Reuniting the Antipodes" book; my current impression is that my result is not as trivial as I was afraid it could be. Homework-in-progress: several cleanups on the preliminary version above, and I'm trying - harder - to understand Moerdijk and Palmgren's sheaf models.) Note (2010): I still don't have the tools for formalizing this idea completely. As what I have is an "incomplete internal language", the ideas in this preprint may help. Sheaves for Non-Categorists (2008)This is another presentation that - maybe after some clean-ups - will be accessible to undergrads... The current version of the slides (far from ready, with lots of garbage and gaps!) is here: pdf, source. The presentation will be at the Logic Seminar at UFF, on 2008sep04, 16:00-17:00hs. Here's an htmlized version of the abstract:
Seminar on downcasing types (nov/2007)If you are going to attend my seminars at PUC at November/2007 and want to take a peek at my notes (they are very incomplete at the moment, it goes without saying), they have just been split into several parts:
Bad news (?), dec/2007: the seminars will not happen - instead, I got a job at São Paulo, on computer stuff. I'll keep working on maths and on my personal free software projects in my spare time. If you find any of these things interesting, and want to discuss or to encourage me to finish something, get in touch! 2008: I am giving a series of seminars at UFF to try to organize my ideas about downcasing types... here are links to some of TeXed slides (they are very preliminary, too. Should I be embarassed to provide links to these things? Well...): General links
Some articles and books that I'm reading:
Category Theory (in general):
Fibrations:
Monads:
Sheaves:Type Theory (mainly the Calculus of Constructions):
Parametricity:Non-standard Analysis, SDG and friends:
Natural Deduction:Grothendieck:
Etc (unclassified):
Links to the home pages of some category theorists (and a few type theorists): Abadi, Abramsky, Aczel, Adamek, Altenkirch, Aspinall, Atanassow, Avigad, Awodey, Baez, Barendregt, Barr, Bauer, Beeson, Bell, Berardi, Berg, Birkedal, Blass, Blute, Brown, Bunge, Butz, Caccamo, Cockett, Coquand, Crosilla, Dawson, DePaiva, Diaconescu, Dosen, Dybjer, Egger, Ehrhard, Escardo, Fiore, Funk, Gaucher, Geuvers, Girard, Grandis, Gurevich, Hasegawa, Hermida, Hofmann, Hofstra, Honsell, Hyland, Jacobs, Jardine, Jibladze, Joyal, Kock, Koslowski, Lack, Lamarche, Lambek, Laurent, Lawvere, Leinster, Levy, Longo, Luo, MPJones, Maietti, Mairson, Makkai, Marcos, McLarty, Maltsiniotis, Milner, Mislove; Moerdijk, Moggi, Nelson, Negri, Niefield, Palmgren, Pare, Pastro, Pavlovic, Petric, Phoa, Pierce, Pitts, Plotkin, Porter, Pratt, Pronk, Queiroz, Regnier, Reynolds, Rosebrugh, Rosolini, Sambin, Scedrov, Schalk, Schuster, Scott, ScottD, Seely, Seldin, Selinger, Simmons, Simpson, Spitters, Street, Streicher, Taylor, Tholen, VanOosten, Vickers, Wadler, Weirich, Wells, Wiedijk, Winskel, Wood, Wraith, Yanofsky. PhD and post-PhD research *I did both my MsC and my PhD (and also my graduation, by the way) at the Department of Mathematics at PUC-Rio. The Dept of Mathematics is a fantastic place - tiny, incredibly friendly, well-equipped, lots of research going on -, but (rant mode on) PUC-Rio is a private university, and most of the students from other departments were ultra-competitive rich kids who had never stepped out of the marble towers they live in. I used to find it very hard - very painful, even - to interact with them, and even to stand their looks, like if they were always trying to tag me as either a "winner" or a "loser", as if there weren't any other ways to live. Eeek! But these days are long gone now (rant mode off). I spent the first eight months of 2002 at McGill University in Montreal, doing research for my PhD thesis there, working with Robert Seely... I was in a "Sandwich PhD" program (thanks CAPES!), which is something that lets us do part of the research abroad and then come back and finish (and defend) the thesis at our university of origin. I defended my PhD thesis (with a few holes) in August, 2003 and presented the final version - filling out most of the gaps - in February, 2004. Then I spent most of 2004 teaching part-time in an university at the outskirts of Rio (the more realworldish job that I've ever had!), and also finishing a very important Free Software project that I've been working on since 1999 (GNU eev). The thesis is in Portuguese and you don't want to see it - you want to see the slides that I'm working on (it's 2005mar12 as I write this), in which the method for interpreting diagrams and "lifting" them from Set to an arbitrary category with the adequate structure in explained in a really nice way. But if you are really anxious you can get in touch with me. News (October 2005): I'm giving a series of talks about my PhD thesis at UFF (see http://www.uff.br/grupodelogica/). Expect slides soon and articles not so soon, but as soon as possible. News (2010/2013): this paper has all the ideas from my PhD thesis, plus some! It fills all the gaps from the thesis, and it is quite well written =). This is the abstract for a talk that I gave at the FMCS2002 in June 8, 2002.
I also gave a shorter version of that talk at the CMS Summer 2002 Meeting, in June 17. Slides for the longer talk (45 minutes, 26+3 pages): pdf, ps, dvi, source. Slides for the shorter talk (one week later, 15 minutes, 16+2 pages: pdf, ps, dvi, source. Fact: all the essential details (i.e., the "T-part", as in the abstract above) of a certain construction of a categorical model of the Calculus of Constructions - and also of categorical models of several fragments of CC - can be expressed in (a few!) categorical diagrams using the DNC language. I'm currently (February/March 2005) preparing talks and articles about that. An older talk about Natural Deduction for Categories. After using something like the DNC notation for years just because "it looked right", but without any good formal justification for it, in February 2001 I had the key idea: there were rules of both discharge and introduction for the "connectives" for functors and natural transformations. A few months after that (in July 5 2001, to be precise) I gave a talk about it at a meeting called Natural Deduction Rio 2001. Abstract (3 pages and a bit): pdf, ps, dvi, source. Slides (16 slides): pdf, ps, dvi+eps's, source. Another talk, even older, about Natural Deduction for Categories. After finding the key idea that I mentioned above I arranged to give a (very informal) talk at the Centro de Lógica e Epistemologia at UNICAMP. It happened in April 25, 2001, and for it I had to assemble my personal notes into something that could be used as slides. The title was ""Set^C is a topos" has a syntactical proof". The notes from which the slides were made: ps, dvi+eps's, source. MsC Thesis and related things *My master's thesis: "Categorias, Filtros e Infinitesimais Naturais" (April, 1999). The thesis and the slides used in the defense are in Portuguese. Thesis (7+116 pages): ps, pdf, dvi+eps's, source. Slides (15 slides): ps, pdf, dvi+eps's, source. The diagrams were made with diaglib and the deduction trees with dednat.icn. A few months after the defense (in February 24, 2000, to be precise) I gave a talk at UFF about a kind of "Nonstandard Analysis with Filters", and about skeletons of proofs. Slides (12 slides plus one page), in Portuguese: pdf, ps, dvi+eps's, source. My advisor at PUC: Nicolau Saldanha Typesetting categorical diagrams in LaTeX2017set19: update: since mid-2015 I'm using Dednat6, LuaLaTeX and pict2e for all my diagrams. My PhD thesis included lots of hairy categorical diagrams, and I ended up writing a LaTeX preprocessor in Lua to help me typeset them. Currently (March 2005) I'm trying to pack that preprocessor and document it; its README is still horribly incomplete. The source code for the examples below is here.
Technical information: this page was made with blogme; the source is here. I access local copies of papers with the functions defined in my .emacs.papers. The diagrams were made by processing this file (oops, which?) with dednat4, then viewing the resulting dvi file with xdvi and taking screenshots with Xscreenshot-rect. |