Skip navigation

I have been interested, for many years, in what is generally called computational classical type theory (CCTT).  The idea is to take some proof system for classical logic, and turn it into a programming language via the Curry-Howard isomorphism.  Cut elimination or normalization for the proofs turns into reduction for the corresponding program terms.  There is nothing at all objectionable about this, and indeed it is very interesting to see term notations for proofs of classical theorems like ((A \to B) \to A) \to A (Peirce’s Law) or A \vee \neg A.  It was the brilliant insight of Griffin (my that POPL ’90 was a good one, as Lamping’s paper on optimal beta-reduction was that year, too) that proofs of such classical theorems essentially involve control operators like call-cc.  This is all super cool and very interesting.

And I accept what I understand to have been David Hilbert’s position that non-constructive reasoning is an essential tool for mathematics, and that rigid constructivism (i.e., insisting on constructive proofs for every theorem) is thus disastrous for advancement of mathematics.  In Computer Science at least, I have sometimes in the past thought that the ability to do things like case-split on whether a term in some unrestricted programming language terminates or not could be very helpful if not critical for verification of general programs.

Since Curry-Howard is great and applies very nicely to classical logic, and since classical logic is useful if not essential for certain kinds of verification, CCTT should be fantastic in my book, right?

No — and of course I will tell you why.

The problem is that the Curry-Howard isomorphism a reasonable programmer expects to hold is broken in CCTT.  The problem can be seen clearly with disjunctions.  Under Curry-Howard, a disjunction A \vee B corresponds to a sum type A + B.  Given an element of such a sum, we can case split on whether that element is the injection of an element in A or else in B.  And in doing so, we gain some actionable information.  But this does not happen when we split on a use of the law of excluded middle A \vee \neg A (LEM).  We gain no information at all in the two branches of the split.  And indeed, the usual way CCTT proves LEM is to say (so to speak): it is \neg A which is true.  Then if the branch of the split for the right disjunct ever tries to make use of that information — wait, how can it do that?  The only thing you can do with the negative fact that \neg A is to apply it to a proof of A to obtain a contradiction.  And if you ever do that, the machinery of CCTT will take your proof of A, backtrack to the point where it originally told you \neg A is true, and then invoke the branch of the split for the left disjunct, with that proof of A.  Super clever!  (This is dramatized by a famous story about the devil told by Phil Wadler; see my old post about this.)  But also, note that it means you can never take action based on the result of such a case split.  Everything must be indefinitely revisable, due to the possible need to backtrack.  So you cannot split on an instance of LEM and print 1 in the first branch and 2 in the second.  Or rather, you can, but the meaning is not at all what you expect.  “This Turing machine either halts or it doesn’t.”  We case split on this, and could easily think that we are gaining some information by doing so.  But we are not.  Your code will just always print 2.  This is not what you reasonably expect under the Curry-Howard interpretation of disjunctions.  And thus using CCTT for programming is not a good idea.

It would be fine to use classical reasoning for reasoning about programs.  For the justification of some property of a program might require (or be easier with) some non-constructive case split.  But the program itself should not do such things, or else the abstraction Curry-Howard seems to offer us is violated.

Is this an argument against sum types in the presence of control operators?  (Genuine question)

 

 

Advertisements

For loyal QA9 readers, advance announcement that our release of Cedille 1.0.0 (promised some time ago!) is going to be made Friday.  You can get a sneak peak at the web site here.  The links on that page to the github repo won’t work yet as the repo is private.  But this will change Friday.  We will have a Debian package for easy installation — and will be happy for pull requests for packaging for other systems!

I remember, from maybe grad school, being puzzled about “semantics”.  What does this word mean?  Having gained a lot more knowledge of this topic since then, I thought I’d share a few thoughts on it, especially in the context of type theory.

“Semantics” means meaning.  In this sense, many different approaches to the study of programming languages are described as giving some form of semantics to a language.  An interpreter gives you a semantics for a language.  It shows you what these funny sequences of keywords or symbols (or more modernly, these peculiar abstract syntax trees) mean by showing how the programs execute.  If one writes an interpreter as a set of inference rules, then this is usually called operational semantics.  Hoare Logic, which is a set of inference rules for verifying that programs started in states satisfying a given precondition will (if they terminate) end in a state satisfying a given postcondition, has traditionally been dubbed axiomatic semantics.  This term “axiomatic” is maybe not too informative, but the idea that you can describe the meaning of an imperative program by explaining how it changes the state indeed gives it a reasonable claim to be a semantics.  What do programs in the language mean?  A semantics tells you.

There was a lot of interest in earlier days on giving denotational semantics to programs.  The idea is to give the meaning of a program by stating what mathematical function the program denotes.  After all, programs are intended (are they not?) to represent some class of functions as understood in mathematics.  A hallmark of denotational semantics is that it is compositional: the meaning of a bigger expression is defined in terms of the meanings of its strict subexpressions.  Notice that this is not true of operational semantics generally: we define the meaning of (\lambda x.\, t)\ t' in terms of [t'/x]t, which is not a strict subexpression of t (indeed it can be a bigger term than t). There was a lot of excitement, it seems, in finding denotational models of languages like lambda calculus.  More recently, it seems more common, at least in Computer Science, to take lambda calculus for granted and not be concerned with mathematical denotations of lambda terms.

Logic is, as far as I know, the earliest field concerned with giving mathematical semantics for formal languages.  There, denotational semantics of formulas is the basis of model theory.  Proof theory can also be viewed as giving a semantics of formulas, and indeed in nice situations these two semantics agree — though even for theories like first-order arithmetic, results like Goedel’s incompleteness theorem imply that no such agreement is possible: the proof-theoretic semantics (showing what formulas mean by showing how to prove them or use them in other proofs) must be weaker, in the sense of proving fewer theorems, than the denotational semantics.  But maybe this is a digression…

In type theory, there is a great tradition of giving denotational semantics for types.  In full generality, if we have a term t of type T (in some typing context G!), we would like to explain what this relation (G \vdash t : T) means.  Historically, it was discovered that one could use a denotational semantics for types as a proof method to show deep properties of the language, like normalization or logical consistency.  I first learned about this in Girard’s Proofs and Types, and still recommend this as a good introduction.  The historical root of this is Kleene’s realizability semantics for first-order intuitionistic arithmetic.  But one does not need to be driven by the desire to prove such metatheorems, in order to want to have a denotational semantics for types.  Here are my amazing new types!  Wouldn’t you like to know what they mean?  I can show you some typing rules, and depending on how I set them up — for example, if you give introduction and elimination rules for the types that are related in certain ways — these could to a greater or lesser extent show you what the types mean.  But a compositional semantics that says, “my funny type construct X A B means …” can be more direct, and provide guidance for crafting typing rules.  One can prove that a set of typing rules is sound with respect to the semantics, for example.

The form of such semantics I have found most useful is a realizability semantics, that tells you what a type means by specifying the set of all terms whose operational behavior is allowed by the type.  For example, in some language, the meaning of a type like “Int -> Int” could be defined to be the set of all programs which, given an Int input, either diverge or produce an Int output.  Or maybe in some other language, it is the set of all terms which, given an Int input, are guaranteed to terminate producing an Int output.  Notice that these example semantics do not say anything about the internal form of the program.  It could fail to be well-typed according to some set of typing rules.  It could do very crazy and upsetting things if not given an Int input.  The only thing the type specifies is the behavior of the term when given an Int input.  So the type describes behavior of terms, through the simple device of giving a set of terms as the meaning of a type (namely, the set of all terms whose behavior is allowed by the type).

For Cedille, I have defined such a semantics, and used it to prove logical consistency of the system.

By Anthony Cantor (University of Iowa PhD student)

Thanks to travel funds generously provided by my advisor, Aaron Stump, as well as the FLOC student travel grant, I was recently fortunate enough to spend a week in Oxford at FLOC 2018. Not only was it an enriching experience, but it was also my first time presenting research. Over the course of the pre-FLOC workshop weekend and the block 1 conferences I saw numerous thought-provoking and enlightening presentations, so I’d like to share some of the highlights here.

Term Assignment for Admissible Rules in Intuitionistic Logic
One of my favorites from my day at the Classical Logic and Computation workshop was Matteo Manighetti’s presentation of an extension of intuitionistic logic that supports admissible intuitionistic rules (with co-author Andrea Condoluci). He explained that if the provability of a formula A implies the provability of a formula B, then the rule A/B is admissible, and if the formula A→B is provable then the rule A/B is derivable. As far as I can tell, these definitions express the difference between meta-theoretic implication and object implication. In classical logic every admissible rule is derivable, but this is not the case in intuitionistic logic: apparently the rule ¬A→(B∨C) / (¬A→B)∨(¬A→C) is admissible but not derivable (this is called “Harrop’s rule”). Manighetti continued by describing an extension of intuitionistic logic obtained by adding axioms corresponding to the admissible rules, and a corresponding Curry-Howard term assignment. I’m really looking forward to reading this paper when it appears in the workshop proceedings because I’m very curious about the details of some of the proofs of theorems that Manighetti claimed during the presentation: one was the disjunction property, and the other he called a “classification” lemma. At the moment I’m quite interested in these sorts of proofs because I’m currently working with Aaron to prove a logical constructiveness result.

Proof Nets and Linear Logic
While at FLOC I attended two great presentations on the subject of proof nets: a presentation on proof nets for bi-intuitionistic linear logic by Willem Heijltjes, and a presentation on a new type of proof nets for multiplicative linear logic by Dominic Hughes. These two presentations caught my interest because of the logic under consideration in the former (bi-intuitionistic logic), and the concept of canonicity in the latter (these two topics relate to research I’ve been working on with Aaron).

Regardless of their potential relevance to my research interests, I’m happy to have attended these presentations because they both had a common property that taught me a lesson about designing slides: when possible, omit words (especially sentences) from a slide. Both of these presentations did a good job of focusing my attention on a particular point of the slide (usually some part of a proof derivation). Throughout the conference I often got lost because I was trying to read sentences on slides instead of focusing on the speaker. By omitting unnecessary words, these presentations kept my eyes on the right part of the slide, and my ears on the speaker. Interestingly, the two presentations differed greatly in terms of the their depth. Heijltjes’ presentation contained a lot details and examples, and Hughes’ stayed extremely high level.

Inspired by Heijltjes and Hughes, I’ve begun exploring linear logic and proof nets via Girard’s “Linear Logic”, a reference cited in both of their papers[1][2]. So far it’s been very rewarding. In particular, I quite liked the following observation made by Girard regarding the connection between the ⊢ relation and constructiveness:

Now, what is the meaning of the separation ⊢? The classical answer is “to separate positive and negative occurrences”. This is factually true but shallow; we shall get a better answer by asking a better question: what in the essence of ⊢ makes the two latter logics more constructive than the classical one? For this the answer is simple: take a proof of the existence or the disjunction property; we use the fact that the last rule used is an introduction, which we cannot do classically because of a possible contraction. Therefore, in the minimal and intuitionistic cases, ⊢ serves to mark a place where contraction (and maybe weakening too) is forbidden; classically speaking, the ⊢ does not have such a meaning, and this is why lazy people very often only keep the right-hand side of classical sequents. Once we have recognized that the constructive features of intuitionistic logic come from the dumping of structural rules on a specific place in the sequents, we are ready to face the consequences of this remark: the limitation should be generalized to the other rooms, i.e., weakening and contraction disappear. As soon as weakening and contraction have been forbidden, we are in linear logic.

Blockchain Verification
Grigore Rosu’s presentation on formally verifying blockchain contracts and virtual machines also stood out. In his talk Rosu advocated the use of a single framework called “K” to generate a suite of language and runtime tools related to a blockchain specification, as opposed to constructing the components first and attempting formal verification as an afterthought. The system uses a logic called “Matching Logic” to generate the components based on configurations containing semantic and syntactic rules. Rosu claimed that many previous methods for defining computational semantics have drawbacks, and that the “K” framework “keeps the advantages of those methods, but without the drawbacks”. Unfortunately he didn’t explain how exactly the “K” framework achieves this, but he did enumerate a rather impressive list of languages that are currently supported by the “K” framework, which included C, Java, and the Ethereum VM. I had a hard time following a lot of the detail about how matching logic enables auto-generation of effective language tools, but I’m at least convinced that it would probably be a lot of fun to try out his framework on a toy language.

Corrado Böhm Memorial
Finally, another standout event was most certainly the pair of talks given by Silvio Micali and Henk Barendregt in memory of Corrado Böhm. After relaying some personal memories, Barendregt presented some highlights of Böhm’s career. He first discussed some of Böhm’s early work on self compilation and bootstrapping. In particular, Böhm proved that one could start with a handwritten slow compiler, and then use that compiler to compile itself to obtain faster and faster compilers. Barendregt also touched on a few other important results achieved by Böhm, and ended by discussing Böhm’s passion for research: apparently Böhm was still stating open problems even while in his 90’s. Barendregt’s conclusion was memorable: “keeping asking questions, it keeps you young.”

[1] http://www.cs.bath.ac.uk/~wbh22/pdf/2018-bellin-heijltjes.pdf
[2] http://boole.stanford.edu/~dominic/papers/unification-nets/unification-nets-LICS-2018.pdf

This past Tuesday (June 19) I gave the second lecture in the series I am working on, about optimal beta-reduction.  The screencast can be found here.  This lecture covers the basic nondeterministic graph reduction rules for lazy duplication.  The notes you will see my writing are here in ora and jpeg formats.  The lambdascope implementation I try using (and many thanks to Jan Rochel for this!) can be found here on hackage.  The lambdascope paper can be found here.