Lambda-calcul, formes normales, types

marco

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.

marco

Cependant, le terme $\lambda x ~(x)x$ est en forme normale sans variable libre, mais je ne sais pas si il est simplement typable.

Alesha

Marco a écrit:

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).

Comment types-tu $\lambda x. (x)x$?

Alesha

Je viens de voir ton dernier message. Bien sûr que $\lambda x.(x)x$ n'est pas simplement typable. Suppose que $x$ a un type $A$. On doit avoir que $A = B \to C$ pour certains $B$ et $C$ et on doit avoir que $x$ est de type $B$, donc $B = B \to C$, ce qui est contradictoire.

marco

Merci, en effet, ça ne marche pas. Mais est-ce qu'il n'y a pas des systèmes de types où tout terme en forme normale est typable ? Par exemple, si on autorise à une variable d'avoir plusieurs types par exemple ici en supposant $x$ de type $A$ et de type $A \to A$: on note $A \wedge (A \to A)$ je crois.

Alesha

Oui, ce sont les types avec intersection.

christophe c

@marco c'est une équivalence entre

ê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

christophe c

Redex** (sacré téléphone) :-D

marco

Merci. Dans le cadres des types avec intersection, est-ce qu'on ne peut pas définir un type minimum pour un terme $t$ en forme normale sans variable libre. Les autres types de $t$ se déduiraient du type minimum, soit par des substitutions (remplacement de variables de type par d'autres types), soit par des suppressions de variables ou d'expressions (peut-être en occurrence positive seulement: en effet un terme de type $A \wedge B$ est donc de type $A$ aussi), soit par des ajouts (en occurrence négative: par exemple un terme de type $A \to C$ est aussi de type $(A \wedge \to C$, soit par une combinaison de ces trois opérations (substitution, suppression, ajout).

christophe c

Oui je l'ai fait sur caml pour m'amuser il y a longtemps. Mais suis sur mon téléphone. De plus ça atteint vite ses limites car "être fortement typable" est récursivement enumerable ET créatif.

marco

Merci Christophe.
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.

marco

À moins que le premier entier soit de type minimum $((A \to \wedge (B \to C))\to (A \to C)$ et le second de type $((A \to \wedge (B \to C) \wedge (C \to D))\to (A \to D)$.

christophe c

Toujours de mon téléphone, à titre personnel mais ce est pas académique, je préfère le procédé "encore plus minimaliste" qui introduit le symbole inclusion au lieu de égal mais qui du coup va ajouter des hypothèses extérieures.

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).

christophe c

Précision : ni Windows ni linux ne sont normalisables évidemment.

marco

D'accord, merci.

christophe c

De mon téléphone : si tu veux accéder au concept robuste et indépendant "des choix des gens" sur le risque acceptable, Google "realisabilite". Ou vas sur la page de Krivine.

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 !

marco

Merci, je vais aller voir la page de Krivine.

marco

Bonjour,

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.

marco

Je crois que ce que j'appelais type minimum s'appelle en fait dans le livre de Krivine "typage principal".

christophe c

Possible. Je ne m'y connais pas assez (en tout cas en vocabulaire officiel)!