Skip to content

#91, #92 #93

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 26, 2022
Merged

#91, #92 #93

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 11 additions & 2 deletions src/lambda-calculus.js
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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); }
Expand Down Expand Up @@ -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 ) );
Expand Down Expand Up @@ -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" ) {
Expand All @@ -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;
}
}
Expand Down
52 changes: 30 additions & 22 deletions tests/basics-binary-scott/solution.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -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)))

Expand All @@ -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
42 changes: 22 additions & 20 deletions tests/basics-binary-scott/test.js
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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$" );
Expand All @@ -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;
Expand All @@ -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);
Expand Down Expand Up @@ -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 );
}
});
Expand Down