CSE526: Principles of Programming Languages
			     Scott Stoller
      hw5 solution: shared-variable concurrency, lambda calculus
			 version: 9pm,16mar2004

problem 1.

introduce a new command CU2 to help represent the intermediate
configuration between the two atomic steps of CU.

<comm> ::= CU2(<var>,<var>,<intcfm>,<var>)

the evaluation rules are as follows.


----------------------------------------------------- where i = [[e]] sigma 
<CU(x,x0,e,flag), sigma> => <CU2(x,x0,i,flag), sigma>


----------------------------------------------------- if sigma x = sigma x0
<CU2(x,x0,i,flag), sigma> => [sigma | x:i | flag:1]


----------------------------------------------------- if sigma x != sigma x0
<CU2(x,x0,i,flag), sigma> => [sigma | flag:0]


problem 2.
Exercise 10.1, 2nd expression.

(a) normal-order reduction sequence

(\d.d d) (\f.\x.f (f x))
(\f.\x.f (f x)) (\f.\x.f (f x))
\x.(\f.\x.f (f x)) ((\f.\x.f (f x)) x)
\x.\x1.(\f.\x.f (f x)) x ((\f.\x.f (f x)) x x1)
\x.\x1.(\x2.x (x x2)) ((\f.\x.f (f x)) x x1)
\x.\x1.x (x ((\f.\x.f (f x)) x x1))
\x.\x1.x (x ((\x5.x (x x5)) x1))
\x.\x1.x (x (x (x x1)))
\x.\x1.x (x (x (x x1)))

(b) it would stop after the third line in part (a).

(e) proof using eager evaluation rules.
Abbreviations:
F  = (\f.\x.f (f x))
D  = (\d.d d)
CF = Evaluation Rule: Canonical Form
BR = Evaluation Rule: beta_E reduction
=> = =>_E

                    ------CF  ------CF  ---------------------------CF
                    F => F    F => F    (\x.F (F x)) => (\x.F (F x))
------CF  ------CF  ------------------------------------------------BR
D => D    F => F    F F => (\x.F (F x))
--------------------------------------------------------------------BR
D F => (\x.F (F x))

You could also use the proof format in the book.
For small proofs, I find the notation used here easier to read.