Hi Ed: > Thank you. but apart from the emptiness of the antecedent, the main > difff is that the formulation is simpler with |-> and mor eintuitive. > Correct? Yes, although the emptiness is important and the main reason to prefer "|->" over "##0". In fact, I would argue that using "##0" will be broken unless there is more case splitting to handle degenerate situations. For example, (1) 1[*0] |=> p is legal, and so is (2) 1 |-> 1[*0] |=> p (1) and (2) are equivalent in the unclocked neutral property semantics, which is defined for non-empty words. But (3) 1 ##0 1[*0] |=> p is not (currently) legal because the antecedent is degenerate. If we allow (3) to be legal, the unclocked semantics as it is currently written makes it a tautology. J.H. > Content-class: urn:content-classes:message > X-MimeOLE: Produced By Microsoft Exchange V6.5 > X-OriginalArrivalTime: 14 Aug 2007 16:49:32.0793 (UTC) FILETIME=[16D47690:01C7DE93] > Date: Tue, 14 Aug 2007 09:49:31 -0700 > X-MS-Has-Attach: > X-MS-TNEF-Correlator: > Thread-Topic: using |-> rather than ##0 > Thread-Index: AcfekgagxoTZSzNPRn6dmz/xXtCEjAAANlyQ > From: "Eduard Cerny" <Eduard.Cerny@synopsys.com> > Cc: <sv-ac@eda-stds.org> > > This is a multi-part message in MIME format. > > ------_=_NextPart_001_01C7DE93.1A879380 > Content-Type: text/plain; > charset="us-ascii" > Content-Transfer-Encoding: quoted-printable > > Hi John, > > Thank you. but apart from the emptiness of the antecedent, the main > difff is that the formulation is simpler with |-> and mor eintuitive. > Correct? > > best... > ed > > > > -----Original Message----- > > From: John Havlicek [mailto:john.havlicek@freescale.com]=20 > > Sent: Tuesday, August 14, 2007 12:42 PM > > To: eduard.cerny@synopsys.COM > > Cc: sv-ac@eda-stds.org > > Subject: using |-> rather than ##0 > >=20 > > Hi Ed: > >=20 > > You asked before about why the 1668 proposal for Annex F > > uses |-> rather than ##0. > >=20 > > I said that I don't think there is any difference, but=20 > > I was wrong and I actually thought about this before. > >=20 > > I think that |-> is preferable when combining with |=3D> > > because |=3D> does not require the antecedent to match=20 > > non-empty. Another point is that the associativity > > is counterintuitive with ##0. > >=20 > > I wrote some notes back in July using only the=20 > > unclocked semantics. I've copied them below. > >=20 > > J.H. > >=20 > > ------------------------------- > > 2007-07-06 > >=20 > > Q: What is the difference between=20 > >=20 > > 1 |-> r |-> p and 1 ##0 r |-> p > >=20 > > ? > >=20 > > Recall that neutral satisfaction is not defined for the empty word. > > Let |w| > 0. > >=20 > > w |=3D 1 |-> r |-> p > > iff w |=3D r |-> p > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and xy |=3D=3D r, yz = > |=3D p > >=20 > > w |=3D 1 ##0 r |-> p > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and xy |=3D=3D 1 ##0=20 > > r, yz |=3D p > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and xy |=3D=3D r, yz = > |=3D p > > iff w |=3D r |-> p > >=20 > >=20 > > ------------------------------- > > 2007-07-05 > >=20 > > Q: What is the difference between=20 > >=20 > > 1 |-> r |=3D> p and 1 ##0 r |=3D> p > >=20 > > ? > >=20 > > Using old semantics of |=3D> (unclocked) > > -------------------------------------- > >=20 > > Recall that neutral satisfaction is not defined for the empty word. > > Let |w| > 0. > >=20 > > w |=3D 1 |-> r |=3D> p > > iff w |=3D r |=3D> p > > iff w |=3D r ##1 1 |-> p > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and xy |=3D=3D r ##1=20 > > 1, yz |=3D p > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and x |=3D=3D r, yz = > |=3D p > > iff for all u,v s.t. w =3D uv and |v| > 0 and u |=3D=3D r, v |=3D p > >=20 > > w |=3D 1 ##0 r |=3D> p > > iff w |=3D (1 ##0 r) ##1 1 |-> p > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and xy |=3D=3D (1 ##0=20 > > r) ##1 1, yz |=3D p > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and x |=3D=3D (1 ##0=20 > > r), yz |=3D p > > iff for all u,v s.t. w =3D uv and |u| > 0 and |v| > 0 and u=20 > > |=3D=3D r, v |=3D p > >=20 > > Thus, for |w| > 0, the formulation > >=20 > > 1 |-> r |=3D> p > >=20 > > is preferable. > >=20 > >=20 > > Using new semantics of |=3D> (unclocked) > > -------------------------------------- > >=20 > > Recall that neutral satisfaction is not defined for the empty word. > > Let |w| > 0. > >=20 > > w |=3D 1 |-> r |=3D> p > > iff w |=3D r |=3D> p > > iff [new semantics of |=3D>] > > for all x,y s.t. w =3D xy and x |=3D=3D r, y |=3D p > >=20 > > There is something potentially ill-defined here, since we=20 > > have not required > > |y| > 0 when we make inductive reference to y |=3D p. > >=20 > > w |=3D 1 ##0 r |=3D> p > > iff [new semantics of |=3D>] > > for all x,y s.t. w =3D xy and x |=3D=3D 1 ##0 r, y |=3D p > > iff for all x,y s.t. w =3D xy and |x| > 0 and x |=3D=3D r, y |=3D p > >=20 > > Again, there is something potentially ill-defined here, since=20 > > we have not=20 > > required |y| > 0 when we make inductive reference to y |=3D p. > >=20 > > Thus, for |w| > 0, the formulation > >=20 > > 1 |-> r |=3D> p > >=20 > > is preferable. > >=20 > >=20 > > ------_=_NextPart_001_01C7DE93.1A879380 > Content-Type: text/html; > charset="us-ascii" > Content-Transfer-Encoding: quoted-printable > > <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN"> > <HTML> > <HEAD> > <META HTTP-EQUIV=3D"Content-Type" CONTENT=3D"text/html; = > charset=3Dus-ascii"> > <META NAME=3D"Generator" CONTENT=3D"MS Exchange Server version = > 6.5.7652.24"> > <TITLE>RE: using |-> rather than ##0</TITLE> > </HEAD> > <BODY> > <!-- Converted from text/plain format --> > > <P><FONT SIZE=3D2>Hi John,<BR> > <BR> > Thank you. but apart from the emptiness of the antecedent, the = > main<BR> > difff is that the formulation is simpler with |-> and mor = > eintuitive.<BR> > Correct?<BR> > <BR> > best...<BR> > ed<BR> > <BR> > <BR> > > -----Original Message-----<BR> > > From: John Havlicek [<A = > HREF=3D"mailto:john.havlicek@freescale.com">mailto:john.havlicek@freescal= > e.com</A>]<BR> > > Sent: Tuesday, August 14, 2007 12:42 PM<BR> > > To: eduard.cerny@synopsys.COM<BR> > > Cc: sv-ac@eda-stds.org<BR> > > Subject: using |-> rather than ##0<BR> > ><BR> > > Hi Ed:<BR> > ><BR> > > You asked before about why the 1668 proposal for Annex F<BR> > > uses |-> rather than ##0.<BR> > ><BR> > > I said that I don't think there is any difference, but<BR> > > I was wrong and I actually thought about this before.<BR> > ><BR> > > I think that |-> is preferable when combining with |=3D><BR> > > because |=3D> does not require the antecedent to match<BR> > > non-empty. Another point is that the associativity<BR> > > is counterintuitive with ##0.<BR> > ><BR> > > I wrote some notes back in July using only the<BR> > > unclocked semantics. I've copied them below.<BR> > ><BR> > > J.H.<BR> > ><BR> > > -------------------------------<BR> > > 2007-07-06<BR> > ><BR> > > Q: What is the difference between<BR> > ><BR> > > 1 |-> r |-> p and 1 ##0 r |-> = > p<BR> > ><BR> > > ?<BR> > ><BR> > > Recall that neutral satisfaction is not defined for the empty = > word.<BR> > > Let |w| > 0.<BR> > ><BR> > > w |=3D 1 |-> r |-> p<BR> > > iff w |=3D r |-> p<BR> > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and xy = > |=3D=3D r, yz |=3D p<BR> > ><BR> > > w |=3D 1 ##0 r |-> p<BR> > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and xy |=3D=3D = > 1 ##0<BR> > > r, yz |=3D p<BR> > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and xy = > |=3D=3D r, yz |=3D p<BR> > > iff w |=3D r |-> p<BR> > ><BR> > ><BR> > > -------------------------------<BR> > > 2007-07-05<BR> > ><BR> > > Q: What is the difference between<BR> > ><BR> > > 1 |-> r |=3D> p and 1 ##0 r |=3D> = > p<BR> > ><BR> > > ?<BR> > ><BR> > > Using old semantics of |=3D> (unclocked)<BR> > > --------------------------------------<BR> > ><BR> > > Recall that neutral satisfaction is not defined for the empty = > word.<BR> > > Let |w| > 0.<BR> > ><BR> > > w |=3D 1 |-> r |=3D> p<BR> > > iff w |=3D r |=3D> p<BR> > > iff w |=3D r ##1 1 |-> p<BR> > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and xy = > |=3D=3D r ##1<BR> > > 1, yz |=3D p<BR> > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and x = > |=3D=3D r, yz |=3D p<BR> > > iff for all u,v s.t. w =3D uv and |v| > 0 and u = > |=3D=3D r, v |=3D p<BR> > ><BR> > > w |=3D 1 ##0 r |=3D> p<BR> > > iff w |=3D (1 ##0 r) ##1 1 |-> p<BR> > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and xy |=3D=3D = > (1 ##0<BR> > > r) ##1 1, yz |=3D p<BR> > > iff for all x,y,z s.t. w =3D xyz and |y| =3D 1 and x |=3D=3D = > (1 ##0<BR> > > r), yz |=3D p<BR> > > iff for all u,v s.t. w =3D uv and |u| > 0 and |v| > 0 = > and u<BR> > > |=3D=3D r, v |=3D p<BR> > ><BR> > > Thus, for |w| > 0, the formulation<BR> > ><BR> > > 1 |-> r |=3D> p<BR> > ><BR> > > is preferable.<BR> > ><BR> > ><BR> > > Using new semantics of |=3D> (unclocked)<BR> > > --------------------------------------<BR> > ><BR> > > Recall that neutral satisfaction is not defined for the empty = > word.<BR> > > Let |w| > 0.<BR> > ><BR> > > w |=3D 1 |-> r |=3D> p<BR> > > iff w |=3D r |=3D> p<BR> > > iff [new semantics of |=3D>]<BR> > > for all x,y s.t. w =3D xy and x = > |=3D=3D r, y |=3D p<BR> > ><BR> > > There is something potentially ill-defined here, since we<BR> > > have not required<BR> > > |y| > 0 when we make inductive reference to y |=3D p.<BR> > ><BR> > > w |=3D 1 ##0 r |=3D> p<BR> > > iff [new semantics of |=3D>]<BR> > > for all x,y s.t. w =3D xy and x = > |=3D=3D 1 ##0 r, y |=3D p<BR> > > iff for all x,y s.t. w =3D xy and |x| > 0 and x |=3D=3D r, = > y |=3D p<BR> > ><BR> > > Again, there is something potentially ill-defined here, since<BR> > > we have not<BR> > > required |y| > 0 when we make inductive reference to y |=3D = > p.<BR> > ><BR> > > Thus, for |w| > 0, the formulation<BR> > ><BR> > > 1 |-> r |=3D> p<BR> > ><BR> > > is preferable.<BR> > ><BR> > ><BR> > </FONT> > </P> > > </BODY> > </HTML> > ------_=_NextPart_001_01C7DE93.1A879380-- -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Tue Aug 14 10:29:39 2007
This archive was generated by hypermail 2.1.8 : Tue Aug 14 2007 - 10:29:51 PDT