5
$\begingroup$

I have some experience with using type theory to do proofs in intuitionistic logic. If I want to prove theorems that require classical logic, I simply pose the law of excluded middle (LEM) as an axiom. As far as I understand, intuitionistic logic + LEM gives you classical logic, so I presume that all theorems that have a classical proof, have a proof in intuitionistic-logic-type-theory with LEM as an axiom.

But then I heard about so called $\lambda$-$\mu$-calculus, and that this is meant to extend the Curry-Howard isomorphism to classical logic. I haven't managed to get the point of $\lambda$-$\mu$-calculus yet, hence this question.

How is $\lambda$-$\mu$-calculus different from $\lambda$-calculus + Curry-Howard + LEM as an axiom?

$\endgroup$
4
$\begingroup$

First, Curry-Howard is not a thing you "add" to the lambda calculus. It is a family of theorems that relates typed lambda calculi and proof theories.

Anyway, let's say you are working in Agda. You want to do some classical reasoning so you postulate LEM, say as:

postulate lem : {P : Set} → isProp P → P ∨ ¬ P

where isProp P just asserts that there is at most one value of P. See below for a full listing.

Now we want to prove a classical theorem like double negation elimination.

dne : {P : Set} → isProp P → ¬ (¬ P) → P
dne isProp-P ¬¬p with lem isProp-P
dne isProp-P ¬¬p | Left p = p
dne isProp-P ¬¬p | Right ¬p = absurd (¬¬p ¬p)

This typechecks and is a valid classical proof, so what's the problem?

The problem is that this doesn't compute. If you try to normalize it, Agda will get stuck (as with all postulates) on the case analysis of lem. Okay, but who actually runs their Agda programs? Agda does. Agda normalizes terms during the course of typechecking, and if it gets stuck, it will just fail to typecheck. Regardless, a key part of the Curry-Howard correspondence is to connect computation to proof reduction, and postulates don't have any computation rules associated with them.

What the $\lambda\mu$ calculus does is make a computational system that does give computational meaning to classical theorems like lem. The equivalent to a use of thedne proof can then be "normalized". Essentially what happens is the call to lem immediately returns Right ¬p where ¬p is a continuation which gets passed to ¬¬p. ¬¬p either produces without using ¬p, in which case we're good because we jump away abandoning this (sub)computation, or it applies ¬p to some p which causes us to jump back to the call to lem and return Left p and we're done. This approach to the computation is not available in the simply typed lambda calculus which represents intuitionistic (or minimal) propositional logic, and remains unavailable in an intuitionistic type theory such as Agda.

Full listing:

data ⊥ : Set where

absurd : {A : Set} → ⊥ → A
absurd ()

¬ : Set → Set
¬ A = A → ⊥

data _≡_ {A : Set} (a : A) : A → Set where
    Refl : a ≡ a

data _∨_ (A B : Set) : Set where
    Left : A → A ∨ B
    Right : B → A ∨ B

isProp : Set → Set
isProp P = (x y : P) → x ≡ y

postulate lem : {P : Set} → isProp P → P ∨ ¬ P

dne : {P : Set} → isProp P → ¬ (¬ P) → P
dne isProp-P ¬¬p with lem isProp-P
dne isProp-P ¬¬p | Left p = p
dne isProp-P ¬¬p | Right ¬p = absurd (¬¬p ¬p)
$\endgroup$
  • $\begingroup$ "Agda normalizes terms during the course of typechecking, and if it gets stuck, it will just fail to typecheck." I don't understand this? A type checker doesn't need to compute the function whose type it is checking, right? A type system in a compiler for JavaScript gives you type errors during compile time, if your program doesn't typecheck. And if I have axioms in my theorem prover, it can still type check the proofs that use those axioms. So I'm confused by this statement. Is this a specific property of Agda? Does it also apply to Coq or Lean? $\endgroup$ – user56834 Apr 24 at 19:30
  • $\begingroup$ Agda terms occur in Agda types. Something like if not true then Nat else Bool is a perfectly valid type in Agda, and Agda has to normalize it to know that true is a value of that type. This is a general property of dependently typed languages. Their term and type languages are mutually dependent. Agda doesn't need to normalize a term to know what its type is, but it may need to normalize other terms to check that type. $\endgroup$ – Derek Elkins Apr 24 at 19:57
0
$\begingroup$

As far as I can tell (I am no expert, I simply googled) they are different ways of doing the same thing. $mu$ calculus appears to give one continuations.

I shall use Haskell notations from here on out. If this does not work for you, I can rewrite my answer, but I am more familiar with logic through Haskell/Coq than the math, so I might get it wrong :)

Now, if we have continuations, then for any type a, we can construct the equivalent value cont_a :: forall r. (a -> r) -> r which is the continuation representation of a.

Setting r = Void gives us cont_a :: forall a. (a -> Void) -> Void. This is the principle of double negation elimination, since it allow us to "instantiate a value" (produce a proof) of $\lnot\lnot a$, since $\lnot a$ is encoded as a -> Void in the type theory.

$\endgroup$
  • 1
    $\begingroup$ Thank you :). Could you explain what the "point" is of "continuations"? I don't know about them and after a quick google I understand roughly what it means, but don't understand the point, or how we would use them to do proofs. $\endgroup$ – user56834 Apr 24 at 16:53
  • $\begingroup$ Continuations were originally discovered to generalize control flow as far as I am aware. It was eventually picked up by the semantics community to represent imperative programs. It was also then picked up by folks writing compilers, since CPS (continuation passing style) allows for easier compiler optimizations in some cases. Of course, once Curry-Howard came into the picture, it is natural to ask about the "logical meaning" of continuations, and I presume that was how this story was discovered. However, as far as I am aware, they came from practice, not theory! $\endgroup$ – Siddharth Bhat Apr 24 at 16:56
  • 1
    $\begingroup$ Interesting, this makes me conjecture: can $\lambda$-$\mu$-calculus be seen as the "imperative" version of the "functional" $\lambda$-calculus? And can the Curry-Howard isomorphism applied to $\lambda$-$\mu$-calculus be seen as introducing "imperative style proofs" as opposed to "functional style proofs" of the $\lambda$-calculus? I wouldn't know why classical logic would be related to imperative programming and intuitionistic logic to functional programming, but that would be interesting. $\endgroup$ – user56834 Apr 24 at 17:01
  • $\begingroup$ I don't know about that, but I found lecture notes that might :) cs.cmu.edu/~rwh/courses/typesys/hws/hw5/continuations-logic.pdf $\endgroup$ – Siddharth Bhat Apr 24 at 17:18
  • $\begingroup$ @user56834 While the $\lambda\mu$ calculus would not really be considered "purely functional", it would be a bridge way too far to call it "the imperative version of the $\lambda$ calculus". It lacks many features one would expect from an imperative language, and even the continuations are constrained in ways that continuations in programming languages usually aren't. There are many lambda calculi that are "more imperative" than the $\lambda\mu$ calculus, yet it still wouldn't make sense to call any of those the imperative version of the lambda calculus as there are so many possibilities. $\endgroup$ – Derek Elkins Apr 24 at 20:05

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.