Discussion :

[blili]

Bonjour à tous,

j'aurais besoin de votre aide pour faire une implémentation du système F en prolog.

D'abord la définition de la grammaire qu'il faut utiliser pour décrire les termes et les types valides du système F, sachant que la définition des types et des termes du système F est donnée comme suit:

1)Les types du système F:

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:

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.

J'ai vraiment besoin de votre aide pour implémenter ça en prolog.

Merci à tous.

[Trap D]

Pas forcément simple, c'est le moins qu'on puisse dire, et j'ai cru comprendre que tu débutais en Prolog.
Il va te falloir choisir des opérateurs par exemple pour ça

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

comment ecrire "MN" ?
Renseigne - toi sur les opérateurs en Prolog.
Je pense que tu devra lier les termes avec leurs types (style A:B) pour pour pouvoir associer un type B a un terme A et que Prolog puisse savoir de quoi on parle (d'ou encore un opérateur à définir).

Commence à ébaucher quelques lignes de code montre les et explique tes problème, alors on pourra t'aider.

Personnellement, je peux t'aider en Prolog mais pas sur le langage F.

[gorgonite]

Il va te falloir choisir des opérateurs par exemple pour ça comment ecrire "MN" ?

et pourquoi pas "simplement" un prédicat App/2 ?


je remets un lien utile : http://www.sfs.uni-tuebingen.de/~fr/...ris-lambda.pdf

[Trap D]

Pourquoi pas effectivement app(M, N) mais on pourrait noter M@N par exemple.

[blili]

Bonjour,

merci pour vos réponses.

Effectivement,on peut utiliser app/2, voici ce que je propose mais je ne suis pas sur si c'est juste:

pour la représentation des termes:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

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

Mon problème est comment représenter l'application de type et l'abstraction de type?

Pour les types, voici ce que je propose:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

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

J'attends vos remarques, j'ai vraiment besoin de votre aide pour valider ça et passer a la suite qui consiste a faire les réductions dans le système F.


Merci a tous.

[blili]

Bonjour à tous,

cette fois, j'ai vraiment besoin d'aide en prolog.

J'ai besoin d'avoir la liste des variables contenues dans un type, sachant qu'un type dans le système F peut être une constante, une variable ou sous la forme X->Y (X et Y des types aussi) ou encore sous la forme all(X,Y) (avec X et Y des types aussi).

j'ai écrit un petit programme qui fonctionne lorsque le type en entrée est une variable, mais j'ai un problème quand je fais la récursion pour les types complexes (X->Y et all(X,Y)).

Voici le code:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
variablesInType(Type,List_Variables):-
                            is_type(Type),!,
                            variablesInType(Type,List_Variables,[]).
 
 
 
variablesInType(Type,[Type|List_Variables],List_Variables):-
                            is_variable(Type),!.
 
variablesInType(Type,List_Variables,List_Variables):-
                      type_fleche(Type),!,
                      Type=..[Symbol|Arguments],
                      Arguments=[Args|Rest],
                      is_variable(Args),!,
                      Rest1=..Rest,
                      is_type(Rest1),!,
                      variablesInType(Rest1,[Args1|List_Variables],List_Variables).

en utilisant "trace.", le code compile parfaitement jusqu’à l'appel récursif de variablesInType.

j'ai vraiment besoin de votre aide pour corriger ça.

Merci a tous.

[Trap D]

Bonjour

Avant d'aller plus loins, tu devrais avoir deux warnings de compilation de ton code dans la deuxième règle variablesInType :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
variablesInType(Type,List_Variables,List_Variables):-
	type_fleche(Type),!,
 
        Type=..[Symbol|Arguments],  <= Symbol est un singleton
 
        Arguments=[Args|Rest],
        is_variable(Args),!,
        Rest1=..Rest,
        is_type(Rest1),!,
        variablesInType(Rest1,[Args1|List_Variables],List_Variables). <== Args1 est un singleton

Cela n'est jamais bon, est-ce volontaire ? Si oui met un '_' devant pour le signifier et ne pas avoir de warning.
Pour le reste donne un code complet (il manque les prédicats is_variable et type_fleche et un exemple de question qui te pose problème, c'est à dire la prédicat d'appel et le resultat attendu.

Bon courage

[blili]

Pour la représentation des types, voici le code:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
 
 
is_cst(e-X):-
        integer(X).
is_cst(t-X):-
        integer(X).
 
is_variable(V-X):-
           var(V),
           integer(X).
 
is_type(U):-
       is_variable(U).
 
is_type(U):-
       is_cst(U).
 
is_type(U->V):-
           is_type(U),
           is_type(V).
 
is_type(pii(A,T)):-
              is_type(A),
              is_type(T).
 
type_fleche(X->Y):-
      is_type(X),
      is_type(Y).
 
type_qant(pii(X,Y)):-
      is_type(X),
      is_type(Y).

pour la ligne de code:
Type=..[Symbol|Arguments],

le but est de former le type (le cas de type complexes) sous forme d'une liste pour pouvoir extraire les variables de ses composants.


un exemple de résultat attendu est:

variablesInType(X-1->X-2,List).

résultat:List=[X-1,X-2]

variablesInType(X-1->X-2->X-1,List).

résultat:List=[X-1,X-2,X-1]


variablesInType(pii(X-1,X-2),List).

résultat:List=[X-1,X-2]

variablesInType(pii(X-1,(X-1->X-2)),List).

résultat:List=[X-1,X-1,X-2]


Merci d'avance.

[Trap D]

Tu as deux prédicats semblables :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
is_type(pi(A,T)):-
              is_type(T),
              var_type(A).
 
is_Type(X):-
       cst_type(X);
       var_type(X).

t minuscule et T majuscule, volontaire ou pas ?

[blili]

pour is_Type(X) avec le t en majuscule était une faute de frappe.

La dernière version du code est la plus correcte, celle que j'ai mis ce matin, donc il ne faut pas regarder l’ancienne version, il faut juste voir celle la:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
 
is_cst(e-X):-
        integer(X).
is_cst(t-X):-
        integer(X).
 
is_variable(V-X):-
           var(V),
           integer(X).
 
is_type(U):-
       is_variable(U).
 
is_type(U):-
       is_cst(U).
 
is_type(U->V):-
           is_type(U),
           is_type(V).
 
is_type(pii(A,T)):-
              is_type(A),
              is_type(T).
 
type_fleche(X->Y):-
      is_type(X),
      is_type(Y).
 
type_qant(pii(X,Y)):-
      is_type(X),
      is_type(Y).

Merci.

[Trap D]

En regardant un peu les prédicats, je pense que que tu utilises le prinicpe des accumulateurs.
L'habitude est de mettre les arguemnts d'unetrée en premier et les arguments de sortie en fin.
Le prédicat d'appel sera donc

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
variablesInType(Type,List_Variables):-
	is_type(Type),!,
        variablesInType(Type,[], List_Variables).

Ce qui fait que ton premier prédicat s'écrit

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
variablesInType(Type, List_Variables, [Type|List_Variables]):-
	is_variable(Type),!.

Maintenant, ceci me gene beaucoup

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
variablesInType(Type,List_Variables,List_Variables):-
	type_fleche(Type),!,
        Type=..[_Symbol|Arguments],
        Arguments=[Args|Rest],
        is_variable(Args),!,
        Rest1=..Rest,
        is_type(Rest1),!,
        variablesInType(Rest1,[Args1|List_Variables],List_Variables).

2 fois la même variables en entrée du predicat, j'aurais plutôt vu

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
variablesInType(Type,List_Variables_In,List_Variables_Out):-
	type_fleche(Type),!,
        Type=..[_Symbol|Arguments],
        Arguments=[Args|Rest],
        is_variable(Args),!,
        Rest1=..Rest,
        is_type(Rest1),!,
        variablesInType(Rest1,[Args1|List_Variables_In],List_Variables_Out).

Maintenant, cela a l'aire de mieux fonctionner

variablesInType(X-1->X-2,List).
List = [X-2,X-1].

17 ?- variablesInType(X-1->X-2->X-1,List).
List = [X-1,X-2,X-1].

Pour variablesInType(pii(X-1,X-2),List). je regarde plus avant.

[blili]

Merci Monsieur pour votre réponse.

Pour pii(X,Y), il suffit juste de modifier dans le code, au lieu de faire le test
fleche_type(Type), il faut mettre is_type(Type).

[Trap D]

OK !
Juste une petite remarque :

?- variablesInType(X-1->X-2->X-3,List).
List = [X-3,X-2,X-1].

Le résultat est-il correct ou faut-il avoir List = [X-1, X-2, X-3] ?

[blili]

justement, avec :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

?- variablesInType(X-1->X-2->X-3,List).

on doit avoir le résultat:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

List = [X-1, X-2, X-3]

Merci.

[Trap D]

Oui, c'est bien ce que je pensais, donc on a

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
variablesInType(Type, List_Variables_In, List_Variables_Out):-
	is_variable(Type),!,
	reverse([Type | List_Variables_In], List_Variables_Out).

Peut-on avoir variablesInType(pii(X-1,X-2,X-3),List). ?

[blili]

Bonjour,

on ne peut pas faire le test:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
 
variablesInType(pii(X-1,X-2,X-3),List).

car pii prends deux paramètres, par contre on peut tester:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
 
?- variables_In_Type(pii(X-1,X-3->X-2),L).

et voici ce qu'il affiche comme résultat:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
 
X = _G425
L = [_G535, _G550, _G425-2] ;

alors qu'on s'attend au résultat suivant:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
 
X = _G425
L = [_G425-1, _G425-3, _G425-2] ;

Est ce que le résultat qu'on a eu est aussi correcte ou pas?

Merci

[Trap D]

Je suis surpris, moi j'obtiens avec mon code :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
 ?- variablesInType(pii(X-1,X-3->X-2),L).
L = [X-1,X-3,X-2].

D'ailleurs, le voici

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
variablesInType(Type,List_Variables):-
	is_type(Type),!,
        variablesInType(Type,[], List_Variables).
 
 
 
variablesInType(Type, List_Variables_In, List_Variables_Out):-
	is_variable(Type),!,
	reverse([Type | List_Variables_In], List_Variables_Out).
 
variablesInType(Type,List_Variables_In,List_Variables_Out):-
	type_fleche(Type),!,
        Type=..[_Symbol|Arguments],
        Arguments=[Args|Rest],
        is_variable(Args),!,
        Rest1=..Rest,
        is_type(Rest1),!,
        variablesInType(Rest1,[Args|List_Variables_In],List_Variables_Out).
%        variablesInType(Rest1,[Args1|List_Variables],List_Variables).
 
variablesInType(Type,List_Variables_In,List_Variables_Out):-
	is_type(Type),!,
        Type=..[_Symbol|Arguments],
        Arguments=[Args|Rest],
        is_variable(Args),!,
        Rest1=..Rest,
        is_type(Rest1),!,
        variablesInType(Rest1,[Args|List_Variables_In],List_Variables_Out).

[blili]

Merci Monsieur,

effectivement c’était une erreur de ma part.

tous les tests m'affichent ce que je veux exactement.

Merci encore une fois.

[Trap D]

Comme ça semble être correct, on perut un peu ameliorer le code en regroupant les deux regles en une seule :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
variablesInType(Type,List_Variables_In,List_Variables_Out):-
 
	(   type_fleche(Type); is_type(Type)),!,   <== changement ici
 
        Type=..[_Symbol|Arguments],
        Arguments=[Args|Rest],
        is_variable(Args),!,
        Rest1=..Rest,
        is_type(Rest1),!,
        variablesInType(Rest1,[Args|List_Variables_In],List_Variables_Out).

[blili]

Mais il reste un petit probleme.

le programme qu'on a traite juste le cas ou le premier argument est une variable, mais si le premier argument de Type est sous la forme (-> ou pii) alors il ne renvoie aucun resultat.

par exemple, si on veut tester:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
 
?- variables_In_Type(pii(X-1,X-4)->(X-2->X-3),L).

on doit avoir le résultat:
L=[X-1,X-4,X-2,X-3]

ou encore:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
 
variables_In_Type((X-1->X-4)->(X-2->X-3),L).

on doit obtenir le résultat suivant:

L=[X-1,X-4,X-2,X-3]

Merci.