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
+model_size = 2
-# solutions = generate_model(R_logic, model_size, print_model=True)
+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))

README.md

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

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:
+            if num_solutions >= 0 and len(satisfied_models) >= num_solutions:
-                return solutions
+                return satisfied_models
 
-    return solutions
+    return satisfied_models

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
-