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 [DNR08]. On disjunctive rules this is more complicated as can be seen in chaseTreeResultIsUniversal.

def TreeDerivation.firstBranch_from_start {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) (start : td.NodeWithAddress) : ChaseDerivation obs rules

The firstBranch_from_start of a TreeDerivation is generated by always picking the first child node by starting from a particular node in the tree.

Equations

• td.firstBranch_from_start start = td.generate_subderivation start (fun (node : td.NodeWithAddress) => node.childNodes[0]?) id ⋯ ⋯

theorem TreeDerivation.branches_start_eq_firstBranch_from_start {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {start : td.NodeWithAddress} (det : rules.isDeterministic) (deriv : ChaseDerivation obs rules) : deriv ∈ start.subderivation.branches → deriv = td.firstBranch_from_start start

In the deterministic setting, each derivation in a branches of a tree derivation node directly corresponds to the firstBranch_from_start.

def TreeDerivation.firstBranch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition 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 starting from the root.

Equations

• td.firstBranch = td.firstBranch_from_start (TreeDerivation.NodeWithAddress.root td)

def TreeDerivation.firstResult {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition 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 : ObsolescenceCondition 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 : ObsolescenceCondition 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 : ObsolescenceCondition 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 : ObsolescenceCondition 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.root_intoTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {det : rules.isDeterministic} : (cd.intoTree det).root = cd.head

The root of intoTree is the original head.

theorem ChaseDerivation.next_intoTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {det : rules.isDeterministic} : (cd.intoTree det).childNodes[0]? = cd.next

The first child node of intoTree is the original next node.

theorem ChaseDerivation.firstBranch_from_start_with_intoTree_eq_cd {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {cd : ChaseDerivation obs rules} (det : rules.isDeterministic) {start : td.NodeWithAddress} (cd_eq : cd.intoTree det = start.subderivation) : td.firstBranch_from_start start = cd

In the context of any TreeDerivation, for a given start node and a ChaseDerivation cd, firstBranch_from_start for the start node returns exactly cd as long as the tree at the start node coincides the tree transformed cd. This is an auxiliary result for firstBranch_intoTree_eq_self below.

theorem ChaseDerivation.firstBranch_intoTree_eq_self {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {deterministic : rules.isDeterministic} (cd : ChaseDerivation obs rules) (det : 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 : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) (deterministic : rules.isDeterministic) : (cd.intoTree deterministic).firstResult = cd.result

The firstResult of intoTree is the original ChaseDerivationSkeleton.result.

def ChaseBranch.intoTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition 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 : ObsolescenceCondition sig} {kb : KnowledgeBase sig} (cb : ChaseBranch obs kb) : kb.isDeterministic → cb.result.universallyModelsKb kb

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