[CST-2] Strictness 99.8.7

[Phebe Mann]

For part 2

if f is S-jointly strict in argument position S, then a call to it fails
to terminate when applied to argument expression which fail to terminate
for a larger set of argument positions.

 |' = capital gamma symbol,
 --> (S) = an arrow with an S floating above it]
---> (S') =  an arrow with an S' floating above it]
(SUB rule)
   |' |- f : int^k  --> (S) int   if S' is a subset of S
-----------------------------
   |' |- f : int^k  --> (S') int
where S' is a subset of S

k = no. of parameters
S = set of parameters that are guarantees to loop

Phebe

On Fri, 1 Jun 2001, Raymond Chan wrote:

> 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/
>
>
>
>
> _______________________________________________
> CST-2 mailing list
> CST-2@srcf.ucam.org
> http://www.srcf.ucam.org/mailman/listinfo/cst-2
>