From 507c8dd51706fe5750791967fb726cafc5eca1b3 Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Thu, 1 Jan 2026 20:42:28 +1300 Subject: Division, logarithm, exponentiation --- src/kompsos-math.adb | 381 ++++++++++++++++++++++++++++++++++++++++++++++++++- src/kompsos-math.ads | 86 +++++++++++- 2 files changed, 461 insertions(+), 6 deletions(-) diff --git a/src/kompsos-math.adb b/src/kompsos-math.adb index 8de7c9f..2c2ddf8 100644 --- a/src/kompsos-math.adb +++ b/src/kompsos-math.adb @@ -53,6 +53,21 @@ package body Kompsos.Math is Inputs : in Term_Array) return Goal := Bounded_Multiply'Access; + Divide_Access : constant access function + (This : in Goal; + Inputs : in Term_Array) + return Goal := Divide'Access; + + Split_Access : constant access function + (This : in Goal; + Inputs : in Term_Array) + return Goal := Split'Access; + + Exp_Two_Access : constant access function + (This : in Goal; + Inputs : in Term_Array) + return Goal := Exp_Two'Access; + Repeated_Multiply_Access : constant access function (This : in Goal; Inputs : in Term_Array) @@ -765,6 +780,364 @@ package body Kompsos.Math is + -- /o -- + + function Divide + (This : in Goal; + Inputs : in Term_Array) + return Goal + is + N_Term : Term renames Inputs (1); + M_Term : Term renames Inputs (2); + Quotient_Term : Term renames Inputs (3); + Remainder_Term : Term renames Inputs (4); + + One, Two, Three : Goal := This; + + N_Low : constant Term := Three.Fresh; + N_High : constant Term := Three.Fresh; + Quot_Low : constant Term := Three.Fresh; + Quot_High : constant Term := Three.Fresh; + Quot_Low_M : constant Term := Three.Fresh; + Quot_Low_M_Remain : constant Term := Three.Fresh; + Remain_Remain : constant Term := Three.Fresh; + Remain_High : constant Term := Three.Fresh; + begin + One.Unify (N_Term, Remainder_Term); + One.Unify (Quotient_Term, Zero_Term); + LT (One, N_Term & M_Term); + + Two.Unify (Quotient_Term, One_Term); + EQ_Length (Two, N_Term & M_Term); + Add (Two, Remainder_Term & M_Term & N_Term); + LT (Two, Remainder_Term & M_Term); + + LT_Length (Three, M_Term & N_Term); + LT (Three, Remainder_Term & M_Term); + GT_Zero (Three, Quotient_Term); + Three.Conjunct (Split_Access, N_Term & Remainder_Term & N_Low & N_High); + Three.Conjunct (Split_Access, Quotient_Term & Remainder_Term & Quot_Low & Quot_High); + declare + Three_A, Three_B : Goal := Three; + begin + Three_A.Unify (N_High, Zero_Term); + Three_A.Unify (Quot_High, Zero_Term); + Subtract (Three_A, N_Low & Remainder_Term & Quot_Low_M); + Multiply (Three_A, Quot_Low & M_Term & Quot_Low_M); + + GT_Zero (Three_B, N_High); + Multiply (Three_B, Quot_Low & M_Term & Quot_Low_M); + Add (Three_B, Quot_Low_M & Remainder_Term & Quot_Low_M_Remain); + Subtract (Three_B, Quot_Low_M_Remain & N_Low & Remain_Remain); + Three_B.Conjunct (Split_Access, + Remain_Remain & Remainder_Term & Zero_Term & Remain_High); + Three_B.Conjunct (Divide_Access, N_High & M_Term & Quot_High & Remain_High); + + return Disjunct (One & Two & Three_A & Three_B); + end; + end Divide; + + + procedure Divide + (This : in out Goal; + Inputs : in Term_Array) is + begin + This := Divide (This, Inputs); + end Divide; + + + + -- splito -- + + function Split + (This : in Goal; + Inputs : in Term_Array) + return Goal + is + N_Term : Term renames Inputs (1); + Remainder_Term : Term renames Inputs (2); + Low_Term : Term renames Inputs (3); + High_Term : Term renames Inputs (4); + + Outputs : Goal_Array := (1 .. 6 => This); + begin + Outputs (1).Unify (N_Term, Zero_Term); + Outputs (1).Unify (High_Term, Zero_Term); + Outputs (1).Unify (Low_Term, Zero_Term); + + declare + B_Var : constant Term := Outputs (2).Fresh; + N_Hat : constant Term := Outputs (2).Fresh; + begin + Outputs (2).Unify (N_Term, T (T (Zero_Element), T (B_Var, N_Hat))); + Outputs (2).Unify (Remainder_Term, Zero_Term); + Outputs (2).Unify (High_Term, T (B_Var, N_Hat)); + Outputs (2).Unify (Low_Term, Zero_Term); + end; + + declare + N_Hat : constant Term := Outputs (3).Fresh; + begin + Outputs (3).Unify (N_Term, T (T (One_Element), N_Hat)); + Outputs (3).Unify (Remainder_Term, Zero_Term); + Outputs (3).Unify (High_Term, N_Hat); + Outputs (3).Unify (Low_Term, One_Term); + end; + + declare + B_Var : constant Term := Outputs (4).Fresh; + N_Hat : constant Term := Outputs (4).Fresh; + A_Var : constant Term := Outputs (4).Fresh; + R_Hat : constant Term := Outputs (4).Fresh; + begin + Outputs (4).Unify (N_Term, T (T (Zero_Element), T (B_Var, N_Hat))); + Outputs (4).Unify (Remainder_Term, T (A_Var, R_Hat)); + Outputs (4).Unify (Low_Term, Zero_Term); + Outputs (4).Conjunct (Split_Access, T (B_Var, N_Hat) & R_Hat & Zero_Term & High_Term); + end; + + declare + N_Hat : constant Term := Outputs (5).Fresh; + A_Var : constant Term := Outputs (5).Fresh; + R_Hat : constant Term := Outputs (5).Fresh; + begin + Outputs (5).Unify (N_Term, T (T (One_Element), N_Hat)); + Outputs (5).Unify (Remainder_Term, T (A_Var, R_Hat)); + Outputs (5).Unify (Low_Term, One_Term); + Outputs (5).Conjunct (Split_Access, N_Hat & R_Hat & Zero_Term & High_Term); + end; + + declare + B_Var : constant Term := Outputs (6).Fresh; + N_Hat : constant Term := Outputs (6).Fresh; + A_Var : constant Term := Outputs (6).Fresh; + R_Hat : constant Term := Outputs (6).Fresh; + L_Hat : constant Term := Outputs (6).Fresh; + begin + Outputs (6).Unify (N_Term, T (B_Var, N_Hat)); + Outputs (6).Unify (Remainder_Term, T (A_Var, R_Hat)); + Outputs (6).Unify (Low_Term, T (B_Var, L_Hat)); + GT_Zero (Outputs (6), L_Hat); + Outputs (6).Conjunct (Split_Access, N_Hat & R_Hat & L_Hat & High_Term); + end; + + return Disjunct (Outputs); + end Split; + + + procedure Split + (This : in out Goal; + Inputs : in Term_Array) is + begin + This := Split (This, Inputs); + end Split; + + + + -- logo -- + + function Logarithm + (This : in Goal; + Inputs : in Term_Array) + return Goal + is + Power_Term : Term renames Inputs (1); + Base_Term : Term renames Inputs (2); + Exponent_Term : Term renames Inputs (3); + Remainder_Term : Term renames Inputs (4); + + Outputs : Goal_Array := (1 .. 7 => This); + begin + Outputs (1).Unify (Power_Term, One_Term); + GT_Zero (Outputs (1), Base_Term); + Outputs (1).Unify (Exponent_Term, Zero_Term); + Outputs (1).Unify (Remainder_Term, Zero_Term); + + Outputs (2).Unify (Exponent_Term, Zero_Term); + LT (Outputs (2), Power_Term & Base_Term); + Add (Outputs (2), Remainder_Term & One_Term & Power_Term); + + Outputs (3).Unify (Exponent_Term, One_Term); + GT_One (Outputs (3), Base_Term); + EQ_Length (Outputs (3), Power_Term & Base_Term); + Add (Outputs (3), Remainder_Term & Base_Term & Power_Term); + + Outputs (4).Unify (Base_Term, One_Term); + GT_Zero (Outputs (4), Exponent_Term); + Add (Outputs (4), Remainder_Term & One_Term & Power_Term); + + Outputs (5).Unify (Base_Term, Zero_Term); + GT_Zero (Outputs (5), Exponent_Term); + Outputs (5).Unify (Remainder_Term, Power_Term); + + Outputs (6).Unify (Base_Term, Build (2)); + declare + DD_Var : constant Term := Outputs (6).Fresh; + begin + GT_Zero (Outputs (6), DD_Var); + Outputs (6).Unify (Power_Term, T (Outputs (6).Fresh, T (Outputs (6).Fresh, DD_Var))); + Outputs (6).Conjunct (Exp_Two_Access, Power_Term & Zero_Term & Exponent_Term); + Outputs (6).Conjunct (Split_Access, + Power_Term & DD_Var & Remainder_Term & Outputs (6).Fresh); + end; + + -- I know what you're thinking. Clear as mud, right? + -- Well unfortunately the original miniKanren Scheme isn't really any better. + -- Needs a refactor or something at some point. + declare + function N is new Make_Fresh (Outputs (7)); + begin + Outputs (7) := Disjunct + (Outputs (7).Unify (Base_Term, Build (3)), + Outputs (7).Unify (Base_Term, T (N, T (N, T (N, N))))); + end; + LT_Length (Outputs (7), Base_Term & Power_Term); + declare + BaseW1_Var : constant Term := Outputs (7).Fresh; + BaseW_Var : constant Term := Outputs (7).Fresh; + PowerW_Var : constant Term := Outputs (7).Fresh; + PowerW1_Var : constant Term := Outputs (7).Fresh; + Exp_Low1_Var : constant Term := Outputs (7).Fresh; + Exp_Low_Var : constant Term := Outputs (7).Fresh; + S_Var : constant Term := Outputs (7).Fresh; + + Exp1_Var : constant Term := Outputs (7).Fresh; + BaseW_Exp1_Var : constant Term := Outputs (7).Fresh; + + Base_Exp_Low_Var : constant Term := Outputs (7).Fresh; + Exp_High_Var : constant Term := Outputs (7).Fresh; + S2_Var : constant Term := Outputs (7).Fresh; + ExpD_High_Var : constant Term := Outputs (7).Fresh; + ExpD_Var : constant Term := Outputs (7).Fresh; + + Base_ExpD_Var : constant Term := Outputs (7).Fresh; + Base_Exp1_Var : constant Term := Outputs (7).Fresh; + Base_Exp_Var : constant Term := Outputs (7).Fresh; + begin + Outputs (7).Conjunct (Exp_Two_Access, Base_Term & Zero_Term & BaseW1_Var); + Add (Outputs (7), BaseW1_Var & One_Term & BaseW_Var); + LT_Length (Outputs (7), Exponent_Term & Power_Term); + + Add (Outputs (7), Exponent_Term & One_Term & Exp1_Var); + Multiply (Outputs (7), BaseW_Var & Exp1_Var & BaseW_Exp1_Var); + LT (Outputs (7), PowerW1_Var & BaseW_Exp1_Var); + + Outputs (7).Conjunct (Exp_Two_Access, Power_Term & Zero_Term & PowerW1_Var); + Add (Outputs (7), PowerW1_Var & One_Term & PowerW_Var); + Divide (Outputs (7), PowerW_Var & BaseW_Var & Exp_Low1_Var & S_Var); + Add (Outputs (7), Exp_Low_Var & One_Term & Exp_Low1_Var); + Outputs (7) := Disjunct + (Outputs (7).Unify (Exponent_Term, Exp_Low_Var), + LT_Length (Outputs (7), Exp_Low_Var & Exponent_Term)); + + Outputs (7).Conjunct (Repeated_Multiply_Access, + Base_Term & Exp_Low_Var & Base_Exp_Low_Var); + Divide (Outputs (7), PowerW_Var & BaseW1_Var & Exp_High_Var & S2_Var); + Add (Outputs (7), Exp_Low_Var & ExpD_High_Var & Exp_High_Var); + Add (Outputs (7), Exp_Low_Var & ExpD_Var & Exponent_Term); + Outputs (7) := Disjunct + (Outputs (7).Unify (ExpD_Var, ExpD_High_Var), + LT (Outputs (7), ExpD_Var & ExpD_High_Var)); + + Outputs (7).Conjunct (Repeated_Multiply_Access, + Base_Term & ExpD_Var & Base_ExpD_Var); + Multiply (Outputs (7), Base_Exp_Low_Var & Base_ExpD_Var & Base_Exp_Var); + Multiply (Outputs (7), Base_Term & Base_Exp_Var & Base_Exp1_Var); + Add (Outputs (7), Base_Exp_Var & Remainder_Term & Power_Term); + LT (Outputs (7), Power_Term & Base_Exp1_Var); + end; + return Disjunct (Outputs); + end Logarithm; + + + procedure Logarithm + (This : in out Goal; + Inputs : in Term_Array) is + begin + This := Logarithm (This, Inputs); + end Logarithm; + + + + -- exp2 -- + + function Exp_Two + (This : in Goal; + Inputs : in Term_Array) + return Goal + is + Power_Term : Term renames Inputs (1); + Base_Term : Term renames Inputs (2); + Exponent_Term : Term renames Inputs (3); + + One, Two, Three, Four : Goal := This; + begin + One.Unify (Power_Term, One_Term); + One.Unify (Exponent_Term, Zero_Term); + + GT_One (Two, Power_Term); + Two.Unify (Exponent_Term, One_Term); + Two.Conjunct (Split_Access, Power_Term & Base_Term & Two.Fresh & One_Term); + + declare + Exp1_Var : constant Term := Three.Fresh; + Base2_Var : constant Term := Three.Fresh; + begin + Three.Unify (Exponent_Term, T (T (Zero_Element), Exp1_Var)); + GT_Zero (Three, Exp1_Var); + LT_Length (Three, Base_Term & Power_Term); + Three.Append (Base_Term & T (T (One_Element), Base_Term) & Base2_Var); + Three.Conjunct (Exp_Two_Access, Power_Term & Base2_Var & Exp1_Var); + end; + + declare + Exp1_Var : constant Term := Four.Fresh; + Power_High_Var : constant Term := Four.Fresh; + Base2_Var : constant Term := Four.Fresh; + S_Var : constant Term := Four.Fresh; + begin + Four.Unify (Exponent_Term, T (T (One_Element), Exp1_Var)); + GT_Zero (Four, Exp1_Var); + GT_Zero (Four, Power_High_Var); + Four.Conjunct (Split_Access, Power_Term & Base_Term & S_Var & Power_High_Var); + Four.Append (Base_Term & T (T (One_Element), Base_Term) & Base2_Var); + Four.Conjunct (Exp_Two_Access, Power_High_Var & Base2_Var & Exp1_Var); + end; + + return Disjunct (One & Two & Three & Four); + end Exp_Two; + + + procedure Exp_Two + (This : in out Goal; + Inputs : in Term_Array) is + begin + This := Exp_Two (This, Inputs); + end Exp_Two; + + + + -- expo -- + + function Exponential + (This : in Goal; + Inputs : in Term_Array) + return Goal + is + begin + return Logarithm (This, Inputs (3) & Inputs (1) & Inputs (2) & Zero_Term); + end Exponential; + + + procedure Exponential + (This : in out Goal; + Inputs : in Term_Array) is + begin + This := Exponential (This, Inputs); + end Exponential; + + + -- repeated-mul -- function Repeated_Multiply @@ -774,7 +1147,7 @@ package body Kompsos.Math is is Base_Term : Term renames Inputs (1); Exponent_Term : Term renames Inputs (2); - Product_Term : Term renames Inputs (3); + Power_Term : Term renames Inputs (3); One, Two, Three : Goal := This; @@ -783,15 +1156,15 @@ package body Kompsos.Math is begin GT_Zero (One, Base_Term); One.Unify (Exponent_Term, Zero_Term); - One.Unify (Product_Term, One_Term); + One.Unify (Power_Term, One_Term); Two.Unify (Exponent_Term, One_Term); - Two.Unify (Base_Term, Product_Term); + Two.Unify (Base_Term, Power_Term); GT_One (Three, Exponent_Term); Subtract (Three, Exponent_Term & One_Term & New_Exponent); Three.Conjunct (Repeated_Multiply_Access, Base_Term & New_Exponent & Partial_Product); - Multiply (Three, Partial_Product & Base_Term & Product_Term); + Multiply (Three, Partial_Product & Base_Term & Power_Term); return Disjunct (One & Two & Three); end Repeated_Multiply; diff --git a/src/kompsos-math.ads b/src/kompsos-math.ads index 093acbf..49f5f8f 100644 --- a/src/kompsos-math.ads +++ b/src/kompsos-math.ads @@ -287,15 +287,65 @@ package Kompsos.Math is with Pre => Inputs'Length = 3; + -- /o -- + -- Inputs = N_Term & M_Term & Quotient_Term & Remainder_Term + function Divide + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 4; + + -- Inputs = N_Term & M_Term & Quotient_Term & Remainder_Term + procedure Divide + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 4; + + + -- logo -- + -- Finds solutions to + -- Base^Exponent + Remainder = Power + -- or rather + -- log_Base (Power - Remainder) = Exponent + + -- Inputs = Power_Term & Base_Term & Exponent_Term & Remainder_Term + function Logarithm + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 4; + + -- Inputs = Power_Term & Base_Term & Exponent_Term & Remainder_Term + procedure Logarithm + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 4; + + + -- expo -- + -- Inputs = Base_Term & Exponent_Term & Power_Term + function Exponential + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 3; + + -- Inputs = Base_Term & Exponent_Term & Power_Term + procedure Exponential + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 3; + + -- repeated-mul -- - -- Inputs = Base_Term & Exponent_Term & Product_Term + -- Inputs = Base_Term & Exponent_Term & Power_Term function Repeated_Multiply (This : in Goal; Inputs : in Term_Array) return Goal with Pre => Inputs'Length = 3; - -- Inputs = Base_Term & Exponent_Term & Product_Term + -- Inputs = Base_Term & Exponent_Term & Power_Term procedure Repeated_Multiply (This : in out Goal; Inputs : in Term_Array) @@ -377,6 +427,38 @@ private with Pre => Inputs'Length = 4; + + -- splito -- + -- Inputs = N_Term & Remainder_Term & Low_Term & High_Term + function Split + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 4; + + -- Inputs = N_Term & Remainder_Term & Low_Term & High_Term + procedure Split + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 4; + + + + -- exp2 -- + -- Inputs = Power_Term & Base_Term & Exponent_Term + function Exp_Two + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 3; + + -- Inputs = Power_Term & Base_Term & Exponent_Term + procedure Exp_Two + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 3; + + end Kompsos.Math; -- cgit