Jason (jcreed) wrote,
Jason
jcreed

I think I totally nailed down the destination-passing result. I had to break symmetry once more --- not only do I have to do a different translation on the left and the right of the turnstile, I also have to have different induction hypotheses for the "forward" and "backward" entailments in the asynchronous part. A bit of a bummer, but at least the proof goes through. Certainly a relief after about 10 hours of continuous pounding away trying to prove a falsehood.

Thanks to simrob for planting the idea in my head of how incredibly related ordered logic on the one hand and destination-passing in linear logic on the other are. He showed me how moving away from destination passing in structural operational semantics makes your life easier, but I've found for my application that avoiding the ordered context and passing destinations seems better.
Tags: math
Subscribe
  • 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 

  • 1 comment