mirror of
https://github.com/Brandon-Rozek/matmod.git
synced 2024-09-17 08:02:29 -04:00
Some optimizations
This commit is contained in:
parent
9f985740e0
commit
20ccacc166
5 changed files with 132 additions and 57 deletions
34
R.py
34
R.py
|
@ -23,38 +23,38 @@ x = PropositionalVariable("x")
|
||||||
y = PropositionalVariable("y")
|
y = PropositionalVariable("y")
|
||||||
z = PropositionalVariable("z")
|
z = PropositionalVariable("z")
|
||||||
|
|
||||||
|
|
||||||
implication_rules = {
|
implication_rules = {
|
||||||
Rule({}, Implication(x, x)),
|
Rule(set(), Implication(x, x)),
|
||||||
Rule({Implication(x, y), Implication(y, z)}, Implication(x, z)),
|
Rule({Implication(x, y), Implication(y, z)}, Implication(x, z)),
|
||||||
Rule({}, Implication(Implication(x, Implication(x, y)), Implication(x, y))),
|
Rule({Implication(x, Implication(x, y)),}, Implication(x, y)),
|
||||||
Rule({}, Implication(Implication(x, Implication(y, z)), Implication(y, Implication(x, z)))),
|
Rule({Implication(x, Implication(y, z)),}, Implication(y, Implication(x, z))),
|
||||||
Rule({}, Implication(Implication(x, y), Implication(Implication(z, x), Implication(z, y)))),
|
Rule({Implication(x, y),}, Implication(Implication(z, x), Implication(z, y))),
|
||||||
Rule({}, Implication(Implication(x, y), Implication(Implication(y, z), Implication(x, z)))),
|
Rule({Implication(x, y),}, Implication(Implication(y, z), Implication(x, z))),
|
||||||
Rule({Implication(x, y), x}, y)
|
Rule({Implication(x, y), x}, y)
|
||||||
}
|
}
|
||||||
|
|
||||||
negation_rules = {
|
negation_rules = {
|
||||||
Rule({}, Implication(Negation(Negation(x)), x)),
|
Rule({Negation(Negation(x)),}, x),
|
||||||
Rule({}, Implication(x, Negation(Negation(x)))),
|
Rule({x,}, Negation(Negation(x))),
|
||||||
Rule({Implication(x, y)}, Implication(Negation(y), Negation(x))),
|
Rule({Implication(x, y)}, Implication(Negation(y), Negation(x))),
|
||||||
Rule({}, Implication(Implication(x, y), Implication(Negation(y), Negation(x))))
|
Rule({Implication(x, y),}, Implication(Negation(y), Negation(x)))
|
||||||
}
|
}
|
||||||
|
|
||||||
conjunction_rules = {
|
conjunction_rules = {
|
||||||
Rule({y, z}, Conjunction(y, z)),
|
Rule({y, z}, Conjunction(y, z)),
|
||||||
Rule({}, Implication(Conjunction(x, y), x)),
|
Rule({Conjunction(x, y),}, x),
|
||||||
Rule({}, Implication(Conjunction(x, y), y)),
|
Rule({Conjunction(x, y),}, y),
|
||||||
Rule({}, Implication(Conjunction(Implication(x, y), Implication(x, z)), Implication(x, Conjunction(y, z))))
|
Rule({Conjunction(Implication(x, y), Implication(x, z)),}, Implication(x, Conjunction(y, z)))
|
||||||
}
|
}
|
||||||
|
|
||||||
disjunction_rules = {
|
disjunction_rules = {
|
||||||
Rule({}, Implication(x, Disjunction(x, y))),
|
Rule({x,}, Disjunction(x, y)),
|
||||||
Rule({}, Implication(y, Disjunction(x, y))),
|
Rule({y,}, Disjunction(x, y)),
|
||||||
Rule({}, Implication(Conjunction(Implication(x, z), Implication(y, z)), Implication(Disjunction(x, y), z))),
|
Rule({Conjunction(Implication(x, z), Implication(y, z)),}, Implication(Disjunction(x, y), z)),
|
||||||
Rule({}, Implication(Conjunction(x, Disjunction(y, z)), Disjunction(Conjunction(x, y), Conjunction(x, z))))
|
Rule({Conjunction(x, Disjunction(y, z)),}, Disjunction(Conjunction(x, y), Conjunction(x, z)))
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
logic_rules = implication_rules | negation_rules | conjunction_rules | disjunction_rules
|
logic_rules = implication_rules | negation_rules | conjunction_rules | disjunction_rules
|
||||||
|
|
||||||
operations = {Negation, Conjunction, Disjunction, Implication}
|
operations = {Negation, Conjunction, Disjunction, Implication}
|
||||||
|
@ -118,7 +118,7 @@ interpretation = {
|
||||||
# Generate models of R of a given size
|
# Generate models of R of a given size
|
||||||
|
|
||||||
model_size = 2
|
model_size = 2
|
||||||
satisfiable_models = generate_model(R_logic, model_size)
|
satisfiable_models = generate_model(R_logic, model_size, print_model=True)
|
||||||
|
|
||||||
print(f"There are {len(satisfiable_models)} satisfiable models of element length {model_size}")
|
print(f"There are {len(satisfiable_models)} satisfiable models of element length {model_size}")
|
||||||
|
|
||||||
|
|
4
common.py
Normal file
4
common.py
Normal file
|
@ -0,0 +1,4 @@
|
||||||
|
from typing import Set
|
||||||
|
|
||||||
|
def set_to_str(x: Set) -> str:
|
||||||
|
return "{" + ", ".join((str(xi) for xi in x)) + "}"
|
|
@ -1,9 +1,11 @@
|
||||||
"""
|
"""
|
||||||
File which generates all the models
|
File which generates all the models
|
||||||
"""
|
"""
|
||||||
from logic import Logic
|
from common import set_to_str
|
||||||
|
from logic import Logic, Operation, Rule, get_operations_from_term, PropositionalVariable
|
||||||
from model import ModelValue, Model, satisfiable, ModelFunction
|
from model import ModelValue, Model, satisfiable, ModelFunction
|
||||||
from itertools import combinations, chain, product
|
from itertools import combinations, chain, product
|
||||||
|
from typing import Set
|
||||||
|
|
||||||
def possible_designations(iterable):
|
def possible_designations(iterable):
|
||||||
"""Powerset without the empty and complete set"""
|
"""Powerset without the empty and complete set"""
|
||||||
|
@ -23,13 +25,59 @@ def possible_functions(operation, carrier_set):
|
||||||
|
|
||||||
yield ModelFunction(new_function, operation.symbol)
|
yield ModelFunction(new_function, operation.symbol)
|
||||||
|
|
||||||
def possible_interpretations(logic, carrier_set):
|
|
||||||
|
def only_rules_with(rules: Set[Rule], operation: Operation) -> Set[Rule]:
|
||||||
|
result_rules = []
|
||||||
|
for rule in rules:
|
||||||
|
is_valid = True
|
||||||
|
for t in (rule.premises | {rule.conclusion,}):
|
||||||
|
t_operations = get_operations_from_term(t)
|
||||||
|
if len(t_operations) > 1:
|
||||||
|
is_valid = False
|
||||||
|
break
|
||||||
|
if len(t_operations) == 0:
|
||||||
|
continue
|
||||||
|
t_operation = next(iter(t_operations))
|
||||||
|
if t_operation != operation:
|
||||||
|
is_valid = False
|
||||||
|
break
|
||||||
|
if is_valid:
|
||||||
|
result_rules.append(rule)
|
||||||
|
return result_rules
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
def possible_interpretations(
|
||||||
|
logic: Logic, carrier_set: Set[ModelValue],
|
||||||
|
designated_values: Set[ModelValue]):
|
||||||
operations = []
|
operations = []
|
||||||
model_functions = []
|
model_functions = []
|
||||||
|
|
||||||
for operation in logic.operations:
|
for operation in logic.operations:
|
||||||
operations.append(operation)
|
operations.append(operation)
|
||||||
model_functions.append(possible_functions(operation, carrier_set))
|
candidate_functions = list(possible_functions(operation, carrier_set))
|
||||||
|
passed_functions = []
|
||||||
|
"""
|
||||||
|
Only consider functions that at least pass
|
||||||
|
in the rules with the operation by itself.
|
||||||
|
"""
|
||||||
|
restricted_rules = only_rules_with(logic.rules, operation)
|
||||||
|
if len(restricted_rules) > 0:
|
||||||
|
small_logic = Logic({operation,}, restricted_rules)
|
||||||
|
for f in candidate_functions:
|
||||||
|
small_model = Model(carrier_set, {f,}, designated_values)
|
||||||
|
interp = {operation: f}
|
||||||
|
if satisfiable(small_logic, small_model, interp):
|
||||||
|
passed_functions.append(f)
|
||||||
|
else:
|
||||||
|
passed_functions = candidate_functions
|
||||||
|
if len(passed_functions) == 0:
|
||||||
|
raise Exception("No interpretation satisfies the axioms for the operation " + str(operation))
|
||||||
|
else:
|
||||||
|
print(
|
||||||
|
f"Operation {operation.symbol} has {len(passed_functions)} candidate functions"
|
||||||
|
)
|
||||||
|
model_functions.append(passed_functions)
|
||||||
|
|
||||||
functions_choice = product(*model_functions)
|
functions_choice = product(*model_functions)
|
||||||
for functions in functions_choice:
|
for functions in functions_choice:
|
||||||
|
@ -39,25 +87,36 @@ def possible_interpretations(logic, carrier_set):
|
||||||
interpretation[operation] = function
|
interpretation[operation] = function
|
||||||
yield interpretation
|
yield interpretation
|
||||||
|
|
||||||
def generate_model(logic: Logic, number_elements: int):
|
def generate_model(logic: Logic, number_elements: int, num_solutions: int = -1, print_model=False):
|
||||||
carrier_set = {
|
carrier_set = {
|
||||||
ModelValue("a" + str(i)) for i in range(number_elements)
|
ModelValue("a" + str(i)) for i in range(number_elements)
|
||||||
}
|
}
|
||||||
|
|
||||||
possible_designated_values = possible_designations(carrier_set)
|
possible_designated_values = possible_designations(carrier_set)
|
||||||
possible_interps = possible_interpretations(logic, carrier_set)
|
|
||||||
|
|
||||||
satisfied_models = []
|
satisfied_models = []
|
||||||
checked = 0
|
for designated_values in possible_designated_values:
|
||||||
for designated_values, interpretation in product(possible_designated_values, possible_interps):
|
|
||||||
checked += 1
|
|
||||||
designated_values = set(designated_values)
|
designated_values = set(designated_values)
|
||||||
|
print("Considering models for designated values", set_to_str(designated_values))
|
||||||
|
possible_interps = possible_interpretations(logic, carrier_set, designated_values)
|
||||||
|
|
||||||
model = Model(carrier_set, set(interpretation.values()), designated_values)
|
for interpretation in possible_interps:
|
||||||
if satisfiable(logic, model, interpretation):
|
is_valid = True
|
||||||
satisfied_models.append(model)
|
model = Model(carrier_set, set(interpretation.values()), designated_values)
|
||||||
print(model)
|
# Iteratively test possible interpretations
|
||||||
|
# by adding one axiom at a time
|
||||||
|
for rule in logic.rules:
|
||||||
|
small_logic = Logic(logic.operations, {rule,})
|
||||||
|
if not satisfiable(small_logic, model, interpretation):
|
||||||
|
is_valid = False
|
||||||
|
break
|
||||||
|
|
||||||
print("Checked", checked)
|
if is_valid:
|
||||||
|
satisfied_models.append(model)
|
||||||
|
if print_model:
|
||||||
|
print(model, flush=True)
|
||||||
|
|
||||||
|
if num_solutions >= 0 and len(satisfied_models) >= num_solutions:
|
||||||
|
return satisfied_models
|
||||||
|
|
||||||
return satisfied_models
|
return satisfied_models
|
||||||
|
|
29
logic.py
29
logic.py
|
@ -1,4 +1,4 @@
|
||||||
from typing import Any, Set
|
from typing import Any, Set, Tuple
|
||||||
from functools import lru_cache
|
from functools import lru_cache
|
||||||
|
|
||||||
class Operation:
|
class Operation:
|
||||||
|
@ -38,14 +38,10 @@ class PropositionalVariable(Term):
|
||||||
|
|
||||||
def __hash__(self):
|
def __hash__(self):
|
||||||
return self.hashed_value
|
return self.hashed_value
|
||||||
# def __setattr__(self, name: str, value: Any):
|
|
||||||
# raise Exception("Propositional variables are immutable")
|
|
||||||
def __str__(self):
|
def __str__(self):
|
||||||
return self.name
|
return self.name
|
||||||
|
|
||||||
# def PropTerm(Term):
|
|
||||||
# def __init__(self, v: PropositionalVariable):
|
|
||||||
# self.v = v
|
|
||||||
|
|
||||||
class OpTerm(Term):
|
class OpTerm(Term):
|
||||||
def __init__(self, operation: Operation, arguments):
|
def __init__(self, operation: Operation, arguments):
|
||||||
|
@ -65,12 +61,12 @@ class OpTerm(Term):
|
||||||
arg_strs = [str(a) for a in self.arguments]
|
arg_strs = [str(a) for a in self.arguments]
|
||||||
return self.operation.symbol + "(" + ",".join(arg_strs) + ")"
|
return self.operation.symbol + "(" + ",".join(arg_strs) + ")"
|
||||||
|
|
||||||
|
# Standard operators
|
||||||
Negation = Operation("¬", 1)
|
Negation = Operation("¬", 1)
|
||||||
Conjunction = Operation("∧", 2)
|
Conjunction = Operation("∧", 2)
|
||||||
Disjunction = Operation("∨", 2)
|
Disjunction = Operation("∨", 2)
|
||||||
Implication = Operation("→", 2)
|
Implication = Operation("→", 2)
|
||||||
|
|
||||||
|
|
||||||
class Inequation:
|
class Inequation:
|
||||||
def __init__(self, antecedant : Term, consequent: Term):
|
def __init__(self, antecedant : Term, consequent: Term):
|
||||||
self.antecedant = antecedant
|
self.antecedant = antecedant
|
||||||
|
@ -104,18 +100,19 @@ class Logic:
|
||||||
self.rules = rules
|
self.rules = rules
|
||||||
|
|
||||||
|
|
||||||
def get_prop_var_from_term(t: Term):
|
def get_prop_var_from_term(t: Term) -> Set[PropositionalVariable]:
|
||||||
if isinstance(t, PropositionalVariable):
|
if isinstance(t, PropositionalVariable):
|
||||||
return {t,}
|
return {t,}
|
||||||
|
|
||||||
result = set()
|
result: Set[PropositionalVariable] = set()
|
||||||
for arg in t.arguments:
|
for arg in t.arguments:
|
||||||
result |= get_prop_var_from_term(arg)
|
result |= get_prop_var_from_term(arg)
|
||||||
|
|
||||||
return result
|
return result
|
||||||
|
|
||||||
def get_propostional_variables(rules):
|
@lru_cache
|
||||||
vars = set()
|
def get_propostional_variables(rules: Tuple[Rule]) -> Set[PropositionalVariable]:
|
||||||
|
vars: Set[PropositionalVariable] = set()
|
||||||
|
|
||||||
for rule in rules:
|
for rule in rules:
|
||||||
# Get all vars in premises
|
# Get all vars in premises
|
||||||
|
@ -126,3 +123,13 @@ def get_propostional_variables(rules):
|
||||||
vars |= get_prop_var_from_term(rule.conclusion)
|
vars |= get_prop_var_from_term(rule.conclusion)
|
||||||
|
|
||||||
return vars
|
return vars
|
||||||
|
|
||||||
|
def get_operations_from_term(t: Term) -> Set[Operation]:
|
||||||
|
if isinstance(t, PropositionalVariable):
|
||||||
|
return set()
|
||||||
|
|
||||||
|
result: Set[Operation] = {t.operation,}
|
||||||
|
for arg in t.arguments:
|
||||||
|
result |= get_operations_from_term(arg)
|
||||||
|
|
||||||
|
return result
|
||||||
|
|
27
model.py
27
model.py
|
@ -1,18 +1,18 @@
|
||||||
"""
|
"""
|
||||||
Defining what it means to be a model
|
Defining what it means to be a model
|
||||||
"""
|
"""
|
||||||
|
from common import set_to_str
|
||||||
from logic import (
|
from logic import (
|
||||||
PropositionalVariable, get_propostional_variables, Logic, Term,
|
PropositionalVariable, get_propostional_variables, Logic, Term,
|
||||||
Operation
|
Operation
|
||||||
)
|
)
|
||||||
from typing import Set, List, Dict
|
from typing import Set, List, Dict, Tuple
|
||||||
from itertools import product
|
from itertools import product
|
||||||
|
from functools import lru_cache
|
||||||
|
|
||||||
__all__ = ['ModelValue', 'ModelFunction', 'Model']
|
__all__ = ['ModelValue', 'ModelFunction', 'Model']
|
||||||
|
|
||||||
|
|
||||||
def set_to_str(x):
|
|
||||||
return "{" + ", ".join((str(xi) for xi in x)) + "}"
|
|
||||||
|
|
||||||
class ModelValue:
|
class ModelValue:
|
||||||
def __init__(self, name):
|
def __init__(self, name):
|
||||||
|
@ -80,7 +80,7 @@ Designated Values: {set_to_str(self.designated_values)}
|
||||||
return result
|
return result
|
||||||
|
|
||||||
|
|
||||||
def evaluate_term(t: Term, f: Dict[PropositionalVariable, ModelValue], interpretation: Dict[Operation, ModelFunction]):
|
def evaluate_term(t: Term, f: Dict[PropositionalVariable, ModelValue], interpretation: Dict[Operation, ModelFunction]) -> ModelValue:
|
||||||
if isinstance(t, PropositionalVariable):
|
if isinstance(t, PropositionalVariable):
|
||||||
return f[t]
|
return f[t]
|
||||||
|
|
||||||
|
@ -93,24 +93,28 @@ def evaluate_term(t: Term, f: Dict[PropositionalVariable, ModelValue], interpret
|
||||||
return model_function(*model_arguments)
|
return model_function(*model_arguments)
|
||||||
|
|
||||||
def all_model_valuations(
|
def all_model_valuations(
|
||||||
pvars: Set[PropositionalVariable],
|
pvars: Tuple[PropositionalVariable],
|
||||||
mvalues: Set[ModelValue]):
|
mvalues: Tuple[ModelValue]):
|
||||||
|
|
||||||
pvars = list(pvars)
|
|
||||||
possible_valuations = [mvalues for _ in pvars]
|
possible_valuations = [mvalues for _ in pvars]
|
||||||
all_possible_values = product(*possible_valuations)
|
all_possible_values = product(*possible_valuations)
|
||||||
|
|
||||||
for valuation in all_possible_values:
|
for valuation in all_possible_values:
|
||||||
mapping = dict()
|
mapping: Dict[PropositionalVariable, ModelValue] = dict()
|
||||||
assert len(pvars) == len(valuation)
|
assert len(pvars) == len(valuation)
|
||||||
for pvar, value in zip(pvars, valuation):
|
for pvar, value in zip(pvars, valuation):
|
||||||
mapping[pvar] = value
|
mapping[pvar] = value
|
||||||
yield mapping
|
yield mapping
|
||||||
|
|
||||||
|
@lru_cache
|
||||||
|
def all_model_valuations_cached(
|
||||||
|
pvars: Tuple[PropositionalVariable],
|
||||||
|
mvalues: Tuple[ModelValue]):
|
||||||
|
return list(all_model_valuations(pvars, mvalues))
|
||||||
|
|
||||||
def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, ModelFunction]):
|
def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, ModelFunction]) -> bool:
|
||||||
pvars = get_propostional_variables(logic.rules)
|
pvars = tuple(get_propostional_variables(tuple(logic.rules)))
|
||||||
mappings = all_model_valuations(pvars, model.carrier_set)
|
mappings = all_model_valuations_cached(pvars, tuple(model.carrier_set))
|
||||||
|
|
||||||
for mapping in mappings:
|
for mapping in mappings:
|
||||||
for rule in logic.rules:
|
for rule in logic.rules:
|
||||||
|
@ -120,6 +124,7 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode
|
||||||
if t not in model.designated_values:
|
if t not in model.designated_values:
|
||||||
premise_met = False
|
premise_met = False
|
||||||
break
|
break
|
||||||
|
|
||||||
if not premise_met:
|
if not premise_met:
|
||||||
continue
|
continue
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue