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

Gary,


Gary Hallmark wrote on 27/05/2009 00:54:17:
> 
> It just takes a counterexample to "prove" this, and here is one, I 
think:
> 
> consider the condition 1=1.  By the model theory, this condition is
> satisfied in every fact base. However, by the matching substitution
> semantics, this condition is satisfied only in fact bases that
> explicitly contain 1=1 as an atomic formula. Now, the equality
> relation is infinite but a fact base is finite, therefore no fact base
> can contain the entire equality relation.

You are absolutely right.

Of course, nothing actually says, in the specification, that the number of 
facts must be finite (that's one of the reasons why I am slightly 
uncomfortable with calling it an "operational" semantics); but it is a 
reasonable expectation.

Btw, I removed all references to pattern matching wrt the semantics of 
condition formulas, and replaced them with ref to matching substitution: 
while the notion of pattern matching is familiar to the PR crowd, its 
usage in the context was confusing, since that part of the spec does not 
imply pattern matching.

The funny thing is that I had been thinking about adding an explicit 
definition of fact, to clarify the spec, and I was wondering whether 
membership and subclass should be defined as facts, or as part of a 
background theory, along with equality... And still, I forgot to take care 
of equality when I corrected the definition of matching substitution to 
take externals into account!

Anyway, I corrected the definition of "matching substitution" as follows:

σ matches ψ to Φ iff one of the following is true:
* ψ is an atomic formula and
** either σ(ψ) ∈ Φ;
** or &psi; is an equality formula, <tt>t1 = t2</tt>, and the ground terms 
&sigma;(t1) and &sigma;(t2) are equal;
** or &psi; is an external ...
* ...

I wonder if we better leave it at that, or if we need to say something 
about &sigma;(t1) and &sigma;(t2) being equal according to some background 
theory, and that any background theory must include, at least, the 
equality theory of all the supported data types (but, then, don't we need, 
also, to add also the case where &psi; is true in the background theory? 
And, then, we can remove the specific condition about equality)?

Cheers,

Christian

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