Marco Solieri (Université Paris 13), Deep into optimality Complexity and correctness of shared implementation of bounded logics.
Schedule
- Jan. 31, 2012, 16:30 - 17:00
Abstract
(joint work with Stefano Guerrini and Thomas Leventis)
Sharing graphs are an implementation of both the Lévy-optimal reduction on
lambda calculus, and of linear logic proof-nets. Since the proof of inadequacy
of Lévy families as a cost model for lambda calculus, studies on the complexity
of the shared reduction are far from complete. Indeed, the only comparative result
considers the restricted case of bounded logics. Because of their well known
complexity, it was possible to provide semantically, via geometry of interaction, a
correspondent bounding of their shared implementation.
In a similarly restricted case, where the abstract algorithm is sufficient, we
present a complete and stronger comparison between the cost of the cut elimination
on proof-nets and the cost of the corresponding shared reduction. Then, for the fi rst
time, the expected bene fits of sharing and avoiding duplication in the reduction
are made explicit. The proof exploits an intermediate graph rewriting system, that
permits us to give a precise account of complexity on the former and to establish
a simulation of the latter. Such simulation implies the main complexity result of
the shared implementation, as well as its correctness.
Attachments
(joint work with Stefano Guerrini and Thomas Leventis) Sharing graphs are an implementation of both the Lévy-optimal reduction on lambda calculus, and of linear logic proof-nets. Since the proof of inadequacy of Lévy families as a cost model for lambda calculus, studies on the complexity of the shared reduction are far from complete. Indeed, the only comparative result considers the restricted case of bounded logics. Because of their well known complexity, it was possible to provide semantically, via geometry of interaction, a correspondent bounding of their shared implementation. In a similarly restricted case, where the abstract algorithm is sufficient, we present a complete and stronger comparison between the cost of the cut elimination on proof-nets and the cost of the corresponding shared reduction. Then, for the fi rst time, the expected bene fits of sharing and avoiding duplication in the reduction are made explicit. The proof exploits an intermediate graph rewriting system, that permits us to give a precise account of complexity on the former and to establish a simulation of the latter. Such simulation implies the main complexity result of the shared implementation, as well as its correctness.