benbrastmckie / ModelChecker

A hyperintensional theorem prover for modal, counterfactual conditional, constitutive explanatory, and extensional operators.
https://pypi.org/project/model-checker/
2 stars 0 forks source link

Infix/prefix translation functions #1

Closed benbrastmckie closed 4 months ago

benbrastmckie commented 4 months ago

This issue will follow the development of the infix and prefix functions described in /Design/Strategies.md, providing a place for questions and problems to be raised. All TODOs can be tracked in the TODO.md file. Here are two initial thoughts.

Feel free to post any related issues or questions that arise here.

mbuit82 commented 4 months ago

Sounds good! I'm wondering—as for the Or(x,y) function that's on the strategy doc, why don't we just call it Fusion(x,y)? seems it would be much more transparent, unless there really is a difference between Or and Fusion that is best be reflected later.

benbrastmckie commented 4 months ago

I'm going to create a new issue to preserve this tread for the infix/prefix functions, though of course all of these issues are going to be related.

mbuit82 commented 4 months ago

Sounds good—just made a function for translating infix to prefix. There's two issues left to resolve: 1. how bad is it if the incoming representations have forward slashes instead of backslashes? 2. what do we want to do with prefix notation? I put both those questions in the questions.md file also

benbrastmckie commented 4 months ago

If the double slash strategy works, that is probably the simplest, but the zero-slash strategy could also work (or forward slash). Whatever works is great.

We chatted about what the prefix function is for, but I will include some notes in the Strategies.md file since I hope to slowly turn this into documentation.

Also, I'm not sure that I mentioned this, but it matters a lot less what name gets used for the operators in prefix notation since these are only help the semantics decide which recursive clause to use. So Maybe best to have no slashes there. Although tempting to go all the way to And instead of Wedge, this might get confusing since And will also show up to connect Z3 conditions.

As for TODOs, it seem that all that remains is:

Seems like we're close to closing our first issue!

mbuit82 commented 4 months ago

I've rewritten it (about to push) so that it should in principle be able to accept all of \wedge, /wedge, or wedge. I think this provides more flexibility on the user end and it may actually be easier and more efficient to resolve the translation from those things to something like Wedge after the construction of the infix form. I cleaned up the prefix_infix file, and now A goes to [A]. This has the consequence that (A \wedge B) goes to [wedge, [A], [B]] (ie, args of operators are in 1-elem lists) but this would make a function calling recursively to get the semantics of an infix function easier to write (given we want A to map to [A]), so I think it's actually good. I think that's basically everything on this! (also, how do you make text in the middle of the comment look like code?)

benbrastmckie commented 4 months ago

Awesome looks great! Regarding you question there are two ways. Either you indent four spaces, or wrap with triple quotes.

benbrastmckie commented 4 months ago

Hey was just looking at the prefix function and it looks great. I'm going to close this issue, though we can continue to post here if anything relevant comes up.