[CST-2] Strictness 99.8.7

Raymond Chan rwlc3@cam.ac.uk
Fri, 1 Jun 2001 16:36:20 +0100


Anyone had a go at the OptComp question in 99.8.7?
The first bit is straighforward strictness bookwork, but then the second bit
is a weird combination of strictness and effect systems... does anyone agree
with me on the following answers for the second half of 99.8.7.... [for 10
marks I think I probably might need to say more?]

[I've used |' instead of that capital gamma symbol,
and --> (S) to mean an arrow with an S floating above it]
(SUB rule)
   |' |- f : t  -->(S') t'
-----------------------------
   |' |- f : t  -->(S) t'
where S' is a subset of S

assumptions |' 0 =
{ plus : int^2 --> {1} int, plus : int^2 --> {2} int,
  cond : int^3 --> {1} int, cond : int^3 --> {2,3} int }

Finally, "f is strict in its ith argument" if and only if S={i} in
|' |- f : t where t = int^k --> (S) int

Hope someone else has tried the question and has some idea of what's going
on....
Cheers,
Raymond :-)
--------------
Raymond Chan, St. John's College, Cambridge, CB2 1TP
http://freespace.virgin.net/kk.chan/raymond/