How to implement a recursive function in lambda calculus using a subset of the Clojure language?

Question

I study lambda calculus using the book "Introduction to Functional Programming through the Lambda Calculus" by Greg Michaelson.

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

• Characters
• functions with one argument lambda
• attachment
• var definition for convenience.

So far I have these functions:

(def identity (fn [x] x)) (def self-application (fn [s] (ss))) (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'm stuck on recursive functions. More precisely, about the implementation of add . The first attempt mentioned in the book is as follows:

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

The rules for calculating the lambda of reduction force in order to replace the internal call with add-1 actual definition containing the definition itself ... are infinite.

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

After some mistakes, the book will suggest a fixture that is used to avoid endless replacements of the previous example.

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

The definition of add extends to

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

This is absolutely normal until we try! 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))) 

The last line (fn [second] zero) has a lambda that expects one argument when applied. Here's the argument ((add (succ zero)) (pred zero)) . Clojure is an "application-oriented" language, so the argument is evaluated before the functional application, even if in this case the argument will not be used at all. Here we return to add , which will be repeated in add ... until the stack explodes. In a language like Haskell, I think that would be nice because it is lazy (normal order), but I use Clojure.

After that, the book goes long, introducing a delicious Y-combinator that avoids the pattern, but I came to the same terrible conclusion.

EDIT

As @amalloy suggests, I defined the Z combinator:

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

I defined add2 as follows:

 (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 StackOverflow.

I tried to expand the function "manually", but after 5 rounds of beta reduction, it looks like it expands indefinitely in the parens forest.

So what trick do Clojure "normal order" and not "applicative order" without macros. Is it possible? Is this even a solution to my question?

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

Answer 1

For strict languages, you need Z combinator instead of Y combinator. This is the same basic idea, but replacing (xx) with (fn [v] (xx) v) so that self-promotion is wrapped in lambda, which means that it is evaluated only when necessary.

You also need to correct your definition of Boolean languages ​​in order to make them work in a strict language: you cannot just pass it the two meanings that you need and choose between them. Instead, you pass it thunks to compute the two values ​​you need, and call the corresponding function with a dummy argument. Just as you fix Y combinator by eta-extending a recursive call, you are correcting Boolean by eta-extending the two if and eta-reduce branches of the logical element itself (I'm not 100% sure that eta- shrinking is the right term) .

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

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

Answer 2

The problem that I see is that your connection between your Clojure program and the Lambda Calculus program is too strong

• you use Clojure lambdas to represent LC lambdas
• you use Clojure variables / definitions to represent LC variables / definitions
• you use the Clojure app engine (Clojure evaluator) as an LC application engine

So, you are actually writing a Clojure program (not an LC program) that is subject to the effects of the Clojure compiler / evaluator, which means rigorous evaluation and recursion of the direction of non-constant space. 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, every time we call add2 , we evaluate

• (zero? b) as value1
• (value1 a) as value2
• (succ a) as value3
• (f value2) as value4
• (pred b) as value5
• (value2 value4) as value6
• (value6 value5)

Now we can see that a call to add2 always leads to a call to the recursion mechanism f - of course, the program never ends and we get a stack overflow!

---

You have several options.

• for @amalloy's suggestions, use thunks to defer evaluation of certain expressions, and then force (run) them when you are ready to continue the calculation - I don't think this will teach you much

• you can use a Clojure loop / recur or trampoline for constant space recursions to implement the Y or Z combinator - it hangs a bit here because you're only to support one-parameter lambdas and it will be difficult (possibly impossible) to do this in a rigorous evaluator that does not optimize tail calls

  I work a lot in JS because most JS machines experience the same problem; If you are interested in workarounds for homebrew methods, check out: How to replace loops with alternative functional programming without tail call optimization?

• write the actual evaluator - this means that you can separate your presentation from your Lambda Calculus program from the data types and behavior of / w120> and the compiler / evaluator Clojure - you can choose how these things work because you're the one who writes the evaluator

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

  Creating a recursive stack is actually very difficult in JavaScript, as I said above, and (sometimes) significant changes must occur in your code before you can make it safe for the stack. It took me two months of sleepless nights to adapt this to a balanced stack expert, normal order: https://repl.it/DIfs/2 - it's like Haskell or Racket #lang lazy

  Regarding this in Clojure, JavaScript code can be easily adapted, but I don’t know enough Clojure to show you what a reasonable evaluator program might look like. In the book The Structure and Interpretation of Computer Programs , (chapter 4), the authors show how to write an evaluator for a Schema (a Lisp) using the Schema itself. Of course, this is 10 times more complicated than the primitive lambda calculus, so it’s quite reasonable that if you can write a Schema evaluator, you can also write LC. This might be more useful to you because the code examples look much more like Clojure

---

starting point

I studied a little Clojure for you and came up with this - this is only the beginning of a rigorous evaluator, but it should give you an idea of ​​how little work is required to get closer to a working solution.

Please note that we use fn when evaluating a 'lambda , but this detail is not disclosed to the user of the program. The same is true for env - i.e. env is just an implementation detail and should not be a problem for the user.

To defeat a dead horse, you can see that the substitution evaluator and the environment-based evaluator come up with equivalent answers for the same input program - I cannot stress enough how these options are right for you - in SICP, the authors even continue change the evaluator to use a simple case-based model to bind variables and call procs. The possibilities are endless because we decided to control the evaluation; writing everything in Clojure (as you originally did) doesn't give us that much 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 may throw an error for the unrelated identifier 'y; your choice}