В чем разница между исчислением и языком программирования?

Я думаю, что я довольно озадачен тем, что называется исчислением и тем, что называется языком программирования.

Я склонен думать и, возможно, мне сказали, что исчисление - это формальная система рассуждений об эквивалентности программ. Программы имеют операционную семантику, указанную машиной, которая должна (я думаю?) Быть детерминированной. Таким образом, (правильное) исчисление для языка является методом доказательства эквивалентности программы.$L$

Мне кажется, это разумный раскол, но является ли это общепринятым значением? А может, это даже неправильно?

Связанный, почему некоторая операционная семантика недетерминирована (предположите, что это слияние)? Что получается, если оставить выбор стратегии открытым?

Я был бы очень признателен за разъяснения по этим вопросам; а конкретных ссылок еще больше! Благодарность!

Значение слов не зафиксировано, но я могу дать вам свое толкование.

Исчисление является то , что мы пересчитываем в смысле жонглирования уравнений (думаем манипуляцию ряда Тейлора или вычисления интегралов в анализе). Исчисление говорит нам, каковы правила манипуляции, но не какие из них мы должны использовать в данной ситуации.

Язык программирования является то , что говорит нам о том , как рассчитать. Это говорит нам точно, как использовать правила. Обычно мы позволяем компьютеру использовать правила, так как это намного быстрее. Правила могут быть недетерминированными, и могут быть очень веские причины их недетерминированности. В основе исчисления может лежать то, что оно недетерминировано (например, параллельные процессы общения), или исправление конкретной стратегии может быть вредным для методов реализации и оптимизации.

$\lambda$$\lambda$

В отличие от стандартного ML является языком программирования. Он дается в терминах операционной семантики, т. Е. Правил вычислений. Есть производные понятия равенства (контекстуальная эквивалентность, наблюдательная эквивалентность и т. Д.), Которые мы можем поставить поверх этого, чтобы рассматривать его как своего рода исчисление.

Конечно, часто существует полезная связь между исчислением и его проявлением в качестве языка программирования. Нормализация слияния - это всего лишь один из способов перехода от исчисления к языку программирования (хотя, к сожалению, некоторые люди превратили его в своего рода религию). Взаимодействие между исчислениями и языками программирования важно: языки программирования действительно могут использоваться, но исчисления объясняют, о чем эти программы.

Просто чтобы раздражать людей, позвольте мне также заявить, что притворство о том, что нет никакого различия между исчислением и его операционным проявлением, иногда приводит к искаженным взглядам на программирование и мини-религии в сообществе программистов. Вы можете попытаться угадать, какой язык я имею в виду. (Это очень крутой язык!)

Цель исчислений - не просто изучение эквивалентности программ, а изучение программ. Примером необычного исчисления является то, что стратегия (вызов по значению или вызов по имени) определяется локально. Это может быть реализовано когда-нибудь на языке программирования, но сначала оно изучается как исчисление. Вы также используете исчисления для изучения систем типов (с некоторыми исчислениями, такими как исчисление в теории типов Мартина-Лёфа, также для вычислений типов).

Я считаю, что основное отличие состоит в том, что исчисления предназначены для (относительно) легкого изучения формально, в то время как языки программирования предназначены для (относительно) легкого использования. Это приводит к следующим различиям:

Исчисления, как правило, минималистичны, в то время как PL имеют тенденцию иметь избыточность (для цикла, когда у вас уже есть цикл while, переключаться, когда у вас уже есть if, ...), чтобы облегчить выражение того, что вы хотите.

В исчислениях полностью указана семантика, в то время как семантика PL часто описывается интерпретатором / компилятором по умолчанию.

Некоторые операционные семантики недетерминированы, потому что они позволяют:

• Чтобы доказать вещи о всей "подсемантике".
• Позволить реализации выбирать и, следовательно, (возможно) ускорить процесс.
• Потому что иногда у вас есть операция "radnom ()", и если вас не интересуют вероятности, а только то, что возможно, недетерминизм - хороший способ представить это.

Обратите внимание, что вызов по значению недетерминирован: вы можете сначала оценить функцию или аргумент.

«Язык программирования» и «исчисление» являются многозначными терминами, то есть они означают разные вещи в зависимости от контекста.

В некоторых контекстах языки программирования и исчисления сходятся, чтобы ссылаться на одну и ту же концепцию - систему переписывания, основанную на наборе формальных правил, которые могут применяться «механически».

Причина, по которой эта конвергенция иногда загадочна для нас (но не для работающих разработчиков программного обеспечения или математиков), заключается в том, что наша работа состоит в том, чтобы задавать конкретные языки программирования, как если бы они были исчислениями, и физически воплощать исчисления в конкретных языках программирования.

Чтобы ответить на ваш вопрос напрямую, путаница между исчислениями и языками программирования (в той степени, в которой они существуют) - это не случайность, а проект. Наш проект. Это свидетельство нашего относительного успеха как научной дисциплины.