Korespondencja Curry-Howard - Curry–Howard correspondence

W programowaniu teorii języka i teoria dowodu The korespondencja Curry-Howard (znany również jako izomorfizmu Curry-Howard lub równoważności , albo dowody-as-programów i propositions- lub interpretacji formuł-as-typy ) jest bezpośredni związek między programami komputerowymi i dowody matematyczne .

Jest to uogólnienie analogii syntaktycznej między systemami logiki formalnej a rachunkiem obliczeniowym, które po raz pierwszy odkryli amerykański matematyk Haskell Curry i logik William Alvin Howard . Jest to powiązanie między logiką a obliczeniami, które zwykle przypisuje się Curry'emu i Howardowi, choć idea ta związana jest z operacyjną interpretacją logiki intuicjonistycznej, podawaną w różnych sformułowaniach przez LEJ Brouwera , Arenda Heytinga i Andreya Kołmogorowa (zob. interpretacja Brouwera-Heytinga-Kolmogorova ) i Stephena Kleene (patrz Możliwość realizacji ). Relacja została rozszerzona o teorię kategorii jako trójstronną korespondencję Curry-Howard-Lambek .

Pochodzenie, zakres i konsekwencje

Początki korespondencji Curry-Howarda leżą w kilku obserwacjach:

  1. W 1934 Curry zauważa, że typy kombinatorów mogą być postrzegane jako aksjomaty dla intuicjonistycznej logiki implikacyjnej.
  2. W 1958 roku zauważył, że pewien rodzaj systemu dowodowego , określany jako systemy dedukcji w stylu Hilberta , pokrywa się na pewnym fragmencie z typowanym fragmentem standardowego modelu obliczeń, znanego jako logika kombinatoryczna .
  3. W 1969 Howard zauważa, że ​​inny, bardziej „wysoki poziom” systemu dowodowego , określany jako naturalna dedukcja , może być bezpośrednio interpretowany w swojej intuicjonistycznej wersji jako typizowany wariant modelu obliczeniowego znanego jako rachunek lambda .

Innymi słowy, korespondencja Curry-Howard jest obserwacją, że dwie rodziny pozornie niepowiązanych ze sobą formalizmów – a mianowicie systemy dowodowe z jednej strony i modele obliczeniowe z drugiej – są w rzeczywistości tym samym rodzajem obiektów matematycznych.

Jeśli streszczamy specyfikę obu formalizmów, pojawia się następujące uogólnienie: dowód jest programem, a formuła, którą udowadnia, jest typem programu . Bardziej nieformalnie, można to traktować jako analogię, która stwierdza, że typ zwracany przez funkcję (tj. typ wartości zwracanych przez funkcję) jest analogiczny do twierdzenia logicznego, z zastrzeżeniem hipotez odpowiadających typom przekazywanych wartości argumentów do funkcji; i że program do obliczenia tej funkcji jest analogiczny do dowodu tego twierdzenia. To ustawia formę programowania logicznego na rygorystycznych podstawach: dowody mogą być reprezentowane jako programy, a zwłaszcza jako terminy lambda lub dowody mogą być uruchamiane .

Korespondencja była punktem wyjścia dla szerokiego spektrum nowych badań po jej odkryciu, prowadząc w szczególności do nowej klasy systemów formalnych zaprojektowanych do działania zarówno jako system dowodowy, jak i jako typizowany język programowania funkcjonalnego . Obejmuje Martin-LOF „s intuicjonistycznej typu teorii i Coquand ” s Rachunek konstrukcji , dwóch kamieni, w których dowody są regularne przedmiotem dyskursu, w którym można stwierdzić właściwości dowodów samo jak każdego programu. Ta dziedzina badań jest zwykle określana jako współczesna teoria typów .

Takie typizowane rachunki lambda wywodzące się z paradygmatu Curry-Howarda doprowadziły do ​​powstania oprogramowania takiego jak Coq, w którym dowody widziane jako programy mogą być sformalizowane, sprawdzane i uruchamiane.

Odwrotnym kierunkiem jest użycie programu do wyodrębnienia dowodu , biorąc pod uwagę jego poprawność — obszar badań ściśle związany z kodem przenoszącym dowód . Jest to wykonalne tylko wtedy, gdy język programowania, dla którego napisany jest program, jest bardzo bogato typowany: rozwój systemów tego typu był częściowo motywowany chęcią uczynienia korespondencji Curry-Howarda praktycznie istotną.

Korespondencja Curry-Howard podniosła również nowe pytania dotyczące obliczeniowej zawartości pojęć dowodowych, które nie zostały uwzględnione w oryginalnych pracach Curry'ego i Howarda. W szczególności wykazano , że logika klasyczna odpowiada zdolności do manipulowania kontynuacją programów i symetrii rachunku sekwencyjnego w celu wyrażenia dwoistości między dwiema strategiami oceny znanymi jako call-by-name i call-by-value.

Przypuszczalnie można oczekiwać, że korespondencja Curry-Howard doprowadzi do znacznego zjednoczenia logiki matematycznej z podstawową informatyką:

Logika w stylu Hilberta i dedukcja naturalna to tylko dwa rodzaje systemów dowodowych wśród dużej rodziny formalizmów. Alternatywne składnie obejmują rachunek sekwencyjny , sieci dowodowe , rachunek struktur itp. Jeśli przyjmie się korespondencję Curry-Howarda jako ogólną zasadę, że każdy system dowodowy ukrywa model obliczeń, teorię leżącą u podstaw nietypowej struktury obliczeniowej tego rodzaju dowodu system powinien być możliwy. Wtedy naturalnym pytaniem jest, czy o tych podstawowych obliczeniach obliczeniowych można powiedzieć coś interesującego matematycznie.

I odwrotnie, logika kombinatoryczna i po prostu typowany rachunek lambda nie są też jedynymi modelami obliczeń . Liniowa logika Girarda została opracowana na podstawie dokładnej analizy wykorzystania zasobów w niektórych modelach rachunku lambda; czy istnieje wpisana wersja maszyny Turinga, która zachowywałaby się jak system dowodowy? Typowane języki asemblerowe są takim przykładem "niskopoziomowych" modeli obliczeń, które przenoszą typy.

Ze względu na możliwość pisania programów niekończących, kompletne modele obliczeń Turinga (takie jak języki z dowolnymi funkcjami rekurencyjnymi ) muszą być interpretowane ostrożnie, ponieważ naiwne stosowanie korespondencji prowadzi do niespójnej logiki. Najlepszym sposobem radzenia sobie z arbitralnymi obliczeniami z logicznego punktu widzenia jest nadal aktywnie dyskutowana kwestia badawcza, ale jedno popularne podejście opiera się na użyciu monad do oddzielenia kodu, którego zakończenie można udowodnić, od potencjalnie niekończącego kodu (podejście, które również uogólnia na znacznie bogatsze modele obliczeń, a sam jest związany z logiką modalną przez naturalne rozszerzenie izomorfizmu Curry-Howarda). Bardziej radykalnym podejściem, zalecanym przez totalne programowanie funkcjonalne , jest wyeliminowanie nieograniczonej rekurencji (i rezygnacja z kompletności Turinga , chociaż nadal zachowująca wysoką złożoność obliczeniową), przy użyciu bardziej kontrolowanej kokurencji wszędzie tam, gdzie rzeczywiście pożądane jest zachowanie niekończące .

Ogólna formuła

W jego bardziej ogólnym sformułowaniu korespondencja Curry-Howard jest korespondencja między formalnych kamicy dowód i systemów typu dla modeli obliczeniowych . W szczególności dzieli się na dwie korespondencje. Jeden na poziomie formuł i typów, który jest niezależny od tego, który konkretny system dowodowy lub model obliczeniowy jest rozważany, oraz jeden na poziomie dowodów i programów, który tym razem jest specyficzny dla konkretnego wyboru systemu dowodowego i modelu obliczeniowego uważany za.

Na poziomie formuł i typów korespondencja mówi, że implikacja zachowuje się tak samo jak typ funkcji, koniunkcja jako typ „produktu” (może to być nazwane krotką, strukturą, listą lub innym terminem w zależności od języka ), alternatywę jako typ sumy (ten typ można nazwać unią), formułę false jako typ pusty i formułę true jako typ singleton (którego jedynym elementem składowym jest obiekt null). Kwantyfikatory odpowiadają zależnej przestrzeni funkcji lub produktom (odpowiednio). Jest to podsumowane w poniższej tabeli:

Strona logiczna Strona programowania
uniwersalna kwantyfikacja uogólniony typ produktu (typ Π)
egzystencjalna kwantyfikacja uogólniony typ sumy (typ Σ)
implikacja typ funkcji
spójnik Rodzaj produktu
dysjunkcja typ sumy
prawdziwa formuła typ jednostki
fałszywa formuła typ dolny

Na poziomie systemów dowodowych i modeli obliczeń korespondencja pokazuje głównie tożsamość struktury, po pierwsze, między niektórymi konkretnymi sformułowaniami systemów znanych jako system dedukcji w stylu Hilberta i logiką kombinatoryczną , a po drugie, między niektórymi konkretnymi sformułowaniami systemów znanych jako naturalna dedukcja i rachunek lambda .

Strona logiczna Strona programowania
System odliczeń w stylu Hilberta system typu dla logiki kombinatorycznej
odliczenie naturalne system typów dla rachunku lambda

Pomiędzy systemem dedukcji naturalnej a rachunkiem lambda zachodzą następujące zależności:

Strona logiczna Strona programowania
hipotezy wolne zmienne
eliminacja implikacji ( modus ponens ) podanie
wprowadzenie implikacji abstrakcja

Odpowiednie systemy

Systemy dedukcji w stylu Hilberta i logika kombinatoryczna

Była to na początku prosta uwaga w książce Curry'ego i Feysa z 1958 r. o logice kombinatorycznej: najprostsze typy podstawowych kombinatorów K i S logiki kombinatorycznej zaskakująco odpowiadały odpowiednim schematom aksjomatów α → ( βα ) i ( α → ( βγ )) → (( αβ ) → ( αγ )) stosowane w systemach dedukcji w stylu Hilberta . Z tego powodu schematy te są obecnie często nazywane aksjomatami K i S. Poniżej podano przykłady programów postrzeganych jako dowody w logice w stylu Hilberta .

Jeśli ograniczymy się do implikacyjnego fragmentu intuicjonistycznego, prosty sposób sformalizowania logiki w stylu Hilberta jest następujący. Niech Γ będzie skończonym zbiorem formuł, traktowanych jako hipotezy. Wtedy δ można wyprowadzić z Γ, oznaczanego Γ ⊢ δ, w następujących przypadkach:

  • δ jest hipotezą, czyli formułą Γ,
  • δ jest przykładem schematu aksjomatu; tj. w najbardziej powszechnym systemie aksjomatów:
    • δ ma postać α → ( βα ), lub
    • δ ma postać ( α → ( βγ )) → (( αβ ) → ( αγ )),
  • δ wynika z dedukcji, tj. dla niektórych α zarówno αδ jak i α są już wyprowadzalne z Γ (jest to reguła modus ponens )

Można to sformalizować za pomocą reguł wnioskowania , jak w lewej kolumnie poniższej tabeli.

Typowaną logikę kombinatoryczną można sformułować przy użyciu podobnej składni: niech Γ będzie skończonym zbiorem zmiennych, opatrzonym adnotacjami ich typów. Wyrażenie T (również z adnotacją typu) będzie zależał od tych zmiennych [Γ ⊢ T: δ ], gdy:

  • T jest jedną ze zmiennych w Γ,
  • T jest podstawowym kombinatorem; tj. zgodnie z najczęstszą podstawą kombinatora:
    • T to K: α → ( βα ) [gdzie α i β oznaczają rodzaje jego argumentów] lub
    • T to S:( α → ( βγ )) → (( αβ ) → ( αγ )),
  • T jest złożeniem dwóch podterminów, które zależą od zmiennych w Γ.

Zdefiniowane tutaj reguły generowania są podane w prawej kolumnie poniżej. Uwaga Curry'ego po prostu stwierdza, że ​​obie kolumny są w korespondencji jeden do jednego. Ograniczenie korespondencji do logiki intuicjonistycznej oznacza, że ​​niektóre klasyczne tautologie , takie jak prawo Peirce'a (( αβ ) → α ) → α , są wyłączone z korespondencji.

Intuicjonistyczna logika implikacyjna w stylu Hilberta Po prostu wpisana logika kombinacyjna

Patrząc na bardziej abstrakcyjnym poziomie, korespondencję można przeformułować, jak pokazano w poniższej tabeli. W szczególności twierdzenie o dedukcji specyficzne dla logiki w stylu Hilberta pasuje do procesu eliminacji abstrakcji z logiki kombinatorycznej.

Strona logiczna Strona programowania
założenie zmienny
aksjomaty kombinatory
modus ponens podanie
twierdzenie o dedukcji eliminacja abstrakcji

Dzięki korespondencji wyniki z logiki kombinatorycznej można przenieść na logikę w stylu Hilberta i odwrotnie. Na przykład pojęcie redukcji terminów w logice kombinatorycznej można przenieść do logiki w stylu Hilberta i zapewnia on sposób kanonicznego przekształcania dowodów w inne dowody tego samego stwierdzenia. Można również przenieść pojęcie normalnych terminów na pojęcie normalnych dowodów, wyrażając, że hipotezy aksjomatów nigdy nie muszą być całkowicie odłączone (ponieważ w przeciwnym razie może nastąpić uproszczenie).

I odwrotnie, niedowodliwość w logice intuicjonistycznej prawa Peirce'a można przenieść z powrotem do logiki kombinatorycznej: nie ma typowanego terminu logiki kombinatorycznej, który można by typować za pomocą typu

(( αβ ) → α ) → α .

Można również przenieść wyniki dotyczące kompletności niektórych zestawów kombinatorów lub aksjomatów. Na przykład fakt, że kombinator X stanowi jednopunktową podstawę (rozszerzającej) logiki kombinatorycznej implikuje, że pojedynczy schemat aksjomatu

((( α → ( βγ )) → (( αβ ) → ( αγ ))) → (( δ → ( εδ )) → ζ )) → ζ ,

który jest głównym typ z X , jest odpowiednia wymiana połączeniu ze schematów aksjomatów

α → ( βα ) i
( α → ( βγ )) → (( αβ ) → ( αγ )).

Odliczenie naturalne i rachunek lambda

Po tym, jak Curry podkreślił zgodność składniową między dedukcją w stylu Hilberta a logiką kombinatoryczną , Howard w 1969 wyraźnie przedstawił analogię składniową między programami prostego rachunku lambda i dowodami dedukcji naturalnej . Poniżej lewa strona formalizuje intuicjonistyczną implikacyjną dedukcję naturalną jako rachunek sekwencyjny (używanie sekwencji jest standardem w dyskusjach nad izomorfizmem Curry'ego-Howarda, ponieważ pozwala na bardziej przejrzyste sformułowanie reguł dedukcji) z niejawnym osłabieniem i prawym -strona strony pokazuje zasady typowania rachunku lambda . Po lewej stronie symbole Γ, Γ 1 i Γ 2 oznaczają uporządkowane sekwencje formuł, natomiast po prawej stronie sekwencje nazwanych (tj. wpisanych) formuł o wszystkich nazwach innych.

Intuicjonistyczna implikacyjna dedukcja naturalna Zasady przypisywania typów w rachunku lambda

Parafrazując korespondencję, dowodzenie Γ ⊢ α oznacza posiadanie programu, który przy danych wartościach z typami wymienionymi w Γ wytwarza obiekt typu α . Aksjomat odpowiada wprowadzeniu nowej zmiennej o nowym, nieograniczonym typie, reguła →  I odpowiada abstrakcji funkcji, a reguła →  E odpowiada zastosowaniu funkcji. Zauważmy, że zgodność nie jest dokładna, jeśli kontekst Γ przyjmuje się za zbiór formuł, jak np. λ- składniki λ xy . x i λ xY . y typu ααα nie zostałyby wyróżnione w korespondencji. Przykłady podano poniżej .

Howard wykazał, że korespondencja rozciąga się na inne spójniki logiki i inne konstrukcje prostego rachunku lambda. Na poziomie abstrakcyjnym korespondencja może być podsumowana, jak pokazano w poniższej tabeli. Zwłaszcza, ale również pokazuje, że pojęcie normalnych form w rachunku lambda meczy Prawitz pojęcie „s normalnego odliczenia w naturalnej dedukcji , z którego wynika, że algorytmy dla problemu typ osadnictwa może być przekształcony algorytmów decydując intuicjonistycznej dowodliwości.

Strona logiczna Strona programowania
aksjomat zmienny
wprowadzenie zasady konstruktor
zasada eliminacji burzyciel
normalne odliczenie normalna forma
normalizacja potrąceń słaba normalizacja
sprawdzalność typ problemu mieszkaniowego
tautologia intuicjonistyczna typ zamieszkany

Korespondencja Howarda naturalnie rozciąga się na inne rozszerzenia naturalnej dedukcji i po prostu typowany rachunek lambda . Oto niewyczerpująca lista:

Klasyczne operatory logiki i sterowania

W czasie Curry, a także w czasie Howard, korespondencji dowody-as-programy dotyczyły jedynie intuicjonistycznej logika , czyli logiki w którym w szczególności prawo Peirce'a było nie wywnioskować. Rozszerzenie korespondencji z prawem Peirce'a, a tym samym z logiką klasyczną, stało się jasne dzięki pracy Griffina nad operatorami typowania, które przechwytują kontekst oceny danego wykonania programu, tak aby ten kontekst oceny mógł być później ponownie zainstalowany. Podstawowa korespondencja stylu Curry-Howarda dla logiki klasycznej jest podana poniżej. Zwróć uwagę na zgodność między translacją podwójnej negacji używaną do mapowania klasycznych dowodów na logikę intuicjonistyczną a tłumaczeniem w stylu z przekazywaniem kontynuacji używanym do mapowania terminów lambda obejmujących kontrolę na terminy czyste lambda. Dokładniej, tłumaczenia w stylu przekazania kontynuacji call-by-name odnoszą się do tłumaczenia podwójnej negacji Kołmogorova , a tłumaczenia w stylu call-by-value z przekazywaniem kontynuacji odnoszą się do rodzaju tłumaczenia z podwójną negacją należnego Kurodzie.

Strona logiczna Strona programowania
Prawo Peirce'a : (( αβ ) → α ) → α rozmowa-z-aktualna-kontynuacja
tłumaczenie z podwójną negacją tłumaczenie w stylu przekazującym kontynuację

Lepsza korespondencja Curry'ego-Howarda istnieje dla logiki klasycznej, jeśli definiuje się logikę klasyczną nie przez dodanie aksjomatu, takiego jak prawo Peirce'a , ale przez dopuszczenie kilku wniosków w sekwencjach. W przypadku klasycznej dedukcji naturalnej istnieje zgodność dowodów jako programów z typowanymi programami rachunku λμ Parigota .

Rachunek sekwencyjny

Korespondencję dowodów jako programów można ustalić dla formalizmu znanego jako rachunek sekwencyjny Gentzena , ale nie jest to korespondencja z dobrze zdefiniowanym wcześniej istniejącym modelem obliczeń, jak miało to miejsce w przypadku dedukcji w stylu Hilberta i dedukcji naturalnych.

Rachunek sekwencyjny charakteryzuje się obecnością lewych reguł wstępnych, prawych reguł wstępnych oraz reguły cięcia, które można wyeliminować. Struktura rachunku sekwencyjnego odnosi się do rachunku, którego struktura jest zbliżona do struktury niektórych abstrakcyjnych maszyn . Korespondencja nieformalna wygląda następująco:

Strona logiczna Strona programowania
eliminacja cięcia redukcja w formie abstrakcyjnej maszyny
właściwe zasady wprowadzenia konstruktorzy kodu
lewe zasady wprowadzenia konstruktorzy stosów ewaluacyjnych
pierwszeństwo prawej strony w eliminacji przecięcia redukcja call-by-name
pierwszeństwo po lewej stronie w eliminacji przecięcia redukcja call-by-value

Powiązane dokumenty jako programy korespondencji

Rola de Bruijn

NG de Bruijn użył notacji lambda do reprezentowania dowodów sprawdzania twierdzeń Automath i reprezentował twierdzenia jako „kategorie” swoich dowodów. Było to pod koniec lat 60., w tym samym czasie Howard napisał swój rękopis; de Bruijn prawdopodobnie nie wiedział o pracy Howarda i niezależnie podawał korespondencję (Sørensen i Urzyczyn [1998] 2006, s. 98–99). Niektórzy badacze mają tendencję do używania terminu korespondencja Curry-Howard-de Bruijn zamiast korespondencji Curry-Howard.

Interpretacja BHK

Interpretacja BHK interpretuje intuicjonistycznej dowody jak funkcje, ale nie określa klasę funkcji istotnych dla interpretacji. Jeśli weźmiemy rachunek lambda dla tej klasy funkcji, to interpretacja BHK mówi to samo, co zależność Howarda między naturalną dedukcją a rachunkiem lambda.

Realizowalność

KLEENE „s rekurencyjnych realizowalności Dzieli dowody intuicjonistycznej arytmetyki do pary funkcji rekurencyjnej i dowodu formuły wyrażającej że rekurencyjna funkcja«uświadamia», czyli poprawnie wystąpienie o zachwianiu i egzystencjalne kwantyfikatorów z pierwotnej formuły tak, że formuła ją prawda.

Kreisel jest zmodyfikowany Realność dotyczy intuicjonistycznej wyższego rzędu logiki bazowego i pokazuje, że po prostu wpisane termin N indukcyjnie ekstrahowano z dowodu realizuje wstępny formuły. W przypadku logiki zdań pokrywa się ona ze stwierdzeniem Howarda: wyodrębniony wyraz lambda jest samym dowodem (postrzeganym jako nieopisany wyraz lambda), a stwierdzenie realizowalności jest parafrazą faktu, że wyodrębniony wyraz lambda ma taki sam typ, jak wzór oznacza (postrzegane jako typ).

Gödel „s interpretacja Dialectica realizuje (rozszerzenie) intuicjonistycznej arytmetyczna z funkcji obliczeniowych. Związek z rachunkiem lambda jest niejasny, nawet w przypadku dedukcji naturalnej.

Korespondencja Curry-Howard-Lambek

Joachim Lambek wykazał na początku lat siedemdziesiątych, że dowody intuicjonistycznej logiki zdań i kombinatory typizowanej logiki kombinatorycznej mają wspólną teorię równań, którą jest teoria kartezjańskich kategorii zamkniętych . Wyrażenie korespondencja Curry-Howard-Lambek jest obecnie używane przez niektórych ludzi w odniesieniu do trójstronnego izomorfizmu między logiką intuicjonistyczną, typizowanym rachunkiem lambda i kartezjańskimi kategoriami domkniętymi, przy czym obiekty są interpretowane jako typy lub zdania, a morfizmy jako terminy lub dowody. Korespondencja działa na poziomie równań i nie jest wyrazem identyczności składniowej struktur, jak to ma miejsce w przypadku każdej z korespondencji Curry'ego i Howarda: tj. struktura dobrze zdefiniowanego morfizmu w kategorii kartezjańsko-zamkniętej nie jest porównywalna z struktura dowodu odpowiedniego sądu w logice w stylu Hilberta lub w dedukcji naturalnej. Aby wyjaśnić to rozróżnienie, poniżej przedstawiono przeformułowaną strukturę składniową kartezjańskich kategorii zamkniętych.

Obiekty (typy) są definiowane przez

  • jest przedmiotem
  • jeśli α i β są obiektami, to i są obiektami.

Morfizmy (terminy) są definiowane przez

  • , , , i są morfizmami
  • jeśli t jest morfizmem, λ t jest morfizmem
  • jeśli t i u są morfizmami i są morfizmami.

Dobrze zdefiniowane morfizmy (terminy typowane) są definiowane przez następujące reguły typowania (w których zwykła notacja kategorycznego morfizmu jest zastępowana notacją sekwencyjną ).

Tożsamość:

Kompozycja:

Typ jednostki ( obiekt terminala ):

Produkt kartezjański:

Projekcja lewa i prawa:

Curry :

Zastosowanie :

Wreszcie równania kategorii to

  • (jeśli dobrze napisane)

Z równań tych wynikają następujące -prawa:

Otóż ​​istnieje t takie, że iff można udowodnić w implikacyjnej logice intuicjonistycznej.

Przykłady

Dzięki korespondencji Curry-Howarda, wpisane wyrażenie, którego typ odpowiada formule logicznej, jest analogiczne do dowodu tej formuły. Oto przykłady.

Kombinator tożsamości jako dowód αα w logice Hilberta

Jako przykład rozważmy dowód twierdzenia αα . W rachunku lambda jest to typ funkcji tożsamości I = λ x . xw logice kombinatorycznej funkcję tożsamości uzyskuje się przez zastosowanie S = λ fgx . fx ( gx ) dwa razy do K = λ xy . x . Oznacza to, że I = (( S K ) K ) . Jako opis dowodu mówi się, że następujące kroki mogą być użyte do udowodnienia αα :

  • wykonaj instancję drugiego schematu aksjomatu wzorami α , βα i α, aby uzyskać dowód ( α → (( βα ) → α )) → (( α → ( βα )) → ( αα ) ) ,
  • utwórz instancję pierwszego schematu aksjomatu raz z α i βα, aby uzyskać dowód α → (( βα ) → α ) ,
  • wykonaj instancję pierwszego schematu aksjomatu po raz drugi za pomocą α i β , aby uzyskać dowód α → ( βα ) ,
  • zastosuj modus ponens dwukrotnie, aby uzyskać dowód αα

Ogólnie procedura polega na tym, że ilekroć program zawiera aplikację formularza ( P Q ), należy postępować zgodnie z następującymi krokami:

  1. Najpierw udowodnij twierdzenia odpowiadające typom P i Q .
  2. Ponieważ P stosuje się do Q , typ P musi mieć formę αβ , a typ Q musi mieć formę α dla niektórych α i β . Dlatego możliwe jest oddzielenie wniosku β , poprzez regułę modus ponens.

Kombinator składu widziany jako dowód ( βα ) → ( γβ ) → γα w logice stylu Hilberta

Jako bardziej skomplikowany przykład spójrzmy na twierdzenie, które odpowiada funkcji B. Typ B to ( βα ) → ( γβ ) → γα . B jest równa ( S ( K S ) K ). To jest nasza mapa drogowa dla dowodu twierdzenia ( βα ) → ( γβ ) → γα .

Pierwszy krok polega na konstrukcji ( K S ). Aby poprzednik aksjomatu K wyglądał jak aksjomat S , ustaw α równe ( αβγ ) → ( αβ ) → αγ , a β równe δ (aby uniknąć zderzeń zmiennych):

K  : αβα
K [ α = ( αβγ ) → ( αβ ) → αγ , β = δ] : (( αβγ ) → ( αβ ) → αγ ) → δ → ( αβγ ) → ( αβ ) → αγ

Ponieważ poprzednikiem jest tutaj po prostu S , następnik można odłączyć za pomocą Modus Ponens:

KS  : δ → ( αβγ ) → ( αβ ) → αγ

Jest to twierdzenie odpowiadające typowi ( K S ). Teraz zastosuj S do tego wyrażenia. Biorąc S w następujący sposób

S  : ( αβγ ) → ( αβ ) → αγ ,

umieścić α = δ , β = αβγ , i γ = ( αβ ) → αγ , otrzymując

S [ α = δ , β = αβγ , γ = ( αβ ) → αγ ] : ( δ → ( αβγ ) → ( αβ ) → αγ ) → ( δ → ( αβγ )) → δ → ( αβ ) → αγ

a następnie odłącz następnik:

S (KS)  : ( δαβγ ) → δ → ( αβ ) → αγ

Jest to wzór na typ ( S ( K S )). Specjalny przypadek tego twierdzenia ma δ = ( βγ ) :

S (KS) [ δ = βγ ] : (( βγ ) → αβγ ) → ( βγ ) → ( αβ ) → αγ

Ta ostatnia formuła musi być zastosowana do K . Specjalizują K , tym razem przez zastąpienie α z ( βy ) i β z α :

K  : αβα
K [ α = βγ , β = α ] : ( βγ ) → α → ( βγ )

Jest to to samo, co poprzednik wcześniejszej formuły, więc odłączając następnik:

S (KS) K  : ( βγ ) → ( αβ ) → αγ

Zamiana nazw zmiennych α i γ daje nam

( βα ) → ( γβ ) → γα

co pozostało do udowodnienia.

Normalny dowód ( βα ) → ( γβ ) → γα w naturalnej dedukcji widzianej jako λ-term

Poniższy diagram daje dowód ( βα ) → ( γβ ) → γα w naturalnej dedukcji i pokazuje, jak można to zinterpretować jako wyrażenie λ λ abg .( a ( b g ) )) typu ( βα ) → ( γβ ) → γα .

                                     a:β → α, b:γ → β, g:γ ⊢ b : γ → β    a:β → α, b:γ → β, g:γ ⊢ g : γ
———————————————————————————————————  ————————————————————————————————————————————————————————————————————
a:β → α, b:γ → β, g:γ ⊢ a : β → α      a:β → α, b:γ → β, g:γ ⊢ b g : β
————————————————————————————————————————————————————————————————————————
               a:β → α, b:γ → β, g:γ ⊢ a (b g) : α
               ————————————————————————————————————
               a:β → α, b:γ → β ⊢ λ g. a (b g) : γ → α
               ————————————————————————————————————————
                        a:β → α ⊢ λ b. λ g. a (b g) : (γ → β) -> γ → α
                        ————————————————————————————————————
                                ⊢ λ a. λ b. λ g. a (b g) : (β → α) -> (γ → β) -> γ → α

Inne aplikacje

Ostatnio zaproponowano izomorfizm jako sposób definiowania podziału przestrzeni poszukiwań w programowaniu genetycznym . Metoda indeksuje zestawy genotypów (drzewa programowe wyewoluowane przez system GP) przez ich izomorficzny dowód Curry-Howarda (określany jako gatunek).

Jak zauważył dyrektor badawczy INRIA Bernard Lang, korespondencja Curry-Howard stanowi argument przeciwko patentowalności oprogramowania: ponieważ algorytmy są dowodami matematycznymi, zdolność patentowa pierwszego z nich oznaczałaby patentowalność drugiego. Twierdzenie może być własnością prywatną; matematyk musiałby zapłacić za korzystanie z niego i zaufać firmie, która go sprzedaje, ale zachowuje w tajemnicy dowód i odrzuca odpowiedzialność za ewentualne błędy.

Uogólnienia

Wymienione tu korespondencje sięgają znacznie dalej i głębiej. Na przykład zamknięte kategorie kartezjańskie są uogólniane przez zamknięte kategorie monoidalne . Wewnętrzny język z tych kategorii jest liniowy układ typu (odpowiadające logiki liniowego ), która jest uogólnieniem prostu wpisany lambda nazębnym języku wewnętrznym kartezjańskiego zamkniętych kategorii. Co więcej, można wykazać, że odpowiadają one kobordyzmom , które odgrywają istotną rolę w teorii strun .

Rozszerzony zestaw równoważności jest również badany w teorii typów homotopii , która stała się bardzo aktywnym obszarem badań około 2013 r. i od 2018 r. nadal jest. W tym przypadku teoria typów jest rozszerzona o aksjomat jednoznaczności („równoważność jest równoważna równości”), który pozwala na wykorzystanie teorii typu homotopii jako podstawy dla całej matematyki (w tym teorii mnogości i logiki klasycznej, zapewniając nowe sposoby omawiania aksjomatu wybór i wiele innych rzeczy). Oznacza to, że zgodność Curry-Howard, że dowody są elementami zamieszkałych typów, jest uogólniona do pojęcia homotopicznej równoważności dowodów (jako ścieżki w przestrzeni, typ tożsamościowy lub typ równości w teorii typów interpretowany jako ścieżka).

Bibliografia

Najważniejsze referencje

  • Curry, HB (1934-09-20). „Funkcjonalność w logice kombinatorycznej” . Materiały Narodowej Akademii Nauk Stanów Zjednoczonych Ameryki . 20 (11): 584–90. Kod bib : 1934PNAS...20..584C . doi : 10.1073/pnas.20.11.584 . ISSN  0027-8424 . PMC  1076489 . PMID  16577644 .
  • Curry, Haskell B; Feys, Robert (1958). Craig, William (red.). Logika kombinatoryczna . Studia z logiki i podstaw matematyki. 1 . Wydawnictwo Północnej Holandii. LCCN  a59001593 ; z dwiema sekcjami Craiga, Williama; patrz paragraf 9ECS1 maint: postscript ( link )
  • De Bruijn, Nicolaas (1968), Automath, język matematyki , Wydział Matematyki, Politechnika w Eindhoven, raport TH 68-WSK-05. Przedruk w poprawionej formie, z dwustronicowym komentarzem, w: Automation and Reasoning, vol. 2, Classical papers on computational logic 1967–1970 , Springer Verlag, 1983, s. 159–200.
  • Howard, William A. (wrzesień 1980) [oryginalny rękopis papierowy z 1969], "The formuły-jako typy pojęcie konstrukcji", w Seldin, Jonathan P .; Hindley, J. Roger (red.), To HB Curry: Eseje o logice kombinatorycznej , Rachunek Lambda i formalizm , Academic Press , s. 479-490, ISBN 978-0-12-349050-6.

Rozszerzenia korespondencji

  1. ^ B Pfenning, Frank; Davies, Rowan (2001), „Sądowa rekonstrukcja logiki modalnej” (PDF) , Struktury matematyczne w informatyce , 11 (4): 511–540, CiteSeerX  10.1.1.43.1611 , doi : 10.1017/S0960129501003322 , S2CID  16467268
  2. ^ Davies, Rowan; Pfenning, Frank (2001), „Modalna analiza obliczeń etapowych” (PDF) , Journal of the ACM , 48 (3): 555-604, CiteSeerX  10.1.1.3.5442 , doi : 10.1145/382780.382785 , S2CID  52148006
  • Griffin, Timothy G. (1990), „Pojęcie formuły jako typy kontroli”, Konf. Rekordowy 17. doroczny Symp ACM. on Principles of Programming Languages, POPL '90, San Francisco, CA, USA, 17-19 stycznia 1990 , s. 47-57, doi : 10.1145/96709.96714 , ISBN 978-0-89791-343-0, S2CID  3005134.
  • Parigot, Michel (1992), „Lambda-mu-calculus: Algorytmiczna interpretacja klasycznej dedukcji naturalnej”, Międzynarodowa konferencja na temat programowania logicznego i automatycznego rozumowania: LPAR '92 Proceedings, St. Petersburg, Rosja , Notatki do wykładu z informatyki, 624 , Springer-Verlag , s. 190-201, ISBN 978-3-540-55727-2.
  • Herbelin, Hugo (1995), "Struktura lambda-rachunek izomorficzna do gentzenskiej struktury rachunku sekwencyjnego", w Pacholski, Leszek; Tiuryn, Jerzy (red.), Computer Science Logic, 8. Międzynarodowe Warsztaty, CSL '94, Kazimierz, Polska, 25-30 września 1994, Selected Papers , Lecture Notes in Computer Science, 933 , Springer-Verlag , s. 61– 75, ISBN 978-3-540-60017-6.
  • Gabbay, Dov; de Queiroza, Ruy (1992). „Rozszerzenie interpretacji Curry-Howarda do liniowych, odpowiednich i innych logik zasobów”. Dziennik Logiki Symbolicznej . Dziennik logiki symbolicznej . 57 . s. 1319–1365. doi : 10.2307/2275370 . JSTOR  2275370 .. (Pełna wersja artykułu zaprezentowana na Logic Colloquium '90 , Helsinki. Abstract in JSL 56(3):1139-1140, 1991.)
  • de Queiroza, Ruy; Gabbay, Dov (1994), "Równość w oznaczonych systemach dedukcyjnych i funkcjonalnej interpretacji równości zdań", w Dekker, Paul; Stokhof, Martin (red.), Proceedings of the Ninth Amsterdam Colloquium , ILLC / Wydział Filozofii Uniwersytetu w Amsterdamie, s. 547-565, ISBN 978-90-74795-07-4.
  • de Queiroza, Ruy; Gabbay, Dov (1995), „Funkcjonalna interpretacja kwantyfikatora egzystencjalnego” , Biuletyn grupy interesów w logice czystej i stosowanej , 3 , s. 243-290. (Pełna wersja artykułu przedstawionego na Logic Colloquium '91 , Uppsala. Abstract in JSL 58(2):753-754, 1993.)
  • de Queiroza, Ruy; Gabbay, Dov (1997), "Funkcjonalna interpretacja konieczności modalnej", w de Rijke, Maarten (red.), Postępy w logice intensjonalnej , Applied Logic Series, 7 , Springer-Verlag , s. 61-91, ISBN 978-0-7923-4711-8.
  • de Queiroza, Ruy; Gabbay, Dov (1999), "Oznaczone odliczenie naturalne" , w Ohlbach, Hans-Juergen; Reyle, Uwe (red.), Logika, język i rozumowanie. Eseje na cześć Dova Gabbay , Trends in Logic, 7 , Kluwer, s. 173-250, ISBN 978-0-7923-5687-5.
  • de Oliveira, Anjolina; de Queiroz, Ruy (1999), „Procedura normalizacji dla równania fragmentu oznaczonej dedukcji naturalnej”, Logic Journal of the Interest Group in Pure and Applied Logics , 7 , Oxford University Press , s. 173-215. (Pełna wersja artykułu przedstawionego na 2nd WoLLIC'95 , Recife. Abstract in Journal of the Interest Group in Pure and Applied Logics 4(2):330-332, 1996.)
  • Poernomo, Iman; Crossley, John; okablowanie; Martin (2005), Adaptacja Proofs-as-Programs: The Curry-Howard Protocol , Monografie w informatyce , Springer , ISBN 978-0-387-23759-6, dotyczy adaptacji syntezy programów dowodowych jako programów do gruboziarnistych i imperatywnych problemów programistycznych, za pomocą metody, którą autorzy nazywają protokołem Curry-Howarda. Zawiera omówienie korespondencji Curry-Howard z perspektywy informatyki.
  • de Queiroz, Ruy JGB; de Oliveira, Anjolina (2011), „Funkcjonalna interpretacja obliczeń bezpośrednich”, Electronic Notes in Theoretical Computer Science , Elsevier , 269 : 19-40, doi : 10.1016/j.entcs.2011.03.003. (Pełna wersja artykułu przedstawionego na LSFA 2010 , Natal, Brazylia.)

Interpretacje filozoficzne

Papiery syntetyczne

Książki

Dalsza lektura

Zewnętrzne linki