# Implementation in Python of the basic narrowing operations described in
# https://en.wikipedia.org/wiki/Narrowing_of_algebraic_value_sets
# SPDX-FileCopyrightText: Chris Pressey, the creator of this work, has dedicated it to the public domain.
# For more information, please refer to <https://unlicense.org/>
# SPDX-License-Identifier: Unlicense
from typing import Set, Callable, Dict, Any, Optional, Tuple, FrozenSet, Union, Iterable
from dataclasses import dataclass, field
import unittest
@dataclass(frozen=True, eq=True, order=True)
class WorldPoint:
variable: str
index: int
def __repr__(self):
return f"⟪{self.variable}_{self.index}⟫"
class World:
def __init__(self, variable: str, index: int):
self._points = frozenset([WorldPoint(variable, index)])
@classmethod
def from_set(cls, s):
instance = cls("*", 0)
instance._points = frozenset(s)
return instance
@classmethod
def empty(cls):
return cls.from_set({})
def __repr__(self):
return f"World({self._points})"
def __hash__(self):
# This makes this frozen like _points is frozen
return hash(self._points)
def __eq__(self, other):
if isinstance(other, World):
return self._points == other._points
return False
def __and__(self, other):
if not isinstance(other, World):
return NotImplemented
# A bit strangely perhaps, when we take the intersection of a World
# with another World, the result is the union of their WorldPoints.
# First, take out any values from other that are already in self.
# This accounts for union being idempotent.
incoming_points = other._points - self._points
# Next, ensure the "world sets" (sets of variables) these worlds are
# coming from, are disjoint. If not, reject.
self_variables = set(w.variable for w in self._points)
other_variables = set(w.variable for w in incoming_points)
if self_variables & other_variables:
return World.empty()
else:
return World.from_set(self._points | other._points)
def is_empty(self) -> bool:
return len(self._points) == 0
@dataclass(frozen=True)
class Value:
value: Any
world: World
def __repr__(self):
return f"Value({self.value} :: {self.world})"
ValueSet = Set[Value]
def narrow(vs1: ValueSet, vs2: ValueSet, op: Callable[[Any, Any], Any]) -> ValueSet:
vs_result: ValueSet = set()
for v1 in vs1:
for v2 in vs2:
new_world = v1.world & v2.world
if new_world.is_empty():
continue # Skip impossible world results
new_value = op(v1.value, v2.value)
if isinstance(new_value, bool) and not new_value:
continue # Skip false boolean results
vs_result.add(Value(new_value, new_world))
return vs_result
class TestWorlds(unittest.TestCase):
def test_intersect_same_worlds(self):
w1 = World("w", 1)
w2 = World("w", 2)
self.assertEqual(w1 & w1, w1)
self.assertEqual(w1 & w2, World.empty())
def test_intersect_different_worlds(self):
u1 = World("u", 1)
v1 = World("v", 1)
z1 = u1 & v1
self.assertEqual(u1 & v1, z1)
self.assertEqual(v1 & u1, z1)
def test_intersect_intersected_worlds(self):
x1 = World("x", 1)
y1 = World("y", 1)
z1 = World("z", 1)
xy1 = x1 & y1
yz1 = y1 & z1
self.assertEqual((x1 & xy1), xy1)
xyz1 = xy1 & yz1
self.assertEqual(xyz1, x1 & y1 & z1)
# note that neither x nor z survives this collision:
y2 = World("y", 2)
self.assertEqual(xyz1 & y2, World.empty())
class TestNarrowing(unittest.TestCase):
def test_narrow_basics(self):
"""First example from Wikipedia article."""
w1 = World("x", 1)
w2 = World("x", 2)
vs1 = {Value(2, w1), Value(-2, w2)}
self.assertEqual(vs1, {Value(2, w1), Value(-2, w2)})
vs2 = narrow(vs1, vs1, lambda x, y: x + y)
self.assertEqual(vs2, {Value(4, w1), Value(-4, w2)})
def test_narrow_boolean_implication(self):
"""Second example from Wikipedia article.
This is a weird example that is not all that illustrative IMO,
but I think I understand what it is trying to say."""
a1 = World("a", 1)
a2 = World("a", 2)
vsa = {Value(False, a1), Value(True, a2)}
vsb = {Value(True, a1), Value(False, a2), Value(True, a2)}
vsc = narrow(vsa, vsb, lambda x, y: x and y)
self.assertEqual(vsc, {Value(True, a2)})
def test_narrow_with_booleans(self):
"""The input sets and the result set are all booleans."""
a1 = World("a", 1)
a2 = World("a", 2)
a3 = World("a", 3)
b1 = World("b", 1)
b2 = World("b", 2)
b3 = World("b", 3)
vsa = {Value(True, a1), Value(True, a2), Value(False, a3)}
vsb = {Value(False, b1), Value(True, b2), Value(True, b3)}
vsc = narrow(vsa, vsb, lambda x, y: x and y)
self.assertEqual(vsc, {
Value(True, a1 & b2),
Value(True, a1 & b3),
Value(True, a2 & b2),
Value(True, a2 & b3),
})
def test_narrow_with_comparator(self):
"""The input sets are integers but the result set is booleans."""
a1 = World("a", 1)
a2 = World("a", 2)
a3 = World("a", 3)
b1 = World("b", 1)
b2 = World("b", 2)
b3 = World("b", 3)
vsa = {Value(10, a1), Value(20, a2), Value(30, a3)}
vsb = {Value(5, b1), Value(15, b2), Value(20, b3)}
vsc = narrow(vsa, vsb, lambda x, y: x < y)
self.assertEqual(vsc, {
Value(True, a1 & b2),
Value(True, a1 & b3)
})
def test_narrow_solving_equations(self):
"""The third example from the article."""
x1 = World("x", 1)
x2 = World("x", 2)
x3 = World("x", 3)
y1 = World("y", 1)
y2 = World("y", 2)
y3 = World("y", 3)
vsx = {Value(1, x1), Value(3, x2), Value(4, x3)}
vsy = {Value(8, y1), Value(9, y2)}
vsr1 = narrow(vsx, vsy, lambda x, y: x * y < 25)
self.assertEqual(vsr1, {
Value(True, x2 & y1),
Value(True, x1 & y1),
Value(True, x1 & y2)
})
vsr2 = narrow(vsx, vsy, lambda x, y: x + y > 10)
self.assertEqual(vsr2, {
Value(True, x2 & y1),
Value(True, x3 & y1),
Value(True, x2 & y2),
Value(True, x3 & y2),
})
vsr3 = narrow(vsr1, vsr2, lambda x, y: x and y)
self.assertEqual(vsr3, {
Value(True, x2 & y1)
})
def test_narrow_solving_equations_2(self):
vsx = {Value(n, World("x", n)) for n in range(1, 11)}
vsy = {Value(n, World("y", n)) for n in range(1, 11)}
vsr1 = narrow(vsx, vsy, lambda x, y: x + y == 5)
vsr2 = narrow(vsx, vsy, lambda x, y: x - y == 1)
vsr3 = narrow(vsr1, vsr2, lambda x, y: x and y)
self.assertEqual(vsr3, {
Value(True, World("x", 3) & World("y", 2))
})
def test_narrow_discrete_constraint_systems(self):
"""The fourth example from the article. This is also slightly
incoherent - the values are strings but the operation is `and`
but how do you `and` strings? We provide an appropriate oper-
ation here, and we do get the same answer they get."""
pizza_shop = {
Value("Carlton", World("p", 1)),
Value("Richmond", World("p", 2)),
Value("South Melbourne", World("p", 3)),
Value("Footscray", World("p", 4)),
Value("St Kilda", World("p", 5)),
Value("Toorak", World("p", 6)),
}
beer_shop = {
Value("South Melbourne", World("b", 1)),
Value("St Kilda", World("b", 2)),
Value("Carlton", World("b", 3)),
Value("Docklands", World("b", 4)),
}
whiskey_shop = {
Value("Essendon", World("w", 1)),
Value("South Melbourne", World("w", 2)),
}
where_to_go = narrow(
pizza_shop,
narrow(
beer_shop,
whiskey_shop,
lambda x, y: x if x == y else False
),
lambda x, y: x if x == y else False
)
self.assertEqual(where_to_go, {
Value("South Melbourne", World("b", 1) & World("w", 2) & World("p", 3))
})
if __name__ == '__main__':
unittest.main()