octalgo.datalogcert.bSemantics

The DatalogCert Library CNRS & Université Paris-Sud, Université Paris-Saclay Copyright 2016-2019 : FormalData Original authors: Véronique Benzaken Évelyne Contejean Stefania Dumbrava
Fourth part of the original file "pengine.v" with an additional new part

Require Import syntax.
Require Import subs.
Require Import pmatch.


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

Set Implicit Arguments.

Semantics of a Datalog program

Section bSemantics.

Consequences of a clause

one iteration of fwd_chain for a one-clause program Given a clause cl: h :- b gives back s h for all s that match b in interpretation i. def is usually not used as cl should be safe and does not introduce variables in its head.
Definition cons_clause (def : syntax.constant) (cl : clause) i : {set gatom} :=
  [set gr_atom_def def s (head_cl cl) | s in match_body i (body_cl cl)].

If clause verifies safe_cl_hd then the symbols we get are all in IDB
Lemma cons_clause_idb (def : syntax.constant) (cl : clause) i :
  safe_cl_hd cl → [∀ x in cons_clause def cl i, predtype (sym_gatom x) == Idb].

one iteration of fwd_chain for a program
Definition fwd_chain def p i : {set gatom} :=
  i :|: \bigcup_(cl <- p) cons_clause def cl i.

Semantic of a program up to m steps

sem p d m i iterates fwd_chain m times over i. Added to the original files
Definition sem (p : program) (def : syntax.constant) (m : nat) (i : interp) :=
  iter m (fwd_chain def p) i.

If p has safe heads, sem is safe (only defines elements in the IDB or it was in i_init
Lemma sem_idb_safe (p : program) (def : syntax.constant) (m : nat) i_init :
  prog_safe_hds p →
  [∀ x in (sem p def m i_init) :\: i_init, predtype (sym_gatom x) == Idb].

If p has safe heads, any atom in the semantics from the EDB comes from init
Lemma sem_idb_in (p : program) (def : syntax.constant) (m : nat) i_init ga :
  prog_safe_hds p → ga \in (sem p def m i_init) →
  predtype (sym_gatom ga) == Edb → ga \in i_init.

End bSemantics.