Haskell: Évaluation des expressions lambda manuellement - déterminer les types généraux

Question

Tout d'abord, désolé si je ne publie pas ceci sur le bon site car je ne suis pas sûr qu'il s'agisse plus d'une question mathématique que d'une question de programmation, mais depuis J'utilise cela avec Haskell et en comparant les résultats avec un interprète Haskell, j'ai juste pensé que je le demanderais ici. Donc, j'essaie essentiellement d'évaluer les expressions lambda dans Haskell et je le fais manuellement (en préparation d'un examen, puisque je serai obligé de le faire sur papier). On me donne des expressions et je dois écrire leurs types généraux après leur évaluation. Pour ce faire, j'utilise un interprète pour obtenir une réponse quelque peu correcte.

En particulier, je vais évaluer les expressions suivantes:

t2 = (\x y z -> y.x.y); 
tx2 = (\x y z -> y.z.z); 
tp2 = (\x -> \y -> (x.y.x)); 
td2 = (\x y z f -> y(z(z(f)))); 
tm2 = (\z -> \y -> \x -> z.y.x); 

Depuis que je ne comprends pas 100% comment faire, je l'ai conçu une méthode. Tout d'abord, je crée un modèle qui ressemble un peu à l'apparence de l'expression évaluée. C'EST À DIRE. si une partie de la variable de taille gauche ('lambda'd') est présente sur le côté droit (car c'est à peu près la composition fonctionnelle dans tous les cas), c'est une fonction. Sinon, c'est juste une variable. Par la suite, j'essaie d'adapter le mieux possible les types généraux de fonctions et j'obtiens des résultats semi-corrects, mais je suis sûr que je fais encore quelques erreurs. Voici tout mon processus d'évaluation:

t2 = (\x y z -> y.x.y); 

(_ -> _) -> (_ -> _) -> c -> _ -> _ 

y(x(y)) 
assume: 
y :: a -> b 
x :: b -> a 

result: (b -> a) -> (a -> b) -> c -> a -> b 
interpreter: (a -> b) -> (b -> a) -> c -> b -> a 

z ne figure pas sur le côté droit, il est donc pas une fonction dans ce cas. Je l'attribue c. Maintenant, je regarde la composition du côté droit. Je vais de droite à gauche et j'attribue un -> b à y puisque je n'ai aucune idée de son entrée ou de sa sortie. Puisque x utilise le résultat de y comme entrée, et y utilise de nouveau x 'comme entrée, x est b -> a. Ce que je peux simplement insérer dans mon modèle. Comme vous pouvez le voir, ce n'est pas exactement le même résultat que celui obtenu par l'interpréteur, mais c'est seulement a et b qui sont inversés, donc cela ne semble pas être faux.

tx2 = (\x y z -> y.z.z); 

a -> (_ -> _) -> (_ -> _) -> _ -> _ 

y(z(z)) 
assume: 
z :: b -> b 
y :: b -> c 

result: a -> (b -> c) -> (b -> b) -> b -> c 
interpreter: a -> (b -> c) -> (b -> b) -> b -> c 

Identique à ci-dessus. Puisque z s'utilise dans la composition fonctionnelle, je suppose qu'il a les mêmes entrées et sorties. y utilise la sortie de z comme entrée et a une sortie inconnue, d'où c. Cela semble correspondre à mon interprète.

tp2 = (\x -> \y -> (x.y.x)); 

(_ -> _) -> (_ -> _) -> _ -> _ 

x(y(x)) 
assume: 
x :: a -> b 
y :: b -> a 

result: (a -> b) -> (b -> a) -> a -> b 
interpreter: (a -> b) -> (b -> a) -> a -> b 

À peu près la même chose que le premier exemple, seulement je n'ai pas de variable lambda inutilisée.

td2 = (\x y z f -> y(z(z(f)))); 

a -> (_ -> _) -> (_ -> _) -> (_ -> _) -> _ -> _ 

y(z(z(f))) 
assume: 
f :: _ -> b 
z :: b -> b 
y :: b -> c 

assume: a -> (b -> c) -> (b -> b) -> (_ -> b) -> b -> c 
result: a -> (b -> c) -> (b -> b) -> (b -> b) -> b -> c 
interpreter: a -> (b -> c) -> (b -> b) -> b -> c 

Tout sauf x est une fonction dans ce cas. L'entrée de f n'est pas initialement connue de moi et je la laisse juste vide à ce moment-là. z utilise la sortie de f et sa propre sortie dans la composition, donc je lui assigne juste b -> b. y utilise la sortie de z, et a une sortie inconnue elle-même, donc elle obtient b -> c. Maintenant, je l'insère dans mon modèle, mais il me manque encore une entrée pour f. Puisqu'il y a un b juste après f, je suppose simplement qu'il utilise b comme une entrée, aussi. Maintenant, il y a la première vraie question: où est-ce que f a disparu dans la réponse donnée par l'interprète? Je ne peux que supposer, car il utilise la même entrée/sortie que z et c'est fondamentalement en composition avec ça, ça s'est simplement simplifié en un seul b-> b, mais je n'en suis pas sûr.

tm2 = (\z -> \y -> \x -> z.y.x); 
tm2 = (\z y x -> z.y.x); 

(_ -> _) -> (_ -> _) -> (_ -> _) -> _ -> _ 

z(y(x)) 
assume: 
x = a -> b 
y = b -> _ 
z = _ -> _ 

assume: (_ -> _) -> (b -> _) -> (a -> b) -> _ -> _ 
result?: (a -> c) -> (b -> a) -> (a -> b) -> a -> c 
interpreter: (a -> b) -> (c -> a) -> (d -> c) -> d -> b 

est ici où tout se désagrège: z, y et x sont des fonctions. Donc j'attribue juste un -> b à x, ce qui signifie que l'entrée de y est b. La sortie est inconnue pour moi en ce moment. Idem pour z, puisque je n'ai aucune idée de la sortie de y. Donc, après que je les ai entré dans mon modèle, la seule chose qui me reste à faire est simplement de remplir les blancs pour les valeurs inconnues. Puisque x nécessiterait une entrée as, cela signifie qu'il y a un a juste après. Ce qui voudrait dire que c'est la contribution de z, aussi. Puisque c'est l'entrée de z, je peux supposer que c'est la sortie de y. La seule chose qu'il me reste à remplir est la sortie de z, et je lui donne juste un c puisque je ne sais pas vraiment ce que ça pourrait être. Comme vous pouvez le voir, ce n'est pas du tout ce que l'interprète me donne, du moins, c'est ce que l'interprète me donne. Bien que le côté gauche soit encore assez similaire, je ne comprends pas du tout ce qui se passe du côté droit. Pourquoi est-ce d -> b? Ne devrait-il pas être tout ce qui est le résultat de (z (y (x))), qui devrait avoir l'entrée/sortie de z?

Merci d'avance pour toute aide que vous pourriez m'offrir.

Answer 1

Il y a trois propriétés de base que vous pouvez exploiter:

1. En raison de taitement, \x y -> z est équivalent à \x -> \y -> z.
2. Pour tout x(y), vous savez que x doit être une fonction et son premier argument correspond au type de l'expression y. Vous connaissez le type ., qui est (b -> c) -> (a -> b) -> a -> c. En outre, . est associatif à droite (c'est-à-dire a.b.c est le même que a.(b.c)). Avec cela à l'esprit

, pensez à votre premier exemple:

t2 = (\x y z -> y.x.y); 

De toute évidence, il est fonction de trois arguments, de sorte que son type sera quelque chose de semblable à

t2 :: ty0 -> ty1 -> ty2 -> ty3 

J'utilise ty0 par ty3 ici pour désigner les types à déduire. ty0 est le type de l'argument x, ty1y est destiné, ty2 pour z et ty3 est le type de la valeur de résultat (à savoir le type de l'expression y.x.y).

Je commencerais par la détermination du type ty3 (qui est défini par l'expression y.x.y) parce que tout en faisant, vous trouverez également les types de utilisés arguments. arguments non utilisés peuvent avoir tout type:

1. y.x.y est équivalent à y.(x.y) (en raison de droit associativité de ., voir point 3 ci-dessus). Donc, vous pouvez commencer en considérant la sous-expression x.y.
2. Cela signifie que x :: (b -> c) et y :: (a -> b) et par conséquent x.y :: a -> c (en raison du type de ., voir à nouveau # 3 ci-dessus). Nous savons donc que y :: (a -> b) et x.y :: a -> c. En gardant cela à l'esprit, la seule façon de vérifier le type y.(x.y) (c'est-à-dire correspondre au type de .) est lorsque c ~ a, c'est-à-dire c et a sont du même type.

Par conséquent, x :: b -> a (notre ty0!) Et y :: a -> b( ty1 ) and y (x.y) :: a -.> B (what we called ty3` ci-dessus). Vous pouvez le brancher dans notre "type de fonction à trois arguments" primitif ci-dessus.

t2 :: ty0 -> ty1 -> ty2 -> ty3 
=> 
t2 :: (b -> a) -> (a -> b) -> ty2 -> (a -> b) 

... et depuis -> est associatif à droite, vous pouvez omettre les derniers parens (et au lieu de ty2 vous auriez pu utiliser c, bien sûr).

Essayons la même stratégie sur votre dernier exemple:

tm2 = (\z -> \y -> \x -> z.y.x); 

1. Cela équivaut à \z y x -> z.y.x (en raison de taitement, voir # 1 dans la liste en haut).
2. Cela signifie qu'il s'agit d'une autre fonction à trois arguments de la forme tm2 :: ty0 -> ty1 -> ty2 -> ty3. Encore une fois, nous commençons par inférer le type ty3 en considérant la définition de la fonction.
3. Le type ty3 est le type de l'expression z.y.x, ce qui équivaut à z.(y.x) (en raison de l'associativité à droite de .).
4. Les trois variables doivent être des fonctions pour satisfaire le type de . (voir # 3 dans la liste en haut).
5. Donc x :: a -> b, y :: b -> c, y.x :: a -> c. De cela, il s'ensuit que z :: c -> d et par conséquent z.y.x :: a -> d.

Depuis z est le premier argument de tm2, y est la deuxième et x est le troisième argument, vous pouvez dire que

tm2 :: (c -> d) -> (b -> c) -> (a -> b) -> (a -> d)