Jason (jcreed) wrote,
Jason
jcreed

I ran into Bob on thursday and he mentioned this paper. It's about an implementation technique called "normalization by evaluation", specifically extending a category-theoretical account of why it really works to coproducts. From this old types list post, it seems that this issue (of decidability of lambda calculus with genuine coproducts, where you have not only commuting conversions, but also the η-like equality e = case e of inl(x) => inl(x) | inr(x) => inr (x)) has been a concern of Bob's for several years at least.

This paper is mightily bad-ass. Already the logically prior work that gives a semantics for a lambda calculus in categories of presheaves was stretching the limits of my category theory knowledge. How that stuff works is by an elegant generalization of ordinary Kripke semantics for intuitionistic logic: instead of a poset of worlds W, and instead of it being an all-or-nothing fact that w ⊩ A ("world w forces proposition A") which satisfies monotonicity, we have a category C of worlds, and a collection of reasons (which one might think of as proofs) why each proposition is true at each world, with monotonicity being replaced by the "arrow part" of the functor from C to Setsop --- it tells us how proofs evolve over time.

But to get normal forms for coproducts, it seems to be necessary to consider contexts plus constraints. This somehow translates in category-land to sheaves instead of mere presheaves. These sheaves are over a Grothendieck topology where the locality condition --- the requirment that every matching family has a unique amalgamation --- amounts, by a clever choice of topology, to the fact that every pair of terms that look like two branches of a case statement have a unique amalgamation into a normal form which is βη equal to actually casing over those two branches.

All I can say is, omg, sheaves.
Tags: categories, 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 

  • 2 comments