Вопросы с тегом «domain-theory»

19
Вычисление вещественных чисел: с плавающей запятой, TTE, теория доменов, и т. Д.

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

16
Ищу Скотта оригинальную бумагу LCF

Доступна ли следующая рукопись публично? Дана Скотт, 1969, Теория вычислимых функций высшего типа . Неопубликованные заметки семинара, 7 страниц, Оксфордский университет. Эта статья обсуждается в разделе 8.1.2, Типы как множества , в Cardone & Hindley, 2006 История лямбда-исчисления и...

14
Является ли eta-эквивалентность для функций совместимой с операцией seke в Haskell?

Лемма: Предполагая, что эта эквивалентность у нас есть (\x -> ⊥) = ⊥ :: A -> B. Доказательство: ⊥ = (\x -> ⊥ x)по eta-эквивалентности и (\x -> ⊥ x) = (\x -> ⊥)по сокращению под лямбду. В отчете Haskell 2010, раздел 6.2, seqфункция определяется двумя уравнениями: seq :: a -> b...

12
Когда у пространств когерентности есть откаты и отжимания?

\newcommand{\symp}{\Bumpeq} ≎X≎X\symp_XXXX(X,≎X)(X,≎X)(X, \symp_X)f:X→Yf:X→Yf : X \to Yf⊆X×Yf⊆X×Yf \subseteq X \times Y(x,y)∈f(x,y)∈f(x,y) \in f(x′,y′)∈f(x′,y′)∈f(x',y') \in f если то иx≎Xx′x≎Xx′x \symp_X x'y≎Yy′y≎Yy′y \symp_Y y' если и то .x≎Xx′x≎Xx′x \symp_X x'y=y′y=y′y = y'x=x′x=x′x = x'...

12
Это эквивалентное условие для алгебраических множеств?

Определение «алгебраической посета» в непрерывных решетках и доменов , Определение I-4,2, говорит , что для всех ,x ∈ Lx∈Lx \in L множество должно быть направленным множеством, иA ( x ) = ↓ x ∩ K( Л )A(x)=↓x∩K(L)A(x) = {\downarrow} x \cap K(L) .х = ⨆ ( ↓ х ∩ К( Л )x=⨆(↓x∩K(L)x = \bigsqcup...

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

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

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

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

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

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