Alt AbstrAction

(this is essentially a copy of the corresponding sections in the current PRD draft, with the following proposed modifications:

• Addition of an Assert(object) action;
• The argument of New is the class of the created object;
• The syntax of the actiond block (Do) is modified to disambiguate the link between an action variable and its binding (as a cnosequnce of changing the arugment of New);
• The well-formedness conditions for an action block are amended accordingly.)

Abstract Syntax

For a production rule language to be able to interchange rules using RIF-PRD, its alphabet for expressing the action part of a rule must, at the abstract syntax level, consist of syntactic constructs to denote:

• the assertion of a positional atom, an atom with named arguments, or a frame or subclass atomic;
• the retraction of a positional atom, an atom with named arguments, or a frame;
• the creation of a new frame object;
• the removal of a frame object and the retraction of the corresponding frames and class membership atomics;
• the assertion of a frame object and of the corresponding class membership atomics;
• a sequence of these actions, including local variables and a mechanism to bind a local variable to a frame slot value or a new frame object.

Editor's Note: ... and/or others. We are especially interested in feedback about actions that cannot be decomposed into a sequence of the above.

For the sake of readability and simplicity, this specification introduces a non-normative notation for these constructs. That notation is not intended to be a concrete syntax and it leaves out many details that are not needed for its purpose. The only normative concrete syntax for RIF-PRD is the XML syntax.

Atomic actions

Atomic action constructs take constructs from the RIF-PRD condition language as their arguments.

Definition (Atomic action). An atomic action can have several different forms and is defined as follows:

1. Assert fact: If φ is a positional atom, an atom with named arguments, a frame or a subclass atomic in the RIF-PRD condition language, then Assert(φ) is an atomic action. φ is called the target of the action.
2. Retract fact: If φ is a positional atom, an atom with named arguments, or a frame in the RIF-PRD condition language, then Retract(φ) is an atomic action. φ is called the target of the action.
3. Retract object: If t is a term in the RIF-PRD condition language, then Retract(t) is an atomic action. t is called the target of the action;
4. Assert object: If t is a term in the RIF-PRD condition language, then Assert(t) is an atomic action. t is called the target of the action.

Editor's Note: In this WD, Assert(f) where f is a subclass atomic is allowed only in unconditional action blocks, that is, in facts, and the assertion of membership facts is allowed only in the context of an object creation and with respect to the created object. Whether and where the assertion of membership and subclass atomics should be allowed is still under discussion in the WG.

Action blocks

The construct that is used in RIF-PRD to serialize the action part of rules is the action block. RIF-PRD provides for the representation of local variables that are declared inside an action block (action variables) and of their binding value, if the binding value can be represented by a RIF-PRD frame slot value or if the binding is to a newly created frame object.

Definition (Object creation). If t is a term in the RIF-PRD condition language, then New(t) denotes the creation of a new object in the class denoted by t. t is called the target class or, simply, the target.

Definition (Action block). An action block is consists of the optional declaration and binding of action variables, and of a sequence of atomic actions: If (v₁ p₁), ..., (v_n p_n), n ≥ 0, are pairs of made of a variable, v_i, (called action variable) and a frame atomic or a object creation, p_i (called action variable binding, or, simply, binding), and if a₁, ..., a_m, m ≥ 1, are atomic actions, then
Do((v₁ p₁), ..., (v_n p_n) a₁ ... a_l) denotes an action block. The pair, (v_i p_i), of an action variable and its binding is called an action variable declaration.

Well-formed actions and action blocks

Definition (Well-formed atomic action). An atomic action is well-formed is and only if one of the following is true:

• it is an Assert and its target is a well-formed term or atomic;
• it is a Retract and its target is a well-formed term or atomic.

Definition (Well-formed object creation). an object creation construct is well-formed if and only if its target class is a well-formed term.

The function Var(f), that has been defined for condition formulae, is extended to actions and object creations as follows:

• if f is an atomic action with target t, then Var(f) = Var(t);
• if f is an object creation construct with target t, then Var(f) - Var(t).

Definition (Well-formed action block). An action block is well-formed if and only if all of the following is true:

• all the action variable declarations, if any, are well-formed, that is, for each action variable declaration, (v p), the action variable binding, p, is a well-formed frame or a well-formed object creation and one of the following is true:
  1. the binding, p, is an object creation and v ∉ Var(p);
  2. the binding is a frame, p = o[a₁->t₁...a_n->t_n], n ≥ 1, and v ∉ Var(o) ∪ Var(a₁) ∪ ... ∪ Var(a_n) and v ∈ {t₁ ... t_n};
• if b₁ = (v₁ p₁) and b₂ = ({v₂ p₂) are two action variable declarations in the action block, then either v₁ ∉Var(p₂) or v₂ ∉Var(p₁);
• all the actions in the action block are well-formed atomic actions;
• if an atomic action in the action block, a, asserts an object, a = Assert(?o), then its target term is an action variable, ?o, that is declared in the action block and the action variable binding is an object creation.

RIF-BLD compatibility

If the then part of a rule consists of a single action Assert(φ) then that action is written as simply φ.

If the then part of a rule consists of the action block Do(Assert(φ₁) ... Assert(φ_n)), n ≥ 2, then that action block is written as simply And(φ₁ ... φ_n).

Operational semantics of actions

This section specifies the intended semantics of the actions in a RIF-PRD document.

The effect intended of the ground actions in the RIF-PRD action language is to change the set of conditions that are satisfied before and after each action is implemented.

As a consequence, the intended semantics of the ground actions in the RIF-PRD action language determines a relation, called the RIF-PRD transition relation: →_RIF-PRD ⊆ P(W) × L × P(W), where W denotes the set of all the ground condition formulas in the RIF-PRD condition languages; where P(W) denotes the power set of W; and where L denotes the set of all the ground atomic actions in the RIF-PRD action language.

Definition (RIF-PRD transition relation). The intended semantics of RIF-PRD actions is completely specified by the transition relation →_RIF-PRD ⊆ P(W) × L × P(W). (w, α, w') ∈ →_RIF-PRD if and only if w ∈ W, w' ∈ W, and one of the following is true:

1. α is Assert(φ) and φ is a ground atomic and for every ground formula ψ in W, w' |= ψ if and only if And(w, φ) |= ψ;
2. α is Retract(φ) and φ is a ground atomic and for every ground formula ψ ∈ W, w' |= ψ if and only if w |= ψ and ψ |≠ φ;
3. α is Retract(o) and o is a constant and f₁, ..., f_n, n ≥ 0, are ground frames where o is the object, and m₁, ..., m_n', n' ≥ 0, are ground member atomics, and for every ground formula φ ∈ W, w' |= φ if and only if w |= φ and φ |≠ Or(f₁, ..., f_n, m₁, ..., m_n');
4. α is Assert(o) and o is a constant c_new that identifies a new object created with a target class identified by the constant c, such that for all ground condition formulae that contain c_new, φ_cnew ∈ W, w |≠  φ_cnew; and for every ground formula ψ in W, w' |= ψ if and only if And(w, c_new#c) |= ψ.

Rule 1 says that all the condition formulas that were satisfied before an assertion will be satisfied after, and that the condition formulas that are satisfied by the asserted ground formula will be satisfied after the assertion.

Rule 2 says that all the condition formulas that were satisfied before a retraction will be satisfied after, except if they are satisfied only by the retracted fact.

Rule 3 says that all the condition formulas that were satisfied before the removal of a frame object will be satisfied after, except if they are satisfied only by one of the frame or membership formulas about the removed object or a conjunction of such formulas.

Objects can be asserted only in the action block where they have been created (see the definition of a well-formed action block). Rule 4 says that all the condition formulas that were satisfied before the assertion of a frame object will be satisfied after, and that, in addtion, the new constant that identifies the asserted, and newly created, object satisfies the membership atomic for the object's class.