Rachunek lambda-mu - Lambda-mu calculus

W matematycznej logiki i informatyki The rachunek lambda-mu jest przedłużeniem rachunku lambda wprowadzony przez M. PARIGOT. Wprowadza dwa nowe operatory: operator μ (który jest zupełnie inny zarówno od operatora μ występującego w teorii obliczalności, jak i operatora μ rachunku modalnego μ ) i operatora nawiasu. Teoretycznie udowadnia , że dostarcza grzecznego sformułowania klasycznej dedukcji naturalnej .

Jednym z głównych celów tego rozszerzonego rachunku różniczkowego jest umiejętność opisu wyrażeń odpowiadających twierdzeniom w logice klasycznej . Zgodnie z izomorfizmem Curry-Howarda , sam rachunek lambda może wyrażać twierdzenia tylko w logice intuicjonistycznej , a kilku klasycznych twierdzeń logicznych nie można w ogóle napisać. Jednak dzięki tym nowym operatorom można pisać terminy, które mają typ np . Prawa Peirce'a .

Pod względem semantycznym operatory te odpowiadają kontynuacjom , które można znaleźć w niektórych funkcjonalnych językach programowania .

Definicja formalna

Możemy rozszerzyć definicję wyrażenia lambda, aby uzyskać jedno w kontekście rachunku lambda-mu. Trzy główne wyrażenia występujące w rachunku lambda są następujące:

1. V , zmienna , gdzie V to dowolny identyfikator .
2. λV.E , abstrakcja , gdzie V to dowolny identyfikator, a E to dowolne wyrażenie lambda.
3. (EE ′) , aplikacja , gdzie E i E ' ; są dowolnymi wyrażeniami lambda.

Aby uzyskać szczegółowe informacje, zapoznaj się z odpowiednim artykułem .

Oprócz tradycyjnych zmiennych λ, rachunek lambda-mu zawiera odrębny zestaw zmiennych μ. Tych μ-zmiennych można używać do nazywania lub zamrażania dowolnych podterminów, co pozwala nam później abstrakcyjnie opisywać te nazwy. Zestaw terminów zawiera terminy nienazwane (wszystkie tradycyjne wyrażenia lambda są tego rodzaju) i nazwane . Terminy dodane przez rachunek lambda-mu mają postać:

1. [α] t to termin nazwany, gdzie α jest zmienną μ, a t jest terminem nienazwanym.
2. (μ α. E) to termin nienazwany, gdzie α to zmienna μ, a E to termin nazwany.

Zmniejszenie

Podstawowe zasady redukcji stosowane w rachunku lambda-mu są następujące:

logiczna redukcja

${\ Displaystyle (\ lambda xu) v \; \ triangleright _ {c} \; u [v / x]}$

redukcja strukturalna

${\ Displaystyle (\ mu \ beta. u) v \; \ triangleright _ {c} \; \ mu \ beta. u \ lewo [[\ beta] (wv) / [\ beta] w \ prawej]}$

zmiana nazwy

${\ Displaystyle [\ alfa] \ mu \ beta. u \; \ triangleright _ {c} \; u [\ alfa / \ beta]}$

odpowiednik redukcji η

${\ displaystyle \ mu \ alpha. [\ alpha] u \; \ triangleright _ {c} \; u}$ , ponieważ α nie występuje swobodnie w u

Te zasady powodują, że rachunek różniczkowy jest konfluentny . Można by dodać dalsze zasady redukcji, aby zapewnić nam silniejsze pojęcie formy normalnej, chociaż byłoby to kosztem konfluencji.

Zobacz też

• Klasyczne systemy typu czystego do typowanych uogólnień rachunków lambda z kontrolą

Bibliografia

Linki zewnętrzne

• Odpowiednia dyskusja Lambda-mu na temat Lambda the Ultimate.