Some differences between lambda-calculus and Lisp (2).

; This is the second part of  previous post . ; ; ; ;                4. Evaluation in Lisp vs. ;    reduction to normal form in lambda-calculus ; ; ; As noted in previous post, in Lisp, evaluation of the function ; application is defined recursively: ; ;      1.  evaluation of the function arguments is performed ;      2.  resulting values are assigned to the parameters of ;          the function ;      2.  evaluation of the function body is performed ; ; In lambda calculus, beta-reductions do not recurse on that way. ; There is no "automatic" beta-reductions of the argument of the ; application. ; ; Because of that, in general case, one applies reductions many ; times to achieve similar effect. How many times? Typically, ; until further reduction is impossible; in that case, it is ; said that expression is reduced to normal form. ; ; There are few differences between evaluation in Lisp and ; reduction to normal form in lambda-calculus: ; ; ;              4.1. Order of reductions in ;            lambda-calculus is not defined ; ; ; Lambda-calculus is not an algorithm. It is a "formal system". One ; who performs reductions - human or computer - can pick the order of ; reductions by any criteria. ; ; ;     4.2. Lisp evaluation strategy is not the best for ;                     lambda-calculus ; ; ; In Lisp, order of evaluations is "from inside"; if application ; is evaluated, for example, ; ;          ((lambda(x)(+ x x)) ((lambda(x)(* x x)) 3) 2) ; ; then inner left argument, in this case ; ;                     ((lambda(x)(* x x)) 3) ; ; is evaluated first. That order is called "applicative order". ; In lambda-calculus, some expressions cannot be reduced applying ; that order of reductions. For example, ; ;               ((^x.a) ((^x.(x x)) (^x.(x x)))) ; ; would be reduced indefinitely, because reduction of ; ;                   ((^x.(x x)) (^x.(x x))) ; ; doesn't terminate. Some other evaluation strategies, for example, ; "normal order", "from outside", as defined in lambda-Church, terminate: ; (println ((lambda-Church (x) a) ((lambda-Church(x)(x x))                                  (lambda-Church(x)(x x)))))                                   ;        => a ; ; ; ;        4.3. Reduction to normal form is more ;           extensive than single evaluation ; ; ; 1. In Lisp, function, like ; ;              (lambda(x)((lambda(y)y) x)), ; ;    if evaluated is either evaluated to some "compiled value", ;    i.e. it is not S-expression any more - or evaluates to ;    itself, as in Newlisp. ;     ;    In lambda-calculus, reduction is performed inside the function ;    body. For example, ; ;               (^x.((^y.y) x)) => (^x.x). ; ; 2. In Lisp, result of the evaluation of the S-expression is frequently ;    in form that allows further evaluation. ; ;               ((lambda(x)(list '+ 1 2 x)) 3) => '(+ 1 2 3) ; ;But, it is not evaluated automatically. ; ; ; To be continued ...