ооп и функциональщина кратко, внятно.

Ring : (c ℓ : Level) → Set (suc (ℓ ⊔ c))

то есть в первом приближении

Ring :: Level -> Level -> Type ?
-- Type 0 = *, Type 1 = BOX, и всё... + импредикативность BOX :: BOX

Level ~ Nat, так что оно. Только иерархии универсумов их полиморфизма и Level в хаскеле пока нет, так что всё это не имеет смысла — ℓ и c это максимум 0 или 1, 0 бы значило, что Ring агрегирует тип (чего тоже нельзя), поэтому он не тип kind-а *, а kind сорта BOX, вообще справа универсум уровня 1 + max(ℓ, c) (зависимость от ℓ и c, подобно Π-types для функций, но dependent polynomial functor — ни того ни другого тоже нет). Если бы такие вещи были, то можно было бы видеть, например, что data List : Type → Type where ... и data {- class -} Monad : (F : Set → Set) → Class where ... и ListIsMonad {- instance -} : Monad List; ListIsMonad = Monad { return = ...; ... } (Type = *, Class = BOX), то есть тип аналогичен множеству, а класс типов классу теории множеств.

есть какой-нибудь док, где на пальцах систематически изложен данный матан применительно к ЯП? В смысле, не «мыслью по древу» «всё на свете что хоть как-то касается логики». А конкретный понимабельный эээ инструмент, содержащий минимум шизофазии.

Поэтому «основные типы» лучше трактовать как множества, а не как алгебраические структуры.

Основные типы лучше трактовать как объекты подходящей категории. Например, когда Скотт искал денотационную семантику для нетипизированного (вообще он искал для типизированного, но не важно) лямбда-исчисления, то обнаружил, что уравнения для типов не решаются в категории Set, то есть типы не могут быть обычными множествами, но могут быть топологическими пространствами, то есть множествами со структурой — категория другая, вычислимые функции не просто функции на множествах, а в строну непрерывных функций на топологических пространствах. Оттуда пошли решётки, _|_ и т.п. в исследовании семантик ЯП (теория доменов). http://math.andrej.com/2006/03/27/sometimes-all-functions-are-continuous

Так же, если говорить про алгебраические типы — есть теория полиномиальных функторов.

Можно такой тип в агде описать?

Тут довольно просто — есть число, помещаем его в кортеж первым, вторым хотим поместить доказательство какого-то его свойства, если такое доказательство строится, то ок — кортеж готов, иначе сам кортеж построить нельзя, получается что тип этого кортежа населён ровно всеми числами удовлетворяющими этому свойству — это тип, например, (int, property), точнее (x : int, property[x]) где property как-то выражается (зависит) от первого элемента кортежа. В теории типов это называется Σ-types, в агде выглядит как-то так:

Primes = Σ[ x ∈ ℕ ] prime-p x

Σ[ x ∈ A ] B это сахар для составления зависимого кортежа:

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

Как в Common Lisp

Там это простой assert времени выполнения. В типах это верификация времени компиляции, тут бы я ещё начал утверждать про непротиворечивость, но это вредно (а вот логическая противоречивость CL очевидна).

Когда на Си пишут глючную и медленную реализацию половины Common Lisp-а — это еще куда ни шло.

примеры таких реализаций будут?

предположу, что глючность объясняется *именно* тем, что делается реализация *лиспа* — т.е. в языке производится изменение AST вместо того, чтобы реализовывать именно языковую фичу

Конкретно в случае glib — это Vala, например.

вот-вот, вала — это как раз «личный с++» glib-щиков

К сожалению, идеология крестов такова, что она провоцирует снова и снова рождать велосипедные недохаскели.

это как минимум лучше, чем идеология, провоцирующая рождать велосипедные недоплюсы, гы-гы

насчет идеологии — качество языка программирования определяется в значительной степении тем, насколько мощный dsl в нем можно удобно сделать; но с++, похоже, делался совершенно без учета этого

Хаскели чтоле? В агде всё ок с типами «кольцо целых чисел» и «аддитивная группа целых чисел» :)

хаскели конечно, ведь никто, похоже, не пытается рекламировать агду исходя из посылки «тип это множество»

____________________________________________________

как ты оцениваешь количество строк кода на минимальную (полезную?) реализацию подмножества хаскеля внутри с++ (т.е. на шаблонах с грязными хаками внешними скриптами)

более подробно:

1. ленивые вычисления с редукцией графа (вот тут в основном вопрос)

2. кривоватый, но настоящий параметрический полиморфизм

3. создание замыканий там, где аргумент функции ленив

цель всего этого, на самом деле, учебная — получше прочувствовать рантайм хаскеля и больше узнать о неудобствах с++

Перейдите уже на хаскель, закопайте стюардессу.

так он же непредсказуемый нифига

вот если бы была маленькая libhaskell (что я примерно и предлагаю), было бы гораздо лучше

но, понятно, тем, кому *нужен* хаскель в более, чем 10% проекта (а, кхм, кто это вообще такие?), пусть юзают хаскель

так же профит libhaskell в том, что убирается лишняя свобода реализации

кстати, у «личного с++ поверх си» обычно этот аргумент (предсказуемость ресурсопотребления) не работает (за исключением случая, когда делается своя система исключений (каламбур получился) — там у плюсов реально плохо)

док

Есть pdf и djvu :) http://alexott.net/en/fp/books/#sec2

А так я не знаю что именно нужно — в посте было про параметризацию, индексирование, уровни и зависимые типы, так что можно почитать на пальцах например там — http://oxij.org/note/BrutalDepTypes.

Про категории и списки-функторы-монады — по первой ссылке (у Пирса).

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

я так полагаю, что это другой тип, но подтип первоначального типа... но именно что полагаю

А www_linux_org_ru говорил про множество которое carrier структуры.

да, его можно было бы назвать carrier (носитель) типа, но это все же не сам тип

вот-вот, вала — это как раз «личный с++» glib-щиков

Это утверждение говорит лишь о том, что вы не знакомы с glib.

Интуиция говорит, что тип одинаковый, а определение «Целочисленное деление? Тип, естественно, другой будет.»

тут можно считать, что в *обоих* случаях тип «целое со всеми использованными операциями»

на самом деле «лишние» операции в типе мешают довольно редко, и можно сказать единственный известный мне практический пример «лишней» операции — это доступ к n-му элементу последовательности, где этот доступ O(n)

речь, понятно, идет о «лишних» операциях, которые делаются из публичных операций над типом, и не идет об операциях, которые залезают в приватные части типа — последних случаев много, и там все ясно

а есть какое-нибудь место типа лора, где общаются по этой теме, или так не принято?

я на «ты» предпочитаю

Это утверждение говорит лишь о том, что вы не знакомы с glib.

ну так можно меня просветить

что я (вроде бы) знаю о glib при ее использовании из си:

1. там есть GObject, все объекты делаются из него, передается в функции часто (указатель?) именно на него, и тогда можно и нужно спрашивать у GObject, что это за объект на самом деле

2. есть reference counting, при выходе из блока он автоматически не декрементируется, так что это надо делать ручками

Там объектная система вся построена на идее инстроспекции. Конечно, не в таком объёме, как в ruby, но для накодированной практически из говна и палок системы (поскольку Си всё-таки никак этому не помогает, а скорее всеми способами мешает), весь впечатляюще.

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

Класс определяется как совокупность методов, сигналов и свойств. Cигналы и свойства связываются «в рантайме», т.е. их имена являются обычными строками, по которым осуществляется связывание. Для сигнала можно узнать его сигнатуру, для свойства — тип.

По сути glib определяет компонентную модель для динамически типизированного языка. Текущие ограничения на её применение это фактически ограничения Си: например, в Си практически бессмыслено динамическое связывание методов по имени или их интроспекция, поэтому этого нет.

(В gtk, который есть надстройка над glib, вообще можно синтезировать целые объектные иерархии по xml-дереву. Те случае, когда xml используется в приложении, чтобы нарисовать формочку с полутора кнопками — это на самом деле очень примитивное использование. Во-первых, этот язык разметки способен на большее. Во-вторых, сам gtk также способен на большее, и многие возможности, которые органично следуют из его архитектуры, просто недоделаны. То ли из-за нехватки сил у разработчиков, то ли потому что это всё невостребовано прикладниками, которые используют только те самые «полторы кнопки».)

Поэтому я еще раз повторю тезис, который выше озвучивал: glib — это шаг в сторону Objective C, Javascript, Ruby, но никак не в сторону С++. Объектная и темплейтная модели крестов в данном случае «не про то», т.е. совершенно про другое.

есть какой-нибудь док, где на пальцах систематически изложен данный матан применительно к ЯП? В смысле, не «мыслью по древу» «всё на свете что хоть как-то касается логики». А конкретный понимабельный эээ инструмент, содержащий минимум шизофазии.

DCPL?..

на это все надо отвечать достаточно длинно (и не сразу), так что вот краткий ответ:

Поэтому я еще раз повторю тезис, который выше озвучивал: glib — это шаг в сторону Objective C, Javascript, Ruby, но никак не в сторону С++. Объектная и темплейтная модели крестов в данном случае «не про то», т.е. совершенно про другое.

когда я 1-й раз говорил о «личном с++», я говорил именно топикстартеру в том контексте, что он, фактически, предложил отказаться от объектов в пользу сишных структур — и я ему объяснил, для чего нужных объекты

когда разговор идет уже с более грамотными людьми, то там я считаю не важным, реализованны объекты так сказать динамически в виде хэша «имя_метода ---> код_метода» или так сказать статически в виде «смещение_метода_в_vtbl ---> код_метода»

«не важным» в том смысле, что результат это уже не си, а «личный с++»

а если взять тему «а как же правильно реализовывать», то тут *мое* мнение *целиком* не совпадает ни с типичными динамическими языками, ни с плюсами — должны быть предоставлены *обе* возможности, при этом для тех, кто хочет быстродействия, должна быть возможность локально запретить хэши

Там объектная система вся построена на идее инстроспекции. Конечно, не в таком объёме, как в ruby,

в чем разница в объеме? для начала, поля и методы — это элементы хэша?

glib — это шаг в сторону Objective C, Javascript, Ruby, но никак не в сторону С++

ок, в разговоре с более грамотными людьми «личный с++» можно заменить на «личный оо язык с доступом к низкому уровню», но это чересчур длинно

а вот случае kernel.org, насколько я могу судить по http://en.wikipedia.org/wiki/Sparse, расширение пошло совсем не в сторону оо и даже не совсем в сторону с++ (__acquire(x), __release(x), __rcu...) — но все равно, скажем, различные типы __le32 и __be32 могут быть сделаны на с++, поэтому с некоторой натяжкой можно говорить о «личном с++»

поэтому с некоторой натяжкой можно говорить о «личном с++»

О sparse невозможно говорить как о «личном оо языке с доступом к нижнему уровню». Совсем. Ни с какой натяжкой.

а я и не собираюсь

о нем я буду говорить как о «личном с++», пусть и с натяжкой

хаскели конечно

В хаскеле вполне можно представлять себе тип как множество. Если рядом есть какой-то интерфейс IFace, то есть другое множество типа tuple<typename, function<IFace<A>(A)>> из всех типов у которых есть реализация IFace, если у исходного типа Foo она есть, то есть элемент make_tuple(Foo, InstanceOfTypeIFace_Foo_). При этом, ещё другой tuple<typename, function<IFace2<A>(A)>> никак с первым не конфликтует, но тоже множество.

как ты оцениваешь количество строк кода на минимальную (полезную?) реализацию подмножества хаскеля внутри с++ (т.е. на шаблонах с грязными хаками внешними скриптами)

Не представляю. Вместо GC будут счётчики ссылок? Или консервативный вариант? Как будет записываться и работать в константной памяти

ns = 1 : 2 : ns
main = mapM_ print $ take 100500 ns

? Есть http://github.com/beark/ftl (там есть lazy.h) код которого как-то отбивает охоту заниматься подобным в C++.

ленивые вычисления с редукцией графа (вот тут в основном вопрос)

Интерпретатор? Такой есть в pj-lester-book (Template.hs).

кривоватый, но настоящий параметрический полиморфизм

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

создание замыканий там, где аргумент функции ленив

Если ленив, то проще всего сделать отложенное вычисление в лямбде, но тогда чаще всего там будет замыкание, да, так что лямбда с captures (и всюду следить за = и &) и толстый std::function, плюс std::shared_ptr повсюду.

ЖЖ, прочие блоги, рассылки? На SO есть немножко. А так теория типов это же академщина — кафедры / конференции / пейперы.

уравнения для типов не решаются в категории Set, то есть типы не могут быть обычными множествами

Зато прекрасно решаются, если ограничиться перечислимыми множествами (каковое ограничение вполне логично). И нахрена выдумывать совершенно искусственную конструкцию с топологическими пространствами? Нахрен не надо.

для начала, поля и методы — это элементы хэша?

Сигналы и свойства - элементы хэша. Методы - обычное имя в объектнике, которое связывается линкером. (Но при вызове имплементация метода будет диспетчеризовываться через vtable.) Поля — просто смещения в структуре. Но публичные поля — это дурной тон. А приватные так использовать вполне логично.

В общем, технологически, лютая смесь Си с JS.

anonymous посягнулся на теорию, так сказать нашу, доменов?

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

разрешимым функциям

А (y id) как моделировать (речь была про нетипизированное)?

теория доменов оказывается лишней сущностью

Пушка же.

А (y id) как моделировать (речь была про нетипизированное)?

А в чем проблема с (y id)? Она вполне разрешима. Вообще неразрешимых ф-й в программировании не существует, не напишешь ты код для такой ф-и, что характерно. И ВНЕЗАПНО непрерывные ф-и - это как раз разрешимые, точь в точь.

Пушка же.

То есть по-твоему искусственная конструкция, которая ничего не привносит и существует поверх -это НЕ лишняя сущность?

Ну а если конкретно, (y id) - пустое множество. (т.к. она возвращает ничего (пустое множество) и dom*{} = {}, то и подмножество произведения - тоже пустое, очевидно)

Вообще неразрешимых ф-й в программировании не существует

Во-первых, http://cs.stackexchange.com/questions/3555/what-is-the-difference-between-dec...

It makes no sense to say a function is decidable.

Во-вторых — открывай Barendregt и смотри что называется разрешимым термом (ты про них), а что нет (такие тоже есть, там есть пример — Ω ≡ (λ x. x x) (λ x. x x), аналогично (y i)).

И ВНЕЗАПНО непрерывные ф-и - это как раз разрешимые, точь в точь.

Не могу понять (комментарий)

Кстати, насчёт «непрерывные функции вычислимы» — это ты тоже загнул, на самом деле: возьми любую функцию Integer->Integer, загоняющую (_|_) в себя; она непрерывна.

Я тогда загнул, да. Смотри http://www.math.psu.edu/simpson/notes/fom.pdf для того чтобы условиться про определения.

1. Пусть наш домен D это объект некоторой категории C. Необходимо D ≊ D → D. Согласно теореме Кантора С ≠ Set (так как единственный такой D в Set тривиально синглетон, что не даёт непротиворечивой модели).

2. При этом C — CCC (точнее, предпочтительно CCC), так как D → (D → D) ≊ D × D → D.

3. CPO подходит как категория для моделей как разрешимых термов и вычислимых (тотально-рекурсивных) функций, так и неразрешимых термов и частично-рекурсивных функций.

Если ты хочешь ограничиться рассмотрением только тотальных функций — интересно посмотреть на ссылку с доказательством существования нетривиальных решений в SetPR / SetComp / etc. дающих непротиворечивые модели.

это НЕ лишняя сущность?

А ты открой Barendregt — там сплошная теория доменов везде. Предлагай тогда альтернативы для моделей теорий.

It makes no sense to say a function is decidable.

Для большинства людей вполне sense. Разрешимая = алгоритмически разрешимая = процесс вычисления которой алгоритмически разрешим = вычислимая. Очевидно же. Алсо, виснущие функции, очевидно, вычислимы (по определению, вычислимая = которая реализуется тьюринг-полным вычислителем, виснущая реализуется).

Не могу понять (комментарий)

И? Приведенная в пример ф-я вполне вычислима (т.к. реализуется на машине тьюринга). Собственно, топология Скотта _специально_ подобрана так, чтобы именно вычислимые функции и были непрерывными. То есть тогда понимали, что проблема именно в том, что нам надо ограничить ф-и вычислимыми, и ограничили. Но вместо того, чтобы сказать «ограничимся вычислимыми функциями» ввели лишнее усложнение.

Я тогда загнул, да. Смотри http://www.math.psu.edu/simpson/notes/fom.pdf для того чтобы условиться про определения.

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

Если ты хочешь ограничиться рассмотрением только тотальных функций

Зачем тотальных? Я говорю о вычислимых функциях. Они же - частично-рекурсивные. Они не обязательно тотальны. Этим функциям соответствует категория перечислимых множеств. При этом очевидно, что функция из перечислимого множества вычислима тогда и только тогда, когда ее множество (в Set функции - это тоже множества, как известно) перечислимо. Так что полученная категория Set_ (объекты - перечислимые множества, морфизмы - вычислимые функции) как раз будет и CCC.

3. CPO подходит как категория для моделей как разрешимых термов и вычислимых (тотально-рекурсивных) функций, так и неразрешимых термов и частично-рекурсивных функций.

Конечно подходит. Но дело то в чем - мы изначально берем именно категорию Set_ и потом замечаем, что она изоморфна CPO. Но вначале идет Set_, CPO - внешняя надстройка. И если она ничего конструктивного не привносит - то и лишняя надстройка. А она ничего не привносит.

А ты открой Barendregt — там сплошная теория доменов везде.

В 99% случаев там можно не исправляя текста просто заменить подлежающую категорию на Set_ и все будет в порядке. Только понятнее станет и уберутся лишние сущности.

Хотя я несколько поторопился на счет изоморфизма Set_ и CPO, в CPO есть неперечислимые множества (но из них нету стрелок. зато есть стрелки _в них_). То есть когда мы отображаем бестиповую лямбду в CPO, то это не сюрьекция. А вот в Set_ - все хорошо, сюрьекция :)

Ну и в CPO есть стрелки, которым никакая осмысленная ф-я не будет соответствовать, то есть сама стрелка будет вычислимой функцией, но она будет из множества, которое мы не сможем построить и _применение_ этой ф-и будет невычислимо :)

То есть интерпретатор CPO алгоритмически неразрешим.

но она будет из множества, которое мы не сможем построить

Во множество, которые мы не можем построить, то есть таки разрешимо, да selffix/

Разрешимая = алгоритмически разрешимая = процесс вычисления которой алгоритмически разрешим = вычислимая

И всё бы хорошо, но разрешимый = есть HNF (см. Barendregt), то есть тотально и не виснет. Вот я называю тотально-рекурсивные вычислимыми (и только).

http://www.math.psu.edu/simpson/notes/fom.pdf

Definition 1.3.1 (Computable Functions). A k-place number-theoretic function λx1 . . . xk [f(x1, . . ., xk)] is said to be computable if there exists a register machine program P which computes it, i.e. for all x1, . . ., xk ∈ N, P(x1, . . . , xk) eventually halts with y = f(x1, . . ., xk) in Rk+1.

Definition 1.4.1 (Recursive Functions and Predicates). A k-place (total) function is said to be recursive if and only if it is computable. A k-place predicate is said to be recursive if its characteristic function is recursive.

Definition 1.4.2 (Partial Recursive Functions). A k-place partial function ψ is said to be partial recursive if it is computed by some register machine program P. This means that, for all x1, . . . , xk ∈ N, ψ(x1, . . . , xk) ≃ the number in Rk+1 if and when P(x1, . . ., xk) stops. In particular, ψ(x1, . . ., xk) is defined if and only if P(x1, . . ., xk) eventually stops.

http://en.wikipedia.org/wiki/Computable_function#Computable_sets_and_relations

http://en.wikipedia.org/wiki/R_(complexity)

http://en.wikipedia.org/wiki/RE_(complexity)

http://en.wikipedia.org/wiki/Recursively_enumerable_set#Formal_definition

λ-определимо <=> частично рекурсивно.

Программа == процедура != алгоритм. http://stackoverflow.com/questions/879015/what-is-the-difference-between-an-a....

Приведенная в пример ф-я вполне вычислима

Но приведена она как пример не (тотально) вычислимой функции :)

Они же - вычислимые.

Но по цитируемой ссылке другое определение :)

Алсо, виснущие функции, очевидно, вычислимы

Ну как хочешь, пусть вычислимы = частично-рекурсивны.

Set_

Ок, с терминологией разобрались. Где почитать про свойства Set_, решения уравнений в ней и построение с её же помощью моделей LC?

Для конкретной модели нас интересует не вся CPO а только нужный (r.e.) рефлексивный домен же.

То есть интерпретатор CPO алгоритмически неразрешим.

Блин, опять. Интерпретатор любого тьюринг-полного языка такой, потому что eval semidecidable по отношению к проблеме останова (говорит «да» за конечное время и молчит сколько угодно долго иначе).

Интерпретатор любого тьюринг-полного языка такой

Что за бред ты говоришь? Интерпретаторы как раз алгоритмически разрешимы.

потому что eval semidecidable по отношению к проблеме останова (говорит «да» за конечное время и молчит сколько угодно долго иначе).

При чем тут проблема останова?

И всё бы хорошо, но разрешимый = есть HNF

Нет, разрешимо = вычислимо.

см. Barendregt)

Барендрегт может что угодно придумывать в своей собственной нотации (это вобщемто вполне нормально когда локально для одной работы переопределяют какие-то термины), но когда я говорю о вычислимых функциях - я говорю об общепринятом определении, вычислимая = частично-рекурсивная = реализуемая на машине тьюринга, так мои слова и надо воспринимать. Не надо их додумывать и перевирать - я имел ввиду именно то, что сказал. Я лучше знаю, что говорил, ок?

Но приведена она как пример не (тотально) вычислимой функции :)

А при чем тут тотальность? Да, она не тотальна. Но вычислима (частично-рекурсивна, реализуется машиной тьюринга).

Но по цитируемой ссылке другое определение :)

Это лично определение Барендрегта. Я использую общепринятое.

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

Ок, с терминологией разобрались. Где почитать про свойства Set_, решения уравнений в ней и построение с её же помощью моделей LC?

Так вся CS теория. Я же сказал - все остается таким же, только не нужно строить искусственных конструкций вроде топологии Скотта.

Нам нужен как минимум 1 объект в категории на каждую функцию (она же CCC).

Что за бред ты говоришь? Интерпретаторы как раз алгоритмически разрешимы.

При чем тут проблема останова?

Пусть интерпретатор это функция eval. К какому классу сложности ты отнесёшь eval? R или RE?

разрешимо = вычислимо

Вот тебе два синонимических ряда. Первый — тотально, не виснет, разрешимо, всегда есть нормальная форма, тотально-рекурсивно, эффективный метод, (эффективный) алгоритм, R. Второй — частично, может виснуть, полуразрешимо, может не иметь нормальной формы, частично-рекурсивно, метод/процедура/программа тьюринг-полного вычислителя, RE.

Ты можешь относить «вычислимо» ко второму — никаких проблем, но тогда не приплетай разрешимость — вот тут претензия.

Это лично определение Барендрегта. Я использую общепринятое.

Не, у него про разрешимые термы, про вычислимость как-то не заметил. Я про ссылку на fom.pdf (негодная ссылка! не «общепринятые» определения!).

Так вся CS теория. Я же сказал - все остается таким же, только не нужно строить искусственных конструкций вроде топологии Скотта.

Я прощу конкретных ссылок. 1) Подкатегория Set о которой речь. 2) Уравнения для рефлексивных доменов в ней и их решения. 3) Модели и непротиворечивость теорий нетипизированного LC (тащемто, до Скотта таковых не было).

Я сказал про Barendregt. Вот ещё — http://arxiv.org/pdf/0904.4756v1.pdf.

Нам нужен как минимум 1 объект в категории на каждую функцию (она же CCC).

В нетипизированном LC это всё один и тот же объект, называтся «рефлексивный домен» (суть «единственный тип» нетипизированного языка), для него D ~ [D => D].

Из ссылки выше:

Definition 1. (Categorical model) A categorical model of λ-calculus is a reflexive object of a Cartesian closed category C, i.e., a triple U = (U, A, λ) such that U is an object of C, and A : U → [U ⇒ U] and λ : [U ⇒ U] → U are two morphisms satisfying A ◦ λ = Id[U⇒U].

И ещё — на каждую функцию (терм) не может быть нужно по объекту, так как термы вообще моделируются как стрелки D^k -> D (экспоненциал это всё функциональное пространство, а не для конкретных функций — в теории с одним типом это будет единственное функциональное пространство изоморфное самому типу).

Пусть интерпретатор это функция eval. К какому классу сложности ты отнесёшь eval? R или RE?

RE, конечно. Вычислимая функция.

Ты можешь относить «вычислимо» ко второму — никаких проблем, но тогда не приплетай разрешимость — вот тут претензия.

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

Я прощу конкретных ссылок. 1) Подкатегория Set о которой речь. 2) Уравнения для рефлексивных доменов в ней и их решения. 3) Модели и непротиворечивость теорий нетипизированного LC (тащемто, до Скотта таковых не было).

Ты дурак? Еще раз - берешь того же Барендрегта. Он пишет про Set_.

В нетипизированном LC это всё один и тот же объект, называтся «рефлексивный домен» (суть «единственный тип» нетипизированного языка), для него D ~ [D => D].

Да, я поторопился, у нас класс морфизмов - объект, но морфизм не обязательно является объектом.

забьем на спор о терминологии

Как только будет «с точностью до» замены слов без возможности противоречий. А пока ты говоришь «decidable» с одной стороны и «RE» (в которой есть undecidable вещи) — с другой.

http://en.wikipedia.org/wiki/Undecidable_problem

Formally, a decision problem is a subset of the natural numbers. The corresponding informal problem is that of deciding whether a given number is in the set. A decision problem A is called decidable or effectively solvable if A is a recursive set. A problem is called partially decidable, semi-decidable, solvable, or provable if A is a recursively enumerable set. This means that there exists an algorithm that halts eventually when the answer is yes but may run for ever if the answer is no. Partially decidable problems and any other problems that are not decidable are called undecidable.

eval в RE, да (но не в R, так как в R _только_ тотальные функции), но он как раз semidecidable по отношению к проблеме останова, то есть an algorithm that halts eventually when the answer is yes but may run for ever if the answer is no.

А вот в http://en.wikipedia.org/wiki/Decidability_(logic)

In logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas, or, more precisely, an algorithm that can and will return a Boolean true or false value (instead of looping indefinitely).

Слово algorithm = effective algorithm = effective method это именно тотальный алгоритм из R.

Еще раз - берешь того же Барендрегта. Он пишет про Set_.

Виртуально? Не нашёл Set_ в указателе. Нашёл CPO начиная с 1.2.

Возвращаясь

Зато прекрасно решаются, если ограничиться перечислимыми множествами

В Set вообще функции тотальны (в математическом смысле, то есть нет денотации для non-termination). Так что по любому нужно добавлять _|_ и смотреть как ведут себя функции по отношению к ним, так что уже будет простая топологическая конструкция множеств со структурой (называется SetPart/Par делается как Set*/Set_|_), но это не удобно, учитывая наличие разных стратегий вычисления (особенно ленивой), поэтому CPO.

Так что по любому нужно добавлять _|_ и смотреть как ведут себя функции по отношению к ним, так что уже будет простая топологическая конструкция множеств со структурой (называется SetPart/Par делается как Set*/Set_|_)

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

но это не удобно

Это как раз удобно, потому что нету лишних надстроек.

поэтому CPO

Почему СРО? Еще раз - нам понятно, что СРО - это надстройка, то есть она вводит дополнительные сущности. Это должно быть обосновано - чем оно обосновано? Что дает СРО, чего нету в перечислимых множествах?

Виртуально? Не нашёл Set_ в указателе. Нашёл CPO начиная с 1.2.

Вот везде где говорится СРО смело подставляй Set_.

Слово algorithm = effective algorithm = effective method это именно тотальный алгоритм из R.

Алгоритм не обязан быть тотальным. Мы уже об этом с тобой разговаривали.

eval в RE, да (но не в R, так как в R _только_ тотальные функции)

А я ни разу об R и не говорил. Я говорил о вычислимых (разрешимых) функциях, которые RE.

Как только будет «с точностью до» замены слов без возможности противоречий. А пока ты говоришь «decidable» с одной стороны и «RE» (в которой есть undecidable вещи) — с другой.

Функция RE тогда и только тогда, когда она decidable (задача ее вычисления алгоритмически разрешима), да.

Сможешь привести контрпример?

«RE» (в которой есть undecidable вещи)

Все RE decidable.

Откуда взялась топологическая структура?

http://homepages.inf.ed.ac.uk/gdp/publications/Domains_a4.ps — читать 1, то есть с самого начала.

Теперь я:

f :: Bool -> Bool
f !x = if x then False else f x

t :: (Bool, Bool, Bool)
t = (f True, f False, let bot = bot in f bot)

Bool = {False, True}, а f : Bool → Bool? Нет. Bool⊥ = {⊥, False, True}, так что ⊥ ≤ False и ⊥ ≤ True, f : Bool⊥ → Bool⊥, f строгая (сохраняет ⊥, она и так сохраняет, но это общее свойство — строгие сохраняют, ленивые — не обязательно) и монотонная. Видишь poset-ы и монотонные функции? Дальше читай Плоткина (и http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf и что угодно по теории доменов) — почему cpo's, где open sets топологии (и непрерывность).

Вот везде где говорится СРО смело подставляй Set_.

«Вот везде где говорится СРО смело подставляй хрень которую я придумал на ЛОРе и упорно не даю ссылок про которую». Я знаю что Set подставлять вместо CPO нельзя. Я не знаю что такое Set_. То есть есть теория доменов, ты говоришь «не нужно», но не говоришь что нужно (то есть не говоришь где учебники про LC, его теории и модели которые бы не использовали теорию доменов).

Алгоритм не обязан быть тотальным.

Я говорю что в статье «Decidability (logic)» говорится именно про тотальный алгоритм (могут ли они быть не тотальными тут не интересно). Равно как и все проблемы R решаются тотальными вычислимыми функциями.

Мы уже об этом с тобой разговаривали.

http://stackoverflow.com/questions/879015/what-is-the-difference-between-an-a... — как-то не я один понимаю Кнута как понимаю.

Я говорил о вычислимых (разрешимых) функциях, которые RE.

Вот и прекращай позориться и называть их разрешимыми — 1) они функции, разрешимы могут быть множества, предикаты, проблемы, термы, языки, теории, разве что функцию f : A → B можно ассоциировать с проблемой (множеством) {(x, y) | f(x) == y, x ∈ A, y ∈ B} и решать её с помощью g(x, y) = f(x) == y, 2) они могут тестировать неразрешимые проблемы.

Сможешь привести контрпример?

http://en.wikipedia.org/wiki/RE_(complexity)#RE-complete

halts(x) = eval x; return 0 это та самая частичная функция (f в https://en.wikipedia.org/wiki/Recursively_enumerable_set#Equivalent_formulations) которая полностью тестирует semidecidable проблему останова. Не тотальная halts частично-рекурсивна и полностью тестирует RE-complete проблему из RE (не из R) на предмет ответов «да». Откуда проблема останова разрешима (decidable) — отлично, чо.

Все RE decidable.

http://complexityzoo.uwaterloo.ca/Complexity_Zoo:R#re

Вместе с проблемой останова. Тьюринг рад.

З.Ы. могу предположить откуда происходит непонимание — http://en.wikipedia.org/wiki/Recursive_set

a set of natural numbers is called recursive, computable or decidable if there is an algorithm which terminates after a finite amount of time and correctly decides whether or not a given number belongs to the set.

algorithm which terminates after a finite amount of time

A subset S of the natural numbers is called recursive if there exists a total computable function f

total computable function

Синонимичность «computable» и «decidable» имеет место быть если под «computable» понимаются тотально-рекурсивные функции.

Иначе http://en.wikipedia.org/wiki/Recursively_enumerable_set

a set S of natural numbers is called recursively enumerable, computably enumerable, semidecidable, provable or Turing-recognizable if: There is an algorithm such that the set of input numbers for which the algorithm halts is exactly S.

the set of input numbers for which the algorithm halts is exactly S

A set S of natural numbers is called recursively enumerable if there is a partial recursive function (synonymously, a partial computable function) whose domain is exactly S, meaning that the function is defined if and only if its input is a member of S.

partial computable function

«computably enumerable», «semidecidable», «partial computable» — твоё «computable», то есть частично-рекурсивные функции, но ни в коем случае не «decidable» тут.

http://homepages.inf.ed.ac.uk/gdp/publications/Domains_a4.ps — читать 1, то есть с самого начала.

Бросай свою привычку овтечать невпопад. Напоминаю - речь шла о перечислимых множествах, при чем тут твоя ссылка?

Дальше читай Плоткина (и http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf и что угодно по теории доменов) — почему cpo's, где open sets топологии (и непрерывность).

Так я и говорю о том, что это все надстройка над Set_, причем лишняя, которая ничего не дает.

Я знаю что Set подставлять вместо CPO нельзя. Я не знаю что такое Set_.

Я выше объяснил, что такое Set.

«Вот везде где говорится СРО смело подставляй хрень которую я придумал на ЛОРе и упорно не даю ссылок про которую».

Ну на тебе ссылку: http://en.wikipedia.org/wiki/Recursively_enumerable_set

что такое Set.

Set_

уравнения для типов не решаются в категории Set, то есть типы не могут быть обычными множествами

Зато прекрасно решаются, если ограничиться перечислимыми множествами (каковое ограничение вполне логично). И нахрена выдумывать совершенно искусственную конструкцию с топологическими пространствами?

«уравнения для типов» это уравнения для рефлексивного домена вида D ≊ D × D ≊ [D ⇒ D], D ≠ 1. Пример домена я привёл — Bool⊥ который _уже_ poset (CPO), все вычислимые функции над ним _уже_ монотонны (непрерывны). В ULC у нас нет отдельного Bool, а именно что рефлексивный домен который естественным образом _уже_ устроен как CPO, а вычислимые функции _уже_ непрерывны.

Так при чём тут перечислимые множества и какие уравнения ты собрался решать в какой-то «Set_»? Начни хотя бы с примера с Bool и f — что будет вместо ⊥, порядка и монотонности?

Ну на тебе ссылку

Всё ещё

не говоришь где учебники про LC, его теории и модели которые бы не использовали теорию доменов

По ссылке нет никакого упоминания категории Set_, тем более доказательств что это категория, что в ней решаются уравнения, что решения-объекты годны как модели теорий ULC.

Речь-то шла чем считать типы — просто множествами значений? Типа Bool = {False, True}? А я сказал, что в программировании с частичными функциями это множества со структурой, а сами вычислимые функции — определенные функции сохраняющие структуру.