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 :

var somme=0;
for(indice=0;indice<=5;indice=indice+1){
somme=somme+indice;
}

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++ ») :

CarMetal - 7.3 ko
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

\fbox{\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\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 !


[1en 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.

Annonces

Prochains rendez-vous de l’IREM

Séminaire EDIM-IREM

- Mercredi 14 juin 2017, 14h-18h, PTU, Saint-Denis, salle S23.6
- Mercredi 21 juin 2017, 14h-18h, 146 route de Grand-Coude, Saint-Joseph


Brèves

Décès de Raymond Smullyan

mercredi 15 mars

Le logicien Raymon Smullyan est décédé en février 2017, à l’âge respectable de 97 ans : Il avait eu Alonzo Church comme professeur ! Pour en savoir plus, voir cet article

Travailler à plusieurs

lundi 19 décembre 2016

Les enseignements d’exploration au lycée imposent aux enseignants de travailler ensemble. Chantal Tuffery-Rochdi a analysé dans sa thèse les pratiques des enseignants de MPS (méthodes et pratiques scientifiques). Elle répond aux questions des Cahiers pédagogiques.

Un document sur Eduscol

mardi 19 mai 2015

Un document clarifiant bien la façon dont les mêmes concepts vivent en mathématiques et dans les sciences « exactes » les utilisant, publié par Eduscol en octobre 2014. Citons-les :
« Le document proposé ci-dessous s’adresse aux professeurs de mathématiques, physique-chimie et sciences de l’ingénieur intervenant dans le segment [Bac-3 ; Bac+3]. Il vise à les informer des différences de présentation et d’interprétation qui sont faites de certains concepts mathématiques dans les autres disciplines. Ces éclaircissements peuvent contribuer à harmoniser et à clarifier l’utilisation de ces notions auprès des élèves. »

Histoire de la comptabilité

vendredi 28 décembre 2012

Sur ce site (en anglais) dédié à la comptabilité, on trouve des informations intéressantes sur l’histoire et les pratiques de ce domaine, qui peuvent être utiles aux professeurs enseignant des mathématiques financières (et aussi aux autres...).

La CGE et la réforme des lycées

lundi 16 janvier 2012

La Conférence des Grandes Écoles publie 19 préconisations pour la réforme du lycée.

Sur le Web : Les 19 préconisations

Pratique des mathématiques en série STD2A

lundi 16 janvier 2012

Le site de l’IGEN offre des recommandations et des ressources pour enseigner les mathématiques en série STD2A. Les thèmes abordés (couleurs et nuances de gris, arcs et architecture, jeux vidéos, photo et tableur, perspectives parallèles...) sont de nature à donner aussi des idées d’activités aux enseignants des autres séries !

En cheminant avec Kakeya

lundi 16 janvier 2012

Un livre (à télécharger) de Vincent Borelli et Jean-Luc Rullière qui présente le calcul intégral et la dérivation en s’appuyant sur la question de Kakeya. Pour les lycéens, les étudiants et tous les esprits curieux qui souhaitent voir les mathématiques sous un jour différent.

Sur le Web : Livre à télécharger

Bicentenaire Galois

lundi 12 septembre 2011

À l’occasion du bicentenaire de la naissance d’Évariste Galois (1811-2011), l’Institut Henri Poincaré et la Société mathématique de France organisent un ensemble de manifestations et proposent un site contenant diverses ressources documentaires susceptibles d’intéresser les enseignants.

Statistiques

Dernière mise à jour

mercredi 28 juin 2017

Publication

757 Articles
Aucun album photo
133 Brèves
11 Sites Web
131 Auteurs

Visites

38 aujourd'hui
994 hier
2051602 depuis le début
10 visiteurs actuellement connectés