### (no subject)

Saw a couple talks today. One was Guy Steele, saying some unsurprising but perfectly understandable things about parallelism. One thing that didn't quite occur to me before Steele made a certain comment is how the thinking behind Savitch's theorem from complexity theory (which says NPSPACE = PSPACE among other consequences --- that you already have all the power of nondeterminism if you're only limited by space!) is kind of implicitly saying how you can parallelize anything as long as you can efficiently represent and compose state transitions. We all know that we can efficiently take big sums or whatever in parallel, because addition is associative, but function composition is too! This latter point is more or less how Steele phrased it --- the connection to Savitch is my own random thought.

The other talk was Christoph Benzmüller selling us on his higher-order theorem prover Leo II, which sounds pretty awesome. It pulls a bunch of tricks to reduce theorem proving problems in HOL to bits and pieces it feeds to first-order provers, and then digests the results, and then feeds back into the first-order provers, and so on. I have a meeting with him and Frank tomorrow morning to see if I can get it to do linear logic proving by pulling the same encoding tricks I did with HLF. It sounds like he already got some cool results with Deepak's authorization logic already.

I've found myself thinking recently about something

Poking at the literature a bit, it seems the right word to look for is "biadjoint" (or occasionally "pseudoadjoint"?) but it seems that if you are smart enough to confidently talk about what biadjoints are in a published paper, you are smart enough to make everything else in your paper impenetrably advanced, so I haven't made a lot of progress understanding them.

---

ETA: But I did make this model in Sketchup, which I think is the analogue of the adjoint triangle equalities one dimension up:

The other talk was Christoph Benzmüller selling us on his higher-order theorem prover Leo II, which sounds pretty awesome. It pulls a bunch of tricks to reduce theorem proving problems in HOL to bits and pieces it feeds to first-order provers, and then digests the results, and then feeds back into the first-order provers, and so on. I have a meeting with him and Frank tomorrow morning to see if I can get it to do linear logic proving by pulling the same encoding tricks I did with HLF. It sounds like he already got some cool results with Deepak's authorization logic already.

I've found myself thinking recently about something

**neelk**mentioned, which is that we lambda-calculus people really ought to "already" understand something of the 2-categorical structure of adjunctions (for example between - x A and A ⇒ -) because we know that you should privilege β-**reduction**and η-**expansion**, this being a finer-grained notion than just adjunction, which says by dint of uniqueness of adjoint transposes that you just get**equality**of terms that are connected βη-convertibility in any direction and indeed any zigzagging path you like.Poking at the literature a bit, it seems the right word to look for is "biadjoint" (or occasionally "pseudoadjoint"?) but it seems that if you are smart enough to confidently talk about what biadjoints are in a published paper, you are smart enough to make everything else in your paper impenetrably advanced, so I haven't made a lot of progress understanding them.

---

ETA: But I did make this model in Sketchup, which I think is the analogue of the adjoint triangle equalities one dimension up: