(Disjunctive) (Existential) Rule

A disjunctive existential rule, or simply Rule, formally is an expression of the form $$∀ \vec{x}, \vec{y}. B(x, y) \to \bigvee_{i = 1}^{k} \exists \vec{z}_i. H_i(y_i, z_i)$$ where $B,H_1,\dots,H_k$ are conjunctions of function free atoms, $y$ is exactly the union of all $y_i$ and $x$, $y$, and all $z_i$ are disjoint lists of variables. $y$ is called frontier. $B$ is called body and the $H_i$ are called heads. We call a rule determinstic if $k = 1$ so if the head is merely a conjunction. For an overview on such rules (without disjunction) consider for example [BLMS11].

To represent this formal definition in Lean, we use a structure with a FunctionFreeConjunction for the body and a list of FunctionFreeConjunctions for the disjunction in the head. That's it! The frontier variables can simply be defined as the variables occurring both in body and head and the existential variables can be indentified as the variables that occur only in the head, without the need for explicit quantification.

structure Rule (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type (max (max u_1 u_2) u_3)

The definition of a Rule as discussed above.

• body : FunctionFreeConjunction sig
• head : List (FunctionFreeConjunction sig)

@[instance_reducible]

instance instDecidableEqRule {sig✝ : Signature} {inst✝ : DecidableEq sig✝.P} {inst✝¹ : DecidableEq sig✝.C} {inst✝² : DecidableEq sig✝.V} : DecidableEq (Rule sig✝)

Equations

• instDecidableEqRule = instDecidableEqRule.decEq

def instDecidableEqRule.decEq {sig✝ : Signature} {inst✝ : DecidableEq sig✝.P} {inst✝¹ : DecidableEq sig✝.C} {inst✝² : DecidableEq sig✝.V} (x✝ x✝¹ : Rule sig✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqRule.decEq { body := a, head := a_1 } { body := b, head := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Rule.frontier_for_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) (i : Nat) (lt : i < r.head.length) : List sig.V

This function returns the frontier variables that occur in a given head disjunct. This is a sublist of all the frontier variables.

Equations

• r.frontier_for_head i lt = List.filter (fun (v : sig.V) => decide (v ∈ r.head[i].vars)) r.body.vars

def Rule.frontier {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : List sig.V

This returns all the frontier variables of the rule, i.e. the variables that occur in both body and some head.

Equations

• r.frontier = List.filter (fun (v : sig.V) => r.head.any fun (h : FunctionFreeConjunction sig) => decide (v ∈ h.vars)) r.body.vars

def Rule.pure_body_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : List sig.V

The pure_body_vars are the variables from the body that are not in the frontier.

Equations

• r.pure_body_vars = List.filter (fun (x : sig.V) => decide ¬x ∈ r.frontier) r.body.vars

def Rule.isDatalog {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : Bool

We call a rule isDatalog if it does not contain existential variables, i.e. if all head variables occur in the body.

Equations

• r.isDatalog = r.head.all fun (h : FunctionFreeConjunction sig) => h.vars.all fun (v : sig.V) => decide (v ∈ r.body.vars)

def Rule.isDeterministic {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : Bool

We call a rule isDeterministic if it has exactly one head disjunct.

Equations

• r.isDeterministic = decide (r.head.length = 1)

def Rule.predicates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : List sig.P

The predicate symbols of a rule are just the predicate symbols from the body and all heads.

Equations

• r.predicates = r.body.predicates ++ List.flatMap FunctionFreeConjunction.predicates r.head

def Rule.constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : List sig.C

The constants of a rule are just the constants from the body and all heads.

Equations

• r.constants = r.body.consts ++ List.flatMap (fun (conj : FunctionFreeConjunction sig) => conj.consts) r.head

def Rule.head_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : List sig.C

Sometimes we require only the constants from the heads and therefore we define them here.

Equations

• r.head_constants = List.flatMap (fun (conj : FunctionFreeConjunction sig) => conj.consts) r.head

def Rule.existential_vars_for_head_disjunct {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) (i : Nat) (lt : i < r.head.length) : List sig.V

The existential variables for a given head are simply the variables from the head that are not in the frontier.

Equations

• r.existential_vars_for_head_disjunct i lt = List.filter (fun (v : sig.V) => decide ¬v ∈ r.frontier) r.head[i].vars

theorem Rule.mem_frontier_iff_mem_frontier_for_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} {v : sig.V} : v ∈ r.frontier ↔ ∃ (i : Nat), ∃ (lt : i < r.head.length), v ∈ r.frontier_for_head i lt

A variable is a frontier variable if and only if it is a frontier variable in some head disjunct.

theorem Rule.mem_frontier_for_head_of_mem_frontier_of_mem_head_terms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} {v : sig.V} {i : Nat} (lt : i < r.head.length) : v ∈ r.frontier → VarOrConst.var v ∈ r.head[i].terms → v ∈ r.frontier_for_head i lt

A variable is in the frontier of a head if it is in the frontier of the rule and occurs as a term in the given head.

theorem Rule.frontier_subset_vars_body {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} : r.frontier ⊆ r.body.vars

All frontier variables occur in the body.

theorem Rule.frontier_for_head_subset_vars_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} {i : Nat} (lt : i < r.head.length) : r.frontier_for_head i lt ⊆ r.head[i].vars

The frontier variables in a given head occur in the list of variables for the same head.

theorem Rule.head_constants_subset_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : r.head_constants ⊆ r.constants

The head constants of the rule are also constants of the whole rule.

theorem Rule.mem_head_vars_of_mem_existential_vars_for_head_disjunct {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} {i : Nat} {lt : i < r.head.length} (v : sig.V) : v ∈ r.existential_vars_for_head_disjunct i lt → v ∈ r.head[i].vars

Each existential variable is in the head.

theorem Rule.not_mem_frontier_of_mem_existential_vars_for_head_disjunct {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} {i : Nat} {lt : i < r.head.length} (v : sig.V) : v ∈ r.existential_vars_for_head_disjunct i lt → ¬v ∈ r.frontier

Each existential variable is not in the frontier.

theorem Rule.mem_frontier_of_mem_head_disjunct_of_not_mem_existential_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} {i : Nat} {lt : i < r.head.length} (v : sig.V) : v ∈ r.head[i].vars → ¬v ∈ r.existential_vars_for_head_disjunct i lt → v ∈ r.frontier

A variable that is in a head but not existential must be in the frontier.

theorem Rule.mem_existential_vars_of_mem_head_disjunct_of_not_mem_frontier {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} {i : Nat} {lt : i < r.head.length} (v : sig.V) : v ∈ r.head[i].vars → ¬v ∈ r.frontier → v ∈ r.existential_vars_for_head_disjunct i lt

A variable that is in a head but not in the frontier must be existential.