Skip to content

Commit f947fda

Browse files
KacarottKacarott
authored
Merge pull request #93 from JohanWiltink/main
#91, #92
2 parents 451ee10 + 83b170a commit f947fda

File tree

3 files changed

+63
-44
lines changed

3 files changed

+63
-44
lines changed

‎src/lambda-calculus.js

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ Kacarott - https://github.com/Kacarott
1919
const config = { verbosity: "Calm" // Calm | Concise | Loquacious | Verbose
2020
, purity: "PureLC" // Let | LetRec | PureLC
2121
, numEncoding: "None" // None | Church | Scott | BinaryScott
22+
, enforceBinaryScottInvariant: true // Boolean
2223
};
2324

2425
export function configure(cfg={}) { return Object.assign(config,cfg); }
@@ -93,7 +94,7 @@ class Tuple {
9394
}
9495

9596
// Used to insert an external (JS) value into evaluation manually ( avoiding implicit number conversion )
96-
function Primitive(v) { return new Tuple(new V( "<primitive>" ), new Env([[ "<primitive>" , function*() { while ( true ) yield v; } () ]])); }
97+
export function Primitive(v) { return new Tuple(new V( "<primitive>" ), new Env([[ "<primitive>" , function*() { while ( true ) yield v; } () ]])); }
9798

9899
const primitives = new Env;
99100
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) {
130131
return config.numEncoding.fromInt(n); // Custom encoding
131132
}
132133

134+
const isPadded = n => n (false) ( z => z (true) ( () => isPadded(z) ) ( () => isPadded(z) ) ) (isPadded) ; // check invariant for BinaryScott number
135+
133136
export function toInt(term) {
134137
try {
135138
if ( config.numEncoding === "Church" ) {
@@ -142,16 +145,22 @@ export function toInt(term) {
142145
term ( () => evaluating = false ) ( n => () => { term = n; result++ } ) ();
143146
return result;
144147
} else if ( config.numEncoding === "BinaryScott" ) {
148+
const throwOnPadding = config.enforceBinaryScottInvariant && isPadded(term);
145149
let result = 0, bit = 1, evaluating = true;
146150
while ( evaluating )
147151
term ( () => evaluating = false ) ( n => () => { term = n; bit *= 2 } ) ( n => () => { term = n; result += bit; bit *= 2 } ) ();
152+
if ( throwOnPadding ) {
153+
if ( config.verbosity >= "Concise" ) console.error(`toInt: Binary Scott number ${ result } has zero-padding`);
154+
throw new TypeError(`toInt: Binary Scott number violates invariant`);
155+
}
148156
return result;
149157
} else if ( config.numEncoding === "None" )
150158
return term;
151159
else
152160
return config.numEncoding.toInt(term); // Custom encoding
153161
} catch (e) {
154-
if ( config.verbosity >= "Concise" ) console.error(`toInt: ${ term } is not a number in numEncoding ${ config.numEncoding }`);
162+
if ( ! e.message.startsWith("toInt:") && config.verbosity >= "Concise" )
163+
console.error(`toInt: ${ term } is not a number in numEncoding ${ config.numEncoding }`);
155164
throw e;
156165
}
157166
}

‎tests/basics-binary-scott/solution.txt

Lines changed: 30 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -48,17 +48,19 @@ curry = \ fn xy . xy fn
4848

4949
# data Number = End | Even Number | Odd Number
5050

51-
zero = \ end _even _odd . end
51+
# zero = \ end _even _odd . end
5252

5353
shiftR0 = \ n . \ _end even _odd . even n # mind that a shiftR in LE is a multiplication
5454
shiftR1 = \ n . \ _end _even odd . odd n # mind that a shiftR in LE is a multiplication
55-
shiftL = \ n . n n I I # mind that a shiftL in LE is a division
55+
shiftL = \ n . n 0 I I # mind that a shiftL in LE is a division
56+
57+
dbl = \ n . n 0 (K (shiftR0 n)) (K (shiftR0 n))
5658

5759
isStrictZero = \ n . n True (K False) (K False) # disallow padding zeroes # O(1)
5860
isZero = \ n . n True isZero (K False) # allow padding zeroes # amortised O(2), so don't worry too much
5961

60-
pad = \ n . n (shiftR0 zero) (B shiftR0 pad) (B shiftR1 pad)
61-
unpad = \ n . n zero ( \ z . ( \ unpadZ . isStrictZero unpadZ (shiftR0 unpadZ) zero ) (unpad z) ) (B shiftR1 unpad)
62+
pad = \ n . n (shiftR0 0) (B shiftR0 pad) (B shiftR1 pad)
63+
unpad = \ n . n 0 ( \ z . ( \ unpadZ . isStrictZero unpadZ (shiftR0 unpadZ) 0 ) (unpad z) ) (B shiftR1 unpad)
6264
isPadded = \ n . n False ( \ z . z True (K (isPadded z)) (K (isPadded z)) ) isPadded
6365

6466
# instance Ord
@@ -75,34 +77,35 @@ gt = \ m n . compare m n False False True
7577

7678
# instance Enum
7779

78-
succ = \ n . n (shiftR1 zero) shiftR1 (B shiftR0 succ)
80+
succ = \ n . n 1 shiftR1 (B shiftR0 succ)
7981

80-
go = \ prefix n . n zero
82+
go = \ prefix n . n 0
8183
(go (B prefix shiftR1))
8284
( \ z . z (prefix z) (K (prefix (shiftR0 z))) (K (prefix (shiftR0 z))) )
83-
pred = go I
85+
pred = go I # allow padding zeroes
86+
pred = \ n . n 0 (B shiftR1 pred) dbl # disallow padding zeroes
8487

8588
# instance Bits
8689

87-
bitAnd = \ m n . m m
88-
( \ zm . n n (B shiftR0 (bitAnd zm)) (B shiftR0 (bitAnd zm)) )
89-
( \ zm . n n (B shiftR0 (bitAnd zm)) (B shiftR1 (bitAnd zm)) )
90+
bitAnd = \ m n . m 0
91+
( \ zm . n 0 (B dbl (bitAnd zm)) (B dbl (bitAnd zm)) )
92+
( \ zm . n 0 (B dbl (bitAnd zm)) (B shiftR1 (bitAnd zm)) )
9093

9194
bitOr = \ m n . m n
9295
( \ zm . n (shiftR0 zm) (B shiftR0 (bitOr zm)) (B shiftR1 (bitOr zm)) )
9396
( \ zm . n (shiftR1 zm) (B shiftR1 (bitOr zm)) (B shiftR1 (bitOr zm)) )
9497

9598
bitXor = \ m n . m n
96-
( \ zm . n (shiftR0 zm) (B shiftR0 (bitXor zm)) (B shiftR1 (bitXor zm)) )
97-
( \ zm . n (shiftR1 zm) (B shiftR1 (bitXor zm)) (B shiftR0 (bitXor zm)) )
99+
( \ zm . n ( dbl zm) (B dbl (bitXor zm)) (B shiftR1 (bitXor zm)) )
100+
( \ zm . n (shiftR1 zm) (B shiftR1 (bitXor zm)) (B dbl (bitXor zm)) )
98101

99102
testBit = \ i n . isZero i
100103
(n False (testBit (pred i)) (testBit (pred i)))
101104
(n False (K False) (K True))
102105

103106
bit = \ i . isZero i (shiftR0 (bit (pred i))) (succ i)
104107

105-
popCount = \ n . n n popCount (B succ popCount)
108+
popCount = \ n . n 0 popCount (B succ popCount)
106109

107110
even = \ n . n True (K True) (K False)
108111
odd = \ n . n False (K False) (K True)
@@ -113,32 +116,37 @@ plus = \ m n . m n
113116
( \ zm . n (shiftR0 zm) (B shiftR0 (plus zm)) (B shiftR1 (plus zm)) )
114117
( \ zm . n (shiftR1 zm) (B shiftR1 (plus zm)) (B shiftR0 (B succ (plus zm))) )
115118

116-
times = \ m n . m m
117-
( \ zm . n n
119+
times = \ m n . m 0
120+
( \ zm . n 0
118121
( \ zn . shiftR0 (shiftR0 (times zm zn)) )
119122
( \ zn . shiftR0 (times zm (shiftR1 zn)) )
120123
)
121-
( \ zm . n n
124+
( \ zm . n 0
122125
( \ zn . shiftR0 (times (shiftR1 zm) zn) )
123126
( \ zn . plus (shiftR1 zn) (shiftR0 (times zm (shiftR1 zn))) )
124127
)
125128

126-
unsafeMinus = \ m n . m zero
129+
unsafeMinus = \ m n . m 0
127130
( \ zm . n (shiftR0 zm) (B shiftR0 (unsafeMinus zm)) (B shiftR1 (B pred (unsafeMinus zm))) )
128131
( \ zm . n (shiftR1 zm) (B shiftR1 (unsafeMinus zm)) (B shiftR0 (unsafeMinus zm)) )
129132
# needs explicit unpad or will litter padding
130-
minus = \ m n . gt m n zero (unpad (unsafeMinus m n))
133+
minus = \ m n . gt m n 0 (unpad (unsafeMinus m n))
134+
# this should solve the littering
135+
go = \ m n . m 0
136+
( \ zm . n m (B dbl (go zm)) (B shiftR1 (B pred (go zm))) )
137+
( \ zm . n m (B shiftR1 (go zm)) (B dbl (go zm)) )
138+
minus = \ m n . gt m n 0 (go m n)
131139

132140
until = \ p fn x . p x (until p fn (fn x)) x
133-
divMod = \ m n . until (B (lt m) snd) (bimap succ shiftR0) (Pair zero n)
141+
divMod = \ m n . until (B (lt m) snd) (bimap succ shiftR0) (Pair 0 n)
134142
\ steps nn . isZero steps
135143
(divMod (minus m (shiftL nn)) n (B Pair (plus (bit (pred steps)))))
136-
(Pair zero m)
144+
(Pair 0 m)
137145
div = \ m n . fst (divMod m n)
138146
mod = \ m n . snd (divMod m n)
139147

140148
square = W times
141-
pow = \ m n . n (shiftR1 zero)
149+
pow = \ m n . n 1
142150
(B square (pow m))
143151
(B (times m) (B square (pow m)))
144152

@@ -152,7 +160,7 @@ gcd = \ m n . m n
152160
(gcd (minus m n) n)
153161
)
154162
)
155-
lcm = \ m n . ( \ g . isZero g (times (div m g) n) g ) (gcd m n)
163+
lcm = \ m n . T (gcd m n) \ g . isZero g (times (div m g) n) g
156164

157165
min = \ m n . le m n n m
158166
max = \ m n . le m n m n

‎tests/basics-binary-scott/test.js

Lines changed: 22 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ const {fromInt,toInt} = LC;
1111
const {False,True,not,and,or,xor,implies} = solution;
1212
const {LT,EQ,GT,compare,lt,le,eq,ge,gt} = solution;
1313
const {Pair,fst,snd,first,second,both,bimap,curry} = solution;
14-
const {zero,shiftR0,shiftR1,shiftL,isStrictZero,isZero,pad,unpad,isPadded} = solution;
14+
const {shiftR0,shiftR1,shiftL,dbl,isStrictZero,isZero,pad,unpad,isPadded} = solution;
1515
const {succ,pred} = solution;
1616
const {bitAnd,bitOr,bitXor,testBit,bit,popCount,even,odd} = solution;
1717
const {plus,times,minus,divMod,div,mod,pow,gcd,lcm,min,max} = solution;
@@ -26,11 +26,12 @@ describe("Binary Scott tests",function(){
2626
this.timeout(0);
2727
it("enumeration",()=>{
2828
LC.configure({ purity: "LetRec", numEncoding: "BinaryScott" });
29-
const one = succ(zero)
30-
const two = succ(one)
31-
const three = succ(two)
32-
const four = succ(three)
33-
const five = succ(four)
29+
const zero = end => _odd => _even => end ;
30+
const one = succ(zero);
31+
const two = succ(one);
32+
const three = succ(two);
33+
const four = succ(three);
34+
const five = succ(four);
3435
assert.equal( toString(zero), "$" );
3536
assert.equal( toString(one), "1$" );
3637
assert.equal( toString(two), "01$" );
@@ -39,10 +40,10 @@ describe("Binary Scott tests",function(){
3940
assert.equal( toString(five), "101$" );
4041
assert.equal( toString(five), "101$" );
4142
assert.equal( toString(pred(five)), "001$" );
42-
assert.equal( toString(unpad(pred(pred(five)))), "11$" );
43-
assert.equal( toString(unpad(pred(pred(pred(five))))), "01$" );
44-
assert.equal( toString(unpad(pred(pred(pred(pred(five)))))), "1$" );
45-
assert.equal( toString(unpad(pred(pred(pred(pred(pred(five))))))), "$" );
43+
assert.equal( toString(pred(pred(five))), "11$" );
44+
assert.equal( toString(pred(pred(pred(five)))), "01$" );
45+
assert.equal( toString(pred(pred(pred(pred(five))))), "1$" );
46+
assert.equal( toString(pred(pred(pred(pred(pred(five)))))), "$" );
4647
});
4748
it("successor",()=>{
4849
let n = 0;
@@ -58,15 +59,16 @@ describe("Binary Scott tests",function(){
5859
assert.equal( n, i );
5960
}
6061
});
61-
it("predecessor robustness",()=>{
62-
assert.equal( toString( pred ( 2 ) ), "1$" );
63-
assert.equal( toString( pred ( end => even => odd => end ) ), "$" );
64-
assert.equal( toString( pred ( end => even => odd => even (
65-
end => even => odd => end ) ) ), "$" );
66-
assert.equal( toString( pred ( end => even => odd => even (
67-
end => even => odd => even (
68-
end => even => odd => end ) ) ) ), "$" );
69-
});
62+
// enforcing the invariant means pred robustness is overrated
63+
// it("predecessor robustness",()=>{
64+
// assert.equal( toString( pred ( 2 ) ), "1$" );
65+
// assert.equal( toString( pred ( end => even => odd => end ) ), "$" );
66+
// assert.equal( toString( pred ( end => even => odd => even (
67+
// end => even => odd => end ) ) ), "$" );
68+
// assert.equal( toString( pred ( end => even => odd => even (
69+
// end => even => odd => even (
70+
// end => even => odd => end ) ) ) ), "$" );
71+
// });
7072
it("ordering",()=>{
7173
for ( let i=1; i<=100; i++ ) {
7274
const m = rnd(i*i), n = rnd(i*i);
@@ -144,7 +146,7 @@ describe("Binary Scott tests",function(){
144146
for ( let i=1; i<=100; i++ ) {
145147
const n = rnd(i*i);
146148
assert.equal( shiftL (n), n >> 1 );
147-
assert.equal( shiftR0 (n), n << 1 );
149+
assert.equal( dbl (n), n << 1 );
148150
assert.equal( shiftR1 (n), n << 1 | 1 );
149151
}
150152
});

0 commit comments

Comments
 (0)