Parallel Determinized Chase

The backbone of the (D/R)MFA computation is chase-like procedure combines all trigger results (for the different disjuncts) into a single fact set, thereby treating disjunctions as conjunctions. This is what we mean by "determinized". Furthermore, all active triggers are applied at once in a single step. This is what we mean by "parallel". The parallelDeterminizedChase will later be passed the MfaObsoletenessConditions to define all the versions MFA/DMFA/RMFA. However, the definitions work with any LaxObsoletenessCondition. As for ChaseBranch and ChaseDerivation, the parallelDeterminizedChase is a more strict version of the parallelDeterminizedDerivation where the former forces the first fact set to be a Database (as part of a KnowledgeBase), while the latter accepts any FactSet.

parallelDeterminizedDerivation

We start with the more general definition, allowing to start from arbitrary FactSets.

def parallelDeterminizedDerivation_step {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (obs : LaxObsoletenessCondition sig) (fs : FactSet sig) : FactSet sig

One step of the parallelDeterminizedDerivation adds the results of all active triggers to the previous fact set. The results for all disjuncts are combined in the procees. Activeness of the triggers is with respect to a given LaxObsoletenessCondition.

Equations

• parallelDeterminizedDerivation_step rs obs fs = fs ∪ fun (f : Fact sig) => ∃ (trg : RTrigger obs rs), trg.val.active fs ∧ ∃ (i : Fin trg.val.mapped_head.length), f ∈ trg.val.mapped_head[↑i]

def parallelDeterminizedDerivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (obs : LaxObsoletenessCondition sig) (fs : FactSet sig) : InfiniteList (FactSet sig)

The parallelDeterminizedDerivation simply iterates the parallelDeterminizedDerivation_step on an initial FactSet using the InfiniteList.iterate function.

Equations

• parallelDeterminizedDerivation rs obs fs = InfiniteList.iterate fs (parallelDeterminizedDerivation_step rs obs)

def parallelDeterminizedDerivation_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (obs : LaxObsoletenessCondition sig) (start : FactSet sig) : FactSet sig

The parallelDeterminizedDerivation_result is the union of all FactSets in the derivation.

Equations

• parallelDeterminizedDerivation_result rs obs start f = ∃ (fs : FactSet sig), fs ∈ parallelDeterminizedDerivation rs obs start ∧ f ∈ fs

theorem parallelDeterminizedDerivation_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} : (parallelDeterminizedDerivation rs obs start).head = start

The parallelDeterminizedDerivation_head is the starting FactSet.

theorem parallelDeterminizedDerivation_head_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} : (parallelDeterminizedDerivation rs obs start).tail.head = parallelDeterminizedDerivation_step rs obs start

The head of the tail (i.e. the next element) results from performing one parallelDeterminizedDerivation_step on the starting FactSet.

theorem parallelDeterminizedDerivation_step_mem_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} (fs : FactSet sig) : fs ∈ parallelDeterminizedDerivation rs obs start → parallelDeterminizedDerivation_step rs obs fs ∈ parallelDeterminizedDerivation rs obs start

Performing a parallelDeterminizedDerivation_step on a member again yields a member.

theorem parallelDeterminizedDerivation_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} (l2 : InfiniteList (FactSet sig)) : l2 <:+ parallelDeterminizedDerivation rs obs start → l2 = parallelDeterminizedDerivation rs obs l2.head

Each suffix of a parallelDeterminizedDerivation is equal to the parallelDeterminizedDerivation that starts on the first element of the suffix.

theorem parallelDeterminizedDerivation_mem_rec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} {motive : (parallelDeterminizedDerivation rs obs start).Element → Prop} (head : motive ⟨(parallelDeterminizedDerivation rs obs start).head, ⋯⟩) (step : ∀ (elem : (parallelDeterminizedDerivation rs obs start).Element), motive elem → motive ⟨parallelDeterminizedDerivation_step rs obs elem.val, ⋯⟩) (a : (parallelDeterminizedDerivation rs obs start).Element) : motive a

This recursor allows proving properties of elements (i.e. FactSets with a membership proof) in a parallelDeterminizedDerivation and can be used with the induction tactic.

theorem parallelDeterminizedDerivation_facts_node_subset_every_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} (fs : FactSet sig) : fs ∈ parallelDeterminizedDerivation rs obs start → (parallelDeterminizedDerivation rs obs start).head ⊆ fs

The starting fact set is a subset of each derivation member,

theorem parallelDeterminizedDerivation_subset_total {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} (fs1 fs2 : FactSet sig) : fs1 ∈ parallelDeterminizedDerivation rs obs start → fs2 ∈ parallelDeterminizedDerivation rs obs start → fs1 ⊆ fs2 ∨ fs2 ⊆ fs1

Each two FactSets in a derivation must subsumes each other in (at least) one of two possible directions.

theorem parallelDeterminizedDerivation_predicates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} (fs : FactSet sig) : fs ∈ parallelDeterminizedDerivation rs obs start → fs.predicates ⊆ rs.predicates ∪ start.predicates

All predicates that occur in the derivation come from the rules or the starting fact set.

theorem parallelDeterminizedDerivation_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} (fs : FactSet sig) : fs ∈ parallelDeterminizedDerivation rs obs start → fs.constants ⊆ rs.head_constants ∪ start.constants

All constants that occur in the derivation come from the rule heads or the starting fact set.

theorem parallelDeterminizedDerivation_functions {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} (fs : FactSet sig) : fs ∈ parallelDeterminizedDerivation rs obs start → fs.function_symbols ⊆ rs.skolem_functions ∪ start.function_symbols

All function symbols that occur in the derivation come from the rule set's skolem functions or the starting fact set.

theorem parallelDeterminizedDerivation_result_predicates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} : (parallelDeterminizedDerivation_result rs obs start).predicates ⊆ rs.predicates ∪ start.predicates

All predicates in the derivation result come from the rules or the starting fact set.

theorem parallelDeterminizedDerivation_result_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} : (parallelDeterminizedDerivation_result rs obs start).constants ⊆ rs.head_constants ∪ start.constants

All constants in the derivation result come from the rule heads or the starting fact set.

theorem parallelDeterminizedDerivation_result_functions {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : RuleSet sig} {obs : LaxObsoletenessCondition sig} {start : FactSet sig} : (parallelDeterminizedDerivation_result rs obs start).function_symbols ⊆ rs.skolem_functions ∪ start.function_symbols

All function symbols in the derivation result come from the rule set's skolem functions or the starting fact set.

parallelDeterminizedChase

A parallelDeterminizedChase fixes a KnowledgeBase and start a parallelDeterminizedDerivation on the knowledge base's database. Some of the above theorems thereby can be refined. For example, function symbols can now only be skolem functions as the database only has constants as terms.

def parallelDeterminizedChase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (kb : KnowledgeBase sig) (obs : LaxObsoletenessCondition sig) : InfiniteList (FactSet sig)

A parallelDeterminizedChase is a special parallelDeterminizedDerivation starting on a database from a KnowledgeBase.

Equations

• parallelDeterminizedChase kb obs = parallelDeterminizedDerivation kb.rules obs kb.db.toFactSet.val

def parallelDeterminizedChase_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (kb : KnowledgeBase sig) (obs : LaxObsoletenessCondition sig) : FactSet sig

The parallelDeterminizedChase_result is simply the result of the underlying derivation.

Equations

• parallelDeterminizedChase_result kb obs = parallelDeterminizedDerivation_result kb.rules obs kb.db.toFactSet.val

theorem parallelDeterminizedChase_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {obs : LaxObsoletenessCondition sig} (fs : FactSet sig) : fs ∈ parallelDeterminizedChase kb obs → fs.constants ⊆ kb.rules.head_constants ∪ kb.db.constants.val

All constants in the chase come from the rule heads or the database.

theorem parallelDeterminizedChase_functions {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {obs : LaxObsoletenessCondition sig} (fs : FactSet sig) : fs ∈ parallelDeterminizedChase kb obs → fs.function_symbols ⊆ kb.rules.skolem_functions

All function symbols in the chase come from the rule set's skolem functions.

theorem parallelDeterminizedChase_result_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {obs : LaxObsoletenessCondition sig} : (parallelDeterminizedChase_result kb obs).constants ⊆ kb.rules.head_constants ∪ kb.db.constants.val

All constants in the chase result come from the rule heads or the database.

theorem parallelDeterminizedChase_result_functions {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {obs : LaxObsoletenessCondition sig} : (parallelDeterminizedChase_result kb obs).function_symbols ⊆ kb.rules.skolem_functions

All function symbols in the chase result come from the rule set's skolem functions.