Merge pull request #93 from JohanWiltink/main

Kacarott · web-flow · commit f947fda35b2d · 2022-04-27T01:09:08.000+02:00
#91, #92
diff --git a/src/lambda-calculus.js b/src/lambda-calculus.js
@@ -19,6 +19,7 @@ Kacarott - https://github.com/Kacarott
 const config = { verbosity: "Calm"    //  Calm | Concise | Loquacious | Verbose
                , purity: "PureLC"     //  Let | LetRec | PureLC
                , numEncoding: "None"  //  None | Church | Scott | BinaryScott
+               , enforceBinaryScottInvariant: true  //  Boolean
                };
 
 export function configure(cfg={}) { return Object.assign(config,cfg); }
@@ -93,7 +94,7 @@ class Tuple {
 }
 
 // Used to insert an external (JS) value into evaluation manually ( avoiding implicit number conversion )
-function Primitive(v) { return new Tuple(new V( "<primitive>" ), new Env([[ "<primitive>" , function*() { while ( true ) yield v; } () ]])); }
+export function Primitive(v) { return new Tuple(new V( "<primitive>" ), new Env([[ "<primitive>" , function*() { while ( true ) yield v; } () ]])); }
 
 const primitives = new Env;
 primitives.setThunk( "trace", new Tuple( Primitive( function(v) { console.info(String(v.term)); return v; } ), new Env ) );
@@ -130,6 +131,8 @@ export function fromInt(n) {
     return config.numEncoding.fromInt(n); // Custom encoding
 }
 
+const isPadded = n => n (false) ( z => z (true) ( () => isPadded(z) ) ( () => isPadded(z) ) ) (isPadded) ; // check invariant for BinaryScott number
+
 export function toInt(term) {
   try {
     if ( config.numEncoding === "Church" ) {
@@ -142,16 +145,22 @@ export function toInt(term) {
         term ( () => evaluating = false ) ( n => () => { term = n; result++ } ) ();
       return result;
     } else if ( config.numEncoding === "BinaryScott" ) {
+      const throwOnPadding = config.enforceBinaryScottInvariant && isPadded(term);
       let result = 0, bit = 1, evaluating = true;
       while ( evaluating )
         term ( () => evaluating = false ) ( n => () => { term = n; bit *= 2 } ) ( n => () => { term = n; result += bit; bit *= 2 } ) ();
+      if ( throwOnPadding ) {
+        if ( config.verbosity >= "Concise" ) console.error(`toInt: Binary Scott number ${ result } has zero-padding`);
+        throw new TypeError(`toInt: Binary Scott number violates invariant`);
+      }
       return result;
     } else if ( config.numEncoding === "None" )
       return term;
     else
       return config.numEncoding.toInt(term); // Custom encoding
   } catch (e) {
-    if ( config.verbosity >= "Concise" ) console.error(`toInt: ${ term } is not a number in numEncoding ${ config.numEncoding }`);
+    if ( ! e.message.startsWith("toInt:") && config.verbosity >= "Concise" )
+      console.error(`toInt: ${ term } is not a number in numEncoding ${ config.numEncoding }`);
     throw e;
   }
 }
diff --git a/tests/basics-binary-scott/solution.txt b/tests/basics-binary-scott/solution.txt
@@ -48,17 +48,19 @@ curry  = \ fn xy  . xy fn
 
 # data Number = End | Even Number | Odd Number
 
-zero = \ end _even _odd . end
+# zero = \ end _even _odd . end
 
 shiftR0 = \ n . \ _end even _odd . even n # mind that a shiftR in LE is a multiplication
 shiftR1 = \ n . \ _end _even odd . odd  n # mind that a shiftR in LE is a multiplication
-shiftL  = \ n . n n I I                   # mind that a shiftL in LE is a division
+shiftL  = \ n . n 0 I I                   # mind that a shiftL in LE is a division
+
+dbl = \ n . n 0 (K (shiftR0 n)) (K (shiftR0 n))
 
 isStrictZero = \ n . n True (K False) (K False) # disallow padding zeroes # O(1)
 isZero       = \ n . n True    isZero (K False) #    allow padding zeroes # amortised O(2), so don't worry too much
 
-pad = \ n . n (shiftR0 zero) (B shiftR0 pad) (B shiftR1 pad)
-unpad = \ n . n zero ( \ z . ( \ unpadZ . isStrictZero unpadZ (shiftR0 unpadZ) zero ) (unpad z) ) (B shiftR1 unpad)
+pad = \ n . n (shiftR0 0) (B shiftR0 pad) (B shiftR1 pad)
+unpad = \ n . n 0 ( \ z . ( \ unpadZ . isStrictZero unpadZ (shiftR0 unpadZ) 0 ) (unpad z) ) (B shiftR1 unpad)
 isPadded = \ n . n False ( \ z . z True (K (isPadded z)) (K (isPadded z)) ) isPadded
 
 # instance Ord
@@ -75,34 +77,35 @@ gt = \ m n . compare m n False False True
 
 # instance Enum
 
-succ = \ n . n (shiftR1 zero) shiftR1 (B shiftR0 succ)
+succ = \ n . n 1 shiftR1 (B shiftR0 succ)
 
-go = \ prefix n . n zero
+go = \ prefix n . n 0
                     (go (B prefix shiftR1))
                     ( \ z . z (prefix z) (K (prefix (shiftR0 z))) (K (prefix (shiftR0 z))) )
-pred = go I
+pred = go I                           #    allow padding zeroes
+pred = \ n . n 0 (B shiftR1 pred) dbl # disallow padding zeroes
 
 # instance Bits
 
-bitAnd = \ m n . m m
-                   ( \ zm . n n (B shiftR0 (bitAnd zm)) (B shiftR0 (bitAnd zm)) )
-                   ( \ zm . n n (B shiftR0 (bitAnd zm)) (B shiftR1 (bitAnd zm)) )
+bitAnd = \ m n . m 0
+                   ( \ zm . n 0 (B dbl (bitAnd zm)) (B     dbl (bitAnd zm)) )
+                   ( \ zm . n 0 (B dbl (bitAnd zm)) (B shiftR1 (bitAnd zm)) )
 
 bitOr = \ m n . m n
                   ( \ zm . n (shiftR0 zm) (B shiftR0 (bitOr zm)) (B shiftR1 (bitOr zm)) )
                   ( \ zm . n (shiftR1 zm) (B shiftR1 (bitOr zm)) (B shiftR1 (bitOr zm)) )
     
 bitXor = \ m n . m n
-    ( \ zm . n (shiftR0 zm) (B shiftR0 (bitXor zm)) (B shiftR1 (bitXor zm)) )
-    ( \ zm . n (shiftR1 zm) (B shiftR1 (bitXor zm)) (B shiftR0 (bitXor zm)) )
+                   ( \ zm . n (    dbl zm) (B     dbl (bitXor zm)) (B shiftR1 (bitXor zm)) )
+                   ( \ zm . n (shiftR1 zm) (B shiftR1 (bitXor zm)) (B     dbl (bitXor zm)) )
 
 testBit = \ i n . isZero i
                     (n False (testBit (pred i)) (testBit (pred i)))
                     (n False (K False)          (K True))
 
 bit = \ i . isZero i (shiftR0 (bit (pred i))) (succ i)
 
-popCount = \ n . n n popCount (B succ popCount)
+popCount = \ n . n 0 popCount (B succ popCount)
 
 even = \ n . n True  (K True)  (K False)
 odd  = \ n . n False (K False) (K True)
@@ -113,32 +116,37 @@ plus = \ m n . m n
                  ( \ zm . n (shiftR0 zm) (B shiftR0 (plus zm)) (B shiftR1 (plus zm)) )
                  ( \ zm . n (shiftR1 zm) (B shiftR1 (plus zm)) (B shiftR0 (B succ (plus zm))) )
 
-times = \ m n . m m
-                ( \ zm . n n
+times = \ m n . m 0
+                ( \ zm . n 0
                            ( \ zn . shiftR0 (shiftR0 (times zm zn)) )
                            ( \ zn . shiftR0 (times zm (shiftR1 zn)) )
                 )
-                ( \ zm . n n
+                ( \ zm . n 0
                            ( \ zn . shiftR0 (times (shiftR1 zm) zn) )
                            ( \ zn . plus (shiftR1 zn) (shiftR0 (times zm (shiftR1 zn))) )
                 )
 
-unsafeMinus = \ m n . m zero
+unsafeMinus = \ m n . m 0
                         ( \ zm . n (shiftR0 zm) (B shiftR0 (unsafeMinus zm)) (B shiftR1 (B pred (unsafeMinus zm))) )
                         ( \ zm . n (shiftR1 zm) (B shiftR1 (unsafeMinus zm)) (B shiftR0 (unsafeMinus zm)) )
 # needs explicit unpad or will litter padding
-minus = \ m n . gt m n zero (unpad (unsafeMinus m n))
+minus = \ m n . gt m n 0 (unpad (unsafeMinus m n))
+# this should solve the littering
+go = \ m n . m 0
+               ( \ zm . n m (B     dbl (go zm)) (B shiftR1 (B pred (go zm))) )
+               ( \ zm . n m (B shiftR1 (go zm)) (B dbl (go zm)) )
+minus = \ m n . gt m n 0 (go m n)
 
 until = \ p fn x . p x (until p fn (fn x)) x
-divMod = \ m n . until (B (lt m) snd) (bimap succ shiftR0) (Pair zero n)
+divMod = \ m n . until (B (lt m) snd) (bimap succ shiftR0) (Pair 0 n)
                  \ steps nn . isZero steps
                                 (divMod (minus m (shiftL nn)) n (B Pair (plus (bit (pred steps)))))
-                                (Pair zero m)
+                                (Pair 0 m)
 div = \ m n . fst (divMod m n)
 mod = \ m n . snd (divMod m n)
 
 square = W times
-pow = \ m n . n (shiftR1 zero)
+pow = \ m n . n 1
                 (B square (pow m))
                 (B (times m) (B square (pow m)))
 
@@ -152,7 +160,7 @@ gcd = \ m n . m n
                                      (gcd (minus m n) n)
                            )
                 )
-lcm = \ m n . ( \ g . isZero g (times (div m g) n) g ) (gcd m n)
+lcm = \ m n . T (gcd m n) \ g . isZero g (times (div m g) n) g
 
 min = \ m n . le m n n m
 max = \ m n . le m n m n
diff --git a/tests/basics-binary-scott/test.js b/tests/basics-binary-scott/test.js
@@ -11,7 +11,7 @@ const {fromInt,toInt} = LC;
 const {False,True,not,and,or,xor,implies} = solution;
 const {LT,EQ,GT,compare,lt,le,eq,ge,gt} = solution;
 const {Pair,fst,snd,first,second,both,bimap,curry} = solution;
-const {zero,shiftR0,shiftR1,shiftL,isStrictZero,isZero,pad,unpad,isPadded} = solution;
+const {shiftR0,shiftR1,shiftL,dbl,isStrictZero,isZero,pad,unpad,isPadded} = solution;
 const {succ,pred} = solution;
 const {bitAnd,bitOr,bitXor,testBit,bit,popCount,even,odd} = solution;
 const {plus,times,minus,divMod,div,mod,pow,gcd,lcm,min,max} = solution;
@@ -26,11 +26,12 @@ describe("Binary Scott tests",function(){
   this.timeout(0);
   it("enumeration",()=>{
     LC.configure({ purity: "LetRec", numEncoding: "BinaryScott" });
-    const one   = succ(zero)
-    const two   = succ(one)
-    const three = succ(two)
-    const four  = succ(three)
-    const five  = succ(four)
+    const zero  = end => _odd => _even => end ;
+    const one   = succ(zero);
+    const two   = succ(one);
+    const three = succ(two);
+    const four  = succ(three);
+    const five  = succ(four);
     assert.equal( toString(zero), "$" );
     assert.equal( toString(one), "1$" );
     assert.equal( toString(two), "01$" );
@@ -39,10 +40,10 @@ describe("Binary Scott tests",function(){
     assert.equal( toString(five), "101$" );
     assert.equal( toString(five), "101$" );
     assert.equal( toString(pred(five)), "001$" );
-    assert.equal( toString(unpad(pred(pred(five)))), "11$" );
-    assert.equal( toString(unpad(pred(pred(pred(five))))), "01$" );
-    assert.equal( toString(unpad(pred(pred(pred(pred(five)))))), "1$" );
-    assert.equal( toString(unpad(pred(pred(pred(pred(pred(five))))))), "$" );
+    assert.equal( toString(pred(pred(five))), "11$" );
+    assert.equal( toString(pred(pred(pred(five)))), "01$" );
+    assert.equal( toString(pred(pred(pred(pred(five))))), "1$" );
+    assert.equal( toString(pred(pred(pred(pred(pred(five)))))), "$" );
   });
   it("successor",()=>{
     let n = 0;
@@ -58,15 +59,16 @@ describe("Binary Scott tests",function(){
       assert.equal( n, i );
     }
   });
-  it("predecessor robustness",()=>{
-    assert.equal( toString( pred ( 2 ) ), "1$" );
-    assert.equal( toString( pred ( end => even => odd => end ) ), "$" );
-    assert.equal( toString( pred ( end => even => odd => even (
-                                   end => even => odd => end ) ) ), "$" );
-    assert.equal( toString( pred ( end => even => odd => even (
-                                   end => even => odd => even (
-                                   end => even => odd => end ) ) ) ), "$" );
-  });
+  // enforcing the invariant means pred robustness is overrated
+  // it("predecessor robustness",()=>{
+  //   assert.equal( toString( pred ( 2 ) ), "1$" );
+  //   assert.equal( toString( pred ( end => even => odd => end ) ), "$" );
+  //   assert.equal( toString( pred ( end => even => odd => even (
+  //                                  end => even => odd => end ) ) ), "$" );
+  //   assert.equal( toString( pred ( end => even => odd => even (
+  //                                  end => even => odd => even (
+  //                                  end => even => odd => end ) ) ) ), "$" );
+  // });
   it("ordering",()=>{
     for ( let i=1; i<=100; i++ ) {
       const m = rnd(i*i), n = rnd(i*i);
@@ -144,7 +146,7 @@ describe("Binary Scott tests",function(){
     for ( let i=1; i<=100; i++ ) {
       const n = rnd(i*i);
       assert.equal( shiftL (n), n >> 1 );
-      assert.equal( shiftR0 (n), n << 1 );
+      assert.equal( dbl (n), n << 1 );
       assert.equal( shiftR1 (n), n << 1 | 1 );
     }
   });
