Un sujet à créer

Pour continuer avec les billets en rapport avec le boulot, voilà une description d'un domaine que j'aimerai voir exister. L'étude des formules logiques minimales.

En informatique, on s'intéresse beaucoup au temps et à l'espace mémoire pris par un programme. Et une manière de réduire le temps de calcul, c'est de réduire l'espace mémoire des constructions intermédiaire. Donc, quand on manipule des objets, on aime bien qu'ils soient minimaux. L'exemple le plus évident de mon domaine, c'est les automates. La minimisation d'un automate déterministe a des propriété mathématiques très intéressantes ce qui permet de calculer l'automate minimal très rapidement.

La Théorie de l'information traite -entre autre- des différentes manières de réduire la taille d'un message, en faisant des suppositions sur les propriétés des messages qu'on aura envie d'utiliser. Par exemple, on peut supposer qu'il y aura en moyenne plus de "e" que de "x". Pour donner un exemple, en français, dire "une figure géométrique close composé d'une suite de segments, tous de tailles égaux, avec 3 angles", ça pourrait être résumé en "un triangle équilatérale", c'est plus rapide. Mais là ce n'est pas ce dont je veux parler, je vais supposer que les objets ont une taille fixe, ou pour le dire autrement dit qu'ils ont tous la même probabilité d'arriver[1].

De manière générale, pour "minimiser" un objet parmi une famille d'objet, il suffit de savoir décider trois choses: la taille de l'objet. Faire la liste de tous les objets d'une taille donné. Et savoir si deux objets sont équivalents. Alors on peut vérifier tous les objets de taille 0 et regarder si l'un deux est équivalent à l'objet à minimiser, puis tout ceux de taille 1, de taille 2, etc... Si on en trouve aucun, l'objet est minimal, sinon on a trouvé comment le minimiser.

Typiquement, pour les automates, on peut calculer leur taille, c'est le nombre d'état, on peut vérifier si deux automates sont équivalents, et on peut énumérer tous les automates de taille N[2]. Mais on n'utilise pas la méthode générale décrite plus haut, car ça prendrait trop de temps, et qu'on peut faire plus intelligent.


Eh bien, j'aimerai étudier la taille des formules logiques minimales pour une sémantique donné. Et je ne trouve pratiquement aucun article sur ce sujet, et les rares s'appliquent à des cas ultra précis sous des conditions très restrictives. Pourtant, dans certains domaines, dont le mien, on génère des formules logiques. La formule pouvant être elle même réutilisé dans une étape supplémentaire. Mais je n'ai vu aucun cas où l'on propose de faire une pause entre les étapes pour réduire la taille de la formule.

Selon les indications que j'ai donné tout à l'heure, on pourrait trouver la formule minimale pour les ensembles de tuples d'entiers définis dans l'arithmétique de Presburger. Mais ça serait très long à faire. Et j'ai beau réfléchir à la question, je ne vois aucune manière de le faire efficacement, d'ailleurs, je ne trouve pas de notion "naturelle" de dire qu'une formule est la même qu'une autre, mais réduite. Et pourtant, ça m'aiderait vraiment, ne serait-ce que pour vérifier ce que je fais. Ainsi, un de mes programmes génère la formule suivante: (je ne sais pas si elle rendra bien sur le blog)

∃sa ta sb tb sc tc sd td se te sf tf .sa = 1 ∧ ta = x ∧ {s = 1 ∧ t = (0, 1)mod 2 ⇒ sb = 1 ∧ tb = 0mod 2 ∧ ta − 2 < tb ≤ ta } ∧ {sa = 1 ∧ ta = (1, 0)mod 2 ⇒ sd = 1 ∧ td = 0mod 2 ∧ ta − 2 < td ≤ ta } ∧ {sb = 1 ∧ tb = (0, 2)mod 2 ⇒ sc = 1 ∧ tc = 04 ∧ tb − 4 < tc ≤ tb } ∧ {sb = 1 ∧ tb = (2, 0)mod 2 ⇒ se = 1 ∧ te = 04 ∧ tb − 4 < te ≤ tb } ∧ {sb = 1 ∧ tb = (2, 0)mod 2 ⇒ sf = 1 ∧ tf = 04 ∧ tb − 4 < tf ≤ tb } ∧ {sb = 1 ∧ tb = (0, 2)mod 2 ⇒ se = 1 ∧ te = 04 ∧ tb − 4 < te ≤ tb } ∧ {sc = 1 ⇒ tc 0 + 4 = t1 } ∧ {s = 1 ⇒ t1 + 4 = t0 } ∧ {s = 1 ⇒ t1 = t0 }

Alors qu'elle est équivalente à la version beaucoup plus simple: |x1-x2|=1.

Notes

[1] mathématiquement c'est incorrect, vu que mon ensemble est infini.

[2] Si l'alphabet a A lettres, alors il y a A puissance (A N) tels automates -argh, je peux pas faire de formule mathématique dans dotclear.

Commentaires

1. Le mardi 11 février 2014, 07:43 par Typhon

« je peux pas faire de formule mathématique dans dotclear. »

Il ne faut jamais sortir sans son LaTeX.

Typhon

Ajouter un commentaire

Le code HTML est affiché comme du texte et les adresses web sont automatiquement transformées.

Fil des commentaires de ce billet