Re: (PRD) Safeness and the semantics of conditions (Was: Re: [PRD] proof that model theory of conditions != matching substitution semantics)

On Thu, May 28, 2009 at 6:30 AM, Christian De Sainte Marie
<csma@fr.ibm.com> wrote:
>
> Gary, all,
>
> (This is only about the safety/safeness part of your email. I reply to the
> part about the semantics of conditions in another message.)
>
> Gary Hallmark <gary.hallmark@gmail.com> wrote on 27/05/2009 21:26:51:
>>
>> 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).
>
> I do not understand why safeness is part of the semantics of conditions?

I don't know how to specify pattern matching operationally unless the
rules are safe.
E.g., the transition system I outlined would not terminate when trying
to evaluate the condition of a rule like
"if P(?x-1) then P(?x)"
>
> What we want to guarantee, is that all the variables that are used in the
> actions part are bound in the condition part (except for the action
> variables, of course). We need that because is is an assumption that is made
> in the semantics of rules and rule sets.
>
> If so, it is a condition on the well-formedness of a rule that Var(A) is a
> subset of VarB(C), where Var(A) are the free variables in the the action
> block and VarB(C) are the variables that must be bound to establish the
> truth value of the conjunction of all the binding patterns and the condition
> of the rule (something like the "restricted variables" in [1]).
>
> Did I miss something?

No, this is also part of safeness.
>
> Then, there is the (different) constraint, that we want the evaluation of
> conditions to be implementable with pattern matching; that is, we want to
> guarantee that it does not require constraint solving.
>
> This implies restrictions on the condition formulas, of course, like
> P(f(?x)), where P is a predicate symbol and f is the symbol of an external
> function, is allowed only if ?x can be bound otherwise, e.g. if P(f(?x)) is
> in a conjunction with Q(?x), where Q is a predicate symbol, and, thus, ?x
> can be bound by matching Q(?x) to a fact (if we have only P(f(?x)) and a
> fact P(a), we need to solve the constraint f(?x) = a, to bind ?x).
>
> But, again, these are not related to the semantics of condition, but to
> implementations:

I would say it is related to the style of semantics. If the semantics
are logic-based, then safeness must be defined logically, as Jos has
done for Core. If the semantics are operational (kind of an abstract
implementation), then safeness gets combined with the pattern matching
semantics (or abstract algorithm).

we do not want that RIF-PRD conformance requires producers
> and consumers to support constraint solving (in the above sense).
>
> If so, these restrictions belong to the conformance clause, not the
> semantics of conditions, or even of rules (in principle, at least: it may be
> easier to specify them along with the well-formedness condition on variables
> in the action part being bound in the condition).
>
> Again, did I miss something?
>
> Could somebody clarify this issues for me, please?

The only issue I raise is should PRD have an operational specification
of pattern matching that is equivalent to the model-theoretic
semantics of conditions on safe rules? This would serve 2 purposes:
1. implementors may be able to "see" from the operational spec the
pattern matching algorithm used by their rule engine, and thus
understand how to implement a translator
2. we may benefit from "proving" the equivalence of logically defined
safeness and operationally defined safeness -- after all, the current
defn of safeness was motivated by operational concerns of existing PR
engines. To know if we got it right, it would be good to have an
abstract model of these operational concerns.

This is certainly not an obstacle for Last Call. It would only be a
different and alternative way to specify what should be the same
semantics we have.

-- 
Cheers,

Gary Hallmark

Received on Thursday, 28 May 2009 23:19:23 UTC