Skip to content

Instantly share code, notes, and snippets.

@TonyMooori
Created June 19, 2020 17:08
Show Gist options
  • Save TonyMooori/05de32db5b48606d713abdfabfa69d21 to your computer and use it in GitHub Desktop.
Save TonyMooori/05de32db5b48606d713abdfabfa69d21 to your computer and use it in GitHub Desktop.
限られた真理関数のみで特定の真理関数と意味論的に同値なものを構成するプログラム
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()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment