19
$\begingroup$

The $\lambda\mu$-calculus is a variant of the $\lambda$ calculus introduced by Parigot to capture classical logic. The Wikipedia article describing it in more detail is here. In modern proof assistants, it is expected that the user should opt-in to breaking canonicity via adding their own axioms if they want to enjoy classical reasoning.

There is an alternative world though, where classical logic is the basis for the core logic. The $\lambda\mu$-calculus is one such calculus that allows this to be possible. I am interested in it specifically because a $\lambda\mu$-cube was constructed for it without much difficulty. It is known that given the Calculus of Constructions that a proof assistant with inductive types is only a stone's throw away by adding on strong sigmas, bolting on an inductive datatype theory, or some other combinations of core types.

There are existing approaches that use classical reasoning such as HOL and other LCF logics where a classical logic can be embedded. However, I am interested in the class of proof assistants that are on equal footing with Coq, Agda, and Lean. That is, they ought to have dependent types at the very least.

Yet, I do not know of any proof assistants that have tried (and definitely none that have had any success!) in using the $\lambda\mu$-calculus as the computational basis. My question is thus in two parts: First, what difficulties might one run into when attempting this? Second, has anyone tried it?

I want to dispense with the obvious objection of normal forms. The calculus does not have a strong notion of normal form (or at least, you have to choose between confluence and normal forms). This is not a show-stopper, a designer can pick confluence and use that for definitional equality while allowing propositional equality to "repair" the lack of strong normal forms. I do not think even usability will be hurt, as I imagine the $\lambda$-calculus fragment can still enjoy $\beta\eta$-equality. If my assumptions here are wrong I would be interested to know.

$\endgroup$
2
  • 4
    $\begingroup$ You can repair it with $\lambda\mu\tilde\mu$-calculi and the like. See e.g. here. A very, very bad aspect of this is that the universe type cannot be polarized. This means that dependent types cannot be full-blown. $\endgroup$
    – Trebor
    Feb 14 at 19:04
  • 1
    $\begingroup$ In category handwaving, it means that the category of polarized categories cannot itself be made into a polarized category. $\endgroup$
    – Trebor
    Feb 14 at 19:06

2 Answers 2

16
$\begingroup$

TL; DR: There are. But there are also severe difficulties that only have unsatisfactory solutions.

Let's see what bad things will happen, so we can attempt to fix it. The first thing when trying to turn sequent calculus into a type theory, is that there are many equivalent but meaninglessly different terms. Consider the left $\wedge$-introduction rule:

$$\frac{A, B, \Delta \vdash \Gamma}{A \wedge B, \Delta \vdash \Gamma}$$

This is very well and all, and we might try to assign the syntax like

$$\frac{t : (x{:}A, y{:}B, \Delta \vdash \Gamma)}{t[p \sim x, y] : (p{:}A \wedge B, \Delta \vdash \Gamma)}$$

it would bind the variables $x,y$ in $t$, as well as creating a free variable $p$. But consider a derivation from $A_1, \dots, A_{10} \vdash B$ to $A_1 \wedge A_2, A_3 \wedge A_4,\dots, A_9 \wedge A_{10} \vdash B$. Since we have five $\wedge$-introduction, we have $5! = 120$ different terms. Which should be normal? There's no canonical way to decide. And therefore such a syntax faces severe metatheoretical problems, because our intended semantics doesn't contain the order information while the syntax does. So even if you construct a model to prove stuff, the model will be very exotic and won't resemble anything familiar or expected.


The fundamental reason that this happens is that the sequent calculus is unfocused. The rules can operate on any formula in random, and as long as they don't affect each other, the order of these rules shouldn't matter.

One way to deal with this is the proof net approach by Girard. But just checking the validity of proof nets seems to be very hard, and there are various criteria and algorithms. They won't look like a type theory anyway. So we won't go down that rabbit hole for now.

Another way to deal with this is, well, obviously, by introducing focus. In intuitionistic logic, there are only one formula on the right of $\vdash$, and the focus is naturally on that formula. This makes all the inference rules sequential, and we can pack it up into a nice term syntax. In classical sequent calculus, we have to manually mark a formula as "focused", and have all the rules operate on it. We also have rules to lose and gain focus.

Let's use square brackets to mark the focus (it's not the standard notation, but I think it's clearer). So for right $\to$-introduction, we have a focused formula on the right:

$$\frac{t : (\Gamma, x{:}A \vdash [B], \Delta)}{\lambda x.t : (\Gamma \vdash [A \to B], \Delta) }$$

Looks nice. And for left $\to$-introduction (remember that there are no elimination rules in sequent calculus, we only have right/left introduction, and the cut rule), we have to focus on the left:

$$\frac{t : (\Gamma \vdash [A], \Delta) \quad c : (\Gamma, [B] \vdash \Delta)}{t\cdot c : (\Gamma, [A \to B] \vdash \Delta)}$$

(If you feel unfamiliar with this, grab a book an sequent calculus and refresh yourself. This is exactly the left-introduction rule for $\to$.)

And, as we said, we need the cut rule for anything interesting to happen:

$$\frac{t : (\Gamma \vdash [A], \Delta) \quad c : (\Gamma, [A] \vdash \Delta)}{\langle c | t \rangle : (\Gamma \vdash \Delta)}$$

We also need ways to unfocus (the cut rule gives the way to focus). Since unfocused formulas corresponds to variables (think intuitionistic logic, where all the formulas on the left are unfocused, and they are each assigned a variable; the focused formula on the right doesn't have a variable), we need to kill a variable. What kills a variable? A binder. So here enters our $\mu$ binder:

$$\frac{E : (\Gamma \vdash \alpha{:}A, \Delta)}{\mu \alpha. E : (\Gamma \vdash [A], \Delta)}$$

Dually we have the $\tilde\mu$ binder:

$$\frac{E : (\Gamma, x {:} A \vdash \Delta)}{\tilde\mu a. E : (\Gamma, [A] \vdash \Delta)}$$

And last but not lease, we of course need to enable terms to refer to variables, or else there's no good doing anything!

$$\frac{}{\alpha : (\Gamma, [A] \vdash \alpha{:}A, \Delta)} \quad \frac{}{x : (\Gamma, x{:} A \vdash [A], \Delta)}$$

Now we have seen three types of things:

  • Terms $t$ have their focus on the right. They are very much like the terms in our usual intuitionistic type theory, as you can see that every rule with the focus on the right looks familiar.
  • Coterms $c$ have their focus on the left. They are like holes, or continuations. But it's fine if you don't get any intuition for them.
  • Commands $E$ (or as Zeilberger calls it, programs) don't have a focus. They are what you get when you put together a term of type $A$ and a continuation demanding a term of type $A$.

Well, that's nice, but as you have mentioned, we now have normalization problems. Also, although you said there is a $\lambda\mu$-cube, the cube is defined in Curry style. And as is well known, even $\lambda 2$ in Curry style has undecidable type checking, making life harder for proof assistants. Apart from decidability, $\lambda \mu$-calculus is actually equationally inconsistent. This means that $\lambda xy. x = \lambda xy.y$. This is fine in simple types, and doesn't affect logical consistency which says the empty type has no closed terms. But in dependent types, equational inconsistency means that any two types will be equal, which further entails logical inconsistency.

The ultimate reason for this is because we haven't chosen a canonical evaluation order. Actually, if you settle on call-by-name, or call-by-value, or any evaluation strategy, as long as you don't change your mind halfways, you do get good normalization properties. However, this arbitrarily chosen order also has a negative impact in dependent types, since some perfectly legit types would have no terms, because they don't reduce in the specific evaluation order to the desired form.

To solve the ad-hoc-ness of the chosen evaluation order, we can add polarity to the types. I linked to a paper in the comments. There's also Zeilberger's thesis. And in my opinion this settles the ad-hoc problem in a pretty elegant way.

But you still have problems when switching to dependent types, because now types may carry computations. And there are partial solutions which only allows types to be dependent on positive values. The link also explains the difficulties in more depth.


And finally, I should really mention Shulman's paper encoding a logic that is symmetric (although not perfectly classical, of course; the negation is involutive, though) purely inside intuitionistic type theory.

$\endgroup$
3
  • 1
    $\begingroup$ "And as is well known, even 𝜆2 in Curry style has undecidable type checking, rendering it unfeasible for proof assistants." Being a user/developer of Cedille I aggressively reject this :) (great answer though) $\endgroup$ Feb 20 at 3:41
  • $\begingroup$ Ok, I wish I could unsay that. There are plenty of proof assistants with undecidable type theories. :P $\endgroup$
    – Trebor
    Feb 20 at 3:46
  • $\begingroup$ "λμ-calculus is actually equationally inconsistent. This means that λxy.x=λxy.y". Is there somewhere this is discussed in more detail? $\endgroup$
    – David
    Mar 16 at 15:28
13
$\begingroup$

I think that the first question can be generalized to "What difficulties are there in adding side-effects to a proof assistant based on dependent type theory."

First-class continuations are just one particular side-effect

The λμ-calculus is only an instance of a more general class of extensions of the λ-calculus with side-effects. There is no unique definition of what a side-effect is, but a good generic approximation is "any feature of the language that makes the difference between call-by-name and call-by-value observable". One can for instance mention exceptions, mutable state, IO, threads and whatnot.

The effect introduced by the λμ-calculus is the notion of first-class exceptions. The μ binder, indeed, allows to capture the current continuation, which can be resumed at a later time with the [α]t construct. This is not possible in the standard λ-calculus, and it is precisely what introduce classical abilities in this system.

In PLT, we ain't afraid of no effects

This other answer insists at length, and rightfully, on the fact that first-class continuations break the CbN-CbV equivalence and thus should be endowed with a stricter reduction strategy to preserve the equational theory. This is not a problem tied to dependent types specifically, but rather by definition the landmark of side-effects.

Now, dependent types rely on the runtime semantics of the proofs, so the degeneracy of the equational theory percolates immediately in the logic. But the very same problem happens already with effectful non-dependent programming languages, and there, it is folklore that one needs to care about the exact reduction strategy. No sane programmer would expect a call-by-name equation to hold in their favourite ML implementation.

So in this regard, I believe that that answer is somewhat missing the really problematic point.

I Can Haz callcc?

Dependent type theories are biased towards call-by-name. The one rule that allows lifting computation to typing is the conversion rule. But this rule bakes in the fact that conversion is call-by-name, as it is generated by the unrestricted β-rule.

So one could expect that throwing side-effects into MLTT is going to be fine, since it already made a choice of strategy for you. Obviously you have to be careful that indeed your effects are call-by-name, but apart from this technical detail it should be fine, shouldn't it?

Alas! If you do this with callcc (which is essentially a flavour of λμ-calculus) you get an inconsistent theory. What went wrong?

The real problem with effects and dependent types

What really separates dependent type theory from other higher-order logics is that it features inductive types equipped with large dependent elimination. The latter is what allows the user to write weird types like forall (b : bool), if b then nat else empty where the shape of a type really depends on the value of a term.

This is precisely this feature that causes the issue with side-effects, and there is a simple intuitive and mostly correct explanation for this phenomenon.

As OP observed, side-effects break the canonicity property of the theory. A term, while reducing to a value, may perform side-effects that are observable. Thus, for instance, not all terms M : bool are convertible to either true or false in presence of effects. A typical PLT-centric way to phrase that is the progress lemma, which says that terms are either values or reduce. And indeed, values of an inductive type have the right shape, but by contrast terms can be wild.

Now, large dependent elimination bakes in the fact that arbitrary terms behave like values. For booleans, for instance, it states that P true and P false are enough to prove forall b : bool, P b for any P : bool -> Type. But obviously, in presence of side-effects there are non-standard boolean terms that are neither true nor false.

No wonder why this principle results in an inconsistent theory!

Embracing effects

Effectful dependent types are a pretty niche area. Still, we do have some proposals for it to work properly.

Some effects can be added relatively straightforwardly and justified by a syntactic translation. As already argued, we need to do something with large elimination or face inconsistency. We believe that a simple linearity criterion is enough to separate the wheat from the chaff.

Linearity is the critical insight of Baclofen Type Theory (BTT), a restriction of MLTT compatible with side-effects. In a nutshell, BTT restricts large elimination to predicates P : bool -> Type that are linear, i.e. which satisfy an equation ensuring that they actually behave as if they were evaluating their argument in a call-by-value / strict way.

Too good to be true?

Unfortunately, while BTT seems to validate a large class of effects, we still do not have a reasonable syntactic model of BTT for first-class continuations. The reason are technical and tied to the impredicative nature of the CPS monad. Yet, we believe that it may be possible to present a variant of BTT with first-class continuations as a standalone theory whose properties are proved directly on the syntax. This requires more work, and novel research, which is why there is no such thing yet.

In any case, BTT might not be a theory you want to work in.

  • From a mathematical standpoint, it really puts emphasis on the potentially effectful nature of proofs-as-programs. This is clearly at odds with the standard mathematical practice.
  • From a programming standpoint, mixing call-by-name and effects is not very nice. You always have to program defensively and rely on weird storage operators to ensure you actually get a value.

It might be more tenable in the long term to switch to a call-by-value (or more generally, call-by-push-value / polarized) type theory. Nonetheless, this move would only make the life of the computer scientist easier, while making the whole experience even more alien to the mathematically inclined user.

$\endgroup$
6
  • $\begingroup$ Interesting insights, though it makes me wonder if a pure $\lambda\mu$-calculus with data encoded directly in the theory itself would avoid a lot of these issues. Large eliminations aren't inherently possible if your inductive data is encoded. Though I guess you still need at least a linear function space to support inductive data with the expected amount of elements. $\endgroup$ Feb 20 at 23:58
  • 1
    $\begingroup$ What do you mean? A deep encoding of the language is not influencing the metatheory in any way. If you want large elimination you'll need some form of induction-recursion, and if you just do it only for simple types this going to be equivalent to using a monadic encoding through a shallow embedding. $\endgroup$ Feb 21 at 14:28
  • $\begingroup$ I mean that if we take CoC as the base, we can church-encode the data. A predicate doesn't have any meaningful way to induct on the data to form a large elimination then. Then maybe we could add refinement types and erased function spaces to emulate large eliminations similarly to how it is done in Cedille. $\endgroup$ Feb 21 at 15:55
  • 1
    $\begingroup$ But then where do you get your equational theory from? I don't really understand if you're just trying to implement some form of CPS with a strong form of induction reminiscent of double negation shift, or something else. $\endgroup$ Feb 21 at 21:48
  • 1
    $\begingroup$ Delimited continuations extend intuitionistic logic with semi-classical principles, though. You can use them to prove Markov's principle or double negation shift. Note that DNS is exactly what is missing to prove AC when interpreting PAω into HAω via a double negation translation, so this is pretty close to getting large elimination in a classical setting. $\endgroup$ Feb 22 at 9:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.