How to implement a recursive function in lambda ca

问题:

I'm studying lambda calculus with the book "An Introduction to Functional Programming Through Lambda Calculus" by Greg Michaelson.

I implement examples in Clojure using only a subset of the language. I only allow :

• symbols
• one-arg lambda functions
• function application
• var definition for convenience.

So far I have those functions working :

(def identity (fn [x] x))
(def self-application (fn [s] (s s)))

(def select-first (fn [first] (fn [second] first)))
(def select-second (fn [first] (fn [second] second)))
(def make-pair (fn [first] (fn [second] (fn [func] ((func first) second)))))    ;; def make-pair =  λfirst.λsecond.λfunc.((func first) second)

(def cond make-pair)
(def True select-first)
(def False select-second)

(def zero identity)
(def succ (fn [n-1] (fn [s] ((s False) n-1))))
(def one (succ zero))
(def zero? (fn [n] (n select-first)))
(def pred (fn [n] (((zero? n) zero) (n select-second))))

But now I am stuck on recursive functions. More precisely on the implementation of add. The first attempt mentioned in the book is this one :

(def add-1
  (fn [a]
    (fn [b]
      (((cond a) ((add-1 (succ a)) (pred b))) (zero? b)))))

((add zero) zero)

Lambda calculus rules of reduction force to replace the inner call to add-1 with the actual definition that contains the definition itself... endlessly.

In Clojure, wich is an application order language, add-1 is also elvaluated eagerly before any execution of any kind, and we got a StackOverflowError.

After some fumblings, the book propose a contraption that is used to avoid the infinite replacements of the previous example.

(def add2 (fn [f]
            (fn [a]
              (fn [b]
                (((zero? b) a) (((f f) (succ a)) (pred b)))))))
(def add (add2 add2))

The definition of add expands to

(def add (fn [a] 
           (fn [b]
             (((zero? b) a) (((add2 add2) (succ a)) (pred b)))))) 

Which is totally fine until we try it! This is what Clojure will do (referential transparency) :

((add zero) zero)
;; ~=>
(((zero? zero) zero) (((add2 add2) (succ zero)) (pred zero)))
;; ~=>
((select-first zero) (((add2 add2) (succ zero)) (pred zero)))
;; ~=>
((fn [second] zero) ((add (succ zero)) (pred zero)))

On the last line (fn [second] zero) is a lambda that expects one argument when applied. Here the argument is ((add (succ zero)) (pred zero)). Clojure is an "applicative order" language so the argument is evaluated before function application, even if in that case the argument won't be used at all. Here we recur in add that will recur in add... until the stack blows up. In a language like Haskell I think that would be fine because it's lazy (normal order), but I'm using Clojure.

After that, the book go in length presenting the tasty Y-combinator that avoid the boilerplate but I came to the same gruesome conclusion.

EDIT

As @amalloy suggests, I defined the Z combinator :

(def YC (fn [f] ((fn [x] (f (fn [z] ((x x) z)))) (fn [x] (f (fn [z] ((x x) z)))))))

I defined add2 like this :

(def add2 (fn [f]
            (fn [a]
              (fn [b]
                (((zero? b) a) ((f (succ a)) (pred b)))))))

And I used it like this :

(((YC add2) zero) zero)

But I still get a StackOverflow.

I tried to expand the function "by hand" but after 5 rounds of beta reduction, it looks like it expands infinitely in a forest of parens.

So what is the trick to make Clojure "normal order" and not "applicative order" without macros. Is it even possible ? Is it even the solution to my question ?

This question is very close to this one : How to implement iteration of lambda calculus using scheme lisp? . Except that mine is about Clojure and not necessarily about Y-Combinator.

回答1:

For strict languages, you need the Z combinator instead of the Y combinator. It's the same basic idea but replacing (x x) with (fn [v] (x x) v) so that the self-reference is wrapped in a lambda, meaning it is only evaluated if needed.

You also need to fix your definition of booleans in order to make them work in a strict language: you can't just pass it the two values you care about and select between them. Instead, you pass it thunks for computing the two values you care about, and call the appropriate function with a dummy argument. That is, just as you fix the Y combinator by eta-expanding the recursive call, you fix booleans by eta-expanding the two branches of the if and eta-reduce the boolean itself (I'm not 100% sure that eta-reducing is the right term here).

(def add2 (fn [f]
            (fn [a]
              (fn [b]
                ((((zero? b) (fn [_] a)) (fn [_] ((f (succ a)) (pred b)))) b)))))

Note that both branches of the if are now wrapped with (fn [_] ...), and the if itself is wrapped with (... b), where b is a value I chose arbitrarily to pass in; you could pass zero instead, or anything at all.

回答2:

The problem I'm seeing is that you have too strong of a coupling between your Clojure program and your Lambda Calculus program

1. you're using Clojure lambdas to represent LC lambdas
2. you're using Clojure variables/definitions to represent LC variables/definitions
3. you're using Clojure's application mechanism (Clojure's evaluator) as LC's application mechanism

So you're actually writing a clojure program (not an LC program) that is subject to the effects of the clojure compiler/evaluator – which means strict evaluation and non-constant-space direction recursion. Let's look at:

(def add2 (fn [f]
            (fn [a]
              (fn [b]
                (((zero? b) a) ((f (succ a)) (pred b)))))))

As a Clojure program, in a strictly evaluated environment, each time we call add2, we evaluate

1. (zero? b) as value1
2. (value1 a) as value2
3. (succ a) as value3
4. (f value2) as value4
5. (pred b) as value5
6. (value2 value4) as value6
7. (value6 value5)

We can now see that calling to add2 always results in call to the recursion mechanism f – of course the program never terminates and we get a stack overflow!

---

You have a few options

1. per @amalloy's suggestions, use thunks to delay the evaluation of certain expressions and then force (run) them when you're ready to continue the computation – tho I don't think this is going to teach you much

2. you can use Clojure's loop/recur or trampoline for constant-space recursions to implement your Y or Z combinator – there's a little hang-up here tho because you're only wishing to support single-parameter lambdas, and it's going to be a tricky (maybe impossible) to do so in a strict evaluator that doesn't optimise tail calls

   I do a lot of this kind of work in JS because most JS machines suffer the same problem; if you're interested in seeing homebrew workarounds, check out: How do I replace while loops with a functional programming alternative without tail call optimization?

3. write an actual evaluator – this means you can decouple your the representation of your Lambda Calculus program from datatypes and behaviours of Clojure and Clojure's compiler/evaluator – you get to choose how those things work because you're the one writing the evaluator

   I've never done this exercise in Clojure, but I've done it a couple times in JavaScript – the learning experience is transformative. Just last week, I wrote https://repl.it/Kluo which is uses a normal order substitution model of evaluation. The evaluator here is not stack-safe for large LC programs, but you can see that recursion is supported via Curry's Y on line 113 - it supports the same recursion depth in the LC program as the underlying JS machine supports. Here's another evaluator using memoisation and the more familiar environment model: https://repl.it/DHAT/2 – also inherits the recursion limit of the underlying JS machine

   Making recursion stack-safe is really difficult in JavaScript, as I linked above, and (sometimes) considerable transformations need to take place in your code before you can make it stack-safe. It took me two months of many sleepless nights to adapt this to a stack-safe, normal-order, call-by-need evaluator: https://repl.it/DIfs/2 – this is like Haskell or Racket's #lang lazy

   As for doing this in Clojure, the JavaScript code could be easily adapted, but I don't know enough Clojure to show you what a sensible evaluator program might look like – In the book, Structure and Interpretation of Computer Programs, (chapter 4), the authors show you how to write an evaluator for Scheme (a Lisp) using Scheme itself. Of course this is 10x more complicated than primitive Lambda Calculus, so it stands to reason that if you can write a Scheme evaluator, you can write an LC one too. This might be more helpful to you because the code examples look much more like Clojure

---

a starting point

I studied a little Clojure for you and came up with this – it's only the beginning of a strict evaluator, but it should give you an idea of how little work it takes to get pretty close to a working solution.

Notice we use a fn when we evaluate a 'lambda but this detail is not revealed to the user of the program. The same is true for the env – ie, the env is just an implementation detail and should not be the user's concern.

To beat a dead horse, you can see that the substitution evaluator and the environment-based evaluator both arrive at the equivalent answers for same input program – I can't stress enough how these choices are up to you – in SICP, the authors even go on to change the evaluator to use a simple register-based model for binding variables and calling procs. The possibilities are endless because we've elected to control the evaluation; writing everything in Clojure (as you did originally) does not give us that kind of flexibility

;; lambda calculus expression constructors
(defn variable [identifier]
  (list 'variable identifier))

(defn lambda [parameter body]
  (list 'lambda parameter body))

(defn application [proc argument]
  (list 'application proc argument))

;; environment abstraction
(defn empty-env []
  (hash-map))

(defn env-get [env key]
  ;; implement
)

(defn env-set [env key value]
  ;; implement
)

;; meat & potatoes
(defn evaluate [env expr]
  (case (first expr)
    ;; evaluate a variable
    variable (let [[_ identifier] expr]
               (env-get env identifier))

    ;; evaluate a lambda
    lambda (let [[_ parameter body] expr]
             (fn [argument] (evaluate (env-set env parameter argument) body)))

    ;; evaluate an application
    ;; this is strict because the argument is evaluated first before being given to the evaluated proc
    application (let [[_ proc argument] expr]
                  ((evaluate env proc) (evaluate env argument)))

    ;; bad expression given
    (throw (ex-info "invalid expression" {:expr expr}))))


(evaluate (empty-env)
          ;; ((λx.x) y)
          (application (lambda 'x (variable 'x)) (variable 'y))) ;; should be 'y

_{* or it could throw an error for unbound identifier 'y; your choice}