These de Church

These de Church

Thèse de Church

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.

Stephen Kleene a appelé le premier « thèse de Church » (en 1943 et 1952) ce que ce dernier présentait comme une définition de la calculabilité effective. Elle est connue plus récemment sous le nom de thèse de Church-Turing terminologie proposée par certains spécialistes[1] dans les années 1990, bien que Church soit sans nul doute le premier, au début des années 1930, à avoir pensé pouvoir définir formellement la calculabilité intuitive (par la λ-définissabilité)[2]. Cependant c'est l'article de Turing de 1936 et son modèle mécanique de calculabilité, qui ont définitivement emporté l'adhésion, selon Gödel, Kleene et Church lui-même.

Sommaire

Formes équivalentes de la thèse

La thèse est formulée en disant que les machines de Turing (les fonctions λ-définissables, les fonctions récursives) formalisent correctement la notion de méthode effective de calcul. On considère généralement qu'une méthode effective doit satisfaire aux obligations suivantes :

  1. l'algorithme consiste en un ensemble fini d'instructions simples et précises qui sont décrites avec un nombre limité de symboles ;
  2. l'algorithme doit toujours produire le résultat en un nombre fini d'étapes ;
  3. l'algorithme peut en principe être suivi par un humain avec seulement du papier et un crayon ;
  4. l'exécution de l'algorithme ne requiert pas d'intelligence de l'humain sauf celle qui est nécessaire pour comprendre et exécuter les instructions.

Un exemple d'une telle méthode est l'algorithme d'Euclide pour déterminer le plus grand commun diviseur d'entiers naturels ou celui qui détermine pour un entier n la longueur de la suite de Goodstein qui commence en n.

Il s'agit là d'une définition intuitive assez claire, mais pas d'une définition formelle, faute d'avoir précisé ce qu'on entend par « instruction simple et précise » ou par « l'intelligence requise pour exécuter les instructions ». On peut en revanche définir formellement ce qu'est un algorithme et pour cela on a le choix de divers formalismes. À ce stade, la thèse de Church affirme que les deux notions, intuitive « méthode effective » et formelle « algorithme », concordent.

Succès de la thèse

Au début du XXe siècle, les mathématiciens utilisaient des expressions informelles comme effectivement réalisable, il était donc important de trouver une formalisation rigoureuse de ce concept. Depuis les années 1940, les mathématiciens utilisent grâce à la thèse de Church une notion bien définie, celle de fonction calculable.

La thèse a d'abord été formulée pour le lambda-calcul, mais d'autres formalismes ont été proposés pour modéliser les fonctions calculables, par exemple les fonctions récursives, les machine de Turing, les machines de Post et les machines à compteurs. La plus surprenante est probablement celle proposée par Yuri Matiyasevich en résolvant le dixième problème de Hilbert. On peut montrer que toutes ces définitions, bien que fondées sur des idées assez différentes, décrivent exactement le même ensemble de fonctions. Ces systèmes, qui ont le même pouvoir d'expression que l'une quelconque de ces définitions équivalentes, sont dits Turing-équivalents ou Turing-complets.

Le fait que toutes ces tentatives pour formaliser le concept d'algorithme aient conduit à des résultats équivalents est l'argument qui rend la thèse de Church incontournable.

Histoire

Dans son article de 1943 Prédicats et quantificateurs récursifs (titre original Recursive Predicates and Quantifiers) Stephen Kleene (repris dans L'Indécidable, titre original The Undecidable) a proposé pour le premier énoncé de la thèse de Church qu'il appelle « THÈSE I » :

« Ce fait heuristique [les fonctions récursives générales sont effectivement calculables]… a conduit Church à énoncer la thèse suivante »

— [note 22 de Kleene], La même thèse est implicite dans la description des machines de Turing [note 23 de Kleene].

« THÈSE I. Chaque fonction effectivement calculable (chaque prédicat effectivement décidable) est récursive générale [les italiques sont de Kleene] »
« Puisque nous recherchions une définition mathématique précise de l'expression effectivement calculable (effectivement décidable), nous prendrons cette thèse comme sa définition ... »

— Kleene, dans l'indécidable, p. 274

La note 22 de Kleene fait référence à l'article de Church tandis que sa note 23 fait référence à l'article d'Alan Turing. Il continue en notant que

« … la thèse n'est qu'une hypothèse -- une constatation déjà soulignée par Post et par Church »

— [sa note 24, dans L'indécidable, P. 274], Il fait référence à l'article de Post (1936) et aux définitions formelles de l'article de Church Formal definitions in the theory of ordinal numbers, Fund. Math. vol. 28 (1936) pp.11-21 (voir réf. 2, P. 286, de l'indécidable).

Dans son article de 1936 « sur des nombres calculables, avec une application à l'Entscheidungsproblem » (titre original « On Computable Numbers, with an Application to the Entscheidungsproblem  ») Turing a formalisé la notion d'algorithme (alors appelée « calculabilité effective »), en introduisant les machines dites maintenant de Turing. Dans cet article il écrit en particulier à la page 239 :

« Une suite calculable γ est déterminée par une description d'une machine qui calcule γ ... et, en fait, n'importe quelle suite calculable est susceptible d'être décrite en termes d'une table [c'est-à-dire d'une machine de Turing]. »

—  , ce qui est la version de Turing de la thèse de Church, qu'il ne connaissait pas à l'époque.

Church avait démontré lui aussi quelques mois plus tôt l'insolvabilité du problème de la décision dans « une note sur l'Entscheidungsproblem » pour cela il avait utilisé les fonctions récursives et les fonctions λ-définissables pour décrire formellement le calculabilité effective. Les fonctions λ-définissables avait été introduites par Alonzo Church et Stephen Kleene (Church 1932, 1936a, 1941, Kleene 1935) et les fonctions récursives avaient été introduites par Kurt Gödel et Jacques Herbrand (Gödel 1934, Herbrand 1932). Ces deux formalismes décrivent le même ensemble de fonctions, comme cela a été démontré dans le cas des fonctions sur les entiers positifs par Church et Kleene (Church 1936a, Kleene 1936). Après avoir entendu parler de la proposition de Church, Turing a pu rapidement esquisser une démonstration que ses machines de Turing décrivent en fait le même ensemble de fonctions (Turing 1936, 263 et suivantes). Dans un article paru en 1937[3] il montre l'équivalence des trois modèles: fonctions λ-définissables, machines de Turing[4] et fonctions générales récursives au sens de Herbrand et Gödel. Rosser[5] résume les sentiments des protagonistes :

« Une fois l'équivalence de la récursivité générale et de la λ-définsissabilité établie, Church, Kleene et moi nous attendions à ce que Gödel nous rejoignent pour supporter la thèse de Church. Gödel avait cependant encore des réserves et ça n'est qu'au moins deux ou trois ans plus tard, après les travaux de Turing, que Gödel devint finalement un adepte (comme le devint aussi Turing). »

Turing écrit[6] en 1937 :

« L'identification des fonctions 'effectivement calculables' avec les fonctions calculables [c-à-d. définies par une machine de Turing] est peut-être plus convaincante que l'identification avec les fonctions λ-définissables ou récursives générales. Pour ceux qui adoptent ce point de vue, la démonstration formelle de l'équivalence fournit une justification du calcul de Church et permet de remplacer les 'machines' qui engendrent des fonctions calculables par les λ-définitions qui sont plus commodes. »

Des fonctions et nombres non calculables

On peut définir très formellement des fonctions (par exemple sur les entiers naturels) qui ne sont pas calculables. Elles prennent en général des valeurs tellement grandes que l'on ne peut pas les calculer et par conséquent on ne peut même pas « exprimer » les valeurs qu'elles prennent, car c'est leur définition qui le dit. La plus connue est celle dite du castor affairé. Pour simplifier, il s'agit de la taille du plus grand travail que peut faire une machine de Turing quand on lui donne une ressource limitée par n. Comme sa définition est obtenue comme une limite de ce que pourraient faire les machines de Turing, le nombre qu'elle produit ne peut pas être calculé, ni même sa valeur exacte exprimée, tout au plus les chercheurs arrivent-ils à donner des nombres qui lui sont inférieurs pour les plus petites valeurs de n (2, 3, 4, 5, péniblement 6).

Le nombre Oméga de Chaitin est un nombre réel parfaitement défini qui n'est pas calculable, précisément parce que sa construction dépend des réponses au problème semi-décidable de l'arrêt des machines de Turing.

Voir aussi

Références

  1. voir Robert I. Soare, article cité.
  2. attesté pas une lettre de Church à Gödel de 1934, voir Soare, article cité
  3. Computability and λdefinissability in J. Symb Logic, vol. 2, pp. 153-163. voir aussi Collected Works of A.M. Turing, tome Mathematical Logic
  4. La terminologie est due à Church.
  5. In Highlights of the History of the Lambda-Calculus, Annals of the History of Computing vol. 6, n°4, oct 1984.
  6. in Computability and λdefinissability

Articles connexes

Sources

Articles originaux

  • Alonzo Church, 1935, An Unsolvable Problem of Elementary Number Theory (abstract), Bull. Amer. Math. Soc. 41 (1935), pp 332-333.
  • Alonzo Church, 1936, An Unsolvable Problem of Elementary Number Theory, American Journal of Mathematics, 58, pp 345-363.
  • Alonzo Church, 1936, A Note on the Entscheidungsproblem, Journal of Symbolic Logic, 1, pp 40-41, correction pp 101-102.
  • Kurt Gödel, 1934, On Undecidable Propositions of Formal Mathematical Systems, lecture notes taken by Kleene and Rosser at the Institute for Advanced Study, reprinted in Davis, M. (ed.) 1965, The Undecidable, New York: Raven Press.
  • Jacques Herbrand, 1931, Sur la non-contradiction de l'arithmétique, Journal fur die reine und angewandte Mathematik, 166, pp 1-8.
  • Stephen Cole Kleene, 1936, Lambda-Definability and Recursiveness, Duke Mathematical Journal 2, pp 340-353.
  • Stephen Cole Kleene, 1943, Recursive predicates and quantifiers, Trans. A.M.S. 53, pp 41-73.
  • Alan Turing, 1936, On Computable Numbers, with an Application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, Series 2, 42 (1936-37), pp.230-265, A correction, vol 43 pp 544-546
  • Alan Turing, 1937, Computability and λ-definability, J. Symbolic Logic, 2 (1937), pp 153-163.

Autres (en anglais)

  • Martin Davis editor, The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions, Raven Press, New York, 1965. Les articles originaux dont ceux de Gödel, Church, Turing, Rosser, Kleene, and Post. Préfaces de Davis.
  • Stephen Cole Kleene, 1952, "Introduction to Metamathematics", Van Nostrand, New York.
  • Stephen Cole Kleene, Origins of Recursive Function Theory in Annals of the History of Computing, Vol. 3 No. 1, janvier 1981.
  • Barkley Rosser Highlights of the History of the Lambda-Calculus, Annals of the History of Computing 6,4 [1984], 337-349
  • Robert Soare, (1995-6), Computability and Recursion, Bulletin of Symbolic Logic 2 (1996), 284--321, version en ligne, article sur l'historique de la calculabilité, qui milite pour un certain nombre de changements terminologiques, écrit par un spécialiste du domaine.
  • Wilfried Sieg Step by recursive step: Church's analysis of effective calculability. Bulletin of Symbolic Logic 3(2): 154-180 (1997).
  • Collected Works of A. M. Turing vol. Mathematical Logic, eds. R. O. Gandy and C. E. M. Yates, ISBN 0-444-50423-0.

Autres (en français)

  • Portail de l’informatique Portail de l’informatique
  • Portail des mathématiques Portail des mathématiques
Ce document provient de « Th%C3%A8se de Church ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article These de Church de Wikipédia en français (auteurs)

Игры ⚽ Нужно сделать НИР?

Regardez d'autres dictionnaires:

  • Thèse de church — 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… …   Wikipédia en Français

  • Thèse de Church — La thèse de Church du nom du mathématicien Alonzo Church est une hypothèse ( thèse ) concernant la définition de la notion de calculabilité. Dans une forme dite physique [1], elle affirme que la notion physique de la calculabilité, définie comme… …   Wikipédia en Français

  • Thèse de Church-Turing — Thèse de Church 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… …   Wikipédia en Français

  • These von Church — Die Church Turing These (benannt nach Alonzo Church und Alan Turing, auch Churchsche These genannt) trifft Aussagen über die Fähigkeiten einer Rechenmaschine. Sie lautet: Die Klasse der Turing berechenbaren Funktionen ist genau die Klasse der… …   Deutsch Wikipedia

  • thèse de Church-Turing — ● loc. f. ►MATH Voir l URL (en anglais)... Voir aussi Church, Alonzo et Turing, Alan Mathison. http://plato.stanford.edu/entries/church turing/ …   Dictionnaire d'informatique francophone

  • Church History —     Ecclesiastical History     † Catholic Encyclopedia ► Ecclesiastical History     I. NATURE AND OFFICE     Ecclesiastical history is the scientific investigation and the methodical description of the temporal development of the Church… …   Catholic encyclopedia

  • Thèse Church-Turing — Thèse de Church 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… …   Wikipédia en Français

  • CHURCH (A.) — CHURCH ALONZO (1903 ) Mathématicien et logicien, philosophe et historien de la logique, Alonzo Church est né à Washington. Professeur de mathématiques à l’université de Princeton, directeur du Journal of Symbolic Logic , il est selon Kneale «le… …   Encyclopédie Universelle

  • Church of Christ — For individual church buildings/congregations, see Church of Christ (disambiguation). The term Church of Christ may refer to: One of several New Testament designations for a local band of people following the teachings of Jesus, whom they… …   Wikipedia

  • Church, Alonzo — ● /t(ch)*rt(ch)/ np. ►PERS (14/06/1903 11/08/1995). Mathématicien ayant énoncé sa thèse en 1936 à Princeton. La thèse de Church affirme que toute fonction calculable peut l être avec un ensemble réduit d instructions. C est une affirmation… …   Dictionnaire d'informatique francophone

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”