6
$\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$

3 Answers 3

6
$\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$
2
  • $\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
    Commented Apr 24, 2019 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$ Commented Apr 24, 2019 at 19:57
1
$\begingroup$

You ask

How is λ-μ-calculus different from λ-calculus + Curry-Howard + LEM as an axiom?

There is no such thing as "Curry-Howard + LEM as an axiom". That's the gap that formalisms like λ-μ seek to resolve. You can't just add an axiom, because you have to make it compatible with the rest of the infrastructure. For instance, if you set, $$LEM: a ∨ ¬a,$$ then what is the reduction rule for $LEM$? What does it operate on?

The closest you have to this arises from the fact that the sublogic consisting of all formulas $a_x = a ⊃ x$ is a Boolean logic, no matter what the choice of $x$ is, and different choices for different $x$ give you (possibly) different Boolean logics. In particular, the following are valid in intuitionism: $$ a_x ∧ b_x ⊃ (a∨b)_x, \quad (a∨b)_x ⊃ a_x ∧ b_x,\\ a_x ∨ b_x ⊃ (a∧b)_x, \quad (a_y ⊃ c_x) ⊃ (b_z ⊃ c_y) ⊃ (a∧b)_z ⊃ c_x,\\ (a_x ⊃ b_x) ⊃ (a_x ∧ b)_x,\quad (a_x ∧ b)_x ⊃ (a_x ⊃ b_x),\\ {{a_x}_x}_y ⊃ a_y,\quad a_x ⊃ {{a_x}_y}_y,\\ ⊤_x ⊃ x,\quad x ⊃ ⊤_x,\quad ⊤_x ⊃ a_x,\\ ⊥_x ⊃ ⊤,\quad ⊤ ⊃ ⊥_x,\quad a_x ⊃ ⊥_x, $$ which show that the Boolean connectives and constants in the $x$ sublogic are $$ a_x \overset{x}∧ b_x = (a∨b)_x ≡ a_x ∧ b_x,\quad a_x \overset{x}∨ b_x = (a∧b)_x,\\ \overset{x}¬ a_x = {a_x}_x,\quad a_x \overset{x}⊃ b_x = (a_x ∧ b)_x ≡ a_x ⊃ b_x,\\ \overset{x}⊥ = ⊤_x ≡ x,\quad \overset{x}⊤ = ⊥_x ≡ ⊤, $$ (where $≡$, here, denotes logical equivalence under intuitionism) and that, even though $a_x \overset{x}∨ b_x$ is weaker than $a_x ∨ b_x$, it still satisfies the least-upper-bound property with respect to the subset of the formulas of the form $c_x$ so that it qualifies as the $\overset{x}∨$ connective for the Boolean-sublogic.

In effect, the $x$, $y$, $z$ are "continuation" return types, there is no need for any mention of $⊥$ as a return type, though it could be thought of as the "return" type for no-return functions, the top-level continuations for stand-alone and embedded applications, or the type for the infinite-loop continuation. Each type $a$ lifts to a "continuation passing" version $a_x^x = a_x ⊃ x$ (and we can more generally define $a_x^y = a_y ⊃ x$), with $u: a$ becoming $T u = λα·α u: a_x^x$, where $α: a_x$ is the continuation and $Tuα$ is $αu$ expressed in continuation-passing form. The conversion from $a$ to $a_x^x$ is actually just the combinator $T = λu·λv·vu$, itself, whose generic type is $$ T = λu·λv·vu: a ⊃ (a ⊃ b) ⊃ b.$$ So, the two double-negative rules cited above could be rewritten as $$\left({a_x^x}\right)_y ⊃ a_y,\quad a_x ⊃ \left({a_x}\right)_y^y.$$

The closest you have to LEM is the intuitionistally-valid rule $$a_x \overset{x}∨ \overset{x}¬ a_x,$$ which is just the formula $$(a_x ∧ a_x^x)_x,$$ which, in turn, is a special case of the formula $$(a_x ∧ a_y^x)_y,$$ which are both intuitionistically valid. In fact, written as a combinator, in its most generic form, it is just $$S π_1 π_0: b ∧ (b ⊃ y) ⊃ y = (b ∧ b_y)_y,$$ where the generic forms of the combinators $S$, $π_0$ and $π_1$ are: $$ S = λu·λv·λw·uw(vw): (a ⊃ b ⊃ c) ⊃ (a ⊃ b) ⊃ a ⊃ c,\\ π_0 = λ(u,v)·u: a∧b ⊃ a,\\ π_1 = λ(u,v)·v: a∧b ⊃ a. $$

The situation is, actually, analogous to what happen in Projective Geometry. It is a non-Euclidean geometry that yields a Euclidean Geometry for each choice of a "plane at infinity" (for the 2-dimensional case, or "subspace at infinity" $x$ for the more general case). The plane at infinity gives you a definition of "parallelism" suitable to satisfy the Euclidean Parallel Line Postulate, just as a formula $x$ gives you a definition of negation over the Boolean sub-logic suitable for satisfying the double-negative rule. So, $x$ is the type for the "return at infinity". In a hosted application it would be whatever the type of value the application gives back to the host, when it is done.

In this light, it might be interesting to see what some of the other "classical" axioms $$ N: ¬¬a ⊃ a,\\ Z: (¬a ⊃ ¬b) ⊃ b ⊃ a,\\ R: (¬a ⊃ ¬b) ⊃ (¬a ⊃ b) ⊃ a,\\ V: ¬a ⊃ a ⊃ b, $$ look like when restricted to subformulas of the form $a_x$. $$ N = λu·λv·u (T v) = C B T: (a_x^x)_y ⊃ a_y,\\ Z = λu·λv·λw·u (T w) v = C ∘ N: (a_x^x ⊃ b_y) ⊃ b ⊃ a_y,\\ R = λu·λv·λw·u (T w) (v (T w)) = C (B ∘ S ∘ N) N: (a_x^x ⊃ b_z) ⊃ (a_y^y ⊃ b) ⊃ a_z,\\ V = λu·λv·λw·u v = B K: a_x ⊃ a ⊃ b_x $$ using the combinators and operator $$ C = λu·λv·λw·uwv: (a ⊃ b ⊃ c) ⊃ b ⊃ a ⊃ c,\\ B = λu·λv·λw·u(vw): (b ⊃ c) ⊃ (a ⊃ b) ⊃ a ⊃ c,\\ K = λu·λv·u: a ⊃ b ⊃ a,\\ \left(\begin{aligned}f: b ⊃ c\\g: a ⊃ b\end{aligned}\right) ⇒ f ∘ g = B f g: a ⊃ c. $$ The corresponding reduction rules are $$ N u v = u (T v),\quad Z u v w = u (T w) v,\quad R u v w = u (T w) (v (T w)),\quad V u v w = u v $$ and classical proofs such as $$V = B Z K = Z ∘ K,\quad N = W (B Z V) = W (Z ∘ V),$$ using the combinator $$W = λu·λv·uvv: (a ⊃ a ⊃ b) ⊃ a ⊃ b,$$ will actually reduce, under the β and η rules as $B Z K → B K$ and $W (B Z V) → C B T$ or even $Z N → T$, which flips the order of the double negation rule using $Z$.

In fact, running Combo, which I put up on GitHub, on

    N = C B T, Z = B C N, V = B Z K, W (B Z V)

with extensionality turned on (for the η-rule) will yield $C B T$, while running it with extensionality on

    N = C B T, Z = B C N, V = B Z K, V

results in $B K$.

In the restricted sub-logics, if you actually do take $LEM = S π_1 π_0$, then you'll have the reduction rule $$LEM (u,v) = v u,$$ assuming ordered pairs $(u,v): a∧b$, with types $u: a$, $v: b$ are included in the language.

$\endgroup$
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$
5
  • 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
    Commented Apr 24, 2019 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$ Commented Apr 24, 2019 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
    Commented Apr 24, 2019 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$ Commented Apr 24, 2019 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$ Commented Apr 24, 2019 at 20:05

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .