Konstruktywnie wydajne algorytmy bez sprawdzania poprawności i wydajności

Szukam naturalnych przykładów wydajnych algorytmów (tj. W czasie wielomianowym) ul

ich poprawność i skuteczność można konstruktywnie udowodnić (np. w lub ), ale $PRA$ $HA$
nie jest znany żaden dowód wykorzystujący tylko wydajne koncepcje (tzn. nie wiemy, jak udowodnić ich poprawność i wydajność w lub ). $TV^0$ $S^1_2$

Mogę samodzielnie tworzyć sztuczne przykłady. Chcę jednak ciekawych naturalnych przykładów, tj. Algorytmów opracowanych dla nich samych, nie stworzonych tylko po to, aby odpowiedzieć na tego rodzaju pytania.

cc.complexity-theory reference-request lo.logic proof-complexity constructive-mathematics Kaveh
źródło

Być może coś z teorii automatów, gdzie algorytm jest łatwy, ale aby pokazać, że działa, należy wziąć pod uwagę wszystkie podzbiory tego czy innego?

Andrej Bauer,

Co powiesz na sprawdzanie pierwotności w czasie wielomianowym? Ten dowód może być na tyle skomplikowany, że trudno będzie go wsadzić do

S_{2}^{1}

$S^1_2$

Andrej Bauer,

@Neel, w rzeczywistości teza Emila „ Słaba zasada szuflady i obliczenia losowe ” dotyczy sformalizowania algorytmów probabilistycznych. Głównym aksjomatem potrzebnym do sformalizowania niektórych z nich wydaje się przybliżone zliczanie, które nie jest częścią

lub

. Myślę, że łatwiej byłoby trzymać się deterministycznego przypadku polytime z

T V^{0}

$TV^0$

S_{2}^{1}

$S^1_2$

T V^{0}

$TV^0$

S_{2}^{1}

$S^1_2$

Kaveh

ps: Byłoby bardziej interesujące, gdybyśmy mogli udowodnić, że poprawność / wydajność algorytmów nie jest możliwa do udowodnienia w tych teoriach, lub przynajmniej są równoważne stwierdzeniom, które uważa się w nich za nie do udowodnienia. Jednak prośba o to prawdopodobnie za dużo w stosunku do tego, co wiemy obecnie.

Kaveh

@Neel, większość odpowiedniego prawdopodobieństwa można zrobić w systemach pierwszego rzędu, ponieważ tak naprawdę nigdy nie trzeba znać dokładnego prawdopodobieństwa zdarzenia, zwykle wystarczy porównać to prawdopodobieństwo z pewnymi liczbami wymiernymi.

François G. Dorais

Odpowiedzi:

Jest to ten sam pomysł, co odpowiedź Andreja, ale zawiera więcej szczegółów.

Krajicek i Pudlak [ LNCS 960, 1995, ss. 210–220 ] wykazali, że jeśli jest właściwością która definiuje liczby pierwsze w modelu standardowym, a $P(x)$ $\Sigma^b_1$

{S.}_{2)}^{1} ⊢ \neg P. (x) \to (\exists y_{1}, y_{2)}) (1 < y_{1}, y_{2)} < x \land x = 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)$ istnieje algorytm faktorowania wielomianowego. Daje to wiele przykładów, ponieważ dowolny algorytm NP do testowania pierwotności daje w zasadzie taką formułę

. W szczególności test pierwotności AKS daje taką formułę (przy odpowiednim przekształceniu w języku

). Artykuł Krajicka i Pudlaka podaje więcej tego rodzaju przykładów związanych z kryptografią, ale wyprzedza AKS i powiązane postępy o kilka lat.

Σ_{1}^{b}

$\Sigma^b_1$

S_{2}^{1}

$S^1_2$

François G. Dorais
źródło

$\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$

Inną klasę przykładów podano w testach nieredukowalności i algorytmach faktoryzacji dla wielomianów (przede wszystkim nad polami skończonymi i racjonalnymi). Te niezmiennie opierają się na małym twierdzeniu Fermata lub na jego uogólnieniu (między innymi) i jako takie nie są znane jako możliwe do sformalizowania w odpowiedniej teorii ograniczonej arytmetyki. Zazwyczaj algorytmy te są losowe, ale w przypadku deterministycznych przykładów czasu wielomianowego można wziąć test nieredukowalności Rabina lub algorytm pierwiastka kwadratowego Tonelli – Shanksa (sformułowany tak, że jako część danych wejściowych wymagana jest kwadratowa nieresztalność).

Emil Jeřábek wspiera Monikę
źródło

Test pierwszeństwa AKS wydaje się dobrym kandydatem, jeśli wierzyć Wikipedii.

Spodziewam się jednak, że taki przykład będzie trudny do znalezienia. Istniejące dowody zostaną sformułowane w taki sposób, aby oczywiście nie były wykonywane w ograniczonej arytmetyce, ale prawdopodobnie będą one „przystosowalne” do ograniczonej arytmetyki przy większym lub mniejszym wysiłku (zwykle większym).

Andrej Bauer
źródło

S_{2}^{1}

$S^1_2$

S_{2}^{1}

$S^1_2$

S_{2}^{1}

$S^1_2$

Jest wspaniały artykuł Krajicka i Pudlaka, który podaje kilka innych przykładów: karlin.mff.cuni.cz/~krajicek/j-crypto.ps

François G. Dorais

@ François, dlaczego nie opublikować odpowiedzi? :)

Kaveh

Tak więc otrzymuję najwyższą liczbę głosów pozytywnych za wcześniejsze zgadywanie, podczas gdy inni wiedzą, co się dzieje. Matematyka jest jak MTV.

Andrej Bauer,