Czyste, intuicyjne wyprowadzenie kombinatora stałoprzecinkowego (kombinator Y)?

28

Kombinator stałoprzecinkowy FIX (znany również jako kombinator Y) w (niepoprawnym) rachunku lambda ( ) jest zdefiniowany jako: $\lambda$

FIX $\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y. x~x~y))$

Rozumiem jego cel i doskonale mogę śledzić wykonanie jego aplikacji; Chciałbym zrozumieć, jak wyprowadzić FIX z pierwszych zasad .

Oto, o ile mi się podoba, gdy próbuję to uzyskać:

FIX to funkcja: FIX $\triangleq \lambda_\ldots$
FIX przyjmuje inną funkcję, $f$ , aby była rekurencyjna: FIX $\triangleq \lambda f._\ldots$
Pierwszym argumentem funkcji $f$ jest „nazwa” funkcji, używana tam, gdzie przewidziana jest aplikacja rekurencyjna. Dlatego wszystkie wyglądy pierwszego argumentu na $f$ powinny być zastąpione przez funkcję, a ta funkcja powinna oczekiwać reszty argumentów $f$ (załóżmy, że $f$ przyjmuje jeden argument): FIX $\triangleq \lambda f._\ldots f~(\lambda y. _\ldots y)$

W tym miejscu nie wiem, jak „zrobić krok” w moim rozumowaniu. Małe elipsy wskazują, gdzie brakuje mojego FIXa (chociaż mogę to wiedzieć tylko przez porównanie z „prawdziwym” FIXem).

Przeczytałem już Typy i języki programowania , które nie próbują wyprowadzić ich bezpośrednio, a zamiast tego odsyłają czytelnika do The Little Schemer w celu uzyskania pochodnej. Też to przeczytałem, a jego „wyprowadzenie” nie było tak pomocne. Co więcej, jest to w mniejszym stopniu bezpośrednie wyprowadzenie, a bardziej wykorzystanie bardzo specyficznego przykładu i próba ad-hoc napisania odpowiedniej funkcji rekurencyjnej w $\lambda$ .

computability logic programming-languages lambda-calculus combinatory-logic BlueBomber
źródło

1

Ten post może być pomocny. Ogólnie rzecz biorąc, myślę, że samo przejrzenie i obliczenie kilku iteracji kombinacji jest pomocne w ustaleniu, dlaczego to działa.

Xodarap

2

Istnieje kilka różnych kombinacji stałych punktów. Być może ludzie po prostu bawili się kombinatorami, dopóki się na nich nie natknęli.

Yuval Filmus

@YuvalFilmus, właśnie takie są moje badania i odpowiedź na to pytanie. Ale nadal uważam, że pouczające byłoby „zobaczenie” logicznego kształtowania kombinatora (ów), umiejętność, która byłaby szczególnie pomocna, np. Podczas próby zbudowania nowego kombinatora.

BlueBomber

Przeczytaj rozdział 9 w „The Little Lisper” Daniela P. Friedmana (lub „The Little Schemer”).

user18199

2

OP wydaje się wskazywać, że już to przeczytali.

Raphael

29

Nigdzie tego nie czytałem, ale wierzę, że można było wyprowadzić: $Y$

Niech będzie funkcja rekurencyjna , być może silnia lub coś podobnego. Nieformalnie definiujemy jako termin pseudo-lambda, gdzie występuje w jego własnej definicji: $f$ $f$ $f$

f = \dots f \dots f \dots

$f = \ldots f \ldots f \ldots$

Po pierwsze, zdajemy sobie sprawę, że wywołanie rekurencyjne może zostać uwzględnione jako parametr:

f = \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} f

$f = \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M} f$

Teraz moglibyśmy zdefiniować , gdybyśmy tylko mieli sposób, aby przekazać to jako argument sam w sobie. Nie jest to oczywiście możliwe, ponieważ nie mamy pod rękąCo mamy pod ręką jest . Ponieważ zawiera wszystko, co potrzebne do zdefiniowania , możemy spróbować przekazać jako argument zamiast i spróbować zrekonstruować z niego później w środku. Nasza pierwsza próba wygląda następująco: $f$ $f$ $M$ $M$ $f$ $M$ $f$ $f$

f = \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}}

$f = \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M} \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}$

Nie jest to jednak do końca poprawne. Wcześniej, , ale podstawiony przez w środku . Ale teraz zamiast tego mijamyMusimy jakoś naprawić wszystkie miejsca, w których używamy tak, aby zrekonstruować od . W rzeczywistości nie jest to wcale trudne: teraz, gdy wiemy, że , wszędzie, gdzie używamy , po prostu zastępujemy go przez . $f$ $r$ $M$ $M$ $r$ $f$ $M$ $f = M M$ $r$ $(r r)$

f = \underset{M^{'}}{\underset{⏟}{(λ r . (\dots (r r) \dots (r r) \dots))}} \underset{M^{'}}{\underset{⏟}{(λ r . (\dots (r r) \dots (r r) \dots))}}

$f = \underbrace{(\lambda r . (\ldots (rr) \ldots (rr) \ldots))}_{M'} \underbrace{(\lambda r . (\ldots (rr) \ldots (rr) \ldots))}_{M'}$

To rozwiązanie jest dobre, ale musieliśmy zmienić wewnątrz. To nie jest zbyt wygodne. Możemy to zrobić bardziej elegancko bez konieczności modyfikowania , wprowadzając inny który wysyła do jego argument dotyczy samego siebie: Wyrażając jako otrzymujemy $M$ $M$ $\lambda$ $M$ $M'$ $\lambda x.M(xx)$

f = (λ x . \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} (x x)) (λ x . \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} (x x))

$f = (\lambda x.\underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}(xx)) (\lambda x.\underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}(xx))$

W ten sposób, gdy jest podstawione na , jest podstawione na , co z definicji jest równe . To daje nam nierekurencyjną definicję , wyrażoną jako prawidłowy termin lambda! $M$ $x$ $MM$ $r$ $f$ $f$

Przejście do jest teraz łatwe. Możemy wziąć dowolny termin lambda zamiast i wykonać na nim tę procedurę. Możemy więc wyliczyć i zdefiniować $Y$ $M$ $M$

Y = λ m . (λ x . m (x x)) (λ x . m (x x))

$Y = \lambda m . (\lambda x. m(xx)) (\lambda x.m(xx))$

Rzeczywiście, zmniejsza się do jak to zdefiniowaliśmy. $Y M$ $f$

Uwaga: Wyprowadziłem zgodnie z definicją w literaturze. Syntezatora już opisany jest wariant dla call-by-value językach, czasami nazywany też . Zobacz ten artykuł w Wikipedii . $Y$ $Y$ $Z$

Petr Pudlák
źródło

1

Brakujące-ale-pozornie oczywiste, intuicja, że doskonała odpowiedź dał mi to, że rekurencyjna funkcja wymaga się jako argument, więc zacząć od założenia, że funkcja będzie mieć postać dla pewnego . Następnie, konstruując , wykorzystujemy to twierdzenie, że jest zdefiniowane jako zastosowanie czegoś do siebie wewnętrznie w , np. Zastosowanie do w twojej odpowiedzi, która z definicji jest równa . Fascynujący!

f = X (X)

$f = X (X)$

X

$X$

X

$X$

f

$f$

X

$X$

x

$x$

x

$x$

f

$f$

BlueBomber

11

Jak zauważył Yuval, nie ma tylko jednego operatora punktu stałego. Dużo ich. Innymi słowy, równanie dla twierdzenia o punkcie stałym nie ma jednej odpowiedzi. Nie można więc uzyskać od nich operatora.

To tak, jakby zapytać, jak ludzie wyprowadzają jako rozwiązanie dla . Oni nie! Równanie nie ma unikalnego rozwiązania. $(x,y)=(0,0)$ $x=y$

Na wypadek, gdybyście chcieli dowiedzieć się, jak odkryto pierwsze twierdzenie o punkcie stałym. Powiem, że zastanawiałem się także, w jaki sposób wymyślili twierdzenia o punkcie stałym / rekurencji, kiedy je zobaczyłem. To wydaje się takie genialne. Szczególnie w formie teorii obliczalności. W przeciwieństwie do tego, co mówi Yuval, ludzie nie bawili się, dopóki czegoś nie znaleźli. Oto, co znalazłem:

O ile pamiętam, twierdzenie to pierwotnie wynika z SC Kleene. Kleene wymyślił pierwotne twierdzenie o stałym punkcie, ocalając dowód niespójności pierwotnego rachunku lambda Kościoła. Oryginalny rachunek lambda Kościoła cierpiał na paradoks typu Russel. Zmodyfikowany rachunek lambda uniknął problemu. Kleene przestudiował dowód niespójności, aby prawdopodobnie sprawdzić, czy zmodyfikowany rachunek lambda cierpiałby na podobny problem i przekształcił dowód niespójności w przydatne twierdzenie o zmodyfikowanym rachunku lambda. Poprzez swoją pracę dotyczącą równoważności rachunku lambada z innymi modelami obliczeń (maszyny Turinga, funkcje rekurencyjne itp.) Przeniósł go na inne modele obliczeń.

Jak uzyskać operatora, o który możesz zapytać? Oto jak o tym pamiętam. Twierdzenie o punkcie stałym dotyczy usuwania odniesienia do siebie.

Każdy zna kłamliwy paradoks:

Jestem legowiskiem.

Lub w bardziej lingwistycznej formie:

To zdanie jest fałszywe.

Teraz większość ludzi uważa, że problem z tym zdaniem dotyczy samego odniesienia. Nie jest! Odniesienia do siebie można wyeliminować (problem dotyczy prawdy, język nie może mówić ogólnie o prawdziwości własnych zdań, patrz twierdzenie Tarskiego o nieokreśloności prawdy ). Formularz, w którym usunięto odniesienie, jest następujący:

Jeśli napiszesz następujący cytat dwa razy, drugi raz w cudzysłowie, wynikowe zdanie będzie fałszywe: „Jeśli napiszesz następujący cytat, drugi raz w cudzysłowie, wynikowe zdanie będzie fałszywe:”

Bez odniesienia do siebie, mamy instrukcje, jak skonstruować zdanie, a następnie coś z nim zrobić. A zdanie, które się konstruuje, jest równe instrukcjom. Zauważ, że w -calculus nie potrzebujemy cudzysłowów, ponieważ nie ma rozróżnienia między danymi a instrukcjami. $\lambda$

Teraz, jeśli to przeanalizujemy, mamy gdzie jest instrukcją, aby skonstruować i coś z tym zrobić. $MM$ $Mx$ $xx$

$Mx = f(xx)$

Więc to i mamy $M$ $\lambda x. f(xx)$

$MM = (\lambda x. f(xx))(\lambda x. f(xx))$

To jest dla ustalonego . Jeśli chcesz uczynić go operatorem, po prostu dodajemy i otrzymujemy : $f$ $\lambda f$ $Y$

$Y = \lambda f. (MM) = \lambda f.((\lambda x. f(xx))(\lambda x. f(xx)))$

Więc po prostu pamiętać paradoksu bez samo-odniesienia i że pomaga mi zrozumieć, co jest. $Y$

Kaveh
źródło

3

Musisz więc zdefiniować kombinator punktów stałych

fix f = f (fix f)
      = f (f (fix f))
      = f (f (f ... ))

ale bez wyraźnej rekurencji. Zacznijmy od najprostszego nieredukowalnego kombinatora

omega = (\x. x x) (\x. x x)
      = (\x. x x) (\x. x x)
      = ...

xW pierwszym lambda wielokrotnie podstawiony przez drugi lambda. Prosta konwersja alfa czyni ten proces jaśniejszym:

omega =  (\x. x x) (\x. x x)
      =α (\x. x x) (\y. y y)
      =β (\y. y y) (\y. y y)
      =α (\y. y y) (\z. z z)
      =β (\z. z z) (\z. z z)

Tzn. Zmienna w pierwszej lambdzie zawsze znika. Więc jeśli dodamy fdo pierwszej lambda

(\x. f (x x)) (\y. y y)

fwola bob górę

f ((\y. y y) (\y. y y))

Mamy swoje omegaplecy. Teraz powinno być jasne, że jeśli dodamy fdo drugiej lambda, to fpojawi się w pierwszej lambdzie, a potem się podskoczy:

Y f = (\x. x x)     (\x. f (x x))
      (\x. f (x x)) (\x. f (x x)) -- the classical definition of Y

Od

(\x. s t) z = s ((\x. t) z), if `x' doesn't occur free in `s'

możemy przepisać wyrażenie jako

f ((\x. x x) (\x. f (x x))

co jest sprawiedliwe

f (Y f)

i mamy nasze równanie Y f = f (Y f). Tak więc Ykombinator jest zasadniczo

podwójny f
zrobić pierwszy fporuszało się w górę
powtarzać

użytkownik3237465
źródło

2

Być może widziałeś klasyczny przykład równania bez normalnej postaci:

(λ x . x x) (λ x . x x) ▹ (λ x . x x) (λ x . x x)

$(\lambda x.xx)(\lambda x.xx) \triangleright (\lambda x.xx)(\lambda x.xx)$

Podobne równanie sugeruje równanie ogólne:

\begin{matrix} (A) & \begin{array}{rr} (λ x . R (x x)) (λ x . R (x x)) \\ ▹ & R ((λ x . R (x x)) (λ x . R (x x))) \\ ▹ & R (R ((λ x . R (x x)) (λ x . R (x x)))) \\ ▹ & \dots \end{array} \end{matrix}

$\begin{array} {rr} & (\lambda x.R(xx))(\lambda x.R(xx)) ~\\ \triangleright & R(~ (\lambda x.R(xx))(\lambda x.R(xx))~) \\ \triangleright & R(R(~ (\lambda x.R(xx))(\lambda x.R(xx))~)) \\ \triangleright & \dots \end{array} \tag{A}$

(A) jest sposobem na pisanie ogólnych równań rekurencyjnych w rachunku lambda (poza prymitywnym rekurencyjnym). Jak więc rozwiązać równanie ? Podłącz dla w powyższym równaniu, aby uzyskać: $Yf = f(Yf)$ $f$ $R$

Y f = (λ x . f (x x)) (λ x . f (x x))

$Yf = (\lambda x.f(xx))(\lambda x.f(xx))$

Y = λ f . (λ x . f (x x)) (λ x . f (x x))

$Y = \lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$

DanielV
źródło

Czyste, intuicyjne wyprowadzenie kombinatora stałoprzecinkowego (kombinator Y)?

Odpowiedzi: