Merge pull request #94 from JohanWiltink/main

custom NegaBinary numbers, plus necessary bugfixes

Author: Kacarott

src/lambda-calculus.js

@@ -58,7 +58,7 @@ class A {
     this.left = left;
     this.right = right;
   }
-  free() { return union(this.left.free(),this.right.free()); }
+  free() { return union( this.left.free?.() || [] , this.right.free?.() || [] ); }
   toString() {
     const left = this.left instanceof L ? `(${this.left})` : this.left ;
     const right = this.right instanceof V ? this.right : `(${this.right})` ;
@@ -271,7 +271,7 @@ function parse(code) {
     function a(i) {
       let q, r = [];
       let j = i;
-      while ( q = paren_d(term)(j) || l(j) || v(j) || n(j) ) {
+      while ( q = paren_d(term)(j) || l(j) || v(j) || n(j) || negative(n)(j) ) {
         [j,q] = q;
         r.push(q);
       }
@@ -280,6 +280,18 @@ function parse(code) {
       else
         return null;
     }
+    const negative = number => function(i) {
+      const j = expect('-')(i);
+      if ( j ) {
+        const q = number(j);
+        if ( q ) {
+          const [k,r] = q;
+          return [k,fromInt(-toInt(r))];
+        } else
+          error(j,"negative: expected a number literal")
+      } else
+        return null;
+    }
     const paren_d = inner => function(i) {
       const j = expect('(')(i);
       if ( j ) {

tests/negabinary-scott/solution.lc

@@ -0,0 +1,91 @@
+#debug
+
+#import combinators.lc
+B = \ f g x . f (g x)
+C = \ f x y . f y x
+K = \ x _ . x
+T = \ x f . f x
+Y = \ f . ( \ x . f (x x) ) ( \ x . f (x x) )
+
+#import church-boolean.lc
+True  = \ true _false . true
+False = \ _true false . false
+
+#import church-ordering.lc
+LT = \ lt _eq _gt . lt
+EQ = \ _lt eq _gt . eq
+GT = \ _lt _eq gt . gt
+
+#import scott-pair.lc
+Pair = \ x y f . f x y
+fst = \ xy . xy \ x _y . x
+snd = \ xy . xy \ _x y . y
+bimap = \ fn xy . xy \ x y . Pair (fn x) (fn y)
+Y2 = B Y (C (B bimap T))
+
+#import scott-triple.lc
+Triple = \ x y z f . f x y z
+fst3 = \ xyz . xyz \ x _y _z . x
+snd3 = \ xyz . xyz \ _x y _z . y
+thd3 = \ xyz . xyz \ _x _y z . z
+trimap = \ fn xyz . xyz \ x y z . Triple (fn x) (fn y) (fn z)
+Y3 = B Y (C (B trimap T))
+
+#import scott-quad.lc
+Quad = \ w x y z f . f w x y z
+fst4 = \ wxyz . wxyz \ w _x _y _z . w
+snd4 = \ wxyz . wxyz \ _w x _y _z . x
+thd4 = \ wxyz . wxyz \ _w _x y _z . y
+fth4 = \ wxyz . wxyz \ _w _x _y z . z
+quadmap = \ fn wxyz . wxyz \ w x y z . Quad (fn w) (fn x) (fn y) (fn z)
+Y4 = B Y (C (B quadmap T))
+
+#export scott-negabinary-number.lc
+
+# NegaBinary = Zero | Bit0 NegaBinary | Bit1 NegaBinary
+
+Bit0 = \ n . \ _end even _odd . even n
+Bit1 = \ n . \ _end _even odd . odd  n
+
+nega-dbl = \ n . n 0 (K (Bit0 n)) (K (Bit0 n))
+
+Enum = Y2 (Pair (T \ succ pred . \ m . m  1 Bit1 (B nega-dbl pred)) # succ
+                (T \ succ pred . \ m . m -1 (B Bit1 succ) nega-dbl) # pred
+          )
+succ = fst Enum
+pred = snd Enum
+
+Num = Y3 (Triple (T \ add adc adb .
+                    \ m n . m n        # add
+                              ( \ zm . n m ( \ zn . nega-dbl (add zm zn) ) ( \ zn . Bit1 (add zm zn) ) )
+                              ( \ zm . n m ( \ zn . Bit1 (add zm zn) ) ( \ zn . nega-dbl (adb zm zn) ) )
+                 )
+                 (T \ add adc adb .
+                    \ m n . m (succ n) # add-with-carry
+                              ( \ zm . n (succ m) ( \ zn . Bit1 (add zm zn) ) ( \ zn . nega-dbl (adb zm zn) ) )
+                              ( \ zm . n (succ m) ( \ zn . nega-dbl (adb zm zn) ) ( \ zn . Bit1 (adb zm zn) ) )
+                 )
+                 (T \ add adc adb .
+                    \ m n . m (pred n) # add-with-borrow
+                              ( \ zm . n (pred m) ( \ zn . Bit1 (adc zm zn) ) ( \ zn . nega-dbl (add zm zn) ) )
+                              ( \ zm . n (pred m) ( \ zn . nega-dbl (add zm zn) ) ( \ zn . Bit1 (add zm zn) ) )
+         )       )
+add = fst3 Num
+adc = snd3 Num
+adb = thd3 Num
+
+negate = \ n . add n (nega-dbl n)
+sub = \ m n . add m (negate n)
+zero = \ n . n True (K False) (K False)
+
+Ord = Y4 (Quad (T \ lt0 le0 ge0 gt0 . \ n . n False gt0 gt0) # lt0
+               (T \ lt0 le0 ge0 gt0 . \ n . n True  ge0 gt0) # le0
+               (T \ lt0 le0 ge0 gt0 . \ n . n True  le0 le0) # ge0
+               (T \ lt0 le0 ge0 gt0 . \ n . n False lt0 le0) # gt0
+         )
+lt0 = fst4 Ord
+le0 = snd4 Ord
+ge0 = thd4 Ord
+gt0 = fth4 Ord
+
+compare = \ m n . T (sub m n) \ d . zero d EQ (lt0 d LT GT) # church boolean

tests/negabinary-scott/test.js

@@ -0,0 +1,77 @@
+import {readFileSync} from "fs";
+import {assert} from "chai";
+
+import * as LC from "../../src/lambda-calculus.js";
+
+const Zero =      end => even => odd => end ;
+const Bit0 = n => end => even => odd => even(n) ;
+const Bit1 = n => end => even => odd => odd (n) ;
+const fromInt = n => n ? n&1 ? Bit1(fromInt(-(n>>1))) : Bit0(fromInt(-(n>>1))) : Zero ;
+const padded = m => m (false) ( n => n (true) ( () => padded(n) ) (padded) ) (padded) ;
+const unsafeToInt = m => m (0) ( n => - 2 * unsafeToInt(n) ) ( n => 1 - 2 * unsafeToInt(n) ) ;
+const toInt = n => {
+  if ( padded(n) )
+    throw new TypeError(`toInt: padded number ${ unsafeToInt(n) }`);
+  else
+    return unsafeToInt(n);
+} ;
+LC.configure({ purity: "LetRec", numEncoding: { fromInt, toInt }, verbosity: "Concise" });
+
+const solutionText = readFileSync(new URL("./solution.lc", import.meta.url), {encoding: "utf8"});
+const solution = LC.compile(solutionText);
+const { succ,pred, add,negate,sub, zero, lt0,le0,ge0,gt0,compare } = solution;
+const { True,False, LT,EQ,GT } = solution;
+
+const toBoolean = p => p (true) (false) ;
+const toOrdering = cmp => cmp ("LT") ("EQ") ("GT") ;
+
+describe("NegaBinaryScott", () => {
+  it("numbers", () => {
+    for ( let n=-10; n<=10; n++ )
+      assert.strictEqual( toInt(fromInt(n)), n, `toInt (fromInt ${ n })` );
+  });
+  it("succ", () => {
+    for ( let n=-10; n<=10; n++ )
+      assert.strictEqual( toInt(succ(fromInt(n))), n+1, `succ ${ n }` );
+      // assert.strictEqual( toInt(pred(fromInt(n))), n-1, `pred ${ n }` );
+  });
+  it("pred", () => {
+    for ( let n=-10; n<=10; n++ )
+      // assert.strictEqual( toInt(succ(fromInt(n))), n+1, `succ ${ n }` ),
+      assert.strictEqual( toInt(pred(fromInt(n))), n-1, `pred ${ n }` );
+  });
+  it("add", () => {
+    for ( let m=-10; m<=10; m++ )
+      for ( let n=-10; n<=10; n++ ) {
+        const actual = toInt(add(fromInt(m))(fromInt(n)));
+        assert.strictEqual(actual,m+n,`add ${ m } ${ n }`);
+      }
+  });
+  it("negate", () => {
+    for ( let n=-10; n<=10; n++ )
+      assert.strictEqual( toInt(negate(fromInt(n))), -n, `negate ${ n }` );
+  });
+  it("sub", () => {
+    for ( let m=-10; m<=10; m++ )
+      for ( let n=-10; n<=10; n++ ) {
+        const actual = toInt(sub(fromInt(m))(fromInt(n)));
+        assert.strictEqual(actual,m-n,`sub ${ m } ${ n }`);
+      }
+  });
+  it("eq, uneq", () => {
+    for ( let n=-10; n<=10; n++ )
+      assert.equal(toBoolean(zero(fromInt(n))),n===0,`zero ${ n }`),
+      assert.equal(toBoolean(lt0(fromInt(n))),n<0,`lt0 ${ n }`),
+      assert.equal(toBoolean(le0(fromInt(n))),n<=0,`le0 ${ n }`),
+      assert.equal(toBoolean(ge0(fromInt(n))),n>=0,`ge0 ${ n }`),
+      assert.equal(toBoolean(gt0(fromInt(n))),n>0,`gt0 ${ n }`);
+  });
+  it("compare", () => {
+    for ( let m=-10; m<=10; m++ )
+      for ( let n=-10; n<=10; n++ ) {
+        const actual = toOrdering(compare(fromInt(m))(fromInt(n)));
+        const expected = m > n ? "GT" : m < n ? "LT" : "EQ" ;
+        assert.equal(actual,expected,`compare ${ m } ${ n }`);
+      }
+  });
+});