Implementing field extensions of the form Q[sqrt(b)]

René Thiemann 🌐

February 6, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We apply data refinement to implement the real numbers, where we support all numbers in the field extension Q[sqrt(b)], i.e., all numbers of the form p + q * sqrt(b) for rational numbers p and q and some fixed natural number b. To this end, we also developed algorithms to precisely compute roots of a rational number, and to perform a factorization of natural numbers which eliminates duplicate prime factors.

Our results have been used to certify termination proofs which involve polynomial interpretations over the reals.

License

GNU Lesser General Public License (LGPL)

History

July 11, 2014
Moved NthRoot_Impl to Sqrt-Babylonian.

Topics

Session Real_Impl

Depends on

Used by

Cite

× 
@article{Real_Impl-AFP,
  author  = {René Thiemann},
  title   = {Implementing field extensions of the form Q[sqrt(b)]},
  journal = {Archive of Formal Proofs},
  month   = {February},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/Real_Impl.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: