RE: B.1, B.2

Minutes:
> > > JimH: Agrees with DanC. Suggests taking out B1/2 and close issue with
> > > proviso that could be re-opened if volunteer appears before last call.
> > >

Jeremy:
> > I suggest the following change is all that is necessary.
> >
> > in S&AS 4.1
> > [[
> > Bnode identifiers here must be taken as local to each
> transformation, i.e.,
> > different identifiers should be used for each invocation of a
> transformation
> > rule.
> > ]]
> >
> > ==>
> >
> > [[
> > Bnode identifiers here are local to each transformation.
> > When the construct being transformed matches the *restriction* or
> > *description*
> > productions from the abstract syntax then
> > the bnode may be shared between multiple identical transformations of
> > identical
> > *restriction*s or *description*s. Otherwise the bnode used in each
> > transformation
> > should be unique for each invocation of a transformation rule.
> > ]]
> >
> > ==

Peter:
> This does not include changes to the equivalence proof.

Agreed.
The proof is more difficult.

Two points:
- the proof is informative, and so by the earlier discussion, could be left
with a "to-do" until after last call. This seems to have been your
suggestion about the graph as triples - since I do not believe we have any
text that correctly describes the current graphs as triples.

- I think the easier (but perhaps not most attractive) fix, would be to
leave Lemma 1 and 2 unchanged except adding that the bnodes are not shared
between multiple identical transformations, and then relaxing that condition
in a new lemma (2.1?). This would then justify the merging of bnodes which
denote the same classes. A more attractive option, requiring more detailed
work, would be to inspect each use of the disjoint bnodes assumption in the
proof, and make necessary changes.

Jeremy

Received on Friday, 21 March 2003 08:34:32 UTC