限られた真理関数のみで特定の真理関数と意味論的に同値なものを構成するプログラム

search_eq_logic.py

from typing import List, Callable, Union, Dict
from copy import deepcopy


def make_logical_op(n: int, f) \
        -> Callable[[List[bool]], bool]:
    def __retfunc(stack: List[bool]):
        if len(stack) < n:
            raise RuntimeError("Lack of arguments")

        xs: List[bool] = []
        for _ in range(n):
            v = stack.pop()
            if not isinstance(v, bool):
                raise RuntimeError("non-bool value is in stack")
            xs.append(v)
        return f(*xs)
    return __retfunc


# Warning: '->' is defined such that  [0, 1, '->'] is 0
BASIC_OPERATION: Dict[str, Callable[[List[bool]], bool]] = {
    'nor': make_logical_op(2, lambda x, y: not(x or y)),
    'nand': make_logical_op(2, lambda x, y: not(x and y)),
    'and': make_logical_op(2, lambda x, y: x and y),
    'or': make_logical_op(2, lambda x, y: x or y),
    'not': make_logical_op(1, lambda x: not x),
    '->': make_logical_op(2, lambda x, y: (not x) or y),
    '<->': make_logical_op(2, lambda x, y: x == y),
    'T': make_logical_op(0, lambda: True),
    'F': make_logical_op(0, lambda: False),
}


def evaluate_core(
        formula: List[Union[bool, str]],
        operation: Dict[str, Callable[[List[bool]], bool]],
        stack: List[bool] = None) -> bool:
    if stack is None:
        stack = []

    if len(formula) == 0:
        if len(stack) == 1:
            return stack.pop()
        else:
            raise RuntimeError("length of stack is not 1")
    else:
        f, formula = formula[0], formula[1:]
        if isinstance(f, bool):
            stack.append(f)
        elif f in operation:
            val = operation[f](stack)
            stack.append(val)
        else:
            raise RuntimeError("Unkown symbol: ", f)

        return evaluate_core(formula, operation, stack)


def evaluate(
        formula: List[str],
        interpret: Dict[str, bool],
        operation: Dict[str, Callable[[List[bool]], bool]] = None) -> bool:

    if operation is None:
        operation = BASIC_OPERATION
    operation = deepcopy(operation)

    formula_ = [interpret[x] if x in interpret else x for x in formula]

    return evaluate_core(formula_, operation)  # type:ignore


def make_row(interpret: Dict[str, bool], formula: List[str]):
    left = ",".join([x+":"+str(int(interpret[x])) for x in interpret.keys()])
    val = int(evaluate(formula, interpret))
    print(left, val)


def make_table(interprets: List[Dict[str, bool]], formula: List[str]):
    print(formula)
    for interpret in interprets:
        make_row(interpret, formula)


def search_constraint_expr(
        target_formula: List[str],
        interprets: List[Dict[str, bool]],
        allowed_characters: List[str],
        operation: Dict[str, Callable[[List[bool]], bool]] = None):
    stacks = [[x] for x in allowed_characters]
    while True:
        formula = stacks[0]
        stacks = stacks[1:]

        for x in allowed_characters:
            stacks.append(formula+[x])

        formula_test = formula + target_formula + ["<->"]
        flag = True
        for interpret in interprets:
            try:
                flag &= evaluate(formula_test, interpret, operation)
            except RuntimeError:
                flag = False

        if flag:
            print("success:", formula)
            break
        else:
            print("failed:", formula)


def test_formula():
    interprets: List[Dict[str, bool]] = [
        {"a": False, "b": False},
        {"a": False, "b": True},
        {"a": True, "b": False},
        {"a": True, "b": True},
    ]
    formulas: List[str] = [
        ["a", "b", "and"],
        ["a", "b", "or"],
        ["a", "b", "->"],
        ["a", "b", "<->"],
        ["a", "not"],
        ["T"],
        ["F"],
    ]

    for formula in formulas:
        make_table(interprets, formula)
        print("-"*30)


def main():
    interprets: List[Dict[str, bool]] = [
        {"a": False, "b": False},
        {"a": False, "b": True},
        {"a": True, "b": False},
        {"a": True, "b": True},
    ]
    operation = deepcopy(BASIC_OPERATION)
    operation["nyoro"] = make_logical_op(2, lambda x, y: (not x) and y)

    search_constraint_expr(
        ["a", "b", "and"],
        interprets,
        ["a", "b", "nyoro"],
        operation
    )

    search_constraint_expr(
        ["a", "b", "and"],
        interprets,
        ["a", "b", "nand"],
        operation
    )


if __name__ == "__main__":
    main()