Конструктивно эффективные алгоритмы без эффективной корректности и доказательства эффективности

Я ищу естественные примеры эффективных алгоритмов (т.е. в полиномиальном времени)

их правильность и эффективность могут быть доказаны конструктивно (например, в $PRA$ или ), но $HA$
не известно никаких доказательств, использующих только эффективные концепции (то есть мы не знаем, как доказать их правильность и эффективность в или ). $TV^0$ $S^1_2$

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

cc.complexity-theory reference-request lo.logic proof-complexity constructive-mathematics Кава
источник

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

Андрей Бауэр

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

S_{2}^{1}

$S^1_2$

Андрей Бауэр

@Neel, на самом деле тезис Эмиля « Принцип слабой ямы и рандомизированные вычисления » о формализации вероятностных алгоритмов. Основной аксиомой, необходимой для формализации некоторых из них, является приблизительный подсчет, который не является частью

или

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

T V^{0}

$TV^0$

S_{2}^{1}

$S^1_2$

T V^{0}

$TV^0$

S_{2}^{1}

$S^1_2$

Каве

ps: было бы более интересно, если бы мы могли доказать, что правильность / эффективность алгоритмов не доказуема в этих теориях или, по крайней мере, эквивалентна утверждениям, которые, как полагают, недоказуемы в них. Однако просить об этом, вероятно, слишком много с тем, что мы знаем в настоящее время.

Каве

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

Франсуа Г. Дорайс

Ответы:

Это та же идея, что и в ответе Андрея, но с более подробной информацией.

Крайчек и Пудлак [ LNCS 960, 1995, с. 210-220 ] показали, что если является -свойством, определяющим простые числа в стандартной модели, и $P(x)$ $\Sigma^b_1$

S_{2}^{1} ⊢ \neg п (Икс) \to (\exists Y_{1}, Y_{2}) (1 < Y_{1}, Y_{2} < Икс \land Икс знак равно Y_{1} Y_{2})

$S^1_2 \vdash \lnot P(x) \to (\exists y_1,y_2)(1 < y_1, y_2 < x \land x = y_1y_2)$ тогда есть полиномиальный алгоритм факторинга времени. Это дает множество примеров, поскольку любой алгоритм NP для тестирования простоты в основном дает такую формулу

. В частности, критерий простоты AKS дает такую формулу (при соответствующей переработке на языке

). В статье Крайчека и Пудлака приводятся дополнительные примеры такого рода, связанные с криптографией, но он предшествует AKS и связанным с ним достижениям на несколько лет.

Σ_{1}^{b}

$\Sigma^b_1$

S_{2}^{1}

$S^1_2$

Франсуа Г. Дорайс
источник

$\mathrm{TC}^0$ $\mathit{VTC}^0$

$\mathit{TV}^0$ $\mathit{VTC}^0$ $\mathrm{TC}^0$

$\left(\frac an\right)$

$p$ $\left(\frac ap\right)=1$ $a$ $p$

$S^1_2$

Другой класс примеров дают алгоритмы проверки на неприводимость и факторизации для полиномов (прежде всего над конечными полями и над рациональными числами). Они неизменно опираются на небольшую теорему Ферма или ее обобщения (среди прочих) и, как таковые, как известно, не формализуемы в соответствующей теории ограниченной арифметики. Как правило, эти алгоритмы являются рандомизированными, но для детерминированных примеров за полиномиальное время можно взять критерий неприводимости Рабина или алгоритм квадратного корня Тонелли – Шанкса (сформулированный так, чтобы в качестве входных данных был необходим квадратичный нерезидент).

Эмиль Йержабек поддерживает Монику
источник

Тест на примитивность AKS кажется хорошим кандидатом, если верить Википедии.

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

Андрей Бауэр
источник

S_{2}^{1}

$S^1_2$

S_{2}^{1}

$S^1_2$

S_{2}^{1}

$S^1_2$

Крайчек и Пудлак опубликовали замечательную статью, в которой приводится еще несколько примеров: karlin.mff.cuni.cz/~krajicek/j-crypto.ps

Франсуа Г. Дорайс,

@ Франсуа, почему бы не опубликовать ответ? :)

Kaveh

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

Андрей Бауэр