Lazi

Calculer dans une extension mathématique

Contexte

Pour voir si toute mathématique peut être définie en lazi.1.0, il faut voir comment traduire en lazi.1.0 une mathématique définie à l'intérieur d'une autre. Comme on définie les mathématiques en utilisant des propriétés, il est nécessaire que l'on puisse en lazi.1.0 calculer des propriétés définies dans des extensions. Voir "Extension mathématique définie en interne".

Question

Soit une mathématique M définie en lazi.1.0. Dans le contexte lazi.1.0/M soit f une fonction définissant une propriété. Comment calculer f en lazi.1.0.

Étude

En lazi.1.0, f est de type "formule" de M. Par exemple M peut étendre les formules lazi.1.0 par des mots définis, donc pour calculer f il faut remplacer ces mots par leurs valeurs.

On voit donc qu'il est nécessaire, pour réaliser les calculs, que la définition d'une mathématique contienne la définition de quelque chose permetant les calculs. Car dans le cas contraire on ne pourrait pas raisonner sur les définitions produites dans cette mathématique.

Déduction de calcul

Si on a une règle de calcul d de M, elle prend en argument une formule x de M et déduit, si la formule est dans le domaine, une vérité de la forme x = y. Il suffit donc de calculer (en lazi.1.0) l'objet de la déduction pour avoir la formule y.

Coût des calculs

On pourrait imaginer que la définition d'une mathématique implique, en plus de la déduction de calcul, d'une fonction de calcul, de sorte que le calcul soit plus rapide. Mais une déduction de calcul peut être casiment (ou même également) rapide.

Réponse

Il faut inclure la définition d'une règle de calcul dans les extensions mathématiques (c'est une forme particulière de règle de déduction). Elles servent à la fois à :

  • définir ce qu'est un calcul élémentaire
  • fournir une méthode de calcul effective
  • calculer une formule par répétition de la règle de calcul élémentaire

Une règle de calcul doit par récurrence aboutir à x = 1b , respectivement 0b, si x = 1b, respectivement 0b.