Re: [PRD] PRD TF telecon Tuesday 17 February

Christian de Sainte Marie wrote:
>
> I think that this bug can be corrected by modifying slightly the 
> definition of refraction, so that action variables be taken into 
> account iff  their initialisation template matches a ground condition 
> element (in the condition or in a binding pattern) that is not inside 
> an existential condition (in the current version of the spec, only 
> rule variables are taken into account for refraction).
>
I think it might be clearer to define a function Normalize(e) that maps 
a term or formula e to a term or formula as follows:

if e is a predicate p(a<sub>i</sub>) then Normalize(e) = 
And(p(v<sub>i</sub>) v<sub>i</sub> = a<sub>i</sub>), forall i where 
a<sub>i</sub> is a Const and v<sub>i</sub> is a new free variable

if e is a frame o[k<sub>i</sub> -> a<sub>i</sub>] then Normalize(e) = 
And(o[k<sub>i</sub> -> v<sub>i</sub>] v<sub>i</sub> = a<sub>i</sub>), 
forall i where a<sub>i</sub> is a Const and v<sub>i</sub> is a new free 
variable

if e is Exist, Const, or Var then Normalize(e) = e

otherwise, recursively normalize the constituents of e.

e.g. Normalize(_P(1, ?x)) = And(_P(?w, ?x) ?w = 1)

Then, refract on Var(Normalize(e))