Есть ли какая-либо Математическая модель или Теория позади Языков программирования? [закрытый]

Есть ли у нас [базовая модель] для языков программирования?

Небеса, да. И поскольку существует так много языков программирования, есть несколько моделей на выбор. Самое важное первое:

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

   e :: = x | e1 e2 | \ x.e 
   

  , которые составляют переменные , приложения функций и определения функций . Лямбда-исчисление также имеет довольно большой набор «правил редукции» для упрощения выражений. Если вы найдете выражение, которое нельзя сократить, оно называется «нормальной формой» и представляет собой значение.

  Лямбда-исчисление настолько универсально, что его можно использовать в нескольких направлениях.

  • Если вы хотите использовать все доступные правила, вы можете написать специализированные инструменты, такие как частичные оценщики и части компиляторов.

  • Если вы избегаете сокращения любого подвыражения с помощью лямбда, но в остальном используете все доступные правила, вы получите модель ленивого функционального языка, такого как Haskell или Clean. В этой модели, если сокращение может завершиться, это гарантировано, и легко представить бесконечные структуры данных. Очень могущественный.

  • Если вы избегаете сокращения любого подвыражения с помощью лямбда, и если вы также настаиваете на приведении каждого аргумента к нормальной форме перед применением функции, тогда у вас есть модель нетерпеливого функционального языка, такого как F # , Lisp, Objective Caml, Scheme или Standard ML.

• Существует также несколько разновидностей типизированных лямбда-исчислений, самые известные из которых сгруппированы под названием Система F , которые были независимо открыты Жираром (в логике) и Рейнольдс (в области информатики). Система F - отличная модель для таких языков, как CLU, Haskell и ML, которые являются полиморфными, но имеют проверку типов во время компиляции. Хиндли (в логике) и Милнер (в информатике) открыли ограниченную форму Системы F (теперь называемую системой типов Хиндли-Милнера), которая позволяет вывести выражения Системы F из некоторых выражений нетипизированного лямбда-исчисление. Дамас и Милнер разработали алгоритм вывода, который используется в стандартном машинном обучении и обобщен на других языках.

• Лямбда-исчисление просто перемещает символы. Новаторская работа Даны Скотт в денотационной семантике показала, что выражения в лямбда-исчислении действительно соответствуют математическим функциям - и он определил, какие из них. Работа Скотта особенно важна для понимания «рекурсивных определений», которые являются обычным явлением в информатике, но бессмысленны с математической точки зрения. Скотт и Кристофер Стрейчи показали, что рекурсивное определение эквивалентно наименее определенному решению рекурсивного уравнения, и, кроме того, показали, как это решение может быть построено. Любой язык, допускающий рекурсию, и особенно языки, допускающие рекурсию произвольного типа (например, Haskell и Clean), чем-то обязаны модели Скотта.

• Существует целое семейство моделей, основанных на абстрактных машинах . Здесь не столько индивидуальная модель, сколько техника. Вы можете определить язык, используя конечный автомат и определяя переходы на нем. Это определение охватывает все, от машин Тьюринга до машин фон Неймана и систем переписывания терминов, но в целом абстрактная машина спроектирована так, чтобы быть «максимально приближенной к языку».«Проектирование таких машин и бизнес по доказательству теорем о них относятся к операционной семантике .

А как насчет объектно-ориентированного программирования?

Я не так хорошо образован как и следовало бы говорить об абстрактных моделях, используемых для ООП. Модели, с которыми я наиболее знаком, очень тесно связаны со стратегиями реализации. Если бы я хотел исследовать эту область дальше, я бы начал с денотационной семантики Уильяма Кука для Smalltalk. язык очень прост, почти такой же простой, как лямбда-исчисление, поэтому он представляет собой хороший пример для моделирования более сложных объектно-ориентированных языков.)

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

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

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

... мы воспринимаем объекты как примитивные и концентрируемся на внутренних правилах, которым объекты должны подчиняться. Мы вводим объектные исчисления и развиваем теорию объектов вокруг них. Эти исчисления объектов так же просты, как исчисления функций, но представляют объекты напрямую.

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