Logique temporelle

jeudi 26 novembre 2009
par  Alain BUSSER

Si l’affectation (« mettre 2 dans x ») est souvent notée par une égalité (« x=2 ») dans les langages de programmation les plus courants, c’est parce qu’après avoir exécuté l’affectation, il y a effectivement égalité (x est vraiment égal à 2). Mais cette égalité n’est pas tout le temps vraie, ce qui mène à une logique où la valeur de vérité d’une proposition varie dans le temps.

À la question

Comment s’appelait le Président de la République Française en mai 1968 ?

Alice répond :

« Charles de Gaulle ayant été élu Président le 8 janvier 1959 et ayant démissionné le 28 avril 1969 (après avoir été réélu en 1965) était donc encore en fonction en mai 1968. D’ailleurs on se souvient de la fermeté dont il avait fait preuve alors. Le Président de la République Française s’appelait donc Charles de Gaulle en mai 1968. »

Bob, lui, répond à la même question :

« Le Président de la République Française s’appelle Nicolas Sarközy de Nagy-Bosca. Il est né le 28 janvier 1955 et avait donc 13 ans en 1968. Il a d’ailleurs pris part à un mouvement de lycéens à l’époque. Il s’appelait déjà Nicolas Sarközy de Nagy-Bosca en mai 1968. En mai 1968, le Président de la République Française s’appelait donc Nicolas Sarközy de Nagy-Bosca. »

Qui a raison ?

Exemple d’une boucle

On va considérer le script ci-dessous, qui calcule la somme des entiers consécutifs jusqu’à 5 :

  1. var somme=0;
  2. for(indice=0;indice<=5;indice=indice+1){
  3. somme=somme+indice;
  4. }

Télécharger

Voici une simulation en mode pas-à-pas, où le temps $N$ est piloté par un curseur situé en bas de la figure (La ligne en cours d’exécution est coloriée en rouge, et on a abrégé « indice=indice+1 » en « indice++ ») :

JavaScript en mode pas-à-pas

Au temps $N=0$, les deux variables $indice$ et $somme$ sont indéfinies. Au temps $N=1$, la proposition $somme=0$ est vraie (effet de l’initialisation), et le reste tant que $N\leqslant 4$ : Après ça, quand $N=5$, $somme=1$ est vraie et donc $somme=0$ ne l’est plus !

Quelques erreurs d’élèves de Seconde

  • faire aller l’indice de 5 en 5 au lieu de 1 en 1 ;
  • remettre l’indice à zéro à chaque retour dans la boucle (donc utiliser l’indice comme mesure du temps, ce qui est impossible car le temps ne revient pas en arrière) ;
  • mauvaise lecture de la sortie de la boucle (le $<=$ vu comme un $<$) ;
  • la somme initialisée à 5 au lieu de 0 ;
  • perception du début "1 3" comme une permutation des premiers entiers, donc la suite est 2...
  • Tout tableau est forcément de proportionnalité, donc la suite des valeurs de $somme$ est la table de multiplication de 5...

Ces erreurs témoignent soit d’une mauvaise perception de l’incrément, soit d’une mauvaise perception du passage du temps.

Histoire d’avoir une notation, comme il est d’usage d’écrire $p$ juste pour dire que $p$ est vraie (et $\neg p$ si $p$ est fausse), notons $p_n$ le fait que $p$ est vraie au temps $n$ (c’est-à-dire lorsque $N=n$). Cela suppose que le temps est discret [1].

Par exemple, la proposition $somme=3$ est vraie aux temps $N=7$ et $N=8$ mais pas avant ni après :

$$\neg(somme=3)_2$$

mais

$$(somme=3)_7$$

et

$$(somme=1)_2$$

Au prochain top

La logique temporelle est une logique modale, ce qui veut dire que non seulement une proposition $p$ peut être vraie ou fausse, mais qu’elle a plusieurs manières d’être vraie (par exemple, dans le futur ou dans le passé).

Le plus simple des opérateurs modaux de la logique temporelle est noté $\bigcirc$ et signifie « vrai au prochain top » (donc là encore, le temps est supposé discret et mesuré par des entiers naturels). Si l’intervalle de mesure du temps est le jour, $\bigcirc$ signifie « vrai le lendemain ».

Dans l’exemple de l’onglet précédent, on a

$\bigcirc (somme=3)_6$ puisque $(somme=3)_7$

$\neg \bigcirc(somme=3)_2$ puisque $\neg (somme=3)_3$

mais

$\bigcirc (somme=0)_3$ puisque $(somme=0)_2$

Plus généralement on a

$$\bigcirc p_n \Leftrightarrow p_{n+1}$$

Axiomes

L’opérateur $\bigcirc$ obéit aux axiomes suivants :

  • $\neg\bigcirc p \Rightarrow \bigcirc \neg p$ (ce qui ne sera pas vrai demain, sera faux demain) ;
  • $\bigcirc(p \wedge q)\Rightarrow \bigcirc p \wedge \bigcirc q$ (s’il pleut et vente demain, alors il pleuvra demain, et il y aura du vent demain) ;
  • $\bigcirc(p \vee q)\Rightarrow \bigcirc p \vee \bigcirc q$ (s’il pleut ou vente demain, alors ou bien il pleuvra demain, ou bien il y aura du vent demain).

Le certain et l’éternel

Toutes ces choses qui sont vraies seulement à certains moments mais pas tous, c’est bien compliqué. La logique temporelle s’intéresse beaucoup plus à ce qui est tout le temps vrai, avec ça au moins on est en terrain stable...

On note donc $\Box p$ le fait que $p$ est vrai mais aussi le restera toujours.

On a donc $\Box p \Rightarrow p$ mais aussi $\Box p \Rightarrow \bigcirc p$.

D’ailleurs $\Box p$ peut être défini récursivement par

$$\Box p \Leftrightarrow p \wedge \bigcirc \Box p$$

(que $p$ soit destiné à être toujours vrai à partir de maintenant, signifie que $p$ est vrai et que son statut sera le même demain).

Un exemple en algorithmique

Un exemple important d’utilisation de la logique temporelle est un invariant de boucle : Une proposition qui est vraie à l’entrée dans la boucle et le reste à chaque passage dans la boucle.

Dans l’exemple du premier onglet (somme des 5 premiers entiers), un invariant de boucle est l’égalité entre $somme$ et $\frac{indice(indice+1)}{2}$ :

$$\left(\Box somme=\frac{indice(indice+1)}{2}\right)_2$$

Ces invariants de boucle servent à démontrer qu’un algorithme fait vraiment ce qu’il est censé faire, ou à démontrer qu’il se termine un jour.

L’opérateur modal « toujours » ($\Box$) obéit aux axiomes suivants :

  • $\Box(p \wedge q) \Leftrightarrow (\Box p \wedge \Box q)$
  • $\Box p \Rightarrow \Box \Box p$ (l’éternité est éternelle)
  • $\Box(p\Rightarrow q) \Rightarrow (\Box p \Rightarrow \Box q)$ (si une implication et sa prémisse sont toujours vrais alors sa conclusion l’est aussi)
  • $\Box(p\Rightarrow \bigcirc p)\Rightarrow(p\Rightarrow \Box p)$ (si chaque fois que $p$ est vrai, il le reste le lendemain, alors dès que $p$ est vrai c’est pour toujours : C’est le principe de récurrence).

Il ne faut jamais dire jamais

Au lieu de noter le fait que $p$ n’est jamais vrai par $\Box \neg p$ on a aussi une notation duale : $\neg \Diamond p$ où $\Diamond p$ veut dire que $p$ sera vrai au moins une fois dans le futur (« $p$ est inéluctable »).

Alors $\Box p \Leftrightarrow \neg \Diamond \neg p$ et $\Diamond p \Leftrightarrow \neg \Box \neg p$ (l’inéluctable, c’est le pas toujours faux).

Une propriété dont on souhaite très fort qu’elle soit inéluctable en algorithmique, c’est l’arrêt d’un algorithme.

L’opérateur $\Diamond$ obéit à ces axiomes :

  • $\Diamond(p \vee q)\Leftrightarrow (\Diamond p \vee \Diamond q)$
  • $\Box p \Rightarrow \Diamond p$
  • $\bigcirc p \Rightarrow \Diamond p$
  • $\Diamond p \Rightarrow \Diamond \Diamond p$ (ce qui est inéluctable, est inéluctablement inéluctable : On dirait du Pierre Dac...)

Qui a raison ?

En notant $P$ le prédicat « est président » et $N$ le prédicat « a pour nom », on a

$$\exists x, P(x)_{1968}\wedge N(x)=\mbox{de Gaulle}$$

$$\exists y, P(y) \wedge N(y)=\mbox{Sarkozy}_{1968}$$

La première interprétation est celle d’Alice, la seconde celle de Bob : La différence entre les deux est le prédicat sur lequel porte la propriété « en 1968 ».

Les deux ont raison !


[1] en informatique, rythmé par les « tops » d’une horloge, dont la cadence, de l’ordre du GigaHertz, est le paramètre le plus connu d’un ordinateur.


Commentaires

jeudi 23 décembre 2010 à 16h03

Qui a raison ?

Conformément à ce qui est dit explicitement en texte et qui me semble correct, j’aurais mis à la deuxième ligne 1968 en indice à droite de N(y) et non de Sarkozy.
Le signe = me paraît mal venu. Il eut été préférable et plus simple de supprimer les quantificateurs existentiels et de substituer de Gaulle à x dans la première ligne et Sarkozy à y dans la deuxième ligne après la rectification signalée et de s’arrêter là. Les prédicats avec quantificateur existentiel s’en déduisent, si on y tient vraiment, par l’axiome d’introduction de « il existe », lequel n’est pas connu de façon évidente par le commun des mortels !

Ceci est aussi un exemple d’une phrase écrite dans la métalangue, c’est à dire ici en français, qui a deux interprétations en langue formelle. Il ne manque pas d’exemples de sujets d’examens, y compris au baccalauréat, où l’on s’est retrouvé dans cette situation au moment de la correction.