Quine w rachunku różnym lambda

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. $(\lambda x.x \; x)\;(\lambda x.x \; x)$

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 .

(λ x . A)

$(\lambda x . A)$

A

$A$

((λ x . A) y)

$((\lambda x . A)\,\, y)$

(λ x . A)

$(\lambda x . A)$

y

$y$

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

lambda-calculus

— Nataniel
źródło

Nie jest to odpowiedź na moje pytanie, ale dla własnego odniesienia (i dla przyszłych gości) przydatne będzie łącze do wiki.haskell.org/Combinatory_logic , w którym ktoś ma o wiele głębsze przemyślenia na temat quines niż ja.

— Nathaniel

Zauważ, że quine musi stworzyć swój własny kod źródłowy . Utworzenie funkcji, którą reprezentuje, nie jest wystarczające.

— PyRulez

@PyRulez jaki jest kod źródłowy wyrażenia lambda? Jeśli jest to sekwencja znaków, wyrażenie lambda nie jest w stanie go wyprowadzić, w związku z czym możemy zdefiniować słowo „quine”, które oznacza coś nieco innego dla wyrażeń lambda bez obawy o dwuznaczność. Z drugiej strony, jeśli myślisz o kodzie źródłowym jako o samej ekspedycji lambda, to „kod źródłowy” i „funkcja, którą reprezentuje” są tym samym. Więc myślę, że u mnie wszystko w porządku.

— Nathaniel,

istnieje kościół kodujący ciągi znaków. Rachunek lambda powinien wypisywać kodowanie kościelne ciągu znaków, które go reprezentują.

— PyRulez,

Jasne, nie jest to trudne, jeśli zdefiniujesz to w ten sposób. To pytanie dotyczyło innej rzeczy.

— Nathaniel,

Odpowiedzi:

Chcesz wyrazu takiego, że : $Q$ $\forall M \in \Lambda$

Q M ⊳_{β} Q

$QM \rhd_\beta Q$

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. $Q$ $M \equiv x$ $M$
- $Q$ to jakiś atom . Następnie . To nie sprowadza się do . $a$ $QM \equiv ax$ $a$
- $Q$ to jakaś aplikacja . Następnie . jest postacią normalną na podstawie hipotezy, więc jest również w postaci normalnej i nie można go zredukować do . $(RS)$ $QM \equiv (RS)x$ $(RS)$ $(RS)x$ $(RS)$
- $Q$ to jakaś abstrakcja (jeśli ma być wolny w , to dla uproszczenia możemy po prostu wybrać równoważne dowolnej zmiennej abstrakty powyżej). Następnie . Od w postaci normalnej, to jest . W związku z tym nie możemy zredukować do . $(\lambda x.A)$ $x$ $A$ $M$ $\lambda$ $QM \equiv (\lambda x.A)x \rhd_\beta A[x/x] \equiv A$ $(\lambda x.A)$ $A$ $A$ $(\lambda x.A)$
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$ $\exists N \in \beta\text{-nf}$ $N \not\equiv Q$ $\forall M \in \Lambda$
$Q M ⊳_{β} Q ⊳_{β} N$

W przypadku musi istnieć również sekwencja redukcji , ponieważ: $M \equiv x$ $Qx \rhd_\beta Nx \rhd_\beta N$
- $Qx \rhd_\beta Nx$ jest możliwe dzięki temu, że . $Q \rhd_\beta N$
- $Nx$ musi się znormalizować, ponieważ jest nf, a jest tylko atomem. $N$ $\beta$ $x$
- Jeśli miałaby znormalizować się do czegoś innego niż , to ma dwa nfs, co nie jest możliwe w następstwie twierdzenia Church-Rosser. (Twierdzenie Church-Rosser zasadniczo stwierdza, że redukcje są zbieżne, jak zapewne już wiesz). $Nx$ $N$ $Qx$ $\beta$
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. $Nx \rhd_\beta 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$
$Q \equiv (λ z . (λ x . λ z . (x x)) (λ x . λ z . (x x)))$ $Q \equiv (\lambda z.(λx.λz.(x x)) (λx.λz.(x x)))$ $\beta$ $\begin{aligned} Q M & \equiv (λ z . (λ x . λ z . (x x)) (λ x . λ z . (x x))) M \\ ⊳_{1 β} (λ x . λ z . (x x)) (λ x . λ z . (x x)) \\ ⊳_{1 β} (λ z . ((λ x . λ z . (x x)) (λ x . λ z . (x x))) \\ \equiv Q \end{aligned}$ $\begin{align} QM &\equiv (\lambda z.(λx.λz.(x x)) (λx.λz.(x x))) M \\ & \rhd_{1\beta} (λx.λz.(x x)) (λx.λz.(x x)) \\ & \rhd_{1\beta} (λz.((λx.λz.(x x))(λx.λz.(x x))) \\ & \equiv Q \end{align}$

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.

— Roy O.
źródło

Gdybym mógł również zaakceptować odpowiedź Denisa, zrobiłbym to, ale (po tym, jak dowiedziałem się nieco więcej i byłem w stanie ją w pełni zrozumieć), ta odpowiedź naprawdę mnie przekonała, że ten „kombinator quine” nie może być wdrożony przez wyrażenie lambda w normalnej formie.

— Nathaniel

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. $(\lambda x. x)$ $(\lambda x. x)$ $(\lambda x. x)$

— Dave Clarke
źródło

To interesujący punkt. W pytaniu próbowałem podać definicję tego, co może być traktowane jako nietrywialny quine w rachunku lambda: funkcja, która zastosowana do dowolnego wejścia, redukuje się do siebie (do podstawień zmiennych). Być może jest to niemożliwe, ale nie jest to oczywiste, przynajmniej dla mnie.

— Nathaniel

Oto propozycja:

Wybieramy jako stały punkt funkcji . $A$ $f=\lambda t. (\lambda z.t)$

Można to zrobić za pomocą kombinatora punktów stałych i ustawienie . $Y=\lambda g.((\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x)))$ $A=Y f=(\lambda x.\lambda z.(x\ x))\ (\lambda x.\lambda z.(x\ x))$

Teraz pokazujemy, że jest quine. Rzeczywiście zmniejsza się do , więc oznacza to, że dla dowolnego , . $A$ $A$ $\lambda z.A$ $y$ $(\lambda z.A)y \to_\beta A \to_\beta (\lambda z.A)$

— Denis
źródło

Jest to dość schludne i odpowiada na zadane pytanie, więc czuję się źle, że go nie zaakceptowałem --- ale niestety popełniłem niewielki błąd, określając, czego chcę. Naprawdę chcę stać się gdy zostanie zredukowany do normalnej postaci, nie tylko po etapie redukcji wersji beta. (Zobacz zaktualizowane pytanie, dlaczego). Oznacza to, że nie może zawierać żadnych powtórzeń, ponieważ jeśli tak, redukcja nie zostanie zakończona.

(λ z . A) y

$(\lambda z.A)\;y$

(λ z . A)

$(\lambda z.A)$

A

$A$

— Nathaniel

Ach, w tym przypadku jestem całkiem pewien, że to jest niemożliwe, z powodu następującego intuicji (nie dowód, ale prawie): Chcesz odgrywać żadnej roli, ponieważ ma do pracy dla każdego , tak nie powinny być wolne w . Następnie tylko redukuje się do . Teraz chcesz zredukować do . To ostatnie wyrażenie nie może być normalną formą, ponieważ wnętrze można ponownie zmniejszyć ...

y

$y$

y

$y$

y

$y$

A

$A$

(λ z . A) y

$(\lambda z.A)y$

A

$A$

A

$A$

λ z . A

$\lambda z.A$

A

$A$

— Denis

To zachowanie nie jest bardzo zaskakujące, ponieważ ponieważ „drukowanie” jest ponownie instrukcją, napis wypisujący własny kod jest zawsze wykonywalny. To, o co pytasz, jest podobne do pytania o quine, tak że jeśli wykonasz wyjście, nic nie drukuje (co z definicji jest niemożliwe).

λ - c a l c u l u s

$\lambda-calculus$

— Denis,

Ach, masz rację oczywiście. Powinienem to zobaczyć. Nie jestem pewien, czy przyjąć odpowiedź, czy edytować pytanie, aby poprosić o lepszą definicję. Zastanowię się trochę. (Nadal wydaje mi się, że powinno być możliwe podanie nietrywialnej definicji, w której prosisz o coś, co się skończy, ale nie jestem pewien jak).

— Nathaniel

Chociaż to powiedziawszy, czy to prawda, że (zakładam, że masz na myśli ) nie musi być wolny w ? Np. może być czymś podobnym do . (Pseudokod, ponieważ nie jestem pewien, czy możliwe jest zdefiniowanie operatora równości dla dowolnych wyrażeń w rachunku lambda, ale myślę, że rozumiecie, co mam na myśli).

z

$z$

z

$z$

A

$A$

A

$A$ if z==p then return q, otherwise return q

— Nathaniel