Jason (jcreed) wrote,
Jason
jcreed

Had a pretty good morning for research actually: I had a bit of a Logical Relations Crisis since Derek pointed out a gap in my continuity-of-evaluation correctness proof when I chatted with him at POPL. Fortunately I think I fixed it now and figured out why I made the mistake in the first place --- the role of logical relations is to strengthen the induction hypothesis, and I just wasn't strengthening it enough. I just need to absorb this whole super-trendy Step-Indexed Logical Relations thing at a greater level of detail than I did before, because I certainly need it to handle recursive types and functions.

Also I had some more success thinking about how to adapt examples from Swarat and pals's "Continuity Analysis of Functions" paper. The tough thing is that I don't know how to do Dijkstra's algorithm itself, because I can't yet figure out any way of, er, controlling control-flow in a benign (i.e. Lipschitz-continuous) way the way the paper does as basically one of its centerpiece ideas.

But I can write a function that inefficiently computes extensionally the same function as Dijkstra (and inefficient computations of minimum spanning tree, and knapsack...) and at least then the linearity really comes into play in a nontrivial way. The reason that the length of the minimum path is 1-continuous in your edge weights is that a path isn't allowed (or, er, I guess, more to the point, doesn't have to) reuse edges.

And I can write a function with linear types that very naturally exhibits why it doesn't reuse edges, even though it does sling them around nontrivially. It's kind of cool!
Tags: work
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 

  • 5 comments