Ta definicja jest lepsza od tej, którą podałem w poprzedniej odpowiedzi, ponieważ jest zwięzła i bardziej ogólna. Ale może być trudniej zrozumieć, ponieważ implikacje twierdzeń o niekompletności mających zastosowanie do programowania i życia w ogólności są trudne dla ludzi, aby otoczyli umysł.
Deklaratywny kontra imperatywny
Właściwość deklaratywna jest dziwna, tępa i trudna do uchwycenia w technicznie precyzyjnej definicji, która pozostaje ogólna i niejednoznaczna, ponieważ jest to naiwne przekonanie, że możemy zadeklarować znaczenie (aka semantyka) programu bez powodowania niezamierzonych skutków ubocznych. Istnieje nieodłączne napięcie między wyrażaniem znaczenia a unikaniem niezamierzonych efektów, a napięcie to faktycznie wywodzi się z twierdzeń o niekompletności programowania i naszego wszechświata.
Uproszczenie, nieprecyzyjne technicznie i często dwuznaczne jest definiowanie deklaratywnego jako „ co robić ”, a imperatywnego jako „ jak to zrobić ” . Niejednoznacznym przypadkiem jest „ co ” to „ jak ” w programie, który generuje program - kompilator.
Najwyraźniej nieograniczona rekurencja, która sprawia, że język Turinga jest kompletny , jest również analogicznie w semantyce - nie tylko w składniowej strukturze oceny (czyli semantyce operacyjnej). Jest to logicznie przykład analogiczny do twierdzenia Gödla - „ każdy kompletny system aksjomatów jest również niespójny ”. Zastanów się nad sprzecznością tego cytatu! Jest to także przykład, który pokazuje, w jaki sposób wyrażenie semantyki nie ma możliwego do udowodnienia ograniczenia, dlatego nie możemy udowodnić 2, że program (i analogicznie jego semantyka) zatrzymał aka twierdzenie Haltinga.
Twierdzenia o niekompletności wywodzą się z fundamentalnej natury naszego wszechświata, który, jak stwierdzono w Drugim Prawie Termodynamiki, brzmi „ entropia (czyli # niezależnych możliwości) na zawsze osiąga maksimum ”. Kodowanie i projektowanie programu nigdy się nie kończy - żyje! - ponieważ stara się zaspokoić potrzeby świata rzeczywistego, a semantyka świata rzeczywistego ciągle się zmienia i zyskuje na popularności. Ludzie nigdy nie przestają odkrywać nowych rzeczy (w tym błędów w programach ;-).
Aby precyzyjnie i technicznie uchwycić wyżej wspomniane pożądane pojęcie w tym dziwnym wszechświecie, który nie ma krawędzi (zastanów się, że! Nie ma „na zewnątrz” naszego wszechświata), wymagana jest zwięzła, ale zwodniczo-prosta definicja, która zabrzmi nieprawidłowo, dopóki nie zostanie wyjaśniona głęboko.
Definicja:
Właściwość deklaratywna to miejsce, w którym może istnieć tylko jeden możliwy zestaw instrukcji, które mogą wyrażać każdy konkretny semantyczny moduł.
Właściwością imperatywną 3 jest dualność, w której semantyka jest niespójna w składzie i / lub może być wyrażona za pomocą odmian zestawów instrukcji.
Ta definicja deklaratywna jest wyraźnie lokalna w zakresie semantycznym, co oznacza, że wymaga, aby semantyczny modułowy zachowywał swoje spójne znaczenie niezależnie od tego, gdzie i jak jest tworzony i stosowany w zakresie globalnym . Zatem każdy deklaratywny modułowy semantyczny powinien być z natury ortogonalny dla wszystkich możliwych innych - i nie być niemożliwym (z powodu twierdzeń o niekompletności) globalnym algorytmem lub modelem służącym do obserwowania spójności, co jest również punktem „ Profesora Roberta Harpera „ Więcej nie zawsze jest lepsze ” informatyki na Carnegie Mellon University, jednym z projektantów Standard ML.
Przykłady tej modułowej semantyki deklaratywnej obejmują funktory teorii kategorii, np .Applicative Typowanie nominalne, przestrzenie nazw, nazwane pola i wrt do poziomu operacyjnego semantyki, a następnie czystego programowania funkcjonalnego.
Tak więc dobrze zaprojektowane języki deklaratywne mogą wyraźniej wyrażać znaczenie , choć z pewną utratą ogólności w tym, co można wyrazić, ale zyskiem w tym, co można wyrazić z wewnętrzną spójnością.
Przykładem wyżej wymienionej definicji jest zestaw formuł w komórkach programu arkusza kalkulacyjnego - które nie powinny mieć takiego samego znaczenia po przeniesieniu do różnych komórek kolumny i wiersza, tj. Zmianie identyfikatorów komórek. Identyfikatory komórek są częścią zamierzonego znaczenia i nie są zbyteczne. Dlatego wynik każdego arkusza kalkulacyjnego jest unikalny dla identyfikatorów komórek w zestawie formuł. Spójnym semantycznym modułem w tym przypadku jest użycie identyfikatorów komórek jako danych wejściowych i wyjściowych funkcji czystych dla formuł komórek (patrz poniżej).
Hyper Text Markup Language, czyli HTML - język statycznych stron internetowych - jest przykładem bardzo (ale nie idealnie 3 ) języka deklaratywnego, który (przynajmniej przed HTML 5) nie był w stanie wyrazić zachowania dynamicznego. HTML jest chyba najłatwiejszym językiem do nauki. W celu zachowania dynamicznego imperatywny język skryptowy, taki jak JavaScript, był zwykle łączony z HTML. HTML bez JavaScript pasuje do deklaratywnej definicji, ponieważ każdy typ nominalny (tj. Tagi) zachowuje swoje spójne znaczenie w składzie zgodnie z regułami składni.
Konkurencyjną definicją deklaratywną są przemienne i idempotentne właściwości instrukcji semantycznych, tzn. Że instrukcje można zmieniać i duplikować bez zmiany znaczenia. Na przykład instrukcje przypisujące wartości do nazwanych pól mogą być ponownie uporządkowane i powielone bez zmiany znaczenia programu, jeśli te nazwy są modularne wrt w dowolnej dorozumianej kolejności. Nazwy czasami sugerują kolejność, np. Identyfikatory komórek obejmują ich pozycję kolumny i wiersza - przeniesienie sumy w arkuszu kalkulacyjnym zmienia jego znaczenie. W przeciwnym razie właściwości te domyślnie wymagają globalnegospójność semantyki. Zasadniczo niemożliwe jest zaprojektowanie semantyki instrukcji, więc pozostają one spójne, jeśli są losowo uporządkowane lub powielane, ponieważ kolejność i duplikacja są nieodłączne od semantyki. Na przykład stwierdzenia „Foo istnieje” (lub konstrukcja) i „Foo nie istnieje” (i zniszczenie). Jeśli weźmie się pod uwagę przypadkową niekonsekwencję endemiczną za zamierzoną semantykę, wówczas uznaje się tę definicję za wystarczająco ogólną dla właściwości deklaratywnej. Zasadniczo definicja ta jest pusta jako definicja uogólniona, ponieważ próbuje ona uczynić spójność ortogonalną względem semantyki, tj. Przeciwstawić się temu, że wszechświat semantyki jest dynamicznie nieograniczony i nie może być ujęty w paradygmacie globalnej spójności.
Wymaganie komutatywnych i idempotentnych właściwości (porządek oceny strukturalnej) semantyki operacyjnej niższego poziomu przekształca semantykę operacyjną w deklaratywną zlokalizowaną modularną semantyczną, np. Czyste programowanie funkcjonalne (w tym rekurencyjne zamiast pętli imperatywnych). Następnie kolejność operacyjna szczegółów implementacji nie wpływa (tj. Rozprzestrzenia się globalnie ) na spójność semantyki wyższego poziomu. Na przykład kolejność oceny (i teoretycznie także powielania) formuł arkusza kalkulacyjnego nie ma znaczenia, ponieważ dane wyjściowe nie są kopiowane do danych wejściowych, dopóki nie zostaną obliczone wszystkie dane wyjściowe, tj. Analogicznie do funkcji czystych.
C, Java, C ++, C #, PHP i JavaScript nie są szczególnie deklaratywne. Składnia Copute'a i Pythona są bardziej deklaratywnie sprzężone z zamierzonymi wynikami , tj. Spójną semantyką składniową, która eliminuje obce, dzięki czemu można łatwo zrozumieć kod po zapomnieniu. Copute i Haskell egzekwują determinizm semantyki operacyjnej i zachęcają do „ nie powtarzania się ” (DRY), ponieważ pozwalają jedynie na paradygmat funkcjonalny.
2 Nawet tam, gdzie możemy udowodnić semantykę programu, np. Za pomocą języka Coq, jest to ograniczone do semantyki wyrażanej podczas pisania , a pisanie nigdy nie może uchwycić całej semantyki programu - nawet w przypadku języków, które są niekompletność Turinga, np. HTML + CSS, można wyrazić niespójne kombinacje, które mają w ten sposób niezdefiniowaną semantykę.
3 Wiele wyjaśnień niesłusznie twierdzi, że tylko programowanie imperatywne ma składniowo uporządkowane instrukcje. Wyjaśniłem to zamieszanie między programowaniem imperatywnym a funkcjonalnym . Na przykład kolejność instrukcji HTML nie zmniejsza spójności ich znaczenia.
w programowaniu funkcjonalnym ... zakres zmienności zmiennej jest typem
W zależności od tego, jak odróżnia się programowanie funkcjonalne od programowania imperatywnego, twoje „przypisywalne” w programie imperatywnym może również mieć typ ograniczający jego zmienność.
Jedyną niezrozumiałą definicją, którą obecnie cenię dla programowania funkcjonalnego, jest: a) funkcje jako obiekty i typy pierwszej klasy, b) preferencja dla rekurencji nad pętlami i / lub c) funkcje czyste - tj. Te funkcje, które nie wpływają na pożądaną semantykę programu po zapamiętywaniu (a zatem całkowicie czyste programowanie funkcjonalne nie istnieje w semantyce denotacyjnej ogólnego przeznaczenia z powodu wpływu semantyki operacyjnej, np. alokacji pamięci ).
Właściwość idempotentna funkcji czystej oznacza, że wywołanie funkcji jej zmiennych można zastąpić jej wartością, co zwykle nie ma miejsca w przypadku argumentów procedury imperatywnej. Funkcje czyste wydają się być deklaratywne w stosunku do nieskomplikowanych przejść stanu między typami danych wejściowych i wyników.
Ale zestaw funkcji czystych nie zachowuje takiej spójności, ponieważ możliwe jest modelowanie procesu imperatywnego skutków ubocznych (stanu globalnego) w czysto funkcjonalnym języku programowania, np. IOMonad Haskella, a ponadto całkowicie niemożliwe jest zapobieganie temu dowolny całkowicie funkcjonalny język programowania Turinga.
Jak napisałem w 2012 r., Który wydaje się podobny do konsensusu komentarzy na twoim niedawnym blogu , to programowanie deklaratywne jest próbą uchwycenia pojęcia, że zamierzona semantyka nigdy nie jest nieprzejrzysta. Przykładami nieprzejrzystej semantyki są zależność od porządku, zależność od usuwania semantyki wyższego poziomu w warstwie semantyki operacyjnej (np. Rzutowania nie są konwersjami, a potwierdzone generyczne ograniczają semantykę wyższego poziomu ) oraz zależność od wartości zmiennych, których nie można sprawdzić (udowodniono poprawne) według języka programowania.
Doszedłem zatem do wniosku, że tylko niekompletne języki mogą być deklaratywne.
Tak więc jednym jednoznacznym i wyraźnym atrybutem języka deklaratywnego może być to, że można udowodnić, że jego wyniki są zgodne z jakimś wymiennym zbiorem reguł generatywnych. Na przykład, dla każdego konkretnego programu HTML (ignorując różnice w sposobie rozbieżności interpretatorów), który nie jest skryptowany (tj. Nie jest kompletny w Turingu), jego zmienność wyjściowa może być policzalna. Lub bardziej zwięźle program HTML jest czystą funkcją jego zmienności. Podobnie program do obsługi arkuszy kalkulacyjnych jest czystą funkcją jego zmiennych wejściowych.
Wydaje mi się więc, że języki deklaratywne są antytezą
nieograniczonej rekurencji , tzn. Według drugiego twierdzenia Gödela o samoreferencyjnych twierdzeniach nie można udowodnić.
Lesie Lamport napisała bajkę o tym, jak Euclid mógł obejść twierdzenia Gödela dotyczące niekompletności zastosowane do dowodów matematycznych w kontekście języka programowania przez zgodność między typami i logiką (korespondencja Curry-Howarda itp.).