Rozwiązywanie równań funkcyjnych dla nieznanych funkcji w rachunku lambda

Czy są jakieś techniki rozwiązywania równań funkcyjnych dla nieznanych funkcji w rachunku lambda?

Załóżmy, że mam funkcję tożsamości zdefiniowaną jako taką:

$I x = x$

(czyli przez spisanie równanie dla oczekiwanego zachowania tej funkcji), a teraz chcę go rozwiązać za wykonując jakąś transformację algebraicznym uzyskać intensional formułę dla tej funkcji:$I$

$I = \lambda x.x$

mówi, jak dokładnie funkcja wykonuje to, czego oczekiwano (to znaczy, jak zaimplementować ją w rachunku lambda).

Oczywiście funkcja tożsamości jest używana tylko jako przykład. Interesują mnie bardziej ogólne metody rozwiązywania takich równań. W szczególności chciałbym znaleźć funkcję która spełnia następujące wymagania:$B$

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

to znaczy „wstrzykuje” daną funkcję do podanej funkcji lambda przed jej „ciałem” (co jest pewnym arbitralnym wyrażeniem lambda), być może przez rozebranie jej i skonstruowanie nowej, tak aby stała się parametr, do którego stosowana jest funkcja .$f$$(\lambda x.M)$$M$$f$

Jest to znany problem, znany jako unifikacja wyższego rzędu .

Niestety ten problem jest ogólnie nierozstrzygalny. Jest rozstrzygalny fragment, znany jako Fragment Wzoru Millera. Jest szeroko stosowany, między innymi, do sprawdzania typów programów zależnie wpisywanych z metawetami lub dopasowywaniem wzorców. W tym fragmencie zmienne unifikacyjne są stosowane tylko do wyraźnie powiązanych zmiennych programu.

Ten papier stanowi świetny samouczek na temat tego, jak działa ujednolicenie wyższego rzędu, i przedstawia (stosunkowo) jego prostą implementację.

Niestety nie wygląda na to, aby twoja funkcja mieściła się w tym fragmencie wzorca. To powiedziawszy, to, co widzę, jest bardzo podobne do składu funkcji. Czy poniższa funkcja spełnia twoje wymagania?

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

Mamy:

• $B\ f\ (\lambda x . M)$
• przezrównoważność$= B\ f\ (\lambda y . [y/x]M)$$\alpha$
• $= \lambda x . f\ ((\lambda y. [y/x]M) x)$
• $= \lambda x . f\ ([x/y][y/x]M)$
• $= \lambda x . f\ M$

Myślę, że mam częściową odpowiedź dotyczącą równania z funkcją tożsamości:

$I x = x$

Chcemy go rozwiązać, znajdując wzór na , który będzie miał postać ( λ p . M ) z pewnym nieznanym jeszcze wyrażeniem M jako jego ciałem. Zastąpmy to ja w pierwotnym równaniu:$I$$(\lambda p.M)$$M$$I$

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

następnie zastosuj funkcję do po lewej stronie:$x$

$M[p/x] = x$

Ale co tu mamy? :> To równanie jest wzorem dla wyrażenia , którego szukamy, po podstawieniu każdego wystąpienia p w nim x , i mówi, że powinno ono wyglądać jak prawa strona :) Innymi słowy, funkcja szukaliśmy to:$M$$p$$x$

$I = (\lambda x.x)$

która oczywiście jest poprawną odpowiedzią :)

Wypróbujmy to samo podejście, aby znaleźć wzór na kombinator . Chcemy, aby działał w taki sposób, aby po nałożeniu na siebie wytworzył się przyłożony do siebie:$\omega$

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

Teraz znaleźliśmy formułę , który ma postać ( λ x . M ) z jakiegoś nieznanego jeszcze ekspresji M . Podstawiając to do równania otrzymujemy:$\omega$$(\lambda x.M)$$M$

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

Zastosowanie go do parametru po lewej stronie daje wzór na :$M$

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

Oznacza to, że po podstawieniu każdego wystąpienia w M przez ω wytworzyło się$x$$M$$\omega$ , więc możemy wywnioskować, że oryginalne wyrażenie M przed podstawieniem powinno być$\omega\;\omega$$M$$x\;x$

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

co jest w rzeczywistości :)

Mam jednak wrażenie, że może być tak łatwo tylko dlatego, że prawa strona była już w takiej formie, jakiej szukamy.