LINUX.ORG.RU

Хмм, похоже что является. Определяем Аксиомы Пеано, но чтоб с 0 начиналось а не с 1. Вводим операцию «x + y», операцию «x - y», деления, умножения и остатка от деления определяем, потом операции битового логического сдвига влево и вправо - так можно сдвигами нарезать число от 0 до inf на бесконечный массив байтов по 8 бит каждый — получим ленту для brainfuck и возможность по ней ходить в любую сторону. А сама программа брейнфака, состоящая из 8 инструкций > < + - . , [ ] - делаем отдельный массив для этих инструкций по три бита на инструкцию. Ну а дальше определяем что вот эта инструкция делает такие-то изменения на ленте.

Только я тогда не совсем понимаю, что значит несводимость логики первого порядка к логике второго порядка? Если брейнфак выразим в логике первого порядка, то я могу скомпилить Coq в этот брейнфак — разве это не будет выражение логики одного порядка в логике другого порядка?

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

скачять реферат безплатно без смс

https://domashke.com/referati/referaty-po-matematike/kursovaya-rabota-nerazre...

3. Вывести неразрешимость логики первого порядка из неразрешимости проблемы остановки.

не уверен, что это то, что тебе нужно, а не обратный результат. в любом случае, см. google://$SUBJ

MyTrooName ★★★★★ ()
Последнее исправление: MyTrooName (всего исправлений: 1)
Ответ на: скачять реферат безплатно без смс от MyTrooName

3. Вывести неразрешимость логики первого порядка из неразрешимости проблемы остановки.

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

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

Только я тогда не совсем понимаю, что значит несводимость логики первого порядка к логике второго порядка?

Ни логика первого порядка, ни логика второго порядка не являются тьюринг-полными. При этом логика второго порядка шире логики первого (и, с-но, лпп не сводится к лвп).

разве это не будет выражение логики одного порядка в логике другого порядка?

Не будет.

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

Гёдель это доказал давно,

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

Зачем нужны вообще эти клоуны? Пусть живут себе в своем мире первых, 10-х и прочих порядков, нормальным посанам это не нада

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

Если руки все-таки дойдут — кастани :)

Пока покажу промежуточный результат. Я использовал нотацию от SMT-солвера alt-ergo https://paste.debian.net/hidden/ead1da5c/
Протестировать можно тут https://alt-ergo.ocamlpro.com/try.php только лучше поставить это через OPAM потому что так быстрее значительно. Не все те «юнит-тесты» завершаются успешно, но это обусловлено лишь исключительно тем, что солвер не может выбрать стратегию правильную и не пытается очень сильно «разворачивать» сдвиги. Там (если собрать себе этот alt-ergo на локалхост без жабаскриптов) есть возможность посмотреть то, каким образом доказывается верность утверждения

Немного о синтаксисе:

forall - квантор всеобщности. Есть еще квантор существования exists. Оператор -> — импликация. Есть встроенный тип int который принимает значения ... -4 -3 -2 -1 0 1 2 3 4 ... т.е. соответствует множеству целых чисел. Там уже есть встроенные операции умножения сложения деления и нахождения остатка от деления. Остальное должно быть самоочевидным.

через двоичные сдвиги я смогу нарезать инты большие чем или равные 0 на массив из 8-битных unsigned char. И еще нарезать для хранения самого «алфавита» брейнфака < > + - . , [ ]. В alt-ergo есть теория для массивов, но я массивы определю через неотрицательные инты, чтоб не возникало вопросов. Отдельным положительным интом будет хранится положение «указателя» на ленте с инструкциями, и еще одним - положение на ленте с ячейками памяти. Еще один инт будет нужен чтобы проматываться между скобочками [ ]. Далее, можно ввести понятия «шага» брейнфака, чтобы на каждом шаге инкрементировать некую переменную, и тогда можно будет попросить SMT солвер решить «а будет ли на таком-то шаге такое-то состояние у нашей брейнфак-машины?». Вообще это все очень напоминает какое-то функциональное программирование. Скоро доделаю

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

Далее, можно ввести понятия «шага» брейнфака, чтобы на каждом шаге инкрементировать некую переменную, и тогда можно будет попросить SMT солвер решить «а будет ли на таком-то шаге такое-то состояние у нашей брейнфак-машины?»

Ты же понимаешь, что умение вычислять МТ до некоторого конечного n, не ведет к полноте по тьюрингу?

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

Для n можно использовать квантор существования т.е. можно сформулировать это как «Существует такой шаг n на котором состояние м.т. при вот таком-то начальном состоянии ленты является таким-то»

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

Но это не дает тьюринг-полноты.

Дает.

вообще никакая непротиворечивая лт не может быть тьюринг-полной. Для тьюринг-полноты надо уметь зависать - то есть выводить nonsense.

А описанная в логике первого порядка машина тьюринга тоже будет уметь зависать.

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

Дает.

Не дает. На не тьюринг-полном ЯП можно написать ф-ю которая вычисляет любую мт до любого шага на любых данных.

А описанная в логике первого порядка машина тьюринга тоже будет уметь зависать.

Описать-то в лпп (точнее, в какой-нибудь в теории первого порядка, например ZFC) МТ можно легко - формальное определение МТ именно таким описанием и является. Это, однако, не делает указанную теорию (и лежащую в основе логику) тьюринг-полной.

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

Не дает. На не тьюринг-полном ЯП можно написать ф-ю которая вычисляет любую мт до любого шага на любых данных.

Если есть штука, которая будет нечто доказывать, пользуясь аксиомами, описанными логикой первого порядка, то она вполне может быть(может делать вычисления) полной по тьюрингу. Проблему останова можно тоже сформулировать, что вот при таком-то состоянии ленты МТ у нас никогда не будет выполнено условие останова(отрицание квантора существования https://ru.wikipedia.org/wiki/Квантор)

Это, однако, не делает указанную теорию (и лежащую в основе логику) тьюринг-полной.

А что делает?

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

что вот при таком-то состоянии ленты МТ у нас никогда не будет выполнено условие останова(отрицание квантора существования

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

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

что вот при таком-то состоянии ленты МТ у нас никогда не будет выполнено условие останова(отрицание квантора существования

да какая ошибка, если ты вообще не понимаешь о чем говоришь? Допустим есть алгоритма который «призван доказать или опровергнуть» утверждение о бесконечности натурального ряда. Алгоритм заключается в реализации индуктивного шага n-next = n + 1. Есть утверждение, что не существует такого n, что машина остановится. Докажем это, запустив нашу машину. Но машина не остановится, следовательно ничего никогда не будет доказано.

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

вообще никакая непротиворечивая лт не может быть тьюринг-полной. Для тьюринг-полноты надо уметь зависать - то есть выводить nonsense.

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

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

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

Да, есть. Но это доказывается не перебором до бесконечности, а напрямую следует из определения натурального числа и аксиомы индукции. Число 1 - натуральное. Любое число, следующее за натуральным - натуральное.

(Аксиома индукции.) Если какое-либо предложение доказано для 1 (база индукции) и если из допущения, что оно верно для натурального числа n, вытекает, что оно верно для следующего за n натурального числа (индукционное предположение), то это предложение верно для всех натуральных чисел.

Алгоритм заключается в реализации индуктивного шага n-next = n + 1.

Можно математически доказать, что этот алгоритм никогда не завершится т.к. любое натуральное число+1 это натуральное число

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

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

У тебя в голове каша.

А что делает?

Делает вычислительная эквивалентность МТ. Если твоя логика не может повиснуть (вывести противоречие), то она слабее МТ.

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

Вот тебе на alt-ergo

goal inf_proff:
  forall x : int.
  x >= 1 -> (* все натуральные числа больше либо равны 1 *) 
  (x+1 >= 1) (* всякое натуральное число, если к нему прибавить 1, будет натуральным *)

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

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

Вывод - это терм. Если терм повис - то тип содержит жопу. Жопа - это противоречивое утверждение. С-но, если МТ содержит виснущие термы, то тьюринг-полная логика, эквивалентная (в смысле изоморфизма Карри-Говарда) позволяет вывести ложное утверждение.

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

anonymous ()

Че то сейчас подумал, и вот что я скажу. Логика и вычислитель(в том числе МТ) вообще имеют разную природу. Принципиальное отличие заключается в том, что вычислитель задает правила вычисления, а логика сама является этим набором правил. Вычислитель вообще ничего не должен доказывать, он должен обеспечивать(если надо) соблюдение этих правил, и осуществление их. Причем, правила могут быть абсолютно любые, не обязательно логические. К примеру, мы можем реализовать вывод «если не А и не Б то С» какая тут логика? да никакой(хотя, формально это, типа импликация). Просто мы так захотели. Или нам так надо. Никакая логика не может не то что реализовать, но и описать данное вычисление, так как нет логических оснований для него.

Алсо, зыбкость логики феерично показал Льюис Керрол в «Черепахе и Аххилесе». Доказательство — это пустой звук, по большому счету. Просто отражение работы человеческого мышления, не более того. Самостоятельного значения она не имеет. Не случайно, до сих пор определение слова «доказательство» весьма туманно, если вообще существует:)

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

Если твоя логика не может повиснуть (вывести противоречие), то она слабее МТ.

А кто-то разве утверждал, что в логике порядка нельзя сформулировать невыводимую и неопровержимую формулу? https://ru.wikipedia.org/wiki/Теорема_Гёделя_о_неполноте

Первая теорема утверждает, что если формальная арифметика непротиворечива, то в ней существует невыводимая и неопровержимая формула.

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

Если терм повис

Кто будет делать вывод о его зависании? Нет этой сущности. Если МТ не закончила вычисление, значит она либо его закончит, либо нет. Что из этих 2 — никто не знает, на любом шаге вычисления. Поэтому нет никакого зависания.

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

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

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

1. Теорема Геделя не относится к лпп, она относится к теориям первого порядка (которые являются расширениями лпп). Сама лпп как раз является полной. И многие ее расширения (которые не являются достаточно сложными для погружения в себя) - тоже являются полными, например арифметика Пресбургера. Так что, да, в лпп не существует формулы, которая была бы не выводима в лпп вместе со своим отрицанием.

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

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

Кто будет делать вывод о его зависании?

Вывод о его зависании делать не надо. Это просто факт, терм повис, нормальной формы у него нет.

Что из этих 2 — никто не знает

Я знаю, потому что я это доказал. for(int i = 0; 1; i++); - зависает в соответствии с семантикой языка. Чтобы в этом убедиться, запускать программу не нужно.

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

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

Но мы легко можем превращать одно - в другое:

https://en.wikipedia.org/wiki/Curry–Howard_correspondence

по-этому на самом деле разницы нет.

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

Не случайно, до сих пор определение слова «доказательство» весьма туманно

Да нет, у этого слова четкое, формально строгое математическое определение. Это вполне конкретный математический объект, вполне определенного вида.

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

Отличной иллюстрацией теоремы Геделя является парадокс Лжеца (она и есть парадокс Лжеца, переведенный на язык математики). Пусть лжец говорит «я лгу» лжет ли он? Допустим лжет. Но он и утверждает, что он лжет. значит он говорит правду. Но если он говорит правду — то он не лжец.

Имхо, решение этого парадокса тривиально. Такая фраза из уст лжеца попросту невозможна по-определению, так же как невозможно существование Расселовского множества. Эти хреноплеты просто перемудрили сами себя, не более того. Можно породить кучу пародоксов на пустом месте. Например, «прыгающий хохол не прыгает» Если он прыгающий, как же он может не прыгать? А если он прыгает, значит он не прыгающий. Парадокс!

На самом деле все эти логические изыскания кажутся обывателю такими сложными из-за того, что их авторы немножко с глупинкой, не более того:) На этом вся логика и математика и стоит:)

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

Но мы легко можем превращать одно - в другое:

Я уже привел пример, где мы не можем превратить одно в другое. Если бы мы могли превращать одно в другое всегда — другое дело.

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

Отличной иллюстрацией теоремы Геделя является парадокс Лжеца (она и есть парадокс Лжеца, переведенный на язык математики).

Не является. Не есть. Невыводимая с отрицанием формула у Геделя это не «данное утверждение ложно» а «данное утверждение невыводимо». Последнее, в отличии от первого, не является парадоксом, не приводит к проитворечия.

На самом деле все эти логические изыскания кажутся обывателю такими сложными

Так ты и есть обыватель. И ты этих рассуждений не понимаешь. Но смеешь мнение иметь.

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

логично?

Что?

Ты вроде утеверждал, что существует общепринятое четкое определение.

И я тебе его дал. Общепринятое, формально строгое математическое определение.

anonymous ()