Lazi

Critère de sélection des prémisses

Contexte

Pour que l'extension "imply" soit valide il faut interdire certains prémisses.

Question

Quel critère utiliser pour que la prémisse soit valide.

Étude

Formules à égalité près

Du point de vue des déductions, deux formules sémentiquement égales sont équivalentes puisque l'on peut les remplacer. Par exemple si a = b alors (a ⇒ c) = (b ⇒ c) et donc si l'une est vraie l'autre aussi.

Nombre d'imply dans une formule

On a 1b = (if 1b 1b \ imply imply imply). Cet exemple nous montre que le nombre d'imply peut varier entre deux formules égales. Pour pouvoir raisonner sur le nombre d'imply il faut ajouter des conditions pour éliminer le "bruit" ou la factorisation (comme dans "($F im → im a (im b c)) imply" ).

Une condition simple est que toute les sous-formules contenant un imply aient leur calcul terminée. Cela suppose qu'elles n'ont pas de récurrence infinie mais on veut justement éviter un nombre infini d'imply.

Qu'est-ce qui fait qu'une prémisse rend la déduction invalide ?

C'est le fait qu'elle peut servir à prouver l'implication entière. Pour cela il faut qu'elle ait le même nombre d'implications que l'énoncé tout entier, ce qui est donc une équation de la forme n ≥ n + 1. La solution est donc n = infini (comme dans A = A ⇒ B ).

Est-ce qu'une prémisse ayant une infinité d'imply peut avoir un intérêt ?

Nous parlons d'une cas d'une formule récurrente, on ne peut les avoir que petit à petit en calculant la formule.

Les imply sont utilisé dans les preuves, si on appliquait tous les imply il faudrait une preuve infinie. Donc pas pour les applications. Un imply qui n'est pas appliqué n'a pas d'intérêt car il pourrait être vrai, faux ou autre.

Donc non, il n'y a pas d'intérêt de pouvoir avoir un nombre infini d'imply dans une formule.

Est-ce que le mot "imply" dans un argument d'une fonction a un intérêt ?

Oui, par exemple on peut définir ¬ x = x ⇒ ⊥ et donc la négation est une fonction, elle a en argument d'un distribute un imply, et si x contient un imply, c'est aussi le cas pour le 3ième argument du distribute (celui qui peut être dupliqué).

Quel critère pourrait-on utiliser ?

On voit qu'il faut éliminer la possibilité d'avoir un nombre infini d'imply. On ne peut pas ajouter un mot clé pour déduire dans la mathématique que la prémisse vérifie la condition car on a plutôt des critères qui ne sont pas compatibles avec l'égalité sémantique.

Essai 2 : Critère du calcul terminé sans calcul (valide)

Contexte

Le problème du critère 1 est de risquer de boucler si le critère est faux. Cela est possible pour les types, mais ici il ne s'agit pas vraiement d'un type.

Le critère

Il dépend du mot clé de la fonction principale. Pour chaque mot clé il existe une fonction qui répond à la question :
Est-ce que la formule ne multiplie pas à l'infini le mot "x" ?

Remarquons que le critère a seulement besoin de rejeter la multiplication à l'infini de imply, c'est acceptable de rejeter plus.

Validité du critère

Si le mot "imply" n'est pas multiplié ou s'il n'est nul part mutiplié à l'infini alors il ne peut y en avoir une infinité.

Implémentation du critère

De toute manière, pour supporter les extensions il était nécessaire d'avoir une fonction supplémentaire par type. Donc il est correcte d'ajouter une fonction aux types. Remarquons que ça impose d'avoir un type pour chaque mot et chaque notation (comme $Def). C'est vrai actuellement pour chaque notation (voir formulaT) mais pas pour chaque mot.
Il est aussi nécessaire d'utiliser la question «La formule contient-elle le mot "x" ?», qui est déjà implémentée.

Le cas "distribute" :

À première vue si imply n'est pas dans le troisième argument alors il ne peut y avoir multiplication. Mais on peut avoir un distribute en argument , par exemple :

distribute (constF \ distribute a b) (constF imply) c = 
(constF \ distribute a b) c \ constF imply c =
distribute a b imply

On peut avoir comme règle :

  • Si imply est nul part : retourne 1b
  • Si le dernier argument n'est pas dupliqué (si l'un des deux premiers arguments est un constF x ou if 1b x ): éxécute le calcul élémentaire et vérifie sur le résultat.
  • Sinon le dernier argument est dupliqué : retourne 0b.

Le cas "($F → ...) x" :

À première vue si imply n'est pas dans l'argument, ou s'il est dans l'argument mais que x n'est utilisé qu'une fois alors il n'y a pas multiplication. Mais sauf si imply est nulle part il faut aussi faire le remplacement et voir pour le résultat, Mais il faut éviter les boucles infinies de calculs. On peut très bien avoir un imply dans un coin non multiplié mais une récursion infinie à vérifier.
Idée de règles :

  • Si imply est nul part : retourne 1b.
  • Si l'argument est dupliqué : retourne 0b.
  • Sinon vérifie le résultat du remplacement.

Essai 1 : Critère du calcul terminé par teste de calcul (invalide)

Le critère

La prémisse doit être sémantiquement égale à une formule telle que toute ses sous-formule contenant un imply doit être un calcul terminé.

Validité du critère

Une formule contenant une infinité d'imply doit avoir une récurrence infinie, elle ne peut avoir ses calculs terminés.

Implémentation du critère

Il suffit de vérifier pour chaque sous-formule de la prémisse contenant un imply qu'elle n'a pas de récurrence infinie. Deux problèmes se posent :

  • Comment ce critère supporte les extension ? En effet une extension pourrait changer la manière de calculer. Par exemple définir une variable et sa valeur change les calculs (il faut remplacer la variable par sa valeur).
  • Quel algorithe de vérification ?

Comment suporter les extensions ?

Il faudrait que les extensions changeant le calcul aient des fonctions supplémentaires dans leurs types.

Algorithe du critère

  1. Chercher toutes les sous-formules contenant un imply (il peut ne pas y en avoir).
  2. Pour toutes ces sous-formules, vérifier si le calcul peut être terminé.

Problème

Si le calcul ne peut être terminé, avec cet algorithme, le calcul de validation boucle indéfiniment. Alors que pour les autres extensions, une fois que les types sont vérifiés il n'y a pas de problème possible.

Réponse

Pour chaque mot clé on définie une fonction qui répond à la question :
Est-ce que la formule ne multiplie pas à l'infini le mot "x" ?
Voir "Essai 2" pour des détails sur le critère.