Jakie są teoretyczne podstawy programowania imperatywnego?

Programowanie funkcjonalne ma teoretyczne podstawy w rachunku lambda i logice kombinatorycznej . Jako osoba zajmująca się obliczeniami statystycznymi uważam te koncepcje za bardzo przydatne do modelowania.

Czy istnieje równoważna matematyczna podstawa programowania imperatywnego , czy może po prostu wyrosła z praktycznej aplikacji sprzętowej w języku maszynowym i późniejszego rozwoju FORTRAN ?

Ogólnie rzecz biorąc, gdy matematyka jest wykorzystywana do badania niektórych X , najpierw trzeba mieć model X , a następnie opracować teorię, zestaw wyników na temat tego modelu. Chyba, że teoria może być uznane za „podstawy teoretyczne” dla X . Teraz ustaw X = obliczenia. Istnieje wiele modeli obliczeń, z których wiele obejmuje „stan”. Każdy model ma swoją „teorię” i czasami można „tłumaczyć” między modelami. Uważam, że trudno powiedzieć, który model jest bardziej „podstawowy” - są one po prostu zaprojektowane z myślą o różnych celach.

Maszyny Turinga zostały zaprojektowane w celu zdefiniowania, co jest obliczalne . Tworzą więc dobry model, jeśli zależy Ci na tym, czy istnieje algorytm dla określonego problemu. Ten model jest czasem nadużywany do badania wydajności algorytmów lub twardości problemów, pod pretekstem, że jest wystarczająco dobry, przynajmniej jeśli dbasz tylko o wielomian / nie-wielomian. Model pamięci RAM jest bliższy prawdziwemu komputerowi i dlatego jest lepszy, jeśli chcesz precyzyjnej analizy algorytmu. Aby postawić dolne granice twardości problemów, lepiej nieużyj modelu, który zbytnio przypomina dzisiejsze komputery, ponieważ chcesz objąć szeroką gamę możliwych komputerów, a jednocześnie być bardziej precyzyjnym niż zwykły wielomian / nie-wielomian. W tym kontekście widziałem na przykład zastosowany model sondy komórkowej.

Jeśli zależy Ci na poprawności , przydatne są jeszcze inne modele. Tutaj masz semantykę operacyjną (która powiedziałbym, że jest to analogiczny rachunek lambda dla stanowych obliczeń), semantykę aksomatyczną (opracowaną w 1969 r. Przez Hoare'a na podstawie indukcyjnych twierdzeń Floyda z 1967 r., Które są spopularyzowane przez Knutha w sztuce programowania komputerowego , tom 1) i inne.

Podsumowując, myślę , że szukasz modeli obliczeniowych. Istnieje wiele takich modeli, opracowanych z myślą o różnych celach, a wiele z nich ma stan, więc odpowiadają one programowaniu imperatywnemu. Jeśli chcesz wiedzieć, czy coś da się obliczyć, spójrz na maszyny Turinga. Jeśli zależy Ci na wydajności, spójrz na modele pamięci RAM. Jeśli zależy Ci na poprawności, spójrz na modele zakończone „semantyką”, takie jak semantyka operacyjna.

Na koniec, pozwól mi wspomnieć, że jest duża książka online tylko o modelach obliczeniowych Johna Savage'a. Chodzi przede wszystkim o wydajność. W części dotyczącej poprawności zalecam zacząć od klasycznych artykułów Floyda (1967) , Hoare (1969) , Dijkstra (1975) i Plotkin (1981) . Wszystkie są całkiem fajne.

Najprostszym teoretycznym modelem programu imperatywnego jest sama maszyna Turinga. Zawiera zarówno istotne komponenty programu imperatywnego: nieograniczony modyfikowalny stan, jak i maszynę stanu, która na nim działa.

Programowanie imperatywne można również uziemić w programowanie funkcjonalne, uznając programy za kompozycje operacji monadycznych, które przekazują i zwracają zmodyfikowane wersje stanu globalnego, tak jak w języku programowania Haskell.

Krótko mówiąc, powiedziałbym, że programowanie imperatywne wywodzi się z języka maszynowego i praktyki programowania. Z drugiej strony monady zapewniają odpowiednie ramy semantyczne do opisu semantyki cech imperatywnego języka programowania. Artykuł Pojęcia obliczeń i monady Moggiego stworzył podstawy formalne. Phil Wadler spopularyzował ten pomysł i znacząco przyczynił się do tego, że był kluczowym sposobem włączenia funkcji imperatywnych w język programowania Haskell. Najnowsze prace Plotkina i pojęcia mocy obliczeniowej określają monady idzie w drugą stronę, stwierdzając, że niektóre, ale nie wszystkie, pojęcia (imperatywnego) obliczenia faktycznie dają monadę, co oznacza, że ​​w bardzo istotny sposób monady odpowiadają imperatywnym (i innym) pojęciom obliczeniowym.

Jeśli szukasz rygorystycznego matematycznego traktowania imperatywnego języka programowania, przykładem tego jest książka Winskela „Formalna semantyka języków programowania” (1993).

W książce definiuje imperatywny język programowania o nazwie IMP i zapewnia jego operacyjną, denotacyjną i aksjomatyczną semantykę.

Spóźniam się na to pytanie, ale jest to fascynujące pytanie. Oto moje poglądy.

Kiedy byłem studentem, mieliśmy świetnego profesora matematyki, który wykładał nam historię i rozwój matematyki. Według niego matematyka rozwijała się w falach „ekspansji” i „konsolidacji”. Podczas fazy ekspansji rozważano i badano nowe pomysły, które wcześniej były nieznane. Następnie, w fazie konsolidacji, nowe teorie zostały zintegrowane z istniejącym zasobem wiedzy. Jednak w XX wieku, powiedział, ekspansja i konsolidacja odbywają się równolegle.

Programowanie imperatywne jest obecnie działaniem rozszerzającym dla matematyki. Wcześniej było to „nieznane”. (To może nie być do końca prawdą. Hoare mówi nam , że Euclid robił coś w rodzaju programowania imperatywnego w swojej geometrii. Ale matematyka straciła zainteresowanie, na dobre i na złe.) Matematyki wciąż nie są zainteresowani programowaniem imperatywnym. Tyle straty dla nich. Ale uważam całą informatykę za gałąź matematyki w sensie abstrakcyjnym. Studiujemy to, poszerzając matematykę.

Nie przejmowałbym się więc szczególnie, czy istnieje a priori teoretyczna podstawa programowania imperatywnego. Jeśli nie ma, pozwól nam go znaleźć. To, co wiemy, mówi nam już, że programowanie imperatywne jest fantastycznie głębokie i piękne. Funkcjonalne programowanie blednie w porównaniu. Ale mamy wiele do zrobienia, aby przekazać całą tę teorię ludziom.

Programowanie funkcjonalne ma wyraźną podstawę w matematyce, ponieważ funkcjonalne języki programowania ewoluowały równolegle z odpowiednią matematyką, a ich projektanci zwykle bardzo ją cenili. Silny i bezpośredni związek jest samospełniającą się przepowiednią.

Programowanie imperatywne ma znacznie bardziej niechlujną historię, która jest znacznie ściślej związana z problemami biznesowymi i inżynierskimi i historycznie była bardziej zainteresowana wydajnością kompilatorów i generowanego przez nie kodu, niż przestrzeganiem formalizmów matematycznych.

Wiele osób próbowało wyjaśnić programowanie imperatywne w (tradycyjnie) kategoriach funkcjonalnych. Może to być najbliżej tego, czego możemy się spodziewać, ale te próby są zawsze niezręczne, żmudne, kryminalistyczne. Jestem prawie pewien, że wolałbym oderwać oczy od twarzy, niż czytać dowód postępu / zachowania dla CLR.

Zwykle, jeśli dojdziesz do końca porządnego podręcznika (np. Typy i języki programowania Pierce'a), zaczniesz widzieć formalne modelowanie imperatywnych funkcji językowych. To może być dla ciebie interesujące.

An Axiomatic Basis for Computer Programming przez CAR HOARE

W tym artykule podjęto próbę zbadania logicznych podstaw programowania komputerowego za pomocą technik, które zostały po raz pierwszy zastosowane w badaniach geometrii, a następnie zostały rozszerzone na inne gałęzie matematyki. Obejmuje to wyjaśnienie zbiorów aksjomatów i reguł wnioskowania, które mogą być wykorzystane w dowodach właściwości programów komputerowych. Podano przykłady takich aksjomatów i reguł oraz przedstawiono formalny dowód na proste twierdzenie. Na koniec argumentuje się, że ważne korzyści, zarówno teoretyczne, jak i praktyczne, mogą wynikać z realizacji tych tematów.

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=rep1&type=pdf

Po drugie, co powiedział Alexandre, że maszyna Turinga stanowiła oryginalną teoretyczną podstawę programowania imperatywnego. W zakresie, w jakim organizacja imperatywnych języków programowania odzwierciedla architekturę maszyny, myślę, że praca Johna von Neumanna byłaby również kluczową częścią ich teoretycznych podstaw.

Czy istnieje równoważna matematyczna podstawa programowania imperatywnego, czy po prostu wyrosła z praktycznej aplikacji sprzętowej w języku maszynowym i późniejszego rozwoju FORTRAN?

Jeśli masz na myśli „podstawę” w sensie historycznym, myślę, że nie ma „równoważnej podstawy matematycznej”. Jednak pomimo tego, że programowanie imperatywne wyrosło z praktycznych problemów, istnieje kilka sposobów kompleksowego scharakteryzowania znaczenia programowania imperatywnego na sposoby, które mogą okazać się „przydatne do modelowania”, takie jak logika Hoare'a .

posty, które wspominają o logice hoare i logice separacji, są poprawne w tej sprawie. Logika Hoare pozwala określić właściwości całej konfiguracji sterty programu, a logika separacji jest nowocześniejszym krewnym, który pozwala na użycie „koniunkcji separującej”, która pozwala określić jako warunek wstępny i końcowy segmentu kodu, dla którego właściwości część sterty, którą będzie manipulować segment programu podczas kwantyfikacji w pozostałej części sterty.

Odpowiedź dotycząca monad nie jest ściśle ścisła, ponieważ w haskell monada jest używana tylko dlatego, że jest abstrakcją, która umożliwia kodowanie kolejności ograniczeń oceny i wyraźne śledzenie właściwości „może użyć IO”.

Warto podkreślić zarówno, że logikę Hoare / Separacji można postrzegać jako monady, oraz że istnieje wiele współczesnych projektów, takich jak Ynot Project na Harvardzie, które badają te tematy.

badania w logice separacji są ciągłą i aktywną dziedziną.

Do tego pytania dochodzę jeszcze później, ale jestem nim równie zafascynowany.

Unika mnie, dlaczego teoria programowania imperatywnego jest mniej ugruntowana niż teoria programowania funkcjonalnego. Prawdopodobnie zaczęło to poważnie traktować Scott i de Bakkera w 1969 r. Wraz z analizą znaczenia rekurencji w prostym języku imperatywnym [1]. Gdy imperatywny język zyskuje na znaczeniu, historia staje się nieco bardziej chaotyczna, ale jest to tylko cena, którą trzeba zapłacić za bycie bliżej metalu. Aby wymienić jeden z bardziej kompleksowych działań, w 1980 r. De Bakker, de Bruin i Zucker napisali monografię na ten temat [2]. Inne zostały wspomniane powyżej. Te odniesienia do logiki separacji przed datą, ale [2] dotyczą jednak tablic i wzajemnie rekurencyjnych procedur.

[1]: niepublikowany w 1969 r., Ale pojawił się jako Jaco W. de Bakker i Dana S. Scott. Teoria programów , strony 1-30. W Klop i in. JW de Bakker, 25 lat temu. CWI, Amsterdam, 1989. Liber Amoricum.

[2]: Jacobus W. de Bakker, Arie de Bruin, Jeffrey Zucker: Matematyczna teoria poprawności programu. Prentice Hall 1980.

Krótko po zadaniu pytania Mark Bender z McMaster University opublikował tezę: Assignment Calculus: A Pure Imperative Reasoning Language (8 września 2010 r.). Teza ta opisuje prosty, imperatywny język odpowiadający rachunku lambda.

Rachunek przydziału składa się tylko z czterech podstawowych konstrukcji, przydziału X:=t, sekwencji t;u, tworzenia ¡tprocedur i wywoływania procedur !t. Dla AC podano trzy interpretacje: semantykę operacyjną, semantykę denotacyjną i system przepisywania terminów. Wszystkie trzy są równoważne.

Teza Mark Bender kontynuuje eksplorację wariantów rozszerzonych o leniwą ocenę, cofanie się, skład procedury. Jest to podobne do badania rachunku lambda za pomocą małych rozszerzeń.

Podsumowując, teza stanowi stosunkowo bezpośrednią odpowiedź na pytanie PO.