Convert between lambda calculus and combinatory logic in Schönfinkel's BCIKS system
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
README.md
cl.rkt
cl.scm

README.md

lambda-CL

λx.λy.(y x) → (C I)

(C I) → λx.λy.(y x)

Convert between lambda expressions and combinatory logic in Schönfinkel's BCIKS system.

BCIKS quick guide

  • B f g x = f (g x) (composition)
  • C f x y = f y x (order swap)
  • I x = x (identity)
  • K x y = x (drop arg)
  • S f g x = (f x) (g x) (duplicate arg)

Usage

On Racket, require ./cl.rkt, and on other scheme interpreters, load ./cl.scm. These provide the T, L, and P functions (described below), as well as the combinators B, C, I, K, S.

$ racket -i --require cl.rkt
$ mit-scheme -load cl.scm

Currying

Arguments must be given in curried form. The T function can parse lambda expressions and curried function applications (i.e. pairs of the form (a b)). The L function can only parse curried function applications. Any free variables will be left intact unless a variable name conflicts with a combinator (watch out for i!).

T: λ -> CL

To convert from expressions of lambda calculus to combinatory logic, use the T function:

> (T '(lambda (x) (lambda (y) (y x))))
; (c i)

> (T '(lambda (x) (lambda (y) ((+ (sin x)) (sin y)))))
; ((c ((b b) ((b +) sin))) sin)

L: CL -> λ

To convert from combinatory logic to expressions of lambda calculus, use the L function. The resulting lambda expression is in beta normal form.

> (L '(C I))
; (lambda (a) (lambda (b) (b a)))

> (L '(((C I) 3) sin))
; (sin 3)

> #| racket     |# (define f (eval (L '(C I)) (current-namespace)))
> #| mit-scheme |# (define f (eval (L '(C I)) user-initial-environment))
; f
> ((f 3) sin)
; .1411200080598672

> (T (L '(C I)))
; (c i)

P: λ -> uncurried and pretty

To uncurry and "prettify" a lambda expression, use the P function. This will minimize use of parentheses, spaces, and lambda literals (λaλb.b a -> λab.b a). It returns a string, not a quoted expression like the other functions, so it can use the unicode λ symbol rather than the verbose word lambda.

> (P '(lambda (x) (lambda (y) (lambda (z) ((((f (g x)) z) (lambda (w) ((+ y) w))) b)))))
; "λxyz.f (g x) z (λw.+ y w) b"

> (P (L '(C I)))
; "λab.b a"