Вопросы с тегом «semantics»

11
Что именно означает «семантически наблюдаемый» побочный эффект?

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

10
Что такое хороший словарь по теории категорий и теории доменов?

Имея дело с теоретико-областными категориями (скажем, CPO и CPO), я часто хотел бы найти словарь для языка теории категорий в теории областей.ωω\omega То есть, учитывая концепцию, скажем, моническую стрелку, я мог бы найти ее в словаре и посмотреть, каковы ее известные характеристики в разных...

10
Рассуждение о недетерминированных концевых циклах

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

10
В чем разница между стратегиями сокращения и оценочными стратегиями?

Из статьи по стратегии оценки в Википедии: Понятие стратегии сокращения в лямбда-исчислении сходно, но различно. Из статьи о стратегии сокращения в Википедии: Это похоже на понятие стратегии оценки в информатике, но немного отличается от него. Какое тонкое различие между стратегиями оценки и...

10
Есть ли какие-либо известные CCC, закрытые при вероятностной операции powerdomain?

Эквивалентно, существует ли известная денотационная семантика для вероятностных функциональных языков программирования высшего порядка? В частности, существует ли доменная модель чистого нетипизированного вычисления, расширенная симметричной случайной операцией двоичного выбора.λλ\lambda мотивация...

10
Минимизация программы

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

10
В чем разница между значением и обозначением?

В программировании семантики языка, он часто слышал , что люди говорят о означая и денотат . Кажется, они не одинаковы. В чем разница? Связано ли первое с операционной семантикой, а второе - с денотационной семантикой?...

10
В какой области теории может использоваться дополнительная структура, присутствующая в метрических пространствах?

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

10
Ссылка для неопределимости модуля непрерывности функционала в ПКФ?

Может ли кто-нибудь указать мне на ссылку на неопределяемость модуля функционала непрерывности в PCF? \newcommand{\N}{\mathbb{N}} \newcommand{\bool}{\mathsf{bool}} Андрей Бауэр написал очень хороший пост в блоге, в котором более подробно рассматриваются некоторые вопросы, но я кратко изложу его...

9
Сертифицированный компилятор и оптимизации в Coq / Agda

Меня интересуют проверенные компиляторы, формализованные в теории типов Мартина-Лёфа, т.е. Coq / Agda. На данный момент я написал небольшой игрушечный пример. Тем самым я могу доказать, что мои оптимизации верны. Например, могут быть исключены дополнения с нуля, например, выражения типа «x + 0»....

9
Формальное определение / встречная часть в математике для «объектов» объектно-ориентированных моделей

Это вопрос, который я задал на форуме по математике SE, и меня сюда направили. Так вот вопрос Я новичок в формальной математике и теоретической информатике, поэтому, пожалуйста, потерпите меня, если вы обнаружите, что мой вопрос не сформулирован должным образом. Объектно-ориентированное...