Fall 99, CSE 520: Solution of Assignment 2
Exercise 1
val composition = fn f => fn g => fn x => g(f x);
Exercise 2
val twice = fn f => composition f f;
Exercise 3
(twice twice f) and (twice (twice f)) are equivalent. In fact:
(twice twice f) = ((twice twice) f) by parentheses convention
= ((composition twice twice) f) by definition of twice
= (composition twice twice f) by parentheses convention
= (twice (twice f)) by definition of composition
Note that this equivalence is just accidental. In general, (f g h) is not
equivalent to (f (g h)).
Exercise 4
- -> is not confluent. In fact, consider the lambda term P =def= (\x. x x)((\y. y)R)
for some lambda term R.
We have that P -> M =def=(\x. x x)R and P -> N =def=((\y. y)R)((\y. y)R), but there is
no common term Q to which both M and N reduce in one step. In fact, M can only reduce to Q =def= R R,
while N can reduce to Q only in two steps.
- -> is weakly confluent; it is an obvious consequence of the confluence of ->>.
We can also give a direct proof of this fact. Assume P -> M and P -> N. Then
P must contain two different lambda redexes P1 and P2.
If P1 and P2 are disjoint, then the conclusion is obvious.
Otherwise, assume that P1 is of the form P1=def= (\x. R1)S1.
If P2 is inside S1, then observe that R1[S1/x] ->>
R1[S'1/x] for some term S'1 such that S1 ->> S'1.
If P2 is inside R1, then observe that R1[S1/x] ->>
R'1[S1/x] for some term R'1 such that R1 ->> R'1.
Exercise 5
- The answer is yes. The proof can be done by induction on the number m of steps in P ->> M and
on the number n of steps
in P ->> N. We will prove that there exists Q such that M ->> Q in n steps and N ->> Q in m steps.
- Base case, m = 0. In this case P is the same as M (modulo alpha-conversion). Then define Q as N.
- Inductive case. Assume P ->> M in m+1 steps and P ->> N in n steps. Let R be such that
P ->> R in m steps and R -> M.
By inductive hypothesis, there exists S such that R ->> S in n steps
and N ->> S in m steps. It can be easily proved (by induction on n and confluence of ->)
that there exists T such that S -> T and M ->> T in n steps.
Since we then have that N ->> T in m+1 steps, we can conclude.
Note that it is quite intuitive that the conflence of -> implies the confluence of ->>.
The following diagrams illustrates the situation for n=2 and m=3 (o stands for an arbitrary term):
P -> o -> o -> M
| .
V .
o .
| .
V .
N .............? Yes:
P -> o -> o -> M
| | | |
V V V V
o -> o -> o -> o
| | | |
V V V V
N -> o -> o -> Q
- The answer is no. For example, assume that the relation -> is defined in such a way that,
for every P, M, and N such
that P -> M and P -> N, there exists only one Q such that M ->> Q and N ->> Q, and
both M ->> Q and N ->> Q take two steps.
Then we can never "complete" a diagram like the one above.
The following diagram illustrate the situation in the case in which P ->> N in one step
and P ->> M in two steps (say, P -> R -> M). Even in this simple case we cannot close the diagram.
In fact, we can find an element T such that N ->> T in two steps and R ->> T in two steps, but
now we are left with the problem of closing the diagram relative to R. Since R ->> M in one step and
R ->> T in two steps, the problem has the same complexity as the initial one;
i.e. we are not getting any closer to the solution (we are assuming, of course, that A has enough elements to
provide always new T's).
P -----> R ----> M
| .
| .
| .
V .
N ...............? No:
P -----> R ----> M
| | .
| V .
| | .
V V .
N -->--> T ......?
Exercise 6
- Weakly normalizing. In fact, by reducing [is_zero] [0] and then [if_then_else] we get
[if_then_else]([is_zero] [0]) [1] Omega -> [if_then_else] [true] [1] Omega -> [1] (normal form)
but also, by reducing Omega, we get
[if_then_else]([is_zero] [0]) [1] Omega -> [if_then_else] ([is_zero] [0]) [1] Omega -> ...
- Not normalizing. In fact, the only "evolving" reductions (i.e. reductions to
a different term) bring to Omega (\y.[false]) [true] [0] [1]:
[if_then_else]([is_zero] Omega) [0] [1] -> ([is_zero] Omega) [0] [1]
-> Omega ([true][false]) [true] [0] [1]
-> Omega (\y.[false]) [true] [0] [1]
but then we have that Omega (\y.[false]) [true] [0] [1] can only reduce to itself:
Omega (\y.[false]) [true] [0] [1] -> Omega (\y.[false]) [true] [0] [1] -> ...
- Weakly normalizing. In fact, let us denote by G the term (\x.F(xx))(\x.F(xx)).
Note that Y F -> G -> F G -> F(F G) ->... . We have:
Y F [3] ->> [if_then_else] ([is_zero] [3]) [1] ([times] [3] (G ([predecessor] [3])))
->> [times] [3] (G [2])
->> [times] [3] (F G [2])
->> [times] [3] ([if_then_else] ([is_zero] [2]) [1] ([times] [2] (G ([predecessor] [2]))))
->> ...
->> [times] [3] ([times] [2] ([times] [1] ([if_then_else] ([is_zero] [0]) [1] ([times] [0] (G ([predecessor] [0]))))))
->> [times] [3] ([times] [2] ([times] [1] [1]))
->> [6] (normal form)
but also
Y F [3] -> F G [3] -> F(F G) [3] -> ...
Note that we cannot replace G by Y F in the above formulas. In fact, although we have Y F = F(Y F) = F(F(Y F)) = ...,
it is not true that Y F ->> F(Y F).
This last exercise illustrates the fact that, even in eager langauges like ML, the if_then_else operator must have a lazy
semantics, otherwise recursive definition cannot be given.
Exercise 7
Of course not, for instance we have
[true] Omega [0] -> Omega -> Omega ...
In this derivation, the first step is not monotonic.
A more interesting example is the following, were every other step is not monotonic.
The symbol I represents the lambda term \y.y (identity).
(\x. I x x)(\x. I x x) -> I (\x. I x x)(\x. I x x)
-> (\x. I x x)(\x. I x x)
-> I (\x. I x x)(\x. I x x)
-> (\x. I x x)(\x. I x x)
-> ...