Last week I had the great pleasure of visiting the amazing PL group at Indiana University. They are doing so much inspiring research in many different areas of programming languages research. It was great. The collective knowledge there was very impressive, and I got a lot of great references to follow up on now that I am back.
I gave two talks: one in the logic seminar, and one for the PL group. In the first talk, one issue I was discussing was an argument, originally sketched by Michael Dummett and developed more fully by Charles Parsons in a paper called “The Impredicativity of Induction” (you can find a revised version of this paper in a book called “Proof, Logic, and Formalization” edited by Michael Detlefsen) — this argument claims to show that induction is impredicative. Impredicativity, as many QA9 readers well know, is the property of a definition D of some mathematical object x that D refers to some collection or totality of which x is a member. Philosophical constructivists must reject impredicative definitions, because they believe that the definition are constructing or creating the entities defined, and hence cannot presuppose that those entities already exist in the course of defining them. This kind of philosophical constructivism must be distinguished from a kind of formal constructivism a type theorist is likely to care about, which I identify with a canonical forms property: every inhabitant of a type A should have a canonical form which is part of the essential nature of type A. Computational classical type theory violates this formal canonicity property, because types like are inhabited by terms which are neither left nor right injections.
Here is Parsons’s argument as I understand (or maybe extrapolate?) it. A philosophical constructivist must reject impredicative definitions, such as the kind one gives for the natural numbers in second-order logic (see my talk slides for this example definition). As an alternative, one may try to say that the meaning of the natural number type is determined by introduction and elimination rules (similarly to the meanings of logical connectives). The introduction rules are about the constructors of the type. And the elimination rule is an induction principle for the type. But then, Parsons and Dummett point out, this explanation of the natural number (or other) inductive type is not any better off with respect to impredicativity than the second-order definition, because the induction principle allows us to prove any property P of n, assuming as premises that Nat n holds and that the base and step cases of induction are satisfied for P. But the predicate P could just as well be Nat itself, or some formula which quantifies over Nat. The latter seems to provoke worries, which I do not understand. It seems already bad enough that P could be Nat. So just moving from a single formula defining Nat to a schematic rule defining Nat cannot save one from the charge of impredicativity. Hence, for avoiding impredicativity, there is no reason to prefer one approach (specifically, the rule-based approach) over the other.
The alternative to this is to reject the idea that we must give a foundational explanation of the natural-number type (or predicate). We just accept the idea of numbers and other datatypes as given, and then induction is a consequence — not part of some definition of numbers, which we are refusing to give. This is a coherent way to avoid impredicativity, but at the cost of having to accept numbers with no deeper analysis — something that a logicist might not like, for example (though I do not know for sure how a logicist would likely view this situation).
I am giving a talk this afternoon titled “From Logic with Love” as part of a special class organized by U. Iowa English Prof. Judith Pascoe, where professors from different departments give talks from the perspective of their discipline on the topic “What We Talk About When We Talk About Love”. The slides are here. I am also including some links and notes below, for students interested in further reading.
The short story Beginners, by Raymond Carver, can be found here. This is the original version of the story that was published as “What We Talk About When We Talk About Love”.
Ray Monk’s biography of Bertrand Russell, while loathed by admirers of Russell, is extremely interesting and revealing reading.
Constance Reid’s biography of David Hilbert is also very interesting and enjoyable reading. It includes a reprint of much of the text of his famous 1900 Paris lecture on future problems of mathematics.
Some Computer Science news articles related to the talk:
Other related articles:
A Man For Others by Patricia Treece is an excellent read about Maximilian Kolbe. It contains first-hand reports and recollections from many different people who knew the saint.
I am driving over this morning to the Computer and Information Sciences department at St. Ambrose University in nearby Davenport, Iowa, to give a brief talk (slides here) and talk to students and faculty about graduate study at The University of Iowa.
[Updated after my visit:] I had a great trip over to St. Ambrose CS. I was very warmly greeted by professors Kevin Lillis, Mark McGinn, and Gary Monnard, as well as a very nice turnout of undergraduates (30?) interested in learning a bit more about University of Iowa graduate programs in CS. I also did tell them a bit about some of our group’s research. My impression was that many students already have great jobs lined up for after college, and the costs of further study are perceived as a major impediment. Now we have a great situation here at Iowa, where we have enough external grant funding and internal funding through fellowships and teaching assistantships that certainly for doctoral study, and even for Master’s study for strong students, graduate study will not cost anything for the student, and they’ll even get a stipend. This is standard, of course, at most research departments, but I think the word is not out to undergraduates about this. It may take some time to change people’s knowledge of the graduate-education system.
Anyhow, I had a great time talking with Kevin, Mark, and Gary, and learning more about St. Ambrose. The school has around 3300 (full-time equivalent) students, of whom around 2600 are undergraduates. I got the impression that most are from Davenport or nearby, with a significant percentage of nontraditional (age) students and commuters who don’t live on campus. The CS department has something like 80 students in a number of different majors the department offers. The campus itself is very nice: it occupies something like a 4-block by 4-block square in Davenport. The building we were in for my talk, the Rogalski Center, is very nice and quite new. Kevin walked me around campus, including the lovely chapel; there was a beautiful Madonna and Child by Fr. Catich, founder of the art department at St. Ambrose and known for beautiful art works on slate of religious scenes (like this).
Our department has sent faculty out to I think it is 8 or 9 colleges in the region this fall, to try to increase our domestic applicant pool for graduate study. I very much hope this succeeds — that’s the kind of extra work on grad admissions we want to have!
I am driving what Google Maps tells me are the three hours down to Kirksville, Missouri, from Iowa City, to visit the Math & CS department at Truman State. I am hoping to meet some more fantastic potential graduate students like Truman alum Ben Delaware (whose paper was just accepted to POPL 2013 — congratulations, Ben!).
The slides for my talk on “Programs, Proofs, and Classical Logic” are here. I am planning to update this post with a little more about the trip once I get back.
[Updated the day after the trip:]
It was a very interesting trip down to Kirksville, on some quiet rural highways through eastern Iowa. The Truman State campus is very nice, quite charming actually. I met up with Jon Beck, a CS faculty member who coincidentally turns out to have ties to Iowa (David Eichmann, of U. Iowa Biomedical Informatics, was his advisor, at another institution). We had a very engaging conversation about CS, CS education, and CS at Truman State. The school transformed itself a couple decades back from what Jon described as a “sleepy teachers’ college” (presumably that phrase associates to the right), into a highly selective public liberal arts college. They actually got the Missouri legislature to agree to let them be as selective in their admissions as they want. This makes a huge difference, since it means they can focus on admitting just people who are adequately prepared and seriously motivated for college study. The same cannot be said about U. Iowa, for example. I also got a little tour of the campus, which again is really idyllic. I like U. Iowa, but I was a bit jealous of the campus there, truly.
I got to talk informally with a few other folks, and then gave my talk and made my grad-school pitch in the afternoon. The talk was really well attended — solely by undergrads, and no one would confess to any bribery to get them there. I was impressed. I got some great questions about both the research I was discussing, and about grad school in general. The students seemed sharp and engaged. I am certainly hoping that we get a couple applications from Truman Math & CS this season!
In a couple weeks I am going to do another of these, at St. Ambrose in Davenport, Iowa. Other colleagues from U. Iowa CS are making similar trips to nearby colleges. We are hoping these will bear some fruit in more domestic applications for grad school here.
It has been the busiest semester on record for me here at The University of Iowa, Computer Science department, due to a lot of group activity. Just one aspect of this has been travel for people I work with, from the summer up until now:
- I presented our paper “Type Preservation as a Confluence Problem” at RTA in Novi Sad, Serbia.
- Duckki Oe presented our paper “Combining a Logical Framework with an RUP Checker for SMT Proofs” at the SMT workshop, in Snow Bird, Utah.
- Frank (Peng) Fu presented our paper with Jeff Vaughan “A Framework for Internalizing Relations into Type Theory” at the PSATTT workshop at CADE, in Wrcolaw, Poland (which necessitated an elaborate visa-renewal trip for Frank to China).
- Duckki Oe also gave a talk at the DTP (Dependently Typed Programming) workshop in Nijmegen, The Netherlands, on his versat verified SAT solver tool, which is fully proved (all lemmas done, showing that if the solver says UNSAT, there is guaranteed to exist a resolution proof of the empty clause from the input clauses, although this proof is not actually created at runtime) and fully operational at this point.
- Harley Eades gave a talk on his work on hereditary substitution for variants of predicative System F, at the well-known TYPES meeting, in Bergen, Norway. You can read about his trip on his new blog, Metatheorem.
- Garrin Kimmell gave a talk at a Shonan meeting (in Japan) on dependently typed programming on call-by-value equational reasoning and general recursion in our Sep3 language, a design being developed in the context of the Trellys project, which I’ve blogged about before.
- And of course, we all went up to Midwest Verification Day in Minneapolis, Minnesota. This was a great event, where we got to see some of our friends working on verification-related topics, from other schools in the Midwest. I had interesting conversations with Grigore Rosu and Eric Van Wyk, and was really pleased to meet David Pichardie for the first time in person. He and two students drove over from Purdue, where they are visiting Jan Vitek to collaborate on compiling Java Byte Code to CompCert C (CompCert is a project developing a verified optimizing C compiler in Coq, led by Xavier Leroy).
So, it has been busy with travel for us (and that doesn’t count trips like to summer schools, or by other members of the group who work primarily with Cesare Tinelli). We definitely have a full semester under way as well, but I will write more about that later (you can get a small taste at the blog I am keeping for my seminar for first-year undergrads, on Hidden Meanings).