W jaki sposób powiązane są języki programowania i podstawy matematyki?

Zasadniczo mam świadomość trzech podstaw matematyki

1. Ustaw teorię
2. Teoria typów
3. Teoria kategorii

Więc w jaki sposób języki programowania i podstawy matematyki są powiązane?

EDYTOWAĆ

Pierwotne pytanie brzmiało: „Języki programowania oparte na podstawach matematyki”

z dodanym paragrafem

I implementacje teorii
1. Teoria typów w Coq
2. Teoria zbiorów w SETL
3. Teoria kategorii w Haskell

Na podstawie sugestii zmieniono to na „W jaki sposób języki programowania i podstawy matematyki są powiązane”

Ponieważ jest to jedno z tych pytań, w których nie wiedziałem wystarczająco dużo o to, o co pytam, ale chciałem się czegoś nauczyć, modyfikuję pytanie, aby było bardziej wartościowe dla nauki i innych, a jednocześnie pozostawiając szczegóły, aby nie tworzyć obecna odpowiedź Andreja Bauera wydaje się nie na temat.

Dzięki za wszystkie komentarze i dotychczasową odpowiedź. Uczę się od nich.

[Uwaga: akapity te są obecnie nieaktualne.] Tytuł twojego pytania zawiera nieuzasadnione założenie, że języki programowania są „oparte na podstawach matematyki”. Zasadniczo tak nie jest, chociaż te dwa obszary mają ważne relacje. Bardziej dokładnym stwierdzeniem byłoby, że (niektóre) języki programowania zostały zaprojektowane przy użyciu podstawowych technik. Lepszym pytaniem byłoby „w jaki sposób powiązane są języki programowania i podstawy matematyki?”

Najbardziej ogólne połączenie zawarte jest w sloganie proof-as-program , który może działać na kilka sposobów. Korespondencja Curry-Howard jest najbardziej oczywista. Dzięki niemu od razu łączymy teorię, logikę i programowanie typów. Należy jednak podkreślić, że korespondencja Curry-Howarda nie działa zbyt dobrze w przypadku ogólnej rekurencji (ponieważ każdy typ staje się zamieszkały), którą obsługuje każdy język programowania ogólnego przeznaczenia.

Subtelniejszym sposobem sprawienia, by hasło działało jako proof-as-programy, jest wykorzystanie wykonalności . Tutaj również odnosimy proofy i programy, ale teraz kierunek przechodzi od proofów do programów: każdy dowód daje program, ale nie każdy program jest koniecznie dowodem.

Głównym przykładem języka programowania opartego na fundamencie jest Agda , która jest po prostu implementacją teorii typów zależnych. Jednak Agda nie jest językiem programowania ogólnego, ponieważ nie obsługuje ogólnej rekursji. Każda funkcja w Agdzie jest sumą i istnieją funkcje obliczalne, których nie można zaimplementować w Agdzie. W praktyce programiści tego nie zauważą, ale zauważą, że Agda nie dopuszcza niezdefiniowanych wartości, na przykład nieskończonych pętli.

Coq to nie język programowania, ale raczej dowodem asystent. Ma jednak również możliwości ekstrakcji, które dają programy z dowodów. Proof asystentów i języków programowania nie należy mylić ze sobą.

Nie powinniśmy zapominać, że prolog i inne logiczne języki programowania czerpią inspirację z idei, że obliczenia są wyszukiwaniem dowodów . To oczywiście wiąże je ściśle z logiką.

Haskell to uniwersalny język programowania oparty na teorii domen . Innymi słowy, jego semantyka ma charakter teoretyczny, ponieważ musi uwzględniać funkcje cząstkowe i rekurencję. Społeczność Haskell opracowała szereg technik inspirowanych teorią kategorii, z których najlepiej znane są monady, ale nie należy ich mylić z monadami . Mówiąc bardziej ogólnie, zaawansowane funkcje programowania są zwykle traktowane za pomocą kombinacji teorii domen i teorii kategorii, ale nie jest to coś, do czego biegły jest programista Haskell na ulicy. Tak zwana „kategoria syntaktyczna” typów Haskella jest świeckim poglądem na to, w jaki sposób Haskell i teoria kategorii odpowiadają sobie nawzajem.

Teoria zbiorów (klasyczna lub konstruktywna) wydaje się inspirować pomysły w języku programowania w mniejszym stopniu. Oczywiście teoria mnogości konstruktywnych ma związek z programowaniem za pomocą logiki konstruktywnej. Jedno ważne zastosowanie intuicyjnej teorii zbiorów do języków programowania podał Alex Simpson, który wykorzystał ją do stworzenia syntetycznej teorii domen. Ale to dość zaawansowane rzeczy, może zobacz te slajdy . Jean-Louis Krivine opracował bardzo interesującą markę wykonalności dla klasycznej teorii zbiorów. Wydaje się to dobrym sposobem na powiązanie klasycznej teorii mnogości i programowania.

Podsumowując, teoria języków programowania wykorzystuje podstawowe techniki. Nie jest to zaskakujące, ponieważ uważamy obliczenia za podstawową koncepcję. Ale zbyt naiwne jest twierdzenie, że języki programowania są „oparte” na pewnych podstawach. W rzeczywistości trikotomia fundamentów „teoria zbiorów - teoria typów - teoria kategorii” jest po prostu użyteczną obserwacją na wysokim poziomie, którą można precyzyjnie matematycznie przedstawić na różne sposoby, ale nie ma w tym nic koniecznego. To historyczny wypadek.

jest to bardzo złożony temat i istnieje wiele świetnych książek na ten temat, jedna z nich nazywa się Katedra Turingsa, geneza wszechświata cyfrowego, a także silniki logiki, matematyków i geneza komputera .

języki komputerowe ewoluowały przez wiele dziesięcioleci, ale wierzcie lub nie, istnieją dwa oryginalne języki programowania, które pokazują, że matematyka i informatyka są ze sobą ściśle powiązane:

• Artykuł Turinga z 1936 r. Na temat problemu zatrzymania . teoretyczna konstrukcja rozwiązania problemu zaproponowana przez Hilberta na przełomie wieków, Entscheidungsproblem , tj. zautomatyzowana procedura rozwiązywania problemów matematycznych!

• Opracowany w tym samym czasie rachunek lambda Kościoła przetrwał w takich językach, jak seplenienie i schematy

są dwie kluczowe postacie, które przekroczyły granice matematyki i informatyki wrt „języków programowania”:

• teoria informacji zapoczątkowana przez Shannona pokazuje głębokie powiązania między matematyką a informatyką

• inną kluczową postacią, która krzyżuje matematykę z informatyką, jest von Neumann . wynalazł architekturę von Neumanna przechowywania programów w pamięci.

nawet wcześniejsze „języki programowania”:

• angielskie słowo „komputer” pierwotnie oznaczało coś więcej jak „kalkulator”, który używał operacji matematycznych na liczbach, a jego znaczenie znacznie zmieniło się w dzisiejszej koncepcji programowania ogólnego. więc istnieje związek między językami programowania a wczesnymi kalkulatorami.
• karty dziurkowania używane w krosnach tkackich z przełomu XIX i XX wieku były „językiem programowania” dla wzorów tkackich. zauważ, że karty dziurkowania były używane do programowania komputerów mainframe w latach sześćdziesiątych. były pierwotnie postrzegane jako „maszyny liczące” (wykorzystujące matematykę!), nie tyle nowoczesne komputery ogólnego zastosowania.
• Babbage i Ada Lovelace opracowali podstawowe koncepcje „języków programowania” w połowie XIX wieku na „silniku obliczeniowym”
• algebra boolowska była pierwotnie czysto matematyczną koncepcją wymyśloną przez Boole'a
• starożytny (liczący tysiące lat) liczydło do obliczeń matematycznych jest postrzegany jako prekursor współczesnego komputera. ale można powiedzieć, że operacje na nim były rodzajem „języka programowania” (po którym następowali ludzie)

jednak we współczesnych językach programowania wraz ze wzrostem i skalowaniem abstrakcji wyraźne, bezpośrednie połączenie z matematyką nieco się zmniejszyło na przestrzeni dziesięcioleci, ale zawsze będzie ono nieodłączne i pod pewnymi względami wzmocnione. na przykład języki takie jak Java ze ścisłymi typami mają powiązania z matematyką, a pod koniec lat 90. popularne języki komputerowe (np. c ++, Java, Ruby itp.) zaczęły jawnie implementować wiele matematycznych obiektów wyższego poziomu jako prawie prymitywne w języki, takie jak zestawy, drzewa (np. Btrees lub hashmaps) itp.