1

I'm trying to learn lambda calculus and Scheme Lisp. The tutorial on lambda calculus can be found here http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf.

The problem I'm facing is I don't know how to properly implement iteration.

(define (Y y) (((lambda (x) (y (x x))) (lambda (x) (y (x x))))))
(define (sum r n) ((is_zero n) n0 (n succ (r (pred n)))))
(display ((Y sum) n5))

I always get this error:

Aborting!: maximum recursion depth exceeded

I know the problem is about the evaluation order: the scheme interprets (Y sum) first, which results in infinite recursion:

((Y sum) n5) -> (sum (Y sum) n5) -> ((sum (sum (Y sum))) n5) -> .... (infinite recursion)

but I want

((Y sum) n5) -> ((sum (Y sum) n5) -> (n5 succ ((Y sum) n4)) -> .... (finite recursion)

How can I solve this problem? thanks.

Will Ness
  • 70,110
  • 9
  • 98
  • 181
PeopleMoutainPeopleSea
  • 1,492
  • 1
  • 15
  • 24

2 Answers2

1

The standard way to delay a computation is by eta-expansion:

(define (Y y) ((lambda (x) (y (x x))) (lambda (x) (y (x x) )) ))
=~
(define (YC y) ((lambda (x) (y (lambda (z) ((x x) z))))
                (lambda (x) (y (lambda (z) ((x x) z)))) ))

Thus

((YC sum) n5) 
=
  (let* ((y sum)
         (x (lambda (x) (y (lambda (z) ((x x) z)))) ))
    ((y (lambda (z) ((x x) z))) n5))
= 
  (let ((x (lambda (x) (sum (lambda (z) ((x x) z)))) ))
    ((sum (lambda (z) ((x x) z))) n5))
= 
  ...

and evaluating (sum (lambda (z) ((x x) z))) just uses the lambda-function which contains the self-application, but doesn't invoke it yet.

The expansion will get to the point

(n5 succ ((lambda (z) ((x x) z)) n4))
=
(n5 succ ((x x) n4))    where x = (lambda (x) (sum (lambda (z) ((x x) z))))

and only at that point will the self-application be performed.

Thus, (YC sum) = (sum (lambda (z) ((YC sum) z))), instead of the diverging (under the applicative order of evaluation) (Y sum) = (sum (Y sum)).

Will Ness
  • 70,110
  • 9
  • 98
  • 181
  • Hello, I've the exactly same problem in Clojure rather Scheme. I tried the YC combinator but I still get a StackOverflowError. I came to the conclusion that we can't have recursion if expressions are not evaluated. Recursive functions likely come with an `if` statement. In clojure `if` is not a function, it's a special keyword that doesn't evaluate the second branch when condition is true. However `if` is a function in lambda-calculus where branches are arguments. Clojure evaluates arguments eagerly, one of them being a recursive call hence the StackOverflowError – Demeter Purjon Sep 04 '17 at 10:53
  • 1
    @DemeterPurjon no, in Scheme `if` doesn't evaluate all of its arguments either. `factorial` has `if` in it and can be coded with `YC` fine. also, in LC (lambda calculus) nothing is evaluated if not needed, it is "normal order evaluation" i.e. "evaluation by name" ("lazy"). What is your code? You could try asking your question on SO, including all the pertinent code, :) desired outcome and what really happens. If you do, @ ping me here so I don't miss it! :) – Will Ness Sep 04 '17 at 13:40
  • Thanks @will-ness ! Your claim sounds more legit than mine. I'll ask a question and ping you :) Thanks – Demeter Purjon Sep 04 '17 at 18:27
  • Hey @WillNess. I asked a new question : https://stackoverflow.com/questions/46061344/how-to-implement-a-recursive-function-in-lambda-calculus-using-a-subset-of-cloju . Thanks for your help ! – Demeter Purjon Sep 05 '17 at 18:42
  • @DemeterPurjon As I suspected, it turned out Clojure has its own specific problems, i.e. the lack of tail call optimization (I don't use Clojure). Hopefully you'll get help from someone knowledgeable in Clojure as to implementing your own trampoline there. TCO is guaranteed under Scheme, and YC code relies on it. – Will Ness Sep 07 '17 at 18:27
1

Lambda calculus is a normal order evaluating language. Thus it has more in common with Haskell than Scheme, which is an applicative order evaluating language.

In DrRacket you have a dialect #lang lazy, which is as close to Scheme you get, but since its lazy you have normal order evaluation:

#!lang lazy

(define (Y f) 
  ((lambda (x) (x x)) 
   (lambda (x) (f (x x)))))

(define sum
  (Y (lambda (r)
       (lambda (n)
         ((is_zero n) n0 (n succ (r (pred n))))))))

(church->number (sum n5))

If you cannot change the language you can just wrap it in a lambda to get it delayed. eg.

if r is a function of arity 1, which all functions in lambda calculus is, then (lambda (x) (r x)) is a perfectly ok refactoring of r. It will halt the infitie recursion since you only get the wrapper and it only applies it every time you recurse even if the evaluation is eager. Y combinator in an eager language is called Z:

(define (Z f) 
  ((lambda (x) (x x)) 
   (lambda (x) (f (lambda (d) ((x x) d))))))

If you want to do Z in Scheme, eg with multiple argument recursive functions you use rest arguments:

(define (Z f) 
  ((lambda (x) (x x)) 
   (lambda (x) (f (lambda args (apply (x x) args))))))

((Z (lambda (ackermann)
      (lambda (m n)
        (cond
          ((= m 0) (+ n 1))
          ((= n 0) (ackermann (- m 1) 1))
          (else (ackermann (- m 1) (ackermann m (- n 1))))))))
 3
 6) ; ==> 509
Sylwester
  • 47,942
  • 4
  • 47
  • 79
  • i remember being corrected once that The Lambda Calculus has no specified evaluation strategy – any strategy can be employed. if i'm able to find it, i will link it. – Mulan Sep 02 '17 at 19:28
  • @naomik Lambda calculus execution is by beta reduction until it can no more, thus we hit normal form. [Applicative order reduction may not terminate, even when the term has a normal form](https://en.wikipedia.org/wiki/Beta_normal_form) – Sylwester Sep 02 '17 at 22:05
  • @naomik I'm pretty sure you're correct here, and having no fixed reduction strategy is what enables the LC's investigation of properties of various reduction strategies in the first place. https://en.wikipedia.org/wiki/Lambda_calculus#Reduction_strategies says e.g., "Full beta reductions ... means essentially the lack of any particular reduction strategy" etc. – Will Ness Sep 25 '17 at 09:10
  • @willness but that means it's undecided if a program halts or not even if we know it will terminate with one reduction strategy? – Sylwester Sep 25 '17 at 10:55
  • @Sylwester I think it just means that a choice of a reduction strategy is outside of LC itself. a program may terminate with one choice, and not, with another. Of course a given programming language would typically have that choice baked in. – Will Ness Sep 25 '17 at 18:55