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

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

Ок, и чему будет равна вероятность, что если я выберу совершенно любое конкретное конечное число, этот рандом вернет его?

И вот, кстати, что подумал, по поводу того, что не может твой декларативный исполнитель. Он не может время, он не может процесс растянутый во времени, где компоненты имеют состояние. Я уж не знаю, можно ли считать, что это может МТ, но в каком то смысле, если рассматривать его не как чистый блекбокс, наверное может, там есть запись и чтение.

вероятность >0, это все что можно сказать. И это не имеет отношения к вопросу.

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

Да, и такая вероятность существует, несмотря на то что она ничтожно мала уже на 10-м шаге. Однако как «логик» ты должен понимать, насколько значима разница между существует и не существует.

и не на step1, а зациклится между первым и вторым шагами, никогда не попадая на 3. Недетерминистский выбор делается на 1-м шаге в примере.

вероятность >0, это все что можно сказать.

Вероятность равна 0 т.к. множество чисел от 0 до бесконечности - бесконечно

Да, и такая вероятность существует, несмотря на то что она ничтожно мала уже на 10-м шаге.

При стремлении числа итераций МТ к бесконечности, вероятность останова стремится к 1.

Я не точно выразился. Имелось в виду от 0 до <бесконечности

Да, только это ничего не меняет

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

Да, я так и сказал, что оно всегда будет прыгать на step1 и таким образом зациклится. Заметь, я не уточнял, откуда оно будет прыгать в step1. Можно сказать что есть бесконечно малая вероятность, что МТ никогда не остановится

Нет, ты не понял. На первом шаге она делает выбор между 2-м и 3-м. То есть, если с первого шага всегда будет переход на второй, вычисление не остановится. А на первый можно попасть только из второго, без вариантов.

То есть правильно — на step2

Вероятность равна 0

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

Нет. Бесконечность это вообще не число. Количество чисел от 1 до бесконечности, не включая бесконечность (потому что бесконечность не число) — бесконечно. Ты с этим будешь спорить?

Вот смотри, мы можем проиллюстрировать это на той же МТ, взяв тот же самый алгоритм. Мы знаем, что МТ либо остановится либо нет(второе эквивалентно бесконечности), значит есть вероятность что остановится. Допустим, ты выбрал цифру один. Если есть вероятность остановки на 1, значит вероятность твоего угадывания не нулевая. Если нет такой вероятности, докажи это. Очевидно, что она есть, значит вероятность >0

Это можно даже строго доказать. Существуют вероятности неостанова и останова на каком либо числе, при этом не существует такого числа, вероятность останова на котором равна 0

Для всех x в астрале, для всех y в астрале... Это и есть ваша савиршеная и илигантная математика? Так даже пхпшники не пишут.

Про FOL давно известно, что нет там полноты.

Еще один. FOL (чистая) полна, причем как семантически так и синтаксически. Абсолютно все тпп - полны семантически. Достаточно сложные тпп - неполны синтаксически (при этом все более простые - полны).

А, так ты тот самый безграмотный долбоеб фанат безграмотного долбоеба Хьюитта. Че ж сразу не сказал? Я б не стал на тебя время тратить.

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

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

когда завершается _хотя бы одна ветка исполнения

там важно не «когда» а «если». Ты опять ННП. Разжевывать не буду, уже тысячи раз все разжевано

там важно не «когда» а «если».

Нету никакого «если». Она всегда завершается. Без «если». В любом случае. Варианта в котором она виснет - не существует.

Еще один промежуточный результат: https://paste.debian.net/hidden/4ad2d54d/

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

https://paste.debian.net/hidden/62b5b56b/ — это я на Си сам написал интерпретатор брейнфака, чтоб как следует во всем разобраться. Это все вполне можно переписать в этом функциональном alt-ergo стиле.

https://github.com/OCamlPro/alt-ergo/blob/master/doc/alt-ergo.1#L70 тут пишут про некую «theory of polymorphic records». Это нечто вроде struct в Си? Или это скорее union? Я конечно могу затолкать все состояние брейнфак-машины в один инт, но это будет уж очень неудобно.

Можно попробовать использовать why3 и протестировать на других SMT-солверах. http://why3.lri.fr/#documentation
Кроме того, этот why3 может «взаимодействовать» с coq, только с самим coq у меня нет опыта общения. Если посмотреть на синтаксис этого why3 http://why3.lri.fr/stdlib-0.87.0/ то он очень близок к alt-ergo.

Машина Тьюринга на Прологе:

turing(Tape0, Tape) :-
    perform(q0, [], Ls, Tape0, Rs),
    reverse(Ls, Ls1),
    append(Ls1, Rs, Tape).

perform(qf, Ls, Ls, Rs, Rs) :- !.
perform(Q0, Ls0, Ls, Rs0, Rs) :-
    symbol(Rs0, Sym, RsRest),
    once(rule(Q0, Sym, Q1, NewSym, Action)),
    action(Action, Ls0, Ls1, [NewSym|RsRest], Rs1),
    perform(Q1, Ls1, Ls, Rs1, Rs).

symbol([], b, []).
symbol([Sym|Rs], Sym, Rs).

action(left, Ls0, Ls, Rs0, Rs) :- left(Ls0, Ls, Rs0, Rs).
action(stay, Ls, Ls, Rs, Rs).
action(right, Ls0, [Sym|Ls0], [Sym|Rs], Rs).

left([], [], Rs0, [b|Rs0]).
left([L|Ls], Ls, Rs, [L|Rs]).

А в прологе аксиомы есть? Сам по себе пролог может доказывать некие теоремы сформулированные относительно состояния этой самой МТ?

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

в чем заключается невыразимость логики второго и более высших порядков в логике первого порядка(ЛПП)

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

если очевидно что в ЛПП выразима машина Тьюринга

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

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

Пока что все идет к тому, что можно (ну т.е. я не вижу такого места в этом интерпретаторе брейнфака, которое я б принципиально не мог описать всем тем, что доступно в этой ЛПП). И я выражу, надеюсь что сделаю это в ближайшую неделю. Просто очень непривычный для меня стиль программирования, я с этой функциональщиной не сталкивался практически. Я изучил то, что из себя представляет этот язык описания для SMT-солвера от alt-ergo, и вижу что он позволяет выразить брейнфак, а следовательно и МТ тоже можно выразить. И сам язык SMT-солвера alt-ergo это по-сути логика первого порядка

Alt-Ergo's native input language is a polymorphic first-order logic «à la ML» modulo theories.

Пока что все идет к тому, что можно (ну т.е. я не вижу такого места в этом интерпретаторе брейнфака, которое я б принципиально не мог описать всем тем, что доступно в этой ЛПП).

Потому что это НЕ интерпретатор брейнфака. Оно же там ты говорил компилируется в coq? Вот попытайся написать интерпретатор брейнфака, который сумеет скомпилироваться в coq, у тебя не выйдет (потому что в coq нельзя написать зависающую ф-ю, а интерпретатор брейнфака может повиснуть.

Я изучил то, что из себя представляет этот язык описания для SMT-солвера от alt-ergo, и вижу что он позволяет выразить брейнфак

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

Не знаю что там конкретно с Coq, но SMT солвер, если я ему опишу полностью математическую модель этой самой машины Тьюринга(брейнфака), сможет делать посредством нее Тьюринг-полные вычисления, при условии что в SMT солвер не было искусственно введено некое ограничение на глубину анализа. Т.е. если я задам некое сосотяние брейнфак-машины («программу» из > < + - . , [ ]) и попрошу SMT солвер доказать, что брейнфак-машина с такой начальной лентой завершится, то SMT солвер может (и скорее всего будет) пытаться доказать завершаемости этой самой брейнфак-машины путем ее непосредственной интерпретации(как интерпретатор брейнфака), т.е. Тьюринг-полнота тут есть определенно.

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

но при этом ZFC как тпп не является тьюринг-полной (при условии своей непротиворечивости).

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

Не знаю что там конкретно с Coq, но SMT солвер, если я ему опишу полностью математическую модель этой самой машины Тьюринга(брейнфака), сможет делать посредством нее Тьюринг-полные вычисления, при условии что в SMT солвер не было искусственно введено некое ограничение на глубину анализа. Т.е. если я задам некое сосотяние брейнфак-машины («программу» из > < + - . , [ ]) и попрошу SMT солвер доказать, что брейнфак-машина с такой начальной лентой завершится, то SMT солвер может (и скорее всего будет) пытаться доказать завершаемости этой самой брейнфак-машины путем ее непосредственной интерпретации(как интерпретатор брейнфака), т.е. Тьюринг-полнота тут есть определенно.

Где она тут есть? Еще раз - все описанное элементарно делается (и уже проделано) в ZFC - то есть дано описание МТ и дано описание процесса ее вычисления. Но при этом логика ZFC не является тьюринг-полной.

А если я и в Coq могу заложить такую стратегию доказательства, и сформулирую теорему о завершимости некоей МТ то и Coq будет пытаться доказать завершаемость МТ путем ее непосредственной интерпретации(как интерпретатор брейнфака), и естественно при попытке такого доказательства может произойти зависание.

В том-то и дело, что не может. Чтобы написать ф-ю в coq, тебе надо доказать, что эта ф-я завершается (или, иначе - доказать утверждение, которое формулируется в виде типа этой ф-и в логике coq). Если ф-я виснет - то это значит, что соответствующее утверждение ложно. Если утверждение ложно - то и доказать его нельзя, а значит и нельзя написать нужную функцию (т.к. терм с данным типом сам по себе является доказательством, то есть нет доказательства => и терма не существует, а нельзя написать то, чего не существует).

Что означает «не является Тьюринг-полной» если я на ней могу выразить МТ?

Чтобы ответить на этом вопрос, надо сперва определить понятие тьюринг-полноты для логических теорий. Изначально оно определено для вычислительных систем, т.о. надо иметь способ сделать из логической теории - вычислительную систему. На данный момент известен лишь один общепринятый способ подобного преобразования - это изоморфизм Карри-Говарда. То есть «не является тьюринг-полной» значит, что вычислительная система, которая согласно изоморфизму Карри-Говарда соответствует лпп - не является тьюринг-полной. В частности, для этой вычислительной системы невозможно написать зависающую программу.

Так почему тпп не является Тьюринг-полной несмотря на это?

Вся шутка в том, что:

выразить на этом «чем-либо» нечто Тьюринг-полное, и заставить это посчитать.

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

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