Re: B.1, B.2

Peter,

As Jim said last week, the chairs are willing to reopen 5.26 wrt. B1 & 
B2 if we can solve it beofre LC. It seems Jeremy has proposed wording 
for changing the document, and also offered two possibilities for 
handling work on the proof. Given this, could you agree to making this 
change? As I said during the telecon, in my view it was in the spirit of 
the editors meeting to see the proposal as one complete set, and it 
seems to me Jeremy has proposed a way to include B1/B2 without requiring 
you to spend much time on it.

Thanks for considering this,

Guus


Jeremy Carroll wrote:
> 
> 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
> 
> 
> 
> 

-- 
A. Th. Schreiber, SWI, University of Amsterdam,
http://www.swi.psy.uva.nl/usr/Schreiber/home.html

Received on Monday, 24 March 2003 11:13:42 UTC