# Are there a lambda-mu expression equivalent to the yin yang puzzle?

The yin yang puzzle was written in Scheme. Since it uses call/cc, it is not possible to express it in a pure lambda expression, unless we do a CPS transform.

However, given the fact that $\lambda \mu$-calculus have the power to model call/cc, is it possible to write an equivalent $\lambda \mu$-expression? I am still learning $\lambda \mu$-deductions, so this would be a good example to show how the deduction works.

There is no need to model the "display" command in a pure expression. Ideally only showing how the calculus keep looping and evaluates diffident terms again and again.

UPDATE My translation in $\lambda$-expression with CPS:

(λcallcc.callcc (λyin.callcc (λyang.yin yang))(λcc.cc cc)


In CPS, (λcc.cc cc) is what "call with current continuation" means. So the expression takes it as a parameter. This will result in assign the sub-expression starts λyin assign its continuation into parameter yin. And then in the body, the second callcc assigns the yang of sub-expression starts λyang into itself. Finally, apply yin yang.

Note the above translate is not full CPS, only the concept of call/cc has been translated. But it provides the same behavior and it is not hard to do a full CPS translate.

You can get an important hint to solution by thinking how to make the yin-yang puzzle work in a typed language, see this question. OCaml computes the type of yin and yang to be ('a -> 'a) as 'a, which is a recursive type equal to its own function space. Such a type is precisely what it takes to implement the untyped $\lambda$-calculus in a typed language.

What does this have to do with your question? In the untyped $\lambda$-calculus (or typed calculus with general recursive types) we can define $\mu$ and other fixed-point combinators. So, since yin and yang cannot be given types, we must use the untyped $\lambda$-calculus, but then $\mu$ is not needed as a primitive. In fact, the CPS transform of the puzzle will be just pure $\lambda$-calculus.

You can compute the CPS transform in the privacy of your mind. Here is my version, written in Ocaml. To run it, you need to pass -rectypes to Ocaml:

let callcc f k = f k ;;
let yin c = callcc (fun x -> x x) (fun k -> print_char '@'; c k) ;;
let yang c = callcc (fun x -> x x) (fun k -> print_char '*'; c k) ;;
let _  = yin yang (fun x -> x) ;;


Clearly, the let statements are just a convenience. Without them, and with callcc expanded out, we get:

(fun c -> (fun x -> x x) (fun k -> print_char '@'; c k))
(fun c -> (fun x -> x x) (fun k -> print_char '*'; c k))
(fun x -> x)


We could remove the print_char statement and $\eta$-reduce:

(fun c -> (fun x -> x x) (fun k -> c k))
(fun c -> (fun x -> x x) (fun k -> c k))
(fun x -> x)

2. Reduce fun k -> c k to c:

(fun c -> (fun x -> x x) c) (fun c -> (fun x -> x x) c) (fun x -> x)

3. Reduce fun c -> (fun x -> x x) c to fun x -> x x:

(fun x -> x x) (fun x -> x x) (fun x -> x)


So the essence of the yin-yang puzzle is just self-application of self-application. How appropriate! As a last step, we can put in the print_char statements again, to get a one-liner:

(fun x -> x (fun k -> print_char '@'; x k)) (fun x -> x (fun k -> print_char '*'; x k)) (fun x -> x)

• Is that you mean I don't need a λμ-expression? Can you please explain how to define μ since μ is not a "fixed-point combinator", as what I know so far. – Earth Engine Apr 20 '13 at 10:20
• I may have answered the wrong question because I totally assumed $\mu$ was a fixed point combinator. Are you referring to Parigot's $\lambda\mu$-calculus? In that case the answer ought to be similar, except we're not going to simulate continuations by explicit continuation passing, I suppose. The main point is that it's going to be untyped, no matter what you do. – Andrej Bauer Apr 20 '13 at 18:01
• I agreed that it is going to be untyped, and this is not what asking. But yes I am referring to Parigot's λμ-calculus so μ is not a fixed point combinator. I am learning it so I would like to see what the result looks like. – Earth Engine Apr 21 '13 at 10:53
• Well, you don't have to use $\mu$ because you can do it just with $\lambda$ (because we're untyped). Let me think what it would look like with $\mu$. – Andrej Bauer Apr 21 '13 at 21:31
• I said I understand that we can do the same thind with λ when using CPS. But CPS changes the semantic of the expression (your - an my - translated expression do not looks like or structured like the origin version any more), this is the reason why I am looking for a direct λμ translation. – Earth Engine Apr 22 '13 at 2:03