Du bruit au signal (et inversement)

Aller au contenu | Aller au menu | Aller à la recherche

Tag - informatique théorique

Fil des billets - Fil des commentaires

vendredi 9 janvier 2009

Les langages de programmation spécialisés sont-ils de véritables langages ?

Un petit billet sur les langages de programmation spécialisés pour commencer l'année. Et tout d'abord un bref rappel:

"Un langage de programmation est dit Turing-complet s'il permet de représenter toutes les fonctions calculables au sens de Turing et Church (nonobstant la finitude de la mémoire des ordinateurs). La plupart des langages usuels de programmation (C, C++, Java, ...) sont Turing-complets. Le fait d'être Turing-complet est généralement requis pour un langage de programmation générique. En revanche, ce n'est pas le cas pour un langage dédié au traitement de problèmes spécifiques." (extrait de Wikipedia)

La dernière phrase ne doit pas être comprise de travers. On pense parfois qu'un langage très spécialisé, dédié au traitement de problèmes spécifiques comme le scripting, le développement Web, ou le traitement graphique, ne peut être considéré comme un véritable langage permettant d'exprimer n'importe quel problème basé sur un algorithme mécanique (moyennant la thèse de Church). Il n'en est rien. Les langages de programmation spécialisés ne sont pas tous des langages "au rabais". Certains d'entre eux qui semblent pourtant conçus pour des tâches extrêmement précises doivent pourtant être considérés comme de "vrais langages universels" car ils sont Turing-complet. Deux exemples:

mardi 25 mars 2008

Quand peut-on dire que deux algorithmes sont identiques ?

When Are Two Algorithms The Same? par Andreas Blass, Nachum Dershowitz, et Yuri Gurevich.

« On considère généralement que les algorithmes sont plus abstraits que les programmes qui les implémentent. La manière naturelle de formaliser cette idée est de considérer que les algorithmes constituent des classes d'équivalence de programmes selon une certaine relation d'équivalence appropriée. Nous soutenons dans cet article qu'il n'existe pas de telle relation d'équivalence.  »

"Capturer" la notion intuitive d'algorithme (de façon analogue à la thèse de Church-Turing qui tente de "capturer" la notion intuitive de calculabilité) signifie être capable de proposer une définition de la relation d'équivalence qui relie deux algorithmes identiques (et pas seulement deux algorithmes qui calculent la même fonction). L'objet de l'article est de mettre en avant plusieurs difficultés concernant cette tentative et de donner des exemples qui indiquent que la notion intuitive n'est pas suffisamment bien définie pour permettre de définir une relation d'équivalence précise.
L'argument principal est que l'équivalence entre algorithmes est une notion subjective.
L'article aborde aussi des problèmes analogues comme la question de reconnaître quand deux preuves sont identiques ou deux idées sont identiques.

Lire aussi les billets sur God Plays Dice et Lambda the Ultimate.

dimanche 9 mars 2008

La thèse de Church : hier, aujourd'hui, demain

« La thèse de Church - du nom du mathématicien Alonzo Church - est le principe de base de la calculabilité. Dans sa forme la plus ordinaire, elle affirme que tout traitement réalisable mécaniquement peut être accompli par un ordinateur (plus précisément dans sa forme idéalisée qu'est une machine de Turing). Dans une forme plus élaborée, elle affirme qu'un concept intuitif, la calculabilité effective, coïncide avec un concept formel et mathématique, la calculabilité, défini de plusieurs façons dont on a pu démontrer mathématiquement qu'elles sont équivalentes. » (Wikipedia)

Colloque de philosophie de l’informatique

La thèse de Church : hier, aujourd'hui, demain
Regards croisés de philosophes et de théoriciens du calcul

VENDREDI 11 avril 2008 Centre Sorbonne, amphi. Descartes
Le colloque se déroulera entre 9h30 et 18h45, amphithéâtre Descartes, université Paris 1 (Panthéon-Sorbonne), 17 rue de la Sorbonne, 75005.

Tel qu’appréhendé par l’informatique théorique contemporaine, le calcul n’a plus guère de traits communs avec l’artefact qu’avaient proposé, au début du XXe siècle, les premières théories de la calculabilité (machines de Turing etc) et dans le contexte desquelles la fameuse « Thèse de Church » fut énoncée. Sous le regard contemporain, le calcul diffère de son ancêtre à la fois par ses propriétés (parallélisme, non déterminisme, concurrence), par la multiplicité de ses échelles (calcul sur les réels, fonctionnalité d’ordre supérieur, complexités intermédiaires) et par ses liens avec les sciences de la nature (calcul quantique, bio-calcul). Quel impact ces métamorphoses du calcul ont-elles sur l’horizon fermé, il y a soixante-dix ans, par la thèse de Church ? Qu’impliquent-elles quant à la question ouverte par la « version physique » de la thèse de Church : la nature calcule-t-elle ?

Coordination : Jean-Baptiste Joinet
Participation libre
Plus d'informations ici (intervenants et programme des exposés)

mercredi 20 février 2008

History of Lambda-Calculus and Combinatory logic

The formal systems that are nowadays called λ-calculus and combinatory logic were both invented in the 1920s, and their aim was to describe the most basic properties of function-abstraction, application and substitution in a very general setting. In λ-calculus the concept of abstraction was taken as primitive, but in combinatory logic it was defined in terms of certain primitive operators called basic combinators. The present article will sketch the history of these two topics through the twentieth century.
.../...
Seen in outline, the history of λ and CL splits into three main periods:  first, several years of intensive and very fruitful study in the 1920s and ’30s; next, a middle period of nearly 30 years of relative quiet; then in the late 1960s an upsurge of activity stimulated by developments in higher-order function theory, by connections with programming languages, and by new technical discoveries.  The fruits of the first period included the first-ever proof that predicate logic is undecidable.  The results of the second attracted very little non-specialist interest, but included completeness, cut-elimination and standardization theorems (for example) that found many uses later.  The achievements of the third, from the 1960s onward, included constructions and analyses of models, development of polymorphic type systems, deep analyses of the reduction process, and many others probably well known to the reader. The high level of activity of this period continues today.
.../...
By Felice Cardone and  J. Roger Hindley, 2006
To be published in Volume 5 of Handbook of the History of Logic, Editors Dov M. Gabbay and John Woods, Elsevier Co.

Article au format PDF

Voir aussi:
Proofs and Types by Jean-Yves Girard, translated and with appendices by Paul Taylor and Yves Lafont
Cambridge University Press, 1989