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:
• #### (no subject)

After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

• #### (no subject)

Thai curry leftovers for dinner. Got a copy of Hennessy and Patterson's textbook on Architecture, and I am enjoying catching up on all the low-level…

• #### (no subject)

Finally the end is in sight for unpacking my books. Heartstrings are pulled over the desire to slim down and get rid of some of them, but so many are…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic