Lambda-calcul typé (système F) : algorithme de substitution

[samou_kh]

Bonjour à tous,

quelqu'un peut me donner en détails l'algorithme de substitution qu'on applique dans le système F?

Merci d'avance.

[gorgonite]

tu devrais lire ceci :
https://who.rocq.inria.fr/Gilles.Dow...es_types.ps.gz

en particulier le chapitre 9

[samou_kh]

Bonjour,

Merci pour le document, mais je trouve toujours un petit soucis concernant le cas d'une abstraction, quelqu'un peut me l'expliquer?

Merci d'avance.

[gasche]

Je connais Système F mais je ne comprends pas ta question. Qu'est-ce qui te pose problème et qu'est-ce que tu attends de nous ?

gorgonite > ce cours est intéressant mais je ne pense pas que ce soit une bonne source pour Système F, qui y est essentiellement décrit comme un cas particulier de Pure Type System. C'est puissant et abstrait, mais pas le plus intuitif ou clair quand on débute...

[gorgonite]

Envoyé par gasche

gorgonite > ce cours est intéressant mais je ne pense pas que ce soit une bonne source pour Système F, qui y est essentiellement décrit comme un cas particulier de Pure Type System. C'est puissant et abstrait, mais pas le plus intuitif ou clair quand on débute...

si je ne devais en lire qu'un seul (disponible en français), ce serait celui-là...

[gasche]

Ton message m'y fait penser: j'ai écris des notes sur les lambda-calculs typés pour un exposé à une groupe de travail de logique, qui présentent le lambda-calcul, Système F et Système Fomega de façon relativement vulgarisée -- mais plutôt pour des logiciens que pour des informaticiens.
Si ça intéresse quelqu'un, c'est ici :
http://gdt.ludics.eu/images/5/58/Type_theory_course.pdf

Bien sûr c'est un document de présentation/vulgarisation, en une dizaine de pages, pas du tout un cours ayant vocation d'être complet sur le sujet. Ça ne peut certainement pas remplacer un document comme le cours de Dowek, mais à mon avis c'est plus accessible pour une première approche.

[samou_kh]

Merci à tous pour ces explications.

Je trouve que ce document est très intéressant.

Ma question est:

est ce qu'il y a une différence entre l'algorithme de substitution dans le lambda calcul pure et l'algorithme de substitution dans le système F?

je sais que dans le système F on doit gérer deux types de substitutions:

la substitution des termes
la substitution des types

Je voudrais savoir est ce que c'est le même algorithme qu'on doit appliquer dans les deux substitutions ou pas?


Je vous remercie tous.

[gasche]

Je pense que tu peux répondre toi-même à ta question en définissant ces deux algorithmes de substitution pour les comparer. L'idée d'un algorithme de substitution est assez simple: on remplace les variables, et on substitue récursivement les sous-termes d'une expression un peu compliquée, en faisant attention à gérer les conflits de variables au niveau des lieurs (lambda, let, etc.) qui définissent de nouvelles variables (ayant peut-être le même nom que la variable substituée).

Comment définis-tu ces deux substitutions ?

[samou_kh]

Pour la substitution des termes, je pense qu'il faut appliquer l'algorithme classique, càd:

-si t est une variable, alors t[x/u]=u si x=t et t sinon

-si t est une application (vw)alors t[x/u]=v[x/u]w[x/u]

-si t est une abstraction (lambda y.v) alors t[x/u]=lambda y.(v[x/u]) si x est différent de y sinon t.

Mais la question se complique au niveau des types.

[gasche]

Ça c'est l'algorithme classique sur le lambda-calcul non typé. Quelle définition de System F utilises-tu ? Je suppose que c'est une définition explicitement typé, et alors tu as des cas supplémentaires à gérer (l'abstraction et l'application de types) dans ta définition de la substitution des termes.

(Quand je demande "quelle définition", je me demande quelles sont les grammaires que tu utilises pour décrire les termes et les types valides de ton système. Les règles de typage sont aussi importantes mais on peut les deviner à partir des grammaires en général.)

[samou_kh]

Bonjour,

Vous avez raison, l'algorithme que je viens de citer concerne le lambda calcul simple et pas le système F.

1)Pour la définition des types dans le système F, on a ceci:

Les types de base: t, v , les variables et les constantes.


Les variables de types: si α est une variable de type, alors α est un type.


Si A et B sont des types alors A ->B est un type.


Si α est une variable de type, B est un type alors ΠαB est un type.


En résumé: A,B:= α| A ->B | ΠαB


2)Les termes du système F sont définis comme suit:

Les termes de base: variables et constantes.


Application: si M et N sont des termes alors MN est un terme.


Abstraction: si x est une variable de terme, A est un type et M est un terme, alors λx:A.M est un terme.


Application de type: si M est un terme, A un type alors M{A} est un terme.


Abstraction de type: si α est une variable de type, M un terme, alors Λα.M est un terme.

Maintenant pour les algorithmes de substitution, on a:

1)Algorithme de substitution des types:

T[α:=A]

a)T est une constante: rien a faire.

b)T est une variable de type:
-T=α alors T[α:=A]=A
-T=B alors T[α:=A]=B

c)T est une application: T est U->V

T[α:=A]= U[α:=A]->V[α:=A]

d)T est une abstraction:ΠB.T[α:=A]

1)α est différent de B:
-pas de B dans A alors:

ΠB.(T[α:=A])


-B dans A alors il faut renommer B en G avec G n'appartient pas a T[B]A

2)α=B alors T.

j'aurais besoin de votre aide pour l'algorithme de substitution des termes.

Merci d'avance.

[samo87]

svp Gasche, est ce que c est possible d avoir un exemple de grammaire contenant la définition des types et des termes du système F
merci d'avance

[samou_kh]

Bonjour,

je ne sais pas si je peux vous aider, mais voici ce que je propose en prolog:

Pour les termes, mais sans l'application de types et sans l'abstraction de types:

Code :

1
2
3
4
5
6
7
8
9
10
11
12
is_Term(X):-
      var(X);
      atomic(X).

is_Term(app(M,N)):-
             is_Term(M),
             is_Term(N).

is_Term(lam(X-A,M)):-
             var(X),
             is_Term(M),
             is_Type(A).

ce je propose pour les types est comme suit:

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
cst_type(e).
var_type(t).

is_Type(X):-
       cst_type(X);
       var_type(X).
       
is_Type(X->Y):-
          is_Type(X),
          is_Type(Y).
          
is_type(pi(A,T)):-
              is_type(T),
              var_type(A).

Est ce que cette définition peut être considérée comme une grammaire à utiliser pour l'algorithme de substitution?

[gorgonite]

inutile de faire doublon, mets juste le lien vers ton proto en prolog
http://www.developpez.net/forums/d12...g/#post6624637

[gasche]

Envoyé par samou_kh

a)T est une constante: rien a faire.

b)T est une variable de type:
-T=α alors T[α:=A]=A
-T=B alors T[α:=A]=B

c)T est une application: T est U->V

T[α:=A]= U[α:=A]->V[α:=A]

d)T est une abstraction:ΠB.T[α:=A]

1)α est différent de B:
-pas de B dans A alors:

ΠB.(T[α:=A])


-B dans A alors il faut renommer B en G avec G n'appartient pas a T[B]A

2)α=B alors T.

j'aurais besoin de votre aide pour l'algorithme de substitution des termes.

En gros, l'idée est d'explorer récursivement les sous-termes, jusqu'à rencontrer un type, et là tu appliques l'algorithme de substitution sur les types.

Donc tu auras par exemple

(M{T})[α:=A] := M[α:=A]{T[α:=A]}

(M[α:=A] est une substitution sur les termes, T[α:=A] sur les types)

Le reste marche à peu près comme ça. La seule subtilité est
l'abstraction de type (Λβ.M)[α:=A] où il faut raisonner selon qu'il
y a un conflit de variables (α=β) ou non.

(Il y a aussi un risque de capture des variables dans A, mais ce
risque est déjà présent dans la substitution de termes et vous n'en
avez pas parlé pour l'instant donc j'imagine qu'on raisonne
avec assez de noms frais, ou modulo α-conversion.)

[SpiceGuid]

Il existe des Prolog étendus spécialement pour la substitution de variables.
Sur l'instant je pense à Alpha-Prolog mais je sais qu'il y en a d'autres (Qu-Prolog, Lambda Prolog) .

[samou_kh]

Bonjour,

merci pour vos réponses.

Pour l'algorithme de substitution pour les termes, d’après ce que j'ai compris, il n y a pas une grande différence avec les types, donc on peut l’écrire de cette façon:

a)T est une constante: rien a faire.

b)T est une variable de type:
-T=α alors T[α:=A]=A
-T=B alors T[α:=A]=B

c)T est une application: T est UV

T[α:=A]= U[α:=A]V[α:=A]

d)T est une abstraction:lambda X:C.T[α:=A] (avec C le type de X

1)α est différent de X:
-pas de X dans A alors:

lambda X:C.T[α:=A]


-X dans A alors il faut renommer X en Y avec Y n'appartient pas a T[X]A

2)α=X alors T.

e)T est une application de type

f)T est une abstraction de type


et dans le cas e et f qu'il faut gérer plusieurs cas.

Est ce que c'est bien ça l'algorithme de substitution des termes dans le système F?

Merci d'avance.

[samou_kh]

Bonjour,

je pense que j'ai dit quelques bêtises sur l'algorithme de substitution des termes, je corrige ça:

on veut gérer l'alpha conversion M[alpha:=A]
1)M est une constante, alors rien a faire

2)M est une variable de terme alors on a deux cas:

a) M=alpha alors M[alpha:=A]=A
b) M est différente de alpha et M=B alors M[alpha:=A]=B

3)M est une application: M=UV

M[alpha:=A]= U[alpha:=A] V[alpha:=A]

4)M est une abstraction: M=lambda x:B.N

a)alpha=x, alors M[alpha:=A]=M=lambda x:B.N

b)alpha est différente de x:

1)x n'appartient pas a N:
M[alpha:=A]:=lambda x:B.(N[alpha:=A])

2)x appartient a N:
a)x ne figure pas dans A alors
M[alpha:=A]:=lambda x:B.(N[alpha:=A])

b)x figure dans A alors on renomme x par y dans M (avec y ne figure pas ni dans N ni dans A) et après on fait la substitution.
M[alpha:=A]:=lambda y:B.(N[alpha:=A]).


pour les deux derniers cas, l'application de type et l'abstraction de type, d’après la réponse de Mr gasche:

application de type:
(M{T})[α:=A] := M[α:=A]{T[α:=A]}

mais est ce que je peux avoir plus d'explication sur comment on fait réellement cette substitution et aussi celle de l'abstraction de type( des exemples si c'est possible)


Merci a tous.

J'attends vos remarques.