Recursive print algorithm

[mbuit82]

Hey Ben, I've been working on the recursive print algorithm and I got it working (as in not crashing; not necessarily correct hahaha). Here's what the function prints for input premises = ['\\neg A','(A \\boxright (B \\vee C))'] and conclusions = ['(A \\boxright B)','(A \\boxright C)']:

A is False
(A \boxright (B \vee C)) is False because:
A is False
A-alternatives to a = {'b', 'c'}
eval world is now b
(B \vee C) is False because:
B is False
C is True
eval world is now c
(B \vee C) is False because:
B is True
C is False
\neg (A \boxright B) is True because:
(A \boxright B) is False because:
A is False
A-alternatives to a = {'b', 'c'}
eval world is now b
B is False
eval world is now c
B is True
\neg (A \boxright C) is True because:
(A \boxright C) is False because:
A is False
A-alternatives to a = {'b', 'c'}
eval world is now b
C is True
eval world is now c
C is False```

[mbuit82]

I ended up having to edit a lot of stuff across many files to make it work, and I also worked with an old version of the files (locally), so it will take some time to push the changes unfortunately

[benbrastmckie]

Hey that's great you got it working! Are you able to push a new branch? I made quite a lot of changes to get things packaged and easy to use, but the changes I made should be pretty easy to separate. We can discuss more later today.

[mbuit82]

I might be able to get started on that—I'll get it done probably right before the meeting. Also, in case you saw this in the output above, I fixed the error for the verifiers of \\vee

[mbuit82]

embedded counterfactuals (as in (A \\boxright (B \\boxright C))) should now be working, if you want to give it a try. Let me know if you run into problems for debugging

[benbrastmckie]

I gave it a try but am getting some repeated print statements (this was before the last push). I tried to figure out what the problem was but it wasn't clear to me. I included an extra print statement in print_props where it shows the repeats is coming from self.extensional_propositions. Those seem to be defined in terms of find_subsentences_of_kind where I suspect the issue is. I tried using a set and list to also sort the sentences as follows:

def find_subsentences_of_kind(prefix_sentences, kind):
    '''used to find the extensional, modal, and counterfactual sentences. 
    kind is a string, either "extensional", "modal", "counterfactual", or 'all' for a tuple of
    of the three kinds in the order extensional, modal, counterfactual, and then all the subsents
    returns a list of that kind'''
    all_subsentences = set()
    for prefix_sent in prefix_sentences:
        # TODO: linter says cannot access member "append" for type "Literal[True]" Member "append" is unknown
        sub_sents = all_subsentences_of_a_sentence(prefix_sent)
        all_subsentences.update(sub_sents)
    list_subsentences = (list(all_subsentences)).sort()
    if kind == 'extensional':
        return_list = [sent for sent in list_subsentences if is_extensional(sent)]
    if kind == 'modal':
        return_list = [sent for sent in list_subsentences if is_modal(sent)]
    if kind == 'counterfactual':
        return_list = [sent for sent in list_subsentences if is_counterfactual(sent)]
    if kind == 'all':
        counterfactual = [sent for sent in list_subsentences if is_counterfactual(sent)]
        modal = [sent for sent in list_subsentences if is_modal(sent)]
        extensional = [sent for sent in list_subsentences if sent not in counterfactual and sent not in modal]
        return (extensional, modal, counterfactual, list_subsentences)
    return repeats_removed(return_list)

I can't test this since it is not running currently but that was the thought. Although I think we should try to start only working on branches given the current complexity of the project, it is also important to test that local changes work before pushing. But no worries about the last push.

[mbuit82]

That's a good point, it is a good idea to start working on branches (sorry about the last push). I also noticed this and I think it is now fixed.

[benbrastmckie]

No worries! And nice work with the fix! It's printing great. Feel free to ignore the branches I created, but also feel free to create and push new branches as needed.

[benbrastmckie]

I got the printing working reasonably well. There may be some more minor changes I'll make at some point, but it reads pretty well right now.

[benbrastmckie]

I think I've gotten a little clearer on the rec_print function. Here is some pseudo code:

def print_ext_prop(prop,world,indent):
    print("{indent}|{sentence(prop)}| = {vers_fals(prop)} is {truth_val(prop, world)} in {state(world)}")
    if 'neg' in prop:
        indent =+ 1
        arg = prop[1]
        print_ext_prop(arg,world,indent)
    if 'wedge' in prop:
        indent =+ 1
        arg_1 = prop[1]
        arg_2 = prop[2]
        print_ext_prop(arg_1,world,indent)
        print_ext_prop(arg_2,world,indent)
    if 'vee' in prop:
        etc
    if 'rightarrow' in prop:
        etc
    if 'leftrightarrow' in prop:
        etc

def print_modal_prop(prop,world,indent):
    print("{indent}|{sentence(prop)}| = {vers_fals(prop)} is {truth_val(prop, world)} in {state(world)}")
    indent =+ 1
    arg = prop[1]
    for u in all_worlds:
        rec_print(arg,u,indent)
    return

def print_ext_prop(prop,world,indent):
    print("{indent}|{sentence(prop)}| = {vers_fals(prop)} is {truth_val(prop, world)} in {state(world)}")
    indent =+ 1
    arg_1 = prop[1]
    arg_2 = prop[2]
    # might make sense to both print and return alt_worlds
    alt_worlds = find_print_alt_worlds(arg_1,world,indent) 
    indent =+ 1
    for u in alt_worlds:
        rec_print(arg_2,u,indent)

def rec_print(prop, world, indent):
    operator = prop[0]
    if 'Box' == operator or 'Diamond' == operator:
        print_modal_prop(prop,world,indent)
        return
    if 'boxright' == operator:
        print_cf_prop(prop,world,indent)
        return
    print_ext_prop(prop,world,indent)

I think this basically is how it works, but some minor changes. Not all the names match, but hopefully clear enough what each thing is.

[benbrastmckie]

I changed comparison world to input world where this is input by the user. This world shouldn't have to ever change. However, the function doing the printing etc should take a world as an argument, updating this argument on recursive calls when evaluating counterfactuals. If we go that way, do we need update_comparison_world?

I'm also a little confused about the self.prop_dict["alternative worlds"] since which worlds are alternatives depends on both the evaluation world in question (could be the input_world or not) as well as on the antecedent of the counterfactual in question. Perhaps I've missed something but curious to get a better sense of this part.

[mbuit82]

Yeah, so suppose we have a Proposition object with prop_object. Say its prefix form, found by prop_object['prefix expression]], is some phi. prop_object['comparison world'] (formerly prop_object['input world']) is a world and prop_object['alternative worlds'] is a set of worlds such that the phi-alternatives to prop_object['comparison world'] are prop_object['alternative worlds']. What you have in mind as the world which does not change and are calling input world is defined in the model structure (by the self.eval_world attribute of ModelStructure, which never changes, and which will have a better name in the next push, something like main world or input world).

When an extensional Proposition object is initialized, it gets by default its comparison world as the model's input world (the immutable one), and the alt worlds are calculated from that. However in the case of evaluating a counterfactual, the comparison world changes, in which case the update_comparison_world method is necessary.

This way of doing things should work but in editing it I am realizing that it is perhaps not the most intuitive and results in lots of unnecessary computations. I'm going to try to get rid of those two things in the next push.

[benbrastmckie]

That helps! I there is something odd about having the prop_object be something that can be updated. I think what would make more sense is to store a dictionary which associates a set of alternative worlds to each world. Then the prop_object would never change, and if we wanted to loop over the alternative worlds to a given world w which make prop_object true, we could use the dictionary stored in prop_object to look up the alternative worlds associated with w. What do you think about that alternative?

Regarding a name for the fixed world, I think "designated_world" might be a good choice. I'll change input world to that, but wanted to flag it here. Then the world of evaluation can be called "eval_world" which will start off as the designated world but could change depending.

[mbuit82]

Yeah, I think an alternative along those lines would be better—I think even better would be only to calculate the alt worlds when they're needed, because they're not even needed that often and in any case where we store all potentially relevant alt worlds we're doing a lot of unnecessary stuff

[benbrastmckie]

Nice, calculating as we go sounds ideal. Maybe the update_world function could be made to do that instead, amounting to a minor change.

[mbuit82]

I just pushed stuff to a new branch called fix_rec_print which gets rid of the need for keeping track of any of that stuff in the Proposition objects. I also updated the find_complex_proposition function so that modals are verified or falsified not by sets of all worlds, but by the null state. Let me know if it gives seemingly incorrect results. I haven't gotten the time to clean it up, so it is still messy (don't merge it with main branch yet, I'll clean some stuff up tonight, just need to eat and do other stuff beforehand).

[benbrastmckie]

Awesome! I'll check it out and let you merge the branch when you are happy with it.

[benbrastmckie]

Just took a look and made one note. It's looking good. I made minor changes to find_complex_proposition, adding an eval_world argument so that we could get the correct assignments for counterfactual sentences. I also started thinking about refactoring print_evaluation and made a note there. I seem to have succeeded in refactoring print_verifiers_and_falsifiers to avoid some redundancy and cleaned up print_states. I'm going to try to do something similar for save_to and print_to.

[mbuit82]

Sounds good! Here is what rec_print currently looks like:

def rec_print(self, prop_obj, world_bit, output, indent=0):
        """recursive print function (previously print_sort)
        returns None"""
        N = self.N
        prop_obj.print_verifiers_and_falsifiers(world_bit, indent, output)
        if str(prop_obj) in [str(atom) for atom in self.sentence_letters]:
            return
        prefix_expr = prop_obj["prefix expression"]
        op = prefix_expr[0]
        first_subprop = self.find_proposition_object(prefix_expr[1])
        indent += 1 # begin subcases, so indent
        if "neg" in op:
            self.rec_print(first_subprop, world_bit, output, indent)
            return
        if 'Diamond' in op or 'Box' in op:
            for u in self.world_bits:
                self.rec_print(first_subprop, u, output, indent)
            return
        left_subprop = first_subprop
        right_subprop = self.find_proposition_object(prefix_expr[2])
        if "boxright" in op:
            assert (
                left_subprop in self.extensional_propositions
            ), "{prop} not a valid cf because antecedent {left_subprop} is not extensional"
            left_subprop_vers = left_subprop['verifiers']
            phi_alt_worlds_to_world_bit = self.find_alt_bits(left_subprop_vers, world_bit)
            alt_worlds_as_strings = {bitvec_to_substates(u,N) for u in phi_alt_worlds_to_world_bit}
            print(
                f'{"  " * indent}'
                f'{left_subprop}-alternatives to {bitvec_to_substates(world_bit, N)} = '
                f'{make_set_pretty_for_print(alt_worlds_as_strings)}',
                file=output
            )
            self.rec_print(left_subprop, world_bit, output, indent)
            indent += 1
            for u in phi_alt_worlds_to_world_bit:
                self.rec_print(right_subprop, u, output, indent)
            return
        self.rec_print(left_subprop, world_bit, output, indent)
        self.rec_print(right_subprop, world_bit, output, indent)

It's definitely clearer, but refactoring it like you were thinking may be nice. What do you think? If we refactor, I was thinking of putting the helper functions in model_definitions because they don't really need to be methods of the ModelStructure class.

[mbuit82]

I just pushed everything and merged. I think most of the things you did ended up being undone, so you may have to add them again (sorry!). I did a quick test run and it works, lmk if it doesn't on your end

[benbrastmckie]

Hey just went through it and it's looks great!

As for moving helper functions into model_definitions, I think it makes a lot of sense to reduce the number of methods in the class. I'll add "move helper functions to model_definitions as a general TODO. I'll do the same for print_to and save_to which I'm trying to improve.

[benbrastmckie]

I finished fixing up print_to and save_to. The only remaining thing to do on the printing is to move as much as possible from model_structure to model_definitions. I wonder if it might make sense to start a new module for all of the printing related helper functions, leaving model_definitions for the more semantics elements. There might also be elements in model_structure or model_definitions that would make sense to move to syntax. Otherwise it's looking really clean!

[mbuit82]

Sounds good! I'll start documenting things and in that process it'll become clear what would move where. I think that having another file called print_helpers.py (and renaming model_definitions to something more specific maybe) or something to that effect may be helpful. I'll let you know what I think once I add docstrings.

[benbrastmckie]

Awesome sounds great! I just pushed a patch for the disjunctive conclusions feature I added. Seems to be working well. I'm going to see if I can figure out how to write unite tests so that I can avoid testing all of the examples one by one before merging new features.

[mbuit82]

You mentioned that there were some functions that might make sense to move to syntax. Do you have any in mind?

[benbrastmckie]

I looked through it and couldn't find anything. I remember saying that, but I think it was just to double check that nothing should be moved. It's cleaning up nicely!

[mbuit82]

Ah gotcha. Also, as a general rule of thumb, I was thinking it'd be nice most of the methods for the ModelStructure class were printing methods, and everything the user would want to otherwise see could be accessible by the attributes or the Proposition class. Now, the user can find a proposition by inputting an infix sentence into the find_proposition_object method of ModelStructure. The next steps for me are to write that function that adds double backslashes to everything, and try to reorganize model_definitions.

[benbrastmckie]

That sounds great! We're getting close!

[benbrastmckie]

I've been going back through print_verifiers_and_falsifiers and wondering if update_verifiers is in fact needed. Currently if occurs as follows in model_structure.py:

    def print_verifiers_and_falsifiers(self, eval_world, print_impossible=False, indent=0, output=sys.__stdout__):
        """prints the possible verifiers and falsifier states for a sentence.
        used in: rec_print() 
        ensures eval_world is in fact the eval_world for CFs"""
        N = self.state_space.N
        truth_value = self.truth_value_at(eval_world)
        # CHECK: I think this does no work
        if 'boxright' in str(self["prefix expression"][0]):
            self.update_verifiers(eval_world)
...

This function gets called in rec_print as a method of the proposition object. If this update_verifiers is needed, what is a case where it makes a difference?

[benbrastmckie]

I ran some tests and it can't see that update_verifiers is needed. I am also uncertain that is_modal is needed in the following:

def evaluate_modal_expr(model_structure, prefix_modal, eval_world):
    '''evaluates whether a counterfatual in prefix form is true at a world (BitVecVal).
    used to initialize Counterfactuals
    returns a bool representing whether the counterfactual is true at the world or not'''
    op, argument = prefix_modal[0], prefix_modal[1]
    # if is_modal(argument):
    #     if model_structure.evaluate_modal_expr(prefix_modal) is True: # ie, verifiers is null state
    #         return True # both Box and Diamond will return true, since verifiers is not empty
    #     return False
    if 'Diamond' in op:
        for poss in model_structure.poss_bits:
            if poss in find_complex_proposition(model_structure, argument, eval_world)[0]:
                return True
        return False
    if 'Box' in op:
        for poss in model_structure.poss_bits:
            if poss in find_complex_proposition(model_structure, argument, eval_world)[1]:
                return False
        return True

My hope is to remove all unnecessary elements, simplifying the code.

[benbrastmckie]

I think this is resolved, or at least old and likely to get refactored significantly.