LINUX.ORG.RU

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

 


2

2

Под эквивалентностью я подразумеваю равенство выходных данных и произведенных побочных эффектов

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


def fib1(n):
    a, b = 0, 1
    for _ in range(n):
        a, b = b, a + b
    return a

def fib2(n):
    if n < 2:
        return n
    return fib2(n-1) + fib2(n-2)

как доказать что соотношения множеств входных и выходных данных для этих функций одинаковы (не учитывая переполнение стека для второй) ?

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


Ответ на: комментарий от emulek

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

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

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

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

qnikst ★★★★★
()
Последнее исправление: qnikst (всего исправлений: 1)
Ответ на: комментарий от emulek

и речь не про «big», а про просто integer, длинна которого не определена.

Одна история охуительнее другой. Что емулек ни бельмеса не смыслит в алгебре мы поняли уже давно - а сейчас он расписался в том, что и в программировании ни бум-бум.

anonymous
()
Ответ на: комментарий от quasimoto

То есть N мы можем расширять кардиналами в одну сторону оставляя полукольцо,

Почему полу? Вполне полноценное кольцо.

там наверно ещё и система бесконечно малых есть для обратных?

Естественно, в нестандартном расширении поля появятся бесконечно малые.

anonymous
()
Ответ на: комментарий от qnikst

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

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

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

конечно.

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

ну как-то так.

emulek
()
Ответ на: комментарий от anonymous

детка, я читер.

Не важно. Пиши.

предлагаешь мне сюда переписывать главы из Кнута? Может ты сам их прочитаешь?

emulek
()
Ответ на: комментарий от emulek

у нас речь за бесконечную машину. Потому деление тоже должно быть бесконечным.

Красота просто! Замечательный образец логики by emulek.

anonymous
()
Ответ на: комментарий от emulek

предлагаешь мне сюда переписывать главы из Кнута?

А ты напиши на сишке. Кнут же не на сишке писал.

anonymous
()
Ответ на: комментарий от anonymous

у нас речь за бесконечную машину. Потому деление тоже должно быть бесконечным.

Красота просто! Замечательный образец логики by emulek.

привыкай.

emulek
()
Ответ на: комментарий от anonymous

предлагаешь мне сюда переписывать главы из Кнута?

А ты напиши на сишке. Кнут же не на сишке писал.

примеры обычно на асме, но переложить на сишку не сложно. А зачем тебе? MIX очень простой.

emulek
()
Ответ на: комментарий от emulek

а зачем мне твоя ссылка?

Там определение. Такое же как и где угодно (поэтому пусть будет википедия, а то вот ещё есть — http://www.cse.chalmers.se/~nad/repos/lib/src/Algebra/Structures.agda). Оно предполагают некоторое знакомство с обычной теорией множеств (чтобы распарсить вещи типа «операция») и логикой (чтобы парсить утверждения с квантификациями и равенствами).

Я разве требовал, что-бы получалось?

В случае кольца целых чисел операция _/_ на (4, 3) либо не определена, либо определена но не является обратной к _*_, либо не является операцией (а более слабой конструкцией типа отношения).

Вот заменим (4, 3) на (x, 0) — та же фигня. И что из этого следует? Что четыре яблока не разделить нацело на трёх человек и что сколь угодно долгое но конечное по времени накручивание «ничего» не даст в итоге «чего-то»? Ну кольцо-то от этого никуда не девается, ему вообще пофиг на деление (в общем случае, в специальном случае целых чисел и евклидовых колец вообще есть деление с остатком и соответствующие свойства, так что в 4/3 таки больше смысла (quot и rem) чем в x/0 (смысла просто ноль при обычной нотации)).

Давай ты решишь проблему деления, напишешь программу, которая говорит «не получается», или «получается 1234545».

Просто возвращаем специальные значения для x/0 при x < 0; x/0 при x > 0, 0/0 и quot с rem в остальных случаях. Евклид говорит нам, что для данных целых чисел quot и rem уникальны, существуют и алгоритмически находимы (но писать это за О-большое это ж СА ;)).

quasimoto ★★★★
()
Ответ на: комментарий от emulek

> примеры обычно на асме, но переложить на сишку не сложно. А зачем тебе?

А тебе зачем? Это же ты первым попросил.

anonymous
()
Ответ на: комментарий от anonymous

Вполне полноценное кольцо.

Целые числа ({0, 1, 2, ...}) это полукольцо — нет у 2, например, аддитивного обратного (как и у aleph_n). Просто полукольца можно расширять бесконечностями по одной за раз сохраняя структуру (алгебраическую, порядок).

quasimoto ★★★★
()
Ответ на: комментарий от quasimoto

Целые числа ({0, 1, 2, ...})

Ты целые с натуральными перепутал. С натуральными, конечно, полукольцо.

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

Ага, но нестандартное расширение получается только если добавлять много бесконечностей.

anonymous
()
Ответ на: комментарий от quasimoto

Там определение

на кой мне определение хрен знает чего, если ты сам пишешь: «Вообще не вижу ничего про деление»?

Оно предполагают некоторое знакомство с обычной теорией множеств (чтобы распарсить вещи типа «операция») и логикой (чтобы парсить утверждения с квантификациями и равенствами).

моя ссылка про балет в китае наверное тоже что-то предполагает. Не смотрел. Давай вернёмся к теме?

Вот заменим (4, 3) на (x, 0) — та же фигня. И что из этого следует? Что четыре яблока не разделить нацело на трёх человек и что сколь угодно долгое но конечное по времени накручивание «ничего» не даст в итоге «чего-то»? Ну кольцо-то от этого никуда не девается, ему вообще пофиг на деление (в общем случае, в специальном случае целых чисел и евклидовых колец вообще есть деление с остатком и соответствующие свойства, так что в 4/3 таки больше смысла (quot и rem) чем в x/0 (смысла просто ноль при обычной нотации)).

тащем-то «кольцо» из математики не я притащил сюда. Я и сам в недоумении, при чём тут оно, и что оно доказывает. Разберись с анонимусом, я не в курсе.

Просто возвращаем специальные значения для x/0 при x < 0; x/0 при x > 0, 0/0 и quot с rem в остальных случаях. Евклид говорит нам, что для данных целых чисел quot и rem уникальны, существуют и алгоритмически находимы (но писать это за О-большое это ж СА ;)).

вот в том-то и дело, что Евклид просто говорит. Как и ты. На самом деле, эта твоя программа тебе докажет те самые вещи, о которых говорю я. А именно про отличие «бесконечного» числа от «любого». Ну и прочие мелочи, вроде проблемы остановки.

emulek
()
Ответ на: комментарий от qnikst

Теория множеств начиная с Кантора — мощности финитных множеств как финитные кардиналы, первый трансфинитный кардинал как мощность натурального ряда, aleph_0, его множество частей — мощность континуума, которая некий следующий кардинал (теорема Кантора), либо строго следующее (CH), aleph_1 = 2^aleph_0 и так далее, допуская GCH — 2^(2^aleph_0), 2^(2^(2^aleph_0)), ...

quasimoto ★★★★
()
Ответ на: комментарий от anonymous

Ты целые с натуральными перепутал.

Там N это ℕ было.

quasimoto ★★★★
()
Ответ на: комментарий от emulek

Я и сам в недоумении, при чём тут оно, и что оно доказывает

Целые числа о которых идёт речь, ℤ, образуют кольцо (евклидово). Любая _правильная_ конструкция для целых чисел (типа количества целых $ на счету с учётом долгов) будет реализовывать собой модель для теории (евклидовых) колец (наоборот — теория колец аксиоматизирует все такие конструкции) и будет изоморфна другим подобным конструкциям, всё вместе — ℤ со своим группоидом моделей. Что доказывает — ну нету в евклидовых кольцах вообще и в целых числах в частности каких-либо проблем с нулём, делением, бесконечностями т.п. Как и смысла в 0 / 0 = 5. То есть вещи устроены как устроены, а соответствующая математика вполне себе _непротиворечива_, так что мне тут непонятно где ты находишь свои проблемы :)

На самом деле, эта твоя программа тебе докажет те самые вещи, о которых говорю я. А именно про отличие «бесконечного» числа от «любого». Ну и прочие мелочи, вроде проблемы остановки.

Любой студент таких программ кучу писал, не вижу смысла этим заниматься, как и не вижу при чём тут идея бесконечности и проблема останова — ну поделишь ты два больших числа получив частное и остаток (например, qr = go 0 where go q r n = if r < n then (q, r) else go (q + 1) (r - n) n для положительных чисел методом вычитаний), реализовав любой из алгоритмов о котором прочитаешь на Википедии, у Кнута или где-то ещё, что с того?

quasimoto ★★★★
()
Последнее исправление: quasimoto (всего исправлений: 1)
Ответ на: комментарий от quasimoto

Целые числа о которых идёт речь, ℤ, образуют кольцо (евклидово). Любая _правильная_ конструкция для целых чисел (типа количества целых $ на счету с учётом долгов) будет реализовывать собой модель для теории (евклидовых) колец (наоборот — теория колец аксиоматизирует все такие конструкции) и будет изоморфна другим подобным конструкциям, всё вместе — ℤ со своим группоидом моделей. Что доказывает — ну нету в евклидовых кольцах вообще и в целых числах в частности каких-либо проблем с нулём, делением, бесконечностями т.п.

проблем нет. Да. Бесконечности в твоём(евклидовом) кольце тоже нет, как я понимаю? Ноль есть, я в курсе. А вот деления на него, как и делителей нуля, нет. Вот и проблемы нет. Я так могу «решить» любую проблему.

То есть вещи устроены как устроены, а соответствующая математика вполне себе _непротиворечива_, так что мне тут непонятно где ты находишь свои проблемы :)

непротиворечивость держится на неполноте. Увы. Тебе к аксиомам нужно добавлять разные костыли-исключения.

ну поделишь ты два больших числа получив частное и остаток (например, qr = go 0 where go q r n = if r < n then (q, r) else go (q + 1) (r - n) n для положительных чисел методом вычитаний)

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

emulek
()
Ответ на: комментарий от emulek

К примеру, я не знаю, что будет при «бесконечном числе»

Нету никаких «бесконечных чисел» в математике, сколько тебе раз еще это повторить?

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

anonymous
()
Ответ на: комментарий от emulek

непротиворечивость держится на неполноте.

Представь себе, нет. Ты опять лезешь в область, о которой не имеешь ни малейшего представления. Хватит делать выводы, основываясь на статьях из вики.

anonymous
()
Ответ на: комментарий от anonymous

тебе делать нечего, кроме как дописывать хрень к каждому моему комменту?

emulek
()
Ответ на: комментарий от emulek

Бесконечности в твоём(евклидовом) кольце тоже нет, как я понимаю?

Так же как в натуральных числах. Бесконечность как элемент есть в кардинальных, ординальных числах, расширенных вещественных/комплексных (в обычном анализе) и гиперреальных.

Вот и проблемы нет

Ну вот.

Тебе к аксиомам нужно добавлять разные костыли-исключения.

То есть ты бы предпочёл теорию которая не имеет «физического» смысла? Если ты занимаешься счётом, то уравнение x * 0 = 1 не решается, очевидно.

А как это связано с

непротиворечивость держится на неполноте

?

Если у тебя есть идея о том как бесконечность может быть числом и как такие числа должны работать (включая правильное обратное деление и решение x * 0 = 1), то делаешь себе такую структуру и решаешь тем все «проблемы», до неполноты тут далеко (неполнота это, например, CH (тоже связанная с бесконечностями) которая формулируется, но не доказывается, то есть при необходимости должна быть аксиомой, на самом деле).

quasimoto ★★★★
()
Последнее исправление: quasimoto (всего исправлений: 1)
Ответ на: комментарий от quasimoto

Бесконечности в твоём(евклидовом) кольце тоже нет, как я понимаю?

Так же как в натуральных числах.

вот. Именно это я и пытался донести здешней публике.

Бесконечность как элемент есть в кардинальных, ординальных числах, расширенных вещественных/комплексных (в обычном анализе) и гиперреальных.

и это тоже.

То есть ты бы предпочёл теорию которая не имеет «физического» смысла?

нет. Я просто говорю, что теорию нельзя просто так взять, и перенести на первую взятую абстракцию, такую как МТ. Бесконечность она в математике разная бывает, и просто сказать «бесконечная лента» недостаточно.

Если ты занимаешься счётом, то уравнение x * 0 = 1 не решается, очевидно.

естественно. Вот только я специально говорил про 0/0. Впрочем, я согласен, что результат 0/0 тоже не имеет смысла. Да.

А как это связано с «непротиворечивость держится на неполноте»

неполнота связана с использование бесконечно большого числа(из мат. анализа) при анализе МТ и проблемы её останова.

emulek
()
Ответ на: комментарий от emulek

Бесконечность она в математике разная бывает, и просто сказать «бесконечная лента» недостаточно

http://www.andrew.cmu.edu/user/avigad/Teaching/candi_notes.pdf

The machine has a two-way infinite tape with discrete cells. Note that “infinite” really means “as big as is needed for the computation”; any halting computation will only have used a finite piece of it.

The textbook describes Turing machines with only two symbols, 0 and 1; but one can show that with only two symbols, it is possible to simulate machines with more. Similarly, some authors use Turing machines with “one-way” infinite tapes; with some work, one can show how to simulate two way tapes, or even multiple tapes or two-dimensional tapes, etc.

Такая же бесконечность, что и в случае натуральных (one-way tapes) и целых чисел (two way tapes, и изоморфных — помноженных декартово на конечные множества (больше алфавита), на те же бесконечные (two-dimensional tapes), параллельно (multiple tapes)) — любая программа за конечное число шагов потребует конечного, но сколь угодно большого куска ленты, как и любое целое число не бесконечно, но всего их бесконечно много.

неполнота связана с использование бесконечно большого числа(из мат. анализа) при анализе МТ и проблемы её останова.

Вообще первая теорема о неполноте следует из проблемы останова — http://www.scottaaronson.com/blog/?p=710, а сама она — http://www.bemuzed.com/lucasd/halting-poem.html :)

quasimoto ★★★★
()
Последнее исправление: quasimoto (всего исправлений: 2)
Ответ на: комментарий от quasimoto

Про непротиворечивость - любая нетривиальная не противоречивая теория неполна (ц) Гёдель, правда к чему это в данной дискуссии мне не ясно:)

qnikst ★★★★★
()
Ответ на: комментарий от qnikst

Если теория аксиоматически считает себя непротиворечивой или может это доказать, то она противоречива (ц) он же :)

quasimoto ★★★★
()
Ответ на: комментарий от anonymous

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

А равенство fib1 и fib2 и вообще всё равно ручками придётся доказывать.

quasimoto ★★★★
()
Ответ на: комментарий от quasimoto

http://www.andrew.cmu.edu/user/avigad/Teaching/candi_notes.pdf

Theorem 3.3.8 (Rice’s theorem) Let C be any set of partial computable functions, and let A = {n | ϕn ∈ C}. If A is computable, then either C is ∅ or C is the set of all the partial computable functions.

An index set is a set A with the property that if n and m are indices which “compute” the same function, then either both n and m are in A, or neither is. It is not hard to see that the set A in the theorem has this property. Conversely, if A is an index set and C is the set of functions computed by these indices, then A = {n | ϕn ∈ C}.

With this terminology, Rice’s theorem is equivalent to saying that no nontrivial index set is decidable. To understand what the theorem says, it is helpful to emphasize the distinction between programs (say, in your favorite programming language) and the functions they compute. There are certainly questions about programs (indices), which are syntactic objects, that are computable: does this program have more than 150 symbols? does it have more than 22 lines? Does it have a “while” statement? Does the string “hello world” every appear in the argument to a “print” statement? Rice’s theorem says that no nontrivial question about the program’s behavior is computable. This includes questions like these: does the program halt on input 0? Does it ever halt? Does it ever output an even number?

С равенство частичных функций, то есть программ, та же история.

quasimoto ★★★★
()
Последнее исправление: quasimoto (всего исправлений: 1)
Ответ на: комментарий от qnikst

Про непротиворечивость - любая нетривиальная не противоречивая теория неполна (ц) Гёдель, правда к чему это в данной дискуссии мне не ясно:)

по ссылке выше:

Instead, I simply observe Gödel’s Theorem as a trivial corollary of what I see as its conceptually-prior (even though historically-later) cousin: Turing’s Theorem on the unsolvability of the halting problem.

emulek
()
Ответ на: комментарий от emulek

неполнота связана с использование бесконечно большого числа(из мат. анализа) при анализе МТ

Ты сколько раз еще будешь повторять этот идиотизм? Ни в матанализе, ни в МТ нету никаких «бесконечных чисел». Это твоя выдумка, пойми.

anonymous
()
Ответ на: комментарий от quasimoto

Если теория аксиоматически считает себя непротиворечивой или может это доказать, то она противоречива (ц) он же :)

Но не любая теория. Так же как не для любого ЯП проблема останова неразрешима. Если ЯП не тьюринг-полон - то, возможно, вполне разрешима :)

anonymous
()
Ответ на: комментарий от quasimoto

А равенство fib1 и fib2 и вообще всё равно ручками придётся доказывать.

Если проблема останова разрешима - то, очевидно, и проблема эквивалентности становится тривиально разрешимой. Достаточно рассмотреть, останавливается или нет программа, которая ищет контрпример для гипотезы «программы эквивалентны».

anonymous
()
Ответ на: комментарий от anonymous

и проблема эквивалентности становится тривиально разрешимой. Достаточно рассмотреть, останавливается или нет программа, которая ищет контрпример для гипотезы «программы эквивалентны».

толку-то от этого «доказательства»?

emulek
()
Ответ на: комментарий от anonymous

Но не любая теория

Достаточно выразительная, да. Например, базовые Agda с Coq строго выразительней PA, так что тоже попадают под действие этих теорем (Гёделя, в смысле), хотя проблема останова и разрешима для них.

Если проблема останова разрешима - то, очевидно, и проблема эквивалентности становится тривиально разрешимой.

Но у нас всё равно нет чёрного ящика в который можно будет закидывать fib1 с fib2 (в каком виде вообще?) и за конечное время получать ответы «равны» или «не равны», туда придётся забросить так же и доказательство предполагаемо населяющее утверждение «fib1 = fib2» и получать тогда ответы «подходит» или «нет» — в такого рода языке пруфчек разрешим, да (отсутствие Тьюринг-полноты тут может играть роль), но в смысле Entscheidungsproblem этот частный случай этой проблемы остаётся неразрешим, я считаю, то есть автоматически строить доказательство для «fib1 = fib2» просто получив fib1 с fib2 (опять, в каком виде?) алгоритмически нельзя — можно перечислить все доказательства (считаем, что язык рекурсивно-перечислим), проверка доказательства занимает конечное время, так что _если_ утверждение истинно, то его автоматическое доказательство (чисто теоретически) займёт конечное время, проблема в том, что если оно ложно, то мы зависнем — такая штука не decidable, но semidecidable, что типично для автоматических пруверов (и вообще для процесса поиска доказательств), вообще в RE-complete находятся и проблема останова, Rice, Entscheidungsproblem, 10-ая проблема Гильберта и т.д.

quasimoto ★★★★
()
Последнее исправление: quasimoto (всего исправлений: 1)
Ответ на: комментарий от emulek

толку-то от этого «доказательства»?

Толк в том, что можно проверять программы на эквивалентность.

anonymous
()
Ответ на: комментарий от quasimoto

Но у нас всё равно нет чёрного ящика в который можно будет закидывать fib1 с fib2 (в каком виде вообще?) и за конечное время получать ответы «равны» или «не равны»

Конечно, есть. На основе кода программ fib1 и fib2 тривиально генерируется код программы isFib1Fib2NotEq, которая останавливается тогда и только тогда, когда fib1 и fib2 не эквивалентны.

Далее мы отдаем на вход алгоритму, решающему проблему останова, программу isFib1Fib2NotEq, результат работы которого и укажет на эквивалентность.

anonymous
()
Ответ на: комментарий от quasimoto

базовые Agda с Coq строго выразительней PA

В каком смысле? В «базовых» Agda с Coq разве есть что-то кроме чистой логики, которую дает изоморфизм Карри-Говарда?

anonymous
()
Ответ на: комментарий от quasimoto

То есть, например, ЛПП у нас полна и противоречива, т.к. строго слабее арифметики. Соответственно, для лямбда-исчисления с зависимыми типами проблема останова разрешима. Даже тривиально разрешима - как и для любой системы лямбда-куба _любая_ программа завершается :)

anonymous
()
Ответ на: комментарий от anonymous

и противоречива

непротиворечива офк

anonymous
()
Ответ на: комментарий от anonymous

isFib1Fib2NotEq

Покажи как её написать. Допустим

open import Data.Nat

fib₁-rec : ℕ → ℕ → ℕ → ℕ
fib₁-rec a b zero = a
fib₁-rec a b (suc n) = fib₁-rec b (a + b) n

fib₁ : ℕ → ℕ
fib₁ = fib₁-rec 0 1

fib₂ : ℕ → ℕ
fib₂ (suc (suc n)) = fib₂ (suc n) + fib₂ n
fib₂ n = n

Круговая рекурсия и по дереву. Нам нужно «тогда и только тогда», что-то такое

open import Relation.Nullary

fib₁-not-eq-1+fib₂ : ℕ → ℕ
fib₁-not-eq-1+fib₂ n with fib₁ n ≟ 1 + fib₂ n
... | yes _ = fib₁-not-eq-1+fib₂ (suc n)
... | no _ = n

не подойдёт — TC не умеет в такие случаи, то есть он видит программу про которую он не может сказать «она завершается», хотя, очевидно, fib₁ n != 1 + fib₂ n и эта функция явно завершается при каждом вызове.

Далее мы отдаем на вход алгоритму, решающему проблему останова

Проблема в том, что «решает» он её ценой отбрасывания программ которые на самом деле завершаются (ELEMENTARY < PR < R < RE — мы где-то между PR и R).

В каком смысле?

Аксиомы PA пишутся как определение индуктивного типа ℕ и прочие теоремы (индукция, например, доказывается) и далее любое выводимое в PA утверждение тоже доказывается.

В «базовых» Agda с Coq разве есть что-то кроме чистой логики, которую дает изоморфизм Карри-Говарда?

«Чистой логики»? :) Если проводить параллели, то там как минимум HOL, допустим. Ну и PA легко делается. Это ж MLTT, то есть если и не ZFC (явно выразительней PA), то http://en.wikipedia.org/wiki/Constructive_set_theory#Interpretability_in_type... (тоже).

quasimoto ★★★★
()
Ответ на: комментарий от quasimoto

Вообще ещё вопрос бывают ли независимые утверждения вида (forall x. f x = g x) и neg (forall x. f x = g x) === (ex x. f x != g x), а то тогда можно перечислить доказательства и опровержения, чередуя, получив за конечное время то или другое.

quasimoto ★★★★
()
Ответ на: комментарий от quasimoto

Покажи как её написать.

i = 1;
while (i++){
    if (fib1(i) != fib2(i)) break;
}

Проблема в том, что «решает» он её ценой отбрасывания программ которые на самом деле завершаются (ELEMENTARY < PR < R < RE — мы где-то между PR и R).

Ну если он так работает, то ничего не выйдет, да.

«Чистой логики»? :)

Подразумевается соответствующая логическая система. Понятно, что для разных систем типов она разная. Собственно, вопрос состоял в том, есть ли там по дефолту определения натуральных чисел и операций над ними? Если нету - то все, очевидно, разрешимо.

anonymous
()
Ответ на: комментарий от anonymous

Вот fib₁-not-eq-1+fib₂ это то же самое.

Вот нашлось:

http://www.cs.bham.ac.uk/~mhe/.talks/popl2012/ -> http://www.cs.bham.ac.uk/~mhe/agda/ -> http://www.cs.bham.ac.uk/~mhe/agda/RicesTheoremForTheUniverse.html

We show that a Martin-Lof universe `a la Russell satisfies the conclusion of Rice's Theorem: it has no non-trivial, decidable, extensional properties. We derive this as a corollary of more general topological facts in type theory, which don't rely on Brouwerian continuity axioms.

Ну если он так работает, то ничего не выйдет, да.

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

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

Ещё интересный вопрос — функция может быть тотальна «на самом деле», но отбрасываться TC, есть техника которая позволяет уговорить TC принять такую функцию — руками доказать что она завершается (уменьшаться будет не основной аргумент, а доказательство). Для всякой ли программы которая тотальна «на самом деле» и пишется в языке существует такое доказательство в языке?

Собственно, вопрос состоял в том, есть ли там по дефолту определения натуральных чисел и операций над ними?

Есть, конечно. http://www.csie.ntu.edu.tw/~b94087/ITT.pdf — тут про натуральные числа ближе к концу.

quasimoto ★★★★
()
Последнее исправление: quasimoto (всего исправлений: 1)
Ответ на: комментарий от quasimoto

Для всякой ли программы которая тотальна «на самом деле» и пишется в языке существует такое доказательство в языке?

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

Есть, конечно. http://www.csie.ntu.edu.tw/~b94087/ITT.pdf — тут про натуральные числа ближе к концу.

Ну тогда ясно, выразительнее PA.

anonymous
()
Ответ на: комментарий от emulek

«Множества рациональных, целых и действительных чисел — не кольца»

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

kaathewise
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.