Skolem Terms

If you are familiar with existential rules, you may have expected (labelled) nulls to be part of the Signature. These nulls would act as placeholders that are introduced during the chase to find fresh representatives for existentially quantified variables. However, implementing this freshness is not really nice to model since it would require is to keep global state around to know which nulls have already been used. Instead, we act as if the existentially quantified variables where Skolemized. By that, freshly introduced terms simply become Skolem terms and we can show that these are indeed fresh by design. Some works on existential rules take this view, first and foremost of course the ones considering the Skolem chase [Mar09].

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

As a building block for Skolem terms, we introduce SkolemFS as a Skolem Function Symbol here. This structure captures the rule, disjunct, and (existential) variable for that the Skolem function was introduced.

• rule : Rule sig
• headIdx : Nat
• headIdx_lt : self.headIdx < self.rule.head.length
• v : sig.V
• v_mem : self.v ∈ self.rule.existential_vars_for_head_disjunct self.headIdx ⋯

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

Equations

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

@[instance_reducible]

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

Equations

• instDecidableEqSkolemFS = instDecidableEqSkolemFS.decEq

@[implicit_reducible]

def SkolemFS.arity {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (sfs : SkolemFS sig) : Nat

The arity corresponds to the size of the frontier of the rule, i.e. the universal variables that occur in both body and head.

Equations

• sfs.arity = sfs.rule.frontier.length

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

The Skolem function symbols of a rule are all SkolemFS with the rule id, all possible head indices and the respective existential variables.

Equations

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

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

With SkolemTerm we mean the Skolemized version of an existential variable. That is, a SkolemTerm only consists of a function symbol (SkolemFS) and a list of universal variables. Beyond that, we allow this inductive structure also to be a plain variable or constant. Thereby, the SkolemTerm can represent any term occurring in a Skolemized rule.

• var {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (v : sig.V) : SkolemTerm sig
• const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (c : sig.C) : SkolemTerm sig
• func {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : SkolemFS sig) (frontier : List sig.V) (arity_ok : frontier.length = fs.arity) : SkolemTerm sig

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

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqSkolemTerm.decEq (SkolemTerm.var a) (SkolemTerm.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqSkolemTerm.decEq (SkolemTerm.var v) (SkolemTerm.const c) = isFalse ⋯
• instDecidableEqSkolemTerm.decEq (SkolemTerm.var v) (SkolemTerm.func fs frontier arity_ok) = isFalse ⋯
• instDecidableEqSkolemTerm.decEq (SkolemTerm.const c) (SkolemTerm.var v) = isFalse ⋯
• instDecidableEqSkolemTerm.decEq (SkolemTerm.const a) (SkolemTerm.const b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqSkolemTerm.decEq (SkolemTerm.const c) (SkolemTerm.func fs frontier arity_ok) = isFalse ⋯
• instDecidableEqSkolemTerm.decEq (SkolemTerm.func fs frontier arity_ok) (SkolemTerm.var v) = isFalse ⋯
• instDecidableEqSkolemTerm.decEq (SkolemTerm.func fs frontier arity_ok) (SkolemTerm.const c) = isFalse ⋯

@[instance_reducible]

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

Equations

• instDecidableEqSkolemTerm = instDecidableEqSkolemTerm.decEq

def SkolemTerm.variables {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : SkolemTerm sig → List sig.V

We may obtain all variables from a SkolemTerm term as the list of all variables occurring in the functional term or, if the term is a plain variable, simply as the singleton list with this one variable.

Equations

• (SkolemTerm.var v).variables = [v]
• (SkolemTerm.const c).variables = []
• (SkolemTerm.func fs vs arity_ok).variables = vs

def VarOrConst.skolemize {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rule : Rule sig) (i : Nat) (lt : i < rule.head.length) : VarOrConst sig → SkolemTerm sig

In the context of a rule and a disjunct (in that rule), we can turn a VarOrConst into a SkolemTerm using the frontier of the rule. This function is used for skolemizing existential variables in rules.

Equations

• One or more equations did not get rendered due to their size.
• VarOrConst.skolemize rule i lt (VarOrConst.const c) = SkolemTerm.const c

theorem VarOrConst.skolemize_injective {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rule : Rule sig) (i : Nat) (lt : i < rule.head.length) (s t : VarOrConst sig) : skolemize rule i lt s = skolemize rule i lt t → s = t

The skolemize function is injective. That is, if the produced SkolemTerms are the same, then they need to result from the same variable. This is important to ensure that introduced Skolem terms are indeed fresh (and unique) in the chase.