benbrastmckie / ModelChecker

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

separate prefix algorithm from semantics #38

Open benbrastmckie opened 4 days ago

benbrastmckie commented 4 days ago

I thought it might be helpful to open an issue for this. The aim is to refactor the prefix function so as not to depend on which operators the language includes, remaining agnostic about the semantics and even arity for those operators. Here is a sketch what I was thinking:

There may well be ways to improve on this but thought this might help to provide a way in.

benbrastmckie commented 3 days ago

I almost got pure_prefix to work. It runs but has errors for complicated cases. I can't quite see what the issue is. If you have a chance to take a look I'd be curious to know if you can spot the error. Seems like it is very close.

benbrastmckie commented 3 days ago

Never mind I got it!

benbrastmckie commented 3 days ago

I made all of the syntax functions methods of the ModelSetup class. If it makes more sense, we could move some of these to a syntax module, though right now no module is imported by hidden_things.py. I suspect elements are still missing from the syntax functions from before, in particular, I did not include the return [Const(token, AtomSort)] though commented out where I think it should go.