Multi-World Semantics and Inheritance¶
Abstract¶
This document formalizes the multi-world inheritance mechanism of Mistaber, where halachic traditions form a directed acyclic graph (DAG) with rule propagation from ancestor to descendant worlds. We define the active_in_world/2 predicate that determines rule visibility, formalize the override mechanism for tradition-specific modifications, and address the diamond inheritance problem arising when a world inherits from multiple parents with conflicting conclusions. We prove confluence of the inheritance system under well-founded priority orderings and establish decidability of machloket (dispute) detection.
1. Introduction¶
1.1 Motivation¶
Halachic traditions do not exist in isolation. The Shulchan Aruch provides a foundation; the Rema glosses it for Ashkenazi practice; later authorities like the Mishnah Berurah and Aruch HaShulchan refine these further. This creates a complex inheritance structure:
graph TD
base --> mechaber
base --> rema
base --> gra
mechaber --> sefardi_yo
rema --> ashk_mb
rema --> ashk_ah
gra --> ashk_ah
Note: ashk_ah inherits from both rema AND gra (diamond inheritance)
When ashk_mb queries a ruling, it should inherit from rema (and transitively from base) unless explicitly overridden. The diamond structure where ashk_ah inherits from both rema and gra (and thus has two paths to base) requires careful handling.
1.2 Contribution¶
We provide:
- Formal semantics for rule activation across world DAGs
- Override mechanism with conditional and unconditional modes
- Diamond inheritance conflict detection and resolution
- Confluence proofs ensuring deterministic outcomes
- Interpretation layer semantics for commentators within worlds
2. Preliminaries¶
2.1 World DAG Structure¶
Definition 2.1 (World DAG). The world structure ⟨𝑊, 𝐴⟩ is a DAG where: - 𝑊 is a finite set of worlds - 𝐴 ⊆ 𝑊 × 𝑊 is the accessibility (parent) relation - 𝐴 is acyclic: no path from any world to itself
Definition 2.2 (Ancestor Relation). The ancestor relation 𝐴⁺ is the transitive closure: $$w_1 𝐴^+ w_2 \text{ iff } ∃w_0, ..., w_n: w_1 = w_0 𝐴 w_1 ... 𝐴 w_n = w_2$$
Definition 2.3 (Root World). A world 𝑤 is a root iff it has no parents: $$root(w) \text{ iff } ¬∃w': w 𝐴 w'$$
In Mistaber, base is the unique root representing Shulchan Aruch common ground.
2.2 Rules and Scoping¶
Definition 2.4 (Rule). A rule 𝑟 is a tuple: $$r = ⟨id, body, head, madrega, makor, scope⟩$$
where:
- id: Unique rule identifier
- body: Preconditions for rule firing
- head: Conclusion when rule fires
- madrega: Normative level (d_oraita, d_rabanan, etc.)
- makor: Source citations
- scope: World(s) where rule is defined
Definition 2.5 (Rule Scope). A rule 𝑟 is scoped to world 𝑤: $$scoped(r, w) \text{ iff } scope(r, w)$$
The scope predicate indicates where a rule is defined, not necessarily where it applies (which includes descendants).
3. Rule Activation Semantics¶
3.1 Active-In-World Relation¶
Definition 3.1 (Active-In-World). Rule 𝑟 is active in world 𝑤: $$active_in_world(r, w) \text{ iff }$$ $$\quad (scoped(r, w) ∧ ¬overridden_in(r, w))$$ $$\quad ∨ (∃w': w 𝐴^+ w' ∧ scoped(r, w') ∧ ¬overridden_in(r, w))$$
In prose: A rule is active in a world if either: 1. The rule is directly scoped to that world and not overridden, or 2. The rule is scoped to an ancestor and not overridden in the descendant
Theorem 3.1 (Activation Monotonicity). If a rule is active in a world and not overridden in any descendant path, it remains active: $$active_in_world(r, w) ∧ w' 𝐴^+ w ∧ ¬overridden_in(r, w') → active_in_world(r, w')$$
Proof. By Definition 3.1, if active_in_world(r, w) and w' A⁺ w, then w' is an ancestor of some world where r is scoped. Since ¬overridden_in(r, w'), the second disjunct of Definition 3.1 applies. □
3.2 ASP Implementation¶
File: mistaber/engine/priorities.lp
% Direct activation
active_in_world(R, W) :-
rule(R),
world(W),
scope(R, W),
not overridden_in(R, W).
% Inherited activation
active_in_world(R, W) :-
rule(R),
world(W),
scope(R, W_ancestor),
ancestor(W, W_ancestor),
not overridden_in(R, W).
4. Override Mechanism¶
4.1 Override Types¶
Definition 4.1 (Override). An override is a tuple: $$override = ⟨r_{child}, r_{parent}, w, type⟩$$
where:
- r_child: The overriding rule
- r_parent: The overridden rule
- w: World where override applies
- type: Override mode (unconditional or conditional)
Definition 4.2 (Override Types).
- Unconditional (always): Override applies whenever the child rule is in scope
- Conditional (condition(C)): Override applies only when condition C holds
4.2 Override Application¶
Definition 4.3 (Override Applies). $$override_applies(r_c, r_p, w, always) \text{ iff } overrides(r_c, r_p, w, always)$$ $$override_applies(r_c, r_p, w, condition(C)) \text{ iff } overrides(r_c, r_p, w, condition(C)) ∧ holds(C)$$
Definition 4.4 (Overridden-In). $$overridden_in(r, w) \text{ iff } ∃r', t: overrides(r', r, w, t) ∧ active_override(r', r, w, t)$$
Definition 4.5 (Active Override). An override is active if the overriding rule is in scope: $$active_override(r_c, r_p, w, t) \text{ iff }$$ $$\quad (scoped(r_c, w) ∧ override_applies(r_c, r_p, w, t))$$ $$\quad ∨ (∃w': w 𝐴^+ w' ∧ scoped(r_c, w') ∧ override_applies(r_c, r_p, w, t))$$
4.3 Override Semantics Example¶
Example 4.1 (Fish and Dairy). The Mechaber rules fish with dairy is forbidden due to sakana. The Rema overrides this:
% Mechaber's rule
rule(r_bb_dag_sakana).
scope(r_bb_dag_sakana, mechaber).
asserts(mechaber, sakana(M)) :- is_dag_chalav_mixture(M).
% Rema's override
rule(r_rema_dag_chalav_mutar).
scope(r_rema_dag_chalav_mutar, rema).
override(rema, sakana(M), no_sakana) :- is_dag_chalav_mixture(M).
In world rema and its descendants (ashk_mb, ashk_ah):
- overridden(sakana(M), rema) holds for dag+chalav mixtures
- holds(sakana(M), rema) is false
In world mechaber and its descendants (sefardi_yo):
- The override does not apply (different inheritance path)
- holds(sakana(M), mechaber) is true
5. Diamond Inheritance¶
5.1 The Diamond Problem¶
Definition 5.1 (Diamond Inheritance). A world 𝑤 exhibits diamond inheritance iff: $$∃w_1, w_2, w_0: w 𝐴 w_1 ∧ w 𝐴 w_2 ∧ w_1 ≠ w_2 ∧ w_1 𝐴^+ w_0 ∧ w_2 𝐴^+ w_0$$
Definition 5.2 (Diamond Conflict). A diamond conflict on topic T in world 𝑤: $$conflict(w, topic(T)) \text{ iff }$$ $$\quad ∃w_1, w_2, r_1, r_2, v_1, v_2:$$ $$\quad\quad w 𝐴 w_1 ∧ w 𝐴 w_2 ∧ w_1 ≠ w_2$$ $$\quad\quad ∧ active_in_world(r_1, w_1) ∧ active_in_world(r_2, w_2)$$ $$\quad\quad ∧ rule_concludes(r_1, position(T, v_1))$$ $$\quad\quad ∧ rule_concludes(r_2, position(T, v_2))$$ $$\quad\quad ∧ v_1 ≠ v_2$$ $$\quad\quad ∧ ¬priority(w_1, w_2, w) ∧ ¬priority(w_2, w_1, w)$$
5.2 Conflict Detection¶
Theorem 5.1 (Conflict Detection Decidability). Detecting diamond conflicts is decidable in polynomial time.
Proof. Given the finite world DAG and finite rule set: 1. For each world 𝑤 with multiple parents, enumerate parent pairs (O(|𝑊|²)) 2. For each pair, compute active rules via fixpoint (O(|Rules| × |𝑊|)) 3. Check conclusion compatibility (O(|Rules|²))
Total: O(|𝑊|² × |Rules|² × |𝑊|) = polynomial. □
5.3 Conflict Resolution via Priority¶
Definition 5.3 (Priority Relation). The predicate priority(w₁, w₂, w) declares that in world 𝑤, tradition 𝑤₁ takes precedence over 𝑤₂.
Definition 5.4 (Resolution). A diamond conflict on topic T in world 𝑤 is resolved iff: $$has_resolution(w, topic(T)) \text{ iff } ∃w_1, w_2: priority(w_1, w_2, w) ∨ priority(w_2, w_1, w)$$
Definition 5.5 (Priority Winner). When priority is declared: $$priority_winner(r, w) \text{ iff }$$ $$\quad ∃w_{pref}, w_{less}, T:$$ $$\quad\quad priority(w_{pref}, w_{less}, w)$$ $$\quad\quad ∧ active_in_world(r, w_{pref})$$ $$\quad\quad ∧ rule_concludes(r, position(T, _))$$
5.4 ASP Implementation¶
% Conflict detection
conflict(W, topic(Topic)) :-
world(W), world(W1), world(W2),
accessible(W, W1), accessible(W, W2),
W1 != W2,
active_in_world(R1, W1), active_in_world(R2, W2),
rule_concludes(R1, position(Topic, Val1)),
rule_concludes(R2, position(Topic, Val2)),
Val1 != Val2,
not priority(W1, W2, W),
not priority(W2, W1, W).
% Resolution via priority
has_resolution(W, topic(Topic)) :-
world(W), world(W1), world(W2),
accessible(W, W1), accessible(W, W2),
W1 != W2,
active_in_world(R1, W1), active_in_world(R2, W2),
rule_concludes(R1, position(Topic, _)),
rule_concludes(R2, position(Topic, _)),
priority(W1, W2, W).
6. Confluence Properties¶
6.1 Confluence Definition¶
Definition 6.1 (Confluence). The inheritance system is confluent iff for any world 𝑤 and proposition φ: - If φ is derivable via multiple inheritance paths, all paths yield the same result - Or an unresolved conflict is explicitly marked
6.2 Confluence Theorem¶
Theorem 6.1 (System Confluence). The Mistaber inheritance system is confluent under the following conditions: 1. The world graph is a DAG (no cycles) 2. Override relations are consistent (no override cycles) 3. Diamond conflicts either have declared priorities or are marked as machloket
Proof. We prove by structural induction on the world DAG height.
Base case (root): The root world base has no parents, so no inheritance conflicts are possible. Conclusions derive only from rules scoped directly to base. ✓
Inductive step: Assume confluence for all worlds of height < k. Consider world 𝑤 of height k.
Case 1: Single parent. 𝑤 has exactly one parent 𝑤'. By induction, 𝑤' is confluent. Rules in 𝑤 either: - Are scoped to 𝑤: Conclusions are deterministic - Are inherited from 𝑤': By confluence of 𝑤', inherited conclusions are deterministic - Are overridden in 𝑤: Override semantics are deterministic
Case 2: Multiple parents (potential diamond). Let 𝑤 have parents 𝑤₁, ..., 𝑤ₙ. For any topic T:
- If all parents agree on T: Inheritance is consistent
- If parents disagree on T:
- If priority(𝑤ᵢ, 𝑤ⱼ, 𝑤) is declared: Winner is deterministic
- Otherwise: conflict(w, topic(T)) is derived, marking the machloket
In all cases, the result is deterministic. □
6.3 Confluence Corollary¶
Corollary 6.1 (Deterministic Query Answers). For any query Q in world 𝑤: $$∀Q, w: |answers(Q, w)| ≤ 1 \text{ (excluding explicit machloket markers)}$$
Proof. Direct consequence of Theorem 6.1. Each query either yields: - A unique answer (confluent derivation) - A machloket marker (conflict detected) - No answer (insufficient information) □
7. Interpretation Layer¶
7.1 Commentators vs. Worlds¶
Mistaber distinguishes between: - Worlds: Major traditions that form the inheritance DAG - Commentators: Authorities who interpret within a world
Definition 7.1 (Commentator). A commentator is an authority who: - Operates within a world (not creating a new world) - Provides interpretations that modify rule conditions - Has precedence relative to other commentators
7.2 Interpretation Types¶
Definition 7.2 (Interpretation). An interpretation modifies a rule's application:
| Type | Effect | Example |
|---|---|---|
adds_condition(C) |
Rule requires additional condition C | Shach requiring cooking |
removes_condition(C) |
Rule no longer requires condition C | Taz removing restriction |
restricts_to(S) |
Rule applies only to scope S | Limiting to specific foods |
expands_to(S) |
Rule applies beyond original scope | Including additional cases |
7.3 Interpretation Precedence¶
Definition 7.3 (Interpretation Precedence). Within a world, commentators have precedence: $$interpretation_precedence(authority, commentator, rank)$$
Higher rank wins in conflicts.
Definition 7.4 (Superseded Interpretation). An interpretation is superseded if a higher-precedence commentator conflicts: $$superseded(auth, rule, comm_1) \text{ iff }$$ $$\quad ∃comm_2, I_1, I_2: interpretation(comm_1, rule, I_1) ∧ interpretation(comm_2, rule, I_2)$$ $$\quad ∧ comm_1 ≠ comm_2 ∧ conflicts(I_1, I_2)$$ $$\quad ∧ precedence(auth, comm_1) < precedence(auth, comm_2)$$
7.4 Effective Interpretation¶
Definition 7.5 (Effective Interpretation). The interpretation that applies after precedence resolution: $$effective_interpretation(auth, rule, interp) \text{ iff }$$ $$\quad interpretation(comm, rule, interp) ∧ interprets(comm, auth)$$ $$\quad ∧ ¬superseded(auth, rule, comm)$$
7.5 ASP Implementation¶
File: mistaber/engine/interpretations.lp
% Commentator declarations
commentator(shach).
commentator(taz).
interprets(shach, mechaber).
interprets(taz, mechaber).
% Interpretation types
interpretation(Comm, Rule, adds_condition(Cond)) :-
adds_condition(Comm, Rule, Cond).
% Precedence system
interpretation_precedence(mechaber, shach, 2).
interpretation_precedence(mechaber, taz, 1).
% Conflict detection
conflicts(adds_condition(C), removes_condition(C)).
conflicts(removes_condition(C), adds_condition(C)).
% Effective interpretation
effective_interpretation(Authority, Rule, Interp) :-
interpretation(Comm, Rule, Interp),
interprets(Comm, Authority),
not superseded_interpretation(Authority, Rule, Comm).
8. Derivation Semantics¶
8.1 Conclusion Derivation¶
Definition 8.1 (Derives). World 𝑤 derives conclusion C: $$derives(w, C) \text{ iff } ∃r: active_in_world(r, w) ∧ rule_concludes(r, C) ∧ conditions_met(r)$$
8.2 Derivation with Interpretation¶
When interpretations apply: $$derives(w, C) \text{ iff } ∃r: active_in_world(r, w) ∧ rule_concludes(r, C)$$ $$\quad ∧ (conditions_met(r) ∧ interpretation_conditions_met(w, r))$$
where: $$interpretation_conditions_met(w, r) \text{ iff }$$ $$\quad ∀I: effective_interpretation(w, r, adds_condition(I)) → holds(I, w)$$
8.3 ASP Implementation¶
% Direct derivation
derives(W, Conclusion) :-
world(W),
active_in_world(R, W),
rule_concludes(R, Conclusion),
rule_conditions_met(R).
% Derivation in specific world
derives_in_world(W, Conclusion) :-
world(W),
active_in_world(R, W),
rule_concludes(R, Conclusion).
9. Implementation Notes¶
9.1 World Declarations¶
File: mistaber/ontology/worlds/base.lp
File: mistaber/ontology/worlds/rema.lp
9.2 Kripke Rules¶
File: mistaber/ontology/worlds/kripke_rules.lp
% Truth propagation
holds(Prop, W) :- asserts(W, Prop), world(W).
holds(Prop, W_child) :-
accessible(W_child, W_parent),
holds(Prop, W_parent),
not overridden(Prop, W_child).
% Override mechanism
overridden(Prop, W) :- override(W, Prop, _).
% Transitive accessibility
accessible_transitive(W1, W2) :- accessible(W1, W2).
accessible_transitive(W1, W3) :-
accessible(W1, W2),
accessible_transitive(W2, W3).
9.3 Priority Rules¶
File: mistaber/engine/priorities.lp
% Ancestor relation
ancestor(W_child, W_parent) :-
world(W_child), world(W_parent),
accessible(W_child, W_parent).
ancestor(W1, W3) :-
world(W1), world(W3),
accessible(W1, W2),
ancestor(W2, W3).
10. Worked Example¶
10.1 Fish and Dairy Across Traditions¶
Consider querying whether eating fish with cheese is permitted.
World Structure:
graph LR
base --> mechaber --> sefardi_yo
base --> rema --> ashk_mb
rema --> ashk_ah
Rules:
- r_bb_dag_sakana (mechaber): Fish+dairy is sakana (forbidden)
- r_rema_dag_chalav_mutar (rema): Fish+dairy is permitted
Query in ashk_mb:
1. Check rules scoped to ashk_mb: None specific to fish+dairy
2. Check inherited from rema: r_rema_dag_chalav_mutar is active
3. Check if overridden: No override in ashk_mb
4. Result: permitted(achiila, fish_cheese_mixture)
Query in sefardi_yo:
1. Check rules scoped to sefardi_yo: None specific
2. Check inherited from mechaber: r_bb_dag_sakana is active
3. Check if overridden: No override (rema's override not in inheritance path)
4. Result: forbidden(achiila, fish_cheese_mixture, sakana)
References¶
- Brewka, G. (1996). Well-Founded Semantics for Extended Logic Programs with Dynamic Preferences. Journal of Artificial Intelligence Research, 4, 19-36.
- Delgrande, J.P., & Schaub, T. (2003). On the Relation Between Reiter's Default Logic and its (Major) Variants. Proceedings of JELIA 2002, 452-463.
- Gelfond, M., & Lifschitz, V. (1991). Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9(3-4), 365-385.
- Lifschitz, V. (2008). What is Answer Set Programming? Proceedings of AAAI 2008, 1594-1597.