Wpisany rachunek lambda

Wpisany ) rachunek lambda to formalizm wpisany , który używa symbolu lambda ( $do$ oznaczenia anonimowej abstrakcji funkcji W tym kontekście typy są zwykle obiektami o charakterze syntaktycznym, które są przypisane terminom lambda; dokładny charakter typu zależy od rozważanego rachunku różniczkowego (patrz rodzaje poniżej). Z pewnego punktu widzenia typowane rachunki lambda można postrzegać jako udoskonalenia nietypowanego rachunku lambda , ale z innego punktu widzenia można je również uznać za bardziej fundamentalną teorię i nietypowany rachunek lambda specjalny przypadek z tylko jednym typem.

Typowane rachunki lambda są podstawowymi językami programowania i są podstawą typowanych funkcjonalnych języków programowania, takich jak ML i Haskell , a także, bardziej pośrednio, typowanych imperatywnych języków programowania . Typowane rachunki lambda odgrywają ważną rolę w projektowaniu systemów typów dla języków programowania; tutaj typowalność zwykle oddaje pożądane właściwości programu (np. program nie spowoduje naruszenia dostępu do pamięci).

Wpisane rachunki lambda są ściśle związane z logiką matematyczną i teorią dowodu poprzez izomorfizm Curry'ego-Howarda i można je uznać za wewnętrzny język klas kategorii ; np. prosty typ rachunku lambda jest językiem zamkniętych kategorii kartezjańskich (CCC).

Rodzaje typowanych rachunków lambda

Zbadano różne typowane rachunki lambda. Rachunek lambda o prostym typie $ma$$tylko$ jeden konstruktor typu strzałkę , a jego jedynymi typami są i typy funkcji System T rozszerza prosty typ rachunku lambda o rodzaj liczb naturalnych i pierwotną rekurencję wyższego rzędu; w tym systemie wszystkie funkcje dające się udowodnić rekurencyjnie w arytmetyce Peano są definiowalne. System F pozwala na polimorfizm przy użyciu uniwersalnej kwantyfikacji dla wszystkich typów; z logicznego punktu widzenia może opisywać wszystkie funkcje, które są możliwe do udowodnienia w logice drugiego rzędu . Rachunki lambda z typami zależnymi są podstawą intuicjonistycznej teorii typów , rachunku konstrukcji i struktury logicznej (LF), czystego rachunku lambda z typami zależnymi. Opierając się na pracy Berardiego nad systemami typu czystego , Henk Barendregt zaproponował kostkę Lambda usystematyzować relacje czysto typowanych rachunków lambda (w tym rachunku lambda typu prostego, Systemu F, LF i rachunku konstrukcji).

$jest$ rachunki lambda wprowadzają pojęcie podtypów , $tj$$.$ jeśli podtypem typu to wszystkie terminy typu $mają$ również Wpisane rachunki lambda z podtypami to po prostu wpisany rachunek lambda z typami koniunkcyjnymi i Systemem F _<: .

Wszystkie wymienione do tej pory systemy, z wyjątkiem nieopisanego rachunku lambda, są silnie normalizujące : wszystkie obliczenia kończą się. Dlatego nie mogą opisać wszystkich obliczalnych przez Turinga . Inną konsekwencją jest to, że są one spójne jako logika, tj. istnieją typy niezamieszkałe. Istnieją jednak typowane rachunki lambda, które nie są silnie normalizujące. Na przykład rachunek lambda typu zależnego z typem wszystkich typów (typ: typ) nie normalizuje się z powodu paradoksu Girarda . Ten system jest również najprostszym systemem typu czystego, formalizmem, który uogólnia kostkę Lambda. Systemy z jawnymi kombinatorami rekurencji, takie jak „ Język programowania funkcji obliczeniowych ” (PCF) Plotkina , nie są normalizujące, ale nie mają być interpretowane jako logika. Rzeczywiście, PCF jest prototypowym, funkcjonalnym językiem programowania, w którym typy są używane w celu zapewnienia, że ​​programy działają dobrze, ale niekoniecznie, że się kończą.

Aplikacje do języków programowania

W programowaniu komputerowym procedury (funkcje, procedury, metody) języków programowania o silnym typie ściśle odpowiadają typowanym wyrażeniom lambda.

Zobacz też

• Rachunek kappa — odpowiednik typowanego rachunku lambda, który wyklucza funkcje wyższego rzędu

Dalsza lektura

•   Barendregt, Henk (1992). „Rachunki lambda z typami” . W Abramsky, S. (red.). Tło: Struktury obliczeniowe . Podręcznik logiki w informatyce . Tom. 2. Oxford University Press. s. 117–309. ISBN 9780198537618 .
• Brandl, Helmut (2022). Rachunek konstrukcyjny / Wpisany rachunek lambda