История изменений
Исправление quasimoto, (текущая версия) :
Вообще неразрешимых ф-й в программировании не существует
Во-первых, 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 — там сплошная теория доменов везде. Предлагай тогда альтернативы для моделей теорий.
Исходная версия quasimoto, :
Вообще неразрешимых ф-й в программировании не существует
Во-первых, 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 — СMС, так как D → (D → D) ≊ D × D → D.
3. CPO подходит как категория для моделей как разрешимых термов и вычислимых (тотально-рекурсивных) функций, так и неразрешимых термов и частично-рекурсивных функций.
Если ты хочешь ограничиться рассмотрением только тотальных функций — интересно посмотреть на ссылку с доказательством существования нетривиальных решений в SetPR / SetComp / etc. дающих непротиворечивые модели.
это НЕ лишняя сущность?
А ты открой Barendregt — там сплошная теория доменов везде. Предлагай тогда альтернативы для моделей теорий.