Les événements

From Lazi wiki
Jump to: navigation, search

Présentation

En mathématique, une définition consiste à attribuer une valeur à un nom qui était jusque-là inutilisé. Une définition ajoute une vérité au contexte mathématique, qui est donc changé. On peut quand même voir une définition comme une déduction: pour cela la déduction de définition doit prendre en argument la valeur, la variable à définir, et une sous déduction qui se fera dans le contexte de cette définition.

On peut décomposer la déduction de définition en deux parties:

  • les informations sur le changement de contexte mathématique,
  • la sous déduction dans le contexte modifié.

Nous appellerons “edéduction” les déductions de cette forme, la partie changeant le contexte ce sera nommé événement.

eventT

eventT est le type des événements, ce sera un type union. L'objet d'un événement est le contexte mathématique résultant de l'événement. Un type événement possède une fonction "translateThis" qui retourne, à partir d'un événement, la fonction traduisant la sous déduction en une déduction équivalente n'utilisant pas l'événement. Par exemple, pour le type “événement de définition”, translateThis retournera la fonction qui remplace dans la déduction la variable définie par sa valeur (avec d'autres modifications que l'on ne précisera pas ici).

Contrairement aux autres traductions (des formules et des déductions), on peut avoir à utiliser une fonction translateThis dans un contexte mathématique où des événements de type définis postérieurement existent. Cela est dû au fait que l'on obtient l'objet d'une e-déduction en traduisant la sous-déduction en une déduction du contexte courant (la sous-déduction est dans le contexte objet de l'événement et c'est la fonction retournée par translateThis qui permet de la traduire).

eDeductionT

eDeductionT est le type des e-déductions, ce sera un nouveau type de déduction qui nécessitera une extension pour être ajoutée à Lazi. Une instance sera constituée d'un événement et d'une sous déduction dans le contexte modifié par l'événement. Son objet sera celui de la déduction après traduction par translate.

storyT

storyT est un type d'événement. Son instance est une liste d'événements (on peut imaginer par exemple des définitions). Une déduction $T[ 'eDeduction, $T['story, $L[ev1,ev2...evn]], d] sera équivalente à $T[ 'eDeduction, ev1, $T[ 'eDeduction, ev2, ... , d ]]]...].

Donc les fonctions "translate" et "object" de storyT seront les compositions de celles des événements.

Traduction des e-déduction pour certains événements

Le système d'extension de Lazi repose sur la traductibilité. Pour ajouter un nouveau type d'événement, il faudra créer une extension. Il faudra donc pouvoir traduire tous les événements d'un certain type.