Beta normal shakli - Beta normal form

In lambda hisobi, muddat ichida beta normal shakli agar yo'q bo'lsa beta-versiyani kamaytirish mumkin.^[1] Muddat beta-eta normal shakli agar na beta pasayish, na an eta kamaytirish mumkin. Muddat bosh normal shakli agar yo'q bo'lsa bosh holatida beta-redeks.

Beta versiyasini kamaytirish

Lambda hisobida, a beta redeks shaklning muddati:

${ displaystyle ( mathbf { lambda} x.A) M}$.

Redex ${ displaystyle r}$ ichida bosh holati bir muddatda ${ displaystyle t}$, agar ${ displaystyle t}$ quyidagi shaklga ega (dastur abstraktsiyaga qaraganda ustuvor ahamiyatga ega ekanligini va quyidagi formula dastur emas, balki lambda-abstraktsiyani anglatishini unutmang):

${ displaystyle lambda x_ {1} ldots lambda x_ {n}. underbrace {( lambda xA) M_ {1}} _ {{ text {redex}} r} M_ {2} ldots M_ {m}}$, qayerda ${ displaystyle n geq 0}$ va ${ displaystyle m geq 1}$.

A beta-versiyani kamaytirish atamada keltirilgan beta redeksga quyidagi qayta yozish qoidasini qo'llash:

${ displaystyle ( mathbf { lambda} x.A) M longrightarrow A [x: = M]}$

qayerda ${ displaystyle A [x: = M]}$ atamani almashtirish natijasidir ${ displaystyle M}$ o'zgaruvchi uchun ${ displaystyle x}$ muddatda ${ displaystyle A}$.

A bosh beta-reduksiya - bu bosh holatida qo'llaniladigan beta-reduksiya, ya'ni quyidagi shaklda:

${ displaystyle lambda x_ {1} ldots lambda x_ {n}. ( lambda xA) M_ {1} M_ {2} ldots M_ {m} longrightarrow lambda x_ {1} ldots lambda x_ {n} .A [x: = M_ {1}] M_ {2} ldots M_ {m}}$, qayerda ${ displaystyle n geq 0}$ va ${ displaystyle m geq 1}$.

Boshqa har qanday pasayish an ichki beta-versiyani kamaytirish.

A normal shakl hech qanday beta redeksni o'z ichiga olmagan atama, ya'ni buni yanada kamaytirish mumkin emas. A bosh normal shakli bosh holatida beta redeksni o'z ichiga olmaydigan atama, ya'ni bundan keyin boshni qisqartirish bilan kamaytirish mumkin emas. Oddiy lambda hisob-kitobini ko'rib chiqishda (masalan, doimiy yoki funktsional belgilar qo'shilmasdan, qo'shimcha delta qoidasi bilan kamaytirilishi kerak), oddiy bosh shakllar quyidagi shaklning shartlari hisoblanadi:

${ displaystyle lambda x_ {1} ldots lambda x_ {n} .xM_ {1} M_ {2} ldots M_ {m}}$, qayerda ${ displaystyle x}$ o'zgaruvchan, ${ displaystyle n geq 0}$ va ${ displaystyle m geq 0}$.

Boshning normal shakli har doim ham normal shakl emas, chunki qo'llanilgan argumentlar ${ displaystyle M_ {j}}$ normal bo'lishi shart emas. Biroq, bu teskari: har qanday normal shakl ham bosh normal shakldir. Darhaqiqat, normal shakllar subtermlar bo'lgan bosh normal shakllardir ${ displaystyle M_ {j}}$ o'zlarining normal shakllari. Bu normal shakllarning induktiv sintaktik tavsifini beradi.

Qo'shimcha tushuncha mavjud zaif bosh normal shakli (whnf): atama mavjud whnf agar u dastur bo'lmasa va u doimiy yoki funktsiya belgisi bilan boshlanmasa. ${ displaystyle mathbf { lambda} x.M}$ ichida whnf chunki bu mavhumlik. ${ displaystyle 1 + 2}$ emas whnf chunki u funktsiya belgisi bilan boshlanadi, ya'ni ${ displaystyle +}$.

Kamaytirish strategiyasi

Umuman olganda, ushbu atama bir nechta redekslarni o'z ichiga olishi mumkin, shuning uchun bir nechta turli xil beta reduktsiyalar qo'llanilishi mumkin. Biz belgilashimiz mumkin strategiya qaysi redeksni kamaytirishni tanlash.

• Oddiy tartibda qisqartirish bu strategiya bo'lib, unda har doim ham bunday pasayish mumkin bo'lmaguncha, bosh holatini beta-versiyada qisqartirish qoidasi qo'llaniladi. O'sha paytda, natijada olingan atama normal shaklda bo'ladi. Keyin subtermiyalarda boshni qisqartirishni qo'llash davom etmoqda ${ displaystyle M_ {j}}$, chapdan o'ngga. Boshqacha qilib aytganda, buyurtmalarni normal qisqartirish - bu har doim chap, eng tashqi va eng redekslarni kamaytiradigan strategiya.
• Aksincha, ichida amaliy buyurtmani qisqartirish, birinchi navbatda ichki qisqartirishni qo'llaydi, so'ngra faqat ichki qisqartirish mumkin bo'lmaganda boshni qisqartirishni qo'llaydi.

Oddiy tartibni qisqartirish tugallandi, agar atama boshning normal shakliga ega bo'lsa, unda normal tartibni qisqartirish oxir-oqibat unga etadi. Yuqoridagi normal shakllarning sintaktik tavsifiga ko'ra, bu "to'liq" normal shakl uchun bir xil bayonotga olib keladi (bu standartlashtirish teoremasi ). Aksincha, amaldagi buyurtmani qisqartirish, hatto muddat odatdagi shaklga ega bo'lsa ham, tugamasligi mumkin. Masalan, amaldagi buyurtmani qisqartirish yordamida quyidagi qisqartirishlar ketma-ketligi mumkin:

${ displaystyle { begin {aligned} & ( mathbf { lambda} xz) (( lambda w.www) ( lambda w.www)) rightarrow & ( lambda xz) (( lambda w .www) ( lambda w.www) ( lambda w.www)) rightarrow & ( lambda xz) (( lambda w.www) ( lambda w.www) ( lambda w.www) ( lambda w.www)) rightarrow & ( lambda xz) (( lambda w.www) ( lambda w.www) ( lambda w.www) ( lambda w.www) ( lambda) w.www)) & ldots end {aligned}}}$

Ammo odatdagi buyurtmani qisqartirishdan foydalanib, xuddi shu boshlang'ich nuqtasi odatdagi shaklga tezda kamayadi:

${ displaystyle ( mathbf { lambda} x.z) (( lambda w.www) ( lambda w.www))}$

${ displaystyle rightarrow z}$

Sinotniki rejissyor torlari beta-kamaytirishning hisoblash murakkabligini optimallashtirish mumkin bo'lgan usullardan biridir.

Shuningdek qarang

• Lambda hisobi
• Oddiy shakl (ajralish)

Adabiyotlar