Refactor Print

[benbrastmckie]

The print functions are mostly working great, and it is not too complicated yet. But once we connect the sentence parsing functions which map input_sentences to sentence_letters, ext_sentences, cf_sentences, and neg_cf_sentences, we will want to add some new layers to print. In anticipation of this, I think it would help to think about the overall structure of the print functions we have so far. Right now there are two inputs: model and sentence_letters. Here are some thoughts about the architecture:

1. From model by alone, we should be able to extract all_bits, poss_bits, and world_bits. Were we to go on to define necessity in terms of counterfactuals (i.e., \box A := \top \boxright A where \top is a logical constant that is verified by every state), it would also be helpful to extract the necessary states nec_bits which are a part of every world. Regardless, I think it makes sense to have a helper function to do all of this work at once.
2. Given sentence_letters and model we should be able extract the verifiers and falsifiers for each as well as the alt_worlds in which each is true. Doing just this may make for a natural helper function.
3. Then there are the various print functions themselves which take the outputs of the helper functions and print the relevant statements. It is at this point that conversion to state fusions takes place.

It shouldn't take too much to restructure what we have, but looking forward I suspect things to get more complicated. Just to have some sense of the direction, consider the following:

1. At some point we will want to replace sentence_letters, drawing on the functions that will help us process input_sentences. For each X in input_sentences, we will want to interpret and print each of its parts in a systematic and readable way. However, not every part is equally helpful. For instance, if we have \neg( A \wedge B) \boxright C, then both \neg(A \wedge B) and A \wedge B are subsentences, but only the former is interesting since to evaluate the counterfactual we will want to know whether C is true in all \neg(A \wedge B) alternatives to the evaluation world.
2. It may be helpful to define a recursive function which takes an element of input_sentences and prints relevant information about each of its most immediate parts, where this will be determined by the outermost connective. Defining such a function should be easy given the functions we will need for generating Z3 constraints. In particular, we will have defined true_at in the semantics, and so may use this to evaluate the the input sentence and its parts.
3. For instance, if the sentence looks like A \wedge B, A \vee B, etc., then we will want to evaluate A and B separately in the evaluation world, printing the outputs of each. If, however, the sentence is A \boxright B, then we will need to generate all A alternatives to the evaluation world, checking whether B is true in each, printing the output. Something similar may be done for \neg(A \boxright B). Note that B may contain a counterfactual, in which case the process would be repeated for B.

Much of this can wait until the semantics is sorted out, but good to start thinking about in considering the print functions and how they are organized.

[benbrastmckie]

Divide this file into model_generator.py which builds a data structure and print.py which includes any print functions.

[benbrastmckie]

I checked find_complex_propositions in model_structure.py and it looks good. I was trying to test it (as currently it is unused) but was having trouble doing so. The natural place would be in print_props in the same module (I made a few changes), replacing ver_states and fal_states, but couldn't get this to work.

Once this is working it shouldn't take much to get the print_props to work recursively as described in strategies.

[mbuit82]

Sounds good—I've been working today on getting the Proposition class integrated, and that function is going to play a role. I'll commit a whole bunch of changes that'll probably address that at the end of the day. I'll let you know when I push so you can see if the issue is fixed

[benbrastmckie]

That sounds great. I hope the merge is not too tricky as I moved some things around. If you have trouble merging, feel free to create a new branch (if you haven't already). I can then try to merge the branch that you push.

[mbuit82]

I just pushed it to a new branch because I saw the conflicts are going to be many lol. Let me know if you have any questions/problems when merging the two branches.

[benbrastmckie]

This looks great! I merged the commits and started debugging. I got it working printing props for sentence letters in the old way, but ran into trouble using the new lines you added for printing extensional propositions. troubleshooting this probably makes sense before moving to the recursive print procedure outlined in strategies, but I got stuck. I left inline TODOs behind to document what I was thinking.

[mbuit82]

No worries! I'll start working on debugging

[mbuit82]

Just finished debugging, it should be working as normal (I actually pushed with some bugs still in, so sorry about that!). Also, we only actually use two functions from print.py, everything else is either in model_definitions or has an identical copy in it (so I just imported the one from model_definitions). The two remaining functions, find_true_and_false_in_alt and print_alt_relation, I think could be moved to model_definitions (really model_definitions when I first made it was a copy of print, so it makes sense those two files have a lot of overlap—my goal with it was to ultimately completely get rid of print.py, supplanting it all by helper funds (those in model_definitions) or by methods in the data structures). I commented out all the unused functions in print.py, along with where their analogues currently live.

[mbuit82]

I didn't get a chance to look at the recursive print algorithm yet, but I'll think about it tonight—I need to do some other work before

[benbrastmckie]

Works great! This is a big step and really helps to see what is going on in each model.

No worries about the bugs, and yes, I think consolidating print and model_definitions makes sense.

I saw the update_comparison_world function and agree that we need some kind of way to manage the shifting world of evaluation. It might make the most sense to let w be called start_world or main_world and then let eval_world move around as needed. So for instance eval_world would begin identical to main_world and change only when evaluating a counterfactual, e.g., to print A \boxright B the print algorithm would consider all A-alt_worlds to eval_world (currently equal to main_world), checking if B is true in each u in A-alt_worlds to eval_world by reassigning eval_world to u and seeing if B is true there. This could be iterated so that if B is C \boxright D, then to see if C \boxright D is true in u it would find all C-alt_worlds to eval_world (now equal to u), reassigning eval_world to each of them and checking if D is true. This might make more sense in the context of defining the print algorithm, but thought it was relevant to mention here.

[mbuit82]

Glad to hear! It's nice seeing the project progress :)

Sounds good—I went ahead and changed the necessary things to consolidate print and model_definition and moved print to the OLD folder.

I have a similar hunch to you on the update_comparison_world and its role in the recursive print function. I'll see what I can think of later today

[benbrastmckie]

That's great! I added linter comments throughout, though these are low priority.

[mbuit82]

Nice! I had an idea for putting N in test_complete. It's looking like it's going to take a while to try it, so I may not get to thinking about the recursive algorithm before tomorrow (thought I should try to implement this before I forget my train of thought)

[benbrastmckie]

That's great! I'm honestly out of ideas myself for how to get N defined in the right place. By contrast, I suspect the print algorithm will be fairly easy. We might be able to code it up tomorrow if you don't have time to get to it.

[benbrastmckie]

I'm going to close this since we are on to a new print function and have an issue open for that.