diff --git a/src/lambda-calculus.js b/src/lambda-calculus.js index f1decf8..3c414ef 100644 --- a/src/lambda-calculus.js +++ b/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 ) { diff --git a/tests/negabinary-scott/solution.lc b/tests/negabinary-scott/solution.lc new file mode 100644 index 0000000..3ee4247 --- /dev/null +++ b/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 diff --git a/tests/negabinary-scott/test.js b/tests/negabinary-scott/test.js new file mode 100644 index 0000000..cd6d915 --- /dev/null +++ b/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 }`); + } + }); +}); \ No newline at end of file