octalgo.octalgo.rinstance

Require Import syntax.
Require Import subs.
Require Import pmatch.
Require Import bSemantics.
Require Import monotonicity.
Require Import soundness.
Require Import fixpoint.
Require Import completeness.

Require Import bigop_aux.
Require Import utils.
Require Import finseqs.

Set Implicit Arguments.

Partially instantiating a Datalog program

Section RuleInstance.

Actual transformation

Hypotheses: a safe program p, an interpretation i and def a default constant

Variable p : program.
Hypothesis psafe : prog_safe p.
Variable i : interp.
Variable def : syntax.constant.

Rv is the set of variables to replace

Variable Rv : {set 'I_n }.

assuming a set of substitutions

Variable subs : {set sub }.

facts fixedpoint

Definition ffp := sem p def #|bp | i.

Any substitution that matches a clause cl (which intersects with Rv) in the model of p has its restriction to Rv in subs. This completeness condition of subs ensures that the transformation does not lose any deductible fact. The intersection condition could be dropped by manually adding emptysub to subs

Hypothesis subs_comp :
  [∀ cl in p ,
    (#|tail_vars (body_cl cl) :&: Rv | > 0) ==>
      [∀ s : sub ,
        (bmatch def ffp cl s )
    ==> (sub_filter s Rv \in subs )]].

stv returns the to-be-replaced variables of a clause

Definition stv cl := Rv :&: tail_vars (body_cl cl).

Instantiation of a clause by subs

returns a sequence of rules by applying on the clause only the substitution whose domain is exactly the domain of the clause

Definition inst_rule (cl : clause): seq clause :=

  if (#|tail_vars (body_cl cl) :&: Rv | > 0) then
    [seq scl s cl | s <- enum subs & dom s == stv cl ]
  else [:: cl ].

tprog is obtained by instantiating all the rules of p

Definition tprog : program :=
flatten [seq (inst_rule cl ) | cl <- p ].

Adequacy of the transformation

Any iteration of the semantic of p from i is in ffp

Lemma ffp_comp (k : nat) : sem p def k i \subset ffp.

For any clause, the set of substitutions that match cl with the mth iteration of the semantic is a subset of those that match cl with the model of p

Lemma nomega_fp : ∀ (cl : clause) (m : nat), cl \in p →
match_body (sem p def m i) (body_cl cl) \subset match_body ffp (body_cl cl).

Completeness: the m iterate of p semantics is contained in the

m iterate of the semantics of tprog

Lemma ccompleteness (m : nat)
: (sem p def m i ) \subset (sem tprog def m i ).

Soundness: the m iterate of tprog semantics is contained in the

m iterate of the semantics of p

Lemma csoundness (m : nat)
: (sem tprog def m i ) \subset (sem p def m i ).

p and tprog semantic coincide àt each iteration

Theorem cadequacy (m : nat)
: (sem tprog def m i ) = (sem p def m i ).

End RuleInstance.