Тьюринг-полнота

[proger]

Допустим есть некий тьюринг-неполный язык. На нем мы можем реализовать исполнитель тьюринг-полного языка. (пример agda-->brainfuck)

Но это неинтересно. Интересно другое. Мы можем из программы тьюринг-неполного языка вызвать исполнитель тьюринг-полного, написанного на этом языке и результат вычисленного выражения записать в output. Получается, что на тьюринг-неполном языке мы вычислили выражение заведомо невычислимое на этом языке. Внимание! Никакой другой язык, кроме нашего, слабого, мы не использовали.

Таким образом, мы имеем тут парадокс. Никакой Тьюринг-полноты не существует.

[Xaositect]

proger в сообщении #874565 писал(а):

Допустим есть некий тьюринг-неполный язык. На нем мы можем реализовать исполнитель тьюринг-полного языка. (пример agda-->brainfuck)

Не можем. Agda --- это тьюринг-полный язык, там есть коиндукция.

[proger]

Xaositect в сообщении #874584 писал(а):

Agda --- это тьюринг-полный язык, там есть коиндукция.

Может быть у Вас есть пруф, что коиндукция делает язык тьюринг-полным?

[arseniiv]

proger в сообщении #874565 писал(а):

Таким образом, мы имеем тут парадокс. Никакой Тьюринг-полноты не существует.

Хе-хе. Если я буду исходить из того, что слоны — фиолетовые, я тоже «парадокс» могу получить. Докажите сначала, что на тьюринг-неполном языке можно написать транслятор тьюринг-полного!

[Aritaborian]

(arseniiv)

[proger]

arseniiv в сообщении #874646 писал(а):

Докажите сначала, что на тьюринг-неполном языке можно написать транслятор тьюринг-полного!

Вообще-то я считал, что agda -- т-неполный. Мне встречалась такая информация неоднократно. А такая реализация есть, тут доказывать ничего не надо.

Однако Xaositect утверждает обратное, хотя пруфа от него я так и не дождался.

-- 12.06.2014, 19:03 --

arseniiv
Вот вы как думаете, в википедии написано: "Agda поддерживает ... проверку завершаемости программ". Это значит, что бесконечный алгоритм не скомпилируется. Можно такой ЯП считать тьюринг-полным? Я считаю что нет.

[arseniiv]

proger в сообщении #874653 писал(а):

Вообще-то я считал, что agda -- т-неполный. Мне встречалась такая информация неоднократно. А такая реализация есть, тут доказывать ничего не надо.

Тогда докажите, что он т-неполный. (Примем, что реализация — действительно реализация, я её не видел, но и проверять не хочу.)

И дальше вы всё-таки говорите просто о тьюринг-неполном языке — и если вы имеете в виду любой тьюринг-неполный язык, то доказать

arseniiv в сообщении #874646 писал(а):

что на тьюринг-неполном языке можно написать транслятор тьюринг-полного

вам всё же придётся.

proger в сообщении #874653 писал(а):

хотя пруфа от него я так и не дождался

Форум — это ведь не чат. Если неделя не прошла, говорить «не дождался» странновато.

(2 Aritaborian.)

Aritaborian в сообщении #874649 писал(а):

Уговорили, живых фиолетовых слонов. Кстати, с возвращением.

proger в сообщении #874653 писал(а):

Вот вы как думаете, в википедии написано: "Agda поддерживает ... проверку завершаемости программ". Это значит, что бесконечный алгоритм не скомпилируется.

Это может значить и другое. Конкретное значение всё же лучше читать в документации к Agda.

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

[Xaositect]

Я очень давно не брал в руки Агду, вот реализация оператора $\mu$:

module Test where

open import Coinduction renaming (∞ to Delayed; ♯_ to delay; ♭ to force)

data CoNat : Set where
  Z : CoNat
  S : (Delayed CoNat) -> CoNat

data Stream (a : Set) : Set where
  Cons : a -> (Delayed (Stream a)) -> Stream a

values' : (CoNat -> CoNat) -> CoNat -> Stream CoNat
values' f x = Cons (f x) (delay (values' f (S (delay x))))

values : (CoNat -> CoNat) -> Stream CoNat
values f = values' f Z

find : Stream CoNat -> CoNat
find (Cons Z xs) = Z
find (Cons (S x) xs) = S (delay (find (force xs)))

mu : (CoNat -> CoNat) -> CoNat
mu f = find (values f)

mu f - минимальное значение, при котором f равна Z, либо бесконечное число x = S(#x).

-- Чт июн 12, 2014 19:22:25 --

Conor McBride, http://permalink.gmane.org/gmane.comp.lang.agda/3132 писал(а):

Remember, "Agda is total, so it can't be Turing Complete" is as much nonsense as saying "Haskell is pure so it can't do IO".

[proger]

Xaositect в сообщении #874678 писал(а):

Haskell is pure so it can't do IO

А хаскель, и на самом деле не может IO, это не заложено в семантике. IO в нем -- это отдельная песня к ЯП не имеющая отношения, и имеющая свою собственную семантику.

[arseniiv]

proger в сообщении #874685 писал(а):

к ЯП не имеющая отношения

Ну тогда и в Си нет IO. Там же нет никаких особых языковых конструкций для этого. Или вы имели в виду что-то другое?

[proger]

arseniiv в сообщении #874687 писал(а):

Там же нет никаких особых языковых конструкций для этого

printf?:)

-- 12.06.2014, 19:34 --

arseniiv в сообщении #874687 писал(а):

никаких особых языковых конструкций

Вообще, любая запись в переменную -- это уже грязь. Нет принципиальной разницы, куда вы пишете.

[arseniiv]

proger в сообщении #874691 писал(а):

printf?:)

Чем это разительно отличается от хаскеля? printf — функция. Если её убрать, язык не сломается.

[proger]

arseniiv в сообщении #874696 писал(а):

отличается

Это шутка была. Там вообще все виды "записей" запрещены. Все операции записи/чтения спрятаны под капот. Изменение переменной -- это тоже частный случай записи, а там, с точки зрения семантики происходит связывание, а не присваивание. Ну а если разрешить на уровне языка явное IO, естественно чистота сломается, запись/чтение будет эквивалентно присваиваниям. Поэтому они прячут под капот это дело, типа, делают вид, что IO нет. А в си ты присваиваешь деструктивно, меняешь состояние, а это не тру. Но это все чушь, на самом деле, я сам это ФП не люблю.

[arseniiv]

(Оффтоп)

Я-то про хаскель знаю. И это неплохой, по-моему, способ.

[proger]

arseniiv в сообщении #874764 писал(а):

(Оффтоп)

Я-то про хаскель знаю. И это неплохой, по-моему, способ.

способ чего?