Model of R that has VSP

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))

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).

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

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
+