lambda mu calculus

Stream: Type theory

[Chris B]

Someone asked a question on the PA stack exchange about a hypothetical proof assistant based on the lambda-mu calculus that hasn't been answered. I always thought the lambda-mu calculus was kind of nice, and was hoping from the sidelines that someone would chime in. If anyone here has an expert opinion they can share, there are at least two people who are interested.

https://proofassistants.stackexchange.com/questions/541/what-difficulties-are-there-in-basing-a-proof-assistant-on-the-lambda-mu-calc

[Trebor Huang]

Not to blow my own horn, but I did make a (classical propositional calculus) type checker based on polarized $\lambda\mu$ calculus. I linked to some papers on this subject in the comment, and you can search for

• polarized type theory, or something like it
• Zeilberger's thesis, which I forgot the exact title. It's something like "semantics of evaluation order and pattern matching".

[Chris B]

Thank you, the first paper seems pretty interesting; I wasn't previously familiar with polarity as such. Is your project the one called thonk?

[Trebor Huang]

That one is related but untyped (and unfinished :-( ). It's not on GitHub, because it's made with a few classmates for fun, and has no readability.

A simple account of polarity:

• Positive types are created by constructors (so to create a function into that type, use constructors), and they are used with pattern matching (so to create a function out of that type, use pattern matching). And the constructors determine how pattern matching looks like.
• Negative types are used by coconstructors, i.e. projections. And they are created by specifying each field. In other words, you pattern match on the coconstructors to create something of negative types.

In intuitionistic logic, they are not symmetric. The positive types dominate. So you can see how recursive positive types (i.e. inductive types) are well studied, have eliminators that capture the behavior of pattern matching etc. But recursive negative types (coinductive) are generally less studied, and you need something like bisimiliarity to get things done.

[Trebor Huang]

You can recover the symmetry by retreating to linear logic, but you don't have to. Classical logic also has this symmetry.

Zeilberger's thesis is here.

[Trebor Huang]

The $\mu\tilde\mu$ thing is actually trying to create the symmetric counterpart of $\lambda$. So along with the intuitionistic $A\to B$, you also have a dual $A - B$, which classically means "A but not B". This is bi-intuitionistic logic. But then you don't need to cling to functions at all, as Zeilberger demonstrates.

[Chris B]

Trebor Huang said:

That one is related but untyped (and unfinished :-( ). It's not on GitHub, because it's made with a few classmates for fun, and has no readability.

I know the feeling. Thanks for taking the time to introduce the polarity concept and including that thesis reference.