matmod/generate_model.py

159 lines
5.8 KiB
Python
Raw Permalink Normal View History

2024-04-08 23:59:21 -04:00
"""
2024-05-28 16:05:06 -04:00
Generate all the models for a given logic
with a specified number of elements.
2024-04-08 23:59:21 -04:00
"""
2024-04-15 00:08:00 -04:00
from common import set_to_str
2024-05-04 16:51:49 -04:00
from logic import Logic, Operation, Rule, get_operations_from_term
2024-05-28 16:05:06 -04:00
from model import (
Interpretation, ModelValue, Model,
2024-05-29 13:50:20 -04:00
ModelFunction, satisfiable
2024-05-28 16:05:06 -04:00
)
2024-04-08 23:59:21 -04:00
from itertools import combinations, chain, product
2024-05-29 13:50:20 -04:00
from typing import Set, List, Tuple
2024-04-08 23:59:21 -04:00
def possible_designations(iterable):
"""Powerset without the empty and complete set"""
s = list(iterable)
return chain.from_iterable(combinations(s, r) for r in range(1, len(s)))
def possible_functions(operation, carrier_set):
2024-05-28 16:05:06 -04:00
"""
Create every possible input, output pair
for a given model function based on an
operation and a carrier set.
"""
2024-04-08 23:59:21 -04:00
arity = operation.arity
2024-05-04 16:51:49 -04:00
inputs = list(product(carrier_set, repeat=arity))
possible_outputs = product(carrier_set, repeat=len(inputs))
2024-04-08 23:59:21 -04:00
for outputs in possible_outputs:
assert len(inputs) == len(outputs)
new_function = dict()
for input, output in zip(inputs, outputs):
new_function[input] = output
2024-04-21 12:15:24 -04:00
2024-05-03 13:06:52 -04:00
yield ModelFunction(arity, new_function, operation.symbol)
2024-04-08 23:59:21 -04:00
2024-04-15 00:08:00 -04:00
2024-05-28 16:05:06 -04:00
def only_rules_with(rules: Set[Rule], operation: Operation) -> List[Rule]:
"""
Filter the list of rules in a logic to those
that only contain the logical operation specified.
"""
result_rules: List[Rule] = []
2024-04-15 00:08:00 -04:00
for rule in rules:
is_valid = True
2024-05-28 16:05:06 -04:00
# Go through every term in the premises and conclusion
2024-04-15 00:08:00 -04:00
for t in (rule.premises | {rule.conclusion,}):
t_operations = get_operations_from_term(t)
2024-05-28 16:05:06 -04:00
# Make sure there's only one operation
# and that it matches the operation specified
2024-04-15 00:08:00 -04:00
if len(t_operations) > 1:
is_valid = False
break
if len(t_operations) == 0:
continue
t_operation = next(iter(t_operations))
if t_operation != operation:
is_valid = False
break
if is_valid:
result_rules.append(rule)
return result_rules
def possible_interpretations(
logic: Logic, carrier_set: Set[ModelValue],
2024-05-28 16:05:06 -04:00
designated_values: Set[ModelValue]):
"""
Consider every possible interpretation of operations
within the specified logic given the carrier set of
model values, and the set of designated values.
"""
operations: List[Operation] = []
model_functions: List[List[ModelFunction]] = []
2024-04-08 23:59:21 -04:00
for operation in logic.operations:
operations.append(operation)
2024-04-15 00:08:00 -04:00
candidate_functions = list(possible_functions(operation, carrier_set))
2024-05-28 16:05:06 -04:00
passed_functions: List[ModelFunction] = []
2024-04-15 00:08:00 -04:00
"""
2024-05-28 16:05:06 -04:00
Discard candidate functions that don't pass
the rules that only contain the given
logical operation.
2024-04-15 00:08:00 -04:00
"""
restricted_rules = only_rules_with(logic.rules, operation)
if len(restricted_rules) > 0:
small_logic = Logic({operation,}, restricted_rules)
2024-05-28 16:05:06 -04:00
# Add candidate functions whose small model
# and logic are satisfied given the restricted
# rule set.
2024-04-15 00:08:00 -04:00
for f in candidate_functions:
2024-05-28 16:05:06 -04:00
small_model = Model(carrier_set, {f,}, designated_values)
2024-04-15 00:08:00 -04:00
interp = {operation: f}
if satisfiable(small_logic, small_model, interp):
passed_functions.append(f)
else:
passed_functions = candidate_functions
if len(passed_functions) == 0:
raise Exception("No interpretation satisfies the axioms for the operation " + str(operation))
else:
print(
f"Operation {operation.symbol} has {len(passed_functions)} candidate functions"
)
model_functions.append(passed_functions)
2024-04-08 23:59:21 -04:00
2024-05-28 16:05:06 -04:00
# The model_functions variables contains
# the candidate functions for each operation.
2024-04-08 23:59:21 -04:00
functions_choice = product(*model_functions)
2024-05-28 16:05:06 -04:00
# Assign a function to each operation
2024-04-08 23:59:21 -04:00
for functions in functions_choice:
assert len(operations) == len(functions)
2024-05-28 16:05:06 -04:00
interpretation: Interpretation = dict()
2024-04-08 23:59:21 -04:00
for operation, function in zip(operations, functions):
interpretation[operation] = function
yield interpretation
2024-05-28 16:05:06 -04:00
def generate_model(
logic: Logic, number_elements: int, num_solutions: int = -1,
print_model=False) -> List[Tuple[Model, Interpretation]]:
"""
Generate the specified number of models that
satisfy a logic of a certain size.
"""
2024-04-21 12:15:24 -04:00
assert number_elements > 0
2024-04-08 23:59:21 -04:00
carrier_set = {
ModelValue("a" + str(i)) for i in range(number_elements)
}
possible_designated_values = possible_designations(carrier_set)
2024-05-28 16:05:06 -04:00
solutions: List[Tuple[Model, Interpretation]] = []
2024-04-15 00:08:00 -04:00
for designated_values in possible_designated_values:
2024-04-08 23:59:21 -04:00
designated_values = set(designated_values)
2024-04-15 00:08:00 -04:00
print("Considering models for designated values", set_to_str(designated_values))
2024-05-28 16:05:06 -04:00
possible_interps = possible_interpretations(logic, carrier_set, designated_values)
2024-04-15 00:08:00 -04:00
for interpretation in possible_interps:
is_valid = True
2024-05-28 16:05:06 -04:00
model = Model(carrier_set, set(interpretation.values()), designated_values)
2024-04-15 00:08:00 -04:00
# Iteratively test possible interpretations
# by adding one axiom at a time
for rule in logic.rules:
small_logic = Logic(logic.operations, {rule,})
if not satisfiable(small_logic, model, interpretation):
is_valid = False
break
2024-04-21 12:15:24 -04:00
2024-04-15 00:08:00 -04:00
if is_valid:
2024-05-03 13:06:52 -04:00
solutions.append((model, interpretation))
2024-04-15 00:08:00 -04:00
if print_model:
print(model, flush=True)
2024-04-21 12:15:24 -04:00
2024-05-03 13:06:52 -04:00
if num_solutions >= 0 and len(solutions) >= num_solutions:
return solutions
2024-04-15 00:08:00 -04:00
2024-05-03 13:06:52 -04:00
return solutions