Add predicate to counterfactual variables for checking tautologies (#101)

* Add implementation

* Add tests

* added is_inconsistent() and updated docstring on has_tautology()

* Update implementation

* Add event predicate

* Update test_dsl.py

* Fix tests

* Add inconsistency tests

Co-authored-by: Jeremy Zucker <[email protected]>

Author: cthoyt

src/y0/dsl.py

@@ -357,6 +357,34 @@ def to_y0(self) -> str:
             ins = ", ".join(i.to_y0() for i in self.interventions)
             return f"{prefix}{self.name} @ ({ins})"
 
+    def is_event(self) -> bool:
+        """Return if the counterfactual variable has a value."""
+        return self.star is not None
+
+    def has_tautology(self) -> bool:
+        """Return if the counterfactual variable contain its own value in the subscript.
+
+        :returns: True if we force a variable X to have a value x and the resulting value of X is x.
+        :raises ValueError: if the counterfactual value doesn't have a value assigned
+        """
+        if not self.is_event():
+            raise ValueError(
+                "Can not determine the consistency of a counterfactual variable with no value assigned."
+            )
+        return any(self.name == i.name and self.star == i.star for i in self.interventions)
+
+    def is_inconsistent(self) -> bool:
+        """Return if the counterfactual variable violates the Axiom of Effectiveness.
+
+        :returns: True if we force a variable X to have a value x and the resulting value of X is not x
+        :raises ValueError: if the counterfactual value doesn't have a value assigned
+        """
+        if not self.is_event():
+            raise ValueError(
+                "Can not determine the consistency of a counterfactual variable with no value assigned."
+            )
+        return any(self.name == i.name and self.star != i.star for i in self.interventions)
+
     def intervene(self, variables: VariableHint) -> CounterfactualVariable:
         """Intervene on this counterfactual variable with the given variable(s).
 

tests/test_dsl.py

@@ -356,6 +356,100 @@ def test_api(self):
                 self.assertEqual(variables, expression.get_variables())
 
 
+class TestCounterfactual(unittest.TestCase):
+    """Tests for counterfactuals."""
+
+    def test_event_semantics(self):
+        """Check DSL semantics."""
+        for expr, counterfactual_star, intervention_star in [
+            (X @ X, None, False),
+            (-X @ X, False, False),
+            (+X @ X, True, False),
+            (~X @ X, True, False),
+        ]:
+            with self.subTest(expr=expr.to_y0()):
+                self.assertIsInstance(expr, CounterfactualVariable)
+                self.assertEqual(counterfactual_star, expr.star)
+                self.assertEqual(1, len(expr.interventions))
+                self.assertEqual(intervention_star, expr.interventions[0].star)
+
+    def test_event_failures(self):
+        """Check for failure to determine tautology/inconsistent."""
+        for expr in [
+            # Opposite variable
+            X @ Y,
+            X @ +Y,
+            X @ -Y,
+            X @ ~Y,
+            # Same variable
+            X @ X,
+            X @ +X,
+            X @ -X,
+            X @ ~X,
+        ]:
+            with self.subTest(expr=expr.to_y0()):
+                self.assertIsInstance(expr, CounterfactualVariable)
+                self.assertFalse(expr.is_event())
+                with self.assertRaises(ValueError):
+                    expr.has_tautology()
+                with self.assertRaises(ValueError):
+                    expr.is_inconsistent()
+
+    def test_tautology(self):
+        """Check for tautologies."""
+        for expr, status in [
+            # Different Variable
+            (~X @ Y, False),
+            (~X @ ~Y, False),
+            # Same variable, self.star is False
+            (-X @ X, True),
+            (-X @ -X, True),
+            (-X @ +X, False),
+            (-X @ ~X, False),
+            # Same variable, self.star is True
+            (+X @ X, False),
+            (+X @ -X, False),
+            (+X @ +X, True),
+            (+X @ ~X, True),
+            # Same variable, self.star is True
+            (~X @ X, False),
+            (~X @ -X, False),
+            (~X @ +X, True),
+            (~X @ ~X, True),
+        ]:
+            with self.subTest(expr=expr.to_y0()):
+                self.assertIsInstance(expr, CounterfactualVariable)
+                self.assertTrue(expr.is_event())
+                self.assertEqual(status, expr.has_tautology())
+
+    def test_inconsistent(self):
+        """Check for tautologies."""
+        for expr, status in [
+            # Different Variable
+            (~X @ Y, False),
+            (~X @ ~Y, False),
+            # Same variable, self.star is False
+            (-X @ X, False),
+            (-X @ -X, False),
+            (-X @ +X, True),
+            (-X @ ~X, True),
+            # Same variable, self.star is True
+            (+X @ X, True),
+            (+X @ -X, True),
+            (+X @ +X, False),
+            (+X @ ~X, False),
+            # Same variable, self.star is True
+            (~X @ X, True),
+            (~X @ -X, True),
+            (~X @ +X, False),
+            (~X @ ~X, False),
+        ]:
+            with self.subTest(expr=expr.to_y0()):
+                self.assertIsInstance(expr, CounterfactualVariable)
+                self.assertTrue(expr.is_event())
+                self.assertEqual(status, expr.is_inconsistent())
+
+
 class TestSafeConstructors(unittest.TestCase):
     """Test that the .safe() constructors work properly."""