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 ${\displaystyle {\mathcal {L}},}$ rachunek programów inaczej logika algorytmiczna ${\displaystyle {\mathcal {AL}}}$ i zbiór aksjomatów specyficznych tej teorii ${\displaystyle 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.

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 ${\displaystyle {\mathcal {L}}=\langle A,W\rangle }$ zdeterminowany jest przez alfabet ${\displaystyle A}$ i zbiór ${\displaystyle 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

${\displaystyle \forall x\ x+1\neq 0}$

${\displaystyle \forall x,y\ x+1=y+1\implies x=y}$

${\displaystyle \forall x\{y:=0;\,\mathbf {while} \ x\neq y\ \mathbf {do} \ y:=y+1\ \mathbf {od} \}(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 ${\displaystyle \alpha (x)}$ oznacza dowolną formułę pierwszego rzędu ze zmienną wolną ${\displaystyle x}$

${\displaystyle {\Big (}\alpha (x/0)\land \forall _{x}{\big (}\alpha (x)\Rightarrow \alpha (x/s(x)){\big )}{\Big )}\implies \forall _{x}\alpha (x)}$

tw. o poprawności algorytmu Euklidesa

${\displaystyle \underbrace {\forall _{n\neq 0}\,\forall _{m\neq 0}\left\{{\begin{array}{l}{\textbf {while}}\ n\neq m\ {\textbf {do}}\ {\textbf {if}}\ n\geqslant m\ {\textbf {then}}\ n:=n-m\ {\textbf {else}}\ m:=m-n\ {\textbf {fi}}\ {\textbf {od}}\end{array}}\right\}(n=m)} _{halting\ formula\ of\ Euclid's\ algorithm}}$

Antoni Kreczmar udowodnił [Kreczmar 1977 ↓ ], ż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:

${\displaystyle \forall _{x\geqslant 0}\forall _{y\geqslant 0}\left\{{\begin{array}{l}\mathbf {while} \ x\neq y\ \mathbf {do} \\\qquad \mathbf {if} \ x>y\ \mathbf {then} \ x:=x-y\ \mathbf {else} \ y:=y-x\ \mathbf {fi} \\\mathbf {od} \end{array}}\right\}x=y,}$

(Euc)

którą należy czytać: dla każdych nieujemnych wartości ${\displaystyle x}$ i ${\displaystyle 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łę ${\displaystyle x=y}$ następującą po nim.

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

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

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

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.

• złożoność obliczeniowa

• [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.