6
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • 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$
    – Dmitri Urbanowicz
    Commented 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$
    – Dmitri Urbanowicz
    Commented Jul 1, 2020 at 5:57

0

Reset to default