[CST-2] Strictness 99.8.7

[Raymond Chan]

Erm...Phebe, you've contradicted yourself (probably due to a typo), first
time you had S on top and S' below, and second time you had S' on top and S
below, but both times gave the condition S' is a subset of S; as far as I
can see, your second solution says a similar thing to mine but more
specifically.
Mond
----- Original Message -----
From: "Phebe Mann" <pm258@hermes.cam.ac.uk>
To: <cst-2@srcf.ucam.org>
Sent: Friday, June 01, 2001 5:28 PM
Subject: Re: [CST-2] Strictness 99.8.7


>
> Moritz
>
>  |' = 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
> -----------------------------
>    |' |- f : int^k  --> (S) int
> where S' is a subset of S
>
> k = no. of parameter
> S = set of parameters that are guaranteed to loop
>
> Phebe
>
> On Fri, 1 Jun 2001, M.Y.W.Y. Becker wrote:
>
> >
> >
> > --On 01 June 2001 17:03 +0100 Phebe Mann <pm258@hermes.cam.ac.uk> wrote:
> > [...]
> > > (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
> > [...]
> >
> > That's wrong. Raymond's answer was already 100% correct (I believe).
> >
> > Mo
> >
> >
> > _______________________________________________
> > CST-2 mailing list
> > CST-2@srcf.ucam.org
> > http://www.srcf.ucam.org/mailman/listinfo/cst-2
> >
>
>
>
> _______________________________________________
> CST-2 mailing list
> CST-2@srcf.ucam.org
> http://www.srcf.ucam.org/mailman/listinfo/cst-2
>