Discussing "Internal Universes in Models of Homotopy Type Theory"

(Link)

Authors: Daniel R. Licata (Wesleyan University), Ian Orton (University of Cambridge), Andrew M. Pitts (University of Cambridge), and Bas Spitters (Aarhus University)

Reference: D. R. Licata, I. Orton, A. M. Pitts, and B. Spitters. “Internal Universes in Models of Homotopy Type Theory”. In: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Ed. by H. Kirchner. Vol. 108. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018, 22:1–22:17. doi: 10.4230/LIPIcs.FSCD.2018.22.

Why this paper? Cited by Homotopy type theory as internal languages of diagrams of ∞-logoses and mitten: a flexible multimodal proof assistant

Although this paper has among its authors my PhD supervisor (Andy) and a former collaborator (Bas), it did not give up its secrets easily, for me at least, thanks to the high technical level in the introduction alone. But, like an early Christmas present, I think there’ s something pretty interesting in here once it is unwrapped.

The story starts with homotopy type theory (on which I have written before), a proposal to improve the treatment of equality in the type-theoretic foundations of mathematics. It continues with cubical type theory, a first shot at actually implementing homotopy type theory. While homotopy type theory can be understood via a general notion of path-up-to-continuous-deformation in a space, cubical type theory is understood through a specific such space, namely the cubical sets. Never mind precisely what they are; it is enough for this less technical blog post to know that there is an interpretation of cubical type theory in some mathematical structure that allows one to give meaning to all constructions. One technicality that is important for understanding the paper of today is that the naïve approach to extracting a type theory from cubical sets (which can be done because the cubical sets form a topos) does not give quite the right thing. One needs the naïve notion of type to come equipped with something extra, called a composition structure; we call types with such structure fibrant. Not every cubical set is fibrant (else we would not have to explicitly require the structure). For example the interval cubical set which is used to define the notion of path, and hence equality, is not itself fibrant, so is not a first class type.

Today’s paper is part of an effort to define the correct notion of model of cubical type theory in type theory itself. This may seem quixotic but is in fact well motivated: such a definition is suitable for machine checking (and indeed this is done by formalising this paper in an Agda fork called Agda-flat), can be simpler than a more standard definition, and can also be more general, which raises the possibility of shifting from cubical sets to some other model if such a shift were found to be more appropriate for some purpose. However cubical sets are not abandoned altogether; the acid test for the type theory used in this paper is whether everything works in the ‘internal language’ of cubical sets (here again we use the fact that we have a topos, and any such comes equipped with its own native type theory).

The problem with the literature up until this paper is that attempts to formalise a model of cubical type theory in this style had not yet included any universe types. Universes are less cosmic than they sound (although the problems they throw up can be mind-expanding), but are rather a standard feature of dependent type theory that allows us to blur or even erase the distinction between types and terms; types are simply terms inside some universe type (more than one such type is required because otherwise we get the universe type as a member of itself, which throws up Russell-style paradoxes). Universes are an indispensable tool for such type theories, allowing one to use the useful constructions of the term-level language to define new types. The omission of universes from the earlier work was not an accident, but stems from an observation of Orton and Pitts that adding universes in the standard way in fact leads to a contradiction. This is related to a fact that not all families of fibrant types - which is to say, correct types for cubical type theory - are themselves fibrant; but if we want universes to be first class types, they must indeed be fibrant.

The solution to this is perhaps a bit surprising (although it is anticipated somewhat by earlier work by Michael Shulman), as it comes from modal logic, or more precisely, modal type theory. In particular there is a ‘global elements’ functor on cubical sets that behaves like the box modality of the intuitionistic version of a well known modal logic called S4. For this reason, techniques in type theory developed for that modal logic are applicable to that functor, namely a `dual zone’ variables context. Here all variables in one zone, called the ‘crisp’ variables, implicitly have the functor applied to them. Any term that is then substituted for a crisp variable must itself depend only on crisp variables. This notion is put to work in the definition of the ‘code’ and ‘elements’ constructions which relate types to elements of universes, as the dependencies in their definitions are required to be crisp, which precisely blocks the earlier proof of contradiction. A final argument which revolves around the interval having a property called ‘tininess’ shows that not only does the universe thus defined enjoy the properties it should have, but that it does so uniquely.

Discussing 'Nominal Unification'

UPDATE - Due to upcoming teaching commitments and, after that, paternity leave, this blog will not be updated again in the near future.

(Link).

Authors: Christian Urban (University of Cambridge), Andrew M. Pitts (University of Cambridge), and Murdoch J. Gabbay (INRIA).

Reference: Theoretical Computer Science vol. 323(1-3), pp. 473-497 (2004)

Why this paper? Cited by 4 (of a possible 28) of the papers in my Google Scholar Updates recommendations.

Comments: In the first iteration of this blog I reviewed recent papers recommended to me to by Google Scholar Updates; one of the reasons I abandoned this is that many of these new papers were quite strongly linked to older work, and I ended up having to explain all that older work before writing about the new. Note that being strongly linked to older work is no bad thing - on the contrary, such incremental research is the unglamorous but essential heart of scientific progress. But my new focus for this blog, on 'classic' (which is to say, highly cited) papers, allows me to focus more on foundational work, which tends to be more original and so may be described with less reference to prior literature.

The reason for this discussion is that I have already discussed this week's paper at some length in a post for the first iteration of this blog. Please feel free to look up the post; the only correction I'd make is that is that a quadratic time (which is to say, feasibly fast) algorithm for nominal unification is in fact sketched in the conclusion of this paper, whereas I had previously thought that credit for this should go to Levy and Villaret alone.

Let me instead discuss something slightly orthogonal to this paper. The phrase 'nominal techniques', which I discussed for example here, actually refers to two things - syntax and semantics. I have previously emphasised the semantical (which is to say, mathematical) side because that is where my interests lie; but here is a paper that is clearly nominal techniques yet makes explicit use of neither Fraenkel-Mostowski set theory nor nominal sets. What brings the syntactic and semantical work together under the heading 'nominal techniques' is their commonality of jargon and notation, their treatment of names as 'first-class' entities rather than as embarassments to be hidden away, and their use of name permutations (name-for-name swappings) as the main technical engine. These links mean that for a trained reader it is simple to see how this paper should be understood semantically, although my workshop paper 'Nominal Logic with Equations Only' is the only place I know of where this is done explicitly (see Section 6).

Discussing 'Nominal logic, a first order theory of names and binding'

(Link).

Author: Andrew M. Pitts (University of Cambridge)

Reference: Information and Computation vol. 186(2), pp. 165–193 (2003).

Why this paper? Cited by 5 (of a possible 29) of the papers in my Google Scholar Updates recommendations.

Comments: Two weeks ago I discussed "A New Approach...", the paper that introduced nominal techniques. In that discussion I specifically mentioned (the conference version of) this week's paper as the one that introduced nominal as the term of the art for these techniques. So this is very much a sequel paper, and as such this is very much a sequel discussion - please do read my earlier discussion before this one.

As I discussed, the innovation of "A New Approach" was the mathematical shift to a non-standard set theory. Such a move is beautiful and clever, but does run the risk of being profoundly alienating to working computer scientists who simply want to solve problems involving names and binding! This paper, without abandoning the central insights gleaned from the Fraenkel-Mostowski setting, shows how much can be accomplished without straying beyond first-order logic, a completely standard logical setting that no one could object to. Along with this, Pitts makes a notion called nominal sets the semantical heart of his developments. Nominal sets appear in "A New Approach" as a preliminary construction on the road to the set-theoretic semantics, but they are far simpler than the full non-standard set theory. Although they are less expressive, this paper makes the case that they are expressive enough for most applications, a view which has been vindicated by the hundreds of papers that have since used the nominal sets framework.

While both logic and semantics have proved very useful, there is an acknowledged mismatch in this paper between them, via an incompleteness result - first-order logic is not really powerful enough to fully describe the properties of nominal sets, even 'cut down' as they are from the full set theory. For the notion of the 'set of free names' of a term (in nominal sets jargon, the support of an element) to be specified we would need the more powerful second-order logic. However the assertion that a name is not in the set of free names of (in the jargon, is fresh for) a term can be expressed in first-order logic, and turns out to be all that is needed for most applications. James Cheney resolved this mismatch in a 2006 paper, which provided a semantics that was complete for this paper's nominal logic, although I'm not aware of any applications of this very interesting theoretical work. After all incompleteness is often unavoidable, so is not necessarily a barrier to getting some work done!

Discussing 'A New Approach to Abstract Syntax with Variable Binding'

(Link).

Authors: Murdoch J. Gabbay and Andrew M. Pitts (University of Cambridge)

Reference: Formal Aspects of Computing Vol. 13(3-5), pp 341-363 (2002).

Why this paper? Cited by 9 (of a possible 29) of the papers in my Google Scholar Updates recommendations (where multiple citations from different papers by the same author(s) in my recommendations are disregarded).

Comments: My PhD and some of my subsequent research was built around something called nominal techniques; this is the journal version of the conference paper that introduced them (in fact the second author, Andrew Pitts, was my PhD supervisor). Already some clarification is necessary: computer science has for some reason developed an unusual publication culture in which peer-reviewed conferences, rather than journals, take center stage. But conference publication often imposes tight space limits on papers, which can force authors to tighten their prose, which I find no bad discpline, but more regrettably can mean some details or examples are omitted. Hence new research is often published twice, with a more detailed 'journal version' following the conference version, often years later because of the slowness of the journal review process (which itself is probably contributed to by so much work having to be reviewed twice!). Another clarification to my first sentence is that the word 'nominal', which has become the brand name under which all developments of this work by Gabbay and Pitts are grouped, does not appear in this paper. I believe it was introduced by Pitts in his 'Nominal logic' paper, which was published before this paper but written after it, thanks again to the vagaries of academic publication.

The problem this paper addresses is that of reasoning formally in the presence of names and binding, ubiquitous features of computer science applications and other formal settings like mathematics. Of course names are everywhere - think of variable names in programs, or the identifiers like x and y we use when we do maths. The precise names we use is at some level arbitrary; while we're doing our mathematical manipulations we better keep track of our xs and ys, but 'from the outside' it obviously wouldn't have mattered if we'd called our variables foo and bar instead. Binding (sometimes, scope) is simply the point where this 'outside' versus 'inside' distinction is made: some operations have the property that the choices of names inside the operation's domain are irrelevant to anything outside that operation's domain. Such structure is vital in software engineering applications where people worry about encapsulation, but is in fact virtually unavoidable in any sufficiently interesting formal setting.

Anyone with a passing interest in computing, or even logic or mathematics, would nod along to most of the previous paragraph, but perhaps would not become greatly interested. Names and binding are basic machinery, and there is no reason to spend time thinking about them, as opposed to getting on with using them! The twist comes when one tries to reason fully formally, for example to convince a computer that a certain program has a certain desirable property. This sort of reasoning, if successful, can yield guarantees about software far more robust than mere testing, but it is not easy, and names and binding structure turns out to be be one of the (many) barriers to doing this successfully. In particular, proofs involving structural induction, which are vital to programming languages applications in particular, do not play well with bound names. So there is a problem to be solved.

The solution proposed by Gabbay and Pitts (I should note that other candidate solutions exist, but I will not discuss them here) is to change the set theoretic foundations on which we build our mathematics, from the standard one to an alternative framework developed by Fraenkel and Mostowski in the 1930s for reasons completely unrelated to computer science. In this framework certain elements called atoms claim a privileged place, giving mathematics in this universe a slightly different flavour. This paper adapts this work in (to me) wildly surprising fashion to show that if we view these atoms as our names then we have just the right 'universe' in which to model, and reason in a reasonably intuitive way about, binding, up to and including the structural induction I mentioned earlier.

It should be acknowledged, of course, that doing mathematics in a 'different universe' sounds like an cumbersome (and possibly eccentric!) move. For this stuff to actually be used, the esoteric set theory needs to be at least partially hidden, and subsequent work, most notably the 'nominal logic' paper I mentioned above, has helped to do this. Still, all of the many subsequent applications of Gabbay and Pitts's work can be seen to rest on some of the most abstruse mathematics you can imagine, a story that must gladden the heart of any working theoretician!

Full Abstraction for Nominal Scott Domains

(Link).

Authors: Steffen Lösch and Andrew M. Pitts (University of Cambridge).

Conference / Reference: 40th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL '13), 23-25 January 2013, Rome, Italy (ACM Press).

Comments: Just two weeks ago I was remarking on the very large proportion of papers recommended by Google Scholar Updates that came from Cambridge; well, here is another one - the fourth of the last six. To be precise, I should say it was the fourth of the last eight, as I have decided to fudge the purity of the experiment for the first time by skipping two papers from the same authors as this this one, on the grounds that I was unlikely to gain much benefit from them.

This paper, whose second author was my PhD supervisor, is much more down my alley, as you might expect; it is another that deals with nominal sets, which I first discussed on this blog here. In that post I mentioned in passing that nominal sets had their origins in 1930s axiomatic set theory, before a rather surprising revival in 1999 by Murdoch Gabbay and Andrew Pitts, who employed them to model syntax with names and binders in computing. However their origins in deep set theory shouldn't be completely forgotten; their original use was for an attempt to construct a model of set theory where the axiom of choice failed.

Mathematics as conceived by Euclid is the process of enumerating axioms and inference rules that are obviously true, and then deriving truths from them (some of which may be far from obvious). Even in Euclid's own work this idealised picture did not really hold, as the fifth postulate of his geometry, regarding non-parallel lines, was rather more complicated that might be desired, and was long regarded as a flaw of his presentation. Much later it turned out that denying this postulate could lead to interesting and valuable mathematics for geometry in curved space. The attempt to axiomatise set theory in the early twentieth century came to a quite similar place, with the axiom of choice (which regards the ability to make systematic choices from unstructured sets, even infinite ones) as the useful but non-obvious 'rogue' axiom. Again, it turned out that both the axiom and its negation were compatible with the other, more obvious, set axioms, and so 'nonstandard set theory' in which the axiom failed - of which nominal sets are an example - could be developed and applied, as with non-Euclidean geometry.

The subjects of this paper, domain theory and denotational semantics, are techniques to interpret computer programs as objects in a mathematical setting that directly supports rich and complex computation phenomena such as recursion. This apparently esoteric material about set theoretic axioms matters because some of the proofs of the basic facts about domains use the axiom of choice. This paper defines a programming language PNA (and an extension, PNA+) with commands for manipulating and binding names, and develops domain theory within nominal sets to provide a characterisation of programs in this language. But domain theory within nominal sets needs, in part, to be reconstructed to avoid reliance on the now invalid axiom, which is one of interesting technical challenges addressed by this work (following earlier work by Glynn Winskel and David Turner (pdf), also at Cambridge).