Jaka jest różnica między rachunkiem a językiem programowania?

13

Myślę, że jestem dość zdezorientowany tym, co nazywa się rachunkiem różniczkowym i językiem programowania.

Zwykle myślę, i można było powiedzieć, że rachunek różniczkowy jest formalnym systemem rozumowania na temat równoważności programów. Programy mają semantykę operacyjną określoną przez maszynę, która powinna (myślę?) Być deterministyczna. W ten sposób (poprawny) rachunek różniczkowy dla języka jest metodą sprawdzającą równoważność programu.L

Wydaje mi się to rozsądnym rozłamem, ale czy jest to powszechnie akceptowane znaczenie? A może to nawet źle?

Powiązane, dlaczego niektóre semantyki operacyjne są niedeterministyczne (zakładając, że są zbieżne)? Co zyskujesz, pozostawiając wybór strategii otwartej?

Byłbym wdzięczny za wyjaśnienie tych kwestii; i jeszcze więcej konkretnych odniesień! Dzięki!

Guido
źródło
3
Są to różne słowa określające różne sposoby patrzenia na to samo.
Raphael
1
@Raphael, jak odpowiada na pytanie? To nie jest miejsce na filozofię.
fade2black
4
Czasami potrzebna jest mała filozofia, gdziekolwiek.
André Souza Lemos

Odpowiedzi:

10

Znaczenie słów nie jest ustalone, ale mogę podać moją interpretację.

Rachunek jest coś, co możemy obliczyć ze w sensie równań żonglerka (myślę manipulacji szereg Taylora lub obliczania całek w analizie). Rachunek mówi nam, jakie są reguły manipulacji, ale nie, które z nich powinniśmy zastosować w danej sytuacji.

Język programowania jest coś, co mówi nam, jak obliczyć. Mówi nam dokładnie, jak korzystać z reguł. Zazwyczaj pozwalamy komputerowi korzystać z reguł, ponieważ jest to znacznie szybsze. Reguły mogą być niedeterministyczne i mogą istnieć bardzo dobre powody, dla których są niedeterministyczne. Charakter rachunku może być taki, że nie jest on deterministyczny (myśl współbieżne procesy komunikacyjne), lub ustalenie konkretnej strategii może być szkodliwe dla technik wdrażania i optymalizacji.

λλ

Natomiast Standard ML jest językiem programowania. Podano go w kategoriach semantyki operacyjnej, tj. Reguł obliczeniowych. Są to pochodne pojęcia równości (równoważności kontekstowej, równoważności obserwacyjnym, etc.), które możemy umieścić na nim myśleć o nim jako o rodzaju rachunku.

Oczywiście często istnieją użyteczne połączenia między rachunkiem a jego manifestacją jako języka programowania. Konfluentna normalizacja jest tylko jednym ze sposobów przejścia z rachunku różniczkowego na język programowania (chociaż niestety niektórzy ludzie przeszli na religię). Ważna jest wzajemna zależność między rachunkowymi a językami programowania: języki programowania mogą być faktycznie używane, ale rachunki wyjaśniają, o czym są programy.

Aby denerwować ludzi, pozwólcie mi również stwierdzić, że udawanie, że nie ma różnicy między rachunkiem a jego manifestacją operacyjną, czasami prowadzi do wypaczonych poglądów na temat programowania i mini-religii w społeczności programistów. Możesz spróbować zgadnąć, który język mam na myśli. (To bardzo fajny język!)

Andrej Bauer
źródło
Czy więc języki programowania są wyposażone w rachunek różniczkowy wyposażony w system strategii / przepisywania?
xavierm02
ppp=p
π
Możesz przedstawić równania, które mówią nie tylko o programie, ale także o jego otoczeniu (stanie lub przejściach). Ale nie powiedziałbym, że coś takiego to rachunek różniczkowy. Jest to raczej model algebraiczny.
Andrej Bauer,
Wielkie dzięki, Andrej, to ma dla mnie sens. Zdaję sobie sprawę, że może się różnić w zależności od osoby, ale akceptuję tę odpowiedź, ponieważ (myślę) jest najlepsza.
Guido
2

Celem rachunku nie jest tylko badanie równoważności programów, to badanie programów. Przykładem fantazyjnego rachunku różniczkowego jest ten, w którym strategia (call-by-value lub call-by-name) jest ustalana lokalnie. Może być kiedyś zaimplementowany w języku programowania, ale najpierw jest badany jako rachunek różniczkowy. Kalkulatorów używasz również do badania układów typów (niektóre rachunki, takie jak te w teorii typów Martina-Löfa, również obliczają typy).


Uważam, że główna różnica polega na tym, że kalkulatory mają być (względnie) łatwe do formalnego studiowania, podczas gdy języki programowania są (względnie) łatwe w użyciu. Prowadzi to do następujących różnic:

Calculi wydają się być minimalistyczne, podczas gdy PL mają tendencję do nadmiarowości (w przypadku pętli, gdy już masz pętlę while, przełączaj, gdy już masz, jeśli ...), aby ułatwić wyrażanie tego, co chcesz.

Rachunki mają w pełni określoną semantykę, podczas gdy semantyka PLs jest często opisywana przez domyślnego interpretera / kompilatora.


Niektóre semantyki operacyjne są niedeterministyczne, ponieważ umożliwiają:

  • Aby udowodnić wszystko na temat całej „podsemantyki”.
  • Aby umożliwić implementacji wybór, a tym samym (być może) przyspieszenie.
  • Ponieważ czasami masz operację „radnom ()”, a jeśli nie zależy ci na prawdopodobieństwach, a tylko na tym, co jest możliwe, niedeterminizm jest dobrym sposobem na ich przedstawienie.

Zauważ, że funkcja call-by-value nie jest deterministyczna: możesz najpierw ocenić funkcję lub argument.

xavierm02
źródło
Nie, nie zgadzam się, że chodzi o poziom formalizacji lub wyrafinowania.
Andrej Bauer,
2

„Język programowania” i „rachunek różniczkowy” to terminy wielomianowe, to znaczy oznaczają różne rzeczy w zależności od kontekstu.

W niektórych kontekstach języki programowania i kalkulatory są zbieżne i odnoszą się do tej samej koncepcji, czyli systemu przepisywania opartego na zestawie formalnych reguł, które można zastosować „mechanicznie”.

Powodem, dla którego ta konwergencja jest czasami enigmatyczna dla nas (ale nie dla działających programistów lub matematyków), jest to, że naszym zadaniem jest tworzenie konkretnych języków programowania tak, jakby były rachunkowymi, oraz fizyczna realizacja rachunków w konkretnych językach programowania.

Aby odpowiedzieć bezpośrednio na twoje pytanie, zamieszanie między rachunkowymi a językami programowania (o ile istnieje) nie jest przypadkiem, ale projektem. Nasz projekt. Jest to świadectwo naszego względnego sukcesu jako dyscypliny naukowej.

André Souza Lemos
źródło