В другом потоке Андрей Бауэр определил денотационную семантику как: значение программы является функцией значений ее частей. Что беспокоит меня в этом определении, так это то, что оно, кажется, не выделяет то, что обычно считается денотационной семантикой, из того, что принято считать...
Я читал « Семантику с приложениями » от Nielson & Nielson , и мне очень нравится эта тема. Я хотел бы иметь еще одну книгу по семантике языка программирования - но я действительно могу получить только одну. Я взглянул на книгу « Турбак / Гиффорд» , но она слишком многословна; Я думал, что с...
Вероятно, наиболее распространенным применением линейных типов в PL является использование их для предоставления языков, которые управляют псевдонимами (т. Е. Линейное значение имеет единственный указатель на него, более или менее). Но есть небольшое несоответствие между этим использованием и...
Теорема Банаха о неподвижной точке говорит, что если у нас есть непустое полное метрическое пространство , то любая равномерно сжимающая функция имеет единственную неподвижную точку . Однако доказательство этой теоремы требует аксиомы выбора - нам нужно выбрать произвольный элемент чтобы начать...
У меня на самом деле есть два вопроса: Кто первым использовал логические отношения, чтобы связать семантику? Я проследил их до Рейнольда « О связи между прямой и семантикой продолжения », но я не могу утверждать, что провел исчерпывающий поиск. Я нашел ссылки на логические отношения, датирующиеся...
С учетом множество и , A бифункционального соотношение между ними определяются как отношение , удовлетворяющее следующее свойство:B ( ∼ ) ⊆ A × BAAAВВB (∼)⊆A×B(∼)⊆A×B(\sim) \subseteq A \times B Если и a ′ ∼ b ′ и a ∼ b ′ , то a ′ ∼ b . a∼ba∼ba \sim ba′∼b′a′∼b′a' \sim b'a∼b′a∼b′a \sim b'a′∼ba′∼бa'...
Усилия по проверке компилятора часто сводятся к тому, чтобы доказать, что компилятор полностью абстрактен: он сохраняет и отражает (контекстуальные) эквивалентности. Вместо того, чтобы предоставлять полные доказательства абстракции, некоторые недавние (основанные на категориях) работы по проверке...
Функциональный язык можно рассматривать как категорию, где его объектами являются типы и функции морфизмов между ними. Как классы типов вписываются в эту модель? Я предполагаю, что мы должны рассматривать только те реализации, которые удовлетворяют ограничению, которое имеет большинство классов...
На странице «Продвинутая схема: некоторые непослушные биты» говорится: Продолжения - это мощная конструкция потока управления, из которой может быть получена почти любая другая структура потока управления [...]. Я думал, что схемы call/cc, связанные (*) с оператором J Питера Лэндена, могут быть...
Имея дело с теоретико-областными категориями (скажем, CPO и CPO), я часто хотел бы найти словарь для языка теории категорий в теории областей.ωω\omega То есть, учитывая концепцию, скажем, моническую стрелку, я мог бы найти ее в словаре и посмотреть, каковы ее известные характеристики в разных...
Глава Смита в руководстве по логике в области компьютерных наук и другие ссылки описывают, как метрические пространства могут использоваться в качестве областей. Я понимаю, что полные метрические пространства дают уникальные неподвижные точки, но я не понимаю, почему метрические пространства важны....
Вот вопрос «следа B», если таковой был. Резюме: первое, о чем я думаю, когда пытаюсь дать семантику недетерминированным программам, приводит к семантике, где я не могу доказать вещи о циклах, которые заканчивают только недетерминированно. Конечно, кто-то определил, что делать в этой ситуации, или,...
Может ли кто-нибудь указать мне на ссылку на неопределяемость модуля функционала непрерывности в PCF? \newcommand{\N}{\mathbb{N}} \newcommand{\bool}{\mathsf{bool}} Андрей Бауэр написал очень хороший пост в блоге, в котором более подробно рассматриваются некоторые вопросы, но я кратко изложу его...
В программировании семантики языка, он часто слышал , что люди говорят о означая и денотат . Кажется, они не одинаковы. В чем разница? Связано ли первое с операционной семантикой, а второе - с денотационной семантикой?...
Эквивалентно, существует ли известная денотационная семантика для вероятностных функциональных языков программирования высшего порядка? В частности, существует ли доменная модель чистого нетипизированного вычисления, расширенная симметричной случайной операцией двоичного выбора.λλ\lambda мотивация...