La logique linéaire polarisée LLP, introduite par Olivier Laurent, est un système issu de la logique linéaire, reposant sur des contraintes de polarité : une formule est soit positive soit négative. Cela donne un système logique moins compliqué que LL, d'expressivité classique, et possédant de très bonnes propriétés, comme en témoigne l'étude des réseaux polarisés par exemple.
Guidés par la sémantique de MELLP (LLP sans additif) dans le modèle de jeux polarisés d'Olivier, nous avons cherché à étendre ce système avec un opérateur de point fixe. Cela nous a conduit à étudier des réseaux polarisés plus généraux, pouvant contenir des cycles (alors que le critère de correction des réseaux de LLP demande l'acyclicité).
Dans cet exposé, après une présentation de LLP, nous introduirons le système MELLPwC (MELLP avec cycles ...). Ce sur-système de MELLP admet la dynamique la plus naturelle qui soit, dans la mesure où nous reprenons exactement les règles d'élimination des coupures de MELLP. Mais MELLPwC est plus expressif et permet d'interpréter naturellement un opérateur de point fixe : le comportement de type récursif est obtenu lorsque sont éliminées des coupures intervenant dans des cycles. Le critère de correction de MELLPwC est extrêmement simple et donne une interprétation « logique » à un grand nombre de réseaux.
Nous montrerons aussi comment ce système étendu s'interprète dans des catégories cartésiennes closes tracées (cf. l'exposé de Nick Benton au séminaire PPS du 12/12/02).