State Representation

[benbrastmckie]

I will copy and likely extend these notes into Strategies but here is the rough idea. Whereas the prefix function is at the beginning of the pipeline, the state representation function is towards the end (just for context).

Say Z3 spits out some kind of model consisting of a bunch of bitvectors etc. Say c = b#10001. Having it written out this way is better than a hex code, but it is still not that salient what is going on. But here we can see that c is the fusion of two atomic states, call them a = b#00001 and b = b#10000. So a better representation would look like c = a.b. Honestly it doesn't matter that, thought of as numbers, a < b. All we care about is that they are both atomic and that c is their fusion.

Given that there is a nice way to identify which states are atomic, it actually doesn't matter whether states are represented in hexadecimal or not since either way it would be nice to represent them in some cleaner way. Maybe you have thoughts about how to do this, but here is a rough idea:

• given some number of states as inputs (these are outputs of the Z3 model), find all atomic states.
• name all input and atomic states in some nice way (more thoughts in Strategies).
• then identify each input state with a fusion of atomic states using their new names.

There will probably be some other natural pieces to add, but getting these identities is a good start. The thought is that eventually, the model representation could include things like |A| = < { a, b, a.b}, {f.g} > for each sentence letter which would make it clear what proposition each sentence letter is being assigned to. Knowing what the fusion relations are and getting nice conventions for naming states will be a key step.

[benbrastmckie]

The bitvec_to_substate function works great! Call the outputs of this function fusions for the purposes of this comment. I began building up definitions which take fusions as arguments, e.g., fusion, parthood, possibility (in a model), compatibility, etc. However, it seemed strange to be working what I take are strings and define notions like fusion when these are already defined for bitvectors.

This got me to thinking that, given a z3 model, the states should be extracted as bitvectors and stored accordingly given their properties (e.g., world, possible, impossible). This allows for the identification of A-verifiers, A-falsifiers, and A-alternatives to the evaluation world for any given sentence letter A. Then when it comes time to print, the various sets of states can be converted to fusions via the bitvec_to_substate function.

I used this strategy in the branch remove_alt which removed the declaration of alternative but more about that elsewhere.

[benbrastmckie]

The state representations are looking great! I'm going to close this issue.