Algorytmiczna teoria liczb

Algorytmiczna teoria liczb – do zadań tej teorii zaliczamy przeprowadzanie dowodów własności programów wykonywanych w dziedzinie liczb naturalnych (lub w innych strukturach liczbowych). Rozważane własności to między innymi: własność stopu, poprawność programu względem warunków początkowego i końcowego, równoważność dwu programów.

Na sformalizowaną teorię algorytmiczną składają się: język programów i formuł algorytmicznych $ℒ,$ rachunek programów inaczej logika algorytmiczna $𝒜ℒ$ i zbiór aksjomatów specyficznych tej teorii $Ax.$

Początki tej nauki sięgają starożytności, kiedy Euklides podał algorytm obliczania największego wspólnego dzielnika, a Eratostenes – metodę znajdowania liczb pierwszych zwaną sitem Eratostenesa. W czasach nowożytnych pojawiły się między innymi nowe testy pierwszości oraz metody faktoryzacji.

Algorytmiczna teoria liczb naturalnych

W 1969 r. podano aksjomat osiągalności. Wykazano, że teoria ta jest kategoryczna, tzn. z dokładnością do izomorfizmu opisuje standardowy model liczb naturalnych. por. [AlgoLog], s. 155.

W tej teorii można przeprowadzić dowody formalne poprawności programów, np. dowód poprawności algorytmu Euklidesa. Nb. podręcznikowe dowody poprawności algorytmu Euklidesa bazują na nieformalnym sformułowaniu aksjomatu Archimedesa, przedstawianym bez dowodu. Aksjomat Archimedesa jest twierdzeniem algorytmicznej teorii liczb naturalnych.

Język tej teorii $ℒ=⟨A,W⟩$ zdeterminowany jest 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) i relację „=” równości.

Aksjomaty algorytmicznej teorii liczb naturalnych

$\mathrm{\forall }xx+1\ne 0$

$\mathrm{\forall }x,yx+1=y+1⟹x=y$

$\mathrm{\forall }x\{y:=0;𝐰𝐡𝐢𝐥𝐞x\ne y𝐝𝐨y:=y+1𝐨𝐝\}(x=y)$

ten aksjomat stwierdza, że każda element struktury jest osiągalny z zera przez dodawanie jedynki, tj. nie ma elementów niestandardowych.

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

niech $\alpha (x)$ oznacza dowolną formułę pierwszego rzędu ze zmienną wolną $x$

$(\alpha (x/0)\wedge {\mathrm{\forall }}_x(\alpha (x)\Rightarrow \alpha (x/s(x))\left)\right)⟹{\mathrm{\forall }}_x\alpha (x)$

tw. o poprawności algorytmu Euklidesa

$\underset{haltingformulaofEucli{d}^{\prime }salgorithm}{\underbrace{{\mathrm{\forall }}_{n\ne 0}{\mathrm{\forall }}_{m\ne 0}\left\{\begin{array}{c}\mathbf{\text{while}}n\ne m\mathbf{\text{do}}\mathbf{\text{if}}n⩾m\mathbf{\text{then}}n:=n-m\mathbf{\text{else}}m:=m-n\mathbf{\text{fi}}\mathbf{\text{od}}\end{array}\right\}(n=m)}}$

Algorytmiczna teoria liczb wymiernych

Antoni Kreczmar udowodnił [[[:Szablon:Odn]]], że każde ciało spełniające własność stopu algorytmu Euklidesa jest izomorficzne z ciałem liczb naturalnych. Inaczej mówiąc algorytmiczne własności programów wykonywanych w ciele liczb wymiernych wynikają z następującej formuły:

Szablon:Wzór

którą należy czytać: dla każdych nieujemnych wartości $x$ i $y,$ program(algorytm) Euklidesa kończy obliczenia. A dokładniej, program ujęty w nawiasy {} kończy swoje obliczenia i jego wyniki spełniają formułę $x=y$ następującą po nim.

Algorytmiczna teoria struktury liczb rzeczywistych z porządkiem

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

Algorytmiczna teoria struktury liczb rzeczywistych bez relacji porządku

Algorytmiczne własności programów, w których nie występuje predykat mniejszości „<”, wynikają z aksjomatów bycia ciałem formalnie rzeczywistym. [[[:Szablon:Odn]]]

Algorytmiczna struktura ciała liczb zespolonych

Własności algorytmiczne programów wykonywanych w ciele liczb zespolonych wynikają z aksjomatu ciała charakterystyki zero. [[[:Szablon:Odn]]]

Inni autorzy uważają, że algorytmiczna teoria liczb to algebraiczna lub obliczeniowa teoria liczb – dział informatyki teoretycznej i matematyki, zajmujący się badaniami nad efektywnością algorytmów obliczeniowych w teorii liczb. Typowym przykładem jest tutaj problem rozkładu liczby na czynniki pierwsze.

Zobacz też

• złożoność obliczeniowa

Bibliografia

• [AK1] Szablon:Cytuj pismo
• [AlgoLog]Szablon:Cytuj książkę
• [LogProg1] Szablon:Cytuj książkę
• [LogProg2] Szablon:Cytuj książkę
• [CentrumBanachAL] Szablon:Cytuj książkę
• [HRAL] Szablon:Cytuj książkę
• [RepoAL] Szablon:Cytuj stronę
• [AL4software] Szablon:Cytuj książkę