Études-Mathématique/Comment gérer les déductions modifiant M ?

From Lazi wiki
Jump to: navigation, search

Question

Certaines règles de déduction (comme l'ajout "addSimpleRule") modifie le contexte M. Pour qu'une telle déduction ait un intérêt il faut utiliser une sous-déduction qui utilise M. Appelons les règles à effet de bord de telles règles.

Est-il possible de trouver une manière qui évite à ces règles de gérer elle-même la sous-déduction ?

Étude

Comparaison avec les sources Lazi

On peut comparer les règles à effet de bord aux sources Lazi : on a divers commandes (comme $Def, ou les notations) qui changent le contexte, puis on a une évaluation.

Gérer la traduction

Si on veut séparer la partie effet de bord de la sous-règle, il faut néanmoins prévoir la traduction de la sous-déduction, qui est dépendante de la règle.

Les types "extensions"

Un type extension ne serait pas une règle de déduciton, il modifie M suivant l'instance. On peut s'en servir pour en dériver un type "règle" en lui enjoignant une déduction sous le M modifié. La règle dérivée a pour instance une paire $T[instance de l'extension, instance d'une déduction sous le M modifié].

On pourrait, à la manière des déductions, lister dans M les types extensions.

On ajoute une règle de déduction à M, qui a pour instance une paire $T[instance d'extension, intance d'une déduction sous l'extension] et qui déduit une vérité.

Comme pour proofT, on peut combiner une liste d'extensions pour en former une seule.

Vocabulaire de types "extensions"

  • Extension : une extension est une fonction de transformation de M
  • Extension traduisible : c'est une extension pour laquelle on possède une fonction de traduction des déductions dans l'extension. Ces traduction son sensées être valide pour les déductions ayant une ctruth dont les formules sont dans le domaine du formulaT du M originel.
  • Extension prouvée : c'est une extension pour laquelle on possède une preuve que toute ctruth prouvée dans le M étendu est prouvable dans le M originel.
  • M .o'eventT : le type des événements valides pour M
  • L'objet d'un événement est une extension.
  • Une règle d'événement de M est un type tel que toutes ses instances sont des instances de M .o'eventT.
  • Une histoire : c'est une liste d'événements. Remarquons que par composition des extensions une liste d'événements correspond à un événement dont l'objet est la compositions des extensions.

Réponse

Oui. Voir Les types "extensions" ci-dessus.