Advanced Methods in Programming Languages (201-2-4411-01)
Notes Week 3 - Michael Elhadad
Reduction Rules, Lambda Calculus
Definition
Our goal is to formalize the idea of the "substitution model" studied in
PPL. The objective is to inductively describe how the value of a Scheme
expression can be computed. To avoid getting into too much detail, we will
restrict our attention to a simple version of the Lambda Calculus.
A "reduction rule" expresses a semantic equivalence between two
expressions. We will describe computation as a rewriting process where an
expression is transformed by the application of primitive "computation
rules". This is an application of a model called operational
semantics.
Other approaches to the formal description of programming language
semantics exist. Among them:
- Denotational semantics: focuses on the effect of executing
a program and models this effect using mathematical functions (ie, a
program is represented as a function from state to state). The semantics
of a program is a function associating a set of initial states with
corresponding final states. This function is constructed
compositionally.
- Axiomatic semantics: is used to verify the partial correcteness
of a program, with respect to a set of pre and post-conditions. Each
computation step derives new post-conditions.
Beta Reduction
Consider the language with the following syntax:
<exp> ::= <varref>
| (lambda (<var>) <exp>)
| (<exp> <exp>)
We want to define the transformation that converts from:
((lambda (var) exp) rand)
to the equivalent expression when replacing references to var
by rand
. We need to worry about conflicts due to the
presence of free variables. For example:
((lambda (x)
(lambda (y) (x y)))
(y w))
It would be incorrect to derive:
(lambda (y) ((y w) y))
because we want the reference to y
in (y w)
to
remain free.
The following inductive definition provides the correct definition of the
substitution model: E[M/x] is read as "E with M instead of x". It is
computed inductively as follows:
- If E is the variable reference x, then: x[M/x] = M.
- If E is a variable reference y different from x, then: y[M/x] = y.
- If E is an application (F G) then: (F G)[M/x] = (F[M/x] G[M/x])
- If E is an abstraction (lambda (y) E') there are several subcases:
- If E=(lambda (x) E') then E[M/x] = (lambda (x) E')
- If E=(lambda (y) E') and x does not occur free in E' then
(lambda (y) E')[M/x] = (lambda (y) E')
- If E=(lambda (y) E') and y is different from x, and y does not
occur free in M then:
(lambda (y) E')[M/x] = (lambda (y) E'[M/x])
- If y is different from x, x occurs free in E' and y occurs free in
M, then:
(lambda (y) E')[M/x] = (lambda (z) (E'[z/y])[M/x])
where z does not occur free in E' or M.
Computation Strategies
A computation strategy determines in which order to apply primitive
computation steps. The strategy defines rules to identify within an
abstract syntax tree the first candidate node on which to apply a reduction
rule.
The following function defines the "Applicative-order strategy" used in
Scheme. With this strategy, no reduction is ever applied inside the body of
a lambda abstraction.
This function is an important example of a programming style known as
"continuation passing style" (CPS).
;; 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)))))))
Recursion in Lambda Calculus
This is a short note on the Y-operator.
There are no define and letrec primitives in the Lambda calculus that allow
us to attach a procedure to a name. How then can we define recursive
procedures in pure lambda calculus?
The following discussion just gives a flavor of the solution. Assume we
are looking for a way to define the factorial procedure. There is no way
to define the name "fact". The only way we can refer to a name is by
defining a binding for this name. So we define the following expression:
(lambda (fact)
(lambda (n)
(if (= n 0) 1 (* n (fact (- n 1))))))
Call this expression f. We are now looking for a way to define the value
fact such that (f fact) is equal to the factorial procedure.
This fact procedure, if it exists, can only depend on the form of the
expression f. We note this in functional terms as:
fact = (Y f)
If such an operator Y can be found, it then fulfils the following
condition:
(f (Y f)) = (Y f)
That is, Y is the operator that when applied to a function returns its
fixed point. Extraordinarily, such an operator can be defined in pure
lambda calculus and is completely general. Its value is:
Y = (lambda (f)
((lambda (x) (f (x x)))
(lambda (x) (f (x x)))))
When using applicative-order strategy, the following form must be used to
avoid divergence:
(define Y
(lambda (f)
((lambda (x) (f (lambda (y) ((x x) y))))
(lambda (x) (f (lambda (y) ((x x) y)))))))
You can verify in Scheme that:
(define fy
(Y (lambda (fact)
(lambda (n) (if (= n 0) 1 (* n (fact (- n 1))))))))
(fy 5) --> 120
Last modified Dec 27, 1998
Michael Elhadad