Point-free style is a programming style in which functions are defined without mentioning their arguments. For a simple example, the function definition
1 2
(define (h x) (g (f x)))
can be converted into a point-free one
1
(define h (compose g f))
with the function composition combinator
1 2
(define (compose g f) (lambda (x) (g (f x)))
Is it possible to transform any function definition to point-free style with a suitable set of combinators?
The goal
Let’s reframe the problem in the -calculus to make it clear. There are three elements in the -calculus,
1 2 3
e = x (variable) | λx.e (abstraction) | e₁ e₂ (application)
Our goal is to find some combinators , , … , so that we can express every term in the -calculus through the use of variables, combinators, and applications, but without using lambda abstractions. In other words, we can write everything in the form
1 2 3
e = x (variable) | K (combinator) | e₁ e₂ (application)
Work it out
1 2
;; convert a term into an equivalent point-free form (define (to-point-free e) ...)
The first two cases are straightforward.
1 2 3 4 5 6
;; convert a term into an equivalent point-free form (define (to-point-free e) (match e [(? symbol? x) x] ; var [`(,e1 ,e2) `(,(to-point-free e1) ,(to-point-free e2))] ; app ...))
The real work begins when we try to eliminate λ-abstractions.
1
[`(λ (,(? symbol? x)) ,e) (... (to-point-free e))] ;; what to do?
Suppose we have transformed into a point-free version through a recursive call. There is no general way to combine with some combinators to get back , because may occur free in , but is always bound in . So we’ll have to look into . Let’s make the ... above into a helper function elim-λ, so the above line of code becomes
1
[`(λ (,(? symbol? x)) ,e) (elim-λ x (to-point-free e))]
We are left to define
1 2 3 4
;; eliminate a λ-abstraction whose body is point-free (define (elim-λ x e) (match e ...))
Note that we only pass point-free to elim-λ. So could only be a variable or an application.
1 2 3 4
(define (elim-λ x e) (match e [(? symbol? y) ...] [`(,e1 ,e2) ...]))
If is a bound variable in , we will get , which is the simplest closed term other than varaibles, so we we designate a combinator for it. Otherwise if occurs free, we have . Then the final result could be as simple as for some combinator . Indeed there is satisfying the above equation. Hence
1
[(? symbol? y) (if (eq? x y) 'I `(K ,y))]
Now there is only one case left
1
[`(,e1 ,e2) ...]
Again, because may occur free in and , there is no way we can directly use them. However, we can somehow eliminate the free occurrences of in by replacing with , and no longer occurs free in . Note that is point-free, and has strictly smaller size than , we can recursively transform into point-free form by elim-λ. Then we have . We only need to find a combinator such that . An obvious solution is . Thus
1
[`(,e1 ,e2) `((S ,(elim-λ x e1)) ,(elim-λ x e2))]
The complete code
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
#lang racket (define I (λ (x) x))
(define K (λ (x) (λ (y) x)))
(define S (λ (x) (λ (y) (λ (z) ((x z) (y z))))))
(define (to-point-free e) (define (elim-λ x e) (match e [(? symbol? y) (if (eq? x y) 'I `(K ,y))] [`(,e1 ,e2) `((S ,(elim-λ x e1)) ,(elim-λ x e2))])) (match e [(? symbol? x) x] ; var [`(,e1 ,e2) `(,(to-point-free e1) ,(to-point-free e2))] ; app [`(λ (,(? symbol? x)) ,e) (elim-λ x (to-point-free e))] ; abs ))