Sebuah quine dalam kalkulus lambda murni

Saya ingin contoh quine dalam kalkulus lambda murni . Saya cukup terkejut bahwa saya tidak dapat menemukannya dengan googling. Halaman quine mencantumkan quine untuk banyak bahasa "nyata", tetapi tidak untuk kalkulus lambda.

Tentu saja, ini berarti mendefinisikan apa yang saya maksudkan dengan quine dalam kalkulus lambda, yang saya lakukan di bawah ini. (Saya meminta sesuatu yang sangat spesifik.)

Di beberapa tempat, misalnya Larkin dan Stocks (2004), saya melihat yang berikut ini dikutip sebagai ekspresi "replikasi diri": $(\lambda x.x \; x)\;(\lambda x.x \; x)$ . Ini berkurang pada dirinya sendiri setelah satu langkah pengurangan beta, memberikannya perasaan seperti quine. Namun, ini tidak seperti quine karena tidak berhenti: pengurangan beta lebih lanjut akan terus menghasilkan ekspresi yang sama, sehingga tidak akan pernah berkurang ke bentuk normal. Bagi saya quine adalah program yang mengakhiri dan mengeluarkan sendiri, jadi saya ingin ekspresi lambda dengan properti itu.

Tentu saja, setiap ekspresi yang tidak mengandung redex sudah dalam bentuk normal, dan karena itu akan berakhir dan dihasilkan sendiri. Tapi itu terlalu sepele. Jadi saya mengusulkan definisi berikut dengan harapan akan menerima solusi yang tidak sepele:

Definisi (tentatif): Sebuah quine dalam kalkulus lambda adalah ekspresi dari bentuk

(λ x . A)

$(\lambda x . A)$ (di mana

A

$A$ adalah singkatan dari beberapa ekspresi kalkulus lambda tertentu) sedemikian rupa sehingga

((λ x . A) y)

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

(λ x . A)

$(\lambda x . A)$ , atau sesuatu yang setara dengan itu di bawah perubahan nama variabel, ketika direduksi menjadi bentuk normal, untuksetiapinput

y

$y$ .

Mengingat bahwa kalkulus lambda adalah setara dengan Turing seperti bahasa lain, sepertinya ini mungkin, tetapi kalkulus lambda saya berkarat, jadi saya tidak bisa memikirkan contohnya.

Referensi

James Larkin dan Phil Stocks. (2004) "Ekspresi mereplikasi diri dalam Kalkulus Lambda" Konferensi dalam Penelitian dan Praktek dalam Teknologi Informasi, 26 (1), 167-173. http://epublications.bond.edu.au/infotech_pubs/158

lambda-calculus Nathaniel
sumber

Bukan jawaban untuk pertanyaan saya, tetapi untuk referensi saya di masa depan (dan untuk pengunjung masa depan) akan bermanfaat untuk memiliki tautan ke wiki.haskell.org/Combinatory_logic , di mana seseorang memiliki pemikiran yang lebih dalam tentang quine daripada saya.

Nathaniel

Perhatikan bahwa quine perlu menghasilkan kode sumbernya sendiri . Memproduksi fungsi yang diwakilinya tidak cukup.

PyRulez

@PyRulez apa kode sumber untuk ekspresi lambda? Jika itu adalah urutan karakter maka tidak mungkin ekspresi lambda menghasilkannya, dan akibatnya kita dapat mendefinisikan kata "quine" untuk mengartikan sesuatu yang sedikit berbeda untuk ekspresi lambda tanpa takut ambiguitas. Di sisi lain, jika Anda menganggap kode sumber sebagai ekspresi lambda itu sendiri maka "kode sumber" dan "fungsi yang diwakilinya" adalah hal yang sama. Jadi saya pikir saya baik-baik saja di sini.

Nathaniel

ada penyandian gereja untuk string. Sebuah kalkulus kalkulus lambda harus menampilkan pengkodean gereja dari string karakter yang mewakilinya.

PyRulez

Tentu, itu tidak sulit dilakukan, jika Anda mendefinisikannya seperti itu. Pertanyaan ini tentang hal yang berbeda.

Nathaniel

Jawaban:

Anda ingin istilah sedemikian rupa sehingga : $Q$ $\forall M \in \Lambda$

Q M ⊳_{β} Q

$QM \rhd_\beta Q$

Saya tidak akan menentukan batasan lebih lanjut pada (misalnya mengenai bentuknya dan apakah itu normalisasi) dan saya akan menunjukkan kepada Anda bahwa itu pasti harus non-normalisasi. $Q$

Asumsikan adalah dalam bentuk normal. Pilih (kita dapat melakukannya karena teorema perlu dipegang untuk semua ). Lalu ada tiga kasus. $Q$ $M \equiv x$ $M$
- adalah beberapa atom . Kemudian . Ini tidak dapat direduksi menjadi . $Q$ $a$ $QM \equiv ax$ $a$
- $Q$ adalah beberapa aplikasi . Kemudian . adalah bentuk normal dengan hipotesis, jadi juga dalam bentuk normal dan tidak dapat direduksi menjadi . $(RS)$ $QM \equiv (RS)x$ $(RS)$ $(RS)x$ $(RS)$
- adalah beberapa abstraksi (jika seharusnya gratis di , maka untuk kesederhanaan kita bisa memilih $Q$ $(\lambda x.A)$ $x$ $A$ $M$ setara dengan variabel apa pun abstrak di atas). Kemudian . Karena dalam bentuk normal, maka $\lambda$ $QM \equiv (\lambda x.A)x \rhd_\beta A[x/x] \equiv A$ $(\lambda x.A)$ $A$ . Akibatnya kita tidak bisa mengurangi ke . $A$ $(\lambda x.A)$
Jadi jika seperti itu ada, tidak mungkin dalam bentuk normal. $Q$
Untuk kelengkapan, misalkan $Q$ memiliki bentuk normal, tetapi tidak dalam bentuk normal (mungkin itu adalah normalisasi lemah), yaitu dengan sehingga : $\exists N \in \beta\text{-nf}$ $N \not\equiv Q$ $\forall M \in \Lambda$
$Q M ⊳_{β} Q ⊳_{β} N$

Maka dengan juga harus ada urutan reduksi , karena: $M \equiv x$ $Qx \rhd_\beta Nx \rhd_\beta N$
- dimungkinkan oleh fakta bahwa . $Qx \rhd_\beta Nx$ $Q \rhd_\beta N$
- harus dinormalisasi karena adalah nf dan hanya atom. $Nx$ $N$ $\beta$ $x$
- Jika dinormalisasi ke hal lain selain , maka memiliki dua nfs, yang tidak mungkin oleh akibat wajar dari teorema Gereja-Rosser. (Teorema Church-Rosser pada dasarnya menyatakan bahwa reduksi adalah pertemuan, seperti yang mungkin sudah Anda ketahui.) $Nx$ $N$ $Qx$ $\beta$
Tetapi perhatikan bahwa tidak dimungkinkan oleh argumen (1) di atas, jadi asumsi kami bahwa memiliki bentuk normal tidak dapat dipertahankan. $Nx \rhd_\beta N$ $Q$
Jika kita mengizinkan seperti itu , maka, kami yakin itu harus non-normalisasi. Dalam hal ini kita bisa menggunakan kombinator yang menghilangkan argumen apa pun yang diterimanya. Saran Denis bekerja dengan baik: $Q$ Kemudian hanya dalam duapengurangan :
$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}$

Hasil ini tidak terlalu mengejutkan, karena Anda pada dasarnya meminta istilah yang menghilangkan argumen apa pun yang diterimanya, dan ini adalah sesuatu yang sering saya lihat disebutkan sebagai aplikasi langsung dari teorema titik tetap.

Roy O.
sumber

Jika saya dapat menerima jawaban Denis juga maka saya akan melakukannya, tetapi (setelah saya belajar sedikit lebih banyak dan dapat memahaminya sepenuhnya) jawaban inilah yang benar-benar meyakinkan saya bahwa "kombinator quine" ini tidak dapat dilaksanakan oleh seorang ekspresi lambda dalam bentuk normal.

Nathaniel

Di satu sisi ini tidak mungkin, karena quine seharusnya mengeluarkan kodenya sendiri, dan kalkulus lambda murni tidak memiliki sarana untuk melakukan keluaran.

Di sisi lain, jika Anda menganggap bahwa istilah yang dihasilkan adalah output, maka setiap bentuk normal adalah quine.

Misalnya, istilah lambda sudah merupakan bentuk normal, kemudian dengan asumsi bahwa outputnya adalah bentuk normal yang dihasilkan, outputnya adalah $(\lambda x. x)$ . Jadi adalah quine. $(\lambda x. x)$ $(\lambda x. x)$

Dave Clarke
sumber

Itu poin yang menarik. Dalam pertanyaan saya mencoba memberikan definisi tentang apa yang mungkin dianggap sebagai quine non-sepele dalam kalkulus lambda: fungsi yang, ketika diterapkan pada input apa pun, pengurangan beta pada dirinya sendiri (hingga penggantian nama variabel). Mungkin ini tidak mungkin, tetapi tidak jelas, setidaknya bagi saya.

Nathaniel

Berikut ini proposisi:

Kami memilih untuk menjadi titik fokus fungsi $A$ . $f=\lambda t. (\lambda z.t)$

Ini dapat dilakukan dengan menggunakan fixpoint combinator , dan pengaturan $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))$

Sekarang kami menunjukkan bahwa adalah quine. Memang tereduksi menjadi , jadi itu berarti bahwa untuk setiap , $A$ $A$ $\lambda z.A$ $y$ . $(\lambda z.A)y \to_\beta A \to_\beta (\lambda z.A)$

Denis
sumber

Ini cukup rapi, dan menjawab pertanyaan ketika saya menanyakannya, jadi saya merasa tidak enak karena tidak menerimanya --- tapi sayangnya saya membuat sedikit kesalahan dalam menentukan apa yang saya inginkan. Saya sebenarnya ingin

menjadi

ketika direduksi menjadi bentuk normal, bukan hanya setelah langkah reduksi beta. (Lihat pertanyaan terbaru untuk alasannya.) Ini berarti bahwa

tidak dapat memuat redeks apa pun, karena jika ya maka reduksi tidak akan berakhir.

(λ z . A) y

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

(λ z . A)

$(\lambda z.A)$

A

$A$

Nathaniel

Ah dalam hal ini saya cukup yakin itu tidak mungkin, karena intuisi berikut (bukan bukti tapi hampir): Anda ingin

memainkan peran karena harus bekerja untuk setiap

, sehingga

tidak harus bebas di

. Kemudian

hanya mengurangi ke

. Sekarang Anda ingin

dikurangi menjadi

. Ungkapan terakhir ini tidak bisa menjadi bentuk normal, karena

di dalam lagi dapat dikurangi ...

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

Perilaku ini tidak terlalu mengejutkan, karena sejak "pencetakan"

lagi instruksi, quine yang mencetak kode sendiri selalu dapat dieksekusi. Apa yang Anda minta mirip dengan meminta quine sehingga jika Anda mengeksekusi output, tidak mencetak apa-apa (yang tidak mungkin menurut definisi).

λ - c a l c u l u s

$\lambda-calculus$

Denis

Ahh, tentu saja kau benar. Saya seharusnya melihat itu. Saya tidak yakin apakah akan menerima jawaban Anda atau mengedit pertanyaan untuk meminta definisi yang lebih baik. Saya akan memberikan sedikit pemikiran. (Menurut saya masih mungkin untuk memberikan definisi non-sepele di mana Anda meminta sesuatu yang akan berakhir, tetapi saya tidak yakin caranya.)

Nathaniel

z

$z$

z

$z$

A

$A$

A

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