Études-Mathématique/Extension compute

From Lazi wiki
Jump to: navigation, search

Contexte

Certaines extensions (comme wordRepr) traduisent leurs déductions en un calcul (comme celui de wordEqual). Pour éviter que ces déductions aient à produire la démonstration (lourde) du calcul, on peut d'abord créer une extension qui déduit une égalité entre une formule et le résultat du calcul de celle-ci. C'est à cette extension de produire la démonstration prouvant le calcul.

Par la suite certaines extensions pourront fournir des shortcuts pour calculer certaines formes de formules.

Question

Quel est l'algorithme de calcul des formules ? Et celui générant sa preuve ? Comment organiser les shortcuts ? Peut-on en tenir compte dans l'extension "compute" alors qu'elle est antérieure ?

Étude

Algorithme de calcul

Chaque type constituant de formulaT possède une fonction "compute". On utilise une pile (une liste) contenant les arguments à calculer, au début elle est vide, "apply" y ajoute des choses (même système que le logiciel lazy-compute).

Une fonction "compute" d'un type constituant prend en argument:

  • la partie "fonction" à calculer (toute la formule au début)
  • la pile des arguments

et elle retourne maybe $T[résultat du calcul, pile des arguments]. Si elle retourne nothing, cela signifie qu'il n'y a pas eu de calcul. Sinon dans la valeur retournée, la pile des arguments est mise à jour.

apply

il retourne la partie fonction et pousse l'argument dans la pile.

if

Il dépile 3 arguments, calcul la condition, puis si le résultat est 1b ou 0b retourne la bonne valeur, sinon retourne "nothing".

:dvar:...

Teste si il existe une fonction compute spécifique pour ne nom (c'est donc un shortcut), si oui sous-traite à cette fonction. Sinon retourne la valeur de la dvar et la pile intacte.

Les shortcuts

Voir algorithme de calcul. Les fonctions de shortcut se trouvent dans un dictionnaire appartenant à computeT.

Bien sûr, chaque extension ajoutant un shortcut devra prouver la validité de cette modification.

Génération de la preuve du calcul

Exemples

if 1b equal 1b 0b

Le résultat du calcul est "equal 0b". On voit qu'il faut effectuer le calcul sur une sous partie, il y a donc une partie de la preuve qui consiste à prouver la valeur globale à partie de la valeur de la sous-partie calculée.

if 1b if 1b 0b 1b 0b

Le résultat du calcul est 0b. On a if 1b if 1b 0b 1b 0b = if 0b 1b 0b = 0b.

if 1b :dvar:pair 1b 0b 1b

Le calcul est

if 1b :dvar:pair 1b 0b 1b = 
:dvar:pair 0b 1b = 
($F  x,y,c → if c x y) 0b 1b =
($F y,c  → if c 0b y) 1b =
($F c  → if c 0b 1b)

L'algorithme

La fonction générale "computeAndProve" délègue au type de la partie fonction, sauf pour Apply.

La preuve est construite linéairement.

computeAndProove prend en argument la pile des arguments. Si la pile n'est pas vide alors la fonction appelante a déjà déterminé que, si un calcul est produit, tous les arguments seront utilisés.

Comme pour compute, la fonction relance le calcul sur le résultat tant que le calcul et sa preuve avance. À chaque pas il faut utiliser la déduction de transitivité pour assembler les deux preuves.

  • Si le type de la formule est "apply":
    • Si la pile n'est pas vide ou si la partie fonction ne peut être calculée seule : on ajoute la partie argument dans la pile, et on récurse sur la partie fonction. En effet, on est sûr que s'il y a un calcul l'argument de la pile sera utilisé: si la pile n'est pas vide, car alors l'argument déjà présent dans la pile sera utilisé cela implique que le nouvel argument le sera aussi, et si la partie fonction ne peut être calculée seule cela implique si s'il y a un calcul c'est avec l'argument.
    • Sinon (on a alors la pile vide et la partie fonction est calculée seule): à partir de la preuve du calcul on génère le calcul et sa preuve avec l'argument ( on a f1=f2 et il faut prouver "f1 a = f2 a").
  • Si le type de la formule n'est pas "apply": on soustraite au type constituant.

Réponse

Pour chaque type composant de formulaT on cré une fonction "compute" et "computeAndProve", compute est une fonction virtuelle qui par défaut appelle computeAndProve et jète la preuve (pour éviter d'écrire du code similaire. Voir l'étude pour le fonctionnement.