コミット: 23bcde0c09f26571b9c259618fa2bfdfb0880c99 - cammy (git)

A categorical programming language

コミットメタ情報

• リビジョン: 23bcde0c09f26571b9c259618fa2bfdfb0880c99 (tree)
• 日時: 2023-02-02 14:41:01
• 作者: Corbin <cds@corb...>
• コミッター: Corbin

ログメッセージ

Debug FP multiplication somewhat.

For some reason, ground inputs are not giving a ground output. This
might be an issue with the structure of eval°, but I'm not seeing how.

変更サマリ

• modified: movelist/cammyo.scm
• modified: movelist/fp.scm

差分

--- a/movelist/cammyo.scm
+++ b/movelist/cammyo.scm
@@ -108,8 +108,8 @@
       ((== expr 'not) (not° i o))
       ((== expr 'zero) (== i 'star) (zeroo o))
       ((== expr 'succ) (succ° i o))
-      ((== expr 'f-zero) (== i 'star) (== o fp-zero+))
-      ((== expr 'f-one) (== i 'star) (== o (build-fp 1.0)))
+      ((== expr 'f-zero) (== o fp-zero+) (== i 'star))
+      ((== expr 'f-one) (== o (build-fp 1.0)) (== i 'star))
       ((== expr 'f-sign) (== o #t) (fp-sign° i 'pos))
       ((== expr 'f-sign) (== o #f) (fp-sign° i 'neg))
       ))

--- a/movelist/fp.scm
+++ b/movelist/fp.scm
@@ -8,10 +8,13 @@
           mini-kanren
           (only matchable match-lambda)
           (only mathh frexp)
-          rels)
+          rels
+          (chicken pretty-print))
 
   ; An implementation of relational floating-point arithmetic, as seen in:
   ; https://www.cs.toronto.edu/~lczhang/sandre_float2021.pdf
+  ; Zeroes and infinities are given their own distinct encodings. Otherwise, we
+  ; follow the paper relatively closely.
 
   ; Like (not (var? x)) but checks entire lists.
   (define nat? (match-lambda [(or (0 . n) (1 . n)) (nat? n)] [() #t] [_ #f]))
@@ -26,9 +29,10 @@
       [_ #f]))
 
   ; Overall precision.
-  (define exp-precision 2)
-  (define exp-mantissa-factor (expt 2.0 exp-precision))
-  (define exp-bias (- (expt 2 (- exp-precision 1)) 1))
+  (define exponent-length 3)
+  (define mantissa-length 4)
+  (define exp-mantissa-factor (expt 2.0 exponent-length))
+  (define exp-bias (- (expt 2 (- exponent-length 1)) 1))
   
   ; Convert an inexact number into a relational term.
   ; float -> Float
@@ -70,9 +74,15 @@
   ; Signed infinities.
   (define fp-inf+ '(pos inf))
   (define fp-inf- '(neg inf))
+  (define (fp-inf° f) (conde ((== f fp-inf+)) ((== f fp-inf-))))
+
+  ; Natural numbers which are mantissas.
+  (define (mantissa° m) (lengtho m (build-num mantissa-length)))
+  (define (mantissa-short° m) (lengtho m (build-num (- mantissa-length 1))))
 
   ; Decompose nonzero finite floating-point numbers.
-  (define (fp-decomp° f s e m) (== f `(,s ,e ,m)))
+  (define (fp-decomp° f s e m) (== f `(,s ,e ,m))
+    (conde ((== s 'pos)) ((== s 'neg))) (mantissa° m))
 
   (define (fp-finite° f)
     (conde
@@ -80,6 +90,7 @@
       ((fresh (s e m) (fp-decomp° f s e m)))))
 
   ; The less-than relation.
+  ; See p3-4.
   (define (fp-<° x y)
     (conde
       ((== x fp-inf-) (fp-finite° y))
@@ -100,22 +111,18 @@
   (define (mantissa-shift° mantissa diff shifted)
     (fresh (prefix)
            (appendo prefix shifted mantissa)
-           (lengtho shifted diff)))
+           (lengtho prefix diff)))
 
   ; Natural numbers which are exponents.
   (define (exponent° e)
-    (fresh (n) (<=o n (build-num exp-precision)) (lengtho e n)))
-
-  ; Natural numbers which are mantissas.
-  (define (mantissa° m) (lengtho m (build-num exp-precision)))
-  (define (mantissa-short° m) (lengtho m (build-num (- exp-precision 1))))
+    (fresh (n) (<=o n (build-num exponent-length)) (lengtho e n)))
 
   ; Trim a mantissa, saving the extra bits.
   (define (drop-leastsig-bit° m rm bits)
     (fresh () (mantissa° rm) (appendo bits rm m)))
 
   ; XXX this is not correct!
-  (define (fp-overflow° e pm m) succeed)
+  (define (fp-overflow° e pm m) (== pm m))
 
   ; Helper for addition.
   ; See p4-5.
@@ -134,18 +141,20 @@
     (conde
       ((fp-zero° f1) (== f2 r))
       ((fp-zero° f2) (== f1 r))
-      ((== f1 fp-inf+) (== f2 fp-inf+) (== r fp-inf+))
-      ((== f1 fp-inf-) (== f2 fp-inf-) (== r fp-inf-))))
+      ((== r fp-inf+)
+       (conde ((== f1 fp-inf+) (fp-finite° f2)) ((fp-finite° f1) (== f2 fp-inf+))))
+      ((== r fp-inf-)
+       (conde ((== f1 fp-inf-) (fp-finite° f2)) ((fp-finite° f1) (== f2 fp-inf-))))))
       ; XXX typical cases
 
   ; XOR for sign bits.
   ; For refutational completeness, this is given as a table.
   (define (sign-xor° s1 s2 s3)
     (conde
-      ((== s1 'pos) (== s2 'pos) (== s3 'neg))
-      ((== s1 'pos) (== s2 'neg) (== s3 'pos))
-      ((== s1 'neg) (== s2 'pos) (== s3 'pos))
-      ((== s1 'neg) (== s2 'neg) (== s3 'neg))))
+      ((== s1 'pos) (== s2 'pos) (== s3 'pos))
+      ((== s1 'pos) (== s2 'neg) (== s3 'neg))
+      ((== s1 'neg) (== s2 'pos) (== s3 'neg))
+      ((== s1 'neg) (== s2 'neg) (== s3 'pos))))
 
   ; Add exponents for multiplication.
   (define (compute-exp° e1 e2 bits re)
@@ -154,17 +163,19 @@
              ((mantissa° bits) (succ° pre-re re))
              ((mantissa-short° bits) (== pre-re re)))
            (+o e1 e2 esum)
-           (+o exp-bias pre-re re)))
+           (+o (build-num exp-bias) pre-re esum)))
 
   ; Multiplication.
   ; See p6.
   (define (fp-*° f1 f2 r)
     (fresh (s1 s2 rs)
            (sign-xor° s1 s2 rs)
+           (fp-sign° f1 s1) (fp-sign° f2 s2) (fp-sign° r rs)
            (conde
-             ((== f1 `(,s1 zero)) (caro f2 s2) (== r `(,rs zero)))
-             ((caro f1 s1) (== f2 `(,s2 zero)) (== r `(,rs zero)))
-             ; XXX infinities
+             ((fp-zero° r) (conde ((fp-zero° f1)) ((fp-zero° f2))))
+             ((fp-inf° r) (conde
+                             ((fp-inf° f1) (fp-finite° f2))
+                             ((fp-finite° f1) (fp-inf° f2))))
              ((fresh (e1 m1 e2 m2 re rm)
                      (fp-decomp° f1 s1 e1 m1)
                      (fp-decomp° f2 s2 e2 m2)