Mu

Lambda Mu Calculus

Haskell implementation on Michel Parigot's λμ calculus. It has the features of STLC, but you can name types (not system F!) and use μ and [_] operators.

This strongly normalising calculus encodes Classical Natural Deduction in a programming language. Hofmann and Streicher later discovered it captures continuation semantics for programming languages.

Prerequisites

You need Haskell, this compiles with GHC 8.2.2 at least (Stack resolver: lts-11.0).

To Build & Run

To compile and run do: ghc -O2 -o mu Main then run ./mu

Alternatively to use the GHCi Interpreter do: ghci Main then type main

In either case you get something like the following:

Welcome to the λμ-calculus REPL
Type some terms or press Enter to leave.
>

Note: When run in GHCi, you don't have the luxury of escaped characters, backspace, delete etc... Compile it using GHC if you need this.

Examples

Where you can then have some fun, try these examples:

• \1:A.1
• λ0:(A->B)->A.μ1:A.[1]0 (λ2:A.μ3:B.[1]2) an encoding of Peirce's Law or call/cc.
• \0:(Q->_)->(P->_).\1:P.M2:Q.0 (\3:Q.[2] 3) 1 contra-position.

Note: λ is the lambda abstraction, μ is the mu (control) abstraction, [2] is the bracketing (command) operator for μ-variable 2, and ⊥ is the bottom type. Alternatively typed as \, M, and [2], and _ respectively.

Note: you cannot encode ((A->⊥)->⊥) -> A (ie double negation elimination) in this language as the type is not inhabited (see Ariola and Herbelin for some solutions).

The parser is smart enough to recognise λ, so you can copy and paste from the output:

Welcome to the λμ-calculus REPL
Type some terms or press Enter to leave.
> \1:A.1
λ1:A.1
> λ1:A.1
λ1:A.1

There is also a reduction tracer, which should print each reduction step. prefix any string with ' in order to see the reductions:

TODO

There is also a typing mechanism, which should display the type or fail as usual.

> tλ0:(A->B)->A.μ1:A.[1]0 (λ2:A.μ3:B.[1]2)
((A->B)->A)->A
> \1:A.1 1
Cannot Type Term: \1:A.1 1

Note: if you provide a non-normalizing term, the type checker will fail and reduction will not occur.

Syntax

We base the language on the BNF for the typed calculus:

However we adopt standard bracketing conventions to eliminate ambiguity in the parser. Concretely, the parser implements the non-ambiguous grammar as follows:

Some notes about the syntax:

• Variables are positive integers (including zero) as this is easy for Haskell to process, and for me implement variable generation. This is isomorphic to a whiteboard treatment using characters (like \x:A.x).
• Types are either chars A,B,C,... to range over base types, or nested arrow types: T -> T. Arrows associate to the right so that T -> T -> T is the same as T -> (T -> T) but not ((T -> T) -> T). This differs from the approach in STLC, where the the emphasis is on base O versus arrow types (O->O)->O etc...
• Type equality is strict syntactic equality, so A = A but not A = B (think of them as propositions!). Term equality adopts alpha-equivalence (assuming types match)
• Nested terms don't need brackets: \1:A.\2:B. 2 unless enforcing application on the right. Whitespace does not matter (\1:A. 1) unless it is between application where you need at least one space.
• To quit use Ctrl+C or whatever your machine uses to interrupt computations.

Semantics

The semantics implements beta-reduction on terms and alpha-equivalence as the Eq instance of MuTerm. The semantics are the same as STLC with the addition of rules for μ and [] operators. We reformulate the semantics as typing judgements:

for variables (adopted from STLC):

for abstractions (adopted from STLC):

and application (adopted from STLC):

the (logical) beta reduction (adopted from STLC):

and special introduction, elimination, and reduction rules for μ and [] operators:

TODO reductions

• λ variables and μ variables are stored in the same context. Most treatments have separate contexts for this but we have one to ensure term naming is distinct.
• This implementation follows a small-step operational semantics and Berendregt's variable convention (see substitution in Mu.hs).
• Reductions include the one-step reduction (see reduce1 in Mu.hs), the many-step reduction (see reduce in Mu.hs).

Other Implementation Details

• Mu.hs contains the Haskell implementation of the calculus, including substitution, reduction, and other useful things.
• Parser.hs contains the monadic parser combinators needed to parse input strings into typed-term ASTs for the calculus.
• Repl.hs contains a simple read-eval-print loop which hooks into main, and into the parser.
• Main.hs is needed for GHC to compile without any flags, it also invokes the repl.

For contributions, see the project to-do list or submit a PR with something you think it needs.