Как побочные эффекты обрабатываются в семантике?

В разделе « Семантика» Энтони Ааби «Введение в языки программирования» он делает следующее наблюдение:

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

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

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

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

Object x = new Object();
Object y = new Object();
... some more code ...

Таким образом, эта программа создает объект и называет его x, а затем создает второй объект с именем y, а затем продолжает выполнять еще немного кода. Теперь предположим, что программист решает изменить порядок размещения этих двух объектов:

Object y = new Object();
Object x = new Object();
... some more code ...

Теперь задайте вопрос: меняет ли этот рефакторинг поведение программы? С одной стороны, на базовом компьютере x и y будут размещены в разных местах в двух запусках программы. Так что в этом смысле программа ведет себя по-разному.

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

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

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

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

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

Я должен также упомянуть возможную семантику миров для локального государства, разработанную Фрэнком Олесом и Джоном Рейнольдсом (извините, не могу найти лучшую ссылку, эта штука с 1982 года), которая предшествует монадам Могги. Они использовали категории предварительных пучков, чтобы обеспечить семантику подобного альголу языка, который корректно моделировал многие аспекты локального состояния (но не все из них, я думаю, что модель допускала мгновенный возврат, но, возможно, моя память служит мне неправильно).

Матиас Феллайзен представил убедительное решение проблемы побочных эффектов в семантике в своей серии «Синтаксические теории управления и состояния».

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

Машина CESK и более мелкая пошаговая операционная семантика являются стандартом де-факто в теории языков программирования уже около двух десятилетий.

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

Среда отображает переменные на адреса; магазин сопоставляет адреса со значениями.

Это упрощает моделирование изменяемых переменных: просто измените значение по его адресу.

Это также упрощает моделирование указателей и динамическое распределение: просто делайте адреса магазинов первоклассными значениями.

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

Как наличие побочных эффектов в языке программирования влияет на способность отображать программу в вычислительной модели?

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

Это не просто побочные эффекты, такие как состояние, которые вызывают проблемы. Простые императивные языки, такие как защищенный командный язык Дейкстры, имеют такие побочные эффекты и имеют хорошую семантику. Проблема возникает с расширениями лямбда-исчисления с типом операционной семантики, ожидаемой от языков программирования даже при отсутствии побочных эффектов: самым ранним, PCF Плоткина, были даны денотационные модели относительно рано, но семантика не была полностью абстрактной, означая, что денотационная семантика была чрезмерно общей, не совсем соответствующей их операционной семантике. PCF наконец получил полностью абстрактную денотационную семантику в конце 1980-х с семантикой игры, которая совсем не похожа на теоретико-порядковую семантику Скотта. Параллелизм до сих пор не получил полностью адекватного денотационного лечения.

Многие сомневаются в важности такого рода семантики. Мы всегда можем предоставить некоторую операционную семантику, даже если эта «семантика» является просто источником программы и именами некоторых машин, которые скомпилировали и запустили программу: по этой причине Стрейчи осудил операционную семантику. Но семантика структурных операций Плоткина показала, как операционная семантика может быть отделена от моделей машин, а работа Питта показала, как такая семантика может поддерживать аналогичные рассуждения о программах и языках программирования для денотационной семантики. Таким образом, операционная семантика является жизнеспособной альтернативой денотационной семантики, и с успехом применяется к значительному числу языков программирования, таких как Standard ML.

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

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