From 17875d57cb332c77aa7c139a83b8d1c6872adbee Mon Sep 17 00:00:00 2001
From: Jan-Niclas Loosen <mail@jnloos.de>
Date: Fri, 18 Apr 2025 20:28:21 +0200
Subject: [PATCH] first homework

---
 chapter-03/binseq/main.py                     |   1 +
 .../__pycache__/decidable.cpython-313.pyc     | Bin 0 -> 2937 bytes
 chapter-03/decidable/decidable.py             |  54 ++++++++++++++++++
 chapter-03/decidable/main.py                  |  10 ++++
 chapter-03/dedekint/main.py                   |   1 +
 5 files changed, 66 insertions(+)
 create mode 100644 chapter-03/decidable/__pycache__/decidable.cpython-313.pyc
 create mode 100644 chapter-03/decidable/decidable.py
 create mode 100644 chapter-03/decidable/main.py

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 0000000000000000000000000000000000000000..d03a1f41490cee7aa21c4332e99af44e80d092ed
GIT binary patch
literal 2937
zcmb7GU2Gf25#IaZ`D}_mA}QH%<>V5{X)Z2BIihM*k?pW*3fGR5#%BU7OyqDP&obrX
zQQA8d{sB@w1$2K9IjC&v$po4Q87)xfEf0N2fV>8fkN_4I4j`a;@k>FM0n*3L?2(j|
zxDQ=`yR$p9GdnZi%&{Gb93n6#?ul2w2ods6+;oTBA=+6W)`&q2;Q~1?P(edlyda*J
zs06e`<s;-JV#r5{5t<N#TQoGU=m(zQMi-bmZ8?rL=h#3?)y1VJ8l0Dq*&X2y(f$aC
zHBuy0FbEY5fl7v0lntpED#{t5sANTWC&|iaZb7C8ifZv-Rxp5TDDXP~Kec$MD03;*
zIEYdU!bC?s4Hs1dxLMH%Bd2%X$Il~h-nZ{OYDBok7+8#Qi*X}H`{(0&Ka(%MnS1Mr
z0;-vClL=Q!QpXA|7zf<9hhSPG1<ipq7=^eabm@5r&#W#orEHffWt)XcHP`cXiOHVr
zT%iX+j$(>D)TL<}dna?XR<$z=mg`nZj^$;3O=}DGHQ&xm*Q$%lzU5bHuH~e2Fx~Jf
zUZ!-_TJ&w29vjba8<>V&YIN}iQ%$qtR(#WB5%g%ZyG7$(A51G`d+_id!`lOce>&8L
zJ@~uGge4}=ReX;r)b^LDyU%+Sgt+(r0%DD1h$|I@G=$2PFZX=UixV9>NzR$T3*}`)
zm@E)tjS!NTF7AydnuTEq86huT#_aNum%2LA5T-PoclR36K*tCHonktHmJ7Mbe}L}8
zT=#*lhTYZZ>C#9cmj*dko|*lh(!#E#8H<o`$DS_FQcV66KB0rU%tF+1=WV9g*L~Y9
zGs&@CrdW%Mu+bHo1R<KjX#ge&t4nV%iP}{rR6N8NBpwEhAvb24PR*S+%az|&JjgXm
zb&|I4Gy<aD?_gRXJF)({yd90*w(HV2{e!Fi-5=F+JF&#7^@r=*@zlNWop9rw#&k3L
zx8aTQU-hlw@vWikSMiDM_&{rr#8dTftDi*Tt0!-tt53HS5>M{l%l$dJ9Z%j-Ka_Sl
znsRrePmhtrvDWkaDuu`cT&|Ze5Z!^<<LEd7#2VRy2*@vV5%Fi@2+^h4eV0%H2C6Od
zOY?#*&i?WNln>S5z(aN?Lh6)bRp-jq8TJAX%@ta!0>b^#DW_Jl9PbPefxvORiTYMZ
zGtZy;K-{f4P>m>oWf<l5TIj0mR7`iv<uFSt<eOM>)mlHh6+5x1p5UtYdD9EQ=OF#A
zyhifmB2eESaN238dpT)1bA|uw29}<98C~V$;xpi1(4J+h+t90WUWPsk=~+-+X}16i
z$!DhvP4RTS3&a@#z8~;lPdqJ7zDmex;g#SW#EL@N_8{O=uc{`&$+tyM)b>h4U(v`V
z(1h_b#L07naHQ~xqtC%1WD7ekv{b>R&jaOQ0JRlfJoLvvvyoj?&`!JjAvDr>^<|j;
zvqBoVX8)t1(JzNaKQcB_fBDT<L!*y|&OXe3B7A)66YJxt&7reA!&C=(sP=>Ia@7Xa
zHOj(e+pSeAE^auQSjt56-z#E0#4*O?rRADWUjQ`}8*ktM`ik}cM$iBv9Bti~v&0X*
zK`*@vFu~h*V(|}d-M-bZ?pN2VfJWX5KDc)KS|fLVW_@NWszX<ZB_G9xw_?N1>AxR)
zaO}(2sk;2Q|Bbrx7(iU!iXGonj|UEpg3{7nMD}p}K5#I}fHEu;KJvX}LW2jV;3J?t
ztEulc@g6L|h9SN!7*ZNKnJdn`7&KTz2GsXZ+_ghU6#jbT#V8q<0S?M6gO+oW31c_q
z>)L7Urlg(Fbcr4X`5>&=9d(%k_6S9nn2Ige^n4mL6SRO44+5@O9<o@NM>^P?1PSjK
zFu}JmIZ#(0Lt|aKd!(M*?n~XjwSH^k<o);7-&>a+j&Jq-^!MkUN+fX<dS_yAwR~^k
z&cbT3nQRuC=Qm@SO*O+~tBVw$#UD7UC-AH6T2&jq%7;v|S}QL*NcWlM(z4}rIPfjF
zQlXyjR9t`=uq9}76k98NL~1pM#*ysv@LxfxYWr7fWv0&L3g*v$b;)3|QvtVLL!(fW
zgre6J|LiddBk?*?117kRw@u6UX=QHNw>{IOSQr5!u-kE9^9kAv@tQEbPg;r?I@}m;
z5m=h9Y)o%VJRI40ee0!D-{MJ2B}!sDJN1+#L#f7i3zufFY?S!!)6}P>&z}1h8EpxK
zTOv@cS2-nwezH2<Ca`o^KtXg-NC~~%NVW+q9TrfnL?|@YkXi(mrt}>y!Q-(D&gu$_
zm1>S-m+-HXH)_q5f)Ix0tBW^Y3&Mh_4&2=DI#Z{D+?=83K?I@iA<kNoAP8TRk*~?X
TPB^lnekYF!WB(>Fam)V&k@;Ja

literal 0
HcmV?d00001

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