FW: [abc] found small mistake in the semantics

Oh, also forget to include the list... Here you go. (that was sent
yesterday already)

Eric

> -----Original Message-----
> From: Eric Bodden
> Sent: Saturday, October 07, 2006 1:03 PM
> To: 'julian.tibble@worcester.oxford.ac.uk'
> Subject: RE: [abc] found small mistake in the semantics
>
> Hi, Julian!
>
> > Sorry for not replying sooner; we had a visitor to the lab
yesterday.
>
> Oh don't worry. I am more than happy that somebody actually made the
> effort to step through the semantics. So thanks a lot!
>
> > conf = 3 -> false
> > 4 -> true
> >
> > e = { (A, {x -> a}), (B, {y -> a}) }
> >
> > and the edges are:
> >
> > 3 to 4 labelled A (doesn't really matter, since 3 is false)
> > 4 to 4 labelled skip-A
> > 4 to 4 labelled skip-B
>
> I tried to reproduce the "problem", but I was not quite able to. In my
> calculations, the following happens:
>
> I ignore the positive edge for now, as it should not contribute
> anything. So I basically first compute...
>
> \delta(\gamma,e,(4,skip-A,e))
>
> ... and then based on the result \gamma_r of this, I compute...
>
> \delta(\gamma_r,e,(4,skip-B,e))
>
> If I am not mistaken, the result of the first computation should be:
>
> \delta(\gamma,e,(4,skip-A,e)) =
>
> { 3 -> false, 4 -> { ({},{x->{a}}) } } =: \gamma_r
>
> This is because in the innermost definition of neg, we take the third
> case, where v=x is yet unbound. (Note that there still was a small
> typing error in that line of the paper: When we add a negative
binding,
> we have to add it to the *set* of negative bindings for that variable
-
> I have to correct this.)
>
> Then, on this configuration \gamma_r , we apply
> \delta(\gamma_r,e,(4,skip-B,e)):
>
> This leads to the computation of:
>
> neg(({},{x->{a}}), {y->a}, y) = ({},{x->{a},y->{a}})
>
> (again, 3rd case)
>
> which leads to a result of:
>
> { 3 -> false, 4 -> { ({},{x->{a},y->{a}}) } }
>
> ...which is what we expect, isn't it?
>
> Thanks in advance,
>
> Eric
Received on Sun Oct 08 17:29:51 2006