HISTOIRES
par David Delaunay
Hlonzo Church, Hlan Turing
et la calculabilité
S'inspirant l'un et l'autre des travaux fondateurs du logicien
Kurt Godel, Alonzo Church et Alan Turing dégagent deux
notions clés : le À-calcul et la machine de Turing. Leur but est
de préciser la notion de calculabilité. Ils ont en fait défini un
seul et même concept !
'
A
la fin du XIXe s ièc le, les fonUn nouueau langage
de me nts des m a th é ma tiqu es
sont re mi s e n cause par l' inLe mathé matic ien et log ic ie n américai n
troduction de paradoxes log iqu es e t
Alonzo C hurc h ( 1903- 1995) co nduit
e nse mbli s tes a na log ues a u paradoxe
du me nte ur affirmant « Je suis un menteur » . Cette c ri se a pa rti c ipé à l'essor
de la log ique m athé ma tique à travers
) 'ax io m a ti sa tion d e la th éor ie d es
e nse mbl es, le calcul des préd icats o u
la th éo ri e des m odè les. En 1930, le
log ic ie n Kurt G ode ) é nonce un premi e r th éo rè m e de co mpl é tud e affirmant que, s i un é noncé est vérifié dans
tous les modè les d ' une théori e, alors cet
é noncé est dé montrabl e. Pe ut-o n a lo rs
e n « ca lcul e r un e dé mon s trati o n » ?
Qu e s ig nifi e ê tre ca lc ulabl e ? Avec
Alonzo Ch u rch e t Alan Turing, o n
obtient de ux approches qui vont converge r vers une mê me dé finiti o n .
Alonzo Church écrivait initialement "x
au lieu de l x, puis le symbole
s'est transformé avec l'usage .. .
des trava ux parallè les à ceux de Godel
et s' intéresse e n particulier à défi nir ce
qui est « algorithmique ment calcul able ».
li introduit po ur ce la ce quel 'on appelle
de nos jours le À-calc ul (lire lambda calcul ). Il s'ag it d'un la ngage serva nt à
décrire et à composer des fo nct ions afi n
de déterminer ce que ce ll es-c i peuvent
calcul e r.
Dans ce langage, to utes les le ttres servent à dés igner des fo ncti o ns . Six e t y
désignent de ux fo ncti ons, écrire ,\)' signifie composer cell es-c i (ce que l' on écrit
aujo urd ' hui x o y ). S i e est un mot de ce
langage o ù po urrait a pparaître la lettre
x, Alonzo Churc h éc rit Àx .e pour désigner la fo nc ti o n qui à x assoc ie e (ce
qu e l 'o n éc rir a it x ~ e ) . A in si .
1 = Àx .x désig ne la fo ncti on identité, tandis que Àx.y désigne la fonction constante
éga le à y . Plu s géné ra lement , o n peut
aussi éc rire Àxy.e , po ur définir la fo ncTangente Hors-série n°52. Mathématiques & informatique
par David Delaunay
Hlonzo Church, Hlan Turing
et la calculabilité
S'inspirant l'un et l'autre des travaux fondateurs du logicien
Kurt Godel, Alonzo Church et Alan Turing dégagent deux
notions clés : le À-calcul et la machine de Turing. Leur but est
de préciser la notion de calculabilité. Ils ont en fait défini un
seul et même concept !
'
A
la fin du XIXe s ièc le, les fonUn nouueau langage
de me nts des m a th é ma tiqu es
sont re mi s e n cause par l' inLe mathé matic ien et log ic ie n américai n
troduction de paradoxes log iqu es e t
Alonzo C hurc h ( 1903- 1995) co nduit
e nse mbli s tes a na log ues a u paradoxe
du me nte ur affirmant « Je suis un menteur » . Cette c ri se a pa rti c ipé à l'essor
de la log ique m athé ma tique à travers
) 'ax io m a ti sa tion d e la th éor ie d es
e nse mbl es, le calcul des préd icats o u
la th éo ri e des m odè les. En 1930, le
log ic ie n Kurt G ode ) é nonce un premi e r th éo rè m e de co mpl é tud e affirmant que, s i un é noncé est vérifié dans
tous les modè les d ' une théori e, alors cet
é noncé est dé montrabl e. Pe ut-o n a lo rs
e n « ca lcul e r un e dé mon s trati o n » ?
Qu e s ig nifi e ê tre ca lc ulabl e ? Avec
Alonzo Ch u rch e t Alan Turing, o n
obtient de ux approches qui vont converge r vers une mê me dé finiti o n .
Alonzo Church écrivait initialement "x
au lieu de l x, puis le symbole
s'est transformé avec l'usage .. .
des trava ux parallè les à ceux de Godel
et s' intéresse e n particulier à défi nir ce
qui est « algorithmique ment calcul able ».
li introduit po ur ce la ce quel 'on appelle
de nos jours le À-calc ul (lire lambda calcul ). Il s'ag it d'un la ngage serva nt à
décrire et à composer des fo nct ions afi n
de déterminer ce que ce ll es-c i peuvent
calcul e r.
Dans ce langage, to utes les le ttres servent à dés igner des fo ncti o ns . Six e t y
désignent de ux fo ncti ons, écrire ,\)' signifie composer cell es-c i (ce que l' on écrit
aujo urd ' hui x o y ). S i e est un mot de ce
langage o ù po urrait a pparaître la lettre
x, Alonzo Churc h éc rit Àx .e pour désigner la fo nc ti o n qui à x assoc ie e (ce
qu e l 'o n éc rir a it x ~ e ) . A in si .
1 = Àx .x désig ne la fo ncti on identité, tandis que Àx.y désigne la fonction constante
éga le à y . Plu s géné ra lement , o n peut
aussi éc rire Àxy.e , po ur définir la fo ncTangente Hors-série n°52. Mathématiques & informatique