Что является теоретической основой императивного программирования?

48

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

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

Шейн
источник

Ответы:

27

В общем, когда математика используется для изучения некоторого X , сначала требуется модель X , а затем разрабатывается теория, набор результатов об этой модели. Я предполагаю , что теория может быть названа «теоретической основой» для X . Теперь установите X = вычисление. Существует много моделей вычислений, многие из которых связаны с «состоянием». Каждая модель имеет свою «теорию», и иногда ее можно «переводить» между моделями. Я считаю, что трудно сказать, какая модель является более «базовой» - они просто разработаны с разными целями.

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

Если вы заботитесь о правильности , тогда вам пригодятся и другие модели. Здесь у вас есть операционная семантика (которую я бы назвал аналогом лямбда-исчисления для вычислений с полным состоянием), аксиоматическая семантика (разработанная Хоаром в 1969 году на основе индуктивных утверждений Флойда от 1967 года, которые популяризируются Кнутом в «Искусстве компьютерного программирования» , том 1) и др.

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

Наконец, позвольте мне упомянуть, что в Интернете есть большая книга о моделях вычислений Джона Сэвиджа. В основном это эффективность. Для корректности я рекомендую начать с классических работ Флойда (1967) , Хоара (1969) , Дейкстры (1975) и Плоткина (1981) . Они все очень крутые.

Раду ГРИГОРЕ
источник
4
Я думаю, что Операционная Семантика - действительно то, что ищет плакат. Немного больше информации о Википедии: en.wikipedia.org/wiki/Operational_semantics
sclv
22

Простейшей теоретической моделью императивной программы является сама машина Тьюринга. У него есть оба важных компонента императивной программы: неограниченное изменяемое состояние и конечный автомат, который работает с ним.

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

Александр Пассос
источник
2
Использование монад для получения императивных конструкций на чисто функциональном языке (таком как Haskell) не дает вам полной возможности императивного программирования. В частности, без действительно изменяемого состояния (например, как во многих языках со ссылками) все еще существует много структур данных, чья эффективная реализация на чисто функциональном языке неизвестна.
Джошуа Грохов
@Joshua: Почему вы думаете, что государственные монады не выражают семантику ссылок? Я в недоумении, чтобы понять, что может быть возражение.
Чарльз Стюарт
Монада состояний в основном является синтаксическим сахаром для наличия набора функций, которые все принимают дополнительный аргумент (состояние) и выводят дополнительный вывод (следующее состояние). Но на чисто функциональном языке вы не можете на самом деле изменить состояние, чтобы получить следующее состояние, вам все равно придется копировать и восстанавливать. Я не знаю, существуют ли конкретные структуры данных, для которых известно, что они не могут быть эффективно реализованы на чисто функциональном языке, но есть, безусловно, убедительные доказательства (например, Пиппенгер. Чистый против нечистого Лисп. 1997).
Джошуа Грохоу
6
С семантикой мутации можно отлично справиться с монадами - см., Например, монаду ST в Хаскеле. Мы говорим здесь о семантике, а не о реализации.
SCLV
20

Короче говоря, я бы сказал, что императивное программирование возникло из машинного языка и практики программирования. С другой стороны, монады предоставляют подходящую семантическую структуру для описания семантики функций императивного языка программирования. В статье « Понятия вычислений и монад » Могги заложены формальные основы. Фил Уодлер популяризировал эту идею и внес существенный вклад в то, что она стала ключевым способом включения императивных функций в язык программирования Haskell. Недавняя работа Плоткина и степенные понятия вычислений определяют монады идет другой путь, утверждая, что некоторые, но не все, понятия (императивного) вычисления на самом деле дают монаду, что означает, что монады очень существенно соответствуют императивным (и другим) понятиям вычисления.

Дэйв Кларк
источник
8
Монады могут использоваться для оцепления императивного программирования в чисто функциональном мире, но я не вижу смысла утверждать, что они образуют теоретическую основу для императивного программирования, аналогичную связи между лямбда-исчислением и многими функциональными языками. Монады не моделируют вычисления настолько, насколько они образуют абстракцию над классами вычислений (например, чистые вычисления против вычислений, которые включают в себя ввод-вывод или вычисления, которые основаны на определенном пакете изменяемого состояния).
blucz
1
Монады - способ написать более понятную денотационную семантику для эффективных языков, так почему бы и нет?
nponeccop
15

Если вы ищете строгую математическую трактовку императивного языка программирования, в качестве примера можно привести книгу Винскеля «Формальная семантика языков программирования» (1993).

В книге он определяет императивный язык программирования, называемый IMP, и предоставляет его операционную, денотационную и аксиоматическую семантику.

yhirai
источник
14

Я подхожу к этому вопросу поздно, но это увлекательный вопрос. Итак, вот мои взгляды.

Когда я был студентом, у нас был великий профессор математики, который давал нам лекции по истории и развитию математики. По его словам, математика развивалась волнами «расширения» и «консолидации». На этапе расширения были рассмотрены и исследованы новые идеи, которые ранее были неизвестны. Затем, на этапе консолидации, новые теории были интегрированы в существующую совокупность знаний. Однако, по его словам, в 20-м веке расширение и консолидация идут параллельно.

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

Поэтому мне было бы все равно, есть ли априорная теоретическая основа для императивного программирования. Если его нет, пойдем и найдем его. То, что мы уже знаем, говорит нам, что императивное программирование фантастически глубоко и красиво. Функциональное программирование меркнет в сравнении. Но у нас много работы, чтобы донести всю эту теорию до людей.

Удай Редди
источник
«Функциональное программирование меркнет в сравнении». Теперь, если бы я только мог вывести вас с Бобом Харпером на боевую арену. Вы бы взмахнули большим блоком команд, и он попытался бы закрыть вас. (PS: очень хороший ответ, я проголосовал за него.)
Андрей Бауэр
Ну, он как бы избегает меня. Я не знаю, означает ли это что-нибудь :-)
Uday Reddy
11

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

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

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

Обычно, если вы подходите к концу достойного учебника по PL (например, «Типы и языки программирования» Пирса), вы начнете видеть формальное моделирование императивных языковых функций. Это может быть интересно для вас.

blucz
источник
11

An Axiomatic Basis for Computer Programming АВТОМОБИЛЕМ

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

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=rep1&type=pdf

Vag
источник
8

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

Kurt
источник
7

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

Если вы имеете в виду «основание» в историческом смысле, я думаю, что не существует «эквивалентной математической основы». Однако, хотя императивное программирование возникло из практических соображений, существует несколько способов всесторонней характеристики значения императивного программирования способами, которые могут оказаться «полезными для моделирования», такими как логика Хоара .

jbapple
источник
ты действительно хотел сделать это сообщество вики?
Суреш Венкат
Да, я хотел сделать это вики-сообществом.
jbapple
7

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

Ответ относительно монад не является строго точным, потому что в haskell монада используется только потому, что это абстракция, которая позволяет кодировать порядок ограничений оценки и явно отслеживать свойство «возможно использовать IO».

Стоит указать и на то, что логику хора / разделения можно рассматривать как монады, и что существует ряд современных проектов, таких как проект ynot в Гарварде, которые изучают эти темы.

исследование логики разделения - это постоянная и активная область.

Картер Тацио Шонвальд
источник
Мне кажется ошибкой путать тот факт, что Haskell использует понятие монад (и класс типов монад) с более общим подходом, предложенным, например, Moggi, который использует монады для структурирования описания категориальной семантики. Принятие монад как инструмента для структурирования программирования не должно закрывать нам глаза на использование категориальной семантики как инструмента для структурирования рассуждений о программировании.
SCLV
очень хорошее пояснение, хотя я верю, что целое множество людей использовали монады а-ля-хаскел для изучения семантики с помощью монадных преобразователей. В частности, различающаяся семантика для операций, которые возникают из-за различных составов упомянутых трансформаторов (например, для состояния / изменчивости, продолжений, недетерминизма и т. Д.)
Картер Тацио Шонвальд
5

Я подойду к этому вопросу еще позже, но я в равной степени очарован этим.

Почему теория императивного программирования считается менее обоснованной, чем теория функционального программирования, уклоняется от меня. Вероятно, он начал серьезно относиться к Скотту и де Баккеру в 1969 году, когда они проанализировали значение рекурсии на простом императивном языке [1]. Когда императивный язык приобретает черты, история становится немного грязнее, но это всего лишь цена, которую нужно заплатить за то, чтобы быть ближе к металлу. Чтобы назвать одно из более всеобъемлющих усилий, в 1980 году де Баккер, де Брюин и Цукер написали монографию на эту тему [2]. Другие были упомянуты выше. Эти ссылки, конечно, предшествуют логике разделения, но [2], тем не менее, затрагивают массивы и взаимно рекурсивные процедуры.

[1]: неопубликованный в 1969 году, но появился как Джако де Баккер и Дана С. Скотт. Теория программ , стр. 1-30. В Klop et al. JW де Баккер, 25 лет семантик. КРИ, Амстердам, 1989. Liber Amoricum.

[2]: Якобус В. де Баккер, Арье де Брюин, Джеффри Цукер: Математическая теория правильности программы. Прентис Холл 1980.

Кай
источник
1
Очевидно, что императивное программирование чрезвычайно хорошо понимается. Я думаю, что люди имеют в виду, когда говорят, что они менее решительны, что структурное императивное программирование богаче, чем чисто функциональное программирование, и была обнаружена гораздо меньшая математическая структура, возникающая в той или иной форме императивного программирования. Например, некоторые виды императивных программ можно рассуждать о правильном использовании логики разделения. Вероятно, это связано с формами обмена. Может быть, такие программы имеют хорошую, абстрактную математическую характеристику?
Мартин Бергер
1
Лично я имею в виду, что теория модульности в императивных языках очень неясна. Мы знаем, что означает модульность для функциональных языков: реляционная параметричность. Для императивных языков существует множество скрывающих информацию идиом, которые (а) явно работают, но (б) для которых у нас нет хороших методов доказательства. Есть дразнящие намеки на то, что здесь есть глубокая теория: например, когда я делаю модульные доказательства последовательных императивных программ, мне в конечном итоге нужны методы из параллелизма. Неофициально, псевдонимы похожи на параллелизм, но я не знаю, как формализовать эту идею ...
Нил Кришнасвами
@Kai. Добро пожаловать в ветку! Прошло много времени с тех пор, как я смотрел на работу де Баккера, но я думаю, что основная проблема заключается в том, что подход не расширился. Для краткого обзора прогресса в императивном программировании с тех пор см. Мой пост в «Что такое денотационная семантика?» нить ссылки .
Uday Reddy
@NeelKrishnaswami. Я хотел бы увидеть эти доказательства. Они на вашей веб-странице? Псевдоним похож на параллелизм в том смысле, что они оба включают сложный обмен и чередование. Параллельно вы отвлекаете чередование и допускаете недетерминизм (что хорошо). В псевдонимах вы заставляете себя бороться с перемежением. Семантика игр - отличный пример такого принудительного чередования, поэтому мне это не нравится.
Uday Reddy
3

Вскоре после того, как вы задали свой вопрос, Марк Бендер из Университета МакМастер опубликовал диссертацию: « Исчисление заданий: чистый язык императивных рассуждений» (8 сентября 2010 г.) Этот тезис описывает простой императивный язык, соответствующий лямбда-исчислению.

Исчисление присваивания состоит только из четырех основных конструкций: присваивания X:=t, последовательности t;u, формирования ¡tпроцедуры и вызова процедуры !t. Для AC даны три интерпретации: операционная семантика, денотационная семантика и система переписывания терминов. Три показаны как эквивалентные.

Тезис Марка Бендера продолжает исследовать варианты, расширенные с ленивой оценкой, возвратом, составлением процедуры. Это похоже на исследование лямбда-исчисления с использованием небольших расширений.

В целом, тезис дает относительно прямой ответ на вопрос ОП.

dmbarbour
источник
pdf ссылка не работает
Куинн Уилсон