lambdaway :: scheme

2 | list | login |load

| |

{require lib_lambdacode}

_h1 scheme, back to λ-calculus | [[white version|?view=scheme2]]

{{block}

_h2 introduction

_p {b Lambdacode} is a homemade {b LISP/SCHEME}-like functional programming language coming with several special forms, {b lambda, def, if, let, set!, ...}, and a set of primitives dealing with booleans, pairs, arrays, numbers, ... See [[lambdacode]] for a quick introduction.

_p Following {b The Lambda Calculus}' notes by [[Don Blaheta|http://cs.brown.edu/courses/cs173/2001/Lectures/2001-10-25.pdf]] we rebuild the language from scratch, focusing on a well known function, the {b factorial}.

_p This is how the factorial function is built using LISP, SCHEME or, in this web page, lambdacode.

{pre {lc
(def fac
 (lambda (n)
  (if (= n 0) 1 (* n (fac (- n 1))))))
-> _(def fac
 (lambda (n)
  (if (= n 0) 1 (* n (fac (- n 1))))))_

(fac 5)
-> _(fac 5)_
}}

_p In this page we rewrite this function at the {b λ-calculus} level, in other words using lambdas exclusively. On the way we will rediscover some basic data and control structures, {b booleans, pairs, lists, numbers, iteration & recursion}.

_p {b Note:} {i All codes can be edited (and so tested) in real time and safely. Just click on the word {b scheme} in the title of the page, {b lambdawalks :: scheme} and do what you want in the page editor.}

_p {i alain marty 2021/10/29}
}

{{block}
_h2 1) lambdas & defs

_p The lambda-calculus is defined this way:

{center {pre x := w | λw.x | xx}}

_p and this is a translation in the lambdacode syntax:

{pre 
exp := word 
    | (lambda (word) exp)
    | (exp exp) }

_p In other words, an expression, {b exp}, is

_ul either a {b word},
_ul or an anonymous function, {b (lambda (word) exp)}, 
_ul or an application, {b (exp exp)}.

_p That's all!

_p As a first example this is a function defined and immediately applied to two values:

{pre {lc
((lambda (a b) (join b a)) 'hello 'world)
-> _((lambda (a b) (join b a)) 'hello 'world)_

}}

_p {b OOPS!} Note that, as a slight exception to our rule, the {b join} primitive is required to deal with sentences, sequences of words. We will never need it when dealing with numbers.
_p And, for convenience, we will add a second special form to facilitate the handling of long expressions, {b (def name expression)}. We will forget it at the end of this exploration.

_p For now, thanks to the {b def} special form the previous example can be splitted into the definition of a function and its application(s) to two words:

{pre {lc
(def SWAP (lambda (a b) (join b a)))
-> _(def SWAP (lambda (a b) (join b a)))_
(SWAP 'hello 'world)
-> _(SWAP 'hello 'world)_
(SWAP 'james 'bond)
-> _(SWAP 'james 'bond)_
...
}}

_p Now we can start building booleans, pairs, lists, numbers and loops.
}

{{block}

_h2 2) data structures

_h3 2.1) booleans

_p {b Booleans} are required to make choices, to build forks.

{pre {lc
(def TRUE (lambda (a b) a))
-> _(def TRUE (lambda (a b) a))_
(def FALSE (lambda (a b) b))
-> _(def FALSE (lambda (a b) b))_
(def IF (lambda (a b c) (a b c)))
-> _(def IF (lambda (a b c) (a b c)))_

(IF TRUE 'yes 'no)
-> _(IF TRUE 'yes 'no)_
(IF FALSE 'yes 'no)
-> _(IF FALSE 'yes 'no)_
}}

_h3 2.2) pairs

_p A {b pair} is a data structure coming with a {b CONS}tructor aggregating two words, two accessors, {b CAR & CDR}, getting each term and two functions, {b NIL & ISNIL}, testing if a pair is NIL or not.

{pre {lc
(def CONS (lambda (a b) (lambda (c) (c a b))))
-> _(def CONS (lambda (a b) (lambda (c) (c a b))))_
(def CAR (lambda (p) (p TRUE)))
-> _(def CAR (lambda (p) (p TRUE)))_
(def CDR (lambda (p) (p FALSE)))
-> _(def CDR (lambda (p) (p FALSE)))_

(def P (CONS 'hello 'world))
-> _(def P (CONS 'hello 'world))_
(CAR P)
-> _(CAR P)_
(CDR P)
-> _(CDR P)_

(def NIL (lambda (x) TRUE)) 
-> _(def NIL (lambda (x) TRUE))_
(def ISNIL (lambda (p) (p (lambda (x y) FALSE))))
-> _(def ISNIL (lambda (p) (p (lambda (x y) FALSE))))_

IF (ISNIL NIL) 'yes 'no)
-> _(IF (ISNIL NIL) 'yes 'no)_

(IF (ISNIL P) 'yes 'no)
-> _(IF (ISNIL P) 'yes 'no)_
}}

_h3 2.3) lists

_p A {b list} is a special case of a pair whose left term is a word and the right term is a pair or {b NIL}. For instance

{pre {lc
(def FRUITS
 (CONS 'apple
  (CONS 'banana
   (CONS 'lemon
    (CONS 'grapes
     (CONS 'orange NIL))))))
-> _(def FRUITS
 (CONS 'apple
  (CONS 'banana
   (CONS 'lemon
    (CONS 'grapes
     (CONS 'orange NIL))))))_ 
}}

_p Note that a list is a {b recursive data structure}.

_h3 2.4) recursion

_p We have all tools required to build a recursive {b control} structure, a {b loop} displaying the list as a sequence of its terms. We could imagine to write

{pre 
(def DISP
 (lambda (l)
  (IF (ISNIL l)
      'STOP
      (join (CAR list) (DISP (CDR l)) )
)))
}

_p meaning "{i if the list is nil then stop else display the first term and do it again with the rest}, but functions are {b geady} and the {b IF} function evaluates the {b then} and {b else} terms before applying the predicate function, {b ISNIL}, leading to an infinite loop...
_p  The workaround is to introduce a kind of {b laziness} using lambdas:

{pre {lc
(def DISP
 (lambda (l)
  ((IF (ISNIL l)
    (lambda (l) ')
    (lambda (l) (join (CAR list) (DISP (CDR l))))) l)))
-> _(def DISP
 (lambda (l)
  ((IF (ISNIL l)
    (lambda (l) ')
    (lambda (l) (join (CAR l) (DISP (CDR l))))) l)))_

(DISP FRUITS)   
-> _(DISP FRUITS)_ 
}}

_p Note that the return value of {b IF} is a either the first or the second lambda, and we want a value, not a function. So we have to apply the chosen function to the list, {b l}, hence the expression {b ((IF (ISNIL l) one two) l)}. See [[coding]] Section 7) for detailed explanations.

_p Let's rewrite this function so that it displays dots instead of terms

{pre {lc
(def LENGTH
 (lambda (l)
  ((IF (ISNIL l)
    (lambda (l) ')
    (lambda (l) (join '• (LENGTH (CDR l))))) l)))
-> _(def LENGTH
 (lambda (l)
  ((IF (ISNIL l)
    (lambda (l) ')
    (lambda (l) (join '• (LENGTH (CDR l))))) l)))_

(LENGTH FRUITS)
-> _(LENGTH FRUITS)_
}}

_p This is a very primitive notation for the number {b 5} and we could build a full set of arithmetical'operarors on them, see [[coding]] Section 8). It's not the way we will choose in this paper.

}

{{block}

_h2 3) arithmetic

_p We will choose the way discovered by the father of λ-calculus, Alonso Church.

_h3 3.1)  church numbers

_p Church numbers are defined as composed functions. The N{sup th} Church number is an {b iterator} applying {b n times} a function to a value, {b (f (f ... (f w)))}. Here are the first ones, {b ZERO, ONE, TWO, THREE}:

{pre {lc
(def ZERO  (lambda (f x) x))
-> _(def ZERO  (lambda (f x) x))_ 
(def ONE (lambda (f x) (f x)))
-> _(def ONE (lambda (f x) (f x)))_
(def TWO (lambda (f x) (f (f x))))
-> _(def TWO (lambda (f x) (f (f x))))_
(def THREE (lambda (f x) (f (f (f (x))))))
-> _(def THREE (lambda (f x) (f (f (f x)))))_
}}

_p For convenience, we will have to display Church numbers as decimal numbers using the {b church} function.

{pre {lc
(def church (lambda (n) (n (lambda (x) (+ x 1)) 0)))
-> _(def church (lambda (n) (n (lambda (x) (+ x 1)) 0)))_

(church TWO)
-> _(church TWO)_
}}

_h3 3.2) a first set of operators

_p Church numbers being iterators, three arithmetic operators can immediately be built , {b SUCCessor, ADDition, MULtiplication}

{pre {lc
(def SUCC (lambda (n) (lambda (x y) (x (n x y)))))
-> _(def SUCC (lambda (n) (lambda (x y) (x (n x y)))))_

(def ADD (lambda (m n) (m SUCC n)))
-> _(def ADD (lambda (m n) (m SUCC n)))_

(def MUL (lambda (m n) (m (lambda (s) (ADD n s)) ZERO) ))
-> _(def MUL (lambda (m n) (m (lambda (s) (ADD n s)) ZERO) ))_

(church (SUCC TWO))
-> _(church (SUCC TWO))_
(church (ADD TWO THREE))
-> _(church (ADD TWO THREE))_
(church (MUL TWO THREE))
-> _(church (MUL TWO THREE))_

}}

_h3 3.3) a second set of operators

_p Computing the PREDecessor and SUBtraction operators is more tricky, thanks to Kleene. Concerning the first one the idea is sketched below:
{pre
0: (0   0)
1: (0   1)
2: (1   2)
3: (2   3)
...
n: (n-1 n) -> get the left one
}

_p leading to this code:

{pre {lc
(def PRED
 (lambda (n) 
  (CAR (n (lambda (p)
           (CONS (CDR p) (SUCC (CDR p)) ))
           (CONS ZERO ZERO)))))
-> _(def PRED
 (lambda (n) 
  (CAR (n (lambda (p)
   (CONS (CDR p) (SUCC (CDR p)) ))
   (CONS ZERO ZERO)))))_

(church (PRED ONE))
-> _(church (PRED ONE))_
(church (PRED ZERO))
-> _(church (PRED ZERO))_    // nothing under ZERO
}}

_p The {b SUB} operator can be built similarily to the {b ADD} operator

{pre {lc
(def SUB (lambda (m n) (n PRED m)))
-> _(def SUB (lambda (m n) (n PRED m)))_

(church (SUB THREE TWO))
->_(church (SUB THREE TWO))_
(church (SUB TWO TWO))
-> _(church (SUB TWO TWO))_
(church (SUB TWO THREE))
-> _(church (SUB TWO THREE))_
}}

_p Note that there is no number under ZERO.

}

{{block}

_h2 4) loops

_h3 4.1) iteration

_p The factorial code can follow the idea used for PRED:

{pre {lc
(def ifac
 (lambda (n) 
  (CDR (n (lambda (p)
   (CONS (SUCC (CAR p)) (MUL (CAR p) (CDR p))))
   (CONS ONE ONE)))))
-> _(def ifac
 (lambda (n) 
  (CDR (n (lambda (p)
   (CONS (SUCC (CAR p)) (MUL (CAR p) (CDR p))))
   (CONS ONE ONE)))))_

(def N (SUCC (SUCC (SUCC (SUCC (SUCC ZERO))))))
-> _(def N (SUCC (SUCC (SUCC (SUCC (SUCC ZERO))))))_
(church N)
-> _(church N)_

(church (ifac N))
-> _(church (ifac N))_

}}

_h3 4.2) recursion

_p We explore now the recursive way. First let's define a function testing if a number is ZERO

{pre {lc
(def ISZERO (lambda (n) (n (lambda (x) FALSE) TRUE)))
-> _(def ISZERO (lambda (n) (n (lambda (x) FALSE) TRUE)))_

(IF (ISZERO ZERO) 'yes 'no)
-> _(IF (ISZERO ZERO) 'yes 'no)_
(IF (ISZERO ONE) 'yes 'no)
-> _(IF (ISZERO ONE) 'yes 'no)_
}}

_p Here is a recursive code for the factorial

{pre {lc
(def rfac
 (lambda (n)
  ((IF (ISZERO n)
   (lambda (n) ONE)
   (lambda (n) (MUL n (rfac (PRED n))))) n)))
-> _(def rfac
 (lambda (n)
  ((IF (ISZERO n)
   (lambda (n) ONE)
   (lambda (n) (MUL n (rfac (PRED n))))) n)))_

(church (rfac N))
-> _(church (rfac N))_
}}

_p This code works similarily to the {b DISP code}.

_h3 4.3) Y combinator

_p A recursive function calls its name in its body. Sometimes it's better to avoid naming and here is the Y-combinator

{pre {lc
(def Y
 (lambda (h)
  ((lambda (x) (h (lambda (a) ((x x) a))))
   (lambda (x) (h (lambda (a) ((x x) a)))))))
-> _(def Y
 (lambda (h)
  ((lambda (x) (h (lambda (a) ((x x) a))))
   (lambda (x) (h (lambda (a) ((x x) a)))))))_

(def yfac
 (lambda (g)
   (lambda (x)
    ((IF (ISZERO x)
     (lambda (x) (SUCC ZERO))
     (lambda (x) (MUL x (g (PRED x))))) x))))
-> _(def yfac
 (lambda (g)
   (lambda (x)
    ((IF (ISZERO x)
     (lambda (x) (SUCC ZERO))
     (lambda (x) (MUL x (g (PRED x))))) x))))_

(church ((Y yfac) N))
-> _(church ((Y yfac) N))_

}}

_p {b Note:} In his paper Don Blaheta writes (page 7, note 9)  " {i In fact, the lambda calculus always requires lazy evaluation; there is a parallel theory known as the lambda-value calculus in which eager evaluation is used. It is left as an exercise to the reader how to modify the example so that it would work in an eager regime.} " The Y-combinator given here could be an answer.

°°°
{pre {lc
_(def Z (lambda (h) (h h)))_

_(def zfac
   (lambda (g x)
    ((IF (ISZERO x)
     (lambda (g x) (SUCC ZERO))
     (lambda (g x) (MUL x (g g (PRED x)))) g x))))_

-> ;; _(church (Z zfac N))_
}}
°°°
}

{{block}
_h2 conclusion

_p Names are optionel and we can forget them, simply using their lambda expressions. For instance this is what the {b ifac} function becomes:

{pre {lc
(def λfac
(lambda (n) 
 ((lambda (p) (p 
   (lambda (a b) b))) (n 
    (lambda (p)
    ((lambda (a b) 
      (lambda (c) (c a b))) 
      ((lambda (n) 
        (lambda (x y) (x (n x y)))) 
        ((lambda (p) (p 
          (lambda (a b) a))) p))
          ((lambda (m n) (m 
            (lambda (s) 
            ((lambda (m n) (m 
              (lambda (n) 
               (lambda (x y) (x (n x y)))) n)) n s)) 
                (lambda (f x) x)) ) 
                ((lambda (p) (p 
                  (lambda (a b) a))) p) 
                  ((lambda (p) (p 
                    (lambda (a b) b))) p))))
                    ((lambda (a b) 
                      (lambda (c) (c a b))) 
                       (lambda (f x) (f x)) 
                        (lambda (f x) (f x))))))) 
-> _(def λfac
(lambda (n) 
 ((lambda (p) (p 
   (lambda (a b) b))) (n 
    (lambda (p)
    ((lambda (a b) 
      (lambda (c) (c a b))) 
      ((lambda (n) 
        (lambda (x y) (x (n x y)))) 
        ((lambda (p) (p 
          (lambda (a b) a))) p))
          ((lambda (m n) (m 
            (lambda (s) 
            ((lambda (m n) (m 
              (lambda (n) 
               (lambda (x y) (x (n x y)))) n)) n s)) 
                (lambda (f x) x)) ) 
                ((lambda (p) (p 
                  (lambda (a b) a))) p) 
                  ((lambda (p) (p 
                    (lambda (a b) b))) p))))
                    ((lambda (a b) 
                      (lambda (c) (c a b))) 
                       (lambda (f x) (f x)) 
                        (lambda (f x) (f x)))))))_
 
(church (λfac N))
-> _(church (λfac N))_
}}

;; _p We are now down to the level of pure λ-calculus and this is the end of the journey.

_p I leave the last words to Don Blaheta:

{blockquote {@ style="padding:10px; transform:rotate(-2deg);"}

_p We have now reduced our language to the following three-case grammar:

{center {pre
Λ :== ⟨var⟩ | (Λ Λ) | (λ(var) Λ)
}}
_p The language Λ has, simply, variables, function application, and abstraction; nothing else. It is known as the lambda calculus, and its development in the 1930s made theoreticians deliriously happy, because A) it strongly lends itself to inductive proofs, and B) the proofs need only deal with three cases!
_p Back in the 1930s, a lot of people were asking the question, “what can we com- pute?” This was not a trivial question, as it had important bearing on whether one language (or method of computation) was ‘more powerful’ than another (is C more powerful than Scheme? and so on). Turing tried and succeeded in reducing a huge variety of computation to a few simple operations involving a tape with a read/write head; meanwhile Church, Curry, et al were attacking the same problem from a completely different direction, and reduced a huge variety of computation to the lambda calculus. Happily, it was proven that Turing’s tape machine and Church’s lambda calculus are isomorphic—an algorithm in one can be reduced to an algorithm for the other—so that theoreticians can prove things under one system or the other, as convenient. Obviously, though, the ones that prove using the lambda calculus are much cooler.
}

_p All is said.

_p {i alain marty 2021/10/29}

_p [[HN|https://news.ycombinator.com/item?id=29037432]]
}

{{hide}
{def block 
  div {@ style="display:inline-block; 
                width:500px; vertical-align:top; margin:10px; padding:5px;
               "}}
}

{style 
body, .page_menu { background:#444; color:#fff; }
#page_frame { border:0; width:600px; margin-left:0; background:transparent; }
#page_content { background:transparent; border:0; width:3400px; box-shadow:0 0 0; font-family:papyrus, optima; }
pre { box-shadow:0 0 8px #000; padding:10px; }
}