From 83b170a6d7842843b22c08e7be89e98ac3fc1712 Mon Sep 17 00:00:00 2001 From: Johan Wiltink Date: Wed, 27 Apr 2022 00:49:26 +0200 Subject: [PATCH] #91, #92 export Primitive config.enforceBinaryScottInvariant toInt.BinaryScott: enforce invariant --- src/lambda-calculus.js | 13 ++++++- tests/basics-binary-scott/solution.txt | 52 +++++++++++++++----------- tests/basics-binary-scott/test.js | 42 +++++++++++---------- 3 files changed, 63 insertions(+), 44 deletions(-) diff --git a/src/lambda-calculus.js b/src/lambda-calculus.js index bc7aeb9..f1decf8 100644 --- 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( "" ), new Env([[ "" , function*() { while ( true ) yield v; } () ]])); } +export function Primitive(v) { return new Tuple(new V( "" ), new Env([[ "" , 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 index 3c18042..de9984f 100644 --- 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,26 +77,27 @@ 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))) @@ -102,7 +105,7 @@ testBit = \ i n . isZero i 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 index 48a31da..b7b1124 100644 --- 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 ); } });