Apa perbedaan antara penulisan ulang istilah dan pencocokan pola?

Karena tidak ada tanggapan di Lambda the Ultimate, saya coba lagi di sini: istilah sistem penulisan ulang digunakan misalnya dalam teorema otomatis yang membuktikan perhitungan simbolis, dan tentu saja untuk mendefinisikan tata bahasa formal. Ada beberapa bahasa pemrograman yang berbasis pada penulisan ulang istilah, tetapi sejauh yang saya mengerti konsepnya lebih dikenal sebagai pencocokan pola . Pencocokan pola banyak digunakan dalam bahasa fungsional. Barry Jay telah menciptakan keseluruhan teori yang disebut kalkulus pola , tetapi ia hanya menyebutkan penulisan ulang istilah secara singkat. Saya merasa mereka semua mengacu pada ide dasar yang sama, jadi bisakah Anda menggunakan penulisan ulang dan pencocokan pola secara sinonim?

Salah satu cara untuk melihat kedua konsep ini adalah dengan mengatakan bahwa pencocokan pola adalah fitur bahasa pemrograman untuk menggabungkan diskriminasi pada konstruktor dan istilah yang merusak (sementara pada saat yang sama memilih dan menamai fragmen istilah) secara aman, kompak dan efisien. Penelitian tentang pencocokan pola biasanya berfokus pada efisiensi implementasi, misalnya tentang cara meminimalkan jumlah perbandingan yang harus dilakukan mekanisme pencocokan.

Sebaliknya, penulisan ulang istilah adalah model umum perhitungan yang menyelidiki berbagai metode (berpotensi non-deterministik) untuk mengganti subterms ekspresi sintaksis (lebih tepatnya elemen istilah-aljabar atas beberapa set variabel) dengan istilah lain. Penelitian tentang sistem penulisan ulang istilah biasanya tentang sifat-sifat abstrak dari sistem penulisan ulang seperti pertemuan, determinisme dan penghentian, dan lebih khusus tentang bagaimana sifat-sifat seperti itu atau tidak dipertahankan oleh operasi aljabar pada sistem penulisan ulang, yaitu sejauh mana sifat-sifat ini bersifat komposisional.

$(l, r)$$C[l\sigma] \rightarrow C[r\sigma]$$C[.]$$\sigma$), sementara pencocokan pola dalam bahasa modern seperti Haskell, OCaml atau Scala hanya menyediakan untuk menulis ulang 'di bagian atas' dari suatu istilah. Batasan ini juga, saya pikir, dikenakan dalam kalkulus pola Jay. Izinkan saya menjelaskan apa yang saya maksud dengan pembatasan ini. Dengan pencocokan pola di OCaml, Haskell, Scala sense, Anda tidak bisa mengatakan sesuatu seperti

match M with
   | C[ x :: _ ]  -> printf "%i ...\n" x
   | C[ [] ] -> printf "[]"

Ada apa C[.]disini Itu seharusnya menjadi variabel yang berkisar pada konteks satu-holed. Tetapi bahasa seperti OCaml, Haskell atau Scala tidak memberikan variabel pemrogram yang berkisar pada konteks arbitrer (satu-holed), hanya variabel yang berkisar pada nilai. Dengan kata lain, dalam bahasa seperti itu Anda tidak dapat mencocokkan pola pada posisi sewenang-wenang dalam suatu istilah. Anda selalu harus menentukan jalur dari akar pola ke bagian yang Anda minati. Saya kira alasan utama untuk memaksakan pembatasan ini adalah bahwa jika pencocokan pola akan menjadi non-deterministik, karena istilah mungkin cocok dengan pola di lebih dari satu cara. Misalnya istilah tersebut (true, [9,7,4], "hello", 7)cocok dengan pola C[7]dalam dua cara, dengan asumsi C[.] berkisar pada konteks seperti itu.

Saya rasa tidak benar menyebut mereka sinonim; ada beberapa tumpang tindih dalam hal penelitian dan implementasi. Saya sama sekali tidak terbiasa dengan pekerjaan Jay, dan saya hanya cukup akrab dengan sistem penulisan ulang istilah, jadi saya mungkin kehilangan sesuatu juga.

Pencocokan pola secara umum berkaitan dengan masalah berikut: Anda memiliki beberapa struktur (pohon atau daftar atau multiset) dan Anda ingin memeriksa apakah struktur cocok dengan pola (atau salah satu dari sejumlah pola). Pertanyaan ini tentu saja relevan dengan penulisan ulang istilah, karena dalam sistem penulisan ulang istilah fakta bahwa suatu istilah cocok dengan suatu pola berarti bahwa istilah tersebut dapat ditulis ulang ke istilah yang berbeda, tetapi itu bukan penulisan ulang istilah yang sinonim. (Mungkin ada formulasi pencocokan pola sebagai penulisan ulang: "Diberi istilah, dapatkah Anda menulis ulang untuk mencocokkan pola?" Tapi saya belum pernah melihat ini.)

Pencocokan pola dalam bahasa pemrograman fungsional memiliki interpretasi logis dalam hal fokus (lihat "Fokus pada Pencocokan Pola" Krishnaswami ), misalnya. Sistem penulisan ulang istilah, di sisi lain, sering melakukan pencocokan modulo beberapa sifat persamaan, yang tidak ada dalam sebagian besar bahasa pemrograman fungsional (Anda tidak dapat mencocokkan dengan multiset dalam ML atau Haskell). Namun, tidak ada alasan mendasar mengapa mencocokkan properti persamaan modulo tidak harus ada dalam bahasa fungsional.

(Saya lebih suka menulis ini sebagai komentar, tetapi saat ini saya tidak bisa.)

Koreksi saya jika saya salah, tetapi sejauh yang saya mengerti, satu lagi perbedaan antara pencocokan pola dan penulisan ulang istilah, selain dari apa yang dikatakan Martin Berger dalam jawaban yang sangat bagus , adalah bahwa aturan pencocokan pola datang dengan urutan yang tetap (dalam implementasi seperti Haskell's), sedangkan dengan aturan penulisan ulang istilah ini belum tentu demikian. Fitur ini, seperti yang diharapkan, dapat membuat banyak perbedaan ketika mempertimbangkan perilaku (khususnya, penghentian) aturan (lihat "Pengantar Lembut untuk Haskell, Versi 98", bagian 4.2 , misalnya, atau hanya faktorial contoh di "Learn you a Haskell" ).

Orang yang lebih berpengetahuan luas dalam teori penulisan ulang akan memiliki lebih banyak untuk mengatakan tentang itu (misalnya, bagaimana cara mengetik cocok perbandingan seperti itu persis?), Tetapi, menurut saya adil untuk setuju dengan Martin Berger, dalam istilah menulis ulang dapat dilihat mencakup pencocokan pola (setidaknya karena ini diterapkan dalam bahasa seperti Haskell), sejauh keduanya dapat (agak kering) dipandang sebagai perangkat yang hanya menggunakan aturan terkait istilah.