From fe8d9b766c14caf8c95c00d4dced46d8a5016e95 Mon Sep 17 00:00:00 2001 From: Emi Simpson Date: Mon, 6 Mar 2023 11:34:19 -0500 Subject: [PATCH] Allow hashing clauses --- ir.py | 52 ++++++++++++++++++++-------------------- resolution.py | 66 ++++++++++++++++++++++++++++++++------------------- 2 files changed, 67 insertions(+), 51 deletions(-) diff --git a/ir.py b/ir.py index e6e2a06..6790e88 100644 --- a/ir.py +++ b/ir.py @@ -2,7 +2,7 @@ from emis_funky_funktions import * from dataclasses import dataclass from functools import reduce -from typing import Sequence, TypeAlias +from typing import Collection, FrozenSet, Sequence, TypeAlias @dataclass(frozen=True) class Subst: @@ -62,7 +62,7 @@ class IRProp: The identifier of this thing, including its location in the source """ - arguments: 'Sequence[IRTerm]' = tuple() + arguments: 'Tuple[IRTerm, ...]' = tuple() def subst(self, subst: Subst) -> 'IRTerm': """ @@ -78,7 +78,7 @@ class IRProp: >>> original.subst(Subst('x1', IRProp('Alex'))) angry(Alex()) """ - return IRProp(self.name, [arg.subst(subst) for arg in self.arguments]) + return IRProp(self.name, tuple(arg.subst(subst) for arg in self.arguments)) def __str__(self) -> str: return repr(self) def __repr__(self) -> str: @@ -166,7 +166,17 @@ class IRNeg: return var in self.inner IRTerm: TypeAlias = IRVar | IRProp | IRNeg -Clause: TypeAlias = Sequence[IRTerm] +Clause: TypeAlias = FrozenSet[IRTerm] +Clause_: TypeAlias = Collection[IRTerm] +""" +A more general definition of `Clause` which uses a collection rather than a frozen set + +Every `Clause` is a `Clause_`, but not vice versa. In other words, true `Clause` is a +subclass of `Clause_`. + +Due to this generalization, `Clause_` does not necessarily benefit from hashability or +deduplication. It exists mostly to make inputing things easier, e.g. in doctests. +""" sub_all: Callable[[Substitutions, IRTerm], IRTerm] = p(reduce, lambda t, s: t.subst(s)) #type:ignore """ @@ -181,19 +191,6 @@ Applies every substitution to the term in order kismesis(Karkat(), Karkat()) """ -sub_all_clause: Callable[[Substitutions, Clause], Clause] = uncurry2(c(p_map, cur2(sub_all))) #type:ignore -""" -Perform a series of substitutions on every term in a list - -Effectively calls `sub_all()` on every element of the list. - ->>> sub_all_clause( -... [Subst('x1', IRVar('Dave')), Subst('x2', IRProp('Karkat'))], -... [IRProp('dating', [IRVar('x1'), IRVar('x2')]), IRVar('x1')], -... ) -[dating(Dave(),Karkat()), Dave()] -""" - def unify(t1: IRTerm, t2: IRTerm) -> Result[Substitutions, UnificationError]: """ Attempt to find a substitution that unifies two terms @@ -228,28 +225,31 @@ def unify(t1: IRTerm, t2: IRTerm) -> Result[Substitutions, UnificationError]: case (IRVar(v), t_other) | (t_other, IRVar(v)) if v not in t_other: #type: ignore return Ok((Subst(v, t_other),)) case (IRProp(n1, a1), IRProp(n2, a2)) if n1 == n2 and len(a1) == len(a2): - return unify_clauses(a1, a2) + return unify_lists(a1, a2) case (IRNeg(i1), IRNeg(i2)): return unify(i1, i2) return Err(UnificationMismatch(t1, t2)) -def unify_clauses(c1: Clause, c2: Clause) -> Result[Substitutions, UnificationError]: +def unify_lists(c1: Sequence[IRTerm], c2: Sequence[IRTerm]) -> Result[Substitutions, UnificationError]: """ - Attempt to perform unification on two clauses or argument lists + Attempt to perform unification on two term/argument lists - See `unify()` for the details of how this works. When working with clauses, the same - rules apply. The substitutions, when applied to every term of both clauses, will - cause the clauses to become exactly the same. + See `unify()` for the details of how this works. When working with lists, the same + rules apply. The substitutions, when applied to every term of both lists, will + cause the lists to become exactly the same. Lists which are not the same length cannot be unified, and will always fail. - >>> unify_clauses( + Notice the difference between a list of `IRTerm`s and a `Clause`: Namely, that a + `Clause` is unordered, while a list of `IRTerm`s is ordered. + + >>> unify_lists( ... [ IRProp('imaginary', [IRProp('Rufio')]), IRProp('friend', [IRVar('x1'), IRVar('x3')]) ], ... [ IRProp('imaginary', [IRVar('x1')]), IRProp('friend', [IRVar('x2'), IRProp('Tavros')]) ] ... ) Ok((Rufio()/x1, Rufio()/x2, Tavros()/x3)) - >>> unify_clauses( + >>> unify_lists( ... [ IRProp('imaginary', [IRProp('Rufio')]), IRProp('friend', [IRVar('x1'), IRVar('x3')]) ], ... [ IRProp('imaginary', [IRVar('x1')]) ] ... ) @@ -260,7 +260,7 @@ def unify_clauses(c1: Clause, c2: Clause) -> Result[Substitutions, UnificationEr return Ok(tuple()) case ([h1, *t1], [h2, *t2]): return unify(h1, h2) << (lambda subs: - unify_clauses((*map(p(sub_all,subs),t1),), (*map(p(sub_all,subs),t2),)) <= ( + unify_lists((*map(p(sub_all,subs),t1),), (*map(p(sub_all,subs),t2),)) <= ( lambda final_subs: (*subs, *final_subs))) case ([h, *t], []) | ([], [h, *t]): return Err(LengthMismatch(h)) diff --git a/resolution.py b/resolution.py index 7aea69e..e5ff81a 100644 --- a/resolution.py +++ b/resolution.py @@ -1,8 +1,19 @@ from emis_funky_funktions import * from itertools import combinations, product +from typing import Collection, FrozenSet, TypeAlias -from ir import Clause, IRNeg, IRProp, IRTerm, IRVar, Substitutions, sub_all, unify, unify_clauses +from ir import Clause, Clause_, IRNeg, IRProp, IRTerm, IRVar, Substitutions, sub_all, unify + +KnowledgeBase: TypeAlias = FrozenSet[Clause] +KnowledgeBase_: TypeAlias = Collection[Clause_] +""" +A more general version of `KnowledgeBase` + +`KnowledgeBase_` : `KnowledgeBase` :: `Clause_` : `Clause` + +A superclass of `KnowledgeBase` +""" def terms_cancel(t1: IRTerm, t2: IRTerm) -> Option[Substitutions]: """ @@ -29,53 +40,54 @@ def terms_cancel(t1: IRTerm, t2: IRTerm) -> Option[Substitutions]: return hush(unify(x, IRNeg(a))) return None -def merge_clauses(c1: Clause, c2: Clause) -> Sequence[Clause]: +def merge_clauses(c1: Clause_, c2: Clause_) -> KnowledgeBase: """ Produce a list of all possible clauses which resolution could derive from c1 and c2 For each term in c1 that could cancel with a term in c2 using a substitution, a - possible clause is produced equal to the concatenation of c1 and c2 with the canceled + possible clause is produced equal to the union of c1 and c2 with the canceled terms removed and the substitution applied. >>> merge_clauses( ... [ IRProp('day'), IRNeg(IRProp('night')) ], ... [ IRProp('night') ] ... ) - [[day()]] + { { day() } } >>> merge_clauses( ... [ IRNeg(IRProp('transgender', [IRVar('x1')])), IRProp('powerful', [IRVar('x1')]) ], ... [ IRNeg(IRProp('powerful', [IRVar('x2')])), IRProp('god', [IRVar('x2')]) ] ... ) - [[¬transgender(*x1), god(*x1)]] + { { god(*x1), ¬transgender(*x1) } } >>> merge_clauses( ... [ IRNeg(IRProp('day')), IRProp('night') ], ... [ IRVar('x2') ] ... ) - [[night()], [¬day()]] + { { night() }, { ¬day() } } - If two clauses cannot merge, an empty list is returned + If two clauses cannot merge, an empty set is returned >>> merge_clauses( ... [ IRProp('day') ], ... [ IRProp('wet') ] ... ) - [] + { } """ + terms1, terms2 = list(c1), list(c2) valid_substitutions = drop_none( map_opt(lambda subs: (subs, i1, i2), terms_cancel(t1, t2)) - for ((i1, t1), (i2, t2)) in product(enumerate(c1), enumerate(c2)) + for ((i1, t1), (i2, t2)) in product(enumerate(terms1), enumerate(terms2)) ) - return [ - [ + return FSet( + FSet( sub_all(subs, term) - for term in (*c1[:i1], *c1[i1 + 1:], *c2[:i2], *c2[i2 + 1:]) - ] + for term in (*terms1[:i1], *terms1[i1 + 1:], *terms2[:i2], *terms2[i2 + 1:]) + ) for (subs, i1, i2) in valid_substitutions - ] + ) -def derive(clauses: Sequence[Clause]) -> Sequence[Clause]: +def derive(clauses: KnowledgeBase_) -> KnowledgeBase: """ All possible clauses which derive in one step of resolution from a knowledge base @@ -86,16 +98,20 @@ def derive(clauses: Sequence[Clause]) -> Sequence[Clause]: ... [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])], ... [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])], ... [IRProp('dog', [IRProp('Kim')])], - ... ]) - [[¬dog(Kim())], [¬cat(Kim())], [animal(Kim())]] + ... ]) #doctest: +NORMALIZE_WHITESPACE + { + { animal(Kim()) }, + { ¬cat(Kim()) }, + { ¬dog(Kim()) } + } """ - return [ - clause + return FSet( + FSet(clause) for (c1, c2) in combinations(clauses, 2) for clause in merge_clauses(c1, c2) - ] + ) -def derive2(kb1: Sequence[Clause], kb2: Sequence[Clause]) -> Sequence[Clause]: +def derive2(kb1: KnowledgeBase_, kb2: KnowledgeBase_) -> KnowledgeBase: """ All clauses which derive in one step from the combination of two knowledge bases @@ -110,13 +126,13 @@ def derive2(kb1: Sequence[Clause], kb2: Sequence[Clause]) -> Sequence[Clause]: ... [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])], ... [IRProp('dog', [IRProp('Kim')])], ... ]) - [[¬dog(Kim())]] + { { ¬dog(Kim()) } } """ - return [ - clause + return FSet( + FSet(clause) for (c1, c2) in product(kb1, kb2) for clause in merge_clauses(c1, c2) - ] + ) if __name__ == '__main__': import doctest