LINEAR LOGIC, COMONADS AND OPTIMAL REDUCTIONS

Article type: Research Article

Authors: Asperti, Andrea

Affiliations: Dipartimento di Matematica, Universitá di Bologna, P.za di Porta S. Donato, 40126 Bologna, Italy, [email protected]

Note: [] Partially supported by the ESPRIT Basic Research Project 6454 - CONFER.

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.

DOI: 10.3233/FI-1995-22121

Journal: Fundamenta Informaticae, vol. 22, no. 1-2, pp. 3-22, 1995