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

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!

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.

$\lambda$$\lambda$

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!)

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.

„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.