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:
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)
Reduce
fun k -> c k
toc
:(fun c -> (fun x -> x x) c) (fun c -> (fun x -> x x) c) (fun x -> x)
Reduce
fun c -> (fun x -> x x) c
tofun 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)