Advanced Methods in Programming Languages (201-2-4411-01)

### 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:

1. If E is the variable reference x, then: x[M/x] = M.
2. If E is a variable reference y different from x, then: y[M/x] = y.
3. If E is an application (F G) then: (F G)[M/x] = (F[M/x] G[M/x])
4. If E is an abstraction (lambda (y) E') there are several subcases:
1. If E=(lambda (x) E') then E[M/x] = (lambda (x) E')
2. If E=(lambda (y) E') and x does not occur free in E' then (lambda (y) E')[M/x] = (lambda (y) E')
3. 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])
4. 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
```