diff --git a/R.py b/R.py index 4eea77b..0e565bf 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, has_vsp, satisfiable 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, @@ -117,8 +117,182 @@ interpretation = { # Generate models of R of a given size -model_size = 2 -satisfiable_models = generate_model(R_logic, model_size, print_model=True) +# model_size = 2 +# solutions = 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(solutions)} 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 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..10c69fb 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,72 @@ 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 +