Last active
July 14, 2022 18:33
-
-
Save TarVK/5e7db4a0d244186dab0a97a825973ad8 to your computer and use it in GitHub Desktop.
Lambda calculus in js
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/** Logic */ | |
True = x=>y=>x | |
False = x=>y=>y | |
iff = c=>t=>f=>c(t)(f) | |
lazyIf = c=>t=>f=>c(t)(f)() // Js evualuation isn't lazy, but it can be simulated by providing callback functions | |
not = f=>x=>y=>f(y)(x) | |
and = x=>y=>x(y)(x) | |
or = x=>y=>x(x)(y) | |
/** Pairs */ | |
Pair = x=>y=>f=>f(x)(y) | |
first = t=>t(True) | |
second = t=>t(False) | |
/** Lists */ | |
Nil = n=>c=>n | |
Cons = x=>y=>n=>c=>c(x)(y) | |
isEmpty = l=>l(True)(()=>()=>False) | |
head = l=>l(l)(True) // First param doesn't matter | |
tail = l=>l(l)(False) // First param doesn't matter | |
fold = b=>s=>l=>F(r=>l=>lazyIf(isEmpty(l))(()=>b)(()=>s(head(l))(r(tail(l)))))(l) | |
concat = a=>b=>fold(b)(Cons)(a) | |
/** Numbers */ | |
V0 = f=>b=>b | |
V1 = f=>b=>f(b) | |
V2 = f=>b=>f(f(b)) | |
V3 = f=>b=>f(f(f(b))) | |
V4 = f=>b=>f(f(f(f(b)))) | |
// ...etc | |
isZero = n=>n(()=>False)(True) | |
add1 = n=>f=>b=>f(n(f)(b)) | |
sub1 = n=>f=>b=>first(n(v=>Pair(second(v))(f(second(v))))(Pair(b)(b))) | |
add = n=>m=>f=>b=>m(f)(n(f)(b)) | |
mul = n=>m=>f=>b=>m(n(f))(b) | |
pow = n=>m=>f=>b=>m(n)(f)(b) | |
sub = n=>m=>f=>b=>m(sub1)(n)(f)(b) | |
div = n=>m=>F(r=>n=>(s=>lazyIf(isZero(s))(()=>V0)(()=>add1(r(s))))(sub(n)(m)))(add1(n)) | |
/** Recursion using fixpoints */ | |
F = f=>(x=>a=>f(x(x))(a))(x=>a=>f(x(x))(a)) // Usually is f=>(x=>f(x(x)))(x=>f(x(x))) which only works under lazy evaluation | |
/** Example program like functions */ | |
fib = n=>first(n(x=>Pair(second(x))(add(first(x))(second(x))))(Pair(V0)(V1))) | |
fac = F(r=>n=>lazyIf(isZero(n))(()=>V1)(()=>mul(n)(r(sub1(n))))) // Have to use lazyIf to prevent infinite recursion | |
fac2 = n=>first(n(x=>Pair(mul(first(x))(second(x)))(add1(second(x))))(Pair(V1)(V1))) // Alternative definition using a paramorphism | |
partition = p=>fold(Pair(Nil)(Nil))(h=>t=>iff(isZero(sub(h)(p)))(Pair(Cons(h)(first(t)))(second(t)))(Pair(first(t))(Cons(h)(second(t))))) | |
quicksort = F(r=>l=>lazyIf(isEmpty(l))(()=>Nil)(()=>l(l)(h=>t=>(p=>concat(r(first(p)))(concat(Cons(h)(Nil))(r(second(p)))))(partition(h)(t))))) | |
/** Helpers to reveal hidden function structure by converting to and from js data */ | |
V = fromJsNumber = n=>new Array(n).fill().reduce(add1, V0); | |
toJsNumber = n=>n(v=>v+1)(0); | |
fromJsArray = ar=>ar.reduceRight((cur, val)=>Cons(val)(cur), Nil); | |
toJsArray = l=>{ | |
const out = []; | |
while(!isTrue(isEmpty(l))){ | |
out.push(head(l)); | |
l = tail(l); | |
} | |
return out; | |
} | |
isTrue = b=>b(true)(false); | |
fromJsNumberArray = ar=>fromJsArray(ar.map(v=>V(v))); | |
toJsNumberArray = l=>toJsArray(l).map(v=>toJsNumber(v)); |
Here's another fun standalone one:
quicksort = (f=>(x=>a=>f(x(x))(a))(x=>a=>f(x(x))(a)))(r=>l=>(c=>t=>f=>c(t)(f)())((l=>l((x=>y=>x))(()=>()=>(x=>y=>y)))(l))(()=>(n=>c=>n))(()=>l(l)(h=>t=>(p=>(a=>b=>(b=>s=>l=>(f=>(x=>a=>f(x(x))(a))(x=>a=>f(x(x))(a)))(r=>l=>(c=>t=>f=>c(t)(f)())((l=>l((x=>y=>x))(()=>()=>(x=>y=>y)))(l))(()=>b)(()=>s((l=>l(l)((x=>y=>x)))(l))(r((l=>l(l)((x=>y=>y)))(l)))))(l))(b)((x=>y=>n=>c=>c(x)(y)))(a))(r((t=>t((x=>y=>x)))(p)))((a=>b=>(b=>s=>l=>(f=>(x=>a=>f(x(x))(a))(x=>a=>f(x(x))(a)))(r=>l=>(c=>t=>f=>c(t)(f)())((l=>l((x=>y=>x))(()=>()=>(x=>y=>y)))(l))(()=>b)(()=>s((l=>l(l)((x=>y=>x)))(l))(r((l=>l(l)((x=>y=>y)))(l)))))(l))(b)((x=>y=>n=>c=>c(x)(y)))(a))((x=>y=>n=>c=>c(x)(y))(h)((n=>c=>n)))(r((t=>t((x=>y=>y)))(p)))))((p=>(b=>s=>l=>(f=>(x=>a=>f(x(x))(a))(x=>a=>f(x(x))(a)))(r=>l=>(c=>t=>f=>c(t)(f)())((l=>l((x=>y=>x))(()=>()=>(x=>y=>y)))(l))(()=>b)(()=>s((l=>l(l)((x=>y=>x)))(l))(r((l=>l(l)((x=>y=>y)))(l)))))(l))((x=>y=>f=>f(x)(y))((n=>c=>n))((n=>c=>n)))(h=>t=>(c=>t=>f=>c(t)(f))((n=>n(()=>(x=>y=>y))((x=>y=>x)))((n=>m=>f=>b=>m((n=>f=>b=>(t=>t((x=>y=>x)))(n(v=>(x=>y=>f=>f(x)(y))((t=>t((x=>y=>y)))(v))(f((t=>t((x=>y=>y)))(v))))((x=>y=>f=>f(x)(y))(b)(b)))))(n)(f)(b))(h)(p)))((x=>y=>f=>f(x)(y))((x=>y=>n=>c=>c(x)(y))(h)((t=>t((x=>y=>x)))(t)))((t=>t((x=>y=>y)))(t)))((x=>y=>f=>f(x)(y))((t=>t((x=>y=>x)))(t))((x=>y=>n=>c=>c(x)(y))(h)((t=>t((x=>y=>y)))(t))))))(h)(t)))))
toJsArray = l=>{
const out = [];
while(l(false)(()=>()=>true)){
out.push(l(l)(h=>t=>h(v=>v+1)(0)));
l = l(l)(h=>t=>t);
}
return out;
}
fromJsArray = ar=>ar.reduceRight((cur, val)=>n=>c=>c(new Array(val).fill().reduce(n=>f=>b=>f(n(f)(b)), f=>b=>b))(cur), n=>c=>n);
toJsArray(quicksort(fromJsArray([11,5,4,2,7,6,3,8,9,0,10,12,1])))
Lists can also be defined in another way, making recursion an intrinsic part of the structure, similar to numbers.
But similar to subtraction with numbers, getting the tail of a list will become more complicated:
Cons = x=>y=>n=>c=>c(x)(y(n)(c))
head = l=>l(l)(True) // First argument to l doesn't matter
fold = b=>s=>l=>l(b)(s)
tail = l=>first(fold(Pair(Nil)(Nil))(v=>p=>Pair(second(p))(Cons(v)(second(p))))(l))
Additionally quicksort has to be changed a bit to no longer exploit the list structure directly but instead only depend on the above definitions:
quicksort = F(r=>l=>lazyIf(isEmpty(l))(()=>Nil)(()=>(p=>concat(r(first(p)))(concat(Cons(head(l))(Nil))(r(second(p)))))(partition(head(l))(tail(l)))));
Everything else remains the same, so for a complete overview:
Nil = n=>c=>n
Cons = x=>y=>n=>c=>c(x)(y(n)(c))
isEmpty = l=>l(True)(()=>()=>False)
head = l=>l(l)(True) // First argument to l doesn't matter
fold = b=>s=>l=>l(b)(s)
tail = l=>first(fold(Pair(Nil)(Nil))(v=>p=>Pair(second(p))(Cons(v)(second(p))))(l))
concat = a=>b=>fold(b)(Cons)(a)
partition = p=>fold(Pair(Nil)(Nil))(h=>t=>iff(isZero(sub(h)(p)))(Pair(Cons(h)(first(t)))(second(t)))(Pair(first(t))(Cons(h)(second(t)))))
quicksort = F(r=>l=>lazyIf(isEmpty(l))(()=>Nil)(()=>(p=>concat(r(first(p)))(concat(Cons(head(l))(Nil))(r(second(p)))))(partition(head(l))(tail(l)))));
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I am obviously using js variables to keep this collection of functions somewhat readable, so I could use js recursion to write factorial.
But real lambda calculus doesn't have assignment like we do in js, so we can't simply do recursion like that. That's why we introduced fixpoint factory F.
Just to make it clear of what a real lambda calculus 'program' as expressed in js syntax would look like, I performed all substitutions on
fac
to obtain this amazing oneliner (which doesn't use recursion):Then we can execute this:
Or apply the lambda calculus expression in its pure form, including the data input (but still translating the result back to js numbers since js itself will hide function details in the scope).