Chciałbym przykład quine w czystym rachunku lambda . Byłem dość zaskoczony, że nie znalazłem go przez google. Strona quine zawiera listę quinów dla wielu „prawdziwych” języków, ale nie dla rachunku lambda.
Oczywiście oznacza to zdefiniowanie, co mam na myśli przez quine w rachunku lambda, co robię poniżej. (Proszę o coś dość konkretnego).
W kilku miejscach, np. Larkin i Stocks (2004), widzę następujące cytowanie jako wyrażenie „samoreplikujące się”: . To zmniejsza się do siebie po pojedynczym etapie redukcji beta, co daje wrażenie quine. Jednak nie jest podobny do quine, ponieważ nie kończy się: dalsze redukcje beta będą wytwarzać ten sam wyraz, więc nigdy nie zmniejszy się do normalnej postaci. Dla mnie quine to program, który sam się kończy i wypisuje, dlatego chciałbym wyrażenie lambda o tej właściwości.
Oczywiście każde wyrażenie, które nie zawiera żadnych powtórzeń, jest już w normalnej formie i dlatego samo się zakończy i wyśle. Ale to zbyt trywialne. Proponuję więc następującą definicję w nadziei, że przyjmie ona nietrywialne rozwiązanie:
definicja (niepewna): Quine w rachunku lambda jest wyrażeniem postaci (gdzie oznacza jakieś określone wyrażenie rachunku lambda), tak że staje się , lub czymś równoważnym przy zmianach nazw zmiennych, po sprowadzeniu do postaci normalnej, dla dowolnego wejścia .
Biorąc pod uwagę, że rachunek lambda jest tak samo równoważny z Turingiem jak każdy inny język, wydaje się, że powinno to być możliwe, ale mój rachunek lambda jest zardzewiały, więc nie mogę wymyślić żadnego przykładu.
Odniesienie
James Larkin i Phil Stocks. (2004) Konferencje „Samoreplikujące się wyrażenia w rachunku Lambda Calculus” w badaniach i praktyce w zakresie technologii informacyjnych, 26 (1), 167-173. http://epublications.bond.edu.au/infotech_pubs/158
źródło
Odpowiedzi:
Chcesz wyrazu takiego, że :∀ M ∈ ΛQ ∀M∈Λ
Nie sprecyzuję żadnych dalszych ograniczeń dotyczących (np. Dotyczących jego formy i tego, czy się normalizuje) i pokażę wam, że zdecydowanie musi to być normalizacja.Q
Załóżmy, że jest w normalnej formie. Wybierz (możemy to zrobić, ponieważ twierdzenie musi się trzymać dla wszystkich ). Potem są trzy przypadki.M ≡ x MQ M≡x M
Więc jeśli takie istnieje, nie może być w normalnej formie.Q
Dla kompletności załóżmy, że ma normalną formę, ale nie jest w normalnej formie (być może słabo się normalizuje), tj. z takim, że :Q ∃N∈β-nf N≢Q ∀M∈Λ
W przypadku musi istnieć również sekwencja redukcji , ponieważ:Q x ⊳ β N x ⊳ β NM≡x Qx⊳βNx⊳βN
Zauważ jednak, że nie jest możliwe na podstawie powyższego argumentu (1), więc nasze założenie, że ma postać normalną, nie jest możliwe do utrzymania.QNx⊳βN Q
Jeśli pozwolimy na takie , to jesteśmy pewni, że musi to być normalizacja. W takim przypadku możemy po prostu użyć kombinatora, który eliminuje wszelkie otrzymywane argumenty. Sugestia Denisa działa dobrze: Następnie tylko w dwóch redukcjach:Q
Wynik ten nie jest bardzo zaskakujące, ponieważ są w istocie pytaniem o termin, który eliminuje wszelkie argumentem to odbiera, a to jest coś, co często widzę wymienione jako bezpośrednie zastosowanie twierdzenia o stałym punkcie.
źródło
Z jednej strony jest to niemożliwe, ponieważ quine ma wypisywać własny kod, a rachunek czysto lambda nie ma możliwości wykonania danych wyjściowych.
Z drugiej strony, jeśli przyjmiesz, że wynikowy warunek jest wynikiem, to każda normalna postać jest quine.
Na przykład termin lambda jest już formą normalną, a przy założeniu, że jego wynikiem jest wynikowa forma normalna, wynikiem jest . Zatem jest quine.(λx.x) (λx.x) (λx.x)
źródło
Oto propozycja:
Wybieramy jako stały punkt funkcji .A f=λt.(λz.t)
Można to zrobić za pomocą kombinatora punktów stałych i ustawienie .Y=λg.((λx.g (x x)) (λx.g (x x))) A=Yf=(λx.λz.(x x)) (λx.λz.(x x))
Teraz pokazujemy, że jest quine. Rzeczywiście zmniejsza się do , więc oznacza to, że dla dowolnego , .A A λz.A y (λz.A)y→βA→β(λz.A)
źródło
if z==p then return q, otherwise return q