The tension between the Open World Assumption (OWA) and Closed World Assumption (CWA) represents one of the fundamental philosophical and practical divides in knowledge representation. OWL (Web Ontology Language) embraces OWA, treating absence of information as unknown rather than false. SHACL (Shapes Constraint Language), conversely, validates data under CWA, where what is not explicitly stated is considered false. This article explores how dependent type theory, specifically Agda, can model both approaches and potentially bridge this conceptual gap.
Open World Assumption (OWA)
Under OWA, the world is inherently incomplete. If we cannot prove a statement is true, we cannot conclude it is false — it remains unknown. This assumption aligns with the reality of distributed, evolving knowledge systems where information is constantly being discovered and added.
Example: If we have no statement that “Alice knows Bob,” we cannot conclude Alice does not know Bob. The information is simply absent.
Closed World Assumption (CWA)
Under CWA, what is not known to be true is considered false. This assumption works well for validation, databases, and bounded domains where we have complete information.
Example: If our database has no record of “Alice knows Bob,” we can definitively say this relationship does not exist in our system.
OWL and the Open World
OWL’s reasoning is built on description logic, which operates under OWA. This has profound implications:
:Alice a :Person . :Bob a :Person .
\# Ontology constraint :Person owl:equivalentClass \[ a owl:Restriction ; owl:onProperty :hasParent ; owl:minCardinality 2 \] .
In this example, even though we haven’t stated Alice’s parents, an OWL reasoner will not conclude Alice violates the constraint. The information about Alice’s parents is simply unknown — she might have parents that haven’t been stated yet.
SHACL and the Closed World
SHACL validates RDF graphs under CWA, making it perfect for data quality checking:
\# SHACL Shape :PersonShape a sh:NodeShape ; sh:targetClass :Person ; sh:property \[ sh:path :hasParent ; sh:minCount 2 ; sh:message "A person must have at least 2 parents declared" \] .
When validating Alice’s data against this shape, SHACL will report a violation because only the stated parents are considered — absence means nonexistence.
Modeling in Agda: Type-Theoretic Foundations
Agda’s dependent types provide a rigorous foundation for modeling both assumptions. The key insight is that OWA corresponds to intuitionistic logic (where absence of proof ≠ proof of absence), while CWA corresponds to classical logic with decidability.
Core Definitions
module WorldAssumptions where
open import Data.Bool using (Bool; true; false) open import Data.Maybe using (Maybe; just; nothing) open import Data.Nat using (ℕ; zero; suc; \+\; \≤\) open import Relation.Nullary using (¬\; Dec; yes; no) open import Relation.Binary.PropositionalEquality using (\≡\; refl)\-- A universe of entities postulate Entity : Set\-- Properties as relations between entities postulate Property : Entity → Entity → Set
Open World Assumption: OWL-like Agda
In the open world, we model knowledge as what we can prove, not what we can disprove:
module OpenWorld where open import Data.List using (List; \[\]; \∷\; any) open import Data.Product using (\×\; ∃; \,\; proj₁; proj₂)
record KnowledgeBase : Set₁ where field facts : List (∃ λ (subject : Entity) → ∃ λ (object : Entity) → Property subject object)
data OWAValue : Set where known-true : OWAValue known-false : OWAValue unknown : OWAValue
query : KnowledgeBase → Entity → Entity → Property → OWAValue query kb subject object prop = if any (matches subject object prop) (KnowledgeBase.facts kb) then known-true else unknown
record OntologyClass : Set₁ where field name : String
necessaryConditions : Entity → Set
checkSatisfiable : (e : Entity) → (kb : KnowledgeBase) → Maybe (necessaryConditions e)
Person : OntologyClass Person = record { name = "Person" ; necessaryConditions = λ e → ∃ λ (p1 : Entity) → ∃ λ (p2 : Entity) → (Property e p1 × Property e p2 × ¬ (p1 ≡ p2)) ; checkSatisfiable = λ e kb →
findParents e kb }
deriveNewFacts : KnowledgeBase → List Inference → KnowledgeBase deriveNewFacts kb rules =
applyInferences kb rules
data QueryResult : Set where definitely-true : QueryResult definitely-false : QueryResult insufficient-data : QueryResult
openWorldQuery : KnowledgeBase → Entity → Property → Entity → QueryResult openWorldQuery kb subj prop obj = case lookup kb subj prop obj of found-true → definitely-true found-false → definitely-false not\-found → insufficient-data
Closed World Assumption: SHACL-like Agda
In the closed world, we can definitively determine truth values based on what’s present:
module ClosedWorld where open import Data.List using (List; \[\]; \∷\; length; filter) open import Data.Nat using (ℕ; \≤?\) open import Data.Product using (\×\; ∃; \,\) open import Relation.Nullary using (Dec; yes; no)
record DataGraph : Set₁ where field entities : List Entity triples : List (Entity × Property × Entity)
complete : Bool
data CWAValue : Set where true : CWAValue false : CWAValue
query : DataGraph → Entity → Property → Entity → CWAValue query dg subject prop object = if (subject , prop , object) ∈ DataGraph.triples dg then true else false
record Shape : Set₁ where field targetClass : Entity → Bool
constraints : List (Entity → DataGraph → Bool)
data ValidationResult : Set where conforms : ValidationResult violates : List String → ValidationResult
PersonShape : Shape PersonShape = record { targetClass = isPersonClass ; constraints = hasMinParents 2 ∷ \[\] } where hasMinParents : ℕ → Entity → DataGraph → Bool hasMinParents n entity dg = let parents = countParents entity dg in n ≤? parents
countParents : Entity → DataGraph → ℕ countParents entity dg = length (filter (isParentTriple entity) (DataGraph.triples dg))
validate : DataGraph → Shape → Entity → ValidationResult validate dg shape entity = if all (λ constraint → constraint entity dg) (Shape.constraints shape) then conforms else violates (collectErrors dg shape entity)
isValid : DataGraph → Shape → Entity → Dec (ValidationResult ≡ conforms) isValid dg shape entity = case validate dg shape entity of conforms → yes refl violates \ → no (λ ())
Bridging the Gap: Hybrid Approach
The most powerful approach combines both paradigms:
module HybridWorld where open OpenWorld using (KnowledgeBase; OWAValue) open ClosedWorld using (DataGraph; ValidationResult)
record HybridKnowledgeSystem : Set₁ where field
ontology : KnowledgeBase inferenceRules : List InferenceRule
instanceData : DataGraph validationShapes : List Shape
enrichData : DataGraph → KnowledgeBase → DataGraph
validateWithReasoning : HybridKnowledgeSystem → Entity → ValidationResult validateWithReasoning hks entity \= let enrichedData \= HybridKnowledgeSystem.enrichData hks (HybridKnowledgeSystem.instanceData hks) (HybridKnowledgeSystem.ontology hks) in ClosedWorld.validate enrichedData shape entity where shape \= head (HybridKnowledgeSystem.validationShapes hks)
inferThenValidate : KnowledgeBase → DataGraph → Shape → Entity → ValidationResult inferThenValidate onto data shape entity \=
let derived \= deriveFromOntology onto data
complete \= mergeInferred data derived
in ClosedWorld.validate complete shape entity
Practical Example: Family Relationships
Let’s model a concrete example with both approaches:
module FamilyExample where open import Data.String using (String)
\-- Entities postulate alice bob charlie diana : Entity
\-- Properties postulate hasParent : Property hasSibling : Property
\-- OWL-like ontology (OWA) familyOntology : OpenWorld.KnowledgeBase familyOntology \= record { facts \= (alice , (bob , hasParent)) ∷ (alice , (charlie , hasParent)) ∷ \[\] }
\-- Question: Does Diana have parents? queryDiana : OpenWorld.OWAValue queryDiana \= OpenWorld.query familyOntology diana anyEntity hasParent \-- Result: unknown (not false!)
\-- SHACL-like validation (CWA) familyData : ClosedWorld.DataGraph familyData \= record { entities \= alice ∷ bob ∷ charlie ∷ diana ∷ \[\] ; triples \= (alice , hasParent , bob) ∷ (alice , hasParent , charlie) ∷ \[\] ; complete \= true }
personShape : ClosedWorld.Shape personShape \= record { targetClass \= λ \_ → true ; constraints \= requiresExactlyTwoParents ∷ \[\] }
\-- Validation: Does Diana conform? validateDiana : ClosedWorld.ValidationResult validateDiana \= ClosedWorld.validate familyData personShape diana \-- Result: violates \["Diana has 0 parents, requires 2"\]
\-- Key difference: \-- \- OWA: "We don't know if Diana has parents" (unknown) \-- \- CWA: "Diana does NOT have parents" (false/violation)
Advanced: Dependent Types for Schema Evolution
One powerful application of this approach is modeling schema evolution:
module SchemaEvolution where
record EvolvingSchema (version : ℕ) : Set₁ where field classes : List OntologyClass
backwardCompatible : (v : ℕ) → v ≤ version → KnowledgeBase → Maybe ValidationResult
record ValidationSnapshot (version : ℕ) : Set₁ where field frozenSchema : EvolvingSchema version dataAtVersion : DataGraph
mustConform : ClosedWorld.validate dataAtVersion shapes entities ≡ conforms
Type-Theoretic Insights
OWA as Intuitionistic Logic
The OWA naturally corresponds to intuitionistic/constructive logic, where:
data Proof (P : Set) : Set where evidence : P → Proof P
\-- But absence of proof is not proof of absence \-- ¬ (Proof P) does NOT imply Proof (¬ P)\-- In Agda, this is natural: openWorldNegation : {P : Set} → ¬ (Proof P) → Proof (¬ P) openWorldNegation absence = {!!} -- Cannot be constructed!
CWA as Classical Logic with LEM
The CWA essentially adds the Law of Excluded Middle:
postulate closed\-world\-LEM : (P : Set) → Dec P
\-- This allows definitive validation closedWorldNegation : {P : Set} → ¬ (Proof P) → Proof (¬ P) closedWorldNegation {P} absence = case closed-world-LEM P of yes p → absurd (absence (evidence p)) no ¬p → evidence ¬p
Modal Logic Perspective
We can also model the distinction using modal operators:
module ModalPerspective where -- □P = "necessarily P" = proven in ontology (OWA) -- ◇P = "possibly P" = not contradicted (OWA) -- P = "actually P" = present in data (CWA)
record ModalKnowledge : Set₁ where field necessary : Entity → Property → Entity → Set -- □ possible : Entity → Property → Entity → Set -- ◇ actual : Entity → Property → Entity → Bool -- P (decidable)
-- Modal axioms necessary-implies-actual : ∀ {s p o} → necessary s p o → actual s p o ≡ true actual\-implies-possible : ∀ {s p o} → actual s p o ≡ true → possible s p o
Practical Implications
When to Use OWA (OWL-like)
Integrating data from multiple sources Evolving schemas over time Reasoning with incomplete information Ontology development and knowledge discovery Semantic web and linked data scenarios
When to Use CWA (SHACL-like)
Data quality validation Database integrity constraints API response validation Form validation and user input Compliance checking with fixed rules
When to Use Hybrid
Validate user input (CWA) against a rich domain model (OWA) Enrich incomplete data with inferred facts before validation Progressive validation: warn vs. error Multi-stage pipelines: reason (OWA) then validate (CWA)
Conclusion
Modeling OWL’s OWA and SHACL’s CWA in Agda reveals the deep logical and type-theoretic foundations of these approaches. OWA corresponds to intuitionistic logic and proof theory, while CWA assumes decidability and classical reasoning. By implementing both in dependent types, we gain:
- Formal precision: Exact specifications of what each assumption means
- Composability: Ability to mix both approaches as needed
- Correctness: Type-checked guarantees about reasoning soundness
- Clarity: Explicit about what we know vs. what we assume
The future of knowledge representation may lie not in choosing one assumption over the other, but in understanding when each applies and how to bridge between them. Dependent type theory provides the rigorous foundation to make this bridge formal, safe, and practical.
To read more :
https://leanpub.com/dependenttypesdttlogicholforaiagentreadyknowledgegraphs