Discussing "A Modal Analysis of Staged Computation"

(Link)

Authors: Rowan Davies and Frank Pfenning (Carnegie Mellon University)

Reference: Davies, Rowan, and Frank Pfenning. "A modal analysis of staged computation". Journal of the ACM (JACM) 48.3 (2001): 555-604.

Why this paper? Cited by A Fibrational Approach to Multiplicative Additive Indexed Linear Logic and Proofs and Refutations for Intuitionistic and Second-Order Logic

This week we have some work I know and love (although I think I’ve spent more time with the shorter conference version, published in 1996). The central idea is for a programmer to state using their type system in which order (expressed as stages) their program will execute. This would allow various optimisations to be applied automatically at compile time. We achieve this via a new type constructor, written ☐. Code of type ☐A is understood as unevaluated code of that type. For example, there is always a function from ☐A to A, which works by evaluating the code.

The cool thing here for a logician interested in the Curry-Howard isomorphism between proofs and programs is that this new type-former behaves exactly like the necessity, or box, modality of the well known modal logic S4 (more precisely, the intuitionistic version of this logic, without the possibility, or diamond, modality). For example, necessitation (a standard feature of all normal modal logics) corresponds to the ability to treat an arbitrary closed program as code, which does not hold of programs with free variables. So this paper, developing as it does lambda calculi for this box, is both a contribution to a particular programming language problem and to the proof theory of an important modal logic.

There are a number of different calculi developed in this paper, with the most important split between the dual context and context stack approaches. This nicely prefigures more recent work in modal lambda calculus, which supports the conclusion that while other approaches work for specific modal logics, these are the two approaches powerful enough to work for a large variety of modal logics; see here for a modern view of the first approach, and a paper of mine for the second. Another split is between the calculi that hew closely to the simply typed lambda calculus and (although this is not proved, it is fairly clear) are guaranteed to terminate, versus the ‘Mini-ML’ variations that achieve Turing completeness via general fixed points, at the cost of muddying the relationship with logic.

Given the context stack approach is close to my heart, I’ll make some more specific comments on this. Without getting distracted by bike shedding I'll briefly note that I do prefer the older term for this approach, Fitch-style (named in honour of work in proof theory by Frederic Fitch) over the coinage of Kripke-style here (Saul Kripke’s famous ‘possible worlds’ semantics should correspond to any reasonable proof theory, although admittedly Fitch’s approach feels closest to this semantics). The basic idea is that use of our Box modality corresponds to navigating through various layers of contexts; this is a wonderfully general idea and not fixed to the particular logic S4.

One interesting feature of S4 is that ☐…☐A is logically equivalent to ☐A for any number of boxes. My work has shown that if we are willing to allow all boxed types to further be isomorphic (true for many applications, but perhaps not appropriate for this work) we can significantly simplify the calculus of this paper. This works by removing the need for natural number indices to track how many layers of contexts are being popped at a given point of the program, and hence removing the need for ‘modal structural transformations’ in the reduction relation that are needed to relabel indices at various points. This actually contradicts the assertion in this paper that indices are necessary because of a certain ‘coherence’ problem; in fact that problem can be shown to resolve (the proof of this is not that easy), so the indices are in fact only necessary to preserve, if desired, the generality of having ☐…☐A be possibly non-isomorphic (genuinely different) to ☐A.

Discussing 'On the homotopy groups of spheres in homotopy type theory'

(Link)

Author: Guillaume Brunerie (Université Nice-Sophia-Antipolis)

Reference: Brunerie, Guillame. “On the homotopy groups of spheres in homotopy type theory.” PhD Thesis, Université Nice-Sophia-Antipolis. 2016

Why this paper? Cited by Formalizing π4(S3)≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda, Commuting Cohesions, and Encoding Dependently-Typed Constructions into Simple Type Theory

Many PhD dissertations are constructed by ‘stapling together’ a variety of different research papers generated during the years of study, with a varying level of effort put into writing connective tissue between them. This is very much not one of those dissertations. Instead, it is a book length development of a single mathematical fact, that π4(S3)≅ℤ/2ℤ. Of course, unpacking this line of mathematics would take time - ‘the fourth homotopy group of the 3-sphere is equivalent to a certain 2-element group’ is a first unpacking, but there is much jargon in there would itself require unpacking – but the focus on this one result is still notable.

I will of course not pretend to do full justice to the multiple years of effort that went into this thesis in the space of a short blog post, but instead try to give some high level feeling for what is going on here. At first glance it is perhaps a bit perplexing; the core result is a well known (although not easy) result in homotopy theory from the 1930s; why is a modern PhD thesis spending hundreds of pages to prove it? The answer is that this a landmark effort within homotopy type theory (HoTT); indeed, it is perhaps the most substantial development of a major result using HoTT. Translating this result into the foundations provided by HoTT turns out to be far from trivial. At one level working within this type theory is helpful, for example obviating the need to ever prove any functions are continuous (well-behaved), because they must be continuous by construction. For example the difficulty of one particularly gnarly part of the standard development, proving that the associativity of the smash product is suitably continuous, simply disappears. Furthermore because the work is ‘synthetic’, in the sense of not being tied to any particular presentation of topology, it is highly general and the core development is not obscured by the particular details of a concrete choice (e.g. working via point-set topology, or simplicial sets).

However, there is a catch: the standard development of results in homotopy theory often contain intermediate constructions that are not well behaved in the sense that HoTT enforces, even where the final product is well behaved. This means that the standard development, at least in this case, cannot be translated line by line into the new formalism as one might naively hope: Brunerie reflects in his superbly reflective concluding chapter that he “often had to find completely different definitions, proofs or statements that would work in homotopy type theory”. The point of all this effort is, of course, not merely to reprove old results, but to pave the way for new advances in homotopy theory (and other areas of mathematics) using HoTT as a tool that avoids certain errors by enforcing certain invariants, in a style amenable to mechanisation.

Having said that, one notable aspect of this development is that it is not mechanised (encoded into a computer), although mechanisation is certainly discussed. This perhaps flies in the face of some people’s intuitions that type theory, resembling as it does a programming language, is innately connected to computer mathematics. Instead this is a significant development of pen and paper type theory, in the 'informal' style recommended by the original HoTT book.

Another interesting aspect of this thesis is its constructivity, and what that means in practice. At the end of chapter 3 it is proved that π4(S3)≅ℤ/nℤ for some integer n. The nature of constructive mathematics is that an existential result of this sort is impossible to prove without generating its ‘witness’; in other words we should have access to the value of the number n (in this case, 2). More precisely, if a witness is not immediately clear from the proof as written, the proof should compute until it produces the witness. This does not happen in this thesis; instead three more chapters are needed to prove that n is in fact equal to 2. What went wrong? One might wonder if the problem is that the proof is pen and paper and hence cannot compute, but although this is part of the problem it is not dispositive: one could try to carry out the computations by hand. Unfortunately these calculations proved too difficult to carry out. An early attempt to develop the thesis within cubical type theory, which is a fully constructive presentation of HoTT which hence would compute, did not prove successful and led Brunerie to conclude “for informal synthetic homotopy theory as done in this thesis, cubical ideas aren’t especially helpful in general”.

There is an important addendum to this picture however: I was recommended this paper in part because of its citation in a just released preprint, in which the results of this thesis (in slightly modified form) were fully mechanised in Cubical Agda by Axel Ljungström and Anders Mörtberg, allowing the ‘Brunerie number’ (that is, 2) to finally be computed from the proof that π4(S3)≅ℤ/nℤ for some integer n.

Discussing "Scalable Verification of Probabilistic Networks"

(Link)

Authors: Steffen Smolka (Cornell University), Praveen Kumar (Cornell University), David M. Kahn (Carnegie Mellon University), Nate Foster (Cornell University), Justin Hsu (University of Wisconsin), Dexter Kozen (Cornell University), and Alexandra Silva (University College London)

Reference: Smolka, Steffen, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva. "Scalable verification of probabilistic networks." In PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 190-203. 2019.

Why this paper? Cited by A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests and Lilac: a Modal Separation Logic for Conditional Probability

I built this blog around the idea of discoverability via Google Scholar both of new papers and, via their citations, influential older papers. Google Scholar generally does an excellent job of this (far better than the new wave of AIs with their tendency to hallucinate literature) but nothing is perfect, and the recommendations from this week are perhaps partly caused by misunderstanding that the word ‘guarded’, which is used a lot in some of my papers, is also used, but in a completely different way, in certain other papers. Still, the paper I got served by my self-imposed algorithm, while not exactly in my wheelhouse, is interesting enough so long as I don’t dive too deep into the technicalities.

This paper describes a system call McNetKAT, which is a grand pileup of acronyms: Mc for ‘Markov chain’, Net for ‘Network’, KA for ‘Kleen Algebra’, and ‘T’ for ‘(with) Tests’. The basic idea is to build capability for automatic verification on top of the programming language ProbNetKAT (Prob for ‘Probabilistic’), a small imperative language that allows one to specify the topology of a network and the policy for moving packets through it. The support for probability helps capture cases “from uncertainty about the inputs, to expected loads, to likelihood of device and link failures” that might effect networks. One can attempt to prove that the network program is fully correct, by showing that is equivalent to a magic network that teleports each packet to its correct destination, but the probabilities really come into play when you show a certain network program improves on another, in the sense that where both succeed they agree on their treatment of packets, but one is less likely to fail than another according to a given failure model on links or switches.

The ‘Mc’ comes into play because a new semantics is presented based on stochastic matrices / Markov chains, a notion of probabilistic transition system. These semantics are proved to be equal to the existing semantics in the literature, but are more amenable to automation. Programs are compiled into their semantics, and then passed to the linear algebra solver UMFPACK. It is shown that this treatment performs well against an alternative route involving compilation into the language of the probabilistic model checker PRISM, and against the (admittedly, more expressive) system Bayonet.

Discussing "The Lean Theorem Prover (System Description)"

(Link)

Authors: Leonardo de Moura (Microsoft Research Redmond)), Soonho Kong (Carnegie Mellon University), Jeremy Avigad (Carnegie Mellon University), Floris van Doorn (Carnegie Mellon University), and Jakob von Raumer (Carnegie Mellon University)

Reference: de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J. (2015). The Lean Theorem Prover (System Description). In: Felty, A., Middeldorp, A. (eds) Automated Deduction - CADE-25. CADE 2015. Lecture Notes in Computer Science(), vol 9195. Springer, Cham. https://doi.org/10.1007/978-3-319-21401-6_26

Why this paper? Cited by Encoding Dependently-Typed Constructions into Simple Type Theory and A Type-Based Approach to Divide-and-Conquer Recursion in Coq

Lean is something of a new kid on the block in the world of interactive theorem proving, coming out just 10 years ago, compared to 34 years for Coq and 36 for Isabelle. Nonetheless it has clearly had impact; for example this year’s CPP (Certified Programs and Proofs) conference, which I had the privilege to be a member of the program committee for, by my count had 7 of 25 accepted papers using Lean.

This short conference paper gives a brief and high-level description of the aims and design principles of the new theorem prover. It is neither a tutorial (see pdf) nor in-depth description of the nitty gritty of the implementation (for which see e.g. here). It does, perhaps, give some sense of why developing a new prover was thought to be desirable rather than simply using the established technologies, although it is rather polite and implicit about any comparisons with other provers. Lean, which like Coq is based on Martin-Löf dependent type theory, has a few features emphasised: its small trusted code base, its support for different proving styles (declarative à la Isabelle, or imperative-style tactics to generate proof terms), its flexible framework for supporting automation and talking to other software, its user interface, and its relatively fast speed and support for parallelism. Homotopy type theory is highlighted as one of the motivating application areas. The bulk of the paper is an informal description of the elaboration algorithm, which compiles definitions and proofs written in various styles down to the proof terms that the small trusted kernel can accept.