Submission instructions:

Submit a single text file.

---------------------------------------


1. With regard to our discussion of denotational semantics,
prove the following:

LUB( F^n(_|_)) is the least fixed point of F.


---------------------------------------

2. We have discussed that, in the context of denotational semantics,
basically all normal functional language constructs yield and preserve 
monotonocitiy and continuity.

On the other hand, we can write Haskell functions like

f :: Float -> Float
f x = if x <= 1 then 1 else 0

which are neither monotonic nor continuous.

Resolve this apparent contradiction!

---------------------------------------

3. In your last handin, you have used

fix f = f (fix f)

to create an appropriate environment. It is unsatisfactory that this definition
does not mirror what is going on in the denotational semantics. We cannot mirror
the fixed point construction exactly, but we can approximate it.

To this end, create a new fixed point operator

newfix :: Int -> (a -> a) -> a

such that "newfix n f" corresponds to f^n(_|_). Use Haskell's "undefined" value
to represent _|_.

The test case

ds_prog exampletest (newfix 4 (ds_fenv [example]))

should yield "*** Exception: Prelude.undefined"

whereas

ds_prog exampletest (newfix 5 (ds_fenv [example]))

should yield "Just 15".

If you have not solved the last handin, you can also test with
fac f n = if n == 0 then 1 else n * f (n-1)

Submit only your definition of "newfix" - it is not necessary to re-submit the whole code.


---------------------------------------

4. Consider the "if-then-else" language defined on slide 53 and 54 of the lecture notes.
Multi-step evaluation for this language is defined as on slide 75.

Prove the following theorems. Be very precise about the form of induction principle you are using.
a) If t -> t' and t -> t'', then t' = t''
b) If t ->* u and t ->* u', where u and u' are both normal forms, then u = u'.

Now consider an extended version of this language with the
following additional evaluation rule:

                 t3 -> t3'
-----------------------------------------------
if t1 then t2 else t3 -> if t1 then t2 else t3'

Now prove, or refute with an example, the theorems above for this extended language:
c) In the extended language, if t -> t' and t -> t'', then t' = t''
d) In the extended language, if t ->* v and t ->* v', where v and v' are both values, then v = v'.
Hint: This is much harder than a) and b