4
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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:

  1. Start with:

    (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)
$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Earth Engine Apr 20 '13 at 10:20
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Apr 20 '13 at 18:01
  • $\begingroup$ 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. $\endgroup$ – Earth Engine Apr 21 '13 at 10:53
  • $\begingroup$ 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$. $\endgroup$ – Andrej Bauer Apr 21 '13 at 21:31
  • $\begingroup$ 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. $\endgroup$ – Earth Engine Apr 22 '13 at 2:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.