Our shipment from HP of 160 nodes for StarExec arrived this week.  Pictures below courtesy of Aran Cox:

Everything needs to be installed and configured, so it will be some time yet (4-6 weeks) until this is incorporated into StarExec.  At that point, we will finally throw open the doors to the public…

I recently had occasion to read two papers by philosopher and logician Neil Tennant.  These were easily the most thought-provoking papers on philosophy of logic that I have read in the past two years.  One I found absolutely compelling, the other I regret to say I found to be completely and spectacularly wrong.  The writing in both was elegant and often witty, a charming change from the more workman-like efforts of us less cultured Computer Scientists.  The papers are:

I have not read other things by Tennant, having only just discovered that I likely would enjoy doing so.  He seems to be a prolific writer, so I am in luck.  I chose these by title to take with on a short trip, and am very glad I did so.

The title of the first of these is really inspiring — more so even the contents.  Despite my college education in Philosophy, I never studied Kant, nor too much of the analytic-synthetic distinction.  As Tennant summarizes it, the question is whether the truth or falsity of a sentence is determined solely by its (intrinsic) meaning, with no further contribution from the way the external world is, or whether the way the external world is contributes to determining the truth or falsity of the sentence.  In the first case (no contribution from the world) the sentence is called analytic.  In the second (some contribution from the world), it is synthetic.  Now, little as I know about this distinction, it is easy to see from the concepts in question, not to mention the custom of philosophers of exploring issues like this from a huge number of angles with endlessly nuanced arguments and positions, that this is a delicate and potentially complex matter.  But it was certainly an informative simple summary for me.

The main point of “The Law of Excluded Middle is Synthetic A Priori, If Valid” is that strictly classical principles like the law of excluded middle (LEM, $p \vee \neg p$), which Tennant says presume a meta-principle of bivalence — that every sentence is either true or false — are synthetic formulas.  They are a priori if valid, in Tennant’s view, in the sense that they are known absolutely independently (in principle?) of empirical experience.  The point is that there may be some additional metaphysical reasons for believing in bivalence, which would justify acceptance of strictly classical principles.  But there is nothing in the inherent meaning of the logical connectives that make sentences like LEM valid, if one assumes that the meaning of a logical connective is determined by its introduction and elimination rules.  Tennant seems skeptical that there is a real metaphysical justification for bivalence and hence LEM, but he is willing to allow the classical reasoner to persist in his bivalent thinking.  What he is not willing to allow is that such thinking is analytic: classical inferences should be explicitly acknowledged as synthetic.

Tennant’s position on strictly classical principles seems pretty compelling if one adopts a proof-theoretic view of logic, because at least for natural deduction systems (which Tennant seems to favor), classical principles are an add-on to the system, and do not follow the usual pattern of specifying the meaning of a logical connective via introduction and elimination rules. One simply has to postulate LEM as an axiom, or add a principle of proof by contraction (to prove $A$, assume $\neg A$ and derive a contradiction). So those principles do not seem to arise as an intrinsic part of the meaning of the logic connectives. Tennant’s position gives us a way to live with this phenomenon: we must just realize that strictly classical principles do not arise intrinsically from the meanings of the logical connectives because those principles really are extra-logical assumptions. The world may be determinate in the sense of bivalence, and it is at least conceivable that it should fail to be so. If we want to proceed under the assumption that it is, we need to make this assumption explicit in our reasoning.

We can perhaps strengthen this line of reasoning if we think of logic not just as a tool for thinking about the real world, which may or may not be determinate, but as a tool for reasoning within theories, which we know from metamathematics can certainly be incomplete and hence fail to satisfy bivalence. Take the fact that the Continuum Hypothesis (CH) is independent of Zermelo-Frankel set theory with the axiom of choice (ZFC), a celebrated result proved in two halves by Kurt Goedel and Paul Cohen. This shows that ZFC is indeterminate with respect to CH. A more basic example is Goedel’s theorem that first-order arithmetic is incomplete. For reasoning in such theories, perhaps it is more faithful to avoid LEM as part of the logic. If we think of the theories as describing only so much of the imaginable mathematical universe, then equipping them with LEM seems wrong. ZFC does not tell us whether CH is true or CH is false. Why should we postulate that despite this indeterminacy, one or the other of CH and its negation must be true? This seems to suggest a view of mathematical theories as being about all of some pre-existing mathematical reality, where there really is a truth of the matter about CH, whether the theory tells it to us or not. But given the multiple incompatible mathematical universes one can describe with a logical theory — for example, there are consistent extensions of ZFC where CH it true and other (incompatible) extensions where it is false — it has always seemed strange to me to assume there is a single pre-existing mathematical reality that is being described by different theories. In this sense, I consider myself an anti-realist about mathematics.

But there are a couple challenges we could mount to Tennant’s position that LEM, as an appendage to the usual natural deduction proof system for (say) first-order logic, should be regarded as synthetic instead
of analytic. First, we could question the choice of natural deduction as the proof system to use for deciding what is intrinsic to a logical connective and what is not. For example, it is well-known that if we use an unrestricted multi-succedent sequent calculus, we can derive classical principles like Peirce’s law just from the rule for assumptions and the left and right rules for implication. Here is  a derivation:

If we are willing to pass from minimal to intuitionistic logic (with a rule of explosion — also called ‘ex falso quodlibet’, or ‘from false, whatever’ — saying that from $\perp$ we can conclude any formula $A$), we can derive $((A \to \perp) \to \perp) \to A$ with a similar derivation. We have used no additional axioms embodying strictly classical principles. The unrestricted right rule for implication has sneakily included a subtle form of classical reasoning into the proof system: so subtle it is not so easy to see what its source is! One explanation for what is happening is that that rule is not compatible with the Kripke semantics for intuitionistic (or minimal) logic, where positive knowledge must persist in future worlds, but negative knowledge need not. We can view the presence of $A$ on the right as an assumption that $A$ is false, and hence we should not be allowed to use that assumption when we step to a new world where we are assuming $A$ is true. But this depends on a particular semantics for the logic. If we are taking the logical rules as primitive, what stops us from adopting this perspective? Likely there is some other way to find bivalence hidden in the basic form of sequents and the rules acting on them (though I do not know what it is).

The other challenge I see to Tennant’s view is simply to deny that the proof-theoretic approach to the semantics of the logical connectives is the right one. After all, the usual boolean semantics seems pretty
natural! I assume there are sophisticated answers to be made to this, so I will leave it be for now, and turn briefly to the second paper.

“Negation, Absurdity, and Contrariety” is largely concerned with denying that $\perp$ (falsity) has a legitimate role in logical formulas. Tennant asks “Is $\perp$ a genuine propositional constant, eligible to be a constituent of other sentences?” The succinct answer he offers is “On the face of it, no; unless $\perp$ is identified with a particular absurd sentence of an already interpreted language.” He goes on to offer reasonably convincing arguments against accepting $0 = 1$ as a definition of $\perp$ (largely because now the notion of falsity is tied to some particular theory, in this case arithmetic). Now, I think we can make Tennant’s job more difficult here, by choosing a formula which is not tied to a particular theory, to be our definition of $\perp$. For example, why not take the formula $\forall x. \forall y. x = y$? Even if we do not think that equality should be considered a logical connective, it does not seem tied to a particular theory. Certainly many theories besides just arithmetic rely on a notion of equality.  So perhaps this definition of $\perp$ can better resist a charge of being overly theory-dependent. Or if that is not abstract enough, let us just switch to a higher-order logic. There, it is standard to define $\perp$ as $\forall F. F$. This definition immediately gives rise to the ex falso quodlibet rule of inference mentioned above), since if $\forall F. F$ is true, we can conclude any formula $A$ by instantiating $F$ with $A$. This is a very strong notion of falsity, as Tennant is also noting (since it implies that a contradiction in one part of a theory automatically infects all other reasoning one might do).

Frank Fu has proposed a different notion of falsity, that has better properties when used in type theory. We can define Leibniz equality $x =_T y$ of terms $x$ and $y$ of type $T$ to be $\forall C:T \to \textit{Prop}. C\ x \to C\ y$. So we are saying that $x$ equals $y$ if all truths about $x$ are also truths about $y$. Now define $\perp$ to be $\forall T:\textit{Type}. \forall x : T. \forall y : T. x =_T y$. Using this definition, Frank has shown we can derive $0 \neq 1$ in pure type theory, where $0$ and $1$ are Church-encoded.

Now all these points aside, I come to my main complaint about this second paper of Tennant’s. He asks whether $\perp$ is a genuine propositional constant that one should be allowed to use in object-language sentences. He devotes significant space to arguing against defining $\perp$. I’d be willing to grant these arguments. But the real question for me is whether or not it makes sense to take $\perp$ as an undefined logical constant. And here, Tennant offers very skimpy arguments. He just says that whenever someone says something like “Contradiction!” or “That’s absurd!”, she is offering a metalinguistic commentary on whether a contradiction can be derived from some set of assumptions. And from this claim, in just a few sentences of consideration, Tennant confidently dismisses the idea of taking $\perp$ as a
propositional constant.

I find this completely inadequate as an argument against $\perp$ as a logical constant. After all, the role of object-language formulas is to reflect certain metalinguistic realities. This is certainly so from Tennant’s constructivist perspective, which emphasizes a tight agreement between the meanings of logical constants and metalinguistic inference rules. I don’t see how this same objection that Tennant is mounting — that something cannot be a logical connective if all it is doing is reflecting metalinguistic commentary — cannot be applied to any formula construct! One could just as well say that when someone says $A_1 \wedge A_2$, all he is really doing is making a metalinguistic statement about derivability of both $A_1$ and $A_2$. So we should not use any object language at all, but speak only in our metalanguage!
(And how is its meaning to be determined?)

A variation on my objection to Tennant: truth and falsity play quite a dual role in many different formulations of logic. How is Tennant’s objection not to be dually applied to rule out the use of $\top$? (Maybe he would urge this — but then I am surprised he takes aim just at $\perp$, and neglects $\top$).

Anyhow, much as I repudiate Tennant’s conclusion in this second paper, I found it as enjoyable and interesting reading as the first, and commend both to you.

This past Thursday and Friday (Oct. 10th and 11th), I organized a mini-symposium on Programming Languages here at U. Iowa.  I invited doctoral students from Indiana, U. Penn., Portland State, and Northwestern to come down and give talks on their research in PL.  Robby Findler from Northwestern also brought his fall PL seminar down — so we had a big group of Racketeers here!  Sam Tobin-Hochstadt gave the keynote, which was simultaneously our departmental colloquium.  Why did I call this a mini-symposium?  Isn’t a “symposium” in the ACM taxonomy just a meeting that is between the size of a workshop and a conference?  I was thinking of Plato’s symposium here, where the emphasis is on lively discourse in pursuit of truth (about love, in Plato’s case, and involving quite a bit of drinking — while our focus was more technical, we did go for local beer).  So we had 45 minutes blocked out for each talk, and lots of breaks and long lunches.  I was really happy with the results, as we did ask a lot of questions, ranging from basic-knowledge questions from folks newer to a particular topic, to quite advanced reflections.  The talks were all really great, too, with the possible exception of my own, which was too jammed with rules and derivations.  Anyhow, it was a very fun event, and I plan to ask for participant travel funds from NSF — which paid for this edition — in my future grant proposals.  You can find the program, with titles and abstracts, and even a group picture, here.

Everyone knows classical logic is nonconstructive. If a classical principle like $\forall x. \phi(x) \vee \neg \phi(x)$ were true constructively, it would mean we would have an effective (i.e., computable) way to tell, for any value $x$, whether or not $\phi(x)$ is true or false. When $\phi(x)$ expresses a property like “the Turing machine coded by natural number $x$ halts”, then we can see that $\forall x.\phi(x) \vee \neg \phi(x)$ cannot be constructively true in general. Case closed.

But a funny thing happened on the way from Amsterdam: computational interpretations of classical type theory were devised, like the $\lambda\mu$-calculus of Parigot and quite a few others.  These type theories have term notations for proofs of classical logic, and give a reduction semantics showing how to simplify proofs to normal forms, similar to standard reduction semantics for good old $\lambda$-calculus.  The reduction semantics is perfectly effective, so one really can compute — or so it would seem — with terms in these type theories.  If the essence of constructivism is computation, then it would seem that classical logic is constructive.  Indeed, titles like that of Girard’s 1991 article “A new constructive logic: classical logic” would suggest this.

But you know, maybe it is intuitionistic logic which is nonconstructive.  Come again?  Well, the past half year or so several of us here at Iowa have been studying so-called bi-intuitionistic logic.  This is a logic that extends standard propositional intuitionistic logic with an operator called subtraction, which is dual to implication.  There are a number of papers about this topic I could recommend.  Maybe the easiest introduction is this one by Goré, although we ultimately followed the approach in this paper by Pinto and Uustalu.   Recall that in the Kripke semantics for propositional intuitionistic logic, the implication $A \to B$ is true iff in all future worlds where $A$ is true, $B$ is also true. The subtraction $A - B$  has a dual semantics: it is true iff there is an earlier world where $A$ is true and $B$ is false.  In intuitionistic logic, one usually defines $\neg A$ as $A \to \perp$.  This negation is true iff $A$ is false in all future worlds.  In bi-intuitionistic logic, one can also define a second kind of negation, using subtraction: $\sim A$ means $\top - A$, and it is true iff there exists an earlier world where $A$ is false.  With this definition, we start to see classical principles re-emerging.  For example, $A \vee \sim A$ holds, because in any world $w$ of any Kripke model, either $A$ is true in $w$, or there is some earlier world (possibly $w$) where $A$ is false.  Valid formulas like $A \vee \sim A$ violate the disjunction property of intuitionistic logic, since neither $A$ nor $\sim A$ holds, despite the fact that the disjunction does hold.  The disjunction property, or in programming-languages terms, canonicity, would seem to be as much a hallmark of constructive reasoning as the law of excluded middle is of classical reasoning.  Yet here we have a conservative extension of intuitionistic logic, based on exactly the same semantic structures, where a form of excluded middle holds and canonicity fails.

What are we to make of this?  Let us think more about our Kripke semantics for (bi-)intuitionistic logic.  In this semantics, we have a graph of possible worlds, and we define when a formula is true in a world.  Formulas that are true stay true (the semantics ensures this), but formulas which are false in one world can become true in a later world.  The critical point is that we have, in a sense, two notions of truth: truth in a world, and truth across time (or across possible worlds).  Truth in a world is usually thought of as being defined classically.  Maybe it is better to say that the modality with which it is defined is not made explicit.  A textbook definition of Kripke semantics is making use of some background meta-language, and I think it is fair to say that without further explicit stipulation, we may assume that background meta-language is the language of informal classical set theory.  So for any particular formula $\phi$, either $\phi$ holds in world $w$, or else it does not.  This is, in fact, what justifies validity of $A \vee \sim A$.  Indeed, to construct a version of Kripke semantics where this is not valid would seem to require something like an infinitely iterated Kripke semantics, where truth in a world is constructively defined (the infinite iteration would be to ensure that the notion of constructive definition being used for truth in a world is the same as the one for truth across worlds).  An interesting exercise, perhaps!  But not one that will validate the laws of bi-intuitionistic logic, for example, where $A \vee \sim A$ is indeed derivable.

So what is it that makes a logic constructive?  Let’s come back to the case of computational classical type theory.  The term constructs that were discovered to correspond to classical principles were not so exotic: they were actually forms of familiar control operators like call-cc from functional programming!  So, these constructs were already in use in the wild; only the connection to logic was a (remarkable!) discovery.  So every day, the working Scheme programmer, or Standard ML programmer, or Haskell programmer has at his disposal these constructs which correspond to nonconstructive reasoning.  But they are writing code!  It is computing something!  What is going on?

Perhaps it is in Haskell where this is clearest.  To use call-cc, one must import Control.Monad.Cont.  And there we see it already: the control operator is only available in a monad.  The sequencing of operations which a monad is designed to provide is critical for taming call-cc from the point of view of lazy functional programming.  In the words of Simon Peyton Jones (from these notes):

Indeed it’s a bit cheeky to call input/output “awkward” at all. I/O is the raison d’etre of every program. — a program that had no observable effect whatsoever (no input, no output) would not be very useful.

And that’s just where the interaction of control operators with pure functional programming seems strange.  Phil Wadler, in his well-known dramatization of the computational content of the law of the excluded middle, has the devil give a man a choice: either the devil pays him one billion dollars, or if the man can pay the devil one billion dollars, the devil will grant him one wish of whatever he wants.  The man accepts the choice, and the devil goes with option 2.  After a life of greed and antisocial accumulation, the man present the devil with one billion dollars, hoping for his wish.  The devil (using a control operator, not that they are intrinsically evil) goes back in time, so to speak, to change the offer to option 1, returning immediately to the man his one billion dollars.

I am reaching the conclusion that it is not the non-canonicity of the law of excluded middle that is the locus of non-constructivity.  It is the lack of a notion of the progression of time.  The devil (indeed, even God Himself) cannot change the past — despite numerous Hollywood offerings (Back to the Future, anyone?) based on the idea of changing the past — but without some restrictions, control operators can revert to an earlier time, thus potentially undoing some of the effects that have already been carried out.  As Peyton Jones is saying, if the computation just spins its wheels and does not interact at all with the outside world, then there is not really any notion of time or cause and effect which could be violated by the use of a control operator.

Another way to think of it: classical logic is the language of mathematics, where everything is considered as a static entity (notwithstanding the fact that dynamic entities like computations can be statically described).  Constructive logic is supposed to have a dynamic character: it should capture the idea, somehow, that the state of information can change over time.

So where I am thinking to go with all this on the language-design side, is rather than developing a type theory based on bi-intuitionistic logic (which we have been hard at work on doing for many months now, and which is likely a good research project anyway), to develop instead a type theory based on classical modal logic, where classical reasoning, and its corresponding type theory with full control operators, can be used at any given time, but not across time.  Reasoning (or computation) across time will be governed by the rules of a modal logic, likely S4 for reflexivity and transitivity of the modality.  Observables operations like input and output will require stepping into the future, from which no control operator can return the flow of control.  Such a type theory would provide a new approach to pure functional programming with effects: at any given instant of time, one could perform reads and writes (for example), possibly backtracking with control operators to cancel some of them out.  But when one wants to step forward in time, the most recent operations (particularly writes) are committed, and become irrevocable.  Such a type theory would hold out the promise of combining classical reasoning (at a particular time) with constructive computation (across time).  If we think of general recursion as computation over time — with each general recursive call requiring a step into the future — we can even combine Turing-complete computation with logically sound classical reasoning in this way.  That would be almost the holy grail of verified programming I have been working towards for the past 7 years or so: a single language supporting sound classical reasoning and general-purpose programming.

So to conclude: what is so nonconstructive about classical logic?  I believe it is not the failure of canonicity, but rather the lack of a notion of progression of time.  Devising type theories with this perspective in mind may bring new solutions to some old conundrums of both type theory and functional programming.  We will see.

This summer, a bunch of us here at U. Iowa were learning Agda, and I thought I’d write up some of my thoughts on the system, now that we have used it a little.  Overall, I found it to be a great tool, with numerous very nice design ideas.  The positives:

• The latex-style syntax for unicode, which I gather is supported in some other tools like Isabelle, is fantastic.  One can type \forall and get ∀.  I thought I would not care much and not use it, and was surprised to find how much I like having these notations available in code.  It is just the best, particularly when it comes to formalizing mathematics of whatever kind.  I only wish I could define my own shortcuts for specific symbols.  If I am typing \cdot a lot, maybe I want to type just \. or something.  For all I know, one can define such shortcuts, but the documentation (one of the few negatives) does not seem to say.  Using unicode notations in Agda has got me thinking about more general notions of syntax.  For example, what about 2-dimensional syntax, where I can supply any scalar vector graphics image as the definition of a symbol?  Then I could design my own notations, and have inputs and outputs coming in and out of different ports on a square displaying that image.
• The support for implicit arguments to functions is very good.  With dependent types, you often need lots of specificational data as arguments to functions, just so that later types come out correctly.  For example, to append vectors of length N and M, you need to make N and M extra arguments to the function.  In most cases, Agda can automatically infer these, and you can omit them where you call the function.  Again, I expected I would not care and would be happy to write out lots of indices to functions explicitly.  Wrong again!  It qualitatively changes the experience to be able to leave those out most of the time.  Code becomes much, much shorter, and when you get lucky and everything lines up correctly, and Agda can figure out instantiations, then it is quicker to write, with less cognitive burden.  This is really a great feature.
• Equational definitions are fantastic.  I had already overcome my foolish bias against these from previous exposure to equational definitions in Haskell.  It is just so nice to be able to write something like

 [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys) 

for append, rather than first abstracting the arguments and then doing the pattern matching and recursion, as one would in OCaml (which is still my go-to programming language, despite all this coolness in these other languages).

• The type refinements in pattern matching (incorporating axiom K, I understand) work simply and naturally.  You match on something of type a ≡ b, you cover that case with just refl, and the type checker knows a must be definitionally equal to b.  That’s exactly what you want in practice, and it’s a pleasure to use.
• The overloading of constructors is outstanding, for the simple reason that it helps you avoid introducing extra names for similar concepts.  Part of what makes theorem proving and dependently typed programming tough is the cognitive burden to keep track of lots of interdependent information.  Just remembering the names for everything is a big part of that.  Fewer names, less cognitive load.  It is easy to greet you if we are all named Tom or Tammy.

Overall, this made for a great experience using Agda.  For example, I formalized Kripke semantics for intuitionistic propositional logic (actually, bi-intuitionistic logic, but that is another post), and proved monotonicity of the semantics, a standard property.  The proof in Agda is significantly shorter than what the paper proof would be.  It is also more readable (I think) by a human than a tactic-based proof in Coq, say, would be.  This is really the first time I felt as thought some result was easier to prove in a theorem prover than slogging it out in LaTex.  I am not saying Agda is unique in enabling this, but it is interesting to me that the first time I have had this feeling (having formalized a number of other things in Coq and other provers, including a couple of my own) is in Agda.

Ok,  now quickly for some constructive criticism:

• The documentation needs to be improved.  I know it is a nuisance to document things, and it seems, from the Agda wiki,  that maybe the documentation has been getting updated or migrated or something.  But it’s not too great right now.  There are many little sources to consult (this tutorial for how to use the Agda emacs mode, these lecture notes for how this or that feature of the language works, this old reference manual for this, a new reference manual for that).  It is irritating.  Agda needs a single consolidated reference manual with all features covered with examples.
• The standard library needs better documentation, too.  Mostly the intended use model seems to be to browse the standard library.  This is not too fun.  The organization of the standard library has some annoyances, like central definitions put in Core.agda files in subdirectories, rather than in the expected file.  Either some kind of agdadoc tool that could generate just type signatures and comments in HTML from the library code, or else a real reference manual for the standard library, would improve usability a lot.  Just look at OCaml’s standard library documentation for a very nice example.
• Error messages involving meta-variables and implicit variables can be hard to decode.  Giving good error feedback with type inference is known to be a tough problem, and it is exacerbated with the dependently typed setting.  I think we need more research (or if it’s already been done, more implemented research) on how to let the programmer interact with a type checker to explore the state the type checker has gotten into when it found a type error.  Mostly Agda’s error messages are reasonable, but once higher-order meta-variables and implicit arguments get involved, it can be pretty confusing to figure out why it’s having trouble typing my term.
• Compilation is a bit funny right now.  Compiling hello-world in Agda took a couple minutes, and generated a 10 megabyte executable.  Wow!  It’s because it is first compiling a big chunk of the standard library to Haskell, and then calling the Haskell compiler.  It still seems too slow, and generating too big an executable.  I asked one major Agda user this summer about this, and he said he had never tried to compile a program before!  So many people are just running the type checker, and using Agda as a theorem prover.  But it does compile, and it can do rudimentary IO with Haskell’s IO monad (this is a plus I did not list above).

Ok, so that’s my feedback from learning Agda this summer.  I’d love to hear others’ experiences or thoughts in the comments!