Outils pour utilisateurs

Outils du site


pages:norae:si:dev_note-form_3

λ-calcul binaire

Intro

John Tromp a mis au point le λ-calcul binaire comme programmation suffisamment puissante pour écrire un programme avec le moins de bits possible pouvant s’approcher au plus près de la complexité de Kolmogorov.

« Compléxité de Kolmogorov : un nombre comme étant la longueur du plus petit programme nécessaire pour calculer ce nombre. Un nombre complètement aléatoire ne peut être décrit par aucun programme plus court que le nombre lui-même, et possède donc une complexité de Kolmogorov maximale (on rejoint ici le concept d’entropie, qui est maximale quand les données sont aléatoires). Exemple : “la la la la la la la la la la la la la la la la la la la la” contient assez peu d’information, résumée dans l’algorithme “écrire 20 fois le mot ‘la’” »

Le langage de John Tromp est issu du λ-calcul, pour lequel tout programme est une expression, qui ne peut être que l’une des 3 formes suivantes :

  • Une variable, de la forme x, y, z ou n’importe quelle autre lettre
  • Une abstraction, de la forme (λx.a), où x est une variable et a est une autre expression
  • Une application, de la forme (a b), où a et b sont deux autres expressions

Syntaxe λ-calcul

Définiton λ-calcul binaire

Plus précisément, λ-calcul binaire définit une machine universelle qui, à partir d'un flux de bits d'entrée, analyse l'encodage binaire d'un terme de calcul lambda, applique cela au reste de l'entrée (traduit en une liste « ennuyeuses de booléens, qui ont une représentation standard en calcul lambda), et traduit le résultat évalué en une serie de bits en sortie.

Spécificité λ-calcul binaire

Biblio

pages/norae/si/dev_note-form_3.txt · Dernière modification : 2021/08/06 11:05 de xavcc