Cores

In this file, we define cores of fact sets. Namely, we define FactSet.isWeakCore and FactSet.isStrongCore. FactSets that are models and cores are interesting since there are (intuitively speaking) the smallest possible models. Under certain condition, the chase is able to produce a core directly, which is very desirable since the result of the chase is also always a universal model. But this is discussed in other files. Here, we are only concerned with the definition of cores on FactSets and some of their properties.

Strong GroundTermMappings (and Homomorphisms)

Intuitively, a homomorphism is strong if it not only retains membership but also non-membership. We define being strong as a standalone property for GroundTermMappings without requiring any additional properties for the underlying GroundTermMapping.

def GroundTermMapping.strong {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (h : GroundTermMapping sig) (domain : Set (GroundTerm sig)) (A B : FactSet sig) : Prop

A GroundTermMapping is strong for FactSets $A$ and $B$ if each element not in $A$, its mapping is not in $B$. However, we only demand this for elements that only feature terms from a given domain because we do not want to care about the mapping of terms outside the domain.

Equations

• h.strong domain A B = ∀ (e : Fact sig), (∀ (t : GroundTerm sig), t ∈ e.terms → t ∈ domain) → ¬e ∈ A → ¬h.applyFact e ∈ B

theorem GroundTermMapping.strong_of_compose_strong {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (g h : GroundTermMapping sig) (domain : Set (GroundTerm sig)) (A B C : FactSet sig) : h.isHomomorphism B C → strong (h ∘ g) domain A C → g.strong domain A B

If the composition of two mappings is strong from $A$ to $C$ and the second mapping is a homomorphism from $B$ to $C$, then the first mapping is strong from $A$ to $B$.

Repetition of GroundTermMappings (and Homomorphisms)

Since homomorphisms are functions over terms, we can repeat them. Here, we show some nice properties of repeated homomorphisms and endomorphisms in particular. For example, we prove that a repeated endomorphisms is again an endomorphisms.

theorem GroundTermMapping.repeat_id_on_const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] {h : GroundTermMapping sig} (idOnConst : h.isIdOnConstants) (i : Nat) : isIdOnConstants (Function.repeat_fun h i)

Repeating a mapping retains the GroundTermMapping.isIdOnConstants property.

theorem GroundTermMapping.repeat_isHomomorphism {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {h : GroundTermMapping sig} {fs : FactSet sig} (hom : h.isHomomorphism fs fs) (i : Nat) : isHomomorphism (Function.repeat_fun h i) fs fs

Repeating a mapping retains the GroundTermMapping.isHomomorphism property at least for endomorphisms.

Cores Definitions and some of their Properties

Here, we finally define isWeakCore and isStrongCore and show some of their relations and additional properties. This also involves some more theorems about homomorphisms.

def FactSet.isWeakCore {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) : Prop

A FactSet is a weak core if every endomorphisms on the fact set is strong and injective.

Equations

• fs.isWeakCore = ∀ (h : GroundTermMapping sig), h.isHomomorphism fs fs → h.strong fs.terms fs fs ∧ Function.injectiveSet h fs.terms

def FactSet.isStrongCore {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) : Prop

A FactSet is a strong core if every endomorphisms on the fact set is strong, injective, and surjective. (By definition, every strong core is a weak core.)

Equations

• fs.isStrongCore = ∀ (h : GroundTermMapping sig), h.isHomomorphism fs fs → h.strong fs.terms fs fs ∧ Function.injectiveSet h fs.terms ∧ Function.surjectiveSet h fs.terms fs.terms

def FactSet.homSubset {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (c fs : FactSet sig) : Prop

We say that a fact set $C$ is a homomorphic subset of another fact set $F$ if $C$ is a subset of $F$ and there is a homomorphism from $F$ to $C$.

Equations

• c.homSubset fs = (c ⊆ fs ∧ ∃ (h : GroundTermMapping sig), h.isHomomorphism fs c)

theorem FactSet.hom_surjective_of_finite_of_injective {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (finite : Set.finite fs) (h : GroundTermMapping sig) : h.isHomomorphism fs fs → Function.injectiveSet h fs.terms → Function.surjectiveSet h fs.terms fs.terms

For a homomorphism on a finite fact set, injectivity implies surjectivity.

theorem FactSet.hom_strong_of_finite_of_injective {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (finite : Set.finite fs) (h : GroundTermMapping sig) : h.isHomomorphism fs fs → Function.injectiveSet h fs.terms → h.strong fs.terms fs fs

For a homomorphism on a finite fact set, injectivity implies that the homomorphisms is also strong.

theorem FactSet.isStrongCore_of_isWeakCore_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (weakCore : fs.isWeakCore) (finite : Set.finite fs) : fs.isStrongCore

For finite fact sets, isWeakCore implies isStrongCore. That means that isWeakCore and isStrongCore are equivalent on finite fact sets.

theorem FactSet.every_weakCore_isomorphic_to_strongCore_of_hom_both_ways {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (sc : FactSet sig) (sc_strong : sc.isStrongCore) (wc : FactSet sig) (wc_weak : wc.isWeakCore) (h_sc_wc h_wc_sc : GroundTermMapping sig) (h_sc_wc_hom : h_sc_wc.isHomomorphism sc wc) (h_wc_sc_hom : h_wc_sc.isHomomorphism wc sc) : ∃ (iso : GroundTermMapping sig), iso.isHomomorphism wc sc ∧ iso.strong wc.terms wc sc ∧ Function.injectiveSet iso wc.terms ∧ Function.surjectiveSet iso wc.terms sc.terms

Given two fact sets A,B of which one is a weak and one is a strong core, if there are homomorphisms from A to B and B to A, then there exists an isomorphism from A to B, i.e. a strong homomorphisms that is injective and surjective.

theorem FactSet.strongCore_unique_up_to_isomorphism_with_respect_to_weak_cores {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs sc : FactSet sig) (sub_sc : sc.homSubset fs) (sc_strong : sc.isStrongCore) (wc : FactSet sig) (sub_wc : wc.homSubset fs) (wc_weak : wc.isWeakCore) : ∃ (iso : GroundTermMapping sig), iso.isHomomorphism wc sc ∧ iso.strong wc.terms wc sc ∧ Function.injectiveSet iso wc.terms ∧ Function.surjectiveSet iso wc.terms sc.terms

Strong cores of fact sets are unique up to isomorphism. That is, consider a fact set $F$. A strong core $C$ for $F$ is a strong core that is also a homomorphic subset of $F$. Now every (other) homomorphic subset $C'$ of $F$ that is at least a weak core has an isomorphism into $C$.

theorem FactSet.every_universal_weakCore_isomorphic_to_universal_strongCore {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} (sc : FactSet sig) (sc_universal : sc.universallyModelsKb kb) (sc_strong : sc.isStrongCore) (wc : FactSet sig) (wc_universal : wc.universallyModelsKb kb) (wc_weak : wc.isWeakCore) : ∃ (iso : GroundTermMapping sig), iso.isHomomorphism wc sc ∧ iso.strong wc.terms wc sc ∧ Function.injectiveSet iso wc.terms ∧ Function.surjectiveSet iso wc.terms sc.terms

Consider a KnowledgeBase and a universal model of the KB that is a strong core. Then every (other) universal model that is at least a weak core, is isomorphism to the strong core.

theorem FactSet.strong_core_of_model_is_model {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} (fs : FactSet sig) (fs_model : fs.modelsKb kb) (sc : FactSet sig) (sc_sub : sc.homSubset fs) (sc_strong : sc.isStrongCore) : sc.modelsKb kb

Given a model of a KnowledgeBase, every strong core of the model is also a model. In general, this does not hold for weak cores (in the infinite setting).

theorem FactSet.strong_core_of_universal_model_is_universal_model {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} (fs : FactSet sig) (fs_univ_model : fs.universallyModelsKb kb) (sc : FactSet sig) (sc_sub : sc.homSubset fs) (sc_strong : sc.isStrongCore) : sc.universallyModelsKb kb

Building on top of the previous theorem, a strong core of a universal model is not only a model but also universal.