Lazi

Extensibilité de Lazi

Définition

Informellement, la mathématique M2 est une extension de M1 si et seulement si :

Pour toute preuve en M2, si la conclusion (la vérité déduite par la preuve) est traduisible en M1 alors il existe une preuve en M1 de cette vérité traduite.

Remarque : cela implique l'existence d'une fonction (souvent partielle) de traduction des formules de M2 en formules de M1.

Utilité

Le langage mathématique est de plus en plus utilisé dans un cadre informatique, par exemple dans les langages informatiques de haut niveau ou encore pour vérifier les preuves mathématiques. Cela implique une définition complètement formalisée de la mathématique, y compris par exemple des notations. Une définition monolithique d'une mathématique n'est pas pratique pour une formalisation totale des mathématiques, car cela implique de tout prévoir dès le départ et d'y incorporer toutes les syntaxes exotiques utilisées. Par exemple, comment intégrer l'analyse non standard ? On peut toujours intégrer des nouveautés à un système monolithique, mais avec les extensions l'intégration devient facile et fiable.

Facilité

Le principe des extensions en Lazi est au cœur de cette mathématique. Dès le départ la mathématique calculatoire permettant de définir le reste de Lazi est elle-même une sous-partie de Lazi. Le langage de base de Lazi est naturellement calculable et donc une définition correspond à un programme exécutable (un interpréteur est déjà réalisé).

Par exemple ne Lazi la notion de définition est intégrée par une extension.

Le fait que Lazi soit une mathématique constructive permet de grandement facilité les preuves de validité des extensions : s'il est prouvé qu'une entité existe alors on peut l'expliciter, ce qui permet de produire effectivement les fonctions de traduction des preuves.

Fiabilité

À terme (ce n'est pas encore formellement fait pour les extensions actuelles) la définition d'une extension s'accompagnera de la preuve de sa validité. Il sera donc impossible d'introduire des erreurs par l'utilisation d'une extension. Cette capacité permet donc d'utiliser sans risque des extensions provenant de tiers.

Les extensions en Lazi

Règle spéciale

Motivation

Imaginons que nous ayons un programme P n'ayant qu'une fonction : vérifier les preuves d'une mathématique M1. Comment alors utiliser une extension M2 à M1 ? Nous pouvons définir M2 en M1 et calculer dans M1 la validité des preuves M2, mais comment ajouter à M1 une vérité provenant de M2 (pour les vérité traduisibles) ? On peut dans M1 définir une fonction de traduction des preuves M2 en preuves M1. Donc on peut se ramener à avoir une représentation en M1 d'une preuve M1 que l'on voudrait utiliser pour ajouter une vérité.

Modifier P ? Non, voici pourquoi :

On pourrait modifier P pour inclure une nouvelle manière d'ajouter des vérités : par les représentations en M1 de preuves M1. Le problème de cette solution est que l'on externalise des mathématiques dans le programme plutôt que de régler mathématiquement le problème. Ce principe de non externalisation des problèmes est important car il permet de préserver la propriété de réentrance de Lazi : Lazi a une représentation complète de son fonctionnement (y compris les notations etc) de sorte qu'il est simple de raisonner dessus (cela offre en fait beaucoup d'avantages).

Une autre solution (retenue) est d'ajouter une règle signifiant "si x est une représentation d'une preuve (or cette règle de déduction) alors la traduction de l'objet de cette preuve est vrai". Remarque : l'objet d'une preuve est la vérité déduite par celle-ci.
Comme Lazi est constructif la traductibilité des déductions de cette règle est simple à prouver : on traduit par l'interprétation de la représentation de la preuve.

Ce qu'est une mathématique Lazi

En Lazi les preuves et les déductions sont unifiés. Une mathématique est un type, le type des déductions de la mathématique. C'est à dire qu'en Lazi la notion de déduction et de mathématique est unifié. Le type comporte un champs "formulaT" qui est le type des formules de la mathématique.

En pratique, définir une extension Lazi

Il faut donc définir le type des déductions, pour cela on définit le type des formules, le type de chaque
déduction, un type permet de rassembler les types des déductions en une seule.
Il faut aussi fournir la preuve (actuellement ce n'est pas fait car il faut déjà que tous les outils soit définis) de la validité de l'extension. En pratique cela consiste à définir la fonction de traduction et la preuve de sa validité.

Les extensions existantes

On peut accéder à leurs définitions, voir "Organisation:Organisation des documents".
Comme Lazi est une sorte de micro noyau beaucoup d'extensions sont nécessaires , par exemple :

  • Pour définir les fonctions (l'équivalent de λ du lambda calcul).
  • Pour définir la notion d'évènement qui permettra d'ajouter, par exemple et par une autre extension, la notion de définition.