JSON-Lang/resolution.py

from emis_funky_funktions import *

from itertools import combinations, product
from operator import eq
from typing import Collection, FrozenSet, TypeAlias

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]:
	"""
	Determine if two terms could cancel each other out, given the right substitutions

	That is, is there some set of substitutions such that t1 = ¬t2 or ¬t1 = t2?

	If negation is possible and a substitution exists, that substitution is returned.
	Otherwise, `None` is returned.

	>>> terms_cancel(IRNeg(IRVar('x1')), IRProp('Terezi'))
	Some((Terezi()/x1,))

	>>> terms_cancel(IRProp('Nepeta'), IRVar('x1'))
	Some((¬Nepeta()/x1,))

	>>> terms_cancel(IRProp('ancestor', [IRVar('x1')]), IRVar('x1')) is None
	True
	"""
	match (t1, t2):
		case (IRNeg(a), b) | (b, IRNeg(a)): #type: ignore
			return hush(unify(a, b))
		case (IRVar(_) as x, a) | (a, IRVar(_) as x): #type: ignore
			return hush(unify(x, IRNeg(a)))
	return None

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 union of c1 and c2 with the canceled
    terms removed and the substitution applied.

    >>> merge_clauses(
    ...     [ IRProp('day'), IRNeg(IRProp('night')) ],
    ...     [ IRProp('night') ]
    ... )
    { { day() } }

    >>> merge_clauses(
    ...     [ IRNeg(IRProp('transgender', [IRVar('x1')])), IRProp('powerful', [IRVar('x1')]) ],
    ...     [ IRNeg(IRProp('powerful', [IRVar('x2')])), IRProp('god', [IRVar('x2')]) ]
    ... )
    { { god(*x1), ¬transgender(*x1) } }

    >>> merge_clauses(
    ...     [ IRNeg(IRProp('day')), IRProp('night') ],
    ...     [ IRVar('x2') ]
    ... )
    { { night() }, { ¬day() } }

    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(terms1), enumerate(terms2))
    )
    return FSet(
        FSet(
            sub_all(subs, term)
            for term in (*terms1[:i1], *terms1[i1 + 1:], *terms2[:i2], *terms2[i2 + 1:])
        )
        for (subs, i1, i2) in valid_substitutions
    )

def derive(clauses: KnowledgeBase_) -> KnowledgeBase:
    """
    All possible clauses which derive in one step of resolution from a knowledge base

    Attempts to merge every possible combination of clauses, in the knowledge base.

    >>> derive([
    ...     [IRNeg(IRProp('animal', [IRProp('Kim')]))],
    ...     [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
    ...     [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
    ...     [IRProp('dog', [IRProp('Kim')])],
    ... ]) #doctest: +NORMALIZE_WHITESPACE
    {
        { animal(Kim()) },
        { ¬cat(Kim())   },
        { ¬dog(Kim())   }
    }
    """
    return FSet(
        FSet(clause)
        for (c1, c2) in combinations(clauses, 2)
        for clause in merge_clauses(c1, c2)
    )

def derive2(kb1: KnowledgeBase_, kb2: KnowledgeBase_) -> KnowledgeBase:
    """
    All clauses which derive in one step from the combination of two knowledge bases

    Each resulting clause is the combination of one clause from the left knowledge base
    with exactly one clause from the right knowledge base.  Clauses from the same
    knowledge base will not be combined.

    >>> derive2([
    ...     [IRNeg(IRProp('animal', [IRProp('Kim')]))],
    ...     [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
    ... ], [
    ...     [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
    ...     [IRProp('dog', [IRProp('Kim')])],
    ... ])
    { { ¬dog(Kim()) } }
    """
    return FSet(
        FSet(clause)
        for (c1, c2) in product(kb1, kb2)
        for clause in merge_clauses(c1, c2)
    )

is_false: Callable[[Clause_], bool] = c(p(eq, 0), len)
"""
Determines whether a clause is equivalent to false

if __name__ == '__main__':
	import doctest
	doctest.testmod()