Jason (jcreed) wrote,

Aha! Everything seems to work out very nicely if I try to do that monoid-labelled logic in the style of my previous CPS-ish encodings of substructural logics into first-order logic, where I get all the statefulness I need just by exploiting the linearity of the intuitionistic conclusion.
Monoid Logic -> FOL

I'm still having some mysterious trouble encoding BI's multiplicative unit. I'm conjecturing that the difference between BI as such and the logic of the category of graphs has something to do with either that, or imposing commutativity on this operation "+" on the first-order domain. To encode BI, I want it to be noncommutative, because the first-order expressions correspond to paths through the context. But with the intuitions coming from graphs, the first-order expressions are merely 0-1 counts of how many times you've passed from the presheaf bucket that holds all the edges of the graph, to the bucket containing vertices --- and these counts are intrinsically commutative. Mmmmmaybe this has to do with how graph-logic seems to be endowed with all these extra equations on contexts. Then again, they all have to do with the multiplicative unit, also, so it's hard for me to discern what to blame yet.


Actually having a lot of trouble figuring out whether this really can model BI even without the multiplicative unit. Might need some noncommutative generalizations of boolean algebras...
Tags: bunched, logic, math

  • (no subject)

    Logic programming lately is a tiny bit unexciting because we are going over linear logic in detail. Surely we will be getting back to more strictly…

  • (no subject)

    Definitely had a more decent day today. Class was kind of interesting, and I got the homework for it done in the afternoon. Thanks to…

  • (no subject)

    Whoops, still not quite done with HOT. Two bugs left... --- I have found and fixed two bugs. Any of you familiar with the arithmetic of bugs knows…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded