Discussion :

[Trap D]

Connaissez vous le mode trace en Prolog, cela permet de suivre le déroulement des prédicats et voir où il y a des problèmes.
En SWI-Prolog, il suffit de taper gtrace dans la console Prolog.

Les deux prédicats échouent car

• pii(X-1,X-4) echoue a is_variable(Args) pour le premier
• X-1->X-4 echoue a is_variable(Args) pour le second

Il faut retravailler is_variable

[blili]

oui, j'ai utilisé trace pour repérer ou est ce que ça bloque, donc pour regler ça j'ai modifier le code comme suit:

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_In,List_Variables_Out):-
                       type_fleche(Type),!,
                       Type=..[_Symbol|Arguments],
                       Arguments=[Arg1|Rest],
                       is_type(Arg1),
                       is_variable(Arg1),
                       Rest1=..Rest,
                       is_type(Rest1),!,
            variablesInType(Rest1,[Arg1|List_Variables_In],List_Variables_Out)
                      ;
                       %sinon si le premier argument n'est pas une variable;
                       type_fleche(Arg1),
                       variablesInType(Arg1,List_Variables_In,List_Variables_Out)
                       ;
                       type_qant(Arg1),
                       variablesInType(Arg1,List_Variables_In,List_Variables_Out).

mais cela ne règle pas le problème et il n'affiche toujours pas le résultat attendu.

[blili]

Bonjour a tous,

j'ai un petit problème avec la substitution des termes, après avoir fait la substitution des types, il faut faire la même chose avec les termes.

La présentation des termes est comme suit:

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
33
34
35
36
37
38
39
40
41
42
 
%variable de terme x:T
 
is_variable_term(X,T):-
                var(X),
                is_type(T).
 
%constantes de terme c:T
 
is_cst_term(C,T):-
             atomic(C),
             is_type(T).
 
%les termes en general
 
is_term(M,T):-
          is_variable_term(M,T).
 
is_term(M,T):-
          is_cst_term(M,T).
 
%abstraction
is_term(lam((X,A),(N,B)),(A->B)):-
              is_variable_term(X,A),
              is_term(N,B),
              is_type(A->B).
 
%application
is_term(appl((M,U->T),(N,U)),T):-
           is_term(M,U->T),
           is_term(N,U).
 
%abstraction de type
is_term(lam_type(X,(N,A)),(pii(X,A))):-
           is_variable(X),
           is_term(N,A),
           is_type(pii(X,A)).
 
%application de type: 
is_term(appl_type((N,pii(X,Y)),U),Y):-
           is_term(N,pii(X,Y)),
           is_type(U).

le but est de faire la substitution d'une variable par un terme et cela dans tous les cas possibles (le cas d'une variable, constante, application, abstraction, application de type et abstraction de type).

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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
 
 
%substitution_term((X,T),(Y,T),(Term,Type),(Term_final,Type)) est vrai si Term_final est le résultat de la substitution de X par Y dans Term
 
%le cas d'une variable
substitution_term((X,T),(Y,T),(Term,Type),(Term_final,Type)):-
               is_variable_term(Term,Type),
               Term==X,!,
               Term_final=Y.
 
substitution_term((X,T),(Y,T),(Term,Type),(Term_final,Type)):-
               is_variable_term(Term,Type),
               Term_final=Term,!.
 
%le cas d'une constante
substitution_term((X,T),(Y,T),(Term,Type),(Term_final,Type)):-
              is_cst_term(Term,Type),
              Term_final=Term.
 
%le cas d'une application
substitution_term((X,T),(Y,T),(appl((M,U->T),(N,U)),T),(Term_final,Type)):-
             is_type(U->T),
             substitution(T,T,U->T,Type_final1),
             substitution_term((X,T),(Y,T),(M,Type_final1),(Term_final1,Type1)),
             substitution_term((X,T),(Y,T),(N,U),(Term_final2,Type2)),
             Term_final=(appl((Term_final1,Type1),(Term_final2,Type2))).
 
%le cas d'une abstraction
%le cas ou X==Z
substitution_term((X,T),(Y,T),(lam((Z,T),(N,B)),(T->B)),(Term_final,Type)):-
                   X==Z,!,
                   Term_final=lam((Z,T),(N,B)).
 
%le cas ou X=/=Z  et Z appartient a Y 
substitution_term((X,T),(Y,T),(lam((Z,T),(N,B)),(T->B)),(Term_final,Type)):-
                   %le prob est la, comment verifier si Z appartient a Y?
 
                   member(Z,Y),!,
                   variables_In_Term((lam((Z,T),(N,B)),(T->B)),L),
 
     %un autre probleme la, comment verifier que W n'appartient pas a L:
                   not(member((W,T),L)),
 
     %renommer Z par W dans Term1 de Type1 pour obtenir Term2 de Type2
 
                   substitution_term((Z,T),(W,T),(Term1,Type1),(Term2,Type2)),
                   substitution_term((X,T),(Y,T),Term2,Type2,(Term_final,Type)).

tout fonctionne bien dans le cas d'une variable, constante ou une application, mais le problème est dans le cas d'une abstraction, comment vérifier si Z appartient a Y? et comment vérifier si W n'appartient pas a L, on veut renommer avec une variable qui n’existe pas dans la liste des variables L?

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

Merci d'avance.

[Trap D]

Bonjour

J'ai commencé à regarde le code seulement aujourd'hui, je pense qu'i a du évoluer depuis qu'il a été posté, ais je mais quand même quelques commentaires
A la compil, sous SWI-Prolog remarque que plusieurs varialbes sont des singletons, ce qui signifie qu"'elles ne sont pas utilisées, volontaire ou erreur ?

Dans les prédicats substitution_term 2 et 3 du code précédent :
substitution_term((X,T),(Y,T),(Term,Type),(Term_final,Type)):-

substitution_term((X,T),(Y,T),(appl((M,U->T),(N,U)),T),(Term_final,Type)):-

substitution_term((X,T),(Y,T),(lam((Z,T),(N,B)),(T->B)),(Term_final,Type)):-

D'autre part le code de substitution(T,T,U->T,Type_final1), et de variables_In_Term((lam((Z,T),(N,B)),(T->B)),L),

Enfin, il faut donner un exemple des diificultés rencontrées c'est-àdire, l'appel d'iun prédicat avec le résultat attendu.

Bon courage.

[blili]

Bonjour,

Merci pour votre réponse.

Effectivement le code a beaucoup évolué depuis la dernière fois.

substitution_term((X,T),(Y,T),(Term,Type),(Term_final,Type)):-

le but est de remplacer X par Y dans Term pour avoir comme résultat Term_final.

dans cette substitution, on ne gère pas les types:

substitution_term((X,T),(Y,T),(appl((M,U->T),(N,U)),T),(Term_final,Type)):-

substitution_term((X,T),(Y,T),(lam((Z,T),(N,B)),(T->B)),(Term_final,Type)):-

pour ce qui concerne la substitution dans lam,

D'autre part le code de substitution(T,T,U->T,Type_final1), et de variables_In_Term((lam((Z,T),(N,B)),(T->B)),L),

le code est modifié et on ne prend pas compte les types.

Pour cette partie du code, je pense que j'ai des problèmes au niveau de l'algorithme de substitution que je dois revoir pour terminer son implémentation.