class semantics approach

[mbuit82]

I started a new branch with some work on the class semantics. It has two new files: class_semantics_playground.py and class_semantics_example.py. Both have docstrings explaining some things and problems I ran into. Something I didn't mention there but is worth saying is there is a new class called a Frame class—it effectively replaces the semantics; if there is a better name for it by all means feel free to change it (and anything else).

[benbrastmckie]

Hey this is off to a great start! I added comments throughout the files you created and just pushed the changes. I have been trying to get it to run, and it looks close, but couldn't quite finish debugging it. I'm curious to know if you can get it to run.

[mbuit82]

Glad to hear you think it's off to a great start! I only really wrote the code to get the idea out there, I never actually tried it, so that could explain the bugs you're getting—I'm sure there's bits of crucial machinery from the old approach that haven't been copy/pasted in here.

I saw your comments and based off them I think it is possible to make an operator class to make them more modular—I'll give that a try.

Update after trying to make the class: making the class depends on which methods will be shared by all operators and whether there will be any special methods/attributes that a specific operator would have, if any (the question of how a frame would access those is relevant here I think)

[benbrastmckie]

Having done a bit more thinking about the class semantics, here are some classes that I think will be important to define:

1. ModelSetup class for storing user inputs and their results:
   • settings and flags
   • premises and conclusions
   • prefix premises and conclusions
   • all subsentences of the premises and conclusions
   • sentence letters
   • Z3 constraints including (drawing on methods from semantics and operator classes):
     • frame constraints
     • model constraints (currently called proposition constraints)
     • premise constraints
     • conclusion constraints
2. A Operator class for each primitive operator in the language including:
   • attribute for arity
   • methods for truth and falsity at a world
   • methods for verification and falsification at a world
   • printing methods
3. Semantics class including:
   • Z3 primitives: verify, falsify, possible, w
   • methods for later finding the following after a Z3 model is found:
     • all bits, possible bits, world bits, main world bit
     • verify, falsify
   • methods for operating on states: fusion, parthood, etc.
   • methods for truth and falsity at a world given an operator
   • method providing the frame constraints
   • method providing model constraints (assigning each sentence letter to a proposition)
4. Proposition class which stores:
   • prefix sentence, infix sentence
   • verifiers, falsifiers (drawing on methods coming from the Semantics class)
   • method for truth value at a world
   • methods for printing a proposition
5. ModelStructure class given a ModelSetup instance as input is used to store:
   • all relevant attributes coming from the ModelSetup
   • resulting Z3 model including:
     • timeout value
     • model status
     • Z3 model
     • model runtime
   • all propositions for the subsentences of the premises and conclusions
   • methods for printing
   • methods for saving output

The hope with organizing things this way (subject to changes) is that the classes 1 and 5 could be suppressed, and only 2-4 exposed. By defining 2-4, one could then rely on the general functionality provided by 1 and 5 in order to set up a semantics. We could also include various helper functions that would also be suppressed. The thought would be that the model checker will come with some default semantics, but running model-checker -n would generate a python file for adapting the definitions of the classes provided in 2-4. This could be a template or a copy of the default semantics. Then one could run that script where some main function would use those definitions to override parts of the default semantics. If need be, we could include 1 and 5 in redefining the default semantics for a new system, but it would be good to try to suppress as much as possible while exposing key elements.

I imagine this can all be improved, but hopefully provides a reasonable overview.

[mbuit82]

Yeah that all sounds really good and I think gets around the previous problems we were having in the old attempt—it should be possible (I hope). I agree that it would be good to hide 1 and 5, ideally users get less objects to customize just to keep things simple, but get lots of room to customize what they do get. I can give this all a try before tomorrow's meeting to hopefully be able to discuss any implementation/design challenges then!

[benbrastmckie]

Great meeting today! I created these notes which goes over the high level architecture with minor revisions and also added a plan to the TODO.md. Although we may need to return at times to make tweaks, I think we have about finished with the architecture phase and on to implementation. I'll leave this issue open for high level topics.

[benbrastmckie]

Although it is still a ways off, I'm starting to think about the main function that will compose the various classes.
I haven't added it to the TODOs, but was thinking it would go roughly like this:

1. the Semantics and Operator classes are passed to a ModelSetup class instance which:
   • stores all user inputs and flags
   • stores Z3 constraints by calling on the Semantics and relevant Operator classes
2. the ModelSetup instance is passed to ModelStructure which:
   • finds and stores the Z3 model
   • builds the relevant state representations
   • runs general print and save methods are called depending on the settings and flags

In (1), I'm wondering what the best way to pass Operator classes into ModelSetup while permitting the number of Operator classes to remain flexible since some semantic systems may require more than others.
When it comes time to think about alternative semantic systems, we would simply pass different Semantics and Operator classes into ModelSetup while allowing the user to specify these classes in a script.

If this seems like a reasonable first pass, I'll add it to the TODOs and we can revise it as need be later.
I nevertheless thought it would help to complete the description of the high level architecture before diving in on the implementation.

[mbuit82]

Hey Ben, sounds good! So far no issues in trying to implement this. One small question though—right now in model_checker there is no ModelStructure class (only StateSpace). For the new approach were you thinking that what is currently StateSpace becomes ModelStructure or to have both?

[benbrastmckie]

ModelStructure might be a better choice so as not to presume to much, but both names refer to the same thing.

[mbuit82]

Got it, sounds good!

[benbrastmckie]

Just looked at the new modules. They are looking really good! I added some comments and questions throughout.

One minor issue that is relevant to the overall architecture is that there are a lot of arguments for ModelSetup. This made me wonder if it makes sense to define an Input class where an instance of which can then be passed into ModelSetup alongside instances of Semantics and all the operators. Happy to chat about this tomorrow.

[benbrastmckie]

We concluded that defining an Input class can be added once we start applications if it feels like it would improve the conceptual hygiene. We also discussed grouping the semantics, operators, and Proposition objects together so that users could compare different combinations. We can return to this once we apply the new semantics.

[benbrastmckie]

I moved solve() over to ModelStructure. Since the output of Solve() may vary, I had to add some conditions conditions to make my linter happy. Let me know what you think when you get a chance to take a look.

[mbuit82]

Looks good to me! I just went through and commented some things/removed old comments/answered comments, let me know what you think particularly about the comment on the Proposition class.

[benbrastmckie]

Just reviewed comments. I lke the parent proposition class idea. I renamed things so that the user defined subclass reads: Defined(Proposition). Maybe not the best name, but seems reasonable enough. Happy to change latter if we think of a better name. I also added some linter comments about shortening the dunder methods in the Operator class.

[benbrastmckie]

I have been messing with the hash function in Proposition. Here is what it looks like now with attempts commented below:

def __hash__(self):
    # B: I tried to define a hash function that is consistent with __eq__
    # so that instances with the same verifiers, falsifiers, and prefix_sentence
    # have the same hash but can't access verifiers and falsifiers from here
    return hash(str(self.prefix_sentence))
    # return hash((str(self.prefix_sentence), tuple(self.verifiers, self.falsifiers)))
    # return 0

I also initialized a name so that proposition instances could be added to the all_propositions dictionary:

def __init__(self, prefix_sentence, model_structure):
    self.prefix_sentence = prefix_sentence
    self.model_structure = model_structure
    self.semantics = model_structure.model_setup.semantics
    # B: the below was needed to add instances to all_propositions dictionary
    self.name = str(self.prefix_sentence)

This allowed me to change the Defined(Proposition) subclass init to the following:

def __init__(self, prefix_sentence, model_structure):
    super().__init__(prefix_sentence, model_structure)
    # self.verifiers, self.falsifiers = None, None # for avoiding useless recursion
    self.verifiers, self.falsifiers = self.find_verifiers_and_falsifiers()
    # B: I think the below adds instances to all_propositions dictionary?
    self.model_structure.all_propositions[self.name] = self
    # self.model_structure.all_propositions.add(self)
    # M: applies to any def of Proposition,
    # but needs to be left here because it must happen after find_verifiers_and_falsifiers
    # (more generally, it depends on __eq__, which is user-defined and which in this def 
    # of Propositions depends on verifiers and falsifiers)

It seems to be finding models and printed the following when I ran print("print all props:", model_structure.all_propositions):

print all props: {'[A]': [A], '[B]': [B], '[\\vee, [A], [B]]': [\vee, [A], [B]
], '[\\neg, [\\vee, [A], [B]]]': [\neg, [\vee, [A], [B]]], '[C]': [C], '[D]': 
[D], '[\\wedge, [C], [D]]': [\wedge, [C], [D]], '[\\neg, [B]]': [\neg, [B]], '
[\\neg, [D]]': [\neg, [D]], '[\\wedge, [\\neg, [B]], [\\neg, [D]]]': [\wedge, 
[\neg, [B]], [\neg, [D]]]}

This seems right given that __repr__ is str(self.prefix_sentence) but wanted to flag these changes.

[mbuit82]

Nice! I actually was also playing around with the hash function and found a way to move it to the parent class (so that users don't have to worry about it). I'll push to incorporate that with the changes you've made!

[benbrastmckie]

Hopefully I didn't clobber your changes, but resolved some merge conflicts. It seems to be working.

[benbrastmckie]

The __post_init__ seems to be working great. Really nice to move the dictionary stuff out of the exposed subclass. I made infix a method of model_structure since we weren't using it in ModelSetup and that way we don't need to import it separately (my linter was angry). I left comments with some past attempts but we can clear these out at some point.

[mbuit82]

Sounds good—and actually thinking about it we don't even need the __post_init__ method anymore, that is only needed if all_propositions is a set (because then the definition of __eq__ matters in the adding of the proposition to all_propositions, so it needs to happen after whatever the things __eq__ depends on are defined (in this case, verifiers and falsifiers)

[benbrastmckie]

Oh got it. Seems to all be working though my linter is raising an error for the except clause in the Proposition __init__. Here is what ChatGPT suggests:

class Proposition:
    """Defaults inherited by every proposition."""

    def __init__(self, prefix_sentence, model_structure):
        if self.__class__ == Proposition:
            raise NotImplementedError((not_implemented_string(self.__class__)))
        self.prefix_sentence = prefix_sentence
        self.name = model_structure.infix(self.prefix_sentence)
        self.model_structure = model_structure
        self.semantics = model_structure.model_setup.semantics
        self.non_null = model_structure.model_setup.non_null
        self.contingent = model_structure.model_setup.contingent
        self.model_structure.all_propositions[self.name] = self

    def __repr__(self):
        return self.name

    def __hash__(self):
        # Consistent with __eq__ and avoids dynamic reassignment.
        return hash(self.name)

    # If needed, implement custom equality checks here.
    def __eq__(self, other):
        return isinstance(other, Proposition) and self.name == other.name

This also seems to work, so I commented out the try/except. Not really sure if the above does what we want.

[mbuit82]

The except clauses are necessary if you want to add Proposition objects to a set. The following code in test_example.py raises an error saying that Defined is unhashable:

a = Defined(model_structure.all_propositions['A'].prefix_sentence,model_structure)
{a} 

I'm not entirely clear on why this is (since the parent class has a hash method) but it looks like if you redefine __eq__ in the subclass you also have to redefine __hash__. The exception got around it by, when an object of the subclass is first initiated, adding the hash method of the super class to the subclass. This would only happen once, since after that any instance of the subclass would be hashable and the except block would not be entered. Would the linter's complaint go away if you change the variable from x to self?
Also the reason for having not_implemented_string as a function defined globally is that it is also used in the Operator subclass—sorry I didn't give a comment on that, it probably seemed kind of pointless out of context

[benbrastmckie]

Changing 'x' to 'self' seems to work. Do propositions need to be added to a set if we are using a dictionary? I'm still not totally clear about what the try/except thing is doing but it is working. Also not sure if __eq__ should be changed since this was a ChatGPT idea in place of the try/except clauses.

I turned the not_implemented_string lambda function into a global function. Are there any reasons not to go this way?

I have also been moving helper functions from old_semantic_helpers.py into hidden_helper.py. Nice to keep old_semantic_helpers around, moving functions as needed. If hidden_helper gets too big, we could divide it into modules. I'm using comments to divide it into sections.

[mbuit82]

Propositions don't need to be added to a set if we are using a dictionary, but if we want to let the user define equality then we need to define hash as well—I gave some thoughts in a couple comments in the code.

I think it would be better to have it as its own function—and on the note of moving things into hidden_helpers.py I moved it in there. I agree it would be good to reorganize/clean that up into separate modules based on what they're used for kind of like we did in the current package!

[benbrastmckie]

Just looked at your comments and I think that makes sense. It seems important to think about all this especially in anticipation of setting up the next hyperintensional layer of the semantics.

Perhaps the best thing to do here is to open an issue to document where we stand and what remains. We can then come back to this once the semantics for CFs has been implemented. I'll cut your comments into a new issue.

[mbuit82]

Implemented a way to see if DerivedOperators are defined in terms of each other (and got rid of the error message with the default arg eval_world = eval_world). Having gotten rid of the issue with the default parameter, the new error message was a RecursionError (much more reasonably than the error we got during the meeting). The source of the RecursionError wasn't obvious so the thing I implemented gives an error message and avoids going through the max recursion depth of the run. To see the solution in action, uncomment the second commented line of the derived_definition of ConditionalOperator