Hybrid Linear Logic, revisited

Abstract : HyLL (Hybrid Linear Logic) is an extension of intuitionistic linear logic (ILL) that has been used as a framework for specifying systems that exhibit certain modalities. In HyLL, truth judgments are labelled by worlds (having a monoidal structure) and hybrid connectives (at and ↓) relate worlds with formulas. We start this work by showing that HyLL's axioms and rules can be adequately encoded in linear logic (LL), so that one focused step in LL will correspond to a step of derivation in HyLL. This shows that any proof in HyLL can be exactly mimicked by a LL focused derivation. Another extension of LL that has extensively been used for specifying systems with modalities is Subexponential Linear Logic (SELL). In SELL, the linear logic exponentials (!, ?) are decorated with labels representing locations, and a pre-order on such labels defines the provability relation. We propose an encoding of HyLL into SELL (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. More precisely, we identify worlds as locations, and show that a flat subexponential structure is sufficient for representing any world structure in HyLL. This shows that HyLL's monoidal structure is not reflected in LL derivations, hence not increasing the expressiveness of LL, from a proof theoretical point of view. We conclude by proposing the notion of fixed points in multiplicative additive HyLL (µHyMALL), which can be encoded into multiplicative additive linear logic with fixed points (µMALL). As an application, we propose encodings of Computational Tree Logic (CTL) into both µMALL and µHyMALL. In the former, states are represented as atoms in the linear context, hence reflecting a more operational view of CTL connectives. In the latter, worlds represent states of the transition system, thus exhibiting a pleasant similarity with the semantics of CTL.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), In press
Liste complète des métadonnées

https://hal.inria.fr/hal-01968154
Contributeur : Kaustuv Chaudhuri <>
Soumis le : mercredi 2 janvier 2019 - 10:50:49
Dernière modification le : mardi 8 janvier 2019 - 13:51:30

Fichier

MSCS_HAL.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01968154, version 1

Citation

Kaustuv Chaudhuri, Carlos Olarte, Elaine Pimentel, Joëlle Despeyroux. Hybrid Linear Logic, revisited. Mathematical Structures in Computer Science, Cambridge University Press (CUP), In press. 〈hal-01968154〉

Partager

Métriques

Consultations de la notice

42

Téléchargements de fichiers

24