Lambda calculus: perbedaan antara konteks dan konteks evaluasi

Pertama, saya ingin mengatakan bahwa teks saya di bawah ini mungkin mengandung kesalahan, jadi silakan tunjukkan kesalahan dalam perumusan pertanyaan saya.

Pertimbangkan kalkulus lambda yang tidak diketik dengan boolean dan jika-pernyataan yang istilahnya diberikan oleh sintaks ini:

 t ::= v | t t | if t t t | x
 v ::= \x.t | #t | #f

Konteks C dalam hal ini akan diberikan sesuai dengan sintaks ini:

C ::= [-] | \x. C | C t | t C | if C t t | if t C t | if t t C 

Selain itu, seseorang dapat mendefinisikan konteks evaluasi E menurut sintaksis lain ini:

E ::= [-] | \x. E | v E | E t | if E t t 

Saya membagi pertanyaan saya menjadi tiga sub-poin yang ingin saya bahas.

1. Kapan kedua konsep ini digunakan? Sebagai contoh, saya tahu bahwa konteks evaluasi digunakan untuk mendefinisikan semantik kalkulus, tetapi penggunaan konteks masih agak sulit dipahami saya. Saya juga ingin konfirmasi pengetahuan saya di sini.
2. Kapan satu lebih disukai dari yang lain dan mengapa?
3. Bisakah Anda menunjukkan artikel yang relevan yang dapat membantu saya menyelesaikan masalah ini?

Konteks digunakan untuk banyak tujuan, tetapi biasanya untuk mendefinisikan kongruensi pada program. Konteks evaluasi adalah bagian dari konteks. Mereka biasanya digunakan untuk mendefinisikan hubungan reduksi. Biarkan saya memberi contoh masing-masing.

Salah satu cara formal untuk mendefinisikan kesetaraan program adalah dengan mengatakan bahwa dua program dan N adalah sama secara kontekstual, mereka dapat menggantikan satu sama lain dalam setiap konteks tanpa perubahan perilaku. Kita dapat mendefinisikan ini sebagai berikut: M dan N secara kontekstual sama disediakan untuk semua konteks penutup C [ ⋅ ] untuk M dan N : C [ M ] ⇓ t jika dan hanya jika C [ N ] ⇓ t . Kami mengatakan konteks mendekati untuk M , N$M$$N$$M$$N$$C[\cdot]$$M$$N$$C[M] \Downarrow t$$C[N] \Downarrow t$$M, N$jika atau C [ N ] tidak memiliki variabel bebas. Ekspresi M ⇓ t berarti bahwa program M mengurangi sejumlah langkah hingga nilai t . (Sebagai tambahan, catat bahwa definisi kesetaraan kontekstual lebih terlibat untuk gagasan kaya perhitungan, misalnya proses bersamaan.)$C[M]$$C[N]$$M \Downarrow t$$M$$t$

$$\frac{M \rightarrow N}{E[M] \rightarrow E[N]}$$ $\lambda$$\lambda$$M \rightarrow N$$\lambda x.M \rightarrow \lambda x.N$$\lambda$Laporan Revisi Pada Teori Sintaksis Kontrol Sekuensial dan Negara oleh Felleisen dan Hieb.

$[]$

$$C ::= [] \mid x \mid t \, C \mid C \, t \mid \lambda x.C$$

$C[]$$t$$C[t]$$t$$[]$$C[t]$$[]$$t$

$$(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}$$ $M \{x\leftarrow N\}$$x \mapsto N$$M$

$t$$M$$N$$x$$t = (\lambda x. M) \, N$$t$$t'$$t' = (\lambda x. M) \, N$$t$$C$$M$$N$$x$$t = C[(\lambda x. M) \, N]$$C[M \{x\leftarrow N\}]$

$$\dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \qquad \dfrac{M \to_\beta N}{C[M] \to_\beta C[N]} (\gamma)$$ $$\dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_\beta N}{\lambda x. M \to_\beta \lambda x. N} (C_\lambda) \qquad \dfrac{M \to_\beta N}{M \, P \to_\beta N \, P} (C_{@\lt}) \qquad \dfrac{M \to_\beta N}{P \, M \to_\beta P \, N} (C_{@\gt})$$

Definisi ini menghasilkan reduksi beta, yaitu gagasan evaluasi yang memungkinkan pengurangan subterm apa pun. Komputasi seperti yang dilakukan dalam bahasa pemrograman sering tidak memungkinkan pengurangan subterma di dalam fungsi: aturan pengurangan hanya dapat diterapkan di tingkat atas, atau di sisi kiri atau sisi kanan aplikasi. Kita dapat mengekspresikan ini dengan mendefinisikan jenis konteks baru yang tidak memungkinkan semua bentuk sintaksis: Kita dapat menggunakan sintaks ini untuk mendefinisikan gagasan semantik evaluasi non-parsial: Kami juga dapat menyajikan definisi ini dengan memperluasnya, seperti yang kami lakukan di atas untuk pengurangan beta penuh:

$$D ::= [] \mid x \mid t \, D \mid D \, t$$ $$\dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} \qquad \dfrac{M \to_{np} N}{D[M] \to_{np} D[N]}$$ $$\dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_{np} N}{M \, P \to_{np} N \, P} (C_{@\lt}) \qquad \dfrac{M \to_{np} N}{P \, M \to_{np} P \, N} (C_{@\gt})$$ $D$ akan disebut konteks evaluasi karena digunakan untuk mendefinisikan pengertian evaluasi. Konteks evaluasi bukanlah jenis konteks khusus; alih-alih, menyebutnya konteks evaluasi adalah masalah konteks apa yang digunakan .

Saya akan memberikan satu lagi contoh konteks. Mari kita mendefinisikan nilai berdasarkan sintaks berikut: Sekarang mari kita tentukan jenis konteks lain: Dibandingkan dengan atas, lubang dapat berada di sisi fungsi aplikasi jika argumen aplikasi tersebut adalah sebuah nilai. Tetapkan pengurangan berikut: $V$

$$V ::= x V_1 \ldots V_n \mid \lambda x. M$$ $$E ::= [] \mid M \, E \mid E \, V$$ $D$ $$\dfrac{}{(\lambda x. M) \, V \to_{cbva} M \{x\leftarrow V\}} (\beta_{cbva}) \qquad \dfrac{M \to_\beta N}{E[M] \to_{cbva} E[N]} (\gamma_{cbva})$$ Dengan batasan bahwa argumen fungsi harus menjadi nilai dalam aturan pertama dan bahwa abstraksi lambda bukan konteks, kami mendefinisikan strategi evaluasi panggilan-oleh-nilai. Dengan pembatasan lebih lanjut bahwa argumen dievaluasi sebelum fungsi, ini adalah panggilan urutan aplikatif berdasarkan nilai.