Re: [PRD] proof that model theory of conditions != matching substitution semantics

Gary,

Gary Hallmark <gary.hallmark@gmail.com> wrote on 27/05/2009 21:26:51:
> 
> I question why we want the matching substitution semantics to be the
> same as the model theory. It is equally declarative and logical, it
> just uses different symbols.

My recollection is that we decided to replace the operational definition 
of rule instantiation, that we had in the FPWD [1], by a model theoretic 
semantics of conditions to make PRD as close as possible to BLD: since the 
semantics of conditions in BLD and PRD are essentially the same, it was 
decided that Adrian would adapt the semantics of BLD conditions to PRD 
condition. The benefits were, also, that it simplified the combination 
with DTB and SWC.

The part about matching substitutions was added to make the link with the 
operational semantics of rules and rule sets. It was improved, recently, 
to make that link more obvious, and we ended up with two almost equivalent 
definitions of the semantics of conditions. But they were only almost 
equivalent, and, thus, they were both required. The "mapping substitution" 
version of the semantics was extended to make it fully equivalent, so that 
people with a pattern matching culture would not be required to read and 
understand the model-theoretic part.

I think that it is valuable to keep the equivalence, because it gives an 
immediate link to Core, and, further, BLD. And it permits the reader to 
choose the style of semantics with which it he most familiar.

We have to debug the "substitution semantics", of course. But I understand 
that bugs are allowed in LC drafts :-)

> I think it would be more useful to specify an alternative semantics
> for conditions that is operational. [...]

I fear that such a change would require more time and effort than we can 
afford before the LC publication.

One option could be to add an alternative, operational, semantics later, 
e.g. as an appendix?

Not sure if it is a good idea to start that kind of work, though. 
Especially now, with the reduced bandwidth and the priority on test cases.

> This would also be valuable for implementors, I think. Such an
> operational semantics would be a transition system where the states
> are [...]

If we decide that it is worth the effort, I would strongly suggest that we 
start from the state where we left the initial attempt at an operational 
semantics of rule instantiation, that is [1].

Cheers,

Christian

[1] 
http://www.w3.org/2005/rules/wg/draft/ED-rif-prd-20080728/#Rules_instantiation:_INSTANTIATE

ILOG, an IBM Company
9 rue de Verdun
94253 - Gentilly cedex - FRANCE
Tel. +33 1 49 08 35 00
Fax +33 1 49 08 35 10


Sauf indication contraire ci-dessus:/ Unless stated otherwise above:
Compagnie IBM France
Siège Social : Tour Descartes, 2, avenue Gambetta, La Défense 5, 92400 
Courbevoie
RCS Nanterre 552 118 465
Forme Sociale : S.A.S.
Capital Social : 609.751.783,30 ?
SIREN/SIRET : 552 118 465 02430