Подтвердить что ты не робот

Существует ли какая-либо математическая модель или теория языков программирования?

RDBMS основаны на Relational Algebra, а также на Codd Model. У нас есть что-то похожее на то, что для языков программирования или ООП?

4b9b3361

ОТВЕТЫ

Ответ 1

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

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

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

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

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

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

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

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

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

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

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

  • Существует целый ряд моделей, основанных на абстрактных машинах. Здесь не так много индивидуальной модели, как техника. Вы можете определить язык с помощью конечного автомата и определения переходов на машине. Это определение включает в себя все: от машин Тьюринга до машин Von Neumann до систем переписывания терминов, но, как правило, абстрактная машина предназначена для "как можно ближе к языку". Дизайн таких машин и бизнес доказательств теорем о них подпадают под рубрику оперативной семантики.

Что относительно объектно-ориентированного программирования?

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

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

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

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

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

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

Ответ 2

Lisp основан на исчислении Лямбды и является источником вдохновения для большей части того, что мы видим сегодня в современных языках.

Машины Von-Neumann являются основой современных компьютеров, которые были сначала запрограммированы на языке ассемблера, а затем в FORmula TRANslator. Затем была применена формальная лингвистическая теория контекстно-свободных грамматик и лежит в основе синтаксиса всех современных языков.

Теория вычислимости (формальные автоматы) имеет иерархию машинных типов, которая параллельна иерархии формальных грамматик, например, регулярная грамматика = машина конечного состояния, контекстная-грамматическая = pushdown-automaton, контекстно-зависимая -grammar = turing-machine.

Существует также теория информации двух типов: Шеннон и Колмогоров, которые могут быть применены к вычислениям.

Существуют менее известные модели вычислений, такие как рекурсивно-функциональная теория, регистрационные машины и почтовые машины.

И не забывайте предикат-логику в ее различных формах.

Добавлено: Я забыл упомянуть о дискретной теории математической группы и теории решетки. Решетки, в частности, являются (ИМХО) особенно отличным понятием, лежащим в основе всей логической логики, и некоторыми моделями вычислений, такими как денотационная семантика.

Ответ 3

Функциональные языки, такие как lisp, наследуют свои основные понятия из церковных "лямбда-вычислений" (статья wikipedia здесь). Отношения

Ответ 5

раздел истории Википедии Объектно-ориентированное программирование может быть полезным.

Ответ 6

Если вы изучаете языки программирования (например, в университете), существует довольно много теории, а не небольшая математика.

Примеры:

Ответ 7

Языки программирования - это продукт применения следующих теорий:

  • Теория алгоритмов
  • Теория вычислений
  • Автоматы состояний
  • и более

Ответ 8

Ближайшая аналогия, о которой я могу думать, - это эволюционирующие алгебры Гуревича, которые в наши дни известны под названием "Абстрактные государственные машины Гуревича" (GASM).

Я давно надеялся увидеть более реальные приложения теории, когда Гуревич присоединился к Microsoft, но, похоже, очень мало выходит. Вы можете проверить страницу ASML на сайте Microsoft.

Хорошим моментом в GASM является то, что они очень похожи на псевдокод, даже если их семантика формально определена. Это означает, что практикующие могут легко понять их.

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

Я думаю, нам нужно что-то подобное для динамических компонентов программной системы.

Ответ 9

Есть много измерений, чтобы решить свой вопрос, рассеиваясь в ответах.

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

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

Чтобы исключить плохие программы, у вас есть система типов.

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

Если вы все это изучаете самостоятельно, я настоятельно рекомендую http://www.uni-koblenz.de/~laemmel/paradigms0910/, потому что лекции снимаются на видео и помещаются онлайн.

Ответ 10

Много упоминалось о применении математики к вычислительной теории и семантике. Мне нравится упоминание теории типов, и я рад, что кто-то упомянул теорию решетки. Вот еще несколько.

Никто явно не упоминал теорию категорий, которая больше проявляется в функциональных языках, чем где-либо еще, например, в понятиях монад и функторов. Тогда есть теория моделей и различные воплощения логики, которые фактически появляются в теоретических проректорах или логическом языке Prolog. Существуют также математические приложения к основам и проблемам в параллельных языках.

Ответ 11

Нет математической модели для ООП.

Реляционная алгебра в математической модели для SQL. Он был создан bt E.F. Codd. C.J. Date также был известным специалистом, который помог с этой теорией. Вся идея состоит в том, что вы можете выполнять каждую операцию как заданную операцию, одновременно влияя на множество значений. Это, конечно же, означает, что движок базы данных должен сказать, ЧТО выйти, и база данных может оптимизировать ваш запрос.

Оба Codd и Date критиковали SQL, потому что они были вовлечены в теорию, но они не участвовали в создании SQL.

Посмотрите это видео: http://player.oreilly.com/videos/9781491908853?toc_id=182164

Существует много информации от Chris Date. Я помню, что дата критиковала язык программирования SQL как ужасный язык, но я не могу найти статью.

Критика в основном заключалась в том, что большинство языков позволяют писать выражения и присваивать переменные этим выражениям, но SQL не делает.

Так как SQL - это своего рода логический язык, я думаю, вы могли бы написать реляционную алгебру в Prolog. По крайней мере, у вас будет настоящий язык. Поэтому вы можете писать запросы в Prolog. И поскольку в прологе у вас есть много программ для интерпретации естественного языка, вы можете запросить свою базу данных с помощью естественного языка.

По словам дяди Боба, базы данных не понадобятся, когда у каждого есть SSD, потому что архитектура SSD означает, что доступ происходит так быстро, как RAM. Таким образом, вы можете иметь все свои объекты в ОЗУ.

https://www.youtube.com/watch?feature=player_detailpage&v=t86v3N4OshQ#t=3287

Единственная проблема с канавкой SQL заключается в том, что вы закончите без языка запросов для базы данных.

Итак, да и нет, реляционная алгебра использовалась как вдохновение для SQL, но SQL на самом деле не является реализацией реляционной алгебры.

В случае Lisp все по-другому. Основная идея заключалась в том, что при реализации функции eval в Lisp вы могли бы реализовать весь язык. Это первая реализация Lisp - это только половина страницы кода.

http://www.michaelnielsen.org/ddi/lisp-as-the-maxwells-equations-of-software/

Смеяться немного: https://www.youtube.com/watch?v=hzf3hTUKk8U

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

Теперь в ООП отсутствует формализация ООП.

Интересно, что второй язык OO, когда-либо созданный, Smalltalk, имеет только объекты, у него нет примитивов или чего-то подобного. И создатель, Алан Кей, явно создал блоки для работы точно как функции Lisp.

Некоторые люди утверждают, что ООП может быть формализовано с использованием теории категорий, которая является своеобразной теорией множеств, но с морфизмами. Морфизм - это структура, сохраняющая отображение между объектами. Таким образом, в общем случае вы можете иметь карту (f, collection) и возвращать коллекцию со всеми элементами, которые применяются f.

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

https://www.youtube.com/watch?feature=player_detailpage&v=o6L6XeNdd_k#t=250

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

Экспериментальный теоретический язык, созданный явно для того, чтобы попытаться формализовать ООП, является Z. Z получен из формализма требований.

Другая попытка - формализм Лука Карделли:

Java http://lucacardelli.name/Papers/PrimObjImp.pdf Java http://lucacardelli.name/Papers/PrimObj1stOrder.A4.pdf Java http://lucacardelli.name/Papers/PrimObjSemLICS.A4.pdf

Я не могу читать и понимать эту нотацию. Это кажется бесполезным упражнением, поскольку, насколько я знаю, никто никогда не реализовывал это так, как вычисление lamba было реализовано в Lisp.