• R/O
  • HTTP
  • SSH
  • HTTPS

Commit

Tags
No Tags

Frequently used words (click to add to your profile)

javac++androidlinuxc#windowsobjective-cqtcocoa誰得pythonphprubygameguibathyscaphec翻訳計画中(planning stage)omegatframeworktwittertestdomvb.netdirectxbtronarduinopreviewerゲームエンジン

A categorical programming language


Commit MetaInfo

Revision23bcde0c09f26571b9c259618fa2bfdfb0880c99 (tree)
Time2023-02-02 14:41:01
AuthorCorbin <cds@corb...>
CommiterCorbin

Log Message

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.

Change Summary

Incremental Difference

--- a/movelist/cammyo.scm
+++ b/movelist/cammyo.scm
@@ -108,8 +108,8 @@
108108 ((== expr 'not) (not° i o))
109109 ((== expr 'zero) (== i 'star) (zeroo o))
110110 ((== expr 'succ) (succ° i o))
111- ((== expr 'f-zero) (== i 'star) (== o fp-zero+))
112- ((== expr 'f-one) (== i 'star) (== o (build-fp 1.0)))
111+ ((== expr 'f-zero) (== o fp-zero+) (== i 'star))
112+ ((== expr 'f-one) (== o (build-fp 1.0)) (== i 'star))
113113 ((== expr 'f-sign) (== o #t) (fp-sign° i 'pos))
114114 ((== expr 'f-sign) (== o #f) (fp-sign° i 'neg))
115115 ))
--- a/movelist/fp.scm
+++ b/movelist/fp.scm
@@ -8,10 +8,13 @@
88 mini-kanren
99 (only matchable match-lambda)
1010 (only mathh frexp)
11- rels)
11+ rels
12+ (chicken pretty-print))
1213
1314 ; An implementation of relational floating-point arithmetic, as seen in:
1415 ; https://www.cs.toronto.edu/~lczhang/sandre_float2021.pdf
16+ ; Zeroes and infinities are given their own distinct encodings. Otherwise, we
17+ ; follow the paper relatively closely.
1518
1619 ; Like (not (var? x)) but checks entire lists.
1720 (define nat? (match-lambda [(or (0 . n) (1 . n)) (nat? n)] [() #t] [_ #f]))
@@ -26,9 +29,10 @@
2629 [_ #f]))
2730
2831 ; Overall precision.
29- (define exp-precision 2)
30- (define exp-mantissa-factor (expt 2.0 exp-precision))
31- (define exp-bias (- (expt 2 (- exp-precision 1)) 1))
32+ (define exponent-length 3)
33+ (define mantissa-length 4)
34+ (define exp-mantissa-factor (expt 2.0 exponent-length))
35+ (define exp-bias (- (expt 2 (- exponent-length 1)) 1))
3236
3337 ; Convert an inexact number into a relational term.
3438 ; float -> Float
@@ -70,9 +74,15 @@
7074 ; Signed infinities.
7175 (define fp-inf+ '(pos inf))
7276 (define fp-inf- '(neg inf))
77+ (define (fp-inf° f) (conde ((== f fp-inf+)) ((== f fp-inf-))))
78+
79+ ; Natural numbers which are mantissas.
80+ (define (mantissa° m) (lengtho m (build-num mantissa-length)))
81+ (define (mantissa-short° m) (lengtho m (build-num (- mantissa-length 1))))
7382
7483 ; Decompose nonzero finite floating-point numbers.
75- (define (fp-decomp° f s e m) (== f `(,s ,e ,m)))
84+ (define (fp-decomp° f s e m) (== f `(,s ,e ,m))
85+ (conde ((== s 'pos)) ((== s 'neg))) (mantissa° m))
7686
7787 (define (fp-finite° f)
7888 (conde
@@ -80,6 +90,7 @@
8090 ((fresh (s e m) (fp-decomp° f s e m)))))
8191
8292 ; The less-than relation.
93+ ; See p3-4.
8394 (define (fp-<° x y)
8495 (conde
8596 ((== x fp-inf-) (fp-finite° y))
@@ -100,22 +111,18 @@
100111 (define (mantissa-shift° mantissa diff shifted)
101112 (fresh (prefix)
102113 (appendo prefix shifted mantissa)
103- (lengtho shifted diff)))
114+ (lengtho prefix diff)))
104115
105116 ; Natural numbers which are exponents.
106117 (define (exponent° e)
107- (fresh (n) (<=o n (build-num exp-precision)) (lengtho e n)))
108-
109- ; Natural numbers which are mantissas.
110- (define (mantissa° m) (lengtho m (build-num exp-precision)))
111- (define (mantissa-short° m) (lengtho m (build-num (- exp-precision 1))))
118+ (fresh (n) (<=o n (build-num exponent-length)) (lengtho e n)))
112119
113120 ; Trim a mantissa, saving the extra bits.
114121 (define (drop-leastsig-bit° m rm bits)
115122 (fresh () (mantissa° rm) (appendo bits rm m)))
116123
117124 ; XXX this is not correct!
118- (define (fp-overflow° e pm m) succeed)
125+ (define (fp-overflow° e pm m) (== pm m))
119126
120127 ; Helper for addition.
121128 ; See p4-5.
@@ -134,18 +141,20 @@
134141 (conde
135142 ((fp-zero° f1) (== f2 r))
136143 ((fp-zero° f2) (== f1 r))
137- ((== f1 fp-inf+) (== f2 fp-inf+) (== r fp-inf+))
138- ((== f1 fp-inf-) (== f2 fp-inf-) (== r fp-inf-))))
144+ ((== r fp-inf+)
145+ (conde ((== f1 fp-inf+) (fp-finite° f2)) ((fp-finite° f1) (== f2 fp-inf+))))
146+ ((== r fp-inf-)
147+ (conde ((== f1 fp-inf-) (fp-finite° f2)) ((fp-finite° f1) (== f2 fp-inf-))))))
139148 ; XXX typical cases
140149
141150 ; XOR for sign bits.
142151 ; For refutational completeness, this is given as a table.
143152 (define (sign-xor° s1 s2 s3)
144153 (conde
145- ((== s1 'pos) (== s2 'pos) (== s3 'neg))
146- ((== s1 'pos) (== s2 'neg) (== s3 'pos))
147- ((== s1 'neg) (== s2 'pos) (== s3 'pos))
148- ((== s1 'neg) (== s2 'neg) (== s3 'neg))))
154+ ((== s1 'pos) (== s2 'pos) (== s3 'pos))
155+ ((== s1 'pos) (== s2 'neg) (== s3 'neg))
156+ ((== s1 'neg) (== s2 'pos) (== s3 'neg))
157+ ((== s1 'neg) (== s2 'neg) (== s3 'pos))))
149158
150159 ; Add exponents for multiplication.
151160 (define (compute-exp° e1 e2 bits re)
@@ -154,17 +163,19 @@
154163 ((mantissa° bits) (succ° pre-re re))
155164 ((mantissa-short° bits) (== pre-re re)))
156165 (+o e1 e2 esum)
157- (+o exp-bias pre-re re)))
166+ (+o (build-num exp-bias) pre-re esum)))
158167
159168 ; Multiplication.
160169 ; See p6.
161170 (define (fp-*° f1 f2 r)
162171 (fresh (s1 s2 rs)
163172 (sign-xor° s1 s2 rs)
173+ (fp-sign° f1 s1) (fp-sign° f2 s2) (fp-sign° r rs)
164174 (conde
165- ((== f1 `(,s1 zero)) (caro f2 s2) (== r `(,rs zero)))
166- ((caro f1 s1) (== f2 `(,s2 zero)) (== r `(,rs zero)))
167- ; XXX infinities
175+ ((fp-zero° r) (conde ((fp-zero° f1)) ((fp-zero° f2))))
176+ ((fp-inf° r) (conde
177+ ((fp-inf° f1) (fp-finite° f2))
178+ ((fp-finite° f1) (fp-inf° f2))))
168179 ((fresh (e1 m1 e2 m2 re rm)
169180 (fp-decomp° f1 s1 e1 m1)
170181 (fp-decomp° f2 s2 e2 m2)