first homework

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 "."

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}"

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))
+

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