Так, я знаю тут есть люди задрочившие фундамент CS, знатоки языков, компиляторов, и просто хорошие математики. Кто-то даже сможет пояснить что хорошего дал миру Prolog, а то и применяет Haskell в продакшне.
Ребята, объясните же кто-нибудь ебучий THE HALTING PROBLEM. Я уже который раз сталкиваюсь и повсюду пруфы похожи на тупой копипаст. Типичный пруф выглядит высосанной из пальца хуитой, где доказывающий даже не пытается чего-то доказывать. Я понимаю, почему это неразрешимо для Тьюринг-машины которая оперирует бинарными данными, да ещё и в пределах одной ленты. Но где там принципиальная невозможность в фонНеймановской архитектуре? А если программе задать сложную структуру и оперировать даже не бинарными, а какими-нибудь многомерными символами? в смысле прикрутить семантику поглубже чем "а == 0xBlahblah"
Доходит до того что можно ведь спокойно написать поганый парсер который будет находить примитивные случаи залупленных кусков программы и указывать на каких входных диапазонах они проявляются. Что характерно, уже и JIT-компиляторы вполне могут тебе поянить что ты бесконечный цикл нахуярил.
Но открывая очередную книгу или очередное видео, я опять обнаруживаю людей которые дают сомнительный и куцый абстрактный разбор и тут же начинают скакать и визжать "НЕРАЗРЕШИМОСТЬ ДОКАЗАНА".
А если я в формальной грамматике определю второй слой токенов, которые будут как раз-таки указывать процедуры и их категории? И там среди прочих определить токен бесконечной залупленности. Это ж блять явно можно сделать для определённого класса программ и инпутов.
Таки поясните мне кто-нибудь пожалуйста где я идиот и почему надо слепо цитировать древнее доказательство.
>>1264468 Скорее всего, в пизде. Без теоремы Пифагора половина математики невозможна.
>>1264475 Не думаю, что ты сразу понял, умнич. Если вообще понимаешь.
А доказательство простое. Следите за руками. NB: это псевдоязык
bool halts(func, input); Функция halts возвращает true если func(input) ретурнит что-то, и возвращает false если функция func(input) циклится. Так же иногда для простоты буду писать не halt(func, input) а halt(func(input))
А теперь медленно... Если halt(func, func) возвращает true, то мы в вечном цикле. Иначе возвращаем 42(не важно что возвращать);
halt(func, func) - возможная функция, так как input может быть и функцией.
А теперь внимание Что вернёт wtf(wtf)?
А нихуя она вернуть не сможет. Допустим halt(wtf(wtf)) -> true; Тогда wtf(wtf) зациклится и не вернёт 42. А какого хуя тогда halt(wtf(wtf)) вернул true? И наоборот. Допустим halt(wtf(wtf)) -> false; Тогда wtf(wtf) вернёт 42. Но мы же только что получили false? Что за хуйня?
Получается, у нас есть парадокс. Следовательно функция halts не возможна. И не возможна не только на машине Тьюринга, но и на любом вычислителе, будь он хоть абстрактный, хоть реальный. Это просто не помещается в логику. В этом и чудо доказательства Тьюринга.
Естественно, речь идёт что функция halts универсальна.
Если функция halts не на 100% определяет что функция func(input) циклится, а например возвращает false если находит while(true) без break, exit и return, то такой функции просто нельзя доверять. Если такая функция halts вернула true, то это ещё не значит что функция func(input) точно вернёт halt.
>>1264485 У нас парадокс, дебич не умеющий в програмирование пытается рассуждать о программировании. Следи за руками, клоун:
>bool halts(func, input); >Функция halts возвращает true если func(input) ретурнит что-то, и возвращает false если функция func(input) циклится. >... >Если halt(func, func) возвращает true, то мы в вечном цикле. Иначе возвращаем 42(не важно что возвращать);
Если halt(func, func) возвращает true, то мы заходим в цикл, попадаем на return и выходим из wtf со значением 2, выполняя тело цикла 1 раз.
>Что вернёт wtf(wtf)?
>halt(wtf(wtf)) -> true; Значит, что wtf(wtf) вернет 42,
>halt(wtf(wtf)) -> false Действительно wtf(wtf) ничего не возвращает и зациклилась, потому что внутренний вызов wtf(wyf) ничего не вернул.
>>1264457 (OP) А что конкретно тебе непонятно-то, анон? Давай ты возьмешь какое-нибудь стандартное доказательство и скопируешь его сюда с твоими пометками, где тебе что-то непонятно. У меня такое чувство, что у тебя просто нет навыка математического мышления, ты пытаешься "на пальцах", интуитивно понять формальные утверждения - и не понимаешь, потому что понимание требует навыка формального рассуждения. Поправь, если я не прав.
Сначала давай-ка уточним что мы вообще знаем о программах и их остановках.
Я говорю, что программа останавливается когда она запущена, в неё введены некоторые и данные и в какой-то момент после запуска её выполнение прекращается. Это может происходить в случаях:
h1. Программа слишком монструозная чтобы поместиться в памяти машины. Сюда же - количество переменных таково что не вместится ни в один реальный стак. h2. Конкретная переменная выходит за предоставленный ей диапазон памяти h3. Несовпадение типов данных h4. Банально настолько кривое написание программы что из-за нарушенной грамматики и написания операндов выполнение невозможно h5. Какая-либо функция входит в неопределённое состояние h6-1. Банальное завершение путём завершения всех операций h6-2. Банальное завершение за счёт выхода по условию h7. Программа завершается извне вне зависимости от стадии её исполнения
Предположим, что мы имеем дело с чем-то компилируемым и типизированным, поэтому отбрасываем h3 и h4, т.к. мы совершенно точно знаем что хороший компилятор не пропустит такое написание, да и вообще это уже не будет являться программой в выбранном языке. Случаи h1 и h2 отсекаются как раз за счёт абстрактного условия о Тьюринг-машине без ограничений на адресное пространство, реальный объём памяти и так далее. h5 можно отсечь дополнительным условием о том, что у нас де язык такой хороший что все функции там однозначно определены без всяких костылей.
Остаётся только два хороших, здоровых варианта: программа отработала своё дело (h6-1), либо была специально завершена в соответствии с выполненным условием (h6-2). И внешнее завершание (h7).
Когда программа не завершается?
l1. Банально цикл для которого входным условием является вечное true l2. Сложное ветвление, основанное на изменении переменных, однако цикл изменения переменных является замкнутым, в итоге цикл условий также становится бесконечным l3. Криво поставленный goto l4. Цикл составлен так, что вместо вычислений происходит тупое увеличение переменной-счётчика в итоге у нас просто расширяется пространство, выделенное на эту переменную, но реальных действий не происходит l5. Ожидается выполнение подпрограммы
Тут мы не можем ничего откинуть, т.к. оно уже полностью соответствует всем условиям, описанным выше.
Однако, я берусь утверждать, что программа, содержащая l1-4 является принципиально дегенеративной как алгоритм вообще: она не может сколько-нибудь адекватно работать без родительского процесса, который будет вовремя производить h7 по отношению к такой программе.
В идеале мы должны работать с программой, которая находится либо в состоянии l5, либо уже выполнять h6-1 или h6-2. И все её подпрограммы должны быть либо аналогичны ей самой, либо находиться в ветке основной программы в которой над ней есть условие h7 которое может выполняться вне зависимости от выполнения данной подпрограммы.
Для того чтобы построить такую валидацию у нас уже есть всё кроме однозначной системы, которая может проверять те самые циклы-подциклы-итд изменения переменных (в смысле растёт она или уменьшается). Но т.к. речь идёт об абстракции без ограничений и т.к. Тьюринг-машина всё равно основывается на бинарных данных, то мы по крайней мере в теории вполне можем сделать программу которая всё это проверяет. Нужно оно для в общем-то ленивых вычислений. Чтобы в нужный момент обнаруживался индукционный вывод и можно было завершать дегенеративный цикл по мере обнаружения. Очевидное: сравниваем две переменные, но одна из них постоянно растёт. На n-м шаге дальнейшая проверка будет бессмысленной т.к. значения растущей переменной перешли область схождения и никогда в неё не попадут.
Я утверждаю, что программа прошедшая такую валидацию является либо выполняющейся до конца или условного выхода, либо прекращающейся за счёт индукционного обнаружения бесконечного перебора после чего сама среда исполнения будет прекращать работу программы, либо завершаться извне вне зависимости от самой себя.
И там как пример ставится задача с Теоремой Ферма. Я утверждаю, что там алгоритм вполне себе вычисляющий и проходящий валидацию. Его вычисление может быть бесконечным только в случае реального отсутствия ответа для данного D. Однако это напрямую связано с тем, что алгоритм не предусматривает условия выхода не случай затянутых вычислений. Если же вводить ограничения, то мы можем даже посчитать сколько времени может занять наиболее долгое исполнение данной программы до завершения. В данном случае вопрос уже перекатывается в более философскую сторону: алгоритмы поиска результатов используются там где эти результаты либо явно есть, либо их явно нет. Но применяют-то только те алгоритмы, которые проходят теоретическое подтверждение со стороны в этом случае математического сообщества. За всю историю человеческой мысли и мысли математической никто не рассматривал перебор уходящий в бесконечность как адекватное решение. Все знают что такой перебор технически даёт ответ, но ни один математик в здравом уме не объявит это валидным решением самой проблемы. Поэтому, в данном случае вопрос завершении этой программы вообще не связан с алгоритмом который присутствует в самой программе.
Если же смотреть на это исключительно как на построение текста в рамках некого формального языка и семантики данного текста, то ответ уровня «оно вычислится, если среди области данных существует подходящее значение» - это уже достаточный финитный ответ на насчёт алгоритма. Программа завершается в зависимости от того что не связанно ни с ней самой, ни с инпутом.
Это всё означает, что H-машина должна давать на выходе не yes/no, а что-то вроде: o1. Введённая программа входит в залупленность из-за дегенеративности её алгоритма o2. Введённая программа завершается только если некая другая программа при том же инпуте даёт на выходе true o3. Введённая программа всегда завершается
А теперь погляди чего там предлагают дальше рассматривать как решение: - никакого разделения по видам бесконечных циклов - никаких валидаций - манипулирование рекурсивным инпутом, которое явно исходит из оригинального текста Тьюринга где манипуляция идёт сугубо бинарными данными. Попробуй представить самоподобную программу в современном языке. Там либо не будет такой проблемы вообще (при нормальном написании кода), либо мы должны сразу понимать что даём не программу а бинарный рандом созданный на её основе.
Итоговый пруф? Итоговый пруф представляет собой построение на основе l1. Где там происходит желаемый логический парадокс я просто не вижу: у нас происходит опять же дегенеративная рекурсия чьё построение ещё и не определено средой исполнения. А вот при определении того что делать с этим самым рекурсивным вызовом мы совершенно однозначно получаем тот или иной ответ у OOP(OOP).
И мне предлагают проглотить это дырявое построение и на основе это вдруг сказать что у нас HALTS вообще не может существовать.
В конечном итоге я просто не вижу вменяемости в предлагаемом мне пруфе.
Сам концепт неразрешимости - нормальная штука. А вот то за счёт чего мне его пытаются подать - с виду уж точно нет.
В особо удачных случаях проблему пытаются иллюстрировать за счёт парадокса брадобрея, который является прямо клиническим случаем хуёвого определения задачи в условиях такой же хуёво определённой "среды исполнения" - теории множеств.
>>1264870 Ну например моя программа делит на два если четное, и делает ×3+1 если нет и завершается если на очередной итерации получается 1. Она что, дегенеративная?
>>1264870 > расширяется пространство, выделенное на эту переменную > выдуманный термин "дегенеративность" мамка твоя дегенеративная > Программа завершается извне > Ожидается выполнение подпрограммы
На каждой ветке имеет очевидно вычислимое выражение. На входе в условие - тоже вычислимая штука.
Далее пусть себе выполняется вплоть до того пока вдруг каким-то неведомым образом не зайдёт на повторный круг (который должен отлавливаться самим алгоритмом).
Ты как раз таки привёл, и ты даже знаешь откуда привёл, тот самый случай когда есть эмпирическая перечислялка, которая по сути находится в тени от реальных математических явлений, которые задают подобное поведение.
>>1264982 > Это полный в общем-то синоним к слову "вырожденный". Давай калькированием не будем заниматься, а всё-таки постараемся на русском языке разговаривать, иначе мы друг друга просто не поймём.
> Если программа существует в вакууме, то это не имеет отношения к Computer Science и формальным грамматикам даже. Как раз таки только этот случай, как правило, и рассматривается. Абстрагирование - слышал про такой мыслителный приём?
>>расширяется пространство, выделенное на эту переменную >Так, а вот тут давай-ка ты с высоты своего явно птичьего полёта возьмёшь и пояснишь чего тебе не понравилось в такой-то банальщине. Объясни мне, глупому, каким именно образом в этом примере https://godbolt.org/z/hxmEbo"расширяется пространство, выделенное на эту переменную" i, а именно регистр rbx. Меня именно механика этого "расширения пространства" интересует.
>>1264457 (OP) Ещё раз, давай пойдём от противного: предположим, ты написал функцию, которая принимает на вход другую функцию, даже хуй с ним, ты наверняка про лисп не слышал никогда, судя по твоим рассуждениям, пусть она принимает на вход текст другой функции и аргументы, с которыми эта другая функция вызывается, и возвращает в ответ true, если эта другая функция не зацикливается, и false, если зацикливается. Теперь представь себе, что будет, если на вход этой функции подать её же саму, и включи на минуту голову. Если у тебя в ней есть хоть капля мозгов, всё, проблемы нет, тред можно закрывать. Вообще, почитай классику - SICP, "Гёдель, Эшер, Бах" Хофштадера и "Новый ум короля" Пенроуза, может, после хотя бы их прочтения перестанешь позориться на анонимных имиджбордах своей тупизной.
>>1264868 >Сначала давай-ка уточним что мы вообще знаем о программах и их остановках. Анон, извини, но ты дальше в посте занимаешься пустой болтологией (можешь назвать это "философией", бгг). Тебе нужно взять конкретный формализм (Машину Тьюринга, например) и провести формальное доказательство. Это делают на первом курсе в любом техническом вузе. Как я уже сказал, от школьных рассуждений "на пальцах" никакого толку нет. Просто возьми учебник по логике и вычислимости (того же Роджерса) или методичку любого вуза по теме и прочитай. Смысла тратить тут время на объяснения не вижу, потому что у тебя проблема именно в отсутствии понимания математических методов, а не этого конкретного доказательство, так что тред скрыл, извини. Удачи в самообразовании, анон.
>>1264457 (OP) Челик, халтинг работает даже блять на недетерминированный МТ с оракулом, что охуеть как круче, чем любые современные манякомпуктеры. Бтв, это док-во Тьюринга одно из красивейших доказательств в CS евер, на уровне теорем Геделя, вообще комбинаторщики тогда ебашили, не то что сейчас эх. Нужно быть рили довном чтоб его не понять, ну или читать жопой.
>>1265149 У меня одногруппник грил тип "а что если создать функцию, которая определяет холтинг для всего, кроме функций где она сама хоть в каком-то виде присутствует?"
>>1265087 Ты, дурачок, даже не спросил, что у этой функции будет при этом в качестве аргументов. Хорошо, делаем следующий шажок. Что будет, если эта волшебная функция (назовём её f), определяющая, зациклится её аргумент или нет, примет на вход некую другую функцию, скажем, f2, которая принимает на вход один аргумент и состоит из одной простой инструкции: вызвать f со своим аргументом и начать крутиться в бесконечном цикле, если она вернула true, и ничего не делать, если она вернула false?
>>1265149 >одно из красивейших доказательств в CS евер, на уровне теорем Геделя Меня это убило, когда изучал. >определяем хренову тучу дополнительных функций >хуяк-хуяк >ВНЕЗАПНО диагональная лемма >????? >ПРОФИТ Причём последние три пункта уместились на полутора страницах, кажется.
Ребята, объясните же кто-нибудь ебучий THE HALTING PROBLEM.
Я уже который раз сталкиваюсь и повсюду пруфы похожи на тупой копипаст. Типичный пруф выглядит высосанной из пальца хуитой, где доказывающий даже не пытается чего-то доказывать.
Я понимаю, почему это неразрешимо для Тьюринг-машины которая оперирует бинарными данными, да ещё и в пределах одной ленты. Но где там принципиальная невозможность в фонНеймановской архитектуре? А если программе задать сложную структуру и оперировать даже не бинарными, а какими-нибудь многомерными символами? в смысле прикрутить семантику поглубже чем "а == 0xBlahblah"
https://www.youtube.com/watch?v=cx1RaTsuB54
Доходит до того что можно ведь спокойно написать поганый парсер который будет находить примитивные случаи залупленных кусков программы и указывать на каких входных диапазонах они проявляются. Что характерно, уже и JIT-компиляторы вполне могут тебе поянить что ты бесконечный цикл нахуярил.
Но открывая очередную книгу или очередное видео, я опять обнаруживаю людей которые дают сомнительный и куцый абстрактный разбор и тут же начинают скакать и визжать "НЕРАЗРЕШИМОСТЬ ДОКАЗАНА".
А если я в формальной грамматике определю второй слой токенов, которые будут как раз-таки указывать процедуры и их категории? И там среди прочих определить токен бесконечной залупленности.
Это ж блять явно можно сделать для определённого класса программ и инпутов.
Таки поясните мне кто-нибудь пожалуйста где я идиот и почему надо слепо цитировать древнее доказательство.