Data Structure

[benbrastmckie]

I updated strategies to include a section for both the data classes and print algorithms.

With regards to classes, I was thinking it would make sense to keep the classes not too big, and to be divided by the type of elements they include. Right now I have one for Sentences, ModelStructure, and Propositions. We could potentially create one for Print too which would store all the states in a printable form, but I'm not sure this is necessary.

With regards to the print algorithm, I think it is not so complicated after all. It provides a recursive procedure for working through each input sentence, printing the appropriate elements as it moves along. This should handle nested counterfactuals.

I added TODOs for both of these since they seem like the most important elements for now. I will try to keep working on debugging the last issues now that we have unsat_core working and reach out for help with Z3. I will also keep thinking about the overall architecture as a step towards packaging the modules.

[benbrastmckie]

I saw that @mbuit82 added the Uninitalized class. Seems like it fixes the errors we were at risk of getting before though I wonder if something is up with __iter__ in Uninitalized. I'm getting the following error (will also put comments in the code) here:

    def find_alt_bits(self, proposition_verifier_bits, comparison_world=None):
        """
        Finds the alternative bits given verifier bits, possible states, worlds, and
        the evaluation world. Used in Proposition class alternative worlds and Proposition
        class attribute update_comparison_world().
        """
        if comparison_world is None:
            comparison_world = self.eval_world
        alt_bits = set()
        for ver in proposition_verifier_bits:
            comp_parts = find_compatible_parts(ver, self.poss_bits, comparison_world)
            max_comp_ver_parts = find_max_comp_ver_parts(ver, comp_parts)
            # TODO: linter error: "Uninitalized" is not iterable   "__iter__" method does not return an object
            for world in self.world_bits:
                if not bit_part(ver, world):
                    continue
                for max_ver in max_comp_ver_parts:
                    if bit_part(max_ver, world) and world.sexpr():
                        alt_bits.add(world)
                        break  # to return to the second for loop over world_bits
        return alt_bits

Any sense of what is going on here?

[mbuit82]

I think this actually means it's catching on to exactly what it was intended to capture—I remember that making the uninitialized objects be None was weird for debugging, since it would say that a None object is not utterable, but a None object can come up from all over so that is not a very helpful error message. So, I added an __iter__ method to the Uninitialized class so that whenever you iterate over an Uninitialized object, it'll raise an error. My guess is, since the attributes are defined this way in the __init__ method, python reasons "oh, in principle we can run find_alt_bits with the attribute values in __init__, but if we did that, we'd run into an error because self.world_bits is an Uninitialized object, which is not iterable" (which is exactly the point—if we were to run find_alt_bits on a ModelStructure object before runningsolve, we should into an error because there are no alt bits yet). (This way of solving the problem of uninitialized attributes may be completely unkosher, for the record—it may be worth asking someone with experience in software development, like Shromona, if there's a more 'standard' way of initializing objects you don't really want to initialize (and want to be raised an error if they are attempted to be accessed).)

[benbrastmckie]

OK cool. I'll ask her about that.

I was trying to get it to evaluate counterfactuals with nonextensional antecedents. The key change happens in extended_verify and extended_falsify. Here is the former:

        if "boxright" in op or "Box" in op or "neg" in op:
            return true_at(ext_sent, eval_world)
            # raise ValueError(
            #     f"\n\nThe antecedent of a counterfactual conditional must be extensional.\n"
            #     f"The sentence '{Infix(ext_sent)}' is not extensional.\n"
            # )

This gives the error: There is no proposition with prefix expression '\Box A'. This prompted me to change ext_only to False in evaluate_cf_expr:

        ant_prop = self.find_proposition_object(antecedent_expr, ext_only=True)

However, doing so gives the error: cannot iterate through all_propositions because it isn't initialized. I'm not totally sure what is going on here, but figures since we now have a proposition (verifiers and falsifiers) for modal and counterfactual sentences, we should be able to evaluate counterfactuals with modal and counterfactual antencedents.

[mbuit82]

What are your input premises and conclusions? I can try to work on that on the fix_rec_print branch and push all at once

[mbuit82]

Sorry didn't mean to close the issue lol

[benbrastmckie]

I was using this:

premises = ['(Box A boxright B)']
conclusions = []

But anything nonextensional in the antecedent will do. I just merged the verify_cf_modal into fix_rec_print so that the latter has the most recent of everything. Hopefully pulling it down won't have too many conflicts.

[benbrastmckie]

I was thinking about the uninitalized problem in ModelStructure and how big the class is in general. I think it might make sense to divide it into two classes: one that does not require a model to be found; and another that includes everything that comes from the found model. This might have the benefit of making Uninitalized unnecessary.

[mbuit82]

Hey Ben, I was cleaning through things and I was wondering what your reasoning for this is:

def truth_value_at(self, eval_world):
        """finds whether a CF is true at a certain world
        returns a Boolean representing yes or no"""
        # TODO: I suspect we need something more like this
        # null_state = {BitVecVal(0,self.N)}
        # if null_state in self["verifiers"]:

I get the intuition for it but implementing it makes things not work (meaning we'd just need to change some other definitions). What's your reasoning for the alternate implementation—is it so things like (A boxright B) wedge (B boxright C) are understandable?

[mbuit82]

Would a counterfactual be true at a world w (and thus its verifiers should be {null_state}) just in case the counterfactual is true at the current world of evaluation?

[benbrastmckie]

Yes. This raises an issue I was also thinking about. For extensional sentences, their verifiers and falsifiers don't depend on the world of evaluation. Same for modal sentences. But for counterfactuals sentences it is different. They could be true at some worlds and false at others, and so should be verified by the null state at some worlds and not at other worlds. This complicates the the assignment of propositions to counterfactual sentences.

I'm not totally sure what to do about this. It would seem that in order to give uniform treatment of all sentences, propositions would have to be assigned relative to worlds. This may require adding an extra world argument when finding prop_objects. I'm curious to know what you think about this.

[mbuit82]

Give me one second, I'm going to push—implemented the above change. I'll think about what you just said in the meantime

[mbuit82]

I think that world argument is effectively already passed in—for find_complex_proposition, we pass in an eval_world. So we can just use whatever is currently the eval_world. On a slightly separate note, is it still worth it keeping track of which worlds a Counterfactual is true in and which it isn't?

[mbuit82]

Put in slightly informal terms, we don't really need to save the current world we are in when evaluating CFs. We could just make it that whenever we happen to evaluate a CF, we necessarily must note whatever world we are in before evaluating it. This would take advantage of current code and I think would solve the problem

[benbrastmckie]

Oops... missed the first comment. Yes exactly. If we want to be able to assign propositions to extensional combinations of nonextensional sentences, then it is important that all sentences have verifiers and falsifiers. My hope was that this would make things more uniform, reducing the need for different cases depending on the type of sentence.

Ah and now for the third comment... if counterfactuals are going to be assigned to some kind of prop_object, it will have to account for the dependency on the world. So maybe it will get assigned to a dictionary matching worlds to verifier-falsifiers propositions. If this is going to be uniform, then all sentences should get the same treatment. Do you think that makes sense?

[benbrastmckie]

Put in slightly informal terms, we don't really need to save the current world we are in when evaluating CFs. We could just make it that whenever we happen to evaluate a CF, we necessarily must note whatever world we are in before evaluating it. This would take advantage of current code and I think would solve the problem

OK great! That sounds like a good plan!

[benbrastmckie]

I'm going to work on the verify_cf_modal branch even though I'm doing a bunch of random things. I'll hold off merging changes into master unless I finish something significant.

[mbuit82]

Sounds good--what are you working on in that branch? To make sure we aren't doing the same thing in different places and make merging a mess

[benbrastmckie]

Right now I'm working on unit testing. I'll stay clear of all of the main modules.

[mbuit82]

Sounds good—I'll work on the cf verifiers issue

[mbuit82]

Just pushed to master. In moving things around I realized that each of the subclasses for Propositions ended up being used not that much. So I just put everything into the big Proposition class and commented the subclasses out. This has the added benefit that if a user wants to make Proposition objects, the program automatically makes them of the right kind—before, you could in principle pass in an extensional prefix sentence into Counterfactual() to make a "counterfactual" proposition (though it wouldn't be, and that would cause problems). I'm going to start looking at helper functions, refactoring, and reorganizing the files

[mbuit82]

My general idea for moving things around is that if a user would find use in that method, it should be in model_structure; otherwise it goes in model_definitions (/the files that come from that). What do you think—is there any other criteria which should be considered for moving things around?

[benbrastmckie]

I think that all sounds great. Nothing is permanent, so if there is reason to moving things back down the line, we can do that. But I think for now moving as much as we can makes good sense.

[benbrastmckie]

I managed to divide the ModelStructure class into two. I still suspect that it can be simplified and improved. I'm curious to know if you think it is any improvement (I'm not entirely sure). We can always revert back if the original way has advantages.

Something else I was thinking about is making ModelStructure a subclass of ModelSetup or vice versa. I'm not too sure what is best. I'll see if I can track down some advice.

[benbrastmckie]

I am trying to make the find_proposition functions more uniform, but have been running into some issues that I can't seem to figure out. Here is what I have found (working on the model_structure branch):

# premises = ['Box A','(A boxright B)'] # no
# premises = ['neg A','(A boxright B)'] # yes
# premises = ['neg A','(neg A boxright B)'] # no
# premises = ['A','(neg A boxright B)'] # yes
# premises = ['A','(Box A boxright B)'] # yes
# premises = ['Box A','(Box A boxright B)'] # no
# premises = ['((C boxright D) boxright B)'] # no
premises = ['(neg (C boxright D) boxright B)'] # yes
conclusions = []

I added some # PROB where it seems to be stuck in a loop. In any case, no rush, but if you have a chance to take a look at this, I'm curious if you can see what is going wrong. Perhaps there is a better way to achieve something similar where there is one function which can assign any prefix sentence to the appropriate proposition.

[benbrastmckie]

I managed to get it working though I noticed there is a slow down. Not sure what is causing this but have held back from merging simp_find_props until the slow down if fixed.

[benbrastmckie]

I fixed the slow down, but noticed another problem. Try running the following:

# SOBEL SEQUENCE (N = 3)
premises = [
    '(A boxright X)', # 0.03 seconds locally
    'neg ((A wedge B) boxright X)', # 14.8 seconds locally
    '(((A wedge B) wedge C) boxright X)', # 4.9 seconds locally
    'neg ((((A wedge B) wedge C) wedge D) boxright X)', # 7.8 seconds locally
]
conclusions = []

Right now it is printing the following (I only included the main statements):

1.  |(A \boxright X)| = < {□}, ∅ >  (True in b.c)
2.  |\neg ((A \wedge B) \boxright X)| = < {□}, ∅ >  (True in b.c)
3.  |(((A \wedge B) \wedge C) \boxright X)| = < {□}, ∅ >  (True in b.c)
4.  |\neg ((((A \wedge B) \wedge C) \wedge D) \boxright X)| = < ∅, {□} >  (False in b.c)

Note that the final statement is false. This is not correct. Or rather, the model does make that premise false, but shouldn't thereby count as a model since it doesn't make all of the premises true. I went pretty far back in the git history and it looks like this is just something I overlooked and was always present. I checked pretty carefully and can't quite see why it counts as a model if one of the premises is false.

[mbuit82]

Small note: I changed make_model_for to now return only a ModelStructure object. Since the ModelSetup object is always stored as an attribute of the ModelStructure object, it can always be accessed, and it makes the user functionality side of things more intuitive. (I changed the corresponding places in the code also in __main__.py so it should work without bugs.) Just thought I'd mention this somewhere in case you strongly prefer it returning both objects

[benbrastmckie]

I ran pytest but all tests failed. I think there may be a better way to define classes but this should be developed on a separate branch and fully tested before merging. But it's a good idea, and I'll think about how that might go.

I pushed the recent commits to a new branch refactor_data. For the time being I'm going to roll back master to before these changes. Even without the breaking changes, I noticed that some of the other changes made it stop printing in color. I'll leave this branch, but it may be best to start a fresh branch for integrating ModelSetup and ModelStructure.

[benbrastmckie]

I started thinking about how to refactor things and remembered why I divided the classes at the point I did. The thought was that ModelSetup gives us everything Z3 needs to look for a model. Whatever it finds is then passed to ModelStructure. But I don't see why that same thing can't happen inside a single class. I just tested and merged changes into master.