<exp> ::= <symbol> varref (var)
| (if <exp> <exp> <exp>) if-exp (test-exp then-exp else-exp)
| (lambda ({<var>}*) <exp>) lambda-exp (formals body)
| (<exp> {<exp>}*) app-exp (rator rands)
Stack ADT
Terms
Substitution
Unification
Reduce-once for the multi-parameters lambda calculus
Reduce-all
empty-stack, push, pop, top and
empty-stack?. Write a specification for these operations in the
style of the finite-function example. Which operations are constructors and
which are accessors?
Implement the stack data type using an abstract syntax tree representation.
This is an example of an Abstract Data Type (ADT) with several accessors.
In the procedural representation for such ADTs, one must design one procedure
for each accessor.
(define-datatype term term? (var-term (id symbol?)) (constant-term (datum constant?)) (app-term (terms (list-of term?))))We represent a term using symbols for variables and lists for
app
terms, while treating everything else as a constant. Thus the term:
("append" ("cons" w x) y ("cons" w z))
represents an abstract syntax tree that can be built by:
(app-term
(list
(constant-term "append")
(app-term
(list
(constant-term "cons") (var-term 'w) (var-term 'x)))
(var-term 'y)
(app-term
(list
(constant-term "cons") (var-term 'w) (var-term 'z)))))
Implement parse-term, unparse-term and
all-ids for this term language. all-ids
finds all the variables in a term.
subst-in-term that takes a term and
a substitution and walks through the term replacing each variable with its
association in the substitution.
Finally, implement a procedure subst-in-terms that takes a list
of terms as parameter.
;; Sample applications
(unparse-term
(subst-in-term
(parse-term '("append" ("cons" w x) y ("cons" w z)))
(extend-subst 'w (parse-term '("cons" a b))
(extend-subst 'y (parse-term '("cons" b c))
(empty-subst)))))
-->
("append" ("cons" ("cons" a b) x) ("cons" b c) ("cons" ("cons" a b) z))
(unparse-term
(subst-in-term
(parse-term '("cons" w x))
(extend-subst 'w (parse-term '("cons" a b))
(extend-subst 'a (parse-term '("cons" b c))
(empty-subst)))))
-->
("cons" ("cons" a b) x)
(subst-in-term t s) and
(subst-in-term u s) are equal?
We say that such an s unifies t and u.
There may be many such unifiers, but there will always be one that is the
most general.
The code below shows part of an algorithm to find the most general
unifying substitution. If no such unifier exists, it returns #f.
(define unify-term
(lambda (t u)
(cases term t
(var-term (tid)
(if (or (var-term? u) (not (memv tid (all-ids u))))
(unit-subst tid u)
#f))
(else
(cases term u
(var-term (uid) (unify-term u t))
(constant-term (udatum)
(cases term t
(constant-term (tdatum)
(if (equal? tdatum udatum) (empty-subst) #f))
(else #f)))
(app-term (us)
(cases term t
(app-term (ts) (unify-terms ts us))
(else #f))))))))
(define unify-terms
(lambda (ts us)
(cond
((and (null? ts) (null? us)) (empty-subst))
((or (null? ts) (null? us)) #f)
(else
(let ((subst-car (unify-term (car ts) (car us))))
(if (not subst-car)
#f
(let ((new-ts (subst-in-terms (cdr ts) subst-car))
(new-us (subst-in-terms (cdr us) subst-car)))
(let ((subst-cdr (unify-terms new-ts new-us)))
(if (not subst-cdr)
#f
(compose-substs subst-car subst-cdr))))))))))
Complete the algorithm by extending the substitution interface with the two
procedures unit-subst and compose-substs. The
application (unit-subst i t) returns a substitution that
replaces symbol i with term t and replaces any other symbol
by its trivial association.
The application (compose-substs s1 s2) returns a substitution
s3 such that for any term t, (subst-in-term t s3)
returns the same term as (subst-in-term (subst-in-term t s1) s2).
The memv test in unify-term is called the
occurs check. Create an example to illustrate that this test
is necessary.
;; For the one-parameter syntax of lambda calculus
(define (answer? exp) (not (app? exp)))
(define (reduce-once e success fail)
(cases exp e
(varref (var) (fail))
(lambda (formal body) (fail))
(app (rator rand)
(if (and (lambda? rator) (answer? rand))
(success (beta-reduce exp))
(reduce-once rator
(lambda (reduced-rator)
(succeed (make-app reduced-rator rand)))
(lambda ()
(reduce-once rand
(lambda (reduced-rand)
(succeed (make-app rator reduced-rand)))
fail)))))))
This function receives a parsed expression and two continuations.
If the expression e can be reduced by beta-reduction, the function passes
the reduced parsed expression to the success continuation.
If more than one beta-redex node exists in the expression, this function
will select the first applicable one according to the applicative order
strategy.
If the expression e does not contain any beta-redex node,
then the fail continuation is invoked with no parameters.
Extend this function to work over the multi-parameter lambda-calculus
according to the syntax provided above. Your function will determine
the order of evaluation of arguments provided to a lambda function -
in such a way that arguments are evaluated left to right.
;; Sample invocation
(reduce-once (parse '((lambda (x y) (x y))
((lambda (x) x) a)
((lambda (z) y) b)))
(lambda (reduced-exp) (pretty-print (unparse reduced-exp)))
(lambda () "expression cannot be reduced"))
reduce-once from the previous question to
implement the function reduce-all. reduce-all keeps
applying reductions to its parameter (an unparsed expression) until no more
reduction can be found. If it returns (that is, if no infinite loop is hit),
it returns the unparsed reduced expression.
;; Sample invocation
(reduce-all '((lambda (x y) (x y))
((lambda (x) x) a)
((lambda (z) y) b)))