Apakah eta-equivalence untuk fungsi-fungsi yang kompatibel dengan operasi seq Haskell?

Lemma: Dengan asumsi kesetaraan eta kita memilikinya (\x -> ⊥) = ⊥ :: A -> B.

Bukti: ⊥ = (\x -> ⊥ x)dengan kesetaraan eta, dan (\x -> ⊥ x) = (\x -> ⊥)dengan pengurangan di bawah lambda.

Laporan Haskell 2010, bagian 6.2 menentukan seqfungsi dengan dua persamaan:

seq :: a -> b -> b
seq ⊥ b = ⊥
seq ab = b, jika a ≠ ⊥

Itu kemudian mengklaim "Sebagai konsekuensinya, ⊥ tidak sama dengan \ x -> ⊥, karena seq dapat digunakan untuk membedakannya."

Pertanyaan saya adalah, apakah itu benar-benar konsekuensi dari definisi seq?

Argumen implisit tampaknya yang seqtidak dapat diperhitungkan jika seq (\x -> ⊥) b = ⊥. Namun saya belum dapat membuktikan bahwa hal seperti seqitu tidak dapat dihitung. Bagi saya, sepertinya seqitu monoton, dan terus-menerus, yang menempatkannya dalam ranah komputabel.

Algoritme yang mengimplementasikan seperti seq mungkin bekerja dengan mencoba mencari beberapa xtempat f x ≠ ⊥dengan menyebutkan domain fdimulai dengan ⊥. Meskipun implementasi seperti itu, bahkan jika mungkin sama sekali, menjadi sangat berbulu ketika kita ingin membuat seqpolimorfik.

Apakah ada bukti bahwa tidak ada dihitung seqbahwa mengidentifikasi (\x -> ⊥)dengan ⊥ :: A -> B? Atau, apakah ada beberapa konstruksi seqyang tidak sesuai (\x -> ⊥)dengan ⊥ :: A -> B?

Pertama, mari kita secara eksplisit tentang bagaimana seqmembedakan dari :$\bot$$\lambda x . \bot$

bottom :: a
bottom = bottom

eta :: a -> b
eta x = bottom

-- This terminates
fortytwo = seq eta 42

-- This does not terminate
infinity = seq bottom 42

Oleh karena itu fakta eksperimental bahwa di Haskell dan dapat dibedakan secara operasional. Itu juga fakta, dan yang cukup jelas, yang dapat dihitung karena Haskell yang menghitungnya. Begitu banyak tentang Haskell. Anda bertanya tentang ungkapan yang sangat khusus dari dokumentasi Haskell. Saya membacanya dengan mengatakan bahwa seharusnya memenuhi dua persamaan yang diberikan, tetapi kedua persamaan itu tidak cukup untuk definisi . Inilah alasannya: Saya dapat memberi Anda dua model (cukup diketik) -calculus yang dapat dihitung dan memenuhi persamaan yang diberikan, tetapi di salah satu model dan$\bot$$\lambda x . \bot$seqseqseq$\lambda$seq$\bot$$\lambda x . \bot$ setuju, sementara yang lain tidak.

Dalam model domain-teori sederhana di mana -expresi ditafsirkan dalam domain fungsi kontinu kita memiliki , tentu saja. Ambil domain Scott yang efektif atau semacamnya untuk membuat semuanya dapat dihitung. Mudah untuk didefinisikan dalam model seperti itu.$\lambda$$[D \to E]$$\bot = \lambda x . \bot$seq

Kita juga dapat memiliki model -calculus yang membedakan dan , dan tentu saja -rule tidak dapat menampung. Sebagai contoh, kita dapat melakukan ini dengan menginterpretasikan fungsi-fungsi dalam domain , yaitu domain fungsi ruang dengan tambahan bottom terpasang. Sekarang adalah, well, bagian bawah , sementara adalah elemen tepat di atasnya. Mereka tidak dapat dibedakan oleh aplikasi karena keduanya mengevaluasi ke , tidak peduli apa pun yang Anda terapkan (keduanya secara ekstensi sama ). Tapi kami punya$\lambda$seq$\bot$$\lambda x . \bot$$\eta$$[D \to E]_\bot$$\bot$$[D \to E]_\bot$$\lambda x . \bot$$\bot$seq sebagai peta antara domain dan itu juga membedakan bawah dari semua elemen lainnya.

Perhatikan bahwa spesifikasi seqyang Anda kutip bukan definisi. Mengutip laporan Haskell "Fungsi seq didefinisikan oleh persamaan : [dan kemudian persamaan yang Anda berikan]".

Argumen yang disarankan tampaknya seq akan tidak dapat dihitung jika seq (\ x -> ⊥) b = ⊥.

Perilaku seperti itu akan melanggar spesifikasi seq.

Yang penting, karena seqbersifat polimorfik, seqtidak dapat didefinisikan dalam hal dekonstruksi (proyeksi / pencocokan pola, dll.) Pada salah satu dari dua parameter.

Apakah ada bukti bahwa tidak ada seq komputer yang mengidentifikasi (\ x -> ⊥) dengan ⊥ :: A -> B?

Jika seq' (\x -> ⊥) b, orang mungkin berpikir kita bisa menerapkan parameter pertama (yang merupakan fungsi) ke beberapa nilai dan kemudian. Keluar. Tetapi, seqtidak pernah dapat mengidentifikasi parameter pertama dengan nilai fungsi (bahkan jika itu menjadi satu untuk beberapa penggunaan seq) karena jenis polimorfik parametriknya. Parametrisitas berarti kita tidak tahu apa pun tentang parameter. Selain itu, seqtidak pernah bisa mengambil ekspresi dan memutuskan "apakah ini ⊥?" (lih. Masalah Berhenti), seqhanya dapat mencoba untuk mengevaluasinya, dan itu sendiri berbeda dengan ⊥.

Yang seqdilakukan adalah mengevaluasi parameter pertama (tidak sepenuhnya, tetapi untuk "bentuk normal kepala lemah" [1], yaitu ke konstruktor paling atas), lalu mengembalikan parameter kedua. Jika parameter pertama kebetulan ⊥(yaitu, perhitungan non terminating) maka mengevaluasi itu menyebabkan seqnon-terminate, dan dengan demikian seq ⊥ a = ⊥.

[1] Teorema Gratis di Hadirat seq - Johann, Voigtlander http://www.iai.uni-bonn.de/~jv/p76-voigtlaender.pdf

$\lambda x.\, \bot$$\lambda x.\, \bot$

Samson Abramsky mempertimbangkan masalah ini sejak lama dan menulis sebuah makalah berjudul " The Lazy Lambda Calculus ". Jadi, jika Anda menginginkan definisi formal, di sinilah Anda akan melihat.

Membuktikan bahwa λ x. Ω ‌ ≠ Ω in adalah salah satu tujuan yang Abramsky tetapkan untuk teori kalkulus lambda malasnya (halaman 2 makalahnya , sudah dikutip oleh Uday Reddy), karena keduanya dalam bentuk kepala normal yang lemah. Pada definisi 2.7, ia membahas secara eksplisit bahwa eta-reduksi λ x. M x → M umumnya tidak valid, tetapi dimungkinkan jika M berakhir di setiap lingkungan. Ini tidak berarti bahwa M harus menjadi fungsi total - hanya bahwa mengevaluasi M harus diakhiri (dengan mengurangi menjadi lambda, misalnya).

Pertanyaan Anda tampaknya dimotivasi oleh masalah praktis (kinerja). Namun, meskipun Laporan Haskell mungkin kurang dari sepenuhnya jelas, saya ragu bahwa menyamakan λ x. ⊥ ‌ dengan ⊥ akan menghasilkan implementasi Haskell yang berguna; apakah itu mengimplementasikan Haskell '98 atau tidak masih bisa diperdebatkan, tetapi memberikan komentar, jelas bahwa penulis bermaksud untuk menjadi demikian.

Akhirnya, bagaimana seq menghasilkan elemen untuk tipe input yang sewenang-wenang? (Saya tahu QuickCheck mendefinisikan typeclass sewenang-wenang untuk itu, tetapi Anda tidak diizinkan untuk menambahkan kendala seperti itu di sini) Ini melanggar parametrik.

Diperbarui : Saya tidak berhasil mengkodekan hak ini (karena saya tidak begitu lancar di Haskel), dan memperbaiki ini sepertinya memerlukan runSTwilayah bersarang . Saya mencoba menggunakan sel referensi tunggal (dalam monad ST) untuk menyimpan elemen arbitrer seperti itu, membacanya nanti, dan membuatnya tersedia secara universal. Parametrisitas membuktikan bahwa di break_parametricitybawah ini tidak dapat didefinisikan (kecuali dengan kembali ke bawah, misalnya kesalahan), sementara itu bisa memulihkan elemen yang seq diusulkan akan menghasilkan.

import Control.Monad.ST
import Data.STRef
import Data.Maybe

produce_maybe_a :: Maybe a
produce_maybe_a = runST $ do { cell <- newSTRef Nothing; (\x -> writeSTRef cell (Just x) >> return x) `seq` (readSTRef cell) }

break_parametricity :: a
break_parametricity = fromJust produce_maybe_a

Saya harus mengakui bahwa saya agak kabur memformalkan bukti parametrik yang diperlukan di sini, tetapi penggunaan parametrikitas informal ini merupakan standar di Haskell; tetapi saya belajar dari tulisan Derek Dreyer bahwa teori yang dibutuhkan dengan cepat dikerjakan dalam tahun-tahun terakhir ini.

EDIT:

• Saya bahkan tidak yakin apakah Anda memerlukan ekstensi itu, yang dipelajari untuk bahasa seperti ML, imperatif, dan tidak ketik, atau apakah teori klasik parametrik meliputi Haskell.
• Juga, saya menyebut Derek Dreyer hanya karena saya baru saja menemukan karya Uday Reddy - saya baru tahu tentang hal itu dari "Esensi Reynolds". (Saya hanya mulai benar-benar membaca literatur tentang parametrik dalam sebulan terakhir ini).