Closed mbuit82 closed 1 week ago
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
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.
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
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
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.
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.
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.
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.
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.
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.
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.
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.
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
Nice, calculating as we go sounds ideal. Maybe the update_world
function could be made to do that instead, amounting to a minor change.
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).
Awesome! I'll check it out and let you merge the branch when you are happy with it.
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
.
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.
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
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.
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!
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.
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.
You mentioned that there were some functions that might make sense to move to syntax
. Do you have any in mind?
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!
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
.
That sounds great! We're getting close!
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?
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.
I think this is resolved, or at least old and likely to get refactored significantly.
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))']
andconclusions = ['(A \\boxright B)','(A \\boxright C)']
: