A jig for combinator programs:

((λSKIY. 42 ; Combinator expressions go here. ) (λfgx.fx(gx)) ; S (λxy.x) ; K (λx.x) ; I (λfx.(f(xx))(λx.(f(xx)))) ; Y )Here is a Scheme program to convert λ-expressions to combinators using the definitions of C and A towards the end of this page. For an expression s in which x is free, A[(x, s)] produces an expression t which does not mention x, but where (t x) is equivalent to s. We encode a simple λ expression M as Scheme data s[M] thus:

s[(λxM)] = (λ (x) s[M]) s[(M N)] = (s[M] s[N]) s[x] = x ; x is a symbol but neither λ, K, S nor I.The yield of C is encoded likewise. Note that the encoding is a Scheme program with the same meaning. See “cnvSch2” here for a program that computes s.

(define (C x) (if (symbol? x) x (if (eq? (car x) 'λ) (A (caadr x) (C (caddr x))) (list (C (car x)) (C (cadr x)))))) (define (A x s) (if (symbol? s) (if (eq? x s) 'I (list 'K s)) (list (list 'S (A x (car s))) (A x (cadr s)))))The interesting result is that x does not appear freely in (A x s).

A trick here is that “s” in “A [ (x, s) ]” subsumes K as well as variables. This subtlety is somewhat buried in the code! The yield is a valid Scheme program in a context that defines S, K and I.

(C 'w) => w s[(λxy.x)] = s[(λx(λyx))] = '(λ (x) s[(λyx)]) = '(λ (x) (λ (y) s[x])) = '(λ (x) (λ (y) x)) (C '(λ (x) (λ (y) x))) => ((S (K K)) I)The Scheme function

(define (ass x) (if (pair? x) (if (pair? (car x)) (append (ass (car x)) (map ass (cdr x))) (cons (car x) (map ass (cdr x)))) x))

Working thru C[(λx(λy x))] by hand:

A[(x, C[(λy x)])] A[(x, A[(y, C[x])])] A[(x, A[(y, x)])] A[(x, (K x))] ((S A[(x, K)]) A[(x, x)]) ((S (K K)) I)In general the yield of

Thus to test

((λSKIY. (((S (K K)) I) 3 5) ; App goes here. ) (λfgx.fx(gx)) ; S (λxy.x) ; K (λx.x) ; I (λfx.(f(xx))(λx.(f(xx)))) ; Y )which indeed yields 3!

And `(C '(λ (x) (λ (y) y)))` yields `(K I)`.

(define (((S f) g) x) ((f x)(g x))) (define ((K x) y) x) (define (I x) x) (((K I) 4) 6) ; => 6

(C S) = (C '(λ (f) (λ (g) (λ (x) ((f x) (g x)))))) => ((S ((S (K S)) ((S ((S (K S)) ((S (K K)) (K S)))) ((S ((S (K S)) ((S ((S (K S)) ((S (K K)) (K S)))) ((S ((S (K S)) ((S (K K)) (K K)))) ((S (K K)) I))))) ((S (K K)) (K I)))))) ((S ((S (K S)) ((S ((S (K S)) ((S (K K)) (K S)))) ((S ((S (K S)) ((S (K K)) (K K)))) (K I))))) ((S (K K)) (K I))))

Notice the expansion.