octalgo.octalgo.tSemantics

Require Import syntax.
Require Import occurrences.
Require Import subs.
Require Import pmatch.
Require Import bSemantics.
Require Import monotonicity.
Require Import soundness.

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

Require Import Coq.Program.Equality.
Require Import Sumbool.

Set Implicit Arguments.

Implicit Types (s r : sub) (d def : syntax.constant) (t : term) (a : atom)
(ga : gatom) (tl : list atom) (cl : clause) (i : interp).

Section tSemantics.

Variable p : program.
Variable gat_def : gatom.

Trace semantics

Rule grounding

Section rul_gr.

rule grounding: a pair of a clause and a substitution

Inductive rul_gr :=
| RS : clause → sub → rul_gr.

Conversion to and from pair so that we have a cancellable

Definition rul_gr_rep l := match l with
| RS c g ⇒ (c, g) end.

Definition rul_gr_pre l := match l with
| (c, g) ⇒ RS c g end.

Lemma rul_gr_repK : cancel rul_gr_rep rul_gr_pre.

rul_gr is an eq type

Definition rul_gr_eqMixin :=
CanEqMixin rul_gr_repK.

Canonical rul_gr_eqType := Eval hnf in EqType rul_gr rul_gr_eqMixin.

rul_gr is a choice type

Definition rul_gr_choiceMixin :=
CanChoiceMixin rul_gr_repK.

Canonical rul_gr_choiceType := Eval hnf in ChoiceType rul_gr rul_gr_choiceMixin.

rul_gr is a count type

Definition rul_gr_countMixin :=
(@CanCountMixin (prod_countType clause_countType sub)
rul_gr _ _ rul_gr_repK).

Canonical rul_gr_countType := Eval hnf in CountType rul_gr rul_gr_countMixin.

rul_gr is a finite type

Definition rul_gr_finMixin :=
(@CanFinMixin rul_gr_countType
(prod_finType clause_finType sub)
_ _ rul_gr_repK).

Canonical rul_gr_finType := Eval hnf in FinType rul_gr rul_gr_finMixin.

End rul_gr.

Semantic trees (traces)

Section trace_sem_trees.

A semantic tree is a tree with bounded width bn (the maximal size of the body of clause),

nodes are in rul_gr ie. pairs of clause and substitution
leaves are ground atoms (from the interpretation).

Definition trace_sem_trees := (@WUtree_sf rul_gr_finType gatom_finType bn gat_def).

force typing

Definition my_tst_sub x (H : wu_pred x) : trace_sem_trees := WU_sf_sub H.

Get the head node label (ie. the last clause and substitution)

Definition tst_node_head (t : trace_sem_trees) := match (val t) with
| ABLeaf _ ⇒ None
| ABNode h _ ⇒ Some h end.

Deduced term: either the fact or the head atom of the last clause grounded by the substitution.

Definition ded def (t : trace_sem_trees) := match (val t) with
| ABLeaf f ⇒ f
| ABNode (RS (Clause h _) s) _ ⇒ gr_atom_def def s h end.

translate a set of traces in an interpretation

Definition sem_tree_to_inter def (ts : {set trace_sem_trees }) : interp := [set ded def x | x in ts ].

Checks that the deduction from the traces is equal to ghe atoms grounded by the supplied substitution. This is what is the relation existing begween the children of a trace node and the body of the clause associated to that node

Definition ded_sub_equal (def : syntax.constant) (lx : seq trace_sem_trees) (s : sub) (ats : seq atom) :=
(map (ded def) lx ) == (map (gr_atom_def def s) ats ).

Computes the traces representing the consequence of a clause from the traces representing the current interpretation

Definition cons_clause_t def (cl : clause) (k : {set trace_sem_trees }) : {set trace_sem_trees } :=
  let b := (body_cl cl) in
  let subs := match_body (sem_tree_to_inter def k) b in
  pset [set (wutree_option_fst (@wu_pcons_seq rul_gr_finType gatom_finType bn gat_def (RS cl s) lx))
                                         | lx : (size b ).-tuple trace_sem_trees ,
                                            s : sub in subs &
                                            (ded_sub_equal def lx s b &&
                                            all (mem k) lx )].

A member of the consequences of the clause is an ABnode labelled by (cl, s) where s is a substitution

Lemma cons_clause_h def cl k (xtrace : trace_sem_trees) :
(xtrace \in cons_clause_t def cl k ) → ∃ s, ABroot (val xtrace) = inl (RS cl s).

Trace semantics definition

Initialize the trace semantic from a standard interpretation of the EDB by creating leaf trees.

Definition base_sem_t (i : interp) : {set trace_sem_trees } :=
[set my_tst_sub (wu_pred_leaf x) | x in i ].

the forward chain step for the trace semantics.

Definition fwd_chain_t def (k : {set trace_sem_trees }) : {set trace_sem_trees } :=
k :|: \bigcup_(cl <- p ) cons_clause_t def cl k.

interp_t is the equivalent of interp for the trace semantics

Notation interp_t := {set trace_sem_trees }.

The m iterate of the semantics

Definition sem_t (def : syntax.constant) (m : nat) (i : interp) :=
iter m (fwd_chain_t def) (base_sem_t i).

The leaf trees in the semantics are the ground atoms of the initial interpretation

Lemma sem_t_leaf def i ga Htra m : {| wht := ABLeaf rul_gr_finType ga ; Hwht := Htra |}
\in sem_t def m i → ga \in i.

The result of fwd_chain contains its argument

Lemma fwd_chain_t_inc (it : interp_t) def : it \subset fwd_chain_t def it.

technical lemma rephrasing the above one

Lemma fwd_chain_t_inc_single (t : trace_sem_trees) (it : interp_t) def : (t \in it ) → t \in fwd_chain_t def it.

and the same for fwd_chain

Lemma fwd_chain_inc_single ga i def : (ga \in i ) → ga \in fwd_chain def p i.

Simple reinterpretation of definition of ded_sub_equal

Lemma ded_sub_equal_equal_to_def l tval def s : (ded_sub_equal def tval s l ) = ([seq ded def i | i <- tval ] == [seq gr_atom_def def s i | i <- l ]).

Trivial technical lemma but inversion was too agressive in the following proof

Lemma simple_cons_eq_inversion {T : Type} (a b : T) (l ll : seq T) : (a ::l = b ::ll ) → (a = b ∧ l = ll ).

If applying s on a list l gives a list of ground atom, then using s as a grounding and applying it to l will also give this list of ground atoms.

Lemma stail_eq_to_gr_atom_eq (l : seq atom) (def : syntax.constant) (s : sub) (gtl : seq gatom) (H : stail l s = [seq to_atom ga | ga <- gtl ]) :
[seq gr_atom (to_gr def s) a | a <- l ] = gtl.

If applying the substitution gives ground atoms, we have ded_sub_equal without explicit grounding on the list of atoms l

Lemma ded_gr_equal_stail l (gtailrec : (size l ).-tuple trace_sem_trees) def s gtl :
([seq ded def i | i <- gtailrec ] = gtl ) → (stail l s = [seq to_atom ga | ga <- gtl ]) → ded_sub_equal def gtailrec s l.

There is no new leaf in the consequence of a clause

Lemma no_deduced_leaf (x : gatom_finType) (def : syntax.constant) (k : {set trace_sem_trees })
(Habs : wutree_fin (wu_leaf x) \in \bigcup_cl cons_clause_t def cl k) : False.

Lemma cons_clause_t_desc def (deduced : {set [finType of trace_sem_trees ]}) (h : rul_gr_finType) (l : seq (@ABtree rul_gr_finType gatom_finType))
      (t : trace_sem_trees) (Hin : val t \in l)
      (Hwup : @wu_pred _ _ bn (ABNode h l)) : (my_tst_sub Hwup
           \in \big [setU (T:=[finType of trace_sem_trees ])/set0 ]_cl
                  cons_clause_t def cl deduced ) → t \in deduced.

If a tree is in a given step of the trace semantic, so are all its subtrees.

Lemma trace_sem_prev_trees nb_iter def init :
∀ (t1 t2 : trace_sem_trees), t2 \in (sem_t def nb_iter init )
→ subtree (val t1) (val t2) → t1 \in (sem_t def nb_iter init ).

If a tree is in a given step of the trace semantic, its strict subtrees are in the previous step.

Lemma trace_sem_prev_trees_m1 nb_iter def init :
∀ (t1 t2 : trace_sem_trees), t2 \in (sem_t def nb_iter init )
→ strict_subtree (val t1) (val t2) → t1 \in (sem_t def nb_iter .-1 init ).

Completeness of the trace semantic.

For each atom in the regular semantic, there is a tree in the trace semantic that can be interpreted (it deduces) the atom

Lemma trace_sem_completeness nb_iter def i :
prog_safe p → [∀ x in (sem p def nb_iter i ), ∃ y in (sem_t def nb_iter i ), ded def y == x ].

Soundness of the trace semantics

technical lemma

Lemma type_preserving_inversion (A B C : finType) (f2 : A → B → C)
(D1 : mem_pred A) (D2 : A → mem_pred B)
: ∀ y : C, imset2_spec f2 D1 D2 y → (∃ x1 : A , ∃ x2 : B , (in_mem x1 D1 ∧ in_mem x2 (D2 x1) ∧ (y = f2 x1 x2 ))).

technical lemma: unification failed with normal setIdP

Lemma setIdP_bool_to_prop {T : finType} (pA pB : pred T) : ∀ x, x \in [set y | pA y & pB y ] → ((pA x ) ∧ (pB x )).

For all trace in the m step of the trace semantic, its deduced atom is in the m step of the regular semantics

Lemma trace_sem_soundness nb_iter def i:
prog_safe p → [∀ t in (sem_t def nb_iter i ), ded def t \in (sem p def nb_iter i )].

If we have a node in the trace semantics with (cl, s) as root, then there is an interpretation where the body of cl matches producing s.

Lemma trace_sem_head_match def cl s l m i Htr :
prog_safe p
→ {| wht := ABNode (RS cl s ) l ; Hwht := Htr |} \in sem_t def m i
→ [∃ i' : interp , ((s \in match_body i' (body_cl cl)))].

technical lemma

Lemma sterm_ga_eq def s aa aga :
[seq sterm s x | x <- aa ] = [seq Val x | x <- aga ]
→ aga = [seq gr_term_def def s i | i <- aa ].

technical lemma

Lemma stail_ded_eq cl s gtl def :
stail (body_cl cl) s = [seq to_atom ga | ga <- gtl ]
→ [seq gr_atom_def def s i | i <- body_cl cl ] =
[seq ded def i | i <- [seq my_tst_sub (x:=ABLeaf rul_gr x) (wu_pred_leaf x) | x <- gtl ]].

technical lemma

Lemma all_mem_edb_tst gtl (i : interp) :
all (mem i) gtl →
all (mem [set my_tst_sub (x:=ABLeaf rul_gr x) (wu_pred_leaf x) | x in i ])
[seq my_tst_sub (x:=ABLeaf rul_gr_finType x) (wu_pred_leaf x) | x <- gtl ].

Let p be safe, forall clause cl of p, and substitution s result of matching cl against the standard semantics of p at step m, then there is a trace t in the (m+1) trace-semantics of p whose head is (cl,s)

Lemma trace_sem_completeness_b def m i: prog_safe p →
[∀ cl:clause in p , [∀ s:sub in match_body (sem p def m i) (body_cl cl),
[∃ t in sem_t def m .+1 i , (tst_node_head t ) == Some (RS cl s)]]].

All the clauses in the roots in the trace semantics of p are clauses of p

Lemma tr_cl_in (tr : trace_sem_trees) def cl s m i:
tr \in sem_t def m i
→ ABroot (val tr) = inl (RS cl s)
→ cl \in p.

For a safe program (for the heads), and any trace in the semantics, if its interpretation is an EDB predicate, then the trace is a leaf.

Lemma sem_t_Edb_pred def k i (tr : trace_sem_trees) ga :
tr \in sem_t def k i
→ prog_safe_hds p
→ ded def tr = ga
→ predtype (sym_gatom ga) = Edb
→ ∃ gab, wht tr = (ABLeaf rul_gr gab ).

For a safe interpretation (an EDB), and any trace in the semantics, if its interpretation is an IDB predicate, then the trace is an internal node.

Lemma sem_t_Idb_pred def k i (tr : trace_sem_trees) ga :
tr \in sem_t def k i

→ safe_edb i
→ ded def tr = ga
→ predtype (sym_gatom ga) = Idb
→ ∃ clsb, ∃ descs, wht tr = (ABNode clsb descs ).

Utility lemmas relating tocc and the trace

we find in the semantics If we have a program with safe heads (no edb pred) and we have a trace in the semantics whose root is clause cl. If we have an occurrence, that points to a term of this clause and is on an atom that is an EDB predicate, then this will appear as a leaf in the direct children of the trace.

Lemma edb_in_sem_t_descs def cl s descs Hwht f (tocc : t_occ_finType p) k (i : interp) :
{| wht := ABNode (RS cl s ) descs ; Hwht := Hwht |}
\in sem_t def k i
→ prog_safe_hds p
→ nth_error p (r_ind tocc) = Some cl
→ p_at tocc = Some f
→ predtype f = Edb
→ ∃ ga, nth_error descs (b_ind tocc) = Some (@ABLeaf _ _ ga).

Same as above, but with an IDB predicate, in that case, the child must be an internal node and its head symbol must be the IDB predicate found

Lemma idb_in_sem_t_descs def cl s descs Hwht f (tocc : t_occ_finType p) k (i : interp) :
   {| wht := ABNode (RS cl s ) descs ; Hwht := Hwht |}
       \in sem_t def k i
→ safe_edb i
→ nth_error p (r_ind tocc) = Some cl
→ p_at tocc = Some f
→ predtype f = Idb
→ ∃ clsb, ∃ descsb, hsym_cl (rul_gr_rep clsb ).1 = f ∧
    nth_error descs (b_ind tocc) = Some (@ABNode _ _ clsb descsb).

End trace_sem_trees.

End tSemantics.