Lazi

Les innovations apportées par lazi

Ce document présente globalement Lazi. Pour une approche plus en douceur abordant des points particuliers voir http://lazi.bobu.eu.

Les domaines scientifiques de Lazi sont les fondations mathématiques et l'informatique théorique.

Si on avait en physique plusieurs théories pour décrire les champs électromagnétiques, toutes à peu près équivalentes mais pas tout à fait, alors les physiciens chercheraient avec ferveur laquelle est la bonne.
Si on avait en mathématique plusieurs manières de faire de l'algèbre (par exemple avec des notions de structures différentes), et que chaque manières se ressemblent mais pas entièrement, on chercherait aussi à unifier l'algèbre.
L'idée derrière Lazi est que cette démarche fructueuse d'unification d'un champs scientifique devrait aussi s'appliquer aux fondations mathématiques et aux langages informatiques. À mon humble avis, les réalisations déjà obtenues sur Lazi en son la preuve.

Il existe à l'heure actuelle de nombreuses manières de définir des fondations mathématiques, et en informatique il existe de nombreux langages. Une démarche usuelle en science est d'augmenter son ambition pour arriver à ses fins, par exemple il peut être plus facile de prouver un théorème plus large ou encore d'obtenir une solution unique en augmentant les contraintes. On peut voir Lazi comme un ensemble de contraintes supplémentaires ajoutées aux fondations mathématiques et aux langages informatiques, avec pour résultat une base commune, à la fois pour les mathématique et l'informatique, ayant des propriétés forts intéressantes.

Les contraintes ajoutées

L'auto-représentation totale et évolutive

  • auto-représentation : Que ce soit en tant que langage informatique ou fondation mathématique, il est incorporé naturellement dans Lazi (c'est en fait une étape nécessaire à sa définition) une représentation de Lazi.
  • totale : Il ne s'agit pas de ne représenter que les informations, mais aussi la logique, de sorte que l'on puisse raisonner sur cette représentation.
  • évolutive : Les raisonnements sur les représentations sont utilisées pour prouver la validité d'extensions qui sont alors utilisables pour étendre les mathématiques et le langage informatique.

Des bénéfices obtenus

Le micro-noyau

  • Un nano-noyau fournissant la base pour définir tout le reste (fondation, langage informatique) formellement. C'est à dire que tout ce qui est en dehors du nano-noyau peut être directement lu et interprété par un logiciel. Le nano-noyau comprend un langage similaire au lambda calcul non typé mais sans variable ni λ et avec un mot nouveau (distribute), plus quelques règles de déductions qui sont en même temps des règles de calcul.
  • Un micro-noyau : il comprend la définition de la fondation mathématique ( et donc y compris ses capacités d'extensions ). "micro" car des concepts comme les quantificateurs ne sont pas intégrés car il peuvent être définits par extension. Il comprend des règles de déduction classiques comme l'induction, une forme faible de tiers exclu.

Mathématiser et informatiser les mathématiques et l'informatique

Pour les mathématiques :

Comme ZFC n'a pas de mécanismes d'extension (par exemple une preuve en analyse non standard ne peut être utilisée par un logiciel de vérification de preuve de ZFC pour prouver une vérité ZFC), il n'existe pas de manière naturelle de créer un logiciel de vérification de preuve. C'est à dire que le logiciel de vérification de preuve doit intégrer des mécanismes hors mathématiques pour gérer les notations et les éventuelles extensions. En Lazi, du fait qu'il a une représentation de lui-même et une règle d'extension, peut importe la mathématique que l'on veut utiliser, il est possible d'intégrer la vérité prouvée (comme une vérité Lazi) à partir d'un texte purement mathématique. Par exemple si vous avez un logiciel de vérification de preuve Lazi, vous pouvez fournir une preuve ZFC et les preuves

Unification des mathématiques et de l'informatique

Il devient en pratique difficile de discerner ce qui est de l'ordre de l'informatique ou des mathématiques, par exemple :

  • Un langage commun pour les mathématiques et l'informatique Lazi.
  • Un même concept unifie les structures algébriques mathématiques et les types informatiques
  • Toute preuve utilisant une extension prouvant un énnoncé hors le langage de l'extension peut être traduite en une preuve sans l'extension. Il en résulte une capacité de traduction toujours possible quand cela a un sens vers le concret informatique, par exemple l'extension "il existe" est constructive.

Un langages informatique universel

Avec le concept de langage informatique actuel l'idée d'un langage universel est absurde car les langages sont des compromis entre la concision, le niveau d'abstraction, l'adaptation à la catégorie de programme à produire (par exemple on ne veut pas remplacer Bash par Haskell).
Pour dépasser ces compromis il faut ajouter un niveau d'abstraction. Ce niveau d'abstraction est déjà existant sous forme ambrionaire :

  • dans des compilateurs multi-langages comme gcc
  • dans des langages de haut niveau comme Haskell, où les monades peuvent être vu comme des abstractions de code, ce qui permet par exemple de définir en Haskell la notion d'exception.

Ce niveau d'abstraction supplémentaire consiste à représenter les langages informatique eux mêmes dans un langage inform-mathématique (comme Lazi).
Les avantages sont par exemple :

  • La traductabilité inter-langages
  • La possibilité de prouver la validité des programmes
  • La possibilité d'utiliser des extentions ajoutant des concepts de haut niveau (comme la preuve de contraintes) à tout langage
  • L'intégration d'éléments quelconque (comme un bout de code source ou encore une manière plus performante de compiler) peuvent être accompagnées de leur preuve de validité. Il devient donc possible d'accepter directement des ajouts/amélioration de toute source sans crainte de dégradation. Les bugs sont alors relégués à la spécification des contraintes. C'est à dire qu'un petit paysan inconnu d'Inde peut publier du code source améliorant la vitesse d'éxécution d'un logiciel et cette amélioration peut être effective 5 minutes après sur toute la planète car la preuve de l'intérêt de cette amélioration et sa diffusion ne passe plus par des testes, vérification manuelles et signature cryptographiques mais par une preuve.

@todo