Algorytmiczna teoria liczb

Algorytmiczna teoria liczb

Algorytmiczna teoria liczb obejmuje zadania związane z dowodzeniem właściwości programów działających w obszarze liczb naturalnych (lub innych struktur liczbowych). Wśród badanych właściwości znajdują się m.in.: własność stopu, poprawność programu w kontekście warunków początkowych i końcowych oraz równoważność dwóch programów.

Teoria ta składa się z sformalizowanego podejścia algorytmicznego, które obejmuje: język programów i formuł algorytmicznych L, rachunek programów, znany również jako logika algorytmiczna AL, oraz zbiór aksjomatów specyficznych dla tej teorii Ax.

Początki tej dziedziny datują się na czasy starożytne, kiedy to Euklides przedstawił algorytm do obliczania największego wspólnego dzielnika, a Eratostenes zaprezentował metodę znajdowania liczb pierwszych, znaną jako sito Eratostenesa. W nowożytności wprowadzono nowe testy pierwszości oraz metody faktoryzacji.

Algorytmiczna teoria liczb naturalnych

W 1969 roku wprowadzono aksjomat osiągalności. Udowodniono, że teoria ta jest kategoryczna, co oznacza, że opisuje standardowy model liczb naturalnych z dokładnością do izomorfizmu (por. [AlgoLog], s. 155).

W ramach tej teorii można przeprowadzać formalne dowody poprawności programów, na przykład dowód poprawności algorytmu Euklidesa. Warto zauważyć, że podręcznikowe dowody poprawności tego algorytmu bazują na nieformalnym sformułowaniu aksjomatu Archimedesa, który jest przedstawiany bez dowodu. Aksjomat Archimedesa stanowi twierdzenie algorytmicznej teorii liczb naturalnych.

Język tej teorii L jest określony przez alfabet A i zbiór W wyrażeń poprawnie zbudowanych. W alfabecie tej teorii wyróżniamy stałe 0 i 1, operatory „s” (następnik), „+” (dodawanie), „*” (mnożenie) oraz relację „=” równości.

Aksjomaty algorytmicznej teorii liczb naturalnych obejmują:

  • ∀x (x + 1 ≠ 0) – dla każdego x, x powiększone o 1 nie jest równe 0.
  • ∀x, y (x + 1 = y + 1 ⇒ x = y) – dla każdego x i y, jeśli x powiększone o 1 jest równe y powiększonemu o 1, to x jest równe y.
  • ∀x{y := 0; while x ≠ y do y := y + 1} (x = y) – dla każdego x, y, jeśli y jest równe 0, to pętla kończy się, gdy x jest równe y. Aksjomat ten stwierdza, że każdy element struktury jest osiągalny z zera przez dodawanie 1, co oznacza brak elementów niestandardowych.

Przykłady twierdzeń w tej teorii to m.in. schemat indukcji:

Niech α(x) oznacza dowolną formułę pierwszego rzędu ze zmienną wolną x. Jeśli α(0) oraz dla każdego x (α(x) ⇒ α(s(x))) to wówczas dla każdego x α(x).

Twierdzenie o poprawności algorytmu Euklidesa brzmi: dla wszystkich n ≠ 0 oraz m ≠ 0, pętla while n ≠ m, w której if n ≥ m, to n := n – m, inaczej m := m – n, kończy się, gdy n = m.

Algorytmiczna teoria liczb wymiernych

Antoni Kreczmar wykazał, że każde ciało spełniające własność stopu algorytmu Euklidesa jest izomorficzne z ciałem liczb naturalnych. Innymi słowy, algorytmiczne właściwości programów działających w ciele liczb wymiernych wynikają z następującej formuły: dla każdej nieujemnej wartości x i y, program Euklidesa kończy obliczenia, a jego wyniki spełniają formułę x = y.

Algorytmiczna teoria struktury liczb rzeczywistych z porządkiem

W 1967 roku E. Engeler udowodnił, że semantyczne właściwości programów w ciele liczb rzeczywistych z porządkiem wynikają z aksjomatu Archimedesa.

Algorytmiczna teoria struktury liczb rzeczywistych bez relacji porządku

Właściwości algorytmiczne programów, w których nie występuje predykat mniejszości „<”, wynikają z aksjomatów definiujących formalnie rzeczywiste ciało.

Algorytmiczna struktura ciała liczb zespolonych

Właściwości algorytmiczne programów działających w ciele liczb zespolonych wynikają z aksjomatu ciała o charakterystyce zero.

Niektórzy autorzy twierdzą, że algorytmiczna teoria liczb to dziedzina związana z algebraiczną lub obliczeniową teorią liczb, która zajmuje się badaniem efektywności algorytmów obliczeniowych w teorii liczb. Typowym przykładem jest problem rozkładu liczby na czynniki pierwsze.

Zobacz też

złożoność obliczeniowa

Bibliografia

  • [AK1] Antoni Kreczmar. Programmability in Fields. „Fundamenta Informaticae”, s. 195–230, 1977.
  • [AlgoLog] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic. Warszawa: PWN, 1987, s. 345.
  • [LogProg1] Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów cz.1. Warszawa: WNT, 1992, s. 294.
  • [LogProg2] Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów cz.2. Warszawa: WNT, 1992, s. 294.
  • [CentrumBanachAL] Lech Banachowski, Antoni Kreczmar, Grażyna Mirkowska, Helena Rasiowa, Andrzej Salwicki: An introduction to Algorithmic Logic – Metamathematical Investigations of Theory of Programs. T. 2: Banach Center Publications. Warszawa: PWN, 1977, s. 7–99, seria: Banach Center Publications.
  • [HRAL] Helena Rasiowa: Algorithmic Logic – Notes from Seminar in Simon Fraser University. T. 281. Warsaw: 1975, seria: Reports of Institute of Computer Science Polish Academy of Sciences.
  • [RepoAL] repozytorium logiki algorytmicznej. 2013. [dostęp 2018-10-07].
  • [AL4software] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic for Software Construction and Verification. Dąbrowa Leśna: Dąbrowa Research, 2014, s. 154.
Przeczytaj u przyjaciół: