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

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.

I think it would be more useful to specify an alternative semantics
for conditions that is operational. It would be equivalent to the
model theory combined with the Core safety restriction (extended to
PRD). This would also be valuable for implementors, I think. Such an
operational semantics would be a transition system where the states
are (sigma, phi) pairs, where sigma is a set of (v,k) pairs, where v
is a Var and k is a Const. Phi is a condition formula. There are also
2 special sigma values "true" and "false" that are used when a
tautology or contradiction is found during matching. Final states are
those where sigma has a pair for every Var in phi, or sigma is "true"
or "false". The transition relation Tmatch is (recursively) defined
as:
if phi is P(?x) or O[p->?x] then sigma' = and-combine((x,k),sigma),
where P(k) or O[p->k] is in the fact base
if phi is P(k) or O[p->k] and P(k) or O[p->k] are not in the fact
base, then sigma' = "false"
if phi is And(phi1...phiN) then sigma' = and-combine(sigma(Tmatch
(sigma,phi1))... sigma(Tmatch (sigma,phiN)))
if phi is Or(phi1...phiN) then sigma' = or-combine(sigma(Tmatch
(sigma,phi1))... sigma(Tmatch (sigma,phiN)))
if phi is k=?y or phi is ?x=?y and ?x is bound to k, then sigma' =
and-combine((y,k), sigma)
if phi is ?y=k or phi is ?y=?x and ?x is bound to k, then sigma' =
and-combine((y,k), sigma)
if phi is Not(phi1) let b = sigma(Tmatch(sigma,phi1)); if b = "true"
then sigma' = "false"; else if b = "false" then sigma' = "true"; else
sigma' = b
if phi is Exists ?x1..?xN (phi1) then phi' = phi1 (need to assume,
without loss of generality, that x1..xN are declared in no other
Exists or Forall in the containing condition formula)
if phi is an external predicate, all its inputs are bound, and its
value is false, then sigma' = "false".
if phi contains an external function f and all its arguments are bound
(every argument is either a Const or a Var in sigma), and if the
value of f with those arguments is k, then phi' is phi with k
substituted for f (and its arguments).

Or-combine is a helper function that returns "true" if any input is
"true", else returns the union of the (v,k) input pairs.
And-combine is a helper function that returns "false" if any input is
"false", else unions the (v,k) input pairs, and if (v1,k1) and (v1,k2)
are 2 such pairs, and k1!=k2, the result is the "false" sigma value,
else the result is the union.

Sigma is a helper function that simply selects sigma from the
transition system state.

The sigma in a final state contains the substitution for the rule
instance (or the constant truth value "false" if there is no
substitution or "true" if phi has negation and no substitution).



On Wed, May 27, 2009 at 4:45 AM, Christian De Sainte Marie
<csma@fr.ibm.com> wrote:
>
> 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:
>
> &sigma; matches &psi; to &Phi; iff one of the following is true:
> * &psi; is an atomic formula and
> ** either &sigma;(&psi;) &isin; &Phi;;
> ** 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
>
>



-- 
Cheers,

Gary Hallmark

Received on Wednesday, 27 May 2009 19:27:26 UTC