[ create a new paste ] login | about

Link: http://codepad.org/2Ucz5Nz7    [ raw code | output | fork | 1 comment ]

fisherro - Scheme, pasted on Aug 31:
;#lang r5rs
;        11111111112222222222333333333344444444445555555555666666666677777777778
;2345678901234567890123456789012345678901234567890123456789012345678901234567890

; ABOUT
;
; Herein I am exploring the lambda calculus through Scheme.
; Using only define and lambda, I'll build up language features.
; (Though Scheme will be needed for communicating with the world.)
;
; A couple of the sources I used...
; https://en.wikipedia.org/wiki/Church_encoding
; http://www.jetcafe.org/jim/lambda.html
;
; Don't be surprised if I get something wrong...

; LAMBDA CALCULUS
;
; A lambda expression may be one of...
; 	variable
; 	constant
; 	application
; 	abstraction
;
; An application is...
; 	(lambda-expression)lambda-expression
;
; An abstraction is...
; 	Lvariable.lambda-expression
;
; Lambda expressions are evaluated via Alpha reduction and Beta reduction.
;
; Alpha reduction:
; Lx.E -> Lz.{z/x}E for any z which is neither free nor bound in E
;
; Beta reduction
; (Lx.P)Q -> [Q/x]P

; LAMBDA CALCULUS TO SCHEME
;
; Lambda expression -> Scheme
; 	Lx.M -> (lambda (x) M)
; 	(M)N -> (M N)
;
; Some of the Lambda calculus notation below seems to use different conventions.
; (It came from a different source.)
; I haven't 100% figured out the conventions of the second one.

; CHURCH ENCODING - NUMERALS
;
; zero = Lf.Lx.x
(define zero (lambda (f) (lambda (x) x)))

; one = Lf.Lx.f x
;       Lf.Lx.(f)x
(define one (lambda (f) (lambda (x) (f x))))

; two = Lf.Lx.f(f x)
(define two (lambda (f) (lambda (x) (f (f x)))))

; succ(n) = n + 1 = plus(1) = Ln.Lf.Lx.f(n f x)
(define succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))

; plus = Lm.Ln.Lf.Lx. m f (n f x)
; (This one may have problems.)
(define plus (lambda (m)
               (lambda (n)
                 (lambda (f)
                   (lambda (x)
                     (m (f ((n f) x))))))))

; More arithmetic (TBD)
; mult = Lm.Ln.Lf. m (n f)
; exp = Lm.Ln. n m
; pred = Ln.Lf.Lx. n (Lg.Lh. h (g f)) (Lu. x) (Lu. u)
; sub = Lm.Ln. (n pred) m

; Scheme functions to convert scheme numbers <-> church numbers.
(define (number->church-old n)
  (if (= n 0)
      (lambda (f)
        (lambda (x)
          x))
      (lambda (f)
        (lambda (x)
          (f (((number->church-old (- n 1)) f) x))))))

; This version leverages the zero and succ we defined above.
(define (number->church n)
  (if (= n 0)
      zero
      (succ (number->church (- n 1)))))

(define (church->number c)
  ((c (lambda (x) (+ x 1))) 0))

; CHURCH ENCODING - BOOLEANS
;
; T = Lx.Ly.x
(define T (lambda (x) (lambda (y) x)))

; F = Lx.Ly.y
(define F (lambda (x) (lambda (y) y)))

; if-then-else = Lp.Lc.La.((p)c)a)
; (p = predicate, c = consequent, a = alternate)
(define if-then-else (lambda (p) (lambda (c) (lambda (a) ((p c) a)))))

; NOTE TO SELF
; In Scheme, you can't implement if as a function this way
; because Scheme predicates return #f or not-#f.
; The if-then-else function above requires predicates to return
; the T and F functions.

; Now back to Church numerals...
;
; zero? = Ln.n (Lx.F) T
(define zero? (lambda (n) ((n (lambda (x) F)) T)))

; Now for a test.
(display (((if-then-else (zero? zero)) 'yes) 'no))
(newline)
(display (((if-then-else (zero? two)) 'yes) 'no))
(newline)

; More Boolean operations (TBD)
; and = Lm.Ln. m n m
; or = Lm.Ln. m m n
; not = Lm.La.Lb. m b a = Lm. m (La.Lb. b) (La.Lb. a)

; CHURCH PAIRS (TBD)
; pair = Lx.Ly.Lz. z x y
; first = Lp. p (Lx.Ly.x)
; second = Lp. p (Lx.Ly.y)

; Pairs, of course, lead to lists.
; Church numerals could be used for characters.
; Lists of Church numerals could be used for strings.
; Pairs can also be used to extend Church numerals from natural numbers to
; ...integers
; ...ratios
; ...floating point
; ...complex
; (There was a good Stack Overflow on this, but I can't find it right now.)

; CURRYING (TBD)
; The Lambda calculus uses only unary functions.
;
; Instead of...
; 	(lambda (x y) ...)
; ...we use...
; 	(lambda (x) (lambda (y) ...)
; Instead of...
; 	(f x y)
; ...we use...
; 	((f x) y)
; 
; Currying can be used to simulate n-ary functions.
; An extension to Lambda expressions to represent n-ary functions:
;       Lx.Ly.x = Lxy.x

; The Y-combinator (TBD)
; The Lambda calculus doesn't have a way to name functions.
; The Y-combinator is a way to create recursion without naming.
; I've been using Scheme's define, so I don't really need the Y-combinator.


Output:
1
2
yes
no


Create a new paste based on this one


Comments:
posted by fisherro on Sep 2
Newer version here: http://codepad.org/l3iGPQJ0
reply