I am learning $\lambda \mu$-calculus (self-study).

I learned it because it seems very useful for understanding Curry-Howard correspondence (e.g understanding the connection between classical logic and intuitionistic logic)

I searched the internet, there is some information about $\lambda \mu$-calculus on Wikipedia, but it does not explore it further (at time of writing). https://en.wikipedia.org/wiki/Lambda-mu_calculus

Is there any more programming way to interpret the intuition behind $\lambda \mu$-calculus?

For example:

In $\lambda \mu$-calculus, there are two additional terms called $\mu$-abstraction $\mu \delta .T$ and named term $[\delta]T$.

Can I think $\mu$-abstraction as a $\lambda $-abstraction which waiting for some continuation $k$ (here, is $\delta$)?

What's the meaning of the named term?

How does it connect to call/cc?

Can I find the corresponding roles in some programming language (e.g. Scheme)?

PS: I can understand $\lambda$-calculus, call/cc in Scheme, and CPS-Translation, but I still cannot clearly understand the intuition behind $\lambda \mu$-calculus.

Very thanks.

  • 1
    $\begingroup$ Following the links from Wikipedia, you can find a paper by Wadler, which has better description of the calculus: homepages.inf.ed.ac.uk/wadler/papers/dual-reloaded/… $\endgroup$ Jul 1, 2020 at 5:55
  • 1
    $\begingroup$ From the paper: “The computational interpretation of a μ- abstraction μα.S is to bind the covariable α and then evaluate statment S; if during evaluation of S the covariable α is applied to a value, then that value is returned as the value of the μ-abstraction; this is similar to the behaviour of callcc in Scheme.” $\endgroup$ Jul 1, 2020 at 5:57


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.