diff --git a/chapter-03/binseq/main.py b/chapter-03/binseq/main.py index b068190..c39ee1b 100644 --- a/chapter-03/binseq/main.py +++ b/chapter-03/binseq/main.py @@ -1,6 +1,7 @@ from binseq import REAL from math import isqrt # integer sqrt +# Theorem 3.1 (2) def one_third(n): if n == 1: return "." diff --git a/chapter-03/decidable/__pycache__/decidable.cpython-313.pyc b/chapter-03/decidable/__pycache__/decidable.cpython-313.pyc new file mode 100644 index 0000000..d03a1f4 Binary files /dev/null and b/chapter-03/decidable/__pycache__/decidable.cpython-313.pyc differ diff --git a/chapter-03/decidable/decidable.py b/chapter-03/decidable/decidable.py new file mode 100644 index 0000000..54a58a3 --- /dev/null +++ b/chapter-03/decidable/decidable.py @@ -0,0 +1,54 @@ +from collections.abc import Callable +from gmpy2 import mpq + +MAX_BITS = 32 + +class REAL: + # x = z + sum(2 ** -(i + 1) for i in A) + # Needed arguments: z in Q and A subset N + def __init__(self, z: int, f: Callable[[int], bool]): + self.decide = f + self.const = z + + @staticmethod + def __long_division(p: int, q: int, bits: int = MAX_BITS) -> list[int]: + bnry = [] + rem = p % q + + for i in range(bits): + # Fill with 0 when finished + if rem == 0: + bnry.extend([0] * (bits - len(bnry))) + break + + # Shift remainder left by 1 bit + rem *= 2 # Shift <=> Doubling + + # Determine bit value + if rem >= q: + bnry.append(1) + rem -= q + else: + bnry.append(0) + return bnry + + @staticmethod + def from_int(x: int): + return REAL(z=x, f=lambda i: False) + + @staticmethod + def from_rational(x: mpq): + quot = x.numerator // x.denominator + rem = x.numerator % x.denominator + + bnry = REAL.__long_division(rem, x.denominator) + decide = lambda n: (0 <= n < len(bnry) and bnry[n] == 1) + return REAL(z=quot, f=decide) + + + def as_str(self, n: int) -> str: + bnry_str = '' + for i in range(n): + bnry_str += '1' if self.decide(i) else '0' + # Binary depiction of z not applied here + return f"x = {self.const} + {bnry_str}" diff --git a/chapter-03/decidable/main.py b/chapter-03/decidable/main.py new file mode 100644 index 0000000..3ee7393 --- /dev/null +++ b/chapter-03/decidable/main.py @@ -0,0 +1,10 @@ +from decidable import REAL +from gmpy2 import mpq + +# Theorem 3.1 (5) + +print(REAL.from_rational(mpq(1,3)).as_str(10)) +print(REAL.from_rational(mpq(41,5)).as_str(10)) +print(REAL.from_rational(mpq(1,5)).as_str(10)) +print(REAL.from_int(1).as_str(10)) + diff --git a/chapter-03/dedekint/main.py b/chapter-03/dedekint/main.py index 8944d2c..15fd838 100644 --- a/chapter-03/dedekint/main.py +++ b/chapter-03/dedekint/main.py @@ -2,6 +2,7 @@ from dedekint import REAL # mpq for rational numbers from gmpy2 import mpq +# Theorem 3.1 (4) def sqrt_two(q): if q <= 0 or q * q < 2: return True