Notes Week 3 - Michael Elhadad

*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.

<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.

;; 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)))))))

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