Algorithmic specifications in linear logic with subexponentials

Nigam Vivek Dale Miller 1, 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : The linear logic exponentials !, ? are not canonical: one can add to linear logic other such operators, say !^l, ?^l, which may or may not allow contraction and weakening, and where l is from some pre-ordered set of labels. We shall call these additional operators subexponentials and use them to assign locations to multisets of formulas within a linear logic programming setting. Treating locations as subexponentials greatly increases the algorithmic expressiveness of logic. To illustrate this new expressiveness, we show that focused proof search can be precisely linked to a simple algorithmic specification language that contains while-loops, conditionals, and insertion into and deletion from multisets. We also give some general conditions for when a focused proof step can be executed in constant time. In addition, we propose a new logical connective that allows for the creation of new subexponentials, thereby further augmenting the algorithmic expressiveness of logic.
Type de document :
Communication dans un congrès
PPDP09 - ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Sep 2009, Coimbra, Portugal. 2009
Liste complète des métadonnées

https://hal.inria.fr/hal-00772332
Contributeur : Dale Miller <>
Soumis le : jeudi 10 janvier 2013 - 13:21:41
Dernière modification le : jeudi 10 mai 2018 - 02:06:31

Identifiants

  • HAL Id : hal-00772332, version 1

Collections

Citation

Nigam Vivek, Dale Miller. Algorithmic specifications in linear logic with subexponentials. PPDP09 - ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Sep 2009, Coimbra, Portugal. 2009. 〈hal-00772332〉

Partager

Métriques

Consultations de la notice

289