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ą:
(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:
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:
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 .
źródło
Myślę, że mam częściową odpowiedź dotyczącą równania z funkcją tożsamości:
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 (λp.M) M I
następnie zastosuj funkcję do po lewej stronie: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
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:ω
Teraz znaleźliśmy formułę , który ma postać ( λ x . M ) z jakiegoś nieznanego jeszcze ekspresji M . Podstawiając to do równania otrzymujemy:ω (λx.M) M
Zastosowanie go do parametru po lewej stronie daje wzór na :M
Oznacza to, że po podstawieniu każdego wystąpienia w M przez ω wytworzyło sięx M ω , więc możemy wywnioskować, że oryginalne wyrażenie M przed podstawieniem powinno być xωω M xx
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.
źródło