Głębokie łącze porównujące dowody matematyczne i programy komputerowe | Magazyn Quanta

Niektóre odkrycia naukowe mają znaczenie, ponieważ ujawniają coś nowego — na przykład podwójną spiralną strukturę DNA lub istnienie czarnych dziur. Jednakże niektóre odkrycia są głębokie, ponieważ pokazują, że dwie stare koncepcje, kiedyś uważane za odrębne, w rzeczywistości są takie same. Weźmy równania Jamesa Clerka Maxwella pokazujące, że elektryczność i magnetyzm to dwa aspekty tego samego zjawiska lub powiązania grawitacji z zakrzywioną czasoprzestrzenią w ogólnej teorii względności.

Korespondencja Curry-Howard robi to samo, ale na większą skalę, łącząc nie tylko oddzielne koncepcje w ramach jednej dziedziny, ale całe dyscypliny: Computer Science i logika matematyczna. Znany również jako izomorfizm Curry'ego-Howarda (termin oznaczający, że istnieje pewien rodzaj zgodności jeden do jednego między dwiema rzeczami), ustanawia powiązanie między dowodami matematycznymi a programami komputerowymi.

Mówiąc najprościej, korespondencja Curry'ego-Howarda zakłada, że ​​dwa pojęcia z informatyki (typy i programy) są równoważne, odpowiednio, twierdzeniom i dowodom - pojęciom z logiki.

Jedną z konsekwencji tej korespondencji jest to, że programowanie – często postrzegane jako rzemiosło osobiste – zostaje wyniesione do wyidealizowanego poziomu matematyki. Pisanie programu to nie tylko „kodowanie”, to akt udowodnienia twierdzenia. To formalizuje czynność programowania i zapewnia sposoby matematycznego wnioskowania o poprawności programów.

Korespondencja nosi imię dwóch badaczy, którzy ją niezależnie odkryli. W 1934 roku matematyk i logik Haskell Curry zauważył podobieństwo między funkcjami w matematyce a relacją implikacji w logice, która przybiera formę zdań „jeśli-to” między dwoma zdaniami.

Zainspirowany obserwacjami Curry'ego logik matematyczny William Alvin Howard odkrył w 1969 roku głębsze powiązanie między obliczeniami a logiką, pokazując, że uruchamianie programu komputerowego przypomina upraszczanie dowodu logicznego. Kiedy program komputerowy jest uruchomiony, każda linia jest „oceniana” w celu uzyskania pojedynczego wyniku. Podobnie w dowodzie zaczynasz od złożonych stwierdzeń, które możesz uprościć (na przykład eliminując zbędne kroki lub zastępując złożone wyrażenia prostszymi), aż dojdziesz do wniosku — bardziej skondensowanego i zwięzłego stwierdzenia wywodzącego się z wielu tymczasowych stwierdzeń .

Chociaż ten opis oddaje ogólny sens korespondencji, aby go w pełni zrozumieć, musimy dowiedzieć się nieco więcej o tym, co informatycy nazywają „teorią typów”.

Zacznijmy od słynnego paradoksu: we wsi mieszka fryzjer, który goli wszystkich mężczyzn, którzy nie golą się sami, i tylko ich. Czy fryzjer goli się sam? Jeśli odpowiedź brzmi tak, to nie wolno mu się golić (ponieważ goli tylko mężczyzn, którzy sami się nie golą). Jeśli odpowiedź brzmi nie, to musi się ogolić (bo goli wszystkich mężczyzn, którzy się nie golą). Jest to nieformalna wersja paradoksu odkrytego przez Bertranda Russella podczas próby ustalenia podstaw matematyki za pomocą pojęcia zwanego zbiorami. Oznacza to, że nie da się zdefiniować zbioru zawierającego wszystkie zbiory, które same siebie nie zawierają, bez napotkania sprzeczności.

Aby uniknąć tego paradoksu, jak pokazał Russell, możemy użyć „typów”. Z grubsza są to kategorie, których określone wartości nazywane są obiektami. Na przykład, jeśli istnieje typ o nazwie „Nat”, oznaczający liczby naturalne, jego obiektami są 1, 2, 3 i tak dalej. Badacze zazwyczaj używają dwukropka do oznaczenia typu obiektu. Liczbę 7 typu całkowitego można zapisać jako „7: liczba całkowita”. Możesz mieć funkcję, która pobiera obiekt typu A i wypluwa obiekt typu B, lub taką, która łączy parę obiektów typu A i typu B w nowy typ, zwany „A × B”.

Dlatego jednym ze sposobów rozwiązania tego paradoksu jest umieszczenie tych typów w hierarchii, tak aby mogły zawierać jedynie elementy „niższego poziomu” niż one same. Wtedy typ nie może zawierać siebie, co pozwala uniknąć samoodniesienia, które tworzy paradoks.

W świecie teorii typów udowodnienie, że stwierdzenie jest prawdziwe, może wyglądać inaczej niż to, do czego jesteśmy przyzwyczajeni. Jeśli chcemy udowodnić, że liczba całkowita 8 jest parzysta, to chodzi nam o pokazanie, że 8 rzeczywiście jest obiektem określonego typu zwanego „Parzystym”, gdzie regułą przynależności jest podzielność przez 2. Po sprawdzeniu, że 8 jest podzielne na podstawie 2 możemy stwierdzić, że 8 rzeczywiście jest „mieszkańcem” typu Parzysty.

Curry i Howard wykazali, że typy są zasadniczo równoważne zdaniami logicznymi. Kiedy funkcja „zamieszkuje” typ — to znaczy, kiedy można pomyślnie zdefiniować funkcję będącą obiektem tego typu — skutecznie pokazujesz, że odpowiadające jej twierdzenie jest prawdziwe. Zatem funkcje, które przyjmują dane wejściowe typu A i dają wyjście typu B, oznaczone jako typ A → B, muszą odpowiadać implikacji: „Jeśli A, to B”. Weźmy na przykład zdanie: „Jeśli pada deszcz, oznacza to, że ziemia jest mokra”. W teorii typów zdanie to byłoby modelowane za pomocą funkcji typu „Deszcz → GroundIsWet”. Różnie wyglądające formuły są w rzeczywistości matematycznie takie same.

Choć to powiązanie może brzmieć abstrakcyjnie, nie tylko zmieniło ono sposób, w jaki praktycy matematyki i informatyki myślą o swojej pracy, ale także doprowadziło do kilku praktycznych zastosowań w obu dziedzinach. Dla informatyki zapewnia teoretyczne podstawy weryfikacji oprogramowania, czyli procesu zapewnienia poprawności oprogramowania. Ujmując pożądane zachowania w logiczne propozycje, programiści mogą matematycznie udowodnić, że program zachowuje się zgodnie z oczekiwaniami. Zapewnia również mocne podstawy teoretyczne do projektowania potężniejszych funkcjonalnych języków programowania.

A w matematyce korespondencja doprowadziła do narodzin asystenci dowodowi, zwane także interaktywnymi dowodami twierdzeń. Są to narzędzia programowe pomagające w konstruowaniu dowodów formalnych, takie jak Coq i Lean. W Coq każdy etap dowodu jest zasadniczo programem, a ważność dowodu jest sprawdzana za pomocą algorytmów sprawdzania typu. Matematycy również korzystają z asystentów dowodu — w szczególności z Dowód twierdzenia Leana — sformalizowanie matematyki, co wiąże się z przedstawianiem pojęć matematycznych, twierdzeń i dowodów w rygorystycznym formacie możliwym do sprawdzenia komputerowego. Pozwala to na sprawdzenie czasami nieformalnego języka matematyki za pomocą komputerów.

Naukowcy wciąż badają konsekwencje tego powiązania między matematyką a programowaniem. Oryginalna korespondencja Curry'ego-Howarda łączy programowanie z rodzajem logiki zwanej logiką intuicjonistyczną, ale okazuje się, że takim unifikacjom można poddać również więcej typów logiki.

„To, co wydarzyło się w ciągu stulecia od spostrzeżenia Curry’ego, polega na tym, że wciąż odkrywamy coraz więcej przypadków, w których „system logiczny X odpowiada systemowi obliczeniowemu Y” – powiedział Michaela Clarksona, informatyk z Cornell University. Badacze powiązali już programowanie z innymi typami logiki, takimi jak logika liniowa, która obejmuje pojęcie „zasobów”, oraz logikę modalną, która zajmuje się pojęciami możliwości i konieczności.

I chociaż w tej korespondencji znajdują się nazwiska Curry'ego i Howarda, w żadnym wypadku nie są oni jedynymi, którzy ją odkryli. To potwierdza fundamentalny charakter korespondencji: ludzie wciąż na nowo ją zauważają. „Wydaje się, że to nie przypadek, że istnieje głęboki związek między obliczeniami a logiką” – stwierdził Clarkson.