<div class="notebook"> <div class="nb-cell markdown" name="md1"> # TP 4 Paradigmes 2022/2023 Valrose # Inférence de types en Prolog sujet : http://i3s.unice.fr/~elozes/enseignement/paradigmes/tp/tp4_inference_de_types_en_prolog/tp4.html ## Étape 1 ### Question 1.1 </div> <div class="nb-cell program" name="p1"> % CODE A GARDER SANS CHANGER! IL EST VALABLE UNIQUEMENT DANS LE DEBUT DU NOTEBOOK % (ICONE "GOOGLE MAPS" A DROITE) % Axiome type([X, Alpha | _], X, Alpha). % Affaiblissement type([X, Alpha | Gamma], E, Tau) :- type(Gamma, E, Tau). % Intro -> type(Gamma, fun(X,E), arrow(Tau1,Tau2)) :- type([X, Tau1 | Gamma], E, Tau2). % Elim -> type(Gamma, app(E1, E2), Tau) :- type(Gamma, E1, arrow(Tau2, Tau)), type(Gamma, E2, Tau2). </div> <div class="nb-cell html" name="htm1"> </div> <div class="nb-cell markdown" name="md2"> #### Question 1.1 - vérifier le type d'une expression Le terme Prolog `fun(x,fun(y,app(y, x)))` représente l'expression Caml `fun x -> fun y -> y x` . Trouvez son type avec Caml. Ce type se modélise par le terme Prolog arrow(Alpha,arrow(arrow(Alpha,Beta),Beta)). Vérifiez que la requête </div> <div class="nb-cell query" data-tabled="true" name="q1"> type([], fun(x,fun(y,app(y, x))), arrow(Alpha,arrow(arrow(Alpha,Beta),Beta))). </div> <div class="nb-cell markdown" name="md3"> termine avec succès (on utilise le programme Prolog pour **vérifier** un type). #### Question 1.2 - inférer le type d'une expression Quel terme représente l'expression ci-dessous? ```OCaml (fun x -> x (fun y -> y)) (fun z -> z) (fun t -> t) ``` À l'aide d'une requête appropriée, calculez son type avec Prolog, et vérifiez le résultat avec Caml (on utilise le programme pour **inférer** un type). </div> <div class="nb-cell query" data-tabled="true" name="q2"> </div> <div class="nb-cell markdown" name="md4"> ## Étape 2 - le fragment fonctionnel, en mieux Si vous ne parvenez pas à faire cette étape, vous pouvez quand même faire les étapes suivantes. #### Question 2.1 - unification avec occurs check Corrigez l'axiomatisation à l'aide du prédicat `unify_with_occurs_check/2`. **Indication**: *lisez rapidement* [ceci](http://www.let.rug.nl/bos/lpn//lpnpage.php?pagetype=html&pageid=lpn-htmlse5), en particulier la partie sur *occurs check* </div> <div class="nb-cell program" data-background="true" name="p2"> % CODE A MODIFIER! IL EST VALABLE DANS TOUTE LA SUITE DU NOTEBOOK (ICONE "PLANISPHERE" A DROITE) % Axiome type([X, Alpha | _], X, Alpha). % Affaiblissement type([X, Alpha | Gamma], E, Tau) :- type(Gamma, E, Tau). % Intro -> type(Gamma, fun(X,E), arrow(Tau1,Tau2)) :- type([X, Tau1 | Gamma], E, Tau2). % Elim -> type(Gamma, app(E1, E2), Tau) :- type(Gamma, E1, arrow(Tau2, Tau)), type(Gamma, E2, Tau2). </div> <div class="nb-cell markdown" name="md27"> Test: vérifiez que la requête ci-dessous échoue </div> <div class="nb-cell query" data-tabled="true" name="q23"> type([], fun(x, app(x, x)), Tau). </div> <div class="nb-cell markdown" name="md5"> #### Question 2.2 - analyse du problème avec les variables introduites plusieurs fois Inférez le type de l'expression ```OCaml fun x -> fun x -> x x ``` et observez que, comme mentioné dans le cours, Prolog parvient à typer cette expression, mais pas Caml. </div> <div class="nb-cell query" data-tabled="true" name="q3"> </div> <div class="nb-cell markdown" name="md6"> #### Question 2.3 - correction du problème Corrigez la règle d'affaiblissement pour ne pas avoir besoin de supposer que l'expression à typer n'introduit jamais deux fois la même variable avec `fun`. Idée: on n'applique pas la règle d'affaiblissement lorsque la règle d'axiome a échoué parce que les types n'étaient pas unifiables: si on a $\Gamma,x:\tau_1\vdash x:\tau_2$ et qu'on ne parvient pas à unifier $\tau_1$ et $\tau_2$, alors l'expression n'est pas typable, il ne faut pas aller chercher plus loin dans $\Gamma$, puisque s'il y a d'autres déclarations de types pour $x$ dans $\Gamma$, ce sont des $x$ qui sont "masqués" par le $x$ actuel. **TODO** corrigez le code à la question 2.1 </div> <div class="nb-cell markdown" name="md7"> ## Étape 3 - les couples #### Question 3.1 - axiomatisation des couples Ajoutez trois règles (ou axiomes) Prolog à la définition de la relation `type`. </div> <div class="nb-cell program" data-background="true" name="p3"> type(Gamma, fst, ...) :- ... type(Gamma, snd, ...) :- ... type(Gamma, couple(E1, E2), ...) :- ... </div> <div class="nb-cell markdown" name="md8"> #### Question 3.2 - test Testez votre code avec les requêtes suivantes </div> <div class="nb-cell query" data-tabled="true" name="q4"> type([], fst, Tau). </div> <div class="nb-cell markdown" name="md9"> renvoie Tau = arrow(product(Alpha1, Alpha2), Alpha1) </div> <div class="nb-cell query" data-tabled="true" name="q5"> type([], snd, Tau). </div> <div class="nb-cell markdown" name="md10"> renvoie Tau = arrow(product(Alpha1, Alpha2), Alpha2) </div> <div class="nb-cell query" data-tabled="true" name="q6"> type([], fun(x, couple(x, x)), Tau). </div> <div class="nb-cell markdown" name="md28"> renvoie Tau = arrow(Alpha,product(Alpha, Alpha)) </div> <div class="nb-cell query" data-tabled="true" name="q24"> type([], fun(x, couple(app(snd, x), app(fst, x))), Tau). </div> <div class="nb-cell markdown" name="md11"> renvoie Tau = arrow(product(Alpha1,Alpha2),product(Alpha2, Alpha1) </div> <div class="nb-cell markdown" name="md12"> #### Question 3.3 - test avancé Cherchez plusieurs (au moins deux) expressions Caml (dans la grammaire ci-dessus) qui ne sont pas typables. Vérifiez avec les requêtes Prolog correspondantes que l'expression n'est effectivement pas typable. </div> <div class="nb-cell query" data-tabled="true" name="q7"> </div> <div class="nb-cell query" data-tabled="true" name="q8"> </div> <div class="nb-cell query" data-tabled="true" name="q9"> </div> <div class="nb-cell query" data-tabled="true" name="q10"> </div> <div class="nb-cell markdown" name="md13"> ## Étape 4 - micro Caml #### Question 4.1 - axiomatisation de micro Caml Étendez l'axiomatisation de la relation `type` pour prendre en compte micro Caml. </div> <div class="nb-cell program" data-background="true" name="p4"> </div> <div class="nb-cell markdown" name="md14"> #### Question 4.2 - test Testez votre code sur les expressions Caml suivantes; vérifiez votre résultat avec Caml, toutes les expression ci-dessous ne sont pas typables, votre code doit inférer le type quand il est inférable, et déclarer l'expression non typable lorsqu'elle n'est pas typable. </div> <div class="nb-cell markdown" name="md15"> ```OCaml fun x -> x=1 ``` </div> <div class="nb-cell query" data-tabled="true" name="q11"> </div> <div class="nb-cell markdown" name="md16"> ```OCaml fun x -> fun y -> x=y ``` </div> <div class="nb-cell query" data-tabled="true" name="q12"> </div> <div class="nb-cell markdown" name="md17"> ```OCaml fun x -> x=x+x ``` </div> <div class="nb-cell query" data-tabled="true" name="q13"> </div> <div class="nb-cell markdown" name="md18"> ```OCaml fun x -> fun y -> fun z -> if x then y else z ``` </div> <div class="nb-cell query" data-tabled="true" name="q14"> </div> <div class="nb-cell markdown" name="md19"> ```OCaml fun x -> if x then x else true ``` </div> <div class="nb-cell query" data-tabled="true" name="q15"> </div> <div class="nb-cell markdown" name="md20"> ```OCaml fun x -> if x then x else 1 ``` </div> <div class="nb-cell query" data-tabled="true" name="q16"> </div> <div class="nb-cell markdown" name="md21"> ```OCaml fun x -> x () ``` </div> <div class="nb-cell query" data-tabled="true" name="q17"> </div> <div class="nb-cell markdown" name="md22"> ```OCaml fun x -> fun y -> ( x; y ) ``` </div> <div class="nb-cell query" data-tabled="true" name="q18"> </div> <div class="nb-cell markdown" name="md23"> ```OCaml fun x -> fun y -> if x then ( y (); 1 ) else 2 ``` </div> <div class="nb-cell query" data-tabled="true" name="q19"> </div> <div class="nb-cell markdown" name="md25"> ```OCaml fun x -> fun y -> if x then y () ``` </div> <div class="nb-cell query" data-tabled="true" name="q21"> </div> <div class="nb-cell markdown" name="md26"> ```OCaml fun x -> if x then x () ``` </div> <div class="nb-cell query" data-tabled="true" name="q22"> </div> </div>