How to implement iteration of lambda calculus using scheme lisp?

Question

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.

Pinnule

Answer 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)).

Sheer

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 – Westcott

@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! :) – Sheer

Thanks @will-ness ! Your claim sounds more legit than mine. I'll ask a question and ping you :) Thanks – Westcott

Hey @WillNess. I asked a new question : #46061844 . Thanks for your help ! – Westcott

@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. – Sheer

Answer 2

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

Amboina

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. – Doscher

@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 – Amboina

@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. en.wikipedia.org/wiki/Lambda_calculus#Reduction_strategies says e.g., "Full beta reductions ... means essentially the lack of any particular reduction strategy" etc. – Sheer

@willness but that means it's undecided if a program halts or not even if we know it will terminate with one reduction strategy? – Amboina

@Amboina 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. – Sheer