Jason (jcreed) wrote,
Jason
jcreed

Did a bit more of paper writing today, thought some more about focusing.

Once again I think I'm in a state where I think I've actually got my personal "holy grail" proof at hand, one that feels modular in the right ineffable way and isn't too messy. This one's right at the threshold of "not too messy" however.

The repeated theme of the last few attempts is something like this:

What is the most pedestrian answer we can give to the question "what is focusing about?", at least in the traditional setting where we don't have big powerful data structures like Noam and Dan use? Well, it cuts down the number of proofs by saying that we can't perform certain steps at certain times. Like, we can't do anything but what we're focused on when we're focused on something, and we can't focus on something before all the asynchronous work is done, and we can't do the asynchronous work in any order but the one prescribed - say, conclusion first, and then hypotheses right to left.

One central idea is that all these prohibitions on decomposing connectives at the wrong time can be built out of (rather ordinary) logical connectives. Consider circle from lax logic; you only get to decompose it on the left when the judgment on the right is also lax.

The connectives I happen to use are all variations on a theme I'm tempted to call "bosonic logic":
      G; n |- A	       	  G, A; n+1 |- C
     ------------         --------------
     G; n+1 |- FA      	  G, FA; n |- C 
			    	    
     G; n+1 |- A           G, A; n |- C	       	  
     -----------         --------------- 	  
      G; n |- UA         G, UA; n+1 |- C	  

where there's an extra zone in the judgment that contains a natural number, and the modalities U and F act kinda like the creation and annihilation operators from QFT depending on which side they're on: critically we have of course the noncommutativity UF != FU, for to give up a token and then to consume it is not the same thing as to require consumption of it and then spit it back out.

Up until recently I thought I had to account for the enforced order in left inversion using either ordered logic (where the requisite token-passing protocol works but gets kind of ugly, and is not too obvious how to extend to other logics) or else curry all non-unary positive connectives away (which requires some creativity in inventing the right connectives for the fully-curried language, and again, isn't as obvious as I'd like to extend to other logics, but I managed to figure out how multimodal logic should probably go).

I thought of a third option this morning, which is definitely now my favorite: it is to get across the enforced order of left inversion by something extremely similar to how destination-passing style works in substructural operational semantics. You have an indexed family of tokens that get passed around, and quantifiers baked into the encoding make fresh token-indices so that you must decompose left inversions in the right order, because that's the only relaying of tokens from one guy to the next that works. Like, suppose A and B and C are floating in the soup that is the linear context, and A requires a and yields b, and B requires b and yields c, and C requires c and yields d. The only way to get d from a is to work on them in the right order!
Tags: math
Subscribe

  • (no subject)

    K's off at an atypically Saturdayish Type-Thursday event, so I stuck around the apartment hiding from 100-degree heat, and noodled around with…

  • (no subject)

    Playing around with the agda javascript backend, now. Like, my ears are popping from the sudden change of type-theory-pressure.

  • (no subject)

    https://deadlockempire.github.io is a very cute edutainment game, meant to teach people about deadlocks and race conditions and concurrency…

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 4 comments