Résolution d'équations fonctionnelles pour des fonctions inconnues dans le calcul lambda

Existe-t-il des techniques pour résoudre des équations fonctionnelles pour des fonctions inconnues dans le calcul lambda?

Supposons que la fonction d'identité soit définie de manière extensionnelle en tant que telle:

$I x = x$

(c'est-à-dire en écrivant une équation pour le comportement attendu de cette fonction) et maintenant je veux la résoudre pour en faisant une transformation algébrique pour obtenir la formule intensionnelle de cette fonction:$I$

$I = \lambda x.x$

qui indique exactement comment la fonction fait ce qui était attendu (c'est-à-dire comment l'implémenter dans le calcul lambda).

Bien entendu, la fonction d'identité n'est utilisée qu'à titre d'exemple. Je m'intéresse aux méthodes plus générales de résolution de telles équations. En particulier, je voudrais trouver une fonction qui réponde à l'exigence suivante:$B$

$B\;f\;(\lambda x.M) = (\lambda x.f M)$

c'est-à-dire "injecte" la fonction donnée dans la fonction lambda donnée avant son "corps" (qui est une expression lambda arbitraire), éventuellement en la démontant et en construisant une nouvelle, de sorte qu'elle devienne un paramètre auquel la fonction est appliquée.$f$$(\lambda x.M)$$M$$f$

Il s'agit d'un problème connu, connu sous le nom d' unification d'ordre supérieur .

Malheureusement, ce problème est indécidable en général. Il existe un fragment décidable, connu sous le nom de fragment de motif de Miller. Il est largement utilisé, entre autres, pour la vérification de type de programmes dépendants avec des métavariables ou la correspondance de modèles. Ce fragment est l'endroit où les variables d'unification ne sont appliquées qu'à des variables de programme liées distinctes.

Cet article fournit un excellent didacticiel sur le fonctionnement de l'unification d'ordre supérieur et en décrit une implémentation (relativement) simple.

Malheureusement, il ne semble pas que votre fonction tombe dans ce fragment de modèle. Cela dit, ce que je regarde est assez similaire à la composition des fonctions. La fonction suivante satisfait-elle votre propriété?

$B = \lambda f\ g\ x\ \ldotp f\ (g\ x)$

Nous avons:

• $B\ f\ (\lambda x . M)$
• $= B\ f\ (\lambda y . [y/x]M)$ par -équivalence$\alpha$
• $= \lambda x . f\ ((\lambda y. [y/x]M) x)$
• $= \lambda x . f\ ([x/y][y/x]M)$
• $= \lambda x . f\ M$

Je pense avoir une réponse partielle, concernant l'équation avec la fonction d'identité:

$I x = x$

Nous voulons le résoudre en trouvant la formule pour , qui sera de la forme avec une expression encore inconnue comme corps. Remplaçons-le par dans l'équation originale:( λ p . M ) M $I$$(\lambda p.M)$$M$$I$

$(\lambda p.M)\; x = x$

puis appliquez la fonction à sur le côté gauche:$x$

$M[p/x] = x$

Mais qu'avons-nous ici? :> Cette équation est la formule de l'expression que nous recherchons, après y avoir substitué chaque occurrence de par , et elle dit qu'elle devrait ressembler au côté droit après :) En d'autres termes, la fonction que nous recherchait c'est:p $M$$p$$x$

$I = (\lambda x.x)$

ce qui bien sûr est la bonne réponse :)

Essayons la même approche pour trouver la formule du combinateur . Nous voulons qu'il fonctionne de telle manière que, appliqué à lui-même, il se produise appliqué à lui-même:$\omega$

$\omega\;\omega = \omega\;\omega$

Maintenant, trouvons la formule pour qui est de la forme pour une expression encore inconnue . En substituant cela dans l'équation, nous obtenons:$\omega$$(\lambda x.M)$$M$

$(\lambda x.M)\;\omega = \omega\;\omega$

Son application au paramètre de gauche donne la formule de :$M$

$M [x/\omega] = \omega\;\omega$

Cela dit qu'après avoir substitué chaque occurrence de dans par cela a produit , donc nous pouvons déduire que l'expression originale avant la substitution aurait dû être , donc la fonction que nous cherchions devrait ressemble à ca:$x$$M$$\omega$$\omega\;\omega$$M$$x\;x$

$\omega = (\lambda x.x\;x)$

ce qui est effectivement le cas :)

J'ai le sentiment, cependant, que cela pourrait devenir si facile simplement parce que le côté droit était déjà dans la forme que nous recherchons.