Описание тега denotational-semantics
Денотационная семантика - это подход формализации значений языков программирования путем создания математических объектов (называемых денотациями), которые описывают значения выражений из языков. Источник: Википедия
1
ответ
Haskell "оценивает" сводится к нормальному или WHNF?
Я понимаю ( я думаю), что Хаскелла seq(в общем случае) уменьшит свой первый аргумент до WHNF и увидит такое поведение, как и ожидалось в GHCi: λ> let x = (trace "foo" Foo (trace "bar" Bar 100)) in seq x 0 foo 0 Тем не менее, хотя документация для…
12 окт '15 в 14:46
1
ответ
Как добавить абстракции функций и процедур к денотационной семантике с использованием haskell?
Я хочу написать программу на Haskell для реализации простого императивного языка, основанного на его денотационной семантике. Я использую GHCi, версия 8.4.2 на Windows. Я столкнулся с некоторой проблемой при реализации абстракции функции и процедуры…
31 янв '19 в 02:39
1
ответ
Денотационная семантика, доказывающая, что итерация с фиксированной точкой приводит к наименьшей фиксированной точке
Я работаю над разделом wikibook на Haskell, посвященном денотационной семантике, и застрял в этом упражнении: Докажите, что фиксированная точка, полученная итерацией с фиксированной точкой, начиная с также наименьшее, что оно меньше, чем любая друга…
01 окт '15 в 12:42
6
ответов
"Какую часть Хиндли-Мильнера ты не понимаешь?"
Клянусь, раньше продавалась футболка с бессмертными словами: Какая часть ты не понимаешь? В моем случае ответ будет... все это! В частности, я часто вижу подобные обозначения в документах на Haskell, но я понятия не имею, что это означает. Я понятия…
21 сен '12 в 14:29
1
ответ
Как обозначить семантику этого синтаксиса?
Я пишу спецификацию языка, и мне нужно решить следующий элементарный вопрос. Предположим, у меня есть (по общему мнению, надуманный) абстрактный синтаксис: <A> ::= <B> | <C> <B> ::= 1 | 2 | 3 <C> ::= 4 | 5 | 6 Как выгля…
11 апр '13 в 16:18
2
ответа
Что такое денотационная семантика?
Я ищу точное и понятное определение. Те, что я нашел, отличаются друг от друга: Из книги по функциональному реактивному программированию Денотационная семантика - это математическое выражение формального значения языка программирования. Тем не менее…
20 июл '16 в 18:24
0
ответов
Формальная проверка с использованием денотационной семантики?
Это может быть связано с обменом стеками cs или cstheory, но я видел большинство вопросов, помеченных здесь формальной проверкой. Существует ли обширная литература по использованию денотационной семантики для верификации программы? С помощью быстрог…
13 янв '16 в 14:50
1
ответ
Какова семантика движка Geavo для интерпретатора Javascript?
редактировать Принимая во внимание ответный ответ ниже относительно справочной спецификации языка ECMAScript -11.13.2 Назначение составных частей Учитывая, почему это, javascript: o=""; o = o + (o+=1) ; alert(o); o=""; o = (o+=1) + o; alert(o); не т…
16 апр '11 в 20:03
1
ответ
Что входит в написание денотационной функции отображения семантики?
Я немного запутался в понятии денотационной семантики. Как я понимаю, денотационная семантика должна описывать, как функции и выражения работают в определенном языке программирования. Какая именно форма используется для описания этих функций и как о…
15 окт '13 в 20:12
1
ответ
Проверка завершения в функциональных программах
Существуют ли функциональные языки, которые могут указывать в контроллере типов, гарантированно ли завершаются определенные вычисления? В качестве альтернативы, вы можете сделать это только на Haskell? Что касается Haskell, то в этом ответе плакат г…
18 окт '13 в 17:10
0
ответов
Денотационная семантика N итерационного цикла
Мне нужно найти расширение языка While, как оно описано в книге Nielson & Nielson, которое включает в себя N итерационных циклов. Это не цикл for со счетчиком, а цикл, который выполняется n раз по данному предложению, если n является целым числом бо…
28 июн '18 в 09:40
1
ответ
Написание программы на языке haskell для вычисления денотационной семантики императивного языка программирования
Я пытаюсь написать программу на Хаскеле для вычисления денотационной семантики императивной языковой программы с целочисленными переменными, одномерными (целочисленными) массивами и функциями. Функция, с которой я начинаю, имеет тип: progsem :: Prog…
04 дек '13 в 19:10
0
ответов
Как доказать через правила Хоара?
Докажите следующее вычисление, используя правила Ho-is? где c - команда, в то время как X ≤ 100 делает X:= X + 2 с местоположением X. {X ≤ 100 ∧ (∃iX = 2 × i + 1)}c{X = 101} где я - целое число
28 май '19 в 04:24
1
ответ
Бесплатная теорема для fmap
Рассмотрим следующую оболочку: newtype F a = Wrap { unwrap :: Int } Я хочу опровергнуть (в качестве упражнения, чтобы осмыслить этот интересный пост ), что существует законный Functor F экземпляр, который позволяет нам применять функции Int -> In…
24 апр '21 в 22:16
1
ответ
Алгоритм построения естественной карты
дает конструктивное определение естественной карты, Этот пост на Reddit от Эдварда Кметтавзятой из бесплатной теоремы (которую я прочитал в еще одном сообщении Эдварда Кметта ): Для данного f, g, h а также k, так что f . g = h . k: $map f . fmap g …
29 апр '21 в 12:50
1
ответ
Какой тип семантики используется в Perl?
Я делаю проект о Perl и хотел бы знать, какой тип семантики он использует (денотационную, операционную или аксиоматическую), но я нигде не могу ее найти. Есть идеи, какой тип использует Perl? Заранее спасибо! :)
24 апр '22 в 08:46
1
ответ
Почему имена функций классифицируются как выражения L-значений?
Согласно статье Кристофера Стрейчи « Разновидности языков программирования» , посвященной денотационной семантике, в любых языках программирования имена могут быть связаны с привязываемыми значениями, что представлено функциейenvironment: Id -> D…
12 июл '23 в 23:46