logique linéaire, affine, autre

Une question à Deufeufeu: tu as l'air spécialiste des logiques linéaires, affines, etc (vu ta thèse que tu as postée ds un autre fil)

Il y a une question qui m'intéresse bcp: il est connu que la logique linéaire n'est pas récursive (ie que l'ensemble de ses théorèmes propositionnels n'est pas récursif). Au début ça m'a emballé mais la preuve (avec les machines de Minsky) montre que c'est en fait "un détail" et que c'est lié "banalement" à la différence (là sous cet angle important) entre la logique affine et la logique linéaire.

Il me semble donc que la logique affine est récursive. Qu'est-ce qu'il pourrait y avoir comme logiques respectable dont l'ensemble des théorèmes ne serait pas récursif et tel que ce dernier point ne serait pas trop sensible (je considère comme "sensible" le fait que ça change de passer de la linéaire à l'affine)?

D'une manière générale, une bonne logique (propositionnelle!) avec des modalités unaires uniquement et non récursive me plairait bien
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi

Réponses

  • Alors je suis très mauvais là-dedans, maintenant après avoir discuté avec Yves Lafont et fait un peu de recherche, il est confirmé que 1) l'utilisation du test à zéro d'un compteur est crucial et pose un problème avec l'affaiblissement 2) la logique linéaire affine est décidable, c'est un résultat de Kopylov (LICS95).
    Je ne peux pas répondre à ta question.
    Je peux juste signaler un problème ouvert pour les jeunes qui nous lisent : on ne sait toujours pas si MELL est décidable. Tout ce que l'on sait c'est que beaucoup de problèmes s'y réduisent.
  • Peux-tu définir MELL? (Ses règles, axiomes?) Si c'est une logique propositionnelle, ça m'intéresse
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • C'est le fragment contenant juste $\otimes$, par (le & a l'envers*), $!$ et $?$. C'est à dire celui qui contient le lambda-calcul simplement typé (et le lambda-calcul pur avec les types purs).

    * notes aux modérateurs : si vous pouviez rajouter le paquet cmll dans le préambule, ce serait gentil
  • En d'autres termes c'est le fragment Multiplicatif et Exponentiel de la Logique Linéaire (je pense Christophe que tu as déjà vu la terminologie multiplicatif/additif/exponentiel pour les différents connecteurs).
  • Merci

    Oui j'ai compris ce que MELL est: hélas, le même fragment de la logique affine étant récursif (puisque la LA l'est tout entière) ça me "passionne" moins, car à vue de nez, je ne vois même pas pourquoi elle serait récursive, pas plus pourquoi elle ne le serait pas (toujours ce problème d'équilibre entre la droite et la gauche dans les séquents...) qui rend ces problèmes proches de celui consistant à résoudre des équations diophantiennes.

    Je vois un peu la logique affine comme, en difficulté, assez proche de celui consistant, étant donné une inéquation diophantienne, à se demander si elle a au moins une solution (ce qui est bcp plus facile)

    Cependant, c'est un beau problème (sans les additifs, ça reste assez naturel comme logique)

    Je présume que la "MELL" intuitionniste (sa récursivité) est tout aussi ouvert (si ce n'est équivalent)?
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Qu'as tu contre les additifs ? :)
  • Bin, la manière dont je les vois fait que quand je fais un terme qui provient d'une preuve, les instructions qui correspondent laissent la main à "un personnage extérieur sceptique" qui a le droit de choisir ce qu'il veut: alors au moment de réfléchir à ce qu'ils font, c'est moins facile
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Dans la correspondance de Hurry-Coward, les additifs correspondent au type somme et se comprennent plutôt bien. A quoi tu fait référence ? Au fait que dans une projection d'un couple, le couple lui-même ne sache pas sur quel côté il va se faire projeter ?

    Tu sais, de ce que j'ai pu en voir (je fait référence à ton sceptique), tu semble fana du concept de paraproofs (qu'on appelle encore test) et tu devrais regarder la ludique qui est une reconstruction de la logique entièrement basée sur la dualité qui découle de l'application d'une preuve contre un test, et les formules apparaissent comme des opérations sur des ensembles de preuves clos par bidualité. C'est vraiment une très jolie théorie, le seul problème c'est qu'on reconstruit MALL, il n'est pas possible de rajouter facilement des exponentielles.
  • lol et bin je vais un oeil au "point aveugle" ya un chapitre dessus...

    Oui, effectivement, les exponentielles et les lambda termes ça semble un mariage dans la douleur, non? Quel terme (ou instruction) réalise !A --->A par exemple?

    Sans parler de (!A--->B)--->(A--->?B)? (d'ailleurs je ne suis même pas sûr à 100% que ce soit un th)
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • $\vdash \lambda x. x : !A \multimap A$ non ?
    Je te rappelle que $!A \multimap A$ c'est juste l'identité dans la co-Kleisli construite sur un modèle de la logique linéaire.

    Tu dois vouloir dire $(! A \multimap B) \multimap (B^\bot \multimap ? A^\bot)$ qui est prouvable, mais la vraie contraposée c'est $(!A \multimap B) \multimap (! B^\bot \multimap A^\bot)$ qui n'est pas prouvable.

    [edit: Kleisly faisait un petit peu trop greg, merci au barbu]
  • Par contre, la Vraie contraposée traduite c'est $!(!A \multimap B) \multimap (! B^\bot \multimap A^\bot)$ qui est prouvable. On a rajouté un ! devant et ça fait tout le travail.
  • AD te rendra grâce d'avoir donné sa majuscule à Kleisli.
    Par contre, je ne suis pas sûr que le grec s'impose au i final... :)

    [Edit : message qui n'a plus de raison d'être. Que le modérateur en manque d'éradication ne se prive pas. :D]
  • Je me doutais que tu allais me répondre l'identité, mais ça me gène un peu (mais tu n'y es pour rien: c'est juste cette mode consistant à exécuter par l'identité les passages au cas particulier...)

    oups sans parenthèse, comme je ne connais pas les priorités tacites: cependant, non, je ne parlais pas de la contraposée, qui s'exécute comme toutes les contraposées***, mais bel et bien de la formule que j'ai écrite (mais j'ignore même comment elle est considérée en logiques plus restreintes que les "connues de tous", peut-être même pas comme un théorème...)


    *** si tu parles bien de l'implication de (nonB) ---> non(!A) par (!A)---->B

    De ce que je comprends de la suite, tu me dis que:

    from (!A)--->B (***); on peut déduire (nonB)---->non(!A) (jusque là, lol) puis (nonB)
    >(?(nonA))

    puis je suppose que tu te sers tacitement d'un axiome (!(X---->?Y))
    >((!X)
    >Y) pour passer de (!(***)) à (!(nonB))
    >(nonA) puis à A
    >(non!nonB) lui-même "égal à" A
    >(?B) qui me satisferait et donc au fond tu me dis que:


    ce n'est pas:
    (!A--->B)--->(A--->?B)
    qui est un théorème mais:

    [!(!A--->B)]--->(A--->?B)

    Ne me suis-je pas trop gourré?
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • non ça ne peut pas être prouvable ce que tu dis, si on traduit cela veut dire étant donné une fonction qui a un $A$ dupliquable plein de fois associe un $B$, et un $A$, je peux peut-être produire un $B$. On voit ce que tu voudrais dire, c'est que des fois une fonction analytique est linéaire. Le problème c'est que pour faire ce raisonnement il faudrait que tu saches comment tu prouves $!A \multimap B$.
    Rajouter le fait que tu puisses dupliquer ta fonction ne va non plus t'aider.
    Maintenant j'ai un autre argument plus géométrique et terre à terre. Ton $!A \multimap B$ une fois qu'il passe à gauche d'un $\multimap$ il se transforme en $! A \otimes B$, or ton tenseur étant multiplicatif, tu vois bien que tu ne va pas pouvoir influer entre la partie qui porte sur $A$ et celle qui porte sur $B$.
  • Bin, je pensais juste avoir traduit ta pensée
    puis je suppose que tu te sers tacitement d'un axiome (!(X---->?Y))
    >((!X)
    >Y) pour passer de

    et de ton annonce du post juste avant barbu??

    donc ce sont mes autres inférences qui sont invalides?
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Dans ton post juste avant barbu, la conclusion est:

    (!(nonB))
    >(nonA)


    or il me semble que ça implique (autorisé?):

    A
    >non(!(nonB)) et que (non!nonX) est une abréviation de ?X

    donc que ça implique:

    A
    >?B
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Détail: mais je suppose que $(nonB\to nonA)\to (A\to B)$ est un théorème aussi en logique linéaire?

    je vais essayer de l'écrire avec tes symboles lol:

    $(B^\bot \multimap A^\bot)\multimap (A\multimap B)$
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • ROOOOOOOO c'est zoli!!!!!

    lol "multimap" ça me fait penser au cinquième élément "multipass"
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.