Études-Mathématique/Quels types racine de Lazi ?

From Lazi wiki
Jump to: navigation, search

Question

Si on ajoute des données dans le contexte général qui ne soit pas sous forme de type (comme une entrée "data" dans topT), est-ce un problème ?

Quels sont les types racines de Lazi ?

Étude

Les données dans le contexte général servent à changer le comportement des types, et donc à les paramétrer. Pourquoi alors ne pas utiliser le système des inchas, c'est à dire que les données sont typés et peuvent être comparées etc.

Par exemple si on veut avoir en paramètre une liste de variable, on cré un type qui prend en instance une liste de mot et qui retourne le type topT de tous les types. Mais alors pour accéder à un des types de topT il faut avoir la liste des variables.

Si les données ne sont pas manipulées (comme un flag "debug"), il n'y a pas d'intérêt de les typer.

Il faut être sûr que les données de topT sont constantes pour le contexte, c'est à dire qu'il n'y a pas besoin de manipuler en même temps deux objets avec des topT différents ou encore de comparer des instances ayant des topT différents.

Exemple des formules

Le type "formule" a en paramètre la liste des noms de variable.

On a besoin de spécifier précisément les types de formules, il faut donc que ces paramètres soit vus comme des instances d'un type plus général. On a donc un type "formulaT" qui a en instance la liste des variables. Comme on ne veut pas utiliser deux système, on n'a donc pas besoin de data.

Exemple du flag debug

Le contexte général n'a pas pour instance un objet utilisable (contrairement à "Formula"). C'est à dire que l'on n'a pas besoin d'un objet qui soit l'unification d'une formule et d'une preuve. On peut alors ajouter un champs directement à topT.


Pas de type top pour le contexte général ?

Comme il n'y a besoin que de deux types (pour les formules et pour les déductions), et qu'il sont indépendants (c'est à dire que l'on a pas un objet qui est soit une formule soit une déduction, il n'y a pas vraiment d'intérêt d'avoir un type topT si ce n'est:

  • la simplicité d'un objet unique
  • l'extensibilité.

Pour ne pas perdre les avantages de topT, il serait possible de créer un contexte général qui soit un objet avec les entrées :

  • getFormulaT
  • setFormulaT
  • getDeductionT
  • setDeductionT

Un type "truthT" ?

Une instance de truthT est une déduction. L'objet correspondant est la liste des conditions et la conclusion.

Les déductions ont en argument truthT, qui est donc récursif.

Une des déductions, "proofT" prend en instance une liste de déduction.

Une des déduction, extensionT prend en argument une preuve d'une extension valide, et une déduction dans cette extension. Son objet est une formule Lazi-0, traduction de la formule déduite dans l'extension.

Ajout à truthT

Certaines déductions nécessitent un truthT utilisant des variables, d'autre part la déduction extensionT a besoin d'ajouter des types de déduction à truthT. On peut remarquer que l'on a uniquement besoin d'ajouter.

truthT = deductionT incluant formulaT

Cela me semble donc une mauvaise idée, il faudrait plutôt garder l'idée du contexte comme couple deductionT,formulaT.

Réponse

Le contexte général M est constitué des deux informations deductionT et formulaT. On utilisera un objet pour assembler ces deux informations. C'est un objet récursif, deductionT a en argument M, formulaT a en argument lui-même.

Lazi-0 est un M particulier: avec deductionLazi0T et formulaLazi0T.