Études-Mathématique/La traduction

From Lazi wiki
Jump to: navigation, search

Question

Qu'est-ce que la traduction et comment fonctionne-t-elle ?

Étude

Qu'est-ce que la traduction ?

La règle d'extension implique de fournir une fonction de traduction des instances du M étendu vers les instances de M.

Cette nécessité engendre la nécessité d'autres fonctions de traductions pour des sous-parties, comme par exemple la traduction de notations dans les formules.

Comment fonctionne la traduction ?

Répartition de la traduction

Les éléments à traduire :

  • les formules (quand l'extension ajoute un type composant de formule)
  • les déductions

Où sont ces éléments:

  • La déduction à traduire.
  • Des déductions ou formules à l'intérieur :
    • d'une déduction
    • d'un événement

Étapes dans la traduction d'une extension

Une extension pourra demander plusieurs étapes pour être traduite.

Prenons l'exemple de la notation des fonctions ($F x -> body). On devra traduire les règles de déductions de l'extension et aussi les formules. Il peut être utile d'avoir les formules pas encore traduite pour traduire les règles. On peut donc décomposer la traduction en au moins deux étapes:

  • traduction des règles,
  • traduction des formules.

Association entre les fonctions de traduction et les éléments à traduire

La traduction d'une extension comprendra en général différente fonctions de traduction: la traduction d'une certaine règle ou d'un certain type composant de formule aura en général sa propre fonction.

On peut alors définir ces fonctions dans les types traduits ou en dehors. Il me parait logique de les définir dans les types.

Parcours commun aux fonctions de traduction

En général la traduction consiste à chercher un certain type global (les déductions, les formules, les événements) et à faire des changements sur certaines instances correspondant à un type constituant. On peut donc utiliser des fonctions communes: parcourir des types, appliquer des fonctions sur les objets à traduire.

Traduction des déductions

La fonction "translate name" où "name" est le nom du type de déduction à traduire est une fonction virtuelle de deductionT. Par défaut :

  • Si le type de déduction est name, elle appelle translateThis de l'objet constituant (cette fonction est définies pour toutes les règles provenant d'extensions).
  • Si le type est différent, elle appelle mapDeductions ($F t → t .o'translate name), ce qui permet de traduire les sous-déductions éventuelles.

La fonction virtuelle de deductionT mapDeductions map les sous-déductions directes, par défaut (pour les déductions n'ayant pas de sous-déductions) elle retourne l'instance inchangée.

Les fonctions de mapage reçoivent en premier argument le type de l'objet mapé, car certains objets ne sont pas dans le type de base (M .o'deductionT par exemple) mais dans un contexte mathématique différent (par exemple sous un événement ou encore les sous-déductions dans la règle d'induction.

Traduction des événements

Exemple des événements de définition

L'extension "définition" permet d'utiliser des événements associant une valeur (une formule) à une variable. L'événement ajoute cette association à la mathématique et une règle permet de déduire cette égalité.

Traduire l'événement nécessite de remplacer la e-déduction par une déduction sans l'événement. Il faudra remplacer la sous-déduction par une déduction ne contenant par la variable ni l'application de la règle déduisant l'égalité variable/valeur.

Cas général

L'information nécessaire pour traduire un événement est une fonction de transformation de déduction. Remarquons qu'un événement ev1 peut se traduire en un événement ev2. Cela est possible avec la fonction de transformation de déduction, car elle peut retourner une e-déduction avec ev2 en événement.

Les stories

Comment définir eventT .o'translateEvents (la traduction des sous-événements d'un événement suivant un critère p) alors que translateEvents est sensé retourner un événement ?

Réponse

Voir l'étude.