The Chase on Deterministic Rules

In our most general setting, we consider existential rules with disjunctions. Here, we consider the special case of deterministic rules, i.e. rules with exactly one head disjunct (so essentially no disjunction at all). Here, ChaseTree and ChaseBranch consequently coincide. At least intuitively. Formally, we still need to implement the corresponding transitions.

Arguably the most interesting result of this file is deterministicChaseBranchResultUniversallyModelsKb. It states that in the deterministic setting, the result of a ChaseBranch is itself a universal model. That is, a model that can be homomorphically embedded into every other model. On disjunctive rules this is more complicated as can be seen in chaseTreeResultIsUniversal.

def TreeDerivation.firstBranch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : ChaseDerivation obs rules

The firstBranch of a TreeDerivation is generated by always picking the first child node.

Equations

• One or more equations did not get rendered due to their size.

def TreeDerivation.firstResult {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : FactSet sig

The firstResult is the result of the firstBranch.

Equations

• td.firstResult = td.firstBranch.result

theorem TreeDerivation.firstResult_mem_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} : td.firstResult ∈ td.result

The firstResult is a member of the TreeDerivation.result.

theorem TreeDerivation.branches_eq_firstBranch_of_determinsitic {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (det : rules.isDeterministic) : td.branches = fun (b : ChaseDerivation obs rules) => b = td.firstBranch

In the deterministic setting, the branches of a TreeDerivation only contain the firstBranch.

theorem ChaseTree.deterministicChaseTreeResultUniversallyModelsKb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree obs kb} : kb.isDeterministic → ct.firstResult.universallyModelsKb kb

In the deterministic setting, the firstResult of a ChaseTree is by itself a universal model.

def ChaseDerivation.intoTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) (deterministic : rules.isDeterministic) : TreeDerivation obs rules

We can straightforwardly convert a ChaseDerivation into a TreeDerivation that has the original ChaseDerivation as its only branch.

Equations

• cd.intoTree deterministic = { tree := FiniteDegreeTree.from_branch cd.branch, isSome_root := ⋯, triggers_exist := ⋯, fairness_leaves := ⋯, fairness_infinite_branches := ⋯ }

theorem ChaseDerivation.firstBranch_intoTree_eq_self {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) (deterministic : rules.isDeterministic) : (cd.intoTree deterministic).firstBranch = cd

The firstBranch of intoTree is the original ChaseDerivation.

theorem ChaseDerivation.firstResult_intoTree_eq_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) (deterministic : rules.isDeterministic) : (cd.intoTree deterministic).firstResult = cd.result

The firstResult of intoTree is the original ChaseDerivation.result.

def ChaseBranch.intoTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (cb : ChaseBranch obs kb) (deterministic : kb.isDeterministic) : ChaseTree obs kb

We can not only convert a ChaseDerivation into a TreeDerivation but also a ChaseBranch into a ChaseTree.

Equations

• cb.intoTree deterministic = { toTreeDerivation := cb.intoTree deterministic, database_first := ⋯ }

theorem ChaseBranch.deterministicChaseBranchResultUniversallyModelsKb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (cb : ChaseBranch obs kb) : kb.isDeterministic → cb.result.universallyModelsKb kb

In the deterministic setting, a ChaseBranch.result is a universal model.