Lambda-calcul, formes normales, types
Bonjour,
Si $t$ est un terme du lambda-calcul, en forme normale, c'est-à-dire qu'on ne peut plus lui appliquer de $\beta$-réduction, et si de plus $t$ n'a pas de variables libres, alors $t$ est simplement typable (il me semble). Est-ce que $t$ possède un type minimum $T_1$, au sens où, si $T_2$ est un autre type de $t$, alors on obtient $T_2$ en substituant des types aux variables de type de $T_1$ ?
Exemple: $\lambda x ~x$ est de type $A \to A$, mais aussi de type $(B \to C) \to (B \to C)$, mais on obtient ce deuxième type en substituant à $A$ le type $B \to C$. Donc ici le type minimum serait $A \to A$.
Est-ce que si deux termes en formes normales sans variables libre ont même type minimum, alors ils sont équivalents (par substitution correct des noms de variables) ?
Exemple: $\lambda x ~x$ et $\lambda y ~ y$ ont même type minimum (si il existe) et sont équivalents en substituant $y$ à $x$.
Merci d'avance.
Si $t$ est un terme du lambda-calcul, en forme normale, c'est-à-dire qu'on ne peut plus lui appliquer de $\beta$-réduction, et si de plus $t$ n'a pas de variables libres, alors $t$ est simplement typable (il me semble). Est-ce que $t$ possède un type minimum $T_1$, au sens où, si $T_2$ est un autre type de $t$, alors on obtient $T_2$ en substituant des types aux variables de type de $T_1$ ?
Exemple: $\lambda x ~x$ est de type $A \to A$, mais aussi de type $(B \to C) \to (B \to C)$, mais on obtient ce deuxième type en substituant à $A$ le type $B \to C$. Donc ici le type minimum serait $A \to A$.
Est-ce que si deux termes en formes normales sans variables libre ont même type minimum, alors ils sont équivalents (par substitution correct des noms de variables) ?
Exemple: $\lambda x ~x$ et $\lambda y ~ y$ ont même type minimum (si il existe) et sont équivalents en substituant $y$ à $x$.
Merci d'avance.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Comment types-tu $\lambda x. (x)x$?
être fortement normalisable (toute réductions de FedEx faites dans l'ordre que tu veux terminé sur terme normal en temps fini)
Être typable avec le système "intersection"
De mon téléphone
Pour ma deuxième question: même type minimum => equivalence, je crois que c'est faux: par exemple l'entier $\lambda f . \lambda x.(f)(f)x$ et l'entier $\lambda f. \lambda x. (f)(f)(f)x$ ont même type minimum (?), mais ne sont pas équivalents.
Par exemple je préfère typer x.x avec :
A inclus dans (A=>B)
plutôt que A = (A=>B)
Bon pardon l'exemple est mal choisi car terme normal et suis sur mon téléphone. Mais l'idée est DE NE PAS , SURTOUT PAS, discriminer les termes non normalisables.
Je préfère imposer la philosophie "tout terme SE DOIT d'être typable".
C'est la traduction des habituels clivages que je dénonce déjà en logique des fondements où on a eu une hystérie qui prétendait ne s'autoriser que des théories consistantes.
Windows ou linux "se doivent d'être typables" par exemple.
La règle est simple: le sous terme u.v doit se typer comme suit:
v : A
u : B->C
Ajout hypothèse : A inclus dans B.
Naturalisme en résumé !
Et SURTOUT PAS A=B. Et ENCORE PLUS SURTOUT PAS reherhe de construction. En maths on suppose on ne construit pas (dans ce paradigme général en tout cas).
Il y a une trialite : terme, environnement, bottom cruciale dont l'approche par contemplation des termes seuls ne rend pas bien compte.
Éliminer une coupure (ie killer UN redex) est qu'une petite partie de ce qu'est "exécuter un terme".
Dans un test par exemple du genre if a then b else c, si a = false et b non normalisable , il est "vraiment dommage" d'exécuter b.
D'une certaine façon "fortement normalisable = trivial" en CARICATURANT !
Est-ce que les termes du lambda-calcul qui représentent des fonctions récursives primitives, se distinguent de ceux qui représentent des fonctions seulement récursives ? (par une propriété du type fortement normalisable, ou typable dans tel système de types, ou autre)
Est-ce que l'on peut de même distinguer les termes simplement typables ? Peut-être que leur application s'éxécute en temps polynomial en fonction des entrées ?
Merci d'avance.