From effc98d589b508ca094a449af6bd437619b16915 Mon Sep 17 00:00:00 2001 From: d_m Date: Sun, 14 Apr 2024 16:07:27 -0400 Subject: [PATCH] rationals working, sort of --- arith.modal | 61 +++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 55 insertions(+), 6 deletions(-) diff --git a/arith.modal b/arith.modal index c6bc774..96d91e5 100644 --- a/arith.modal +++ b/arith.modal @@ -1,5 +1,6 @@ <> (-- ?x) () --- ( little endian binary natural numbers and integers ) + +-- ( N: little-endian natural numbers ) -- ( constants ) <> zero ((0 ())) @@ -42,15 +43,23 @@ <> ((tostr1 (N (?h ?t)) ?a)) ((tostr2 (divmod (N (?h ?t)) (N ten)) ?a)) <> ((tostr2 ((N ?q) (N ?r)) ?a)) ((tostr1 (N ?q) ((decimal ?r) ?a))) +-- ( concatenate lists ) +<> ((concat (?h ?t) ?r)) ((?h (concat ?t ?r))) +<> ((concat () ?r)) (?r) + -- ( to string ) +<> ((str (N ?x))) (emit force (tostr (N ?x))) <> ((str (Z (+ ?x)))) ((str (N ?x))) <> ((str (Z (- ?x)))) (emit force (- (tostr (N ?x)))) -<> ((str (N ?x))) (emit force (tostr (N ?x))) +<> ((str (Q (?s ?n ?d)))) ((qstr ?s (force (tostr (N ?n))) (force (tostr (N ?d))))) +<> ((qstr + (force/r ?l) (force/r ?m))) (emit force (concat ?l (/ ?m))) +<> ((qstr - (force/r ?l) (force/r ?m))) (emit force (concat (- ?l) (/ ?m))) -- ( force a list to evaluate to digits/letters ) <> ((?h force/r ?t)) (force/r (?h ?t)) <> (force ()) (force/r ()) <> (force (- ?t)) ((- force ?t)) +<> (force (/ ?t)) ((/ force ?t)) <> (force (0 ?t)) ((0 force ?t)) <> (force (1 ?t)) ((1 force ?t)) <> (force (2 ?t)) ((2 force ?t)) @@ -201,8 +210,8 @@ <> ((mod1 (?q ?r))) (?r) -- ( expontentiation ) -<> ((pow (N ?x) ())) ((N (1 ()))) -<> ((pow (N ?x) (N (0 ())))) ((N (1 ()))) +<> ((pow (N ?x) ())) ((N one)) +<> ((pow (N ?x) (N (0 ())))) ((pow (N ?x) ())) <> ((pow (N ?x) (N (1 ())))) ((N ?x)) <> ((pow (N ?x) (N (0 ?k)))) ((pow (mul (N ?x) (N ?x)) (N ?k))) <> ((pow (N ?x) (N (1 ?k)))) ((mul (N ?x) (pow (mul (N ?x) (N ?x)) (N ?k)))) @@ -267,6 +276,8 @@ <> ((decimal (0 (0 (0 (1 ())))))) (8) <> ((decimal (1 (0 (0 (1 ())))))) (9) +-- ( Z: signed integers ) + <> ((nat>int + (N ?x))) ((Z (+ ?x))) <> ((nat>int - (N ?x))) ((Z (- ?x))) <> ((nat>pos (N ?x))) ((Z (+ ?x))) @@ -277,7 +288,7 @@ <> ((cmp (Z (?s (0 ()))) (Z (?s (0 ()))))) (#eq) <> ((cmp (Z (+ ?x)) (Z (+ ?y)))) ((cmp (N ?x) (N ?y))) -<> ((cmp (Z (+ ?x)) (Z (- ?y)))) (#gt) +<> ((cmp (Z (+ ?x)) (Z (?s ?y)))) (#gt) <> ((cmp (Z (- ?x)) (Z (- ?y)))) ((cmp (N ?y) (N ?x))) <> ((cmp (Z (- ?x)) (Z (?s ?y)))) (#lt) @@ -326,4 +337,42 @@ <> ((int1 (?h ?t))) ((int2 + (nat1 (?h ?t)))) <> ((int2 ?s (N ?x))) ((Z (?s ?x))) -(str (mul (int -133) (int 77))) +-- ( Q: rational numbers ) + +-- ( ensure n and d are coprime by dividing both by their gcd ) +<> ((ratify ?s (N (0 ())) (N ?d))) ((Q (+ zero one))) +<> ((ratify ?s (N ?n) (N ?d))) ((ratify1 ?s (N ?n) (N ?d) (gcd (N ?n) (N ?d)))) +<> ((ratify1 ?s (N ?n) (N ?d) (N ?g))) ((ratify2 ?s (div (N ?n) (N ?g)) (div (N ?d) (N ?g)))) +<> ((ratify2 ?s (N ?n) (N ?d))) ((Q (?s ?n ?d))) + +-- ( convert N to Q ) +<> ((nat>rat + (N ?x))) ((Q (+ ?x one))) +<> ((nat>rat - (N ?x))) ((Q (- ?x one))) + +-- ( convert Z to Q ) +<> ((int>rat (Z (+ ?x)))) ((Q (+ ?x one))) +<> ((int>rat (Z (- ?x)))) ((Q (- ?x one))) + +<> ((negate (Q (+ ?n ?d)))) ((Q (- ?n ?d))) +<> ((negate (Q (- ?n ?d)))) ((Q (+ ?n ?d))) + +<> ((cmp (Q (?s (0 ()) (1 ()))) (Q (?s (0 ()) (1 ()))))) (#eq) +<> ((cmp (Q (+ ?x ?d)) (Q (+ ?y ?e)))) ((cmp (mul (N ?x) (N ?e)) (mul (N ?y) (N ?d)))) +<> ((cmp (Q (+ ?x ?d)) (Q (?s ?y ?e)))) (#gt) +<> ((cmp (Q (- ?x ?d)) (Q (- ?y ?e)))) ((cmp (mul (N ?y) (N ?d)) (mul (N ?x) (N ?e)))) +<> ((cmp (Q (- ?x ?d)) (Q (?s ?y ?e)))) (#lt) + +<> ((add (Q (?s ?x ?d)) (Q (?t ?y ?e)))) ((qadd1 ?s ?t (mul (N ?x) (N ?e)) (mul (N ?y) (N ?d)) (mul (N ?d) (N ?e)))) +<> ((qadd1 ?s ?t (N ?x) (N ?y) (N ?d))) ((qadd2 (add (Z (?s ?x)) (Z (?t ?y))) (N ?d))) +<> ((qadd2 (Z (?s ?n)) (N ?d))) ((ratify ?s (N ?n) (N ?d))) + +<> ((sub (Q (?s ?x ?d)) (Q (?t ?y ?e)))) ((qsub1 ?s ?t (mul (N ?x) (N ?e)) (mul (N ?y) (N ?d)) (mul (N ?d) (N ?e)))) +<> ((qsub1 ?s ?t (N ?x) (N ?y) (N ?d))) ((qsub2 (sub (Z (?s ?x)) (Z (?t ?y))) (N ?d))) +<> ((qsub2 (Z (?s ?n)) (N ?d))) ((ratify ?s (N ?n) (N ?d))) + +<> ((mul (Q (?s ?x ?d)) (Q (?t ?y ?e)))) ((qmul1 (mul (Z (?s ?x)) (Z (?t ?y))) (mul (N ?d) (N ?e)))) +<> ((qmul1 (Z (?s ?n)) (N ?d))) ((ratify ?s (N ?n) (N ?d))) + +<> ((div (Q (?s ?x ?d)) (Q (?t ?y ?e)))) ((mul (Q (?s ?x ?d)) (Q (?t ?e ?y)))) + +(str (mul (Q (+ sixteen ten)) (Q (- sixteen ten))))