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

From: Christian De Sainte Marie <csma@fr.ibm.com>
Date: Wed, 27 May 2009 13:45:21 +0200
To: Gary Hallmark <gary.hallmark@gmail.com>
Cc: RIF WG <public-rif-wg@w3.org>
```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.

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
```
Received on Wednesday, 27 May 2009 11:47:54 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:47:56 UTC