divine recursion
introduction
« Pour comprendre la récurion vous devez comprendre la récursion. »
« To understand recursion, you must understand recursion. »
En d'autres termes "passez votre chemin" vous ne comprendrez rien à la récursion si vous ne faites pas partie des heureux élus. Dans ce papier, prenant des chemins de traverse oubliés, je me propose de démontrer le contraire, de montrer pourquoi elle nous est consubstantielle et pourquoi elle nous concerne tous en tant qu'humains.
In other words "go your way" you will not understand anything about recursion if you are not among the lucky ones. In this paper, taking forgotten byways, I propose to demonstrate the opposite, to show why recursion is consubstantial to us and why it concerns us all as humans.
Je commencerai le voyage avec cette étrange et minuscule expression :
I'll start the journey with this strange and tiny expression:
λw.x w
écrite au milieu des années 30 à Princeton par le mathématicien Alonzo Church dans la syntaxe d'un langage qu'il développait, le λ-calcul, une dizaine d'années avant l'apparition du premier ordinateur.
written in the mid-1930s at Princeton by the mathematician Alonzo Church in the syntax of a language he was developing, the λ-calculus, about ten years before the first computer appeared.
Le λ-calcul est habituellement défini par les règles suivantes
The λ-calculus is usually defined by the following rules
x := w // mot/word | λw.x // abstraction | x x // application
ce qui se lit ainsi « une expression x est soit un mot, w, soit une abstraction, λw.x, soit une application, x x. », ce qui ne nous avance guère pour l'instant. Je note simplement que dans l'application x x le premier x peut être une abstraction, λ.w x, et le second x un mot, w, ce qui conduit à l'expression λw.x w qui va nous servir de base.
which reads " an expression x is either a word, w, or an abstraction, λw.x, or an application, x x", which does not advance us much for the moment. I simply note that in the application x x the first x can be an abstraction, λ.w x, and the second x a word, w, which leads to the expression λw.x w which will serve as a basis.
Et ça simplifie tout !
And that simplifies everything!
This page is an editable lambdatalk program!
Cette page est un programme lambdatalk modifiable !
Ce qui veut dire que vous pouvez ouvrir l'éditeur du code de la page - en cliquant sur le mot "divine_recursion" du titre en haut de la page - survoler le code en repérant les correspondances avec l'affichage - c'est facile pour les blocs de texte pur - et, une fois familiarisés, vous pouvez modifier à votre guise, sans autre risque que de devoir recharger la page si les choses vont mal. C'est en bidouillant le code qu'on finit par le comprendre.
This means that you can open the page's code editor - by clicking on the word "divine_recursion" in the title at the top of the page - hover over the code, spotting matches with the display - this is easy for pure text blocks - and, once you're familiar with it, you can modify it as you like, without any risk other than having to reload the page if things go wrong. It's only by tinkering with the code that you get the hang of it.
syntax
Je ne réécrirai pas, après tant d'autres, une introduction "académique" à ce langage, jugé par certains comme inaccessible au commun des mortels et je commencerai par une commande simple écrite dans mon langage natal, le français.
I will not rewrite, after so many others, an "academic" introduction to this language, considered by some as inaccessible to the common man, and I will start with a simple command written in my native language, french.
remplace : :a & :b
dans : Je m'appelle :b, :a :b !
par : james & bond
Il s'agit donc simplement de remplacer deux mots ":a" et ":b" dans la phrase "Je m'appelle :b, :a :b !" par deux autres mots "james" et "bond". Et je suis sûr que vous devinez la réponse : "Je m'appelle bond, james bond !"
So it's just a matter of replacing two words ":a" and ":b" in the sentence "My name is :b, :a :b !" with two other words "james" and "bond". And I'm sure you can guess the answer, "My name is bond, james bond!"
Bienvenue dans le monde du code, vous venez d'écrire votre premier "programme", et vous pourrez l'appliquer à toute sorte de prénoms et noms, Ward Cunningham, Monica Bellucci, ... et jouer avec bien d'autres combinaisons différentes, à l'infini.
Welcome to the world of code, you have just written your first "program", and you will be able to apply it to all kinds of names, Ward Cunningham, Monica Bellucci, ... and play with many other different combinations, endlessly.
Il reste un petit problème : mon ordinateur ne comprend pas ce langage, ne serait-ce que parce qu'il est ... anglophone. J'ai bien essayé de lui parler en anglais
There is still one small problem: my computer doesn't understand this language, if only because it is... English-speaking. I tried to talk to it in English
replace : :a & :b
in : My name is :b, :a :b!
by : james & bond
sans plus de succès.
without further success.
Je me suis donc adressé à Alonzo Church qui m'a gentiment proposé de réécrire la formule λw.x w en suivant la syntaxe parenthésée préfixée d'un de ses descendants, John McCarthy, l'inventeur du LISP en 1958. J'ai donc écrit
So I approached Alonzo Church who kindly offered to rewrite the formula λw.x w following the prefixed parenthetical syntax of one of his descendants, John McCarthy, the inventor of LISP in 1958. So I wrote
{{lambda {:a :b} My name is :b, :a :b! } james bond}
où l'on voit que le mot lambda remplace le mot replace et que les conjonctions &, in, by sont remplacées par un jeu "bien balancé" d'accolades, {}.
where we see that the word lambda replaces the word replace and that the conjunctions &, in, by are replaced by a "well balanced" set of braces, {}.
Et ça marche ! Mon ordinateur répond
And it works! My computer responds
My name is bond, james bond!
Note : Vous pouvez le vérifier par vous-même : ouvrez l'éditeur de cette page (en repérant le titre de la page, lambdaway :: divine_recursion et en cliquant sur le mot divine_recursion) ; puis faites défiler le code jusqu'au passage précédent et constatez que la portion de code {{lambda {:a :b} My name is :b, :a :b!} james bond} a bien été remplacée par My name is bond, james bond!. Remplacez les noms par ce que vous voulez et constatez les changements.
Note: You can check this for yourself: open the editor for this page (by locating the title of the page, lambdaway :: divine_recursion and clicking on the word divine_recursion); then scroll down to the previous passage and see that the portion of code {{lambda {:a :b} My name is :b, :a :b! } james bond} has been replaced by My name is bond, james bond!. Replace the names with whatever you want and see the changes.
Cette syntaxe est évidemment moins "lisible" que la commande initiale mais le gain est énorme, je ne suis plus seul, j'ai maintenant un compagnon d'une infinie patience qui peut me seconder dans de nombreuses explorations dans le monde des algorithmes, à l'infini. Un compagnon présent dans n'importe quel navigateur web, sur n'importe quel ordinateur, tablette ou smartphone.
This syntax is obviously less "readable" than the initial command but the gain is enormous, I am no longer alone, I now have a companion of infinite patience who can assist me in many explorations in the world of algorithms. A companion present in any web browser, on any computer, tablet or smartphone.
De manière générale la formule λw.x w s'écrira ainsi
In general, the formula λw.x w can be written as follows
{{lambda {:variables} expression} values}
Avant de commencer une exploration qui nous conduira pas à pas vers la compréhension sans ombre de la récursion, qui est l'objet de ce papier, je voudrais répondre à une question que vous vous êtes probablement posée : « Pourquoi les noms de variables sont-ils préfixés par un caractère ":" ? »
Before we begin an exploration that will lead us step by step to the shadowless understanding of recursion, which is the focus of this paper, I would like to answer a question you have probably asked yourself, "Why are variable names prefixed by a ":" character?"
Testons donc l'écriture sans les ":"
Let's test the writing without the ":"
{{lambda {a b} My name is b, a b! } james bond} -> My njamesme is bond, james bond!
Pas vraiment le résultat attendu ! Et pourtant très logique, le caractère a du mot name a lui aussi été remplacé par le mot james, devenant ainsi njamesme, et ce n'est pas ce que nous voulons. En préfixant le nom des variables par un caractère "spécial", :a, on protège le caractère a du mot name. Un autre avantage à systématiquement respecter cette convention est que les noms de variable se distinguent mieux des autres mots de la phrase.
Not really the expected result! And yet very logical, the character a of the word name has also been replaced by the word james, thus becoming njamesme, and this is not what we want. By prefixing variable names with a "special" character, :a, we protect the a character of the word name. Another advantage of consistently following this convention is that variable names are more distinct from other words in the sentence.
La commande initiale s'applique bien sûr à d'autres noms, par exemple
The initial command applies of course to other names, for example
{{lambda {:a :b} My name is :b, :a :b!} james bond} -> My name is bond, james bond! {{lambda {:a :b} My name is :b, :a :b!} ward cunningham} -> My name is cunningham, ward cunningham! {{lambda {:a :b} My name is :b, :a :b!} monica bellucci} -> My name is bellucci, monica bellucci!
lambda & def
C'est quand même un peu lourd et répétitif. Donnons un nom simple, par exemple HI, à l'expression interne {lambda {:a :b} My name is :b, :a :b!} qui revient trois fois à l'identique
It's still a bit cumbersome and repetitive. Let's give a simple name, for example HI, to the internal expression {lambda {:a :b} My name is :b, :a :b!} which comes back three times in the same way
{def HI {lambda {:a :b} My name is :b, :a :b!}} -> HI
où def signifie définir. On vient de donner un nom à une abstraction, on a caché l'expression {lambda {:a :b} My name is :b, :a :b!} sous le nom HI. Nous avons créé une fonction attendant deux mots, cette fonction est enregistrée dans un dictionnaire. Et on peut maintenant réécrire de façon très lisible les trois commandes précédentes
where def means define. We have just given a name to an abstraction, we have hidden the expression {lambda {:a :b} My name is :b, :a :b!} under the name HI. We have created a function waiting for two words, this function is stored in a dictionary. And we can now rewrite the three previous commands in a very readable way
{HI james bond} -> My name is bond, james bond! {HI ward cunningham} -> My name is cunningham, ward cunningham! {HI monica belluci} -> My name is belluci, monica belluci!
Nous avons appliqué des abstractions à des mots. C'est exactement ainsi que nous allons procéder pour la suite, utilisant de façon conjointe des abstractions et des applications opérant sur des mots. L'abstraction, principe féminin, le Yin, et l'application, principe masculin, le Yang, opêrant sur un océan de mots. Au début êtait le verbe. Un avant-gout du TAO. Pourquoi pas ?
We have applied abstractions, (functions) to words. This is exactly how we will proceed in the following, using both abstractions and applications operating on words. The abstraction, the feminine principle, Yin, and the application, the masculine principle, Yang, operating on a sea of words. In the beginning was the verb. A foretaste of TAO. Why not?
Nous avons maintenant l'outillage nécessaire et suffisant pour construire les fondations d'un langage primitif.
We now have the necessary and sufficient tools to build the foundations of a primitive language.
Note : j'ai pris le parti de choisir l'anglais dans les exemples de code, afin de rester proche des noms utilisés dans la littérature informatique.
Note : I have chosen to use English in the code examples, in order to stay close to the names used in the computer literature.
Comme premier exemple de fonction voici la fonction identité, I
As a first example of a function here is the identity function, I
{def I {lambda {:a} :a}} -> I {I james} -> james {I ward} -> ward
On a bien compris, I n'est autre que {lambda {:a} :a} qui attend un mot et le retourne tel quel. Continuons avec une fonction échangeant deux mots
We have understood well, I is none other than {lambda {:a} :a} which waits for a word and returns it as is. Let's continue with a function exchanging two words
{def SWAP {lambda {:a :b} :b :a}} -> SWAP {SWAP james bond} -> bond james
Rien n'empêche de combiner les fonctions HI et SWAP
There is nothing to prevent combining the functions HI and SWAP
{def YEP {lambda {:a :b} My name is :b, {SWAP :a :b}! }} -> YEP {YEP james bond} -> My name is bond, bond james!
Faites une pause. Essayez d'écrire la fonction YEP en langage naturel et vous comprendrez vite en quoi la syntaxe choisie devient vite indispensable.
Take a break. Try to write the function YEP in natural language and you will quickly understand how the chosen syntax becomes indispensable.
Dans tout ce qui précède il ne s'agit que de remplacement de texte, on joue avec des mots. Mais d'habiles combinaisons de mots et de fonctions vont nous permettre de créer des assemblages bien plus complexes, à l'infini. Commençons par un jeu de fonctions introduisant un concept clé, le choix.
In all of the above, we are only talking about text replacement, we are playing with words. But clever combinations of words and functions will allow us to create much more complex assemblies, ad infinitum. Let's start with a set of functions introducing a key concept, the choice.
bifurcation
Il y a toujours le moment où l'on doit choisir entre deux chemins. C'est là qu'apparaissent deux mots chargés de sens, le vrai et le faux, TRUE & FALSE.
There is always the moment when one has to choose between two paths. This is where two words with meaning appear, true and false, TRUE & FALSE.
{def TRUE {lambda {:a :b} :a}} -> TRUE {def FALSE {lambda {:a :b} :b}} -> FALSE {TRUE da niet} -> da {FALSE da niet} -> niet
Analysons {TRUE da niet}
Let's analyse {TRUE da niet}
0: {TRUE da niet} - TRUE => {lambda {:a :b} :a} - da => da - niet => niet ↑‾‾‾‾‾‾↓ 1: {{lambda {:a :b} :a} da niet} ↑__________↓ 2: da
A ce stade l'essentiel est de comprendre la simplicité du processus, la fonction TRUE retourne le premier des deux mots, la fonction FALSE retourne le second. On ajoute une troisième fonction, IF
At this stage the main thing is to understand the simplicity of the process, the function TRUE returns the first of the two words, the function FALSE returns the second. We add a third function, IF
{def IF {lambda {:a :b :c} {:a :b :c}}} -> IF {IF TRUE oui non} -> oui {IF FALSE oui non} -> non
Que peut bien signifier le corps de la lambda, {:a :b :c} ? Analysons le fonctionnement de l'expression {IF TRUE oui non} en remplaçant les noms par leurs lambda expressions
What can the body of the lambda expression, {:a :b :c}, mean? Let's analyze how the expression {IF TRUE oui non} works by replacing the names with their lambda expressions
0: {IF TRUE oui non} - IF => {lambda {:a :b :c} {:a :b :c}} - TRUE => {lambda {:a :b} :a} - oui => oui - non => oui ↓‾‾‾‾‾‾‾‾‾↑_________________ 1: {{lambda {:a :b :c} {:a :b :c}} {lambda {:a :b} :a} oui non} ↑__↑________________________↓___↓ - :a => {lambda {:a :b} :a}, - :b => oui, - :c => non. ↑‾‾‾‾‾‾↓ 2: {{lambda {:a :b} :a} oui non} ↑__________↓ - :a => oui 3: oui et voilà !
Relisez bien, lentement, jusqu'à ce que cette suite de remplacements vous devienne famillière. C'est du solfège, de l'algèbre, c'est un cap à passer, pas si facile. Mais c'est bien plus simple que les règles du tennis ... que je n'ai jamais eu la patience de lire jusqu'au bout. Mais ici l'effort nous donne la clé d'accès au monde du code. Le retour sur investissement est assuré. Courage.
Read it again, slowly, until this sequence of replacements becomes familiar to you. It's solfeggio, algebra, it's a step to take, not so easy. But it is much simpler than the rules of tennis ... which I never had the patience to read to the end. But here the effort gives us the key to the world of code. The return on investment is assured. Take heart.
En l'espace de trois petites fonctions nous venons de créer une "structure de contrôle" if then else, "si une condition est remplie alors prend le premier mot sinon le second." Notons que cela ne fonctionne que pour deux mots, il n'est pas encore possible de choisir entre deux phrases. Pour cela nous devrons construire des aggrégations de mots, des structures de données, à commencer par l'agrégation de deux mots.
In the space of three small functions we have just created a "control structure" if then else, "if a condition is met then takes the first word otherwise the second." Note that this only works for two words, it is not yet possible to choose between two sentences. For that we will have to build word aggregations, data structures, starting with the two-word aggregation.
agregation
Une phrase est une suite de mots, il est utile de la considérer comme un tout. Commençons avec deux mots.
A sentence is a sequence of words, so it is useful to think of it as a whole. Let's start with two words.
On définit une paire, un couple de deux mots, à l'aide de trois fonctions, une fonction construisant la paire, PAIR, et deux fonctions retournant chacun des deux mots aggrégés, LEFT & RIGHT.
We define a pair, a pair of two words, using three functions, a function constructing the pair, PAIR, and two functions returning each of the two aggregated words, LEFT & RIGHT.
{def PAIR {lambda {:a :b :c} {:c :a :b}}} -> PAIR {def LEFT {lambda {:c} {:c TRUE}}} -> LEFT {def RIGHT {lambda {:c} {:c FALSE}}} -> RIGHT {def JB {PAIR james bond}} -> JB {LEFT {JB}} -> james {RIGHT {JB}} -> bond
Analysons le fonctionnement de l'expression {LEFT {JB}} en remplaçant les noms par leurs lambda expressions
Let's analyze how the expression {LEFT {JB}} works by replacing the names by their lambda expressions
0: {LEFT {JB}} - LEFT => {lambda {:c} {:c TRUE}} - {JB} => {PAIR james bond} 1: {{lambda {:c} {:c TRUE}} {PAIR james bond}} - TRUE => {lambda {:a :b} :a} - PAIR => {lambda {:a :b :c} {:c :a :b}} 2: {{lambda {:c} {:c {lambda {:a :b} :a}}} {{lambda {:a :b :c} {:c :a :b}} james bond}} - {{lambda {:a :b :c} {:c :a :b}} james bond} => {lambda {:c} {:c james bond}} 3: {{lambda {:c} {:c {lambda {:a :b} :a}}} {lambda {:c} {:c james bond}}} - :c => {lambda {:c} {:c james bond}} 4: {{lambda {:c} {:c james bond}} {lambda {:a :b} :a}} - :c => {lambda {:a :b} :a} 5: {{lambda {:a :b} :a} james bond} - :a => james 6: james
Toujours là ?
Still here?
Oui c'est laborieux, mais c'est une application absolument systématique du processus de remplacement qui devrait devenir quasi automatique, et qui l'est de fait pour l'ordinateur, sans état d'âme, à la vitesse de la lumière.
Yes, it is laborious, but it is an absolutely systematic application of the replacement process which should become almost automatic, and which is in fact automatic for the computer, without any qualms, at the speed of light.
Le seul point délicat, car nouveau, se trouve dans le passage de la ligne 2: à la ligne 3:. En effet dans l'expression {{lambda {:a :b :c} {:c :a :b}} james bond} on note que la fonction attend trois valeurs, :a, :b, :c et qu'elle n'en reçoit que deux. Eh bien elle s'en contente et retourne à la volée une nouvelle fonction "anonyme" {lambda {:c} {:c james bond}} dans laquelle les variables :a & :b ont été remplacées par les mots james & bond, et ainsi mémorisés. Cette fonction qui ne possède qu'un argument, :c, est appelée par la fonction LEFT qui fera son travail d'extraction jusqu'au résultat, james.
The only tricky point, because it is new, is in the passage from the line 2: to the line 3:. In the expression {{lambda {:a :b :c} {:c :a :b}} james bond} we note that the function expects three values, :a, :b, :c and that it receives only two. Well, it is satisfied with this and returns a new "anonymous" function {lambda {:c} {:c james bond}} in which the variables :a & :b have been replaced by the words james & bond, and thus stored. This function which has only one argument, :c, is called by the function LEFT which will do its job of extracting the result, james.
Plutôt que d'être effrayé par l'apparente complexité de la séquence des remplacements, dont on n'aura jamais à se soucier, je vous propose de louer la puissance d'une telle syntaxe qui cache un mécanisme "pénible" sous une simple expression, {LEFT {JB}}. Qui n'a d'égale que la puissance elle-même du concept de PAIRe.
Rather than being frightened by the apparent complexity of the sequence of replacements, which one will never have to worry about, I suggest you praise the power of such a syntax which hides a "painful" mechanism under a simple expression, {LEFT {JB}}. Which is matched only by the power itself of the concept of PAIRe.
Deux fonctions supplémentaires, NIL & ISNIL, vont nous être utiles pour répondre à la question : "est-ce une paire ou non ?".
Two additional functions, NIL & ISNIL, will be useful to answer the question: "is it a pair or not?".
{def NIL {lambda {:a} TRUE}} -> NIL {def ISNIL {lambda {:c} {:c {lambda {:a :b} FALSE}}}} -> ISNIL {ISNIL NIL} -> TRUE {ISNIL {JB}} -> FALSE
Acceptez ces définitions sans plus d'explications pour l'instant. Je vous laisse le loisir de détailler le fonctionnement des deux dernières expressions.
Accept these definitions without further explanation for now. I will leave it to you to explain in detail how the last two expressions work.
recursion
Une liste est une paire dont le terme de gauche est un mot et le terme de droite est une paire ou la fonction NIL. Notons que la définition contient en son corps le mot qu'on cherche à définir, paire = liste, il s'agit du premier exemple d'une forme auto-référente, une structure récursive.
A list is a pair whose left term is a word and whose right term is a pair or the NIL function. Note that the definition contains in its body the word we want to define, paire = list, this is the first example of a self-referential form, a recursive structure.
Par exemple
For instance
{def LIST {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}}} -> LIST
Voici comment on accède à chacun des termes de la liste:
Here is how to access each of the terms in the list:
1: {LEFT {LIST}} -> hello 2: {LEFT {RIGHT {LIST}}} -> brave 3: {LEFT {RIGHT {RIGHT {LIST}}}} -> new 4: {LEFT {RIGHT {RIGHT {RIGHT {LIST}}}}} -> world
Par curiosité testons à chaque étape la partie droite de la liste
For curiosity let's test at each step the right part of the list
{ISNIL {LIST}} -> FALSE {ISNIL {RIGHT {LIST}}} -> FALSE {ISNIL {RIGHT {RIGHT {LIST}}}} -> FALSE {ISNIL {RIGHT {RIGHT {RIGHT {LIST}}}}} -> FALSE {ISNIL {RIGHT {RIGHT {RIGHT {RIGHT {LIST}}}}}} -> TRUE
On peut voir apparaître un motif répétitif. Sans plus d'explication voici un algorithme qui automatise tout cela :
We can see a repetitive pattern appear. Without further explanation here is an algorithm that automates all this:
{def DISP {lambda {:list} {{IF {ISNIL :list} {lambda {:list} } {lambda {:list} {LEFT :list} {DISP {RIGHT :list}}}} :list}}} -> DISP {DISP {LIST}} -> hello brave new world
Ça marche et il ne reste plus qu'à comprendre comment ça marche. En donnant des noms, YES & NO, aux deux lambdas internes :
It works and all that's left is to understand how it works. By giving names, YES & NO, to the two internal lambdas:
{def YES {lambda {:list} }} -> YES {def NO {lambda {:list} {LEFT :list} {DISP {RIGHT :list}}}} -> NO
la fonction DISP s'écrit plus simplement
the function DISP is written more simply
{def DISP {lambda {:list} {{IF {ISNIL :list} YES NO} :list}}}
Lançons-nous dans l'analyse de l'expression {DISP {LIST}}
Let's analyse th {DISP {LIST}} expression
0: {DISP {LIST}} - DISP => {lambda {:list} {{IF {ISNIL :list} YES NO} :list}} - {LIST} => {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}} 1: {{lambda {:list} {{IF {ISNIL :list} YES NO} :list}} {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}}} - :list => {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}} 2: {{IF {ISNIL {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}}} YES NO} {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}}} - {ISNIL {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}}} => FALSE 3: {{IF FALSE YES NO} {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}}} - {IF FALSE YES NO} => NO 4: {NO {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}}} - NO => {lambda {:list} {LEFT :list} {DISP {RIGHT :list}}} 5: hello brave new world - :list => {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}} 6: {LEFT {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}}} {DISP {RIGHT {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}}}} - {LEFT {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}}} => hello - {DISP {RIGHT {PAIR hello {PAIR brave {PAIR new {PAIR world NIL}}}}}} => {DISP {PAIR brave {PAIR new {PAIR world NIL}}}} 7: hello {DISP {PAIR brave {PAIR new {PAIR world NIL}}}}
A cet instant le premier terme est affiché et la fonction DISP est appliquée au reste de la liste, brave new world. En recommençant successivement le même processus on obtient
At this moment the first term is displayed and the function DISP is applied to the rest of the list, brave new world. By repeating successively the same process we obtain
1: hello {DISP {PAIR brave {PAIR new {PAIR world NIL}}}} 2: hello brave {DISP {PAIR new {PAIR world NIL}}} 3: hello brave new {DISP {PAIR world NIL}} 4: hello brave new world {DISP NIL}
Finalement l'expression {DISP NIL} s'évalue ainsi
Finally the expression {DISP NIL} is evaluated as follows
0: {DISP NIL} - DISP => {lambda {:list} {{IF {ISNIL :list} YES NO} :list}} 1: {{lambda {:list} {{IF {ISNIL :list} YES NO} :list}} NIL} - :list => NIL 2: {{IF {ISNIL NIL} YES NO} NIL} - {ISNIL NIL} => TRUE 3: {{IF TRUE YES NO} NIL} - {IF TRUE YES NO} => YES 4: {YES NIL} - YES => {lambda {:list} } 5: rien/nothing
Et voilà ! DISP est donc une fonction récursive affichant automatiquement les termes d'une liste LIST, hello brave new world. En voici une autre renversant l'ordre des mots de la liste :
So DISP is a recursive function that automatically displays the terms of a list LIST, hello brave new world. Here is another one that reverses the order of the words in the list:
{def REVERSE {lambda {:list} {{IF {ISNIL :list} {lambda {:list} } {lambda {:list} {REVERSE {RIGHT :list}} {LEFT :list}}} :list}}} -> REVERSE {REVERSE {LIST}} -> world new brave hello
Et une dernière retournant la longueur de la liste.
And a last one returning the length of the list.
{def LENGTH {lambda {:list} {{IF {ISNIL :list} {lambda {:list} } {lambda {:list} •{LENGTH {RIGHT :list}}}} :list}}} -> LENGTH {LENGTH {LIST}} -> ••••
Je suis sûr que vous lisez 4, sous une forme primaire boen sûr, mais qui laisse imaginer comment on pourrait introduire les nombres et l'arithmétique dans un monde qui ne connait que les mots. La page coding en indique quelques pistes.
I'm sure you read 4, in a primary form of course, but that lets you imagine how one could introduce numbers and arithmetic in a world that only knows words. The coding page shows some tracks.
En conclusion provisoire, il faut se rappeler que depuis le début il ne s'agit que de remplacements de texte, un processus systématique, sans exception. En utilsant les deux formes spéciales lambda et def nous avons construit les fonctions booléennes TRUE, FALSE, IF, les fonctions sur les paires PAIR, LEFT, RIGHT, NIL, ISNIL, les listes et quelques fonctions opérant sur les listes. Il en existe bien d'autres mais c'est une autre histoire. Dans ce papier nous allons retourner aux sources, du côté de cette petite formule où tout a commencé : λw.x w.
As a provisional conclusion, it should be remembered that from the beginning it is only about text replacements, a systematic process, without exception. Using the two special forms lambda and def we have built the boolean functions TRUE, FALSE, IF, functions on pairs PAIR, LEFT, RIGHT, NIL, ISNIL, lists and some functions operating on lists. There are many others but that's another story. In this paper we will go back to the sources, to the side of this little formula where it all started: λw.x w.
back to lambdas
Afin de comprendre la puissance contenue dans l'expression initiale {{lambda {:variables} expression} valeurs} nous allons démontrer qu'une expression comme {DISP {LIST}} peut s'écrire sous la forme d'une cascade de lambdas. Pour cela nous devons remplacer les noms par leurs lambda expression équivalentes.
In order to understand the power contained in the initial expression {{lambda {:variables} expression} values} we will demonstrate that an expression like {DISP {LIST}} can be written as a cascade of lambdas. To do this we need to replace the names with their equivalent lambda expressions.
Il y a un obstacle majeur à cela, la fonction DISP est récursive et contient dans son corps son propre nom. Il faut trouver une expression équivalente ne faisant aucune auto-référence au nom. La solution relève de la magie, elle a fait couler beaucoup d'encre mais au fond c'est très simple.
There is one major obstacle to this, the function DISP is recursive and contains in its body its own name. We need to find an equivalent expression that does not self-reference the name. The solution is magic, it has been much talked about but it is actually very simple.
On commence par remplacer la fonction récursive DISP par une nouvelle ADISP, presque récursive, qui contient son nom sous forme de référence locale, et on l'applique à elle même puis à la liste
We start by replacing the recursive function DISP by a new ADISP, almost recursive, which contains its name as a local reference, and we apply it to itself and then to the list
{def ADISP {lambda {:f :l} {{IF {ISNIL :l} {lambda {:f :l} } {lambda {:f :l} {LEFT :l} {:f :f {RIGHT :l}}}} :f :l}}} -> ADISP {ADISP ADISP {LIST}} -> hello brave new world
On améliore cette technique en définissant une fonction annexe, appelée le Ω combinateur, qui applique la fonction à elle-même
We improve this technique by defining an auxiliary function, called the Ω combiner, which applies the function to itself
{def Ω {lambda {:f} {:f :f}}} -> Ω {{Ω ADISP} {LIST}} -> hello brave new world
On fusionne les deux fonctions en une nouvelle fonction ΩDISP
We merge the two functions into a new function ΩDISP
{def ΩDISP {lambda {:l} {{Ω ADISP} :l}}} -> ΩDISP
soit
in other words
{def ΩDISP {lambda {:l} {{{lambda {:f} {:f :f}} {lambda {:f :l} {{IF {ISNIL :l} {lambda {:f :l} } {lambda {:f :l} {LEFT :l} {:f :f {RIGHT :l}}}} :f :l}}} :l}}} -> ΩDISP {ΩDISP {LIST}} -> hello brave new world
On peut maintenant oublier le nom ΩDISP
We can now forget the name ΩDISP
{{lambda {:l} {{{lambda {:f} {:f :f}} {lambda {:f :l} {{IF {ISNIL :l} {lambda {:f :l} } {lambda {:f :l} {LEFT :l} {:f :f {RIGHT :l}}}} :f :l}}} :l}} {LIST}} -> hello brave new world
et enfin remplacer soigneusement tous les noms par leurs lambda expressions
and then carefully replace all the names with their lambda expressions
{{lambda {:l} {{{lambda {:f} {:f :f}} {lambda {:f :l} {{{lambda {:a :b :c} {:a :b :c}} {{lambda {:c} {:c {lambda {:a :b} {lambda {:a :b} :b}}}} :l} {lambda {:f :l} } {lambda {:f :l} {{lambda {:c} {:c {lambda {:a :b} :a}}} :l} {:f :f {{lambda {:c} {:c {lambda {:a :b} :b}}} :l}}}} :f :l}}} :l}} {{lambda {:a :b :c} {:c :a :b}} hello {{lambda {:a :b :c} {:c :a :b}} brave {{lambda {:a :b :c} {:c :a :b}} new {{lambda {:a :b :c} {:c :a :b}} world {lambda {:a} {lambda {:a :b} :a}}}}}}} -> hello brave new world
conclusion
Le λ-calcul tel que nous l'avons exploré dans ce papier nous a permis de construire sur une seule forme, la lambda expression agissant sur des mots, est sans aucune zone d'ombre, les briques essentielles d'un langage de programmation, notamment la divine récursion. Le reste peut être analysé ailleurs dans ce wiki, notamment dans coding et concepts.
The λ-calculus as we explored it in this paper allowed us to build on a single form, the lambda expression acting on words, is without any grey area, the essential building blocks of a programming language, notably the divine recursion. The rest can be analyzed elsewhere in this wiki, notably in coding and concepts.
Reste maintenant à montrer en quoi la récursion nous est "consubstantielle" et en quoi elle nous concerne tous.
It remains now to show how recursion is "consubstantial" to us and how it concerns us all.
En quoi par exemple la cascade de lambdas produisant la phrase "hello brave new world" est-elle révélatrice du fonctionnement de notre cerveau, ou tout au moins de notre pensée ? Dans une autre page, 4bit_adder2, j'ai écrit ceci
For example, how does the cascade of lambdas producing the sentence "hello brave new world" reveal the functioning of our brain, or at least our thinking? In another page, 4bit_adder2, I wrote this
{def 4bitsAdder {lambda {:a4 :a3 :a2 :a1 :b4 :b3 :b2 :b1} {{lambda {:a4 :a3 :a2 :b4 :b3 :b2 :fa1} {{lambda {:a4 :a3 :b4 :b3 :fa1 :fa2} {{lambda {:a4 :b4 :fa1 :fa2 :fa3} {{lambda {:fa1 :fa2 :fa3 :fa4} {car :fa4} {cdr :fa4} {cdr :fa3} {cdr :fa2} {cdr :fa1} } :fa1 :fa2 :fa3 {fullAdder :a4 :b4 {car :fa3}}} } :a4 :b4 :fa1 :fa2 {fullAdder :a3 :b3 {car :fa2}}} } :a4 :a3 :b4 :b3 :fa1 {fullAdder :a2 :b2 {car :fa1}}} } :a4 :a3 :a2 :b4 :b3 :b2 {halfAdder :a1 :b1} }}} -> 4bitsAdder {4bitsAdder false true true true // 0111 3 false false false true} // + 0001 + 1 -> false true false false false // = 1000 = 4
Nous voila devant un algorithme statique, sans boucle, capable de faire la somme de deux nombres binaires, ici 3+1=4. C'Est ainsi que fonctionnent les portes logiques dans une unité de traitement parmi les millions que contient un microprocesseur. Deux nombres se présentent en entrée et par une mystérieuse percolation à travers ces portes logiques se retrouve leur somme en sortie. Une opération qui ne peut s'imaginer que comme une suite d'étapes du genre 3+4 = 2+5 = 1+6 = 0+7 donc le résulat est 7 semble "hard-codée", codée en dur dans le coeur du processeur.
Here we are in front of a static algorithm, without loop, able to make the sum of two binary numbers, here 3+1=4. This is how logic gates work in a processing unit among the millions that a microprocessor contains. Two numbers are presented as input and by a mysterious percolation through these logic gates, their sum is found as output. An operation that can only be imagined as a sequence of steps like 3+4 = 2+5 = 1+6 = 0+7, so the result is 7, seems to be "hard-coded", hard-coded in the heart of the processor.
Dans une autre page, concepts, j'en suis arrivé à cette autre cascade de lambdas :
In another page, concepts, I came to this other cascade of lambdas:
{{{lambda {:g} {:g :g}} {lambda {:g :n :a :b :c} {{{lambda {:a :b :c} {:a :b :c}} {{lambda {:c} {:c {lambda {:a :b} {lambda {:a :b} :b}}}} :n} {lambda {:g :n :a :b :c} } {lambda {:g :n :a :b :c} {:g :g {{lambda {:c} {:c {lambda {:a :b} :b}}} :n} :a :b :c} {div} move {{lambda {:c} {:c {lambda {:a :b} :a}}} :n} from tower :a to tower :b {:g :g {{lambda {:c} {:c {lambda {:a :b} :b}}} :n} :c :b :a} }} :g :n :a :b :c}}} {{lambda {:a :b :c} {:c :a :b}} ■■■■.■■■■ {{lambda {:a :b :c} {:c :a :b}} ■■■.■■■ {{lambda {:a :b :c} {:c :a :b}} ■■.■■ {{lambda {:a :b :c} {:c :a :b}} ■.■ {lambda {:a} {lambda {:a :b} :a}}}}}} A B C} -> move ■.■ from tower A to tower B move ■■.■■ from tower A to tower B move ■.■ from tower C to tower B move ■■■.■■■ from tower A to tower B move ■.■ from tower C to tower B move ■■.■■ from tower C to tower B move ■.■ from tower A to tower B move ■■■■.■■■■ from tower A to tower B move ■.■ from tower C to tower B move ■■.■■ from tower C to tower B move ■.■ from tower A to tower B move ■■■.■■■ from tower C to tower B move ■.■ from tower A to tower B move ■■.■■ from tower A to tower B move ■.■ from tower C to tower B
Il s'agit de la suite des mouvements de disques dans le jeu des Tours de Hanoï. L'évaluateur a remplacé la cascade figée par une noria de disques. L'évaluateur a parcouru le labyrinthe des lambdas à la vitesse de l'éclair et 4 disques empilés sont passés d'une tour à l'autre.
This is the sequence of disc movements in the Towers of Hanoi game. The evaluator replaced the frozen waterfall with a noria of discs. The evaluator went through the maze of lambdas at lightning speed and 4 stacked discs went from one tower to another.
Prenez bien conscience qu'il y a une totale équivalence entre la cascade de lambdas, le code, et la séquence de mouvements, le résultat, "code is data". Ce sont deux aspects de la même chose, les deux faces de la même pièce. Mais il y quand même une différence, on peut passer des lambdas aux mouvements mais pas l'inverse. Une histoire d'entropie croissante. Même énergie mais qualité différente. On a perdu l'algorithme pour ne garder que le résultat. Je pense que notre cerveau conserve les algorithmes et que nos prises de conscience en sont des évaluations fulgurantes. Enseigner, par exemple, ce n'est pas partager les résultats, c'est partager les algorithmes. Convaincre ce n'est pas asséner des résultats, c'est échanger des algorithmes. Les images que nous mémorisons ne peuvent être vues dans un scanner, le scanner ne voit que des aiguillages. Observer un microprocesseur au microscope ne donne aucune information sur les algorithmes qui l'habitent, percolent à travers les portes logiques.
Be aware that there is a total equivalence between the cascade of lambdas, the code, and the sequence of movements, the result, "code is data". They are two aspects of the same thing, two sides of the same coin. But there is a difference, we can go from lambdas to movements but not the other way around. A story of increasing entropy. Same energy but different quality. We lost the algorithm to keep only the result. I think that our brain keeps the algorithms and that our awarenesses are lightning evaluations of them. Teaching, for example, is not sharing results, it is sharing algorithms. To convince is not to assert results, it is to exchange algorithms. The images we store cannot be seen in a scanner, the scanner only sees switches. Observing a microprocessor under a microscope gives no information about the algorithms that inhabit it, that percolate through the logic gates.
Pour moi tout ceci est une fenêtre ouverte vers de nouveaux mondes. Je pense au crible d'Érathostène qui produit la série des nombres premiers. Je pense aux ravinements sur les flancs d'une montagne qui vont guider les eaux de pluie, je pense aux gouttes d'eau sur une vitre qui suivent des chemins toujours changeants. Je pense aux influx nerveux qui se propagent dans le cerveau, de neurone en neurone, en fonction des la résistance électique des synapses. Des arbres lumineux qui s'entrecroisent dans le cortex, l'espace d'un instant.
For me all this is a window open to new worlds. I think of the sieve of Erathostene which produces the series of prime numbers. I think of the gullies on the sides of a mountain that guide the rainwater, I think of the drops of water on a window that follow ever-changing paths. I think of the nerve impulses that propagate in the brain, from neuron to neuron, according to the electic resistance of the synapses. Luminous trees that intersect in the cortex, for a moment.
La récursion est au coeur de la plupart des algorithmes, et nous avons vu que cette récursion peut être représentée par une cascade figée de lambdas. Notre pensée est algorithmique. Notre pensée est récursive, arborescente, une forêt d'éclairs qui s'entrecroisent et fleurissent en canopée. Notre pensée est une sculpture géométrique, fractale. La sculpture EST la pensée, hors du temps.
Recursion is at the heart of most algorithms, and we have seen that this recursion can be represented by a fixed cascade of lambdas. Our thinking is algorithmic. Our thought is recursive, tree-like, a forest of lightning bolts that intertwine and bloom in a canopy. Our thought is a geometrical sculpture, fractal. The sculpture IS the thought, out of time.
Notre cerveau est le siège d'une myriade de réécritures permanentes qui se passent hors de notre conscience. Nous arrivons parfois, péniblement, à reconstituer des bribes de phrases, des associations d'idées, nous en prenons conscience, nous élaborons des séquences de mots que nous exprimons au dehors, on parle, on écrit, on dessine, on échange.
Our brain is the seat of a myriad of permanent rewritings that take place outside our consciousness. We sometimes manage, painfully, to reconstitute snatches of sentences, associations of ideas, we become aware of them, we elaborate sequences of words that we express outside, we speak, we write, we draw, we exchange.
Et mon ordinateur est là qui m'attend, comme un chien fidèle, qui attend que j'écrive quelques cascades de lambdas qu'il évaluera instantanément, sans relache, sans état d'âme. Le curseur clignote ...|... et attend de lancer le fidèle robot, λw.x w, à l'assaut d'un océan de mots.
And my computer is there waiting for me, like a faithful dog, waiting for me to write a few stunts of lambdas that it will evaluate instantly, without relenting, without a qualm. The cursor blinks ...|... and waits to launch the faithful robot, λw.x w, to the assault of an ocean of words.
alain marty 2022/01/09 - 2023/03/11
