Abstract
The paper discusses, in a categorical perspective, some recent works on optimal graph reduction techniques for the λ-calculus. In particular, we relate the two “brackets” in [GAL92a] to the two operations associated with the comonad “!” of Linear Logic. The rewriting rules can be then understood as a “local implementation” of naturality laws, that is as the broadcasting of some information from the output to the inputs of a term, following its connected structure.
Get full access to this article
View all access options for this article.