diff --git a/R.py b/R.py index 4eea77b..ee5b96e 100644 --- a/R.py +++ b/R.py @@ -11,7 +11,7 @@ from logic import ( Disjunction, Rule, ) -from model import Model, ModelFunction, ModelValue +from model import Model, ModelFunction, ModelValue, violates_vsp from generate_model import generate_model @@ -71,26 +71,26 @@ a1 = ModelValue("a1") carrier_set = {a0, a1} -mnegation = ModelFunction({ +mnegation = ModelFunction(1, { a0: a1, a1: a0 }) -mimplication = ModelFunction({ +mimplication = ModelFunction(2, { (a0, a0): a1, (a0, a1): a1, (a1, a0): a0, (a1, a1): a1 }) -mconjunction = ModelFunction({ +mconjunction = ModelFunction(2, { (a0, a0): a0, (a0, a1): a0, (a1, a0): a0, (a1, a1): a1 }) -mdisjunction = ModelFunction({ +mdisjunction = ModelFunction(2, { (a0, a0): a0, (a0, a1): a1, (a1, a0): a1, @@ -122,3 +122,6 @@ 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}") +for smodel in satisfiable_models: + print(violates_vsp(smodel[0], smodel[1])) + diff --git a/README.md b/README.md new file mode 100644 index 0000000..6e0ed93 --- /dev/null +++ b/README.md @@ -0,0 +1,6 @@ +# 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 11108b2..88b9bc9 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 +from typing import Set, List, Dict, Tuple 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(new_function, operation.symbol) + yield ModelFunction(arity, 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): +def generate_model(logic: Logic, number_elements: int, num_solutions: int = -1, print_model=False) -> List[Tuple[Model, Dict[Operation, ModelFunction]]]: 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) - satisfied_models = [] + solutions: List[Tuple[Model, Dict[Operation, ModelFunction]]] = [] for designated_values in possible_designated_values: designated_values = set(designated_values) print("Considering models for designated values", set_to_str(designated_values)) @@ -126,11 +126,12 @@ def generate_model(logic: Logic, number_elements: int, num_solutions: int = -1, break if is_valid: - satisfied_models.append(model) + solutions.append((model, interpretation)) + # satisfied_models.append(model) if print_model: print(model, flush=True) - if num_solutions >= 0 and len(satisfied_models) >= num_solutions: - return satisfied_models + if num_solutions >= 0 and len(solutions) >= num_solutions: + return solutions - return satisfied_models + return solutions diff --git a/model.py b/model.py index b2a80ed..1518aa1 100644 --- a/model.py +++ b/model.py @@ -4,11 +4,13 @@ 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 +Operation, Conjunction, Disjunction, Implication ) -from typing import Set, List, Dict, Tuple, Optional -from itertools import product +from typing import Set, Dict, Tuple, Optional from functools import lru_cache +from itertools import combinations, chain, product +from copy import deepcopy + __all__ = ['ModelValue', 'ModelFunction', 'Model'] @@ -33,17 +35,21 @@ class ModelValue: class ModelFunction: - def __init__(self, mapping, operation_name = ""): + def __init__(self, arity: int, 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 @@ -188,9 +194,69 @@ 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 violates_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> bool: + """ + Tells you whether a model violates the + variable sharing property. + + If it returns false, it is still possible that + the variable sharing property is violated + just that we didn't check for the appopriate + subalgebras. + """ + + 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)) + + # 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: + print("FAIL: Carrier sets intersect") + return True + + for (x2, y2) in product(carrier_set_left, carrier_set_right): + if impfunction(x2, y2) in model.designated_values: + print(f"({x2}, {y2}) take on a designated value") + return True + + return False