30 mai 2007
La riche zoologie des automates cellulaires
Nous avions déjà attiré votre attention sur une très bonne introduction aux automates cellulaires parue sur le site Interstices. Voici un autre article remarquablement intéressant traitant de ce même sujet, toujours sur le site Interstices.
"Les automates cellulaires modélisent des phénomènes variés tels la circulation automobile et la propagation des feux de forêt. De nouvelles techniques d’analyse classent les automates selon une échelle de complexité."
- Complication ou complexité
- Les classes de Wolfram
- Comportements inextricables
- Les groupages
- Échelles de complexité
Lire l'intégralité de cet article sur le site Interstices.
À la découverte des automates cellulaires
Qu'est-ce que la vie ? Certains phénomènes calculables peuvent-ils être considérés comme vivants ? Ce n'est pas l'objet de cet article que d'y répondre, mais de vous introduire à un domaine de l'informatique théorique qui se situe précisément à la limite des phénomènes vivants : les automates cellulaires. Le site Interstices a publié sur ce sujet une très bonne introduction :
"Explorer les relations mathématiques entre les phénomènes observés chez des êtres vivants et des machines, c'est là l'une des possibilités offertes par les automates cellulaires. Découvrez ce moyen d'investigation des processus auto-reproductifs à travers différents exemples d'automates cellulaires..."
Lire l'intégralité de cet article sur le site d'Interstices.
25 mai 2007
40 ans d'interfaces hommes-machines
Dans un très intéressant article publié sur le site d'Interstices, Michel Beaudouin-Lafon revient sur 40 ans de progrès en matière d'interfaces hommes-machines, abordant l'apparition de la souris en 1968, de l'interface graphique moderne avec l'ordinateur conceptuel Star de Xerox (photo ci-contre) et diverses autres étapes :
"Depuis qu'existent les ordinateurs, la question de l'interface avec les utilisateurs s'est posée. En quarante ans, l'interaction homme-machine (IHM) a permis de rendre l'informatique accessible à un plus grand nombre, d'une façon que nul ne pouvait prédire. Que serait le visage de l'informatique aujourd'hui sans les interfaces graphiques ?
S'il est vrai que la programmation aux clés des premiers ordinateurs pourrait être qualifiée de « manipulation directe » au sens littéral du terme, et si l'on peut présenter l'invention des langages de programmation comme un moyen de faciliter l'interaction avec les machines informatiques, ce sont bien les travaux de Ivan Sutherland sur SketchPad au début des années 1960 qui marquent le début de l'histoire de l'interaction homme-machine."
Lire l'intégralité de l'article de Michel Beaudouin-Lafon sur le site d'Interstices.
24 mai 2007
Preuves formelles, preuves calculatoires
Si elle est complètement détaillée, une preuve se ramène à l'utilisation de règles logiques, dont la correction est précisément définie de manière syntaxique : c'est là une des caractéristiques du raisonnement mathématique. Réussir cette opération en pratique demande de faire appel à l'informatique, et plus précisément à sa branche dite des méthodes formelles.
Dans cet exposé, structuré en quatre chapitres, Benjamin Werner distingue tout d'abord les deux rôles de l'ordinateur, son rôle de vérificateur formel étant bien distinct de son rôle de calculateur.
À travers plusieurs exemples, il s'attache ensuite à montrer comment les systèmes de preuves modernes, comme Coq, permettent de s'attaquer à des preuves nécessitant des calculs importants, et de répondre à des interrogations quant à la validité de certains résultats spectaculaires. Il montre ainsi comment Coq sert à prouver qu'un grand nombre est premier, puis comment ce système a permis de valider la démonstration du théorème des quatre couleurs . Il présente enfin un chantier toujours en cours, la validation de la démonstration de la conjecture de Kepler.