From: Vassil Nikolov
Subject: Re: Problem in beta reduction
Date:
Message-ID: <snzbq1foesb.fsf@luna.vassil.nikolov.name>
On Tue, 1 Jul 2008 22:46:59 -0700 (PDT), suchi <··············@gmail.com> said:
| (define (reduce f)
| ((lambda (value) (if (equal? value f) f (reduce value)))
| (let r ((f f) (g ()))
| (cond ((not (pair? f))
| (if (null? g) f (if (eq? f (car g)) (cadr g) (r f (caddr g)))))
| ((and (pair? (car f)) (= 2 (length f)) (eq? 'lambda (caar f)))
| (r (caddar f) (list (cadar f) (r (cadr f) g) g)))
| ((and (not (null? g)) (= 3 (length f)) (eq? 'lambda (car f)))
| (cons 'lambda (r (cdr f) (list (cadr f) (delay (cadr f)) g))))
| (else (map (lambda (x) (r x g)) f))))))
| This piece of code is supposed to do beta and alpha reduction.
By the way... While Real Programmers do not even use `define', thou
shalt not take shortcuts through thy abstractions. Note that in the
version below, I have _not_ changed the algorithm, nor have I
checked it for correctness or fixed its bugs if any---that was not
the purpose of the exercise. (The abstractions are implemented in a
very plain vanilla way, and only to the extent they are immediately
needed. If I used one-letter variable names, I would have t and e
for term and environment, rather than f and g.)
(define (reduce term)
((lambda (result)
(if (term-equal? result term)
term
(reduce result)))
(let reduce-once ((term term) (env empty-environment))
(cond ((var? term)
;; look term up in env:
(cond ((empty? env) term)
((var-equal? term (first-binding-var env)) (first-binding-value env))
(else (reduce-once term (rest-bindings env)))))
((app? term)
(reduce-once (app-l-term term)
(bind (app-l-var term)
(reduce-once (app-arg term) env)
env)))
((and (l-abs? term)
(not (empty? env)))
(make-l-abs (reduce-once (l-var-term term)
(bind (l-var term)
(delay (l-var term))
env))))
(else (map (lambda (subterm) (reduce-once subterm env))
term))))))
where:
;; term ::= variable | lambda-abstraction | application
(define (term-equal? term1 term2) (equal? term1 term2))
;; variable ::= atom
(define (var? term) (not (pair? term)))
(define (var-equal? v1 v2) (eq? v1 v2))
;; lambda-abstraction ::= (LAMBDA variable term)
(define (l-abs? term) (and (pair? term) (= (length term) 3) (eq? (car term) 'lambda) (var? (cadr term))))
(define (make-l-abs var-term) (cons 'lambda var-term))
(define (l-var-term l-abs) (cdr l-abs))
(define (l-var l-abs) (cadr l-abs))
(define (l-term l-abs) (caddr l-abs))
;; application ::= (lambda-abstraction term)
(define (app? term) (and (pair? term) (l-abs? (car term)) (= (length term) 2)))
(define (app-l-abs app) (car app))
(define (app-l-var app) (l-var (app-l-abs app)))
(define (app-l-term app) (l-term (app-l-abs app)))
(define (app-arg app) (cadr app))
;; environment ::= () | (variable value environment)
(define empty-environment '())
(define (empty? env) (null? env))
(define (first-binding-var env) (car env))
(define (first-binding-value env) (cadr env))
(define (rest-bindings env) (caddr env))
(define (bind var value env) (list var value env))
---Vassil.
--
Peius melius est. ---Ricardus Gabriel.