lambdaway
::
tromp
6
|
list
|
login
|
load
|
|
{center [[oops7]] | tromp | [[tromp2]]} {uncover http://lambdaway.free.fr/workshop/data/brussels/nef.jpg 100 300 The Sagrada Familia in Barcelona, Antonio Gaudi architect.{br}A deeply nested composition of catenaries, approximated by parabolas.{br}The architectural equivalent of λ-calculus.{br}} ;; {uncover http://villemin.gerard.free.fr/aMaths/ThNb/Peano_fichiers/image024.gif 100 300 [[numbers|http://villemin.gerard.free.fr/aMaths/ThNb/Peano.htm]]} ;; {center [[oops6]] | tromp | [[tromp2]]} _h1 exploring big numbers in λ-calculus ;; _p Sharing ideas with [[John Tromp|https://github.com/tromp]]. See also [[wikipedia|https://en.wikipedia.org/wiki/Multiplication_algorithm]]. _p Breaking the glass ceiling of Church numerals we can compute (inside the web browser) big {b fibonacci & factorial} numbers using binary numbers of variable length at the [[λ-calculus|?view=lambda_calculus]] level, i.e. using [[lambdatalk|?view=coding]] with nothing but two special forms, {b lambda & def}, and without {b if} or {b let} syntactic sugar, except for inputs and outputs. A previous attempt can be seen [[here|?view=oops6]] and in this page I'm working in some improvements after a few advices from [[John Tromp|https://github.com/tromp]]. {pre ;; uncomment to test '{bool2dec {B.FIB 128 {dec2bool 128 100}}} // about 6200ms -> fib(100) = {b 354224848179261915075} '{bool2dec {B.FAC 128 {dec2bool 128 25}}} // about 6200ms -> fac(25) = {b 15511210043330985984000000} '{bool2dec {B.FAC 256 {dec2bool 256 50}}} // about 31500ms -> fac(50) = {b 30414093201713378043612608166064768844377641568960512000000000000} } _h2 B.FIB & B.FAC {pre '{def B.FIB {def B.FIB.rec {lambda {:a :b :c} {{IF {B.ZERO? :c} {lambda {:a :b :c} :a} {lambda {:a :b :c} {B.FIB.rec {B.ADD :a :b} :a {B.PRED :c}}}} :a :b :c}}} {lambda {:n :a} {B.FIB.rec {ZERO :n} {ONE :n} :a}}} -> {def B.FIB {def B.FIB.rec {lambda {:a :b :m} {{IF {B.ZERO? :m} {lambda {:a :b :m} :a} {lambda {:a :b :m} {B.FIB.rec {B.ADD :a :b} :a {B.PRED :m}}}} :a :b :m}}} {lambda {:n :m} {B.FIB.rec {ZERO :n} {ONE :n} :m}}} '{def B.FAC {def B.FAC.rec {lambda {:n :a :b} {{IF {B.ZERO? :a} {lambda {:n :a :b} :b} {lambda {:n :a :b} {B.FAC.rec :n {B.PRED :a} {B.MUL :n :a :b}}}} :n :a :b}}} {lambda {:n :a} {B.FAC.rec :n :a {ONE :n}}}} -> {def B.FAC {def B.FAC.rec {lambda {:n :a :b} {{IF {B.ZERO? :a} {lambda {:n :a :b} :b} {lambda {:n :a :b} {B.FAC.rec :n {B.PRED :a} {B.MUL :n :a :b}}}} :n :a :b}}} {lambda {:n :a} {B.FAC.rec :n :a {ONE :n}}}} } _h2 B.ADD {pre '{def B.ADD {def B.ADD.bit {lambda {:x :a :b} {PAIR {XOR :x {XOR :a :b}} {OR {AND :a :b} {OR {AND :x :a} {AND :x :b}}}}}} {def B.ADD.rec {lambda {:x :a :b} {{IF {OR {NIL? :a} {NIL? :b}} {lambda {:x :a :b} {{lambda {:x} {IF {LEFT :x} :x {RIGHT :x}} } {PAIR :x NIL}}} {lambda {:x :a :b} {{lambda {:x :a :b} {PAIR {LEFT :x} {B.ADD.rec {RIGHT :x} {RIGHT :a} {RIGHT :b}}} } {B.ADD.bit :x {LEFT :a} {LEFT :b}} :a :b}}} :x :a :b }}} {lambda {:a :b} {B.ADD.rec #0 :a :b }}} -> {def B.ADD {def B.ADD.bit {lambda {:x :a :b} {PAIR {XOR :x {XOR :a :b}} {OR {AND :a :b} {OR {AND :x :a} {AND :x :b}}}}}} {def B.ADD.rec {lambda {:x :a :b} {{IF {OR {NIL? :a} {NIL? :b}} {lambda {:x :a :b} {{lambda {:x} {IF {LEFT :x} :x {RIGHT :x}}} {PAIR :x NIL}}} {lambda {:x :a :b} {{lambda {:x :a :b} {PAIR {LEFT :x} {B.ADD.rec {RIGHT :x} {RIGHT :a} {RIGHT :b}}} } {B.ADD.bit :x {LEFT :a} {LEFT :b}} :a :b}}} :x :a :b }}} {lambda {:a :b} {B.ADD.rec #0 :a :b }}} '{bool2dec {B.ADD {dec2bool 65 {pow 2 64}} {dec2bool 65 {pow 2 64}}}} -> 36893488147419104000 // about 50ms } _h2 B.MUL °°° https://en.wikipedia.org/wiki/Multiplication_algorithm {def mul {lambda {:a :b :c} {if {= :a 0} then :c else {mul {floor {/ :a 2}} {* :b 2} {if {= {% :a 2} 0} then :c else {+ :c :b}}}}}} °°° {pre 5830 * 23958233 = 139676498390 Decimal: Binary: ;;x=x//2 y=y*2 shift x right shift y left 5830 {del 23958233} 1011011000110 {del 1011011011001001011011001} 2915 47916466 101101100011 10110110110010010110110010 1457 95832932 10110110001 101101101100100101101100100 728 {del 191665864} 1011011000 {del 1011011011001001011011001000} 364 {del 383331728} 101101100 {del 10110110110010010110110010000} 182 {del 766663456} 10110110 {del 101101101100100101101100100000} 91 1533326912 1011011 1011011011001001011011001000000 45 3066653824 101101 10110110110010010110110010000000 22 {del 6133307648} 10110 {del 101101101100100101101100100000000} 11 12266615296 1011 1011011011001001011011001000000000 5 24533230592 101 10110110110010010110110010000000000 2 {del 49066461184} 10 {del 101101101100100101101100100000000000} 1 98132922368 1 1011011011001001011011001000000000000 ———————————— ————————————————————————————————————— 139676498390 10000010000101010111100011100111010110 '{def B.MUL {def B.MUL.rec {lambda {:a :b :c} {{IF {B.ZERO? :a} {lambda {:a :b :c} :c} // return :c {lambda {:a :b :c} {B.MUL.rec {B.SHFTR :a} // :a / 2 {B.SHFTL :b} // :b * 2 {IF {LEFT :a} // if :a even {B.ADD :b :c} // then add :b to :c :c}} }} // else discard :b :a :b :c}}} {lambda {:n :a :b} {B.MUL.rec :a :b {ZERO :n}}}} // initialize and loop -> {def B.MUL {def B.MUL.rec {lambda {:a :b :c} {{IF {B.ZERO? :a} {lambda {:a :b :c} :c} {lambda {:a :b :c} {B.MUL.rec {B.SHFTR :a} ;; a / 2 {B.SHFTL :b} ;; b * 2 {IF {LEFT :a} {B.ADD :c :b} :c}} } } :a :b :c}}} {lambda {:n :a :b} {B.MUL.rec :a :b {ZERO :n}}}} '{bool2dec {B.MUL 65 {dec2bool 65 {pow 2 32}} {dec2bool 65 {pow 2 32}}}} -> 18446744073709551616 // < about 600ms '{* {pow 2 32} {pow 2 32}} -> {* {pow 2 32} {pow 2 32}} '{long_mult {pow 2 32} {pow 2 32}} -> {long_mult {pow 2 32} {pow 2 32}} } _h2 B.POW {pre {center {pre 3{sup 9} = {pow 3 9} Decimal: Binary: shifts a*a b//2 shiftleft siftright 3 9 {dec2bin 16 3} {dec2bin 16 9} {* 3 3} 4 {dec2bin 16 9} {dec2bin 16 4} {* 9 9} 2 {dec2bin 16 81} {dec2bin 16 2} {* 81 81} 1 {dec2bin 16 6561} {dec2bin 16 1} {* 6561 3} 0 {dec2bin 16 19683} {dec2bin 16 0} }} '{def B.POW {def B.POW.rec {lambda {:n :a :b :c} {{IF {B.ZERO? :b} {lambda {:n :a :b :c} :c} {lambda {:n :a :b :c} {B.POW.rec :n {B.MUL :n :a :a} {B.SHFTR :b} {IF {LEFT :b} {B.MUL :n :a :c} :c} }}} :n :a :b :c}}} {lambda {:n :a :b} {B.POW.rec :n :a :b {ONE :n}}}} -> {def B.POW {def B.POW.rec {lambda {:n :a :b :c} {{IF {B.ZERO? :b} {lambda {:n :a :b :c} :c} {lambda {:n :a :b :c} {B.POW.rec :n {B.MUL :n :a :a} {B.SHFTR :b} {IF {LEFT :b} {B.MUL :n :a :c} :c} }}} :n :a :b :c}}} {lambda {:n :a :b} {B.POW.rec :n :a :b {ONE :n}}}} '{bool2dec {B.POW 192 {dec2bool 192 2} {dec2bool 192 128}}} -> 340282366920938463463374607431768211456 // < 0.5 second } _h2 B.ZERO?, B.PRED, B.SUCC, B.SHFTL, B.SHFTR {pre '{def B.ZERO? {def B.ZERO?.rec {lambda {:a :b} {{IF {NIL? :a} {lambda {:a :b} :b} {lambda {:a :b} {B.ZERO?.rec {RIGHT :a} {IF {LEFT :a} #0 :b}}}} :a :b}}} {lambda {:a} {B.ZERO?.rec :a #1}}} -> {def B.ZERO? {def B.ZERO?.rec {lambda {:a :b} {{IF {NIL? :a} {lambda {:a :b} :b} {lambda {:a :b} {B.ZERO?.rec {RIGHT :a} {IF {LEFT :a} #0 :b} }}} :a :b}}} {lambda {:a} {B.ZERO?.rec :a #1}}} '{B.ZERO? {ZERO 8}} -> #1 '{B.ZERO? {ONE 8}} -> #0 '{def B.PRED {def B.PRED.rec {lambda {:a :c} {{IF {NIL? :a} {lambda {:a :c} {PAIR :c NIL} } {lambda {:a :c} {{lambda {:a :c} {PAIR {LEFT :c} {B.PRED.rec {RIGHT :a} {RIGHT :c}}} } :a {B.ADD.bit {LEFT :a} #1 :c}} }} :a :c}}} {lambda {:a} {L.REV {RIGHT {L.REV {B.PRED.rec :a #0}}}}}} -> {def B.PRED {def B.PRED.rec {lambda {:a :c} {{IF {NIL? :a} {lambda {:a :c} {PAIR :c NIL} } {lambda {:a :c} {{lambda {:a :c} {PAIR {LEFT :c} {B.PRED.rec {RIGHT :a} {RIGHT :c}}} } :a {B.ADD.bit {LEFT :a} #1 :c}} }} :a :c}}} {lambda {:a} {L.REV {RIGHT {L.REV {B.PRED.rec :a #0}}}}}} '{bool2dec {B.PRED {dec2bool 128 4294967296}}} -> 4294967295 // 2{sup 32}-1 '{def B.SUCC {def B.SUCC.rec {lambda {:a :c} {{IF {NIL? :a} {lambda {:a :c} {PAIR :c NIL} } {lambda {:a :c} {{lambda {:a :c} {PAIR {LEFT :c} {B.SUCC.rec {RIGHT :a} {RIGHT :c}}} } :a {B.ADD.bit {LEFT :a} #0 :c}} }} :a :c}}} {lambda {:a} {L.REV {RIGHT {L.REV {B.SUCC.rec :a #1}}}}}} -> {def B.SUCC {def B.SUCC.rec {lambda {:a :c} {{IF {NIL? :a} {lambda {:a :c} {PAIR :c NIL} } {lambda {:a :c} {{lambda {:a :c} {PAIR {LEFT :c} {B.SUCC.rec {RIGHT :a} {RIGHT :c}}} } :a {B.ADD.bit {LEFT :a} #0 :c}} }} :a :c}}} {lambda {:a} {L.REV {RIGHT {L.REV {B.SUCC.rec :a #1}}}}}} '{bool2dec {B.SUCC {dec2bool 32 4294967295}}} -> 4294967296 // 2{sup 32} '{def B.SHFTR {lambda {:b} {L.REV {PAIR #0 {L.REV {RIGHT :b}}}}}} -> {def B.SHFTR {lambda {:b} {L.REV {PAIR #0 {L.REV {RIGHT :b}}}}}} '{def B.SHFTL {lambda {:b} {PAIR #0 {L.REV {RIGHT {L.REV :b}}}}}} -> {def B.SHFTL {lambda {:b} {PAIR #0 {L.REV {RIGHT {L.REV :b}}}}}} '{bool2dec {B.SHFTL {dec2bool 16 256}}} -> {bool2dec {B.SHFTL {dec2bool 16 256}}} '{bool2dec {B.SHFTR {dec2bool 16 256}}} -> {bool2dec {B.SHFTR {dec2bool 16 256}}} } _h2 PAIRS & LISTS _p Binary numbers are implemented as lists of booleans, {b #0 & #1}, for true & false. {pre '{def PAIR {lambda {:a :b :c} {:c :a :b}}} -> {def PAIR {lambda {:a :b :c} {:c :a :b}}} '{def LEFT {lambda {:c} {:c #1}}} -> {def LEFT {lambda {:c} {:c #1}}} '{def RIGHT {lambda {:c} {:c #0}}} -> {def RIGHT {lambda {:c} {:c #0}}} '{def NIL {lambda {:a} #1}} -> {def NIL {lambda {:a} #1}} '{def NIL? {lambda {:c} {:c {lambda {:a :b} #0}}}} -> {def NIL? {lambda {:c} {:c {lambda {:a :b} #0}}}} '{def L.DISP {lambda {:l} {{IF {NIL? :l} {lambda {:l} } {lambda {:l} {LEFT :l} {L.DISP {RIGHT :l}}}} :l}}} -> {def L.DISP {lambda {:l} {{IF {NIL? :l} {lambda {:l} } {lambda {:l} {LEFT :l} {L.DISP {RIGHT :l}}}} :l}}} '{def L.REV {def L.REV.r {lambda {:a :b} {{IF {NIL? :a} {lambda {:a :b } :b} {lambda {:a :b} {L.REV.r {RIGHT :a} {PAIR {LEFT :a} :b}}}} :a :b}}} {lambda {:l} {L.REV.r :l NIL}}} -> {def L.REV {def L.REV.r {lambda {:a :b} {{IF {NIL? :a} {lambda {:a :b } :b} {lambda {:a :b} {L.REV.r {RIGHT :a} {PAIR {LEFT :a} :b}}}} :a :b}}} {lambda {:l} {L.REV.r :l NIL}}} '{def mylist {PAIR a {PAIR b {PAIR c {PAIR d NIL}}}}} -> {def mylist {PAIR a {PAIR b {PAIR c {PAIR d NIL}}}}} '{NIL? {mylist}} -> {NIL? {mylist}} '{NIL? NIL} -> {NIL? NIL} '{L.DISP {mylist}} -> {L.DISP {mylist}} '{LEFT {mylist}} -> {LEFT {mylist}} '{L.DISP {RIGHT {mylist}}} -> {L.DISP {RIGHT {mylist}}} '{L.DISP {L.REV {mylist}}} -> {L.DISP {L.REV {mylist}}} } _h2 BOOLEANS {pre '{def #1 {lambda {:a :b} :a}} -> {def #1 {lambda {:a :b} :a}} '{def #0 {lambda {:a :b} :b}} -> {def #0 {lambda {:a :b} :b}} '{def IF {lambda {:a :b :c} {:a :b :c}}} -> {def IF {lambda {:a :b :c} {:a :b :c}}} '{def NOT {lambda {:a} {IF :a #0 #1}}} -> {def NOT {lambda {:a} {IF :a #0 #1}}} '{def AND {lambda {:a :b} {IF :a :b #0}}} -> {def AND {lambda {:a :b} {IF :a :b #0}}} '{def OR {lambda {:a :b} {IF :a #1 :b}}} -> {def OR {lambda {:a :b} {IF :a #1 :b}}} '{def XOR {lambda {:a :b} {OR {AND :a {NOT :b}} {AND :b {NOT :a}}}}} -> {def XOR {lambda {:a :b} {OR {AND :a {NOT :b}} {AND :b {NOT :a}}}}} } _h2 INPUT & OUTPUT _p The following functions are used exclusively to input and output binary numbers as decimals. They are out of the λ-calculus level and use the {b if then else} and {b let} lambdatalk special forms, the javascript math standard primitives and two necessary primitives, {b long_add & long_mult}, dealing with big numbers. {pre '{def dec2bool {lambda {:n :m} {L.REV {bin2bool {dec2bin :n :m}}}}} -> {def dec2bool {lambda {:n :m} {L.REV {bin2bool {dec2bin :n :m}}}}} '{def bool2dec {lambda {:m} {bin2dec {bool2bin {L.REV :m}}}}} -> {def bool2dec {lambda {:m} {bin2dec {bool2bin {L.REV :m}}}}} '{def ZERO {lambda {:n} {bin2bool {zpadd :n}}}} -> {def ZERO {lambda {:n} {bin2bool {zpadd :n}}}} '{def ONE {lambda {:n} {bin2bool 1{zpadd {- :n 1}}}}} -> {def ONE {lambda {:n} {bin2bool 1{zpadd {- :n 1}}}}} '{def bin2dec {def bin2dec.r {lambda {:p :r} {if {A.empty? :p} then :r else {bin2dec.r {A.rest :p} {long_add {A.first :p} {long_mult 2 :r}}}}}} {lambda {:p} {bin2dec.r {A.split :p} 0}}} -> {def bin2dec {def bin2dec.r {lambda {:p :r} {if {A.empty? :p} then :r else {bin2dec.r {A.rest :p} {long_add {A.first :p} {long_mult 2 :r}}}}}} {lambda {:p} {bin2dec.r {A.split :p} 0}}} '{def dec2bin {def dec2bin.r {lambda {:dec} {if {= :dec 0} then 0 else {if {< :dec 2} then 1 else {dec2bin.r {floor {/ :dec 2}}}{% :dec 2} }}}} {lambda {:n :dec} {let { {:n :n} {:b {dec2bin.r :dec}} } {zpadd {- :n {W.length :b}}}:b}}} -> {def dec2bin {def dec2bin.r {lambda {:dec} {if {= :dec 0} then 0 else {if {< :dec 2} then 1 else {dec2bin.r {floor {/ :dec 2}}}{% :dec 2} }}}} {lambda {:n :dec} {let { {:n :n} {:b {dec2bin.r :dec}} } {zpadd {- :n {W.length :b}}}:b}}} '{def zpadd {lambda {:n} {if {= :n 0} then else 0{zpadd {- :n 1}}}}} -> {def zpadd {lambda {:n} {if {= :n 0} then else 0{zpadd {- :n 1}}}}} '{def bin2bool {def bin2bool.r {lambda {:s} {if {= {S.length :s} 1} then {PAIR :s NIL} else {PAIR {S.first :s} {bin2bool.r {S.rest :s}}}} }} {lambda {:w} {bin2bool.r {S.replace _ by space in {S.replace 1 by #1_ in {S.replace 0 by #0_ in :w}}}}}} -> {def bin2bool {def bin2bool.r {lambda {:s} {if {= {S.length :s} 1} then {PAIR :s NIL} else {PAIR {S.first :s} {bin2bool.r {S.rest :s}}}} }} {lambda {:w} {bin2bool.r {S.replace _ by space in {S.replace 1 by #1_ in {S.replace 0 by #0_ in :w}}}}}} '{def bool2bin {lambda {:b} {S.replace \s by in {S.replace #0 by 0 in {S.replace #1 by 1 in {L.DISP :b}}}}}} -> {def bool2bin {lambda {:b} {S.replace \s by in {S.replace #0 by 0 in {S.replace #1 by 1 in {L.DISP :b}}}}}} } _p {i alain marty | 2020/02/24} _p [[HN|https://news.ycombinator.com/item?id=30564263]]
lambdaway v.20211111