An algorithmic approach to p-adic integers

Abstract

The ring of p-adic integers can be embedded as the maximal elements in a Scott domain with algebraic structure. We show how definitions and proofs in the mathematical theory of p-adics can be replaced by algorithms on the partial elements and formal programming methods working on the algorithms. Certain types of argument translate naturally into non-deterministic algorithms using the Smyth power domain.