История изменений

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

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

Пусть интерпретатор это функция 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?

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

Вот тебе два синонимических ряда. Первый — тотально, не виснет, разрешимо, всегда есть нормальная форма, тотально-рекурсивно, эффективный метод, (эффективный) алгоритм, 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].