diff --git a/src/argumentation/structured/aspic/datalog_grounding.py b/src/argumentation/structured/aspic/datalog_grounding.py index ef68e4b..715d451 100644 --- a/src/argumentation/structured/aspic/datalog_grounding.py +++ b/src/argumentation/structured/aspic/datalog_grounding.py @@ -77,9 +77,53 @@ def ground_defeasible_theory( comparison=comparison, link=link, simplify=simplify, + rule_variable_orders=rule_variable_orders(theory), ) +def rule_variable_orders(theory: "DefeasibleTheory") -> Mapping[str, tuple[str, ...]]: + """Map each rule id to its variables in first-appearance order. + + Variables are ordered by where they first occur: the head's terms left to + right, then each body literal left to right (default negation included). + ``rel(Y, A) :- pair(Y, A)`` therefore orders ``(Y, A)``, not the + alphabetical ``(A, Y)``. This is the order in which a named defeater + ``~r(t1, ..., tn)`` binds ``r``'s variables. + """ + from gunray.parser import parse_atom_text + + orders: dict[str, tuple[str, ...]] = {} + for rule in ( + *theory.strict_rules, + *theory.defeasible_rules, + *theory.defeaters, + *theory.presumptions, + ): + variables: dict[str, None] = {} + for text in (rule.head, *rule.body): + atom_text = text.strip() + if atom_text.startswith("not "): + atom_text = atom_text[4:].strip() + for term in parse_atom_text(atom_text).terms: + for name in _term_variables_in_order(term): + variables.setdefault(name, None) + orders[rule.id] = tuple(variables) + return orders + + +def _term_variables_in_order(term: Any) -> tuple[str, ...]: + from gunray.types import AddExpression, SubtractExpression, Variable + + if isinstance(term, Variable): + return (term.name,) + if isinstance(term, (AddExpression, SubtractExpression)): + return ( + *_term_variables_in_order(term.left), + *_term_variables_in_order(term.right), + ) + return () + + def grounding_inspection_to_aspic( inspection: "GroundingInspection", *, @@ -88,11 +132,19 @@ def grounding_inspection_to_aspic( comparison: str = "elitist", link: str = "last", simplify: bool = True, + rule_variable_orders: Mapping[str, tuple[str, ...]] | None = None, ) -> GroundedDatalogTheory: """Project a Gunray ``GroundingInspection`` into ASPIC+ objects. This is the direct integration point for callers that already ran Gunray and kept the inspection report, such as propstore's ``GroundedRulesBundle``. + + A named defeater ``~r(t1, ..., tn)`` undercuts the instance of rule ``r`` + whose variables, in first-appearance order (head, then body left to + right), take the values ``t1..tn``. The inspection carries no rule text, + so callers with such defeaters pass ``rule_variable_orders`` (see + :func:`rule_variable_orders`); without it a named defeater with arguments + raises ``ValueError`` rather than guessing an order. """ simplification = inspection.simplification @@ -112,23 +164,34 @@ def grounding_inspection_to_aspic( axioms = frozenset(_literal_from_ground_atom(atom) for atom in fact_atoms) rule_origins: dict[Rule, GroundRuleOrigin] = {} + # Distinct authored rules can ground to one ASPIC+ rule; keep every + # (rule, origin) pair so no source id is dropped. + ground_origins: list[tuple[Rule, GroundRuleOrigin]] = [] strict_rules = tuple( _rule_from_instance( instance, kind="strict", name=None, origins=rule_origins, + ground_origins=ground_origins, ) for instance in strict_instances ) + # Generated rule names n(r) are literals of L that undercuts target, so + # they must be fresh with respect to every authored predicate. + reserved_names = _authored_predicates( + fact_atoms, + (*strict_instances, *defeasible_instances, *defeater_instances), + ) defeasible_rules = [] for index, instance in enumerate(defeasible_instances): defeasible_rules.append( _rule_from_instance( instance, kind="defeasible", - name=f"gr{index}", + name=_fresh_rule_name(f"gr{index}", reserved_names), origins=rule_origins, + ground_origins=ground_origins, ) ) defeasible_rules.extend( @@ -136,10 +199,12 @@ def grounding_inspection_to_aspic( defeater_instances, defeasible_rules, rule_origins, + reserved_names, + rule_variable_orders, ) ) - source_to_ground = _source_to_ground_rules(rule_origins) + source_to_ground = _source_to_ground_rules(ground_origins) pref = PreferenceConfig( rule_order=_project_rule_order(superiority, source_to_ground), premise_order=frozenset(), @@ -195,6 +260,7 @@ def _rule_from_instance( kind: str, name: str | None, origins: dict[Rule, GroundRuleOrigin], + ground_origins: list[tuple[Rule, GroundRuleOrigin]], ) -> Rule: if getattr(instance, "default_negated_body", ()): raise ValueError("ASPIC+ grounding does not accept default-negated rule bodies") @@ -204,11 +270,13 @@ def _rule_from_instance( kind=kind, name=name, ) - origins[rule] = GroundRuleOrigin( + origin = GroundRuleOrigin( source_rule_id=instance.rule_id, substitution=tuple((name, value) for name, value in instance.substitution), role="ground", ) + origins.setdefault(rule, origin) + ground_origins.append((rule, origin)) return rule @@ -216,6 +284,8 @@ def _undercut_rules_from_defeaters( defeater_instances: tuple["GroundRuleInstance", ...], target_rules: list[Rule], origins: dict[Rule, GroundRuleOrigin], + reserved_names: set[str], + variable_orders: Mapping[str, tuple[str, ...]] | None, ) -> tuple[Rule, ...]: undercut_rules: list[Rule] = [] for instance in defeater_instances: @@ -225,7 +295,9 @@ def _undercut_rules_from_defeaters( ) defeater_head = _literal_from_ground_atom(instance.head) antecedents = tuple(_literal_from_ground_atom(atom) for atom in instance.body) - defeater_targets = _defeater_targets(defeater_head, target_rules, origins) + defeater_targets = _defeater_targets( + defeater_head, target_rules, origins, variable_orders + ) for target_rule in defeater_targets: if target_rule.name is None: continue @@ -233,7 +305,7 @@ def _undercut_rules_from_defeaters( antecedents=antecedents, consequent=Literal(GroundAtom(target_rule.name), negated=True), kind="defeasible", - name=f"uc{len(undercut_rules)}", + name=_fresh_rule_name(f"uc{len(undercut_rules)}", reserved_names), ) origins[rule] = GroundRuleOrigin( source_rule_id=instance.rule_id, @@ -247,20 +319,60 @@ def _undercut_rules_from_defeaters( return tuple(undercut_rules) +def _authored_predicates( + fact_atoms: Any, + instances: tuple["GroundRuleInstance", ...], +) -> set[str]: + atoms = [*fact_atoms] + for instance in instances: + atoms.append(instance.head) + atoms.extend(instance.body) + return {_literal_from_ground_atom(atom).atom.predicate for atom in atoms} + + +def _fresh_rule_name(preferred: str, reserved_names: set[str]) -> str: + """Return ``preferred`` or a suffixed variant not yet reserved, and reserve it.""" + name = preferred + suffix = 0 + while name in reserved_names: + suffix += 1 + name = f"{preferred}_{suffix}" + reserved_names.add(name) + return name + + def _defeater_targets( defeater_head: Literal, rules: list[Rule], origins: Mapping[Rule, GroundRuleOrigin], + variable_orders: Mapping[str, tuple[str, ...]] | None, ) -> tuple[Rule, ...]: if defeater_head.negated: - source_id_targets = tuple( + # ``~r(t1, ..., tn)`` names the instance of rule ``r`` whose variables, + # in first-appearance order (head, then body left to right), take the + # values ``t1..tn`` (Diller et al. 2025: each ground instance r theta + # is a separate rule). A nullary ``~r`` names every instance of ``r``. + source_id = defeater_head.atom.predicate + named_rules = [ rule for rule in rules - if rule.name is not None - and origins[rule].source_rule_id == defeater_head.atom.predicate - ) - if source_id_targets: - return source_id_targets + if rule.name is not None and origins[rule].source_rule_id == source_id + ] + arguments = defeater_head.atom.arguments + if named_rules and arguments: + if variable_orders is None or source_id not in variable_orders: + raise ValueError( + f"named defeater {defeater_head!r} needs the variable order of " + f"rule {source_id!r}; pass rule_variable_orders" + ) + order = variable_orders[source_id] + named_rules = [ + rule + for rule in named_rules + if _values_in_order(origins[rule].substitution, order) == arguments + ] + if named_rules: + return tuple(named_rules) return tuple( rule for rule in rules @@ -268,13 +380,21 @@ def _defeater_targets( ) +def _values_in_order( + substitution: tuple[tuple[str, Scalar], ...], + order: tuple[str, ...], +) -> tuple[Scalar, ...] | None: + bindings = dict(substitution) + if set(bindings) != set(order): + return None + return tuple(bindings[name] for name in order) + + def _source_to_ground_rules( - origins: Mapping[Rule, GroundRuleOrigin], + ground_origins: list[tuple[Rule, GroundRuleOrigin]], ) -> Mapping[str, frozenset[Rule]]: grouped: dict[str, set[Rule]] = {} - for rule, origin in origins.items(): - if origin.role != "ground": - continue + for rule, origin in ground_origins: grouped.setdefault(origin.source_rule_id, set()).add(rule) return {source_id: frozenset(rules) for source_id, rules in grouped.items()} diff --git a/tests/structured/aspic/test_datalog_grounding.py b/tests/structured/aspic/test_datalog_grounding.py index 53c510b..bd9146e 100644 --- a/tests/structured/aspic/test_datalog_grounding.py +++ b/tests/structured/aspic/test_datalog_grounding.py @@ -1,5 +1,6 @@ from __future__ import annotations +import pytest from gunray import DefeasibleTheory, Rule as GunrayRule from argumentation.structured.aspic.aspic import GroundAtom, Literal, build_arguments @@ -181,3 +182,210 @@ def test_defeater_projection_records_structured_undercut_origin() -> None: assert undercut_origin.substitution == (("X", "tweety"),) assert undercut_origin.role == "undercut" assert undercut_origin.target_rule == target_rule + + +def _flies(constant: str) -> Literal: + return Literal(GroundAtom("flies", (constant,))) + + +def _birds_fly_theory(defeater_head: str, exception_facts) -> DefeasibleTheory: + return DefeasibleTheory( + facts={"bird": {("a",), ("b",)}, "exception": exception_facts}, + defeasible_rules=[ + GunrayRule(id="birds_fly", head="flies(X)", body=["bird(X)"]), + ], + defeaters=[ + GunrayRule(id="except", head=defeater_head, body=["exception(X)"]), + ], + ) + + +def test_named_defeater_undercuts_only_its_matching_rule_instance() -> None: + """Issue #66: ``~birds_fly(a)`` undercuts only the ``X = a`` instance. + + Diller et al. 2025 ground each rule instance ``r theta`` separately, and + an undercut targets the name ``n(r)`` of one defeasible rule (Def 3), so + a named defeater for ``birds_fly(a)`` must not undercut ``birds_fly(b)``. + """ + from argumentation.structured.aspic.aspic_encoding import solve_aspic_grounded + + grounded = ground_defeasible_theory(_birds_fly_theory("~birds_fly(X)", {("a",)})) + + targets = [ + grounded.rule_origins[origin.target_rule].substitution + for origin in grounded.rule_origins.values() + if origin.role == "undercut" and origin.target_rule is not None + ] + accepted = solve_aspic_grounded( + grounded.system, grounded.kb, grounded.pref + ).accepted_conclusions + + assert targets == [(("X", "a"),)] + assert _flies("b") in accepted + assert _flies("a") not in accepted + + +def _pair_theory(*, head: str, body: list[str]) -> DefeasibleTheory: + """Rule ``r`` over facts pair(a, b) and pair(b, a); the defeater + ``~r(a, b)`` fires on exc(a, b).""" + return DefeasibleTheory( + facts={"pair": {("a", "b"), ("b", "a")}, "exc": {("a", "b")}}, + defeasible_rules=[GunrayRule(id="r", head=head, body=body)], + defeaters=[GunrayRule(id="except", head="~r(P, Q)", body=["exc(P, Q)"])], + ) + + +def _undercut_target_substitutions(grounded) -> list[tuple[tuple[str, str], ...]]: + return [ + grounded.rule_origins[origin.target_rule].substitution + for origin in grounded.rule_origins.values() + if origin.role == "undercut" and origin.target_rule is not None + ] + + +def test_named_defeater_binds_variables_in_first_appearance_order() -> None: + """Issue #66 (maintainer decision): ``~r(t1, ..., tn)`` binds r's + variables in first-appearance order, head then body left to right. For + ``rel(Y, A) :- pair(Y, A)`` that is (Y, A), not the alphabetical (A, Y), + so ``~r(a, b)`` names the instance Y = a, A = b.""" + from argumentation.structured.aspic.aspic_encoding import solve_aspic_grounded + + grounded = ground_defeasible_theory( + _pair_theory(head="rel(Y, A)", body=["pair(Y, A)"]) + ) + accepted = solve_aspic_grounded( + grounded.system, grounded.kb, grounded.pref + ).accepted_conclusions + + assert _undercut_target_substitutions(grounded) == [(("A", "b"), ("Y", "a"))] + assert Literal(GroundAtom("rel", ("a", "b"))) not in accepted + assert Literal(GroundAtom("rel", ("b", "a"))) in accepted + + +def test_named_defeater_orders_body_variables_left_to_right() -> None: + """Issue #66: a variable first seen in the body follows the head's + variables, in body order: ``ok(Y) :- pair(Y, A)`` orders (Y, A).""" + grounded = ground_defeasible_theory(_pair_theory(head="ok(Y)", body=["pair(Y, A)"])) + + assert _undercut_target_substitutions(grounded) == [(("A", "b"), ("Y", "a"))] + + +def test_named_defeater_alphabetical_and_first_appearance_agree_control() -> None: + """Issue #66 control: for ``rel(A, Y)`` both orders are (A, Y), so + ``~r(a, b)`` names A = a, Y = b.""" + grounded = ground_defeasible_theory( + _pair_theory(head="rel(A, Y)", body=["pair(A, Y)"]) + ) + + assert _undercut_target_substitutions(grounded) == [(("A", "a"), ("Y", "b"))] + + +def test_inspection_projection_needs_variable_order_for_named_arguments() -> None: + """Issue #66: a bare Gunray inspection carries no rule text, so the + first-appearance order is unknown; a named defeater with arguments is + rejected instead of guessed, and succeeds once the order is supplied.""" + import gunray + + theory = _pair_theory(head="rel(Y, A)", body=["pair(Y, A)"]) + inspection = gunray.inspect_grounding(theory) + + with pytest.raises(ValueError, match="variable order"): + grounding_inspection_to_aspic(inspection) + + grounded = grounding_inspection_to_aspic( + inspection, rule_variable_orders={"r": ("Y", "A")} + ) + assert _undercut_target_substitutions(grounded) == [(("A", "b"), ("Y", "a"))] + + +def test_named_defeater_without_exception_undercuts_nothing() -> None: + """Issue #66 control: with no exception fact both birds fly.""" + from argumentation.structured.aspic.aspic_encoding import solve_aspic_grounded + + grounded = ground_defeasible_theory(_birds_fly_theory("~birds_fly(X)", set())) + accepted = solve_aspic_grounded( + grounded.system, grounded.kb, grounded.pref + ).accepted_conclusions + + assert {_flies("a"), _flies("b")} <= accepted + + +def _animal_theory(heads: tuple[str, str]) -> DefeasibleTheory: + return DefeasibleTheory( + facts={"bird": {("a",)}}, + strict_rules=[ + GunrayRule(id=rule_id, head=head, body=["bird(X)"]) + for rule_id, head in zip(("s1", "s2"), heads, strict=True) + ], + ) + + +def test_identically_grounded_strict_rules_keep_every_source_id() -> None: + """Issue #67: two authored rules grounding to one ASPIC+ rule keep both ids. + + Diller et al. 2025 (Def 9) ground each authored rule separately, so the + source-to-ground relation is many-to-one and must not drop ``s1``. + """ + grounded = ground_defeasible_theory( + _animal_theory(("animal(X)", "animal(X)")), simplify=False + ) + animal = Literal(GroundAtom("animal", ("a",))) + + assert set(grounded.source_to_ground_rules) == {"s1", "s2"} + assert ( + grounded.source_to_ground_rules["s1"] == grounded.source_to_ground_rules["s2"] + ) + assert {rule.consequent for rule in grounded.source_to_ground_rules["s1"]} == { + animal + } + + +def test_distinctly_grounded_strict_rules_keep_every_source_id() -> None: + """Issue #67 control: distinct heads give distinct ground rules.""" + grounded = ground_defeasible_theory( + _animal_theory(("animal(X)", "creature(X)")), simplify=False + ) + + assert set(grounded.source_to_ground_rules) == {"s1", "s2"} + assert grounded.source_to_ground_rules["s1"].isdisjoint( + grounded.source_to_ground_rules["s2"] + ) + + +def _flying_with_unrelated_fact(fact_predicate: str) -> frozenset[Literal]: + from argumentation.structured.aspic.aspic_encoding import solve_aspic_grounded + + grounded = ground_defeasible_theory( + DefeasibleTheory( + facts={"bird": {("a",)}, fact_predicate: {()}}, + defeasible_rules=[ + GunrayRule(id="birds_fly", head="flies(X)", body=["bird(X)"]), + ], + ) + ) + authored = { + Literal(GroundAtom(fact_predicate.removeprefix("~")), negated=True), + Literal(GroundAtom("bird", ("a",))), + } + names = { + rule.name for rule in grounded.system.defeasible_rules if rule.name is not None + } + assert not names & {literal.atom.predicate for literal in authored} + return solve_aspic_grounded( + grounded.system, grounded.kb, grounded.pref + ).accepted_conclusions + + +def test_generated_rule_names_avoid_authored_predicates() -> None: + """Issue #68: generated names n(r) must be fresh in the language. + + An undercut targets ``n(r)`` (Diller et al. 2025, Def 3), so a generated + name equal to an authored predicate turns the unrelated fact ``~gr0`` + into an undercutter of ``birds_fly``. + """ + assert _flies("a") in _flying_with_unrelated_fact("~gr0") + + +def test_generated_rule_names_with_unrelated_fact_control() -> None: + """Issue #68 control: a non-colliding unrelated fact changes nothing.""" + assert _flies("a") in _flying_with_unrelated_fact("~unrelated")