Études-Mathématique/Mathématiques extensibles

From Lazi wiki
Jump to: navigation, search

Question

Qu'est-ce qu'une mathématique extensible et comment l'implémenter ?

Étude

Définition de mathématique extensible

Extensibilité par preuve

Une mathématique extensible par preuve permet de prouver qu'une extension est valide et de l'intégrer dans la mathématique.

Dans le cadre de Lazi, on peut voir une mathématique extensible comme un type d'événement qui a pour instance une extension et sa preuve et qui modifie M en ajoutant l'extension.


Extensibilité par traduction

Une mathématique extensible par traduction permet d'intégrer une extension, mais on passe par la fonction de traduction pour tout faire (domaine etc).

Implémentation des extensions par preuve

Si une mathématique a une représentation d'elle-même, elle peut:

  • Vérifier des preuves sur elle-même, par exemple une preuve qu'une extension est valide.
  • Mettre à jour la représentation d'elle même par l'extension.

Il me semble donc possible de définir une extension des extensions par preuve.

Pour cela, une mathématique M doit avoir une entrée "me" qui est la formule telle que son interprétation soit égale à M.

Pour accepter d'utiliser une mathématique M2, il faut une représentation rM2 de M2 et fournir une preuve au sujet de la valeur de "me" et rM2. On peut alors utiliser des déductions utilisant des déductions de M2.

Est-ce que l'on peut définir "me = lazi1M" ? Ça pose un problème de récursivité.

Problème du M contenant sa propre représentation

Essai 1 (bof)

On peut le résoudre par une formule infinie. Mais ça ne me semble pas pratique à manipuler.

Essai 2 (problématique)

On peut le résoudre par un mot spécial où la variable globale "me" représente M. Dans M on aurait "me = $Fo[me]" et les preuves d'extensions utiliserait la déduction supplémentaire "me = Lazi1".

Pour produire des preuves sur la représentation de M, ces preuves devraient avoir une déduction "me = ...".

Mais il me semble que cela ne fait que déplacer le problème car on a toujours une formule de Lazi1 dans Lazi1.

Essai 3 (problématique)

On définit preLazi1 sans l'entrée "me" (voir essai 2), puis on définit Lazi1 comme preLazi1 où l'on ajoute l'entrée " me = $F[ preLazi1 ∪o $O[me = $F[me]]

Essai 4 (Problème de récurrence)

On définit Lazi1F comme une fonction prenant en argument "me", la représentation de lui-même. Puis on définit Lazi1 =Lazi1F $F[LaziF].

On définit une déduction par extension par: Instance:

  • La représentation du la mathématique étendue (c'est donc une formule représentant une fonction, comme Lazi1F).
  • La preuve que les objets de la mathématique étendue qui sont de type objet pour la mathématique de base, sont des objets de la mathématique de base.
  • Une instance ie de la mathématique étendue tel que l'objet est de type objet pour la mathématique de base.

Objet: L'objet correspondant à ie par la mathématique étendue.

Essai 5 (presque bien)

Une extension n'a pas besoin de connaître la règle d'extension puisque celle-ci ne permet pas de déduire de vérité conditionnelle supplémentaire. On peut déjà définir Lazi sans la partie extension (Lazi1-NE, pour non extension).

On définit le type d'événement extensionT qui permet d'ajouter des extensions. Les extensions sont des événements et s'intègrent donc dans la structure déjà mise en place.

extensionT a pour instance:

  • La formule Lazi1NE dont l'objet (c'est mieux que les objets des formules soient leur interprétation, voir plus bas) est le M.
  • La formule Lazi1NE dont lobjet est tr: la fonction de traduction des déductions.
  • Une instance de deductionT qui a pour objet:
    • Conditions:
      • £M .o'deductionT i
      • ctruthT Lazi1NE .o'domain \ £M .o'deductionT .o'object i
    • Conclusion: Lazi1NE .o'deductionT (£tr i) ∧b ctruthT Lazi1NE .o'equal( Lazi1NE .o'deductionT .o'object (£tr i) , £M .o'deductionT .o'object i )

où £M et £tr sont remplacés dans les formules par les formules M et tr de l'instance.

Son objet est l'objet de la formule M.

Essai 6 (presque bien)

Le problème de l'essai 5 est que l'on a besoin de la règle eDeductionT, alors qu'elle n'est pas nécessaire dans les bases. On peut faire la même chose mais sans les événements.

Essai 7 (bien)

On peut simplifier l'essai 6: extensionT est une déduction ayant pour instance:

  • dom : une formule, qui représente le domaine des instances
  • tr : une formule, qui représente la fonction de traduction des instances
  • p : une preuve
  • i : une chose telle que formulaT .o'object dom i

Pour que l'instance soit valide il faut que p ait pour objet (dans M où la variable globale "i" est ajoutée):

$T[ $L[ dom +f $F[j] ] , $F[ Lazi1NE .o'deductionT .o'domain ] +f (tr +f $F[j]) ]

L'objet de la déduction est deductionT .o'object (formulaT .o'object tr i)

Cette définition est simple mais suffisante: Par exemple si on veut une extension MQ implémentant les quantificateurs: dom sera le domaine du deductionT de MQ tel que les objets sont des objets pour Lazi1NE, et tr sera la traduction des déductions en déductions de Lazi1NE.

Objet des représentations de formule

Jusqu'à présent il n'y avait pas réellement d'objet puisque l'instance était retournée. Maintenant il y a besoin d'interpréter les formules et ça me parait logique que ce soit l'objet des formules.

La fonction "objet" n'a pas d'autre argument que l'instance.

Mais quel objet donner aux variables globales ? Les variables sont des formules virtuelles, c'est à dire sans objet, on doit donc les remplacer d'abord si on veut obtenir l'objet d'une formule.

Traduction

Nous avons vu qu'une extension doit fournir une fonction de traduction des instances de déduction.

Suivant les extensions on peut avoir toute une variété de traduction. Mais il arrive souvent que la traduction d'une extension vérifie des propriétés simples tel que:

  • devoir modifier toutes les formules des déductions,
  • il suffit de convertir les déductions introduites par l'extension.

Fonctions pratiques de deductionT pour la traductions:

  • mapFormulas : change les formules
  • mapDeductions name: change les sous-deductions d'une déduction, name est le nom de la déduction à mapper. La déduction enfant peut ne pas l'implémenter (s'il n'y a rien à faire), le comportement par défaut étant de ne rien faire.
  • translateThis : pour les déductions d'extension, la fonction de traduction de l'instance.
  • translate name : traduit les déductions "name", que ce soit la déduction composante ou les sous-déductions. En général pas surchargée par la déduction composante, mais peut l'être, par exemple la déduction des événements "eDeduction" la surchage pour transférer l'appel à l'événement.

Réponse

Voir l'essai 7.