Sztuczka zastosowana w dowodzie podwójnie wykładniczej złożoności arytmetyki Presburger'a

Wysłałem to na MathUnderflow, ale nie otrzymałem odpowiedzi, więc pomyślałem, że spróbuję tutaj,

Czytam stary artykuł Rabina i Fischera [opublikuje link, jeśli to możliwe], gdzie między innymi udowodniono podwójnie wykładniczą złożoność arytmetyki Presburger'a.

Dowód opiera się na istnieniu formuły $I_{n}(x)$ nieformalne stwierdzenie „$x < 2^{2^{kx+1}}$" z $|I_{n}| \in O(n)$. Chociaż konstrukcja tej formuły nie została podana w artykule, co było dla mnie zaskoczeniem, biorąc pod uwagę, że jest ona prawdopodobnie wysoce nietrudna, biorąc pod uwagę tę granicę i fakt, że mamy do dyspozycji tylko dodatek! ¹

Później dowiedziałem się, że konstrukcja tej formuły opiera się na „sztuczce” odkrytej wcześniej przez Fischera i niezależnie przez Volkera Strassena, ale nie udało mi się wyśledzić artykułu szczegółowo opisującego tę sztuczkę!

Więc jeśli ktoś wie o artykule, o którym mówię i może albo skierować mnie w jego stronę, albo nawet opisać mi sztuczkę ...

Ten post z blogu Liptona zawiera link do artykułu, a także wspomina [i zawiera przybliżony, niestety niewystarczający dla mnie szkic] wspomnianej sztuczki BTW.

¹ Wiem, że jest to niejasny opis. Chociaż wystarczająco szczegółowy opis byłby o wiele za długi dla postu SX, mam tylko nadzieję, że ktoś, kto już wie o danym papierze - a zatem może zrobić to z krótkim szkicem - wpadnie na to i może mi pomóc .

Komentarz Martina (i kontynuacja Yuvala) zawiera odniesienie, które wyjaśnia konstrukcję bardziej szczegółowo.

Opracuję trochę, ponieważ uważam, że jest to wspaniały dowód: w zasadzie wykonuje on „zwykły” dowód nierozstrzygalności PA (arytmetyka z dodawaniem i mnożeniem), ale relatywizowany do$2^{2^{c\cdot n}}$! Oznacza to, że istnieje (krótka) formuła, która wyraża mnożenie do tej liczby, tj. Formuła$M_n(x,y,z)$ takie, że

$$M_n(x,y,z) \Leftrightarrow x\times y=z\ \wedge x< 2^{2^n}$$

Teraz budujesz $M_n$ przez włączenie indukcyjne $n$, z kluczową sztuczką, która przypomina algorytm Karatsuba do mnożenia liczb binarnych lub niektóre sztuczki do mnożenia macierzy:

W definicji dla $M_{n+1}(x,y,z)$ kończy się to koniunkcją formularza

$$M_{n}(x_1,y_1,z_1)\wedge M_{n}(x_2,y_2,z_2)\wedge M_{n}(x_3,y_3,z_3)$$

Ale możesz to zastąpić

$$\forall u v w,(u=x_1\wedge v=y_1\wedge w=z_1)\vee(u=x_2\wedge v=y_2\wedge w=z_2)\vee(u=x_3\wedge v=y_3\wedge w=z_3)\Rightarrow M_n(u,v,w)$$

Ta sztuczka pozwala na liniowy wzrost wielkości zamiast wykładniczej (w zależności od $n$).

W grę wchodzi kilka innych sztuczek, ale to jest główna. Wewnętrzne elementy rekurencji są oczywiście ważne, ale podobieństwo do sztuczki Karatsuba jest naprawdę dość uderzające.