LINUX.ORG.RU

Является ли логика первого порядка Тьюринг-полной?

 , , , ,


0

1

Является ли логика первого порядка Тьюринг-полной? Можно ли описать brainfuck на логике первого порядка?

★★★★★

Последнее исправление: SZT (всего исправлений: 1)

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

Зачем? Он ведь со мной согласен. Ты просто не понимаешь ни формулировки теоремы, ни ее доказательства. Иди почитай учебник по формальным системам и перестань быть дебилом.

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

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

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

Он не утверждал обратное. Не надо выдумывать за Геделя, он бы откусил свой язык, если бы тот произнес сказанный тобой бред.

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

Последнее, в отличии от первого, не является парадоксом, не приводит к проитворечия.

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

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

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

Только игра в слова может изменить суть

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

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

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

Открой учебник и прочитай его. Внимательно. Тогда следующий раз ты так не обосрешься.

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

Да и вообще поменьше пытайся строить из себя того, кем не являешься. Ведь всегда можно нарваться на человека, который, в отличии от тебя, разбирается в предмете рассуждения. И тогда тебя ждет неминуемое перемешивание с говном.

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

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

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

ладно гуру, может я чего то не понимаю. Объясни простым языком, какк если бы объяснял ребенку. Вот есть у меня парадокс лжеца. Чтобы он перестал быть парадоксом, и система превратилась из противоречивой в неполную, я просто должен объявить данное утверждение невыводимым, так?

Ну, допустим, у меня машина не работает, не заводится. Я говорю, абра-кадабра, моя машина заводится, просто моя система неполна. Что от этого изменилось? Какая разница, что я говорю об этой системе, что от этого машина тронется?

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

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

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

смешно ты рассуждаешь. Я представляю такую картину. Ты стоишь возле МТ и орешь на нее: «останавливайся уже, есть ведь аксиома индукции»

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

Вот есть у меня парадокс лжеца. Чтобы он перестал быть парадоксом, и система превратилась из противоречивой в неполную, я просто должен объявить данное утверждение невыводимым, так?

Из парадокса лжеца (и любого подобного парадокса, вообще говоря) можно сделать некое другое утвержедние, которое парадоксом уже являться не будет. В случае с парадоксом лжеца это особенно просто, надо лишь «х = ложно(х)» поменять на «х = невыводимо(х)». При этом парадокс снимается т.к. утверждение может спокойно быть невыводимым, но при этом истинным в стандартной интерпретации (одновременно же ложным и истинным оно быть не может). С другой стороны, это утверждение не может быть невыводимым (т.к. в силу семантической полноты оно тогда будет ложным на всех интерпретациях, в том числе на стандартной, а поскольку его стандартаня интерпретация - невыводимость, то отрицание будет выводимость => противоречие). В результате мы записали утверждение которое невыводимо, но истинно (а значит его отрицание - тоже невыводимо).

Дальше вопрос состоит в том, чтобы записать такое утверждение, т.к. самореференций в лпп нет, формальное «x = невыводимо(х)» мы записать не можем. Это делается через спец. костыль - теория погружается сама в себя (именно оттуда требование для теории быть «достаточно сложной» - если теория не достаточно сложна, она не сможет сама себя описать).

а парадокса лжеца в лтт нет, потмоу что он просто не пишется. То есть «x = невыводимо(х)» пишется (пусть и с костылями) а «x = ложно(х)» - ну ваще никак.

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

Что от этого изменилось? Какая разница, что я говорю об этой системе, что от этого машина тронется?

Правильно. На неполноту совершенно плевать, на самом деле это даже полезное свойство (если бы сложные лтт были полны, они бы поетряли корректность).

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

Это вещи являются ключевыми, это основная антитеза.

Нету там в теореме никакой антитезы. Не делай вид, что ты ее читал.

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

это утверждение не может быть невыводимым

не может быть выводимым офк селффикс

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

Ну, это собственно, то о чем я и говорю. Чтобы из противоречивой системы сделать неполную, мы просто выдираем из нее противоречия руками. Протеворечивые утверждения мы просто объявляем невыводимыми, вот и все.

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

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

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

Протеворечивые утверждения мы просто объявляем невыводимыми, вот и все.

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

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

Кстати, похоже, все аксиомы, фактически, являются примерами невыводимых и истинных в стандартной интерпретации утверждений.

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

они бы ломали теорию, вне зависимости от их выводимости

Да нет же. Именно их (потенциальная) выводимость и ломает теорию(логическую систему), поскольку выводимость таких утверждений ведет к противоречию.

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

Кстати, похоже, все аксиомы, фактически, являются примерами невыводимых и истинных в стандартной интерпретации утверждений.

Ну естественно. Если аксиома независима от других, конечно.

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

Да нет же. Именно их (потенциальная) выводимость и ломает теорию

Теорию ломает само их _наличие_. Тот факт что можно их записать. Если бы можно было парадокс лжеца записать в тпп - это бы сразу ее ломало. И плевать выводим он или нет. В этом суть парадокса - теорию ломает его наличие.

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

Я о полноте. Вопрос ТС об описании - по сути, лишь следствие некоторой фривольности в обращении с языком.
Про FOL давно известно, что нет там полноты.

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

Ну, вот допустим берем наивную теорию множеств. Жила себе жила теория, пока в ней не нашли противоречие Рассела. Значит ли это, что теория не работала? Она работала. Проблема была в том, что она позволяля сформулировать в ней понятие «множество всех множеств не содержащее само себя». Из того, что система позволяет такое, мы делаем вывод, что она противоречива. Далее мы можем ввести аксиому, которая ограничивает теорию в подобных утверждениях. Система снова *считается* непротиворечивой. Как доказать, в общем случае, что она не содержит в себе еще парадоксы? На чем основано наше утверждение, что она непротиворечива? Тот факт, что мы не нашли противоречий до сей поры не означает что их нет, не так ли?

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

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

Но это ладно. Дальше что? Где условие останова машины? С чего ты взял, что вычисление остановится? Это у тебя описание или реализация? Если это просто описание, то оно не дает никакого вычислительного профита, а если это реализация, то это будет бесконечный луп, где на каждом шаге определяется новое число.

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

Иными словами, например, я могу утверждать, что где то во вселенной есть слон. Допустим, ты не видел слона, и отрицаешь его существование. Тогда у тебя есть конкретный механизм вычисления. Ты идешь по планете, и рано или поздно натыкаешься на слона, твой поиск останавливается. Знаем ли мы, что данный алгоритм остановится в общем случае? Нет. Применив этот «общий механизм» к произвольному X(вместо слона) мы не знаем, остановится ли когда либо поиск, поскольку не знаем существует ли X. А если мы это знаем, то нам и искать ничего не надо. Вот это и есть принципиальное отличие описания и исполнения. У алгоритма существует не только описание, но и реализация. Твоя логика может быть реализована, только описание реализации этой логики это не то же самое, что сама логика.

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

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

Реализация вот тут https://alt-ergo.ocamlpro.com/try.php

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

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

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

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

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

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

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

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

На МТ ты можешь написать эмулятор любого возможного ЯП со всеми этими конкурентностями и прочим.

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

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

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

Страница 72. Цитирую:

By the Computational Representation Theorem, computations of effective Actor systems on integers are enumerable by a Turing machine. Consequently, every deterministic computable function on integers can be implemented by a Turing machine.

В твоей ПДФ-ке скорее всего идет речь о каком-то сферическом коне в вакууме, который существовать в реальном мире не может. Ну примерно как всякие сверхтьюринговые вычисления, машина Зенона например.

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

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

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

Это значит что этот алгоритм вообще нельзя реализовать никаким способом. Ну хотя конечно есть шанс, что ученые откроят какие-то новые законы физики, которые позволят делать эти сверхтьюринговые вычисления, только я пока предпочитаю считать истинным https://ru.wikipedia.org/wiki/Тезис_Чёрча_—_Тьюринга_—_Дойча

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

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

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

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

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

А что собственно доказывается там на странице стр 40? Что «Смотрите, мы построили некую гипотетическую теоретическую модель вычислений на акторах, нереализуемую на реальных вычислительных устройствах, которая оказывается еще и нереализуема на МТ»? Какой от этого вообще толк? Столько же толку и от какой-нибудь машины Зенона.

Пойду лучше аксиомы допишу для брейнфака на alt-ergo

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

с чего ты взял, что она не реализуема на реальных устройствах? Она давно реализована в реальных устройствах, но на МТ не реализуема.

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

И где можно посмотреть реализацию? Ну вот предположим что это реализовали на x86-64 архитектуре используя Haskell или еще что-то вроде этого. И что мне мешает сделать эмулятор x86-64 на брейнфаке и запустить там собранный через GHC бинарник, который реализует эту модель вычислений?

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

да ты не читал нифига текст. Это алгоритм, который возвращает неопределенное число в диапазоне от 1 до бесконечности. Обычный random это реализует. Есть реализация рандома? Только не псевдо, а настоящего?

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

Это алгоритм, который возвращает неопределенное число в диапазоне от 1 до бесконечности. Обычный random это реализует.

Нет, это нереализуемо вообще никак. Матожидание такого рандома будет равно бесконечности, а бесконечности не существует вообще (нельзя вывести бесконечное число за конечное время. Да и за бесконечное тоже нельзя). За конечное время ты никогда не выведешь число от 1 до бесконечности

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

бесконечности не существует вообще

да что ты говоришь. Тогда и МТ не существует, там бесконечная память.

Ладно, отстань от этой реальности. Даже если рассматривать только модели, МТ не может реализовать подобный алгоритм:

Step 1: Either print 1 on the next square of tape or execute Step 3.
Step 2: Execute Step 1.
Step 3: Halt.

According to the definition of Nondeterministic Turing Machines, the above machine might never halt.

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

Матожидание такого рандома будет равно бесконечности

Кстати, тут ты тоже не прав. Матожидание будет <бесконечности, диапазон возможных значений от нуля до <бесконечности (бесконечность не включена).

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

да что ты говоришь. Тогда и МТ не существует, там бесконечная память.
да что ты говоришь. Тогда и МТ не существует, там бесконечная память.

Ну насчет МТ у меня еще есть сомнения, может там физики откроют какие-то законы физики, которые позволяют получить квантовую ерунду c бесконечной памятью, логически эквивалентную МТ(еще непонятно, можно ли проквантовать пространство). А вот про то чтобы получить случайное число от 1 до бесконечности - у меня нет никаких сомнений, что это невозможно вообще никак, даже чисто исходя из теории вероятности. Вот смотри, если ты возвращаешь целое число от 1 до 2 то вероятность каждого исхода у тебя 1/2 или 50% т.к. возможных возвращаемых значений 2. Если возвращать число от 1 до 5 то соотвественно у тебя будет уже 1/5 и 20%. А если ты возвращаешь случайное число от 1 до бесконечности, то вероятность что оно вернет любое конечное число равно 1/∞ что вообще говоря равно 0 и 0% вероятности получить какое-либо число от такого алгоритма.

Даже если рассматривать только модели, МТ не может реализовать подобный алгоритм:

Да ладно, вот я на Си реализовал, неужели МТ не справится?

#include <sys/types.h>
#include <sys/stat.h>
#include <fcntl.h>

#include <stdio.h>

int main(void)
{
  int randomData = open("/dev/random", O_RDONLY);
  unsigned char randchar;
  unsigned char tape[10000] = {};
  unsigned int tape_pos = 0; 
  
step1:  // Either print 1 on the next square of tape or execute Step 3.
  read(randomData,&randchar,1);
  randchar = randchar % 2;
  if(randchar) goto step3;
  printf("write to tape position %u\n", tape_pos);
  tape[tape_pos] = 1;
  tape_pos++;
  
step2: // Execute Step 1.
  goto step1;
  
step3: // Halt.
  printf("Halt.\n");
  return 0;
}

According to the definition of Nondeterministic Turing Machines, the above machine might never halt.

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

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