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

Algorytmiczna teoria liczb naturalnychEdytuj

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   zdeterminowany jest przez alfabet   i zbiór   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

 
 
 

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   oznacza dowolną formułę pierwszego rzędu ze zmienną wolną  

 

tw. o poprawności algorytmu Euklidesa

 

Algorytmiczna teoria liczb wymiernychEdytuj

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:

 
(Euc)

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

Algorytmiczna teoria struktury liczb rzeczywistych z porządkiemEdytuj

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ądkuEdytuj

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 ↓]

Algorytmiczna struktura ciała liczb zespolonychEdytuj

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.

Zobacz teżEdytuj

BibliografiaEdytuj