Lazi

Qu'est-ce qu'un calcul

Contexte

Le postulat des principes fondateurs utilise la notion de calcul mais en forçant à un système de calcul (celui utilisé par la fonction everything), ce qui est réducteur. D'autre part comme le postulat affirme que tout calcul a lui-même une cause qui est un calcul, il faut que la notion de calcul soit large.

Question

Comment étendre de manière plus large la notion de calcul ?

Étude

Essai 3

Pour définir un calcul on a besoin :

  • d'un chemin mathématique de calcul C
  • d'une liste de formules de C qui corresponde à une déduction de calcul de C.

Un chemin mathématique de calcul est un chemin mathématique où l'on ajoute l'information, associée à chaque mathématique, d'une règle de calcul finale.

Essai 2

La notion de calcul, du fait que l'on veut comparer les ressources utilisées pour le réaliser, implique la notion de calcul élémentaire.

On peut avoir des calculs sophistiqués nécéssitant de garder des informations en mémoire (par exemple si on fait des calculs utilisant des références de manière à partager le résultat des calculs sur des formules identiques).

Le calcul univocal ne permet pas de calculer en parallèle car on ne peut pas calculer effictivement les données se trouvant dans une structure.

On voit que la manière d'évaluer une fonction change le calcul si on tient compte de l'effectivité. Donc un calcul n'a pas seulement comme paramètre ce qui est calculé mais aussi l'interpréteur du calcul. Si on définit l'interpréteur comme une fonction (sur des 1-formules), est-ce que fournir une fonction pour définir un interpréteur est suffisant ou cette fonction dépend-elle elle-aussi d'un interpréteur ? Comment définir un interpréteur ?

Donc un calcul est constitué :

  • d'une mathématique M extension de lazi.1.0
  • d'une formule à calculer f de M
  • d'une déduction de calcul c.

Problème

Il faut mieux que la définition même de calcul inclue les différentes étapes pour pouvoir définir ce que signifie "exister".
Il faut supporter les calculs infinis, donc on ne peut pas assimiler un calcul directement à une preuve.
Si l'interprétation de la mathématique réalisant le calcul est en lazi.1.0, alors est-ce que cela limite l'efficacité possible ?

De toute manière à la base il y a une interprétation en lazi.1.0.
S'il y a besoin de plusieurs niveaux d'interprétation, est-ce que tout peut-être condensé dans la mathématique interprétée en lazi.1.0 ?
Il y a équivalence entre une déduction de calcul et un calcul car :
À partir d'une règle de déduction de calcul (ou plus simplement "règle de calcul") on peut calculer cette déduction et donc déduire la formule d'arrivée (le y du x=y) à partir de la formule de départ (le x).
Le calcul (par interprétation) produit des égalités, comme on peut les prouver, on peut transformer cela en règle de calcul.
Les différents niveaux d'interprétation peuvent être vu comme différentes règles de calcul utilisés dans le calcul, comme on peut le faire dans une seule mathématique, de par l'équivalence "règle de calcul / fonction d'interpréation", on peut tout ramener à une mathématique.
Donc la réponse est "non".

Essai 1

Si on veut donner une définition mathématique il faut avoir un formalisme pour représenter les données du calcul, donc autant prendre les formules Lazi.0.0.

La notion de calcul implique une méthode déterministe pour passer d'un état au suivant, que l'on peut représenter par une fonction mais il faut qu'elle soit calculable et retourne une formule. Donc la fonction doit être une fonction partielle de l'ensemble des 1-formules vers l'ensemble des 1-formules.

Dfinition :
Soit F l'ensemble des formules lazi.0.0.
Soit x une suite dans F, on dit que x est un calcul ssi il existe une fonction partielle calculable c de F dans F tq pour tout n∈ℕ, xn + 1 = c(xn)
c est appelé les règles du calcul.

Le problème est que j'ai besoin d'une notion plus étendue (pour le calcul loose). D'autre part on peut imaginer que F ait besoin de garder des valeurs en mémoire et doivent donc posséder un état. Ce peut être utile par exemple pour un calcul comprenant des références : quand on exécute un "distribute" on cré une référence qui sera utilisée par la suite.

On pourrait distinguer les calculs automatiques, où il n'y a pas besoin d'instruction, des calculs à instructions. On peut aussi distinguer les calculs à états et sans état.
Ici pour le paradigme on a besoin de calculs automatiques mais il peut y avoir un état. Avec états on doit dfinir l'état de départ et la fonction de calcul doit retourner le couple $T[ état, formule ]. Il faut aussi que la formule puisse retourner l'information que la fonction n'est pas calculable.

Est-il nécessaire d'autoriser à retourner nom pas la formule suivante mais une liste de formules suivantes ?

Cela peut être utile pour optimiser le calcul, mais aussi pour réaliser un calcul en parallèle, car alors la formule suivante n'est pas déterminée par la précédente.

Pourquoi dans ce cas ne pas retourner le calcul entier ?

On définit une fonction "calculator" qui retourne le calcul entier. Mais si on veut garder la structure de liste il faut l'inverser pour que le dernier élément soit le premier du calcul puisque les listes infinies Lazi on juste un dernier élément. Le calcul peut être vide si aucun calcul n'est possible. Comme la valeur retournée est une liste la fonction calculator ne peut indéfiniment calculer un des termes du calcul, mais elle peut retourner une liste infinie.

Donc un calcul est une liste de 1-formule résultant d'une fonction Lazi. Ce ne peut être des 0-formules car on doit pouvoir calculer les éléments de la liste.

Puisque l'on n'a plus la notion d'étapes de calcul, peut-on quand même avoir une notion de temps ?

Pour cela il faut montrer que, peut-importe la manière de calculer, un calcul est toujours calculé par étapes. On calcule par étape car on parcours la liste en calculant les éléments un par un. On peut éventuellement définir un interpréteur spécial qui calcule explicitement la liste des 1-formules.

Que signifie qu'un calcul A est la cause de l'existence d'un calcul B ?

Il y a beaucoup de manières de représenter une formule, le problème est que la fonction de traduction ne doit pas faire elle-même le calcul. Par exemple le calcul A pourrait juste énumérer les entiers et ce serait la fonction de traduction qui génèrerait B.
Pour s'adapter à diverses formes de calculs il faut utiliser la notion d'extension mathématique.

Remarques sur les mathématiques Lazi et les extensions

Le système d'extension défini dans les fondations

En Lazi il est possible de signifier "ceci est vrai" et aussi "le sens de cette phrase". On peut dès lors définir un autre représentation de preuve différente, une fonction de traduction, prouver que sur un certain domaine ces nouvelles preuves se traduisent en preuves valides lazi, et donc déduire ainsi des vérités.

Essai 1 : calcul du point de vue mathématique

Définition d'un calcul

Soit M une mathématique et l une formule pour M. On dit que l est un calcul ssi :
Pour M, l est une liste, finie ou non.
Pour M tous les éléments de la liste l sont égaux entre eux.

Remarque : on pourrait se demander si la liste l est récursive primitive, c'est forcément le cas puisqu'elle est définie par une formule l.

Définition d'un calcul A cause d'un calcul B

Soit l1 un calcul pour une mathématique M1. Soit l2 une sous-liste de sous-formules de l1 qui est un calcul pour M2. Alors le calcul l1 est une cause du calcul l2.

Exemple trivial :
l1 est la liste infinie où alterne 1 + 0 et 0 + 1.
l2 est la liste infinie de 1
l1 est une cause de l2 car on peut êtraire de l1 une sous-liste de 1.

Exemple très complexe :
l1 est le calcul de notre univers par la mathématique M1.

Remarque : est-ce que l'égalité dans les termes de B ne devraient utiliser M1 ?

Pourquoi devrait-on avoir égalité entre les éléments ?

Réponse

Un calcul est défini par :

  • un chemin mathématique de calcul C
  • d'une liste de formules de C qui corresponde à une déduction de calcul de C.

Un chemin mathématique de calcul est un chemin mathématique où l'on ajoute l'information, associée à chaque mathématique, d'une règle de calcul finale.

@todo