Études-Mathématique/Extension pour les fonctions

From Lazi wiki
Jump to: navigation, search

Question

Préambule

Pour faire des preuves sur les formules, notamment celles définissant Lazi, il faut qu'elles ne soit pas trop grosses et ressemblantes à celles utilisées pour définir Lazi. Pour cela les notations nécessaires sont les mêmes que celles utilisées dans compute:

  • les fonctions
  • les définitions par globale variable
  • les représentations des mots

La question

Comment définir une extension pour ajouter la notation des fonctions ?

Étude

Il faut pouvoir ajouter des types composants pour les formules. Le mieux pour cela est que le dictionnaire des composants soit dans M.

Le composant de formule

Pour représenter une fonction il faut :

  • le nom de la variable
  • la formule corps de fonction

Les variables utilisées sont des variables locales, il faut donc créer un nouveau type de mot. Il faut que le dictionnaire des types de mots composants soient dans M.

Il n'y a pas de calcul à l'intérieur des fonctions, et donc les variables locales ne sont pas à ajouter à M pour faire des déductions, comme on le fait pour les variables globales.

La déduction de calcul

Il faut une déduction pour appliquer un argument à la fonction. Instance: une formule, de la forme "f a" où f est une fonction. Aucune condition. Déduit: le corps de la fonction où la variable est remplacée par la valeur. On peut utiliser la fonction de remplacement replaceTypedWords mais il faut la surcharger pour les fonctions car il faut gérer les collisions de nom.

La déduction de simplification

Il faut une déduction qui fasse un pas de traduction d'une fonction, comme dans compute.

Instance: une fonction Condition: aucune Déduit : une égalité entre la fonction est sa version simplifiée.

La traduction

Traduire une preuve avec cette extension nécessite de traduire les nouvelles déductions, mais aussi les formules.

Il me semble bien de traduire déjà les déductions, puis les formules. Car la traduction des déductions peut nécessite l'information sur la fonction.

Traduction des déductions

functionTranslateT

Il faut que la conclusion soit la même une fois traduit les formules. On a alors une vérité de la forme "x = x", et donc on doit traduire cette déduction par la déduction equalReflexivity. Il faudrait donc, soit définir cette déduction, soit importer les déductions déjà définies. La deuxième solution me parait mieux car on pourrait par ailleurs avoir besoin d'autres déductions.

Traduction des formules dans les déductions

Comme on aura déjà traduit les déductions, il s'agit des déductions hors cette extension.

Réponse