[sv-ac] using |-> rather than ##0

Hi Ed:

You asked before about why the 1668 proposal for Annex F
uses |-> rather than ##0.

I said that I don't think there is any difference, but 
I was wrong and I actually thought about this before.

I think that |-> is preferable when combining with |=>
because |=> does not require the antecedent to match 
non-empty.  Another point is that the associativity
is counterintuitive with ##0.

I wrote some notes back in July using only the 
unclocked semantics.  I've copied them below.

J.H.

-------------------------------
2007-07-06

Q:  What is the difference between 

  1 |-> r |-> p  and  1 ##0 r |-> p

?

Recall that neutral satisfaction is not defined for the empty word.
Let |w| > 0.

w |= 1 |-> r |-> p
iff  w |= r |-> p
iff  for all x,y,z s.t. w = xyz and |y| = 1 and  xy |== r, yz |= p

w |= 1 ##0 r |-> p
iff  for all x,y,z s.t. w = xyz and |y| = 1 and xy |== 1 ##0 r, yz |= p
iff  for all x,y,z s.t. w = xyz and |y| = 1 and  xy |== r, yz |= p
iff  w |= r |-> p


-------------------------------
2007-07-05

Q:  What is the difference between 

  1 |-> r |=> p  and  1 ##0 r |=> p

?

Using old semantics of |=> (unclocked)
--------------------------------------

Recall that neutral satisfaction is not defined for the empty word.
Let |w| > 0.

w |= 1 |-> r |=> p
iff  w |= r |=> p
iff  w |= r ##1 1 |-> p
iff  for all x,y,z s.t. w = xyz and |y| = 1 and  xy |== r ##1 1, yz |= p
iff  for all x,y,z s.t. w = xyz and |y| = 1 and  x |== r, yz |= p
iff  for all u,v s.t. w = uv and |v| > 0 and  u |== r, v |= p

w |= 1 ##0 r |=> p
iff  w |= (1 ##0 r) ##1 1 |-> p
iff  for all x,y,z s.t. w = xyz and |y| = 1 and xy |== (1 ##0 r) ##1 1, yz |= p
iff  for all x,y,z s.t. w = xyz and |y| = 1 and x |== (1 ##0 r), yz |= p
iff  for all u,v s.t. w = uv and |u| > 0 and |v| > 0 and  u |== r, v |= p

Thus, for |w| > 0, the formulation

   1 |-> r |=> p

is preferable.


Using new semantics of |=> (unclocked)
--------------------------------------

Recall that neutral satisfaction is not defined for the empty word.
Let |w| > 0.

w |= 1 |-> r |=> p
iff  w |= r |=> p
iff  [new semantics of |=>]
     for all x,y s.t. w = xy and x |== r, y |= p

There is something potentially ill-defined here, since we have not required
|y| > 0 when we make inductive reference to y |= p.

w |= 1 ##0 r |=> p
iff  [new semantics of |=>]
     for all x,y s.t. w = xy and x |== 1 ##0 r, y |= p
iff  for all x,y s.t. w = xy and |x| > 0 and x |== r, y |= p

Again, there is something potentially ill-defined here, since we have not 
required |y| > 0 when we make inductive reference to y |= p.

Thus, for |w| > 0, the formulation

   1 |-> r |=> p

is preferable.


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.