Apa itu kesetaraan beta?

Dalam skrip yang saat ini saya baca pada kalkulus lambda, kesetaraan beta didefinisikan sebagai ini:

The $\beta$ -equivalence adalah kesetaraan terkecil yang berisi . $\equiv_\beta$ $\rightarrow_\beta$

Saya tidak tahu apa artinya itu. Adakah yang bisa menjelaskannya dengan istilah yang lebih sederhana? Mungkin dengan contoh?

Saya membutuhkannya untuk seorang lemma yang mengikuti teorema Gereja-Russer, mengatakan

Jika M N maka ada L dengan M L dan N L. $\equiv_\beta$ $\twoheadrightarrow_\beta$ $\twoheadrightarrow_\beta$

logic terminology lambda-calculus type-theory agung
sumber

Maaf jika bahasanya tidak sempurna, saya menerjemahkan kutipan dari jerman.

magnattic

Jawaban:

$\to_\beta$ adalah hubungan satu langkah antara istilah-istilah dalam $\lambda$ -kalkus. Hubungan ini tidak refleksif, simetris, atau transitif. Relasi ekivalensi $\equiv_\beta$ adalah penutupan reflektif, simetris, transitif $\to_\beta$ . Ini berarti

Jika maka . $M\to_\beta M'$ $M\equiv_\beta M'$
Untuk semua istilah , berlaku. $M$ $M\equiv_\beta M$
Jika , maka . $M\equiv_\beta M'$ $M'\equiv_\beta M$
$M\equiv_\beta M'$ $M'\equiv_\beta M''$ $M\equiv_\beta M''$
$\equiv_\beta$ adalah hubungan terkecil yang memenuhi syarat 1-4.

Lebih konstruktif, pertama terapkan aturan 1 dan 2, lalu ulangi aturan dan berulang sampai mereka tidak menambahkan elemen baru ke relasi. $3$ $4$

Dave Clarke
sumber

Ok terima kasih, saya pikir saya mengerti. Asumsi pertama saya adalah bahwa berarti bahwa M entah bagaimana dapat direduksi menjadi N, tetapi itu tidak harus berlaku karena mereka jelas juga setara jika mereka dapat direduksi menjadi istilah yang sama. Karena poin Anda 3 ini dapat dibangun, kurasa. Terima kasih, itu banyak membantu.

M \equiv_{β} N

$M \equiv_\beta N$

magnattic

Bukankah hubungannya sangat besar? Apakah saya tidak selalu dapat menemukan Term L untuk Term M sehingga ?

L \to_{β} M

$L \rightarrow_\beta M$

Magnattic

Memang, tapi itu seharusnya tidak bermasalah. Mengapa Anda mencari huruf ?

L

$L$

Dave Clarke

Saya tidak tahu Saya hanya berdebat dengan pasangan saya jika selalu akan sangat besar. Terima kasih telah menjelaskan. :)

magnattic

Benar-benar teori himpunan elementer. Anda tahu apa itu hubungan refleksif, apa itu hubungan simetris, dan apa itu hubungan transitif, kan? Relasi ekivalensi adalah relasi yang memenuhi ketiga properti tersebut.

Anda mungkin pernah mendengar tentang "penutupan transitif" dari suatu hubungan ? Yah, itu tidak lain adalah hubungan transitif setidaknya yang mencakup . Itulah arti istilah "penutupan". Demikian pula, Anda dapat berbicara tentang "penutupan simetris" dari suatu hubungan , "penutupan refleksif" dari suatu hubungan dan "penutupan ekivalensi" dari suatu hubungan dengan cara yang persis sama. $R$ $R$ $R$ $R$ $R$

Dengan beberapa pemikiran, Anda dapat meyakinkan diri sendiri bahwa penutupan transitif adalah . Penutupan simetris adalah . Penutupan refleksif adalah (di mana adalah hubungan identitas). $R$ $R \cup R^2 \cup R^3 \cup \ldots$ $R \cup R^{-1}$ $R \cup I$ $I$

Kami menggunakan notasi untuk . Ini adalah penutupan transitif refleksif dari . Sekarang perhatikan bahwa jika simetris, masing-masing hubungan , , , , ... adalah simetris. Karenanya juga akan simetris. $R^*$ $I \cup R \cup R^2 \cup \ldots$ $R$ $R$ $I$ $R$ $R^2$ $R^3$ $R^*$

Jadi penutupan ekivalen dari adalah penutupan transitif dari penutupan simetrisnya, yaitu, . Ini mewakili urutan langkah, beberapa di antaranya adalah langkah maju ( ) dan beberapa langkah mundur ( ). $R$ $(R \cup R^{-1})^*$ $R$ $R^{-1}$

Relasi dikatakan memiliki properti Church-Rosser jika penutupan ekivalensi sama dengan relasi komposit . Ini mewakili urutan langkah-langkah di mana semua langkah maju datang pertama, diikuti oleh semua langkah mundur. Jadi, properti Church-Rosser mengatakan bahwa setiap interleaving langkah maju dan mundur dapat dilakukan secara setara dengan melakukan langkah maju pertama dan langkah mundur nanti. $R$ $R^* (R^{-1})^*$

Uday Reddy
sumber

Jika Anda menambahkan satu kalimat terakhir untuk dikaitkan dengan pertanyaan, ini akan menjadi jawaban yang baik.

Raphael

Semuanya sangat mendasar sehingga orang sampai pada akhirnya dan bertanya-tanya "di mana jawabannya, sebenarnya?"

Marco Faustinelli