Tell me a story of logic

I have a little technical note that I'm working on, in which I tell a story about linear logic that I tried to work out a year ago and finally returned to with Bernardo Toninho and Yuxin Deng last week. But as I tried to write the introduction, the two-year-old voice in my head kept asking "why?" Why do I need to tell this story? What's the point? The resulting thoughts don't really belong in the technical note I wanted to write, but I hope they're just barely coherent enough that they're worth putting here. (Note: there is a similar discussion to this one in Section 3 of my thesis proposal.)

Big picture: before we can contemplate any discussion of the formal correctness of any system (a logic, type theory, programming language, cryptographic protocol, or self-driving car) - before we can even ask ourself what "correctness'' means - we have to have a way of formally specifying the system itself. Mathematicians do this by defining sets, category theorists by enumerating universal mapping properties. However, if you're writing down theorems to be checked by a computer, there's almost exactly one game in town: systems for mechanized mathematics have a built-in facility for directly giving (co)inductive specifications of systems.

A tool's interface for describing inductive specifications is, therefore, a matter of some importance. In most systems, the statement of an inductive specification looks something like a datatype declaration in a programming language in ML or Haskell. One system for mechanized mathematics, Twelf, takes a rather different approach. Rather than directly specifying an inductive structure, Twelf users specify a signature of type families and constants in the dependent type theory LF. If you asked someone about this while they were in a hurry to catch a plane, they'd probably respond "oh, that's what adequacy theorems are for" and run away.

A word on adequacy

In the first paper on LF, Harper, Honsell, and Plotkin discuss adequacy theorems. When we write down a bunch of type families and constants in an LF signature, that means that we can form a certain (inductively-defined!) set of terms. To use a standard example, given the LF signature

  nat: type.

  z: nat.

  s: nat -> nat.

we can create well-typed terms of type nat that look like z, (s z), (s (s z)), and ((λx. s x) (s z)). That fourth example has a β-redex that, when we reduce it, turns it into the third example. We usually say that the above LF specification is adequate because there is a one-one-correspondence between natural numbers and normal terms of type nat in this signature.¹ In general, to quote Harper and Licata's 2007 "Mechanizing metatheory in a logical framework",

An LF representation of a language is adequate iff it is isomorphic to the informal definition of the language.

I'm currently thinking that this might be the wrong slogan, because the imprecision of "informal" leads to seemingly inevitable misunderstandings. Another slogan that I might consider in its place is that an LF specification is adequate iff it is isomorphic to the inductive specification of the language. It's just really very deeply ingrained in our collective heads that when we're writing down horizontal lines on paper, that means an inductive specification. But perhaps that's not giving LF enough credit! There's no reason to cede that my scratches on a whiteboard have any special spiritual relationship with inductive definitions and not LF signatures (or sets in ZFC or constructions in category theory, for that matter).

Taking the view that adequacy relates the canonical forms of LF to some inductively defined structure ("on paper" or otherwise) has two advantages that I see. First, it turns adequacy into something that takes place entirely within formal mathematics. In fact, we have a pretty clear understanding of how to write "first-order" or "concrete" LF types that encode inductive definitions (hint: never allow left-nested arrows). But this means that we can prove adequacy theorems in Twelf. My Twelf code proving a bijection between de Bruijn lambda calculus terms and HOAS lambda calculus terms is, in this view, part of an adequacy theorem.² The second advantage, in my mind, is it clarifies why we never formally prove adequacy with respect to our "informal definitions" (a point that Daniel Lee and I poked a bit of fun in our SIGBOVIK 2007 paper Manifest Adequacy). When I've been using Adga for awhile, I think of my on-paper notation as corresponding to inductive definitions (or, occasionally, inductive-recursive definitions, the more powerful variant of inductive definitions available in Agda). When I've been using Twelf for awhile, I think of my on-paper notation as corresponding to LF signatures that use higher-order abstract synatx. It's only in the event that I want to know that these two ways of formalizing the same system coincide that I would actually think about adequacy in practice. To reempahsize, in this event adequacy is an entirely formal concept.

Why logical frameworks?

There's no contrarian impulse that lead to LF being used to encode systems. Harper, Honsell, and Plotkin made the point as well as I could hope to:

The structure of the LF type system provides for the uniform extension of the basic judgment forms to two higher-order forms introduced by Martin-Löf, the hypothetical, representing consequence, and the schematic, representing generality.

There are two important points to make about the above quote. The more obvious one is that LF, compared to "raw" inductive definitions, gives a clean notion of hypothetical reasoning and uniform substitution (the basis of what was later termed "higher-order abstract syntax"). The less obvious point is that, in the above quote, Harper, Honsell, and Plotkin are referencing Martin-Löf's "On the meaning of logical constants and the justification of the logical laws," which isn't actually about LF. Rather, it's a story about how we understand the meaning of propositions and how we establish that a logic's definition makes sense in the presence of a uniform notion of hypothetical judgments.

Martin-Löf's discussion, which Pfenning and Davies termed the "judgmental methodology" in their their judgmental reconstruction of modal logic, is important for people who write systems in Twelf because it sets up a particular world-view that maps quite well onto formalization in LF. To put it another way, the judgmental methodology is one important source of intuitions that guide the mental process of mapping between our "on-paper" notation and LF signatures. And so it's no accident that 1) we use Twelf a lot at Carnegie Mellon 2) our student reading group usually reads On the meaning of logical constants and the justification of the logical laws at least once every other year. The judgmental properties underlying LF and Martin Löf's reconstruction are the same, so understanding the judgmental methodology is a good way of understanding LF formalization.

This continues to be the case in the Linear LF extension to LF, where linear hypothetical assumptions are understood to be resources that will be consumed in the service of building a goal. The underlying story here, which Wikipedia originally attributes to Lafont, is called the resource interpretation, and it allows us to understand how to do things like represent programming languages with state conveniently, because "a bunch of memory" is a concept that can be represented as "a bunch of resources." The story that we tell about linear logic - the resource interpretation - is important in part because it gives us intuitions for understanding LLF formalizations.

I don't know that I can speak for where my intuitions about inductive definitions come from - as I've said before, computer scientists tend to treat them as pretty foundational. On the other hand, it's difficult to really use the "raw" inductive definitions provided natively by most non-Twelf provers to reason about programming languages, which is why there has been much recent (and, from an outside perspective, seemingly quite successful) work aimed at providing the right tool support for specifying and reasoning about programming languages in highly-developed proof assistants like Coq. The only danger here is, as soon as you start adding layers of interface between yourself and inductive definitions, the question of adequacy (the informal version, at least) again raises its head: there's not necessarily the same Martin-Löfian story guiding you, so where are your intuitions about the correctness of your system coming from? How would you actually prove that it corresponds to an ostensibly equivalent LF signature?

This, in turn, is one reason why two-level approach have been recently popularized by Felty's Hybrid system and Gacek's Abella. In these systems, there's a specially supported logical layer where one can use the same kind of intuitions we use in LF encodings. LF or LLF could, in fact be used for this logical layer, though these two systems use different variations on that theme. The second layer is a separate facility for reasoning about these encodings.

I'll stop here, though one argument I might be interested in trying to make in the future is that Twelf itself is actually the original two-level approach. There's an even stronger argument to be made in the case of HLF, Jason Reed's implementation of meta-reasoning for LLF on top of Twelf. However

¹ We usually say canonical terms or canonical forms, not normal terms. The canonical forms are the β-normal η-long terms. However, η-expansion doesn't mean anything for this example.

² It would be a full adequacy theorem if I'd shown that the bijection was compositional - that substitution on the de Bruijn terms means the same thing as substitution that LF gives us for free - but I didn't prove that part. Perhaps I should.

Request for Typestate, Part 2: Linear Types, Now!

Part 2 in a series. Part 1 began with a discussion hypothetical discussion of a ML-like language with linear types.

So in my previous post, I used the REPL loop of an "Imaginary Future Linear ML." In the following month, I've learned that there are no less than three different proposals of Imaginary Future Linear ML. Two of them, Alms and LinearML, are implemented systems that you can presumably download and run onto the device that you're using to read this very blog post!¹ The third, F-Pop by Mazurak et al, is, I believe, less seriously implemented but is formalized in Coq (which is also awesome: three cheers for mechanized metatheory!).

I was actually pleased with how much I "guessed correctly" in my discussion. For instance, Alms is a serious implementation of a language with affine, not linear, types: if you recall, affine functions can't use their arguments twice, but they can avoid using them at all. One argument from the Alms designers, which I had not considered, is that requiring a linear type discipline - where all variables get used exactly once along every "control path" - can make it rather difficult to work with handled exceptions.

Another thing that I "guessed" was in Take 3, when I suggested that we might want some syntactic sugar to make code look more like "methods" - the print method takes a string and a linear reference to a string and returns a new linear reference to that string, so why don't we have syntax that supports writing (print "Hello World" outstream) instead of (let outstream = print "Hello World" outstream). The F-Pop paper explicitly discusses this kind of notation in Section 5.2. I like that this is something they considered, though I'm still a little unsure how I feel about it "in practice." What it's doing is capturing a common intuition, that an argument, passed by reference, is both an input and an output. But how much of this intuition is fundamental, and how much is it based on path dependence - we happened to start out with languages like C and Java that force functions to have only one "official" output, so are we just used to being forced into using this unnatural design pattern?

¹ Caveat 1: well, as long as you're not using iOS. (I just got an iPad. I am not proud of this but yes, it is shiny.) Caveat 2: I couldn't get either Alms or LinearML to run on my laptop.

Request for Typestate, Part 1

Part 1 of a series. If you're interested in Imaginary Future ML, a number of proposals exist: see Part 2.

Recently I have been trying to understand typestate, since a lot of my friends, hallmates, and fellow distance runners have written implementations, papers, Ph.D. theses, and SIGBOVIK presentations on the topic. A conversation with Ron Garcia helped me get the first idea of what is going on and how it relates to linear type systems, a topic I do feel like I understand.

Some background, as I understand it. The word "typestate" was introduced by Strom and Yemini way back a long time ago in 1984 in a paper entitled "Typestate: A Programming Language Concept for Enhancing Software Reliability" (Jonathan Aldritch has posted the PDF here). It was an attempt to capture the fact that function calls often have a "do this, then do that, then don't do that anymore" kind of flavor. The most obvious and simple example is one that most every programmer has encountered, thanks to C's ubiquity:



In other words, we create a pointer by mallocing it, and then we can use that pointer as long as we want to, but if we free it we can't use that pointer anymore. (Well, we can, but we're not supposed to, C sucks, whatever.) Okay, but now you're scratching your head thinking that this is basically why modern humans use garbage collection. Well, sure, but while this solves a particular problem, the problem is really a pattern of problems, and the pattern just re-asserts itself in different ways. For instance, take this interaction with SML/NJ's toplevel:

  $ sml
  Standard ML of New Jersey v110.70 [built: Wed Jun 17 16:24:00 2009]
  - val FILE = TextIO.openOut("foo.txt");
  val FILE = - : TextIO.outstream
  - TextIO.output(FILE, "Hello world\n");
  val it = () : unit
  - TextIO.closeOut(FILE);
  val it = () : unit
  - TextIO.output(FILE, "I've got a bad feeling about this\n");

  uncaught exception Io [Io: output failed on "foo.txt", closed stream]
    raised at: Basis/Implementation/IO/text-io-fn.sml:443.14-443.56

What's happened here is that we've run afoul of exactly the same pattern that we know from C.



Because we're in a safe language, the results are less dire; a dynamic exception gets thrown rather than memory being silently corrupted. However, the problem remains: it seems like this is the sort of thing we should be able to statically preclude (using a type system), or at least warn programmers about ahead of time (using a static analysis).

Typestate-oriented programming

Both of these approaches (type systems and static analyses) have been investigated thoroughly by my friends in Jonathan Aldrich's group, such as Kevin Bierhoff, Nels Beckman, Ciera Jaspan, Karl Naden, Roger Wolff, and Ron Garcia. The following example is a way of taking that doomed ML snippet above and making it a piece of typestate-checked code; it's mostly copied from Typestate Oriented Programming by Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks and was presented at ONWARD 2009.

  state File {
    public final String filename;
  }

  state OpenFile extends File {
    private CFilePtr filePtr;
    public void write(str : String) { ... }
    public void close() [OpenFile>>ClosedFile]
    { ... }
  }

  state ClosedFile extends File {
    public void open() [ClosedFile>>OpenFile]
  }

The idea here is that a File is a file that might be open or closed; you can only read from an OpenFile, which is a subtype of File. That annotation on the close() and open() methods is telling us that those functions actually change the type of the object they're acting upon; the typesystem has to work accordingly to make sure you only close or read from an OpenFile, even if though, after you close it, the object has "become" exactly the thing - a ClosedFile - that you were making sure it wasn't before.

I have some particular questions about the nature of the thing called "subtyping" in typestate oriented programming that I hope to get to in a separate post, but I hope this gives a decent overview of how typestate intuitively works even if it doesn't give much intuition as to how the typing rules "actually" work. As it turns out, the type theory behind typestate-oriented programming uses ideas from linear logic, which can also be used to directly solve the motivating problem. What I really hope to explore in this series of posts is the way in which typestate - which is mostly being investigated in object oriented settings - can (or can't) be understood as a linear type discipline in a functional programming language.

Linear Types

From a programmer's perspective, linear logic is a functional programming language where all variables only get to be mentioned once. There's an additional requirement, which is that every variable must be used once, but sometimes people ignore this requirement: the system where variables are mentioned no more than once is technically an "affine" system and not a "linear" one, but it's common to call affine systems linear anyway, because the more general term is "substructural" and "substructural" is for some reason a word that people get scared by. (This turns out to be pretty problematic for me, but that's a different blog post.)

So, nothing to be scared of, can't use variables twice. Let's see what happens with our interaction with SML:

  $ smlinear
  Imaginary Future Linear ML [built: IN THE FUTURE]
  - val FILE = TextIO.openOut("foo.txt");
  val FILE = - : TextIO.outstream
  - TextIO.output(FILE, "Hello world\n");
  val it = () : unit
  - TextIO.closeOut(FILE);
  stdIn:1.17-1.21 Error: unbound variable or constructor: FILE
  Variable "FILE" was previously in scope as a linear resource,
    but that resource already consumed

Oh dear, that doesn't work at all - we can't close the file or even write to it twice! This is our fault; when we ported the SML Basis Library from SML/NJ to Imaginary Future Linear ML, we needed to make some changes to the way we deal with TextIO. Here's (part of) the old signature for TextIO, with the arrows -> turned into lollipops -o to emphasize that we're in linear logic now. (Again, nothing scary, it just means that variables can only be mentioned once.)

  signature OLD_TEXT_IO = sig
    type outstream
    val openOut : string -o outstream
    val output : outstream * string -o unit
    val close : outstream -o unit
  end

This signature had just the right type when we could reuse the variable FILE that we got from openOut, but now, in Imaginary Future Linear ML, we can't.

Take 1: Restoring the old behavior

It's ridiculous, however, to make the output stream go away forever whenever we write to it! So what do we do? Well, all we need is for the functions that currently return unit to give us back a new object of type outstream, and then we can use it again!

  signature NEW_TEXT_IO_1 = sig
    type outstream
    val openOut : string -o outstream
    val output : outstream * string -o outstream
    val close : outstream -o outstream
  end

With this new signature for TextIO, we could have exactly the same (failed) interaction with the toplevel that we had before, the difference is that, now, we always bind a new variable when we run a function so that we have an outstream object to use in the future.

  $ smlinear
  Imaginary Future Linear ML [built: IN THE FUTURE]
  - val FILE1 = TextIO.openOut("foo.txt");
  val FILE1 = - : TextIO.outstream
  - val FILE2 = TextIO.output(FILE1, "Hello world\n");
  val FILE2 = - : TextIO.outstream
  - val FILE3 = TextIO.closeOut(FILE2);
  val FILE3 = - : TextIO.outstream
  - TextIO.output(FILE3, "I've got a bad feeling about this\n");

  uncaught exception Io [Io: output failed on "foo.txt", closed stream]
    raised at: Basis/Implementation/IO/text-io-fn.sml:443.14-443.56

Okay, well, why did I show an example that didn't solve the problem at all? Because it's important to realize that we haven't really lost any expressiveness in the language: even though we have a more restrictive system that prevents us from using variables twice, we can still express most of the things we could before.

(Side note: in the case of the strictly-linear variant of Gödel’s System T, it's actually been proven that we lose exactly nothing in terms of mathematical expressiveness by using the more restrictive type system, which is neat.)

Take 2: Actually fixing the problem

So, intuitively, we know what to do here: once we've closed an outstream we shouldn't be able to re-close it or output to it. The easiest solution is to make the function close have the type outstream -o unit - that way, closing an outstream consumes the variable representing the output stream and leaves us with no way to even mention it.

  signature NEW_TEXT_IO_1 = sig
    type outstream
    val openOut : string -o outstream
    val output : outstream * string -o outstream
    val close : outstream -o unit
  end

This suffices to turn our original dynamic exception into a static type error like the Variable...already consumed error I made up earlier.

Take 3: Matching the typestate example

For the sake of completeness, let's think about how our example looks different from the typestate example. The big difference is that all the functions in the typestate example are void: they don't output anything, they just change the type of their argument. But I believe that this is actually something that it would be reasonable to mimic in a linear system like "Imaginary Future Linear ML." The first step is to say: well, when I consumed FILE there was no longer a FILE hanging around, so why don't I just reuse that variable name?

  $ smlinear
  Imaginary Future Linear ML [built: IN THE FUTURE]
  - val FILE = TextIO.openOut("foo.txt");
  val FILE = - : TextIO.outstream
  - val FILE = TextIO.output(FILE, "Hello world\n");
  val FILE = - : TextIO.outstream
  - val FILE = TextIO.closeOut(FILE);
  val FILE = - : TextIO.outstream
  - TextIO.output(FILE, "I've got a bad feeling about this\n");
  stdIn:1.17-1.21 Error: unbound variable or constructor: FILE
  Variable "FILE" was previously in scope as a linear resource,
    but that resource already consumed

The second step is to consider that the typestate-oriented examples really do have "outputs" - their outputs are the new states of the this object. This would be easy syntactic sugar to whip up, just let val output : [outOpen >> outOpen] * string -o unit mean val output : outOpen * string -o outOpen and give the following signature

  signature NEW_TEXT_IO_2 = sig
    openOut : string -o outOpen
    output : [outOpen >> outOpen] * string -o unit
    closeOut : [outOpen >> outClosed] -o unit
    reopenOut : [outClosed >> outOpen] -o unit
  end

With this use of syntactic sugar, we could support the following interaction with our pretend ML:

  $ smlinear
  Imaginary Future Linear ML [built: IN THE FUTURE]
  - val FILE = TextIO.openOut("foo.txt");
  val FILE = - : TextIO.outOpen
  - TextIO.output(FILE, "Hello world\n");
  val it = () : unit
  - TextIO.closeOut(FILE);
  val it = () : unit
  - TextIO.output(FILE, "I've got a bad feeling about this\n");
  stdIn:6.1-6.59 Error: operator and operand don't agree [tycon mismatch]
    operator domain: TextIO.openOut * string
    operand:         TextIO.closeOut * string
    in expression:
      TextIO.output (FILE,"I've got a bad feeling about this\n")

I think that's pretty nice.

Conclusion

I think the lesson of this first discussion is that, when relating linear functional programming languages to imperative programming languages, it's useful to think of object passed to functions as being "lost" to that function and then automatically "re-bound" with the same name when the function returns. Once we make this step, the notion that the re-bound variable can have a different type - which is one key insight of typestate-oriented programming - seems quite natural.

It's important to note that none of the stuff I said about linearity and state is at all novel; for further reading see Wadler's paper Linear Types Can Change The World! (warning: .ps) or David Walker's chapter "Substructural Type Systems" in Advanced Topics in Types and Programming Languages. Those two sources just about cover the background reading; if anyone has other suggestions please feel free to put them in the comments.

Two new papers

I have a post on typestate that has been languishing while I've been spending a lot of time on CMU's admissions committe, but now that that's over I hopefully will be able to get back to it. But first, two papers:

Logical Approximation for Program Analysis

My paper with Frank Pfenning, Logical Approximation for Program Analysis, has been accepted to HOSC. This paper extends of the work from the PEPM 2009 paper Linear logical approximations [ACM Link] - the acceptance is actually to a HOSC special issue on PEPM 2009. However, this paper also synthesizes a lot of stuff from our LICS 2009 paper Substructural Operational Semantics as Ordered Logic Programming. The point of this journal paper is to provide a story about allowing substructural operational semantics specifications of programming language, written in the style of the LICS 2009 paper/my thesis proposal, to be approximated. The approximation process lets us derive program analyses like control flow and alias analysis in the style of the PEPM 2009 paper.

Anyway: PDF, which I'm still polishing for final submission this weekend.

It occurs to me that I should write some more substructural operational semantics posts on this blog, seeing as that's my thesis topic and all.

Constructive Provability Logic

Since Bernardo and I got the principles of constructive provability logic nailed down, we've done a little more exploring. The most important thing about this paper, relative to the technical report, is that it presents a less restricted version of constructive provability logic (the "de-tethered variant" CPL*); I think this less restricted version is going to be critical to understanding logic programming through the lens of constructive provability logic, which is my ultimate goal for the project. The second new thing about the paper is that we nailed down (with one perplexing exception) which of the "normal" axioms of intuitionistic modal logic do or don't hold.

What does this mean? Well, any classical logician will tell you that, in order to be a modal logic, you have to obey one axiom - the "K" axiom, □(A → B) → □A → □B - and one rule, which is that if you can prove A with no assumptions then you can also prove □A ("necessitation"). And any intuitionistic modal logic worth its salt is going to do the same, so far so good. However, intuitionstic modal logic also has a possibility modality ◇A. In classical logic saying something is possible is the same as saying that it's not necessarily false, so ◇A is defined as ¬□¬A. But in intuitionistic logic we tend to think of possibility as a genuinely different thing, and that's where stuff gets complicated. The two most important proof theories for intuitionistic modal logic are probably Alex Simpson's IK - which describes a whole bunch of intuitionistic modal logics - and Pfenning-Davies S4, which describes S4. Some of the axioms that Simpson claims are fundamental to intuitionistic modal logics, like (◇A → □B) → □(A → B), don't hold in Pfenning-Davies S4; it turns out that particular axiom doesn't hold in constructive provability logic, either.

As we discuss in the paper, it seems like the de-tethered variant, CPL*, lies between Pfenning-Davies S4 and Simpson-style S4 on the "which axioms hold" meter, whereas CPL (the tethered version of constructive provability logic from the tech report) may or may not have the same "normal" axioms as Pfenning-Davies; we are currently stuck on whether the ◇◇A → ◇A holds in CPL - it definitely holds in CPL*, Simpson-style S4, and Pfenning-Davies S4, but we are a bit perplexed by our inability to prove or disprove it in CPL.

Here's the PDF, and here's the bitbucket repository with all our Agda. As a side note, "oh, all these proofs are in Agda so we're not discussing them" makes the whole "omitted due to space" thing feel way, way less sketchy. This is just a submission at this point, so comments are especially welcome!

Two twists on a graph

So, something that shouldn't be terribly surprising is that one can take a graph (edges and vertices) and represent it as a set of vertices. This innocent-looking cube will be our example:

edge(a, b)    edge(a, c) edge(c, d) edge(b, d) edge(a, e) edge(b, f)

edge(c, g)    edge(d, h) edge(e, f) edge(e, g) edge(g, h) edge(f, h)

vertex(a) vertex(b) vertex(c) vertex(d) vertex(e) vertex(f) vertex(g) vertex(h)

We'll collect this set of facts and call the collection of propositions (20 atomic propositions in all) GRAPH.

Also not terribly interesting, but maybe ever-so-slightly interesting, is that one can take this representation of a graph and do forward-chaining logic programming with it. Consider, for example, the following forward-chaining logic program made up of two rules.

  edge(Y,X) <- edge(X,Y).
  reachable(Y) <- edge(X,Y), reachable(X), vertex(Y).

These are just logical propositions; the upper-case identifiers are implicitly universally quantified, the comma represents conjunction, and (following common convention for logic programming) we write implication backwards as B <- A instead of A -> B. We'll call this collection of two rules REACH.

Recall that the behavior of a forward chaining logic program is to take facts that it has and learn more facts. If we just throw the graph at this program, it will use the first rule to derive all the backwards edges (edge(b,a), edge(c,a), and so on) but nothing else. If we add an additional single fact reachable(a), then our forward chaining logic program will furiously learn that b, c, and indeed all the other vertices are reachable. We can rephrase this in the following way: for a specific choice of X and Y, there is a path from X to Y if and only if there is a derivation of this sequent:

  GRAPH, REACH ⊢ reachable(X) -> reachable(Y)

In fact, the forward chaining logic programming engine, given reachable(X) for some specific X, will derive a fact of the form reachable(Y) for every reachable Y.

Twist 1: weighted logic programming

The first interesting twist on our boring program is this: we consider those proofs of the sequent

  GRAPH, REACH ⊢ reachable(X) -> reachable(Y)

and we ask, what if some proofs are better than others? One way to introduce a metric for "what is better" is to say that every one of those atomic propositions has a cost, and every time we use that atomic proposition in a proof we have to pay that cost: we want the cheapest proof:

edge(a, b) = 66    edge(a, c) = 53 edge(c, d) = 12 edge(b, d) = 57 edge(a, e) = 19 edge(b, f) = 53

edge(c, g) = 92    edge(d, h) = 6 edge(e, f) = 8 edge(e, g) = 84 edge(g, h) = 162 edge(f, h) = 4

vertex(a) = 0 vertex(b) = 0 vertex(c) = 0 vertex(d) = 0 vertex(e) = 0 vertex(f) = 0 vertex(g) = 0 vertex(h) = 0

This sort of problem is amenable to what is called weighted logic programming, a declarative way of specifying dynamic programming problems. In this case, if the edge weights are all positive, this is a declarative way of specifying Dijkstra's algorithm for single-source shortest path. Before, our forward-chaining logic programming engine took a single fact reachable(X) and computed all the nodes reachable from X. Now, our weighted logic programming engine takes a single fact reachable(X) with cost 0 and computes the minimum-cost route to every node reachable from X.

Related work

In fact we can play the same game on any semiring as long as the "score" of a proof is the semiring product of the score of the axioms (in this case, "plus" was the semiring product) and the way we combine the scores of different proofs is the semiring sum of the scores of the two proofs (in this case, "min" was the semiring sum). This sort of generalization-to-an-arbitrary semiring is something that isn't noticed as much as it probably should be. If you're interested in learning or thinking more about weighted logic programming, the first eleven pages of the paper I coauthored with Shay Cohen and Noah Smith, Products of Weighted Logic Programs, were written specifically as a general audience/programming languages audience introduction to weighted logic programming. Most of the other literature on weighted logic programming is by Jason Eisner, though the semiring generalization trick was first extensively covered by Goodman in the paper Semiring Parsing; that paper was part of what inspired Eisner's work on weighted logic programming, at least as I understand it.

Twist 2: linear logic programming

Another direction that we can "twist" this initially graph discussion is by adding linearity. Linear facts (in the sense of linear logic) are unlike "regular" facts - regular facts can be used any number of times or used not at all - they are persistent. Linear facts can only be used once in a proof - and in fact, they must be used once in a proof.

We've had the vertex propositions hanging around all this time and not doing much; one thing we can do is make these vertex propositions linear, and we'll make the reachable propositions linear as well. In this example, we'll designate linear propositions by underlining them and coloring them red; our program before turns into this:

  edge(Y,X) <- edge(X,Y).
  reachable(Y) <- edge(X,Y), reachable(X), vertex(Y).

By the way, if you're familiar with linear logic, the logical meaning of this formula is captured by the following two propositions written properly in linear logic:

  ∀x. ∀y. !edge(x,y) -o edge(y,x).
  ∀x. ∀y. !edge(x,y) -o reachable(x) -o vertex(y) -o reachable(y).

We'll talk a little bit more about this specification (call it LREACH) shortly; for the moment let's switch to a different train of thought.

Greedy logic programming with linear logic

When we talked before about the cost of using a fact in a proof, we were actually assuming a little bit about proofs being focused; we'll talk a little bit about focusing and synthetic rules in this section (see this old blog post for background).

If we make all of our atomic propositions positive, then the synthetic rule associated with the critical second rule above ends up looking like this:

  Γ, edge(X,Y); Δ, reachable(Y) ⊢ C
  ---------------------------------------------
  Γ, edge(X,Y); Δ, reachable(X), vertex(Y) ⊢ C

Recall that we like to read forward chaining rules from the bottom to the top. If we assume that the context only ever contains a single reachable(X) proposition, then we can think of the linear context as a resource consuming automaton that is in state X. At each step, the automaton consumes an available resource vertex(Y) with the constraint that there must be an edge from X to Y; the automaton then transitions to state Y.

One efficient way to give a logic programming semantics to these kind of forward-chaining linear logical specifications is to just implement an arbitrary run of the automaton without ever backtracking. This is a greedy strategy, and it can be used to efficiently implement some greedy algorithms. This was the point of Linear Logical Algorithms, a paper I coauthored with Frank Pfenning. One neat example from that paper was the following graph program, which computes a spanning tree for a graph rooted at the vertex a:

  edge(Y,X) <- edge(X,Y).
  intree(a) <- vertex(a).
  tree(X,Y), intree(Y) <- edge(X, Y), intree(X), vertex(Y).

This program works like another little resource-consuming automaton that, at each step, consumes a vertex resource to add a non-tree vertex to the tree along a newly added tree edge. This is, incidentally, the same way Prim's algorithm for minimum spanning trees progresses.

Hamiltonian paths in linear logic

The greedy strategy where we look at one possible set of choices is very different than the behavior of our briefly-sketched forward-chaining persistent and weighted logic programming engines. The latter worked by taking some initial information (reachable(X) for some X) and finding, all at once and with reasonable efficiency, every single Y for a given X such that the following sequent holds:

  GRAPH, REACH ⊢ reachable(X) -> reachable(Y)

Call the (persistent) edges EDGE, and the (linear) vertices VERT. Now we can look at the (seemingly) analogous problem stated in linear logic to see why it is in practice, so different:

  LREACH, EDGE; VERT ⊢ ⊢ reachable(X) -o reachable(Y)

Because linear logic requires that we eventually use every resource in VERT, this derivation corresponds to a run of the automaton where the automaton visited every single node and then ended at Y. If we consider just the case where X and Y are the same, complete derivations correspond to Hamiltonian tours.

By adding linearity, we've made the forward chaining language more expressive, but in doing so we created a big gulf between the "existential" behavior (here's one way the automaton might work, which we found by being greedy) and the "universal" behavior (the automaton can, potentially, follow a Hamiltonian path, which we learned by calling a SAT solver). This gap did not exist, at least for our running example, in the persistent or weighted cases.

Combining the twists?

Both linear logic programming and weighted logic programming arise start from a simple observation: the shape of proofs can capture interesting structures. The "structure" in this case was a path through a graph; in weighted logic programming the structures are often parse trees - you know, "boy" is a noun, "fast" is an adverb, "the" is a demonstrative adjective, and the two combined are a noun phrase, until you get a tree that looks something like this:

    Sentence 
      /  \
     NP  VP
    /|   | \
  /  |   |  \
 D   N   V   A
 |   |   |   |
the boy ran fast

(More on this in the "Products of Weighted Logic Programs" paper.)

Weighted logic programming enriches this observation by allowing us to measure structures and talk about the combined measure of a whole class of structures; linear logic, on the other hand, greatly improves on the things that we can measure. But what about using the observations of weighted logic programming to assign scores in the richer language of linear logic programming? What would that look like? I'll give a couple of sketches. These are questions I don't know the answers to, don't know that I'll have time to think about in the near future, but would love to talk further about with anybody who was interested.

Minimum spanning tree

I commented before that the logic programming engine described in Linear Logical Algorithms implements something a bit like Prim's algorithm to produce a graph spanning tree. In fact, the engine we described does so with provably optimal complexity - O(|E| + |V|), time proportional to the number of edges in the graph or the number of vertices in the graph (whichever is larger). What's more, we have a good cost semantics for this class of weighted logic programs; this means you don't actually have to understand how the interpreter works, you can reason about the runtime behavior of linear logical algorithms on a much more abstract level. The recorded presentation on Linear Logical Algorithms, as well as the paper, discuss this.

If we replace a queue inside the engine with an appropriately configured priority queue, then the logic programming engine actually implements Prim's algorithm for the low cost of an log(|V|) factor. But can this be directly expressed as a synthesis of weighted logic programming and linear logic programming? And can we do so while still maintaining a reasonable cost semantics? I don't know.

Traveling salesman problem

While minimum spanning tree is a greedy "existential" behavior of linear logic proof search, the weighted analogue of the Hamiltonian Path problem is just the Traveling Salesman problem - we not only want a Hamiltonian path, we want the best Hamiltonian path as measured by a straightforward extension of the notion of weight from weighted logic programming.

Not-linear logics?

Adding some linearity turned a single-source shortest path problem into a Hamiltonian path problem - when we turned vertices from persistent facts into linear resources, we essentially required each vertex to be "visited" exactly once. However, an affine logic interpretation of the same program would preserve the resource interpretation (vertices cannot be revisited) while removing the obligation - vertices can be visited once or they can be ignored altogether.

This makes the problem much more like the shortest path problem again. If edge weights are positive, then the shortest path never revisits a node, so it's for all intents and purposes exactly the shortest path problem again. If edge weights are negative, then disallowing re-visiting is arguably the only sensible way to specify the problem at all. Can this observation be generalized? Might it be possible to solve problems in (weighted) affine logic more easily than problems in weighted linear logic?

Principles of Constructive Provability Logic

So I think Bernardo and I have finally finished slaying the beast of a technical report we've been working on on-and-off all semester. I previously mentioned this tech report here. The intended audience for this paper is anyone who has read "A Judgmental Reconstruction of Modal Logic" (also known ubiquitously to CMUers as "Pfenning-Davies") and/or who has tasteful ideas about natural deduction and some notion of how modal logic works.

Unlike this blog post, which I wrote in 15 minutes while tired, Bernardo and I have worked very, very hard on trying making this report foundational and clear, and I'd definitely appreciate any feedback people have (large and small) since hopefully this won't be the last time I talk about constructive provability logic. Even if the feedback is that my jokes are really dumb and don't add anything to the paper (I should mention for Bernardo's sake that all the dumb jokes are my fault).

Principles of Constructive Provability Logic
Robert J. Simmons and Bernardo Toninho.
[PDF], [Agda tarball], and [Agda HTML]

Abstract: We present a novel formulation of the modal logic CPL, a constructive logic of provability that is closely connected to the Gödel-Löb logic of provability. Our logical formulation allows modal operators to talk about both provability and non-provability of propositions at reachable worlds. We are interested in the applications of CPL to logic programming; however, this report focuses on the presentation of a minimal fragment (in the sense of minimal logic) of CPL and on the formalization of minimal CPL and its metatheory in the Agda programming language. We present both a natural deduction system and a sequent calculus for minimal CPL and show that the presentations are equivalent.

The topic of the paper is "constructive provability logic" (CPL), a rich vein of logic that we've only just begun exploring.¹ The abstract and the introduction point out our primary reason for being interested in this logic: we want to give a general, satisfying, and proof-theoretic account for negation in logic programming. In fact, I've already gone out on a limb and written out the design of a distributed logic programming language based on a variant of CPL that I haven't quite-just-yet gotten around to entirely writing down. But I'm also just starting to implement the logic programming language, so it's not like I'm that far ahead of myself. The classical modal logic (which has about a dozen names but let's call it GL for Gödel-Löb) that we're intuitionisticing² about with has deep connections to everything from Gödel's incompleteness theorems to the denotational semantics of programming languages (it's the "modal" in the very modal models).

What's so special about this logic? Well, when you're working in the Kripke semantics of a modal logic, you should think of yourself as standing and a particular world and looking at some other worlds (these worlds are called accessible, and an accessibility relation determines which worlds are accessible). Maybe there aren't any! Maybe there are. Maybe you can see the world you're standing on, like being in a hall of mirrors. Maybe you can see one other world, and then beyond that world you can see back to the world you're standing on, like being in Pac-Man. The situation for GL and CPL is that not only can you not see yourself, you can't see forever - you can look past the accessible worlds to the worlds accessible from those (the "2-accessible" worlds, say) and then to the 3-accessible worlds... but this can't go on forever (jargon: the accessibility relation is "converse well-founded," there are no infinite ascending chains).

If you find yourself in a planetary system with a converse well-founded accessibility relation such as this one, the key is that, if you ever find your spaceship and go to one of those accessible worlds, there's now strictly less to see. Put another way, there's necessarily a little more going on where you're standing than in the places you're looking at. If this leads you to think that the places you can see are kind of an approximation of the place where you are, you're heading towards the approximation ("modal model"-esque) interpretation of GL. If you think "oh, the little more going on could refer to logical consistency," then you're heading towards the "provability" interpretation of GL. Perhaps the provability interpretation will inspire you to send a logician on every world and allow each logician to reason about the logical consistency of all the logicians he can see.³ Sure, you'll never get enough watchers for all the watchmen, but that is an occupational hazard of modern mathematics.

Anyway, I'll stop there: hopefully the details in the tech report are much, much clearer than the discussion in the preceding few paragraphs.

---

¹ I don't know when I started referring to my life as "working in the logic mines," it's really not fair to miners who have a really hard job that often isn't fun, unlike me. Maybe I'm just jealous of Mary's hat
² Intuitionisticing. v. To experimentally take a classical logic and try to deduce constructive, intuitionistic principles and proof theories out of it: Rowan and Alex were intuitionisticing about with propositional S4, and they both came up with things that seemed internally consistent but that were oddly incompatible.
³ Hey! It's a bad idea to use male pronouns to describe mathematicians! Okay, would you rather me be shooting female logicians into space for no compelling reason? Alright then.

Totally nameless representation

[Note: I am unaware of any truly original content in this post; when I say "we picked this up from Dan" it doesn't imply Dan worked it out himself; when I say "we worked this out" I don't have any reason to believe we were the first. Dan Licata in a comment lists some of the references to things we generally absorbed from him.]

This post is about two things. The first topic is a style of formalization in Agda that Bernardo Toninho and I picked up on from Dan Licata. The second topic is a way of establishing termination arguments that Bernardo and I worked out and used extensively in the Agda formalizaiton of several variants of Constructive Provability Logic, which I've mentioned before. Because I'm a bit perverse, I'll be using my own Agda Standard Library as the basis for this post; the code for this post can be found here - since it's a demo bound together with my library, technically I guess I'm supposed to keep the file at that link (though maybe not this post) in sync with the library as the library evolves.

Starting point: the simply-typed lambda calculus

This is a pretty standard Agda formalization of "Church-style" simply-typed lambda calculus terms. "Church-style," as opposed to "Curry-style," encodings only allow for the existence of well-typed terms.*

   open import Prelude

   infixr 5 _⊃_
   data Type : Set where
      con : String → Type
      _⊃_ : Type → Type → Type

   Ctx = List Type

   infixl 5 _·_
   data Term (Γ : Ctx) : Type → Set where
      var : ∀{A} → A ∈ Γ → Term Γ A
      _·_ : ∀{A B} → Term Γ (A ⊃ B) → Term Γ A → Term Γ B
      Λ : ∀{A B} → Term (A :: Γ) B → Term Γ (A ⊃ B)

The only non-obvious part of this encoding is that variables are represented by "dependent de Bruijn indices" - instead of a de Bruijn index being just a natural number, it's the pointer into its type in the context. The nice part about doing it this way is that you can define a very powerful notion of "generalized weakening" that is based on the "subset" partial order on contexts (Γ ⊆ Δ is a function mapping all the indices A ∈ Γ to indices A ∈ Δ).

   _⊆_ : Ctx → Ctx → Set
   _⊆_ = LIST.SET.Sub

   wk : ∀{Γ Δ A} → Γ ⊆ Δ → Term Γ A → Term Δ A 
   wk θ (var n) = var (θ n)
   wk θ (n1 · n2) = wk θ n1 · wk θ n2
   wk θ (Λ n) = Λ (wk (LIST.SET.sub-cons-congr θ) n)

The nice part about this definition, and one of the things I picked up on from Dan, is that we can then define the usual weakening, exchange, and contraction properties directly by using generalized weakening and the corresponding facts about the subset relation on lists (which are defined in my standard library).

   wken : ∀{Γ A C} → Term Γ C → Term (A :: Γ) C
   wken = wk LIST.SET.sub-wken

   exch : ∀{Γ A B C} → Term (A :: B :: Γ) C → Term (B :: A :: Γ) C
   exch = wk LIST.SET.sub-exch

   cntr : ∀{Γ A C} → Term (A :: A :: Γ) C → Term (A :: Γ) C 
   cntr = wk LIST.SET.sub-cntr

With that out of the way, we can talk about substitution, both the "obvious way" and the metric-indexed way Bernardo and I have used extensively.

Straightforward substitution

The obvious (for some value of obvious) and direct definition of substitution involves 1) generalizing the induction hypothesis to allow for even more additions (tm-subst) and 2) writing a variable substitution lemma that handles the case where the substituted-into term is a variable and we either perform the substitution, lower the de Bruijn index, or leaving the de Bruijn index alone (var-subst). The main theorem is inductive on the structure of the first term.

   subst : ∀{Γ A C} → Term Γ A → Term (A :: Γ) C → Term Γ C
   subst = tm-subst [] _
    where
      var-subst : ∀{A C} (Γ Γ' : Ctx)
         → Term Γ' A
         → C ∈ (Γ ++ [ A ] ++ Γ') 
         → Term (Γ ++ Γ') C
      var-subst [] Γ' n1 Z = n1
      var-subst [] Γ' n1 (S n) = var n
      var-subst (_ :: Γ) Γ' n1 Z = var Z
      var-subst (_ :: Γ) Γ' n1 (S n) = wken (var-subst Γ Γ' n1 n)
 
      tm-subst : ∀{A C} (Γ Γ' : Ctx) 
         → Term Γ' A
         → Term (Γ ++ [ A ] ++ Γ') C 
         → Term (Γ ++ Γ') C 
      tm-subst Γ Γ' n1 (var n) = var-subst Γ Γ' n1 n
      tm-subst Γ Γ' n1 (n · n') = tm-subst Γ Γ' n1 n · tm-subst Γ Γ' n1 n'
      tm-subst Γ Γ' n1 (Λ n) = Λ (tm-subst (_ :: Γ) Γ' n1 n)

To motivate the next step, I'll point out that the only reason we had to generalize the induction hypothesis is because of the lambda case - if we try to prove the theorem directly, we find ourselves in the position of having a Term Γ A and a Term (B :: A :: Γ) C; we can't apply the induction hypothesis directly on these two terms. We can apply wken to the first subterm and apply exch to the second subterm and call subst recursively, but now we can't establish termination on the structure of the second term, since we've passed it to the exch function, which changed its structure by replacing Zs with (S Z)s and vice versa.

Setting up a metric

The alternate solution I intend to present involves setting up a metric; this metric expresses the "shape" of a term, disregarding all binding. This is a three-step process: first we define a generic "tree" piece of data that can capture the shape of a term (disregarding binding), and second we define a copy of the Term datatype, called MTerm, that has a Metric as one of its indices.

   data Metric : Set where
      ○ : Metric
      _●_ : Metric → Metric → Metric
      > : Metric → Metric

   data MTerm (Γ : Ctx) : Type → Metric → Set where
      var : ∀{A} → A ∈ Γ → MTerm Γ A ○
      _·_ : ∀{A B m m'} → MTerm Γ (A ⊃ B) m → MTerm Γ A m' → MTerm Γ B (m ● m')
      Λ : ∀{A B m} → MTerm (A :: Γ) B m → MTerm Γ (A ⊃ B) (> m)

The third step is to show that we can freely get into and out of the metric; potentially we should also show that these two actions are an isomorphism, but I haven't run across the need to actually prove that. It really turns out that Agda does most of the work here...

   tm→ : ∀{Γ A m} → MTerm Γ A m → Term Γ A
   tm→ (var n) = var n
   tm→ (n1 · n2) = tm→ n1 · tm→ n2
   tm→ (Λ n) = Λ (tm→ n)

   →tm : ∀{Γ A} → Term Γ A → ∃ λ m → MTerm Γ A m
   →tm (var n) = , var n
   →tm (n1 · n2) = , snd (→tm n1) · snd (→tm n2)
   →tm (Λ n) = , Λ (snd (→tm n))

Now that we have our metric, we can prove a stronger and more useful version of the generalized weakening lemma: not only can we apply generalized weakening to terms, but the resulting term has the exact same shape (as shown by the fact that the same metric "m" appears as an index both to the function's argument and its conclusion.

   wkM : ∀{Γ Δ A m} → Γ ⊆ Δ → MTerm Γ A m → MTerm Δ A m
   wkM θ (var n) = var (θ n)
   wkM θ (n · n') = wkM θ n · wkM θ n'
   wkM θ (Λ n) = Λ (wkM (LIST.SET.sub-cons-congr θ) n)

We don't need to prove weakening twice; our previous weakening lemma is just a simple consequence of this new, stronger one:

   wk : ∀{Γ Δ A} → Γ ⊆ Δ → Term Γ A → Term Δ A 
   wk θ n = tm→ (wkM θ (snd (→tm n)))

Substitution with the metric

With the metric in tow, substitution is straightforward. Termination is established by induction on the metric of the second term. Note the use of both wken (weakening outside of the metric) and exchM (exchange inside the metric) in the lambda case.

   subst : ∀{Γ A C} → Term Γ A → Term (A :: Γ) C → Term Γ C
   subst n1 n2 = substM n1 (snd (→tm n2))
    where
      substM : ∀{Γ A C m} → Term Γ A → MTerm (A :: Γ) C m → Term Γ C
      substM n1 (var Z) = n1
      substM n1 (var (S n)) = var n
      substM n1 (n · n') = substM n1 n · substM n1 n'
      substM n1 (Λ n) = Λ (substM (wken n1) (exchM n))

In this example, it's not clear that we've saved much work: setting up the metric was a lot of boilerplate, though it is straightforward; the benefit that we gained in terms of proof simplicity was primarily an artifact of Agda's pattern matching: either a variable was the first variable in the context (and therefore represented by the de Bruijn index Z), or it was later in the context. So this example isn't the world's best argument for this style, but in the more complex logics that Bernardo and I dealt with, we found that this technique seemed, of all the approaches we could think of, to be the one least likely to fail on us.

Comments

Dan's said on a couple of occasions that he thinks there are less painful ways of doing this sort of thing, existing Agda techniques that avoid the annoying duplication of data types. My understanding is also that there is a not-totally-integrated notion of "sized types" in Agda that could maybe handle this sort of thing, but that the way it works is by defining metrics that are only natural numbers. It seems like a step backwards, somehow, if we go from structural induction to natural number induction. Furthermore, sized types based on natural numbers would almost certainly fail to handle the vaguely insane termination arguments that come up in constructive provability logic.

Totally nameless representations?

The germ of this post comes from a conversation with Chris Casinghino at UPenn back in May. He was working on extending this sort of simple representation in a way that was similarly-insane but mostly unrelated to constructive provability logic. Our problems were different; he placed the blame for some of the difficulties he encountered on the "sillyness of using all de bruijn indices instead of a locally nameless encoding," which was a response that I initially found puzzling. I've since decided that my puzzlement was the result of the fact that he was thinking of the specific thing he was doing in terms of programming languages, and I was thinking about the thing I was doing (constructive provability logic) in terms of logic - my guess is that we're both so used to working on both sides of the Curry-Howard correspondence that it wouldn't have occurred to us that this might make a difference!

From a programming languages perspective, we have programs and typing derivations that show programs to be well typed; the locally nameless encoding gives you the ability to apply the exchange or weakening lemma and get a new typing derivation that says that the same term is still well typed. That wasn't the case for our original "Church-style" lambda calculus terms. In my current view, that's because a "Church-style" lambda calculus term is more like the typing derivation than it is like a term. It's a typing derivation without the term it's typing; in other words, it's a proof in natural deduction form! And what Bernardo and I was using was something that, for our purposes, was just as good as a derivation that the same term was well typed in the exchanged context - we got that the same metric was associated with the exchanged proof term.

In other words, it seems that, for the purposes of termination arguments, the metric serves the same purpose a locally nameless proof term does. Certainly it avoids the "silliness of using all de Bruijn indices," as it uses none whatsoever, hence the mostly-joking title of this post. However, it's quite possible I'm off base; I'd be interested in what people more versed in locally nameless representation thought. I should add that I certainly think it is possible to do an intrinsically typed locally nameless representation; you'd just have to have (at minimum) the free variables be aware of their type. If you were interested primarily in representing a programming language that might even be the right thing to do; but the totally nameless metrics seem to be an easier fit for developments where the primary interest is in the logic side of the correspondence.

* Shameless plug for my advisor Frank Pfenning's excellent essay, "Church and Curry, Combining Intrinsic and Extrinsic Typing" which talks about properties of Church-style versus Curry-style encodings and relates them to subtyping and work by William Lovas.

P.S. This blog post has been about Agda; the first time I used this kind of tree structural metric on terms was in Twelf, when (on a challenge from John Boyland) I showed a bijection between HOAS and de Bruijn form representations of the terms of an untyped (or, if you prefer, "Curry-style") lambda calculus terms.