diff --git a/R.py b/R.py index 0e565bf..4eea77b 100644 --- a/R.py +++ b/R.py @@ -11,7 +11,7 @@ from logic import ( Disjunction, Rule, ) -from model import Model, ModelFunction, ModelValue, has_vsp, satisfiable +from model import Model, ModelFunction, ModelValue from generate_model import generate_model @@ -71,26 +71,26 @@ a1 = ModelValue("a1") carrier_set = {a0, a1} -mnegation = ModelFunction(1, { +mnegation = ModelFunction({ a0: a1, a1: a0 }) -mimplication = ModelFunction(2, { +mimplication = ModelFunction({ (a0, a0): a1, (a0, a1): a1, (a1, a0): a0, (a1, a1): a1 }) -mconjunction = ModelFunction(2, { +mconjunction = ModelFunction({ (a0, a0): a0, (a0, a1): a0, (a1, a0): a0, (a1, a1): a1 }) -mdisjunction = ModelFunction(2, { +mdisjunction = ModelFunction({ (a0, a0): a0, (a0, a1): a1, (a1, a0): a1, @@ -117,182 +117,8 @@ interpretation = { # Generate models of R of a given size -# model_size = 2 -# solutions = generate_model(R_logic, model_size, print_model=True) +model_size = 2 +satisfiable_models = generate_model(R_logic, model_size, print_model=True) -# print(f"There are {len(solutions)} satisfiable models of element length {model_size}") +print(f"There are {len(satisfiable_models)} satisfiable models of element length {model_size}") -# for model, interpretation in solutions: -# print(has_vsp(model, interpretation)) - -###### - -# Smallest model for R that has the variable sharing property - -a0 = ModelValue("a0") -a1 = ModelValue("a1") -a2 = ModelValue("a2") -a3 = ModelValue("a3") -a4 = ModelValue("a4") -a5 = ModelValue("a5") - -carrier_set = { a0, a1, a2, a3, a4, a5 } -designated_values = {a1, a2, a3, a4, a5 } - -mnegation = ModelFunction(1, { - a5: a0, - a4: a1, - a3: a3, - a2: a2, - a1: a4, - a0: a5 -}) - -mimplication = ModelFunction(2, { - (a5, a5): a5, - (a5, a4): a0, - (a5, a3): a0, - (a5, a2): a0, - (a5, a1): a0, - (a5, a0): a0, - - (a4, a5): a5, - (a4, a4): a1, - (a4, a3): a0, - (a4, a2): a0, - (a4, a1): a0, - (a4, a0): a0, - - (a3, a5): a5, - (a3, a4): a3, - (a3, a3): a3, - (a3, a2): a0, - (a3, a1): a0, - (a3, a0): a0, - - (a2, a5): a5, - (a2, a4): a2, - (a2, a3): a0, - (a2, a2): a2, - (a2, a1): a0, - (a2, a0): a0, - - (a1, a5): a5, - (a1, a4): a4, - (a1, a3): a3, - (a1, a2): a2, - (a1, a1): a1, - (a1, a0): a0, - - (a0, a5): a5, - (a0, a4): a5, - (a0, a3): a5, - (a0, a2): a5, - (a0, a1): a5, - (a0, a0): a5 -}) - - -mconjunction = ModelFunction(2, { - (a5, a5): a5, - (a5, a4): a4, - (a5, a3): a3, - (a5, a2): a2, - (a5, a1): a1, - (a5, a0): a0, - - (a4, a5): a4, - (a4, a4): a4, - (a4, a3): a3, - (a4, a2): a2, - (a4, a1): a1, - (a4, a0): a0, - - (a3, a5): a3, - (a3, a4): a3, - (a3, a3): a3, - (a3, a2): a1, - (a3, a1): a1, - (a3, a0): a0, - - (a2, a5): a2, - (a2, a4): a2, - (a2, a3): a1, - (a2, a2): a2, - (a2, a1): a1, - (a2, a0): a0, - - (a1, a5): a1, - (a1, a4): a1, - (a1, a3): a1, - (a1, a2): a1, - (a1, a1): a1, - (a1, a0): a0, - - (a0, a5): a0, - (a0, a4): a0, - (a0, a3): a0, - (a0, a2): a0, - (a0, a1): a0, - (a0, a0): a0 -}) - -mdisjunction = ModelFunction(2, { - (a5, a5): a5, - (a5, a4): a5, - (a5, a3): a5, - (a5, a2): a5, - (a5, a1): a5, - (a5, a0): a5, - - (a4, a5): a5, - (a4, a4): a4, - (a4, a3): a4, - (a4, a2): a4, - (a4, a1): a4, - (a4, a0): a4, - - (a3, a5): a5, - (a3, a4): a4, - (a3, a3): a3, - (a3, a2): a4, - (a3, a1): a3, - (a3, a0): a3, - - (a2, a5): a5, - (a2, a4): a4, - (a2, a3): a4, - (a2, a2): a2, - (a2, a1): a2, - (a2, a0): a2, - - (a1, a5): a5, - (a1, a4): a4, - (a1, a3): a3, - (a1, a2): a2, - (a1, a1): a1, - (a1, a0): a1, - - (a0, a5): a5, - (a0, a4): a4, - (a0, a3): a3, - (a0, a2): a2, - (a0, a1): a1, - (a0, a0): a0 -}) - -logical_operations = { - mnegation, mimplication, mconjunction, mdisjunction -} -R_model_6 = Model(carrier_set, logical_operations, designated_values) - -interpretation = { - Negation: mnegation, - Conjunction: mconjunction, - Disjunction: mdisjunction, - Implication: mimplication -} - -print("Satisfiable", satisfiable(R_logic, R_model_6, interpretation)) - -print("Has VSP?", has_vsp(R_model_6, interpretation)) diff --git a/README.md b/README.md deleted file mode 100644 index 6e0ed93..0000000 --- a/README.md +++ /dev/null @@ -1,6 +0,0 @@ -# Matmod: Matrix Model Generator for Implicative Connectives - -This repository is mostly an experiment to help -me better understand matrix models. - -You're likely better off using [arranstewart/magic](https://github.com/arranstewart/magic). diff --git a/generate_model.py b/generate_model.py index 88b9bc9..11108b2 100644 --- a/generate_model.py +++ b/generate_model.py @@ -5,7 +5,7 @@ from common import set_to_str from logic import Logic, Operation, Rule, get_operations_from_term, PropositionalVariable from model import ModelValue, Model, satisfiable, ModelFunction, ModelOrderConstraint from itertools import combinations, chain, product -from typing import Set, List, Dict, Tuple +from typing import Set def possible_designations(iterable): """Powerset without the empty and complete set""" @@ -23,7 +23,7 @@ def possible_functions(operation, carrier_set): for input, output in zip(inputs, outputs): new_function[input] = output - yield ModelFunction(arity, new_function, operation.symbol) + yield ModelFunction(new_function, operation.symbol) def only_rules_with(rules: Set[Rule], operation: Operation) -> Set[Rule]: @@ -86,7 +86,7 @@ def possible_interpretations( interpretation[operation] = function yield interpretation -def generate_model(logic: Logic, number_elements: int, num_solutions: int = -1, print_model=False) -> List[Tuple[Model, Dict[Operation, ModelFunction]]]: +def generate_model(logic: Logic, number_elements: int, num_solutions: int = -1, print_model=False): assert number_elements > 0 carrier_set = { ModelValue("a" + str(i)) for i in range(number_elements) @@ -108,7 +108,7 @@ def generate_model(logic: Logic, number_elements: int, num_solutions: int = -1, possible_designated_values = possible_designations(carrier_set) - solutions: List[Tuple[Model, Dict[Operation, ModelFunction]]] = [] + satisfied_models = [] for designated_values in possible_designated_values: designated_values = set(designated_values) print("Considering models for designated values", set_to_str(designated_values)) @@ -126,12 +126,11 @@ def generate_model(logic: Logic, number_elements: int, num_solutions: int = -1, break if is_valid: - solutions.append((model, interpretation)) - # satisfied_models.append(model) + satisfied_models.append(model) if print_model: print(model, flush=True) - if num_solutions >= 0 and len(solutions) >= num_solutions: - return solutions + if num_solutions >= 0 and len(satisfied_models) >= num_solutions: + return satisfied_models - return solutions + return satisfied_models diff --git a/model.py b/model.py index 10c69fb..b2a80ed 100644 --- a/model.py +++ b/model.py @@ -4,13 +4,11 @@ Defining what it means to be a model from common import set_to_str from logic import ( PropositionalVariable, get_propostional_variables, Logic, Term, -Operation, Conjunction, Disjunction, Implication +Operation, Conjunction, Disjunction ) -from typing import Set, Dict, Tuple, Optional +from typing import Set, List, Dict, Tuple, Optional +from itertools import product from functools import lru_cache -from itertools import combinations, chain, product -from copy import deepcopy - __all__ = ['ModelValue', 'ModelFunction', 'Model'] @@ -35,21 +33,17 @@ class ModelValue: class ModelFunction: - def __init__(self, arity: int, mapping, operation_name = ""): + def __init__(self, mapping, operation_name = ""): self.operation_name = operation_name - self.arity = arity # Correct input to always be a tuple corrected_mapping = dict() for k, v in mapping.items(): if isinstance(k, tuple): - assert len(k) == arity corrected_mapping[k] = v elif isinstance(k, list): - assert len(k) == arity corrected_mapping[tuple(k)] = v else: # Assume it's atomic - assert arity == 1 corrected_mapping[(k,)] = v self.mapping = corrected_mapping @@ -194,72 +188,9 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode if consequent_t not in model.designated_values: return False + # Make sure ordering constraint is met + for premise_t in premise_ts: + if consequent_t < premise_t in model.ordering: + return False + return True - - -def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction]): - last_set: Set[ModelValue] = set() - current_set: Set[ModelValue] = initial_set - - while last_set != current_set: - last_set = deepcopy(current_set) - - for mfun in mfunctions: - # Get output for every possible input configuration - # from last_set - for args in product(*(last_set for _ in range(mfun.arity))): - current_set.add(mfun(*args)) - - return current_set - -def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> bool: - """ - Tells you whether a model violates the - variable sharing property. - """ - - impfunction = interpretation[Implication] - - # Compute I the set of tuples (x, y) where - # x -> y does not take a designiated value - I: Set[Tuple[ModelValue, ModelValue]] = set() - - for (x, y) in product(model.carrier_set, model.carrier_set): - if impfunction(x, y) not in model.designated_values: - I.add((x, y)) - - print("I", [(str(x), str(y)) for (x, y) in I]) - - # Construct the powerset without the empty set - s = list(I) - I_power = chain.from_iterable(combinations(s, r) for r in range(1, len(s) + 1)) - # ((x1, y1)), ((x1, y1), (x2, y2)), ... - - for xys in I_power: - # Compute the closure of all operations - # with just the xs - xs = {xy[0] for xy in xys} - carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations) - - # Compute the closure of all operations - # with just the ys - ys = {xy[1] for xy in xys} - carrier_set_right: Set[ModelValue] = model_closure(ys, model.logical_operations) - - # If the carrier set intersects, then we violate VSP - if len(carrier_set_left & carrier_set_right) > 0: - continue - # print("FAIL: Carrier sets intersect") - # print(xys) - # return True - - for (x2, y2) in product(carrier_set_left, carrier_set_right): - if impfunction(x2, y2) in model.designated_values: - continue - print(f"({x2}, {y2}) take on a designated value") - return True - - return True - - return False -