Terms

In this file, we define various kinds of terms that form some of the most basic building blocks of other structures like atoms and rules.

structure Signature : Type (max (max (u + 1) (v + 1)) (w + 1))

First of all, almost all of our definitions consider a fixed but arbitrary Signature of predicate symbols P, variables V, and constants C. Also every predicate has a fixed arity. Note that P, V, and C can be arbitrary types so there are no requirements in terms of countability or finiteness. However, intuitively you can consider them to be countably infinite sets. This would allow to pick fresh elements for example. In places where we need this property, we express this through the GetFreshInhabitant type class.

• P : Type u
• V : Type v
• C : Type w
• arity : self.P → Nat

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.

structure SkolemFS (sig : Signature) [DecidableEq sig.V] : Type u_2

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. The arity corresponds to the size of the frontier of the rule, i.e. the universal variables that occur in both body and head.

• ruleId : Nat
• disjunctIndex : Nat
• var : sig.V
• arity : Nat

def instDecidableEqSkolemFS.decEq {sig✝ : Signature} {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 instDecidableEqSkolemFS {sig✝ : Signature} {inst✝ : DecidableEq sig✝.V} : DecidableEq (SkolemFS sig✝)

Equations

• instDecidableEqSkolemFS = instDecidableEqSkolemFS.decEq

inductive SkolemTerm (sig : Signature) [DecidableEq sig.C] [DecidableEq sig.V] : Type (max 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.C] [DecidableEq sig.V] (v : sig.V) : SkolemTerm sig
• const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (c : sig.C) : SkolemTerm sig
• func {sig : Signature} [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✝.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 instDecidableEqSkolemTerm {sig✝ : Signature} {inst✝ : DecidableEq sig✝.C} {inst✝¹ : DecidableEq sig✝.V} : DecidableEq (SkolemTerm sig✝)

Equations

• instDecidableEqSkolemTerm = instDecidableEqSkolemTerm.decEq

def SkolemTerm.variables {sig : Signature} [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

VarOrConst

We introduce VarOrConst as yet another inductive type representing a term. This is a function free SkolemTerm, i.e. either a variable or a constant (thus the name). Having this is a separate type is more convenient for us than restricting the SkolemTerm further. VarOrConst is used to define FunctionFreeAtom later and is thus also the basic building block of (non-Skolemized) Rules.

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

As the name suggests, a VarOrConst is either a variable or a constant.

• var {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (v : sig.V) : VarOrConst sig
• const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (c : sig.C) : VarOrConst sig

def instDecidableEqVarOrConst.decEq {sig✝ : Signature} {inst✝ : DecidableEq sig✝.C} {inst✝¹ : DecidableEq sig✝.V} (x✝ x✝¹ : VarOrConst sig✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqVarOrConst.decEq (VarOrConst.var a) (VarOrConst.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqVarOrConst.decEq (VarOrConst.var v) (VarOrConst.const c) = isFalse ⋯
• instDecidableEqVarOrConst.decEq (VarOrConst.const c) (VarOrConst.var v) = isFalse ⋯
• instDecidableEqVarOrConst.decEq (VarOrConst.const a) (VarOrConst.const b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance instDecidableEqVarOrConst {sig✝ : Signature} {inst✝ : DecidableEq sig✝.C} {inst✝¹ : DecidableEq sig✝.V} : DecidableEq (VarOrConst sig✝)

Equations

• instDecidableEqVarOrConst = instDecidableEqVarOrConst.decEq

def VarOrConst.isVar {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] : VarOrConst sig → Bool

A VarOrConst is a variable if it was built using the var constructor.

Equations

• (VarOrConst.var v).isVar = true
• (VarOrConst.const c).isVar = false

def VarOrConst.filterVars {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] : List (VarOrConst sig) → List sig.V

Given a list of VarOrConst, we can filter out all the variables. Note that we do not use List.filter here since we need to change the list type on the way.

Equations

• VarOrConst.filterVars [] = []
• VarOrConst.filterVars (VarOrConst.var v :: vocs) = v :: VarOrConst.filterVars vocs
• VarOrConst.filterVars (VarOrConst.const c :: vocs) = VarOrConst.filterVars vocs

def VarOrConst.filterConsts {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] : List (VarOrConst sig) → List sig.C

Analogous to filterVars, we can also filter for constants.

Equations

• VarOrConst.filterConsts [] = []
• VarOrConst.filterConsts (VarOrConst.var v :: vocs) = VarOrConst.filterConsts vocs
• VarOrConst.filterConsts (VarOrConst.const c :: vocs) = c :: VarOrConst.filterConsts vocs

def VarOrConst.skolemize {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (ruleId disjunctIndex : Nat) (frontier : List sig.V) (voc : 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 ruleId disjunctIndex frontier (VarOrConst.const c) = SkolemTerm.const c

theorem VarOrConst.filterVars_occur_in_original_list {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (l : List (VarOrConst sig)) (v : sig.V) : v ∈ filterVars l → var v ∈ l

Each member of filterVars is in the original list (when applyign the var constructor again.)

theorem VarOrConst.mem_filterVars_of_var {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (l : List (VarOrConst sig)) (v : sig.V) : var v ∈ l → v ∈ filterVars l

If a variable is in a list of VarOrConst, then it occurs in filterVars.

theorem VarOrConst.filterConsts_occur_in_original_list {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (l : List (VarOrConst sig)) (c : sig.C) : c ∈ filterConsts l → const c ∈ l

Each member of filterConsts is in the original list (when applyign the const constructor again.)

theorem VarOrConst.mem_filterConsts_of_const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (l : List (VarOrConst sig)) (c : sig.C) : const c ∈ l → c ∈ filterConsts l

If a constant is in a list of VarOrConst, then it occurs in filterConsts.

theorem VarOrConst.skolemize_injective {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (ruleId i : Nat) (frontier : List sig.V) (s t : VarOrConst sig) : skolemize ruleId i frontier s = skolemize ruleId i frontier t → s = t

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

Ground Terms

A GroundTerm is a constant or a functional term with arbitrary nesting of function symbols (SkolemFS). Aiming to define GroundTerm, we need to define a more basic structure first, where we do not demand yet that function symbol arities are respected. PreGroundTerms need to be able to model Skolem terms, i.e. function terms. We can represent those conveniently using inductively defined FiniteTrees.

With PreGroundTerms in place, we merely define GroundTerms to be the PreGroundTerms where arity_ok holds. We then define appropriate constructors and recursion principles on the GroundTerm to make it behave almost like an inductive type with a const and func constructor.

@[reducible, inline]

abbrev PreGroundTerm (sig : Signature) [DecidableEq sig.C] [DecidableEq sig.V] : Type (max u_2 u_3)

The PreGroundTerm is simply a FiniteTree (SkolemFS sig) sig.C. That is a tree that features Skolem function symbols in its inner nodes and constants in its leaf nodes.

Equations

• PreGroundTerm sig = FiniteTree (SkolemFS sig) sig.C

@[irreducible]

def PreGroundTerm.arity_ok {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] : FiniteTree (SkolemFS sig) sig.C → Bool

The arity of a functional term is ok if the defined arity of its function symbol matches its number of children and arity_ok also holds for each child. For constants, i.e. the leaf nodes, the arity is trivially ok.

Equations

• One or more equations did not get rendered due to their size.
• PreGroundTerm.arity_ok (FiniteTree.leaf a) = true

@[reducible, inline]

abbrev GroundTerm (sig : Signature) [DecidableEq sig.C] [DecidableEq sig.V] : Type (max 0 u_3 u_2)

As mentioned above, a GroundTerm is simply a PreGroundTerm subtype where arity_ok holds.

Equations

• GroundTerm sig = { t : PreGroundTerm sig // PreGroundTerm.arity_ok t = true }

def GroundTerm.const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (c : sig.C) : GroundTerm sig

A GroundTerm can be direclty constructed from a constant.

Equations

• GroundTerm.const c = ⟨FiniteTree.leaf c, ⋯⟩

def GroundTerm.func {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (func : SkolemFS sig) (ts : List (GroundTerm sig)) (arity_ok : ts.length = func.arity) : GroundTerm sig

Also, a GroundTerm can be constructed from a SkolemFS and a list of GroundTerms as long as the length of the list matches the function symbol's arity.

Equations

• GroundTerm.func func ts arity_ok = ⟨FiniteTree.inner func ts.unattach, ⋯⟩

def GroundTerm.cases {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] {motive : GroundTerm sig → Sort u} (t : GroundTerm sig) (const : (c : sig.C) → motive (const c)) (func : (func : SkolemFS sig) → (ts : List (GroundTerm sig)) → (arity_ok : ts.length = func.arity) → motive (GroundTerm.func func ts arity_ok)) : motive t

We define a cases eliminator for the GroundTerm having a case for each constructor. This allows to use the cases tactic direcly on GroundTerms.

Equations

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

@[irreducible]

def GroundTerm.rec {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] {motive : GroundTerm sig → Sort u} (const : (c : sig.C) → motive (const c)) (func : (func : SkolemFS sig) → (ts : List (GroundTerm sig)) → (arity_ok : ts.length = func.arity) → ((t : GroundTerm sig) → t ∈ ts → motive t) → motive (GroundTerm.func func ts arity_ok)) (t : GroundTerm sig) : motive t

We define an induction eliminator for the GroundTerm having a case for each constructor. This allows to use the induction tactic direcly on GroundTerms.

Equations

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

def GroundTerm.toConst {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (t : GroundTerm sig) (isConst : ∃ (c : sig.C), t = const c) : sig.C

A GroundTerm that has been constructed from a constants can be converted into this constants again.

Equations

• t.toConst isConst = match eq : t.val with | FiniteTree.leaf c => c | FiniteTree.inner a a_1 => ⋯.elim

def GroundTerm.depth {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (t : GroundTerm sig) : Nat

The depth of a GroundTerm is the depth of the underlying FiniteTree, i.e. the deepest nesting of function symbols (+1).

Equations

• t.depth = FiniteTree.depth t.val

def GroundTerm.constants {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (t : GroundTerm sig) : List sig.C

The constants occurring in a GroundTerm are exactly the leaves of the underlying FiniteTree.

Equations

• t.constants = FiniteTree.leaves t.val

def GroundTerm.functions {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (t : GroundTerm sig) : List (SkolemFS sig)

The functions (i.e. function symbols SkolemFS) occurring in a GroundTerm are exactly the inner labels of the underlying FiniteTree.

Equations

• t.functions = FiniteTree.innerLabels t.val

theorem GroundTerm.depth_const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (c : sig.C) : (const c).depth = 1

Constants have depth 1.

theorem GroundTerm.depth_func {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (f : SkolemFS sig) (ts : List (GroundTerm sig)) (arity_ok : ts.length = f.arity) : (func f ts arity_ok).depth = 1 + (List.map depth ts).max?.getD 1

The depth of a function term is the maximum depth of its children + 1.

theorem GroundTerm.constants_const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (c : sig.C) : (const c).constants = [c]

The constants of a constant are the singleton list with the constant itself.

theorem GroundTerm.constants_func {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (f : SkolemFS sig) (ts : List (GroundTerm sig)) (arity_ok : ts.length = f.arity) : (func f ts arity_ok).constants = List.flatMap constants ts

The constants of a function term are the constants of its children.

theorem GroundTerm.functions_const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (c : sig.C) : (const c).functions = []

A constant has no functions.

theorem GroundTerm.functions_func {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (f : SkolemFS sig) (ts : List (GroundTerm sig)) (arity_ok : ts.length = f.arity) : (func f ts arity_ok).functions = f :: List.flatMap functions ts

The functions of a function term consist of the function symbol of the current term and the function symbols of all its children.