Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions

Andrej Bauer (University of Ljubljana, Slovenia)

Jens Blanck (Swansea University, United Kingdom)

Abstract: We prove general theorems about unique existence of effective subalgebras of classical algebras. The theorems are consequences of standard facts about completions of metric spaces within the framework of constructive mathematics, suitably interpreted in realizability models. We work with general realizability models rather than with a particular model of computation. Consequently, all the results are applicable in various established schools of computability, such as type 1 and type 2 effectivity, domain representations, equilogical spaces, and others.

Keywords: computable and effective algebra, constructive metric spaces, realizability

Categories: G.0