Hybrid Linear Logic, revisited - Laboratoire d'informatique de l'X (LIX) Accéder directement au contenu
Article Dans Une Revue Mathematical Structures in Computer Science Année : 2019

Hybrid Linear Logic, revisited

Résumé

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.
Fichier principal
Vignette du fichier
MSCS_HAL.pdf (422.05 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01968154 , version 1 (02-01-2019)

Licence

Paternité

Identifiants

Citer

Kaustuv Chaudhuri, Carlos Olarte, Elaine Pimentel, Joëlle Despeyroux. Hybrid Linear Logic, revisited. Mathematical Structures in Computer Science, inPress, ⟨10.1017/S0960129518000439⟩. ⟨hal-01968154⟩
167 Consultations
253 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More