Lambda as JS by Glen Lebec (test outputs)

lambda.log

I := λx.x

✅  I tweet = tweet
✅  I chirp = chirp
✅  I I = I

Idiot := I


Mockingbird := M := ω := λf.ff

✅  M I = I I = I
✅  M M = M M = M M = Maximum call stack size exceeded

First encodings: boolean value functions


T := λxy.x


F := λxy.y

✅  T tweet chirp = tweet
✅  F tweet chirp = chirp

Cardinal := C := flip := λfab.fba


F = C T

✅  flip T tweet chirp = chirp

NOT := λb.bFT

✅  NOT T = F
✅  NOT F = T
✅  CF = T
✅  CT = F

AND := λpq.pqF

✅  AND F F = F
✅  AND T F = F
✅  AND F T = F
✅  AND T T = T

OR := λpq.pTq

✅  OR F F = F
✅  OR T F = T
✅  OR F T = T
✅  OR T T = T
✅  M F F = F
✅  M T F = T
✅  M F T = T
✅  M T T = T

De Morgan: not (and P Q) = or (not P) (not Q)

✅  NOT (AND F F) = OR (NOT F) (NOT F)
✅  NOT (AND T F) = OR (NOT T) (NOT F)
✅  NOT (AND F T) = OR (NOT F) (NOT T)
✅  NOT (AND T T) = OR (NOT T) (NOT T)

BEQ := λpq.p (qTF) (qFT)

✅  BEQ F F = T
✅  BEQ F T = F
✅  BEQ T F = F
✅  BEQ T T = T

Numbers


0 := λfx.x

✅  0 M tweet = tweet

hard-coded 1 and 2


1 := λfx.fx

✅  1 I tweet = tweet
✅  0 yell λ = λ
✅  1 yell λ = yell λ = λ!

2 := λfx.f(fx)

✅  2 yell λ = yell (yell λ) = λ!!

SUCCESSOR


SUCCESSOR := λnfx.f(nfx)

✅  1 yell λ = λ!
✅  2 yell λ = λ!!
✅  3 yell λ = λ!!!

Bluebird := B := (∘) := compose := λfgx.f(gx)

✅  (B NOT NOT)  T =  NOT (NOT T)
✅  (B yell NOT) F = yell (NOT F)

SUCC := λnf.f∘(nf) = λnf.Bf(nf)

✅  1 yell λ = λ!
✅  2 yell λ = λ!!
✅  3 yell λ = λ!!!
✅  4 yell λ = λ!!!!

ADD := λab.a(succ)b

✅  ADD 5 2 yell λ = λ!!!!!!!
✅  ADD 0 3 yell λ = λ!!!
✅  ADD 2 2 = 4

LC <-> JS: church & jsnum

✅  church(5) = n5
✅  jsnum(n5) === 5
✅  jsnum(church(2)) === 2

MULT := λab.a∘b = compose

✅  MULT 1 5 = 5
✅  MULT 3 2 = 6
✅  MULT 4 0 = 0
✅  MULT 6 2 yell λ = λ!!!!!!!!!!!!

Thrush := POW := λab.ba

✅  POW 2 3 = 8
✅  POW 3 2 = 9
✅  POW 6 1 = 6
✅  POW 5 0 = 1

ISZERO := λn.n(λ_.F)T

✅  ISZERO 0 = T
✅  ISZERO 1 = F
✅  ISZERO 2 = F

Kestrel combinator and IS0


Kestrel := K := konst := λk_.k

✅  K0 tweet = 0
✅  K0 chirp = 0
✅  K tweet chirp = tweet

IS0 := λn.n(KF)T

✅  IS0 0 = T
✅  IS0 1 = F
✅  IS0 2 = F

         K = T


Kite := KI = F

✅  K  tweet chirp = tweet
✅  KI tweet chirp = chirp
✅  De Morgan using K and KI

PREDECESSOR := λn.n (λg.IS0 (g 1) I (B SUCC g)) (K0) 0

✅  PREDECESSOR 0 = 0
✅  PREDECESSOR 1 = 0
✅  PREDECESSOR 2 = 1
✅  PREDECESSOR 3 = 2

Pair: a Tiny Functional Data Structure


Vireo := V := PAIR := λabf.fab

✅  (PAIR tweet chirp) T = tweet
✅  (PAIR tweet chirp) F = chirp

FST := λp.pT; SND = λp.pF

✅  FST (PAIR tweet chirp) = tweet
✅  SND (PAIR tweet chirp) = chirp

SET_FST := λcp.PAIR c (SND p)

✅  FST (SET_FST chirp (PAIR tweet tweet)) = chirp
✅  SND (SET_FST chirp (PAIR tweet tweet)) = tweet

SET_SND := λcp.PAIR (FST p) c

✅  FST (SET_SND chirp <tweet, tweet>) = tweet
✅  SND (SET_SND chirp <tweet, tweet>) = chirp

PHI := Φ := λp.PAIR (SND p) (SUCC (SND p))

✅  Φ <chirp, 0> = <0, 1>
✅  Φ <tweet, 4> = <4, 5>

PRED := λn.FST (n Φ <0, 0>)

✅  PRED 0 = 0
✅  PRED 1 = 0
✅  PRED 2 = 1
✅  PRED 3 = 2

SUB := λab.b PRED a

✅  SUB 5 2 = 3
✅  SUB 4 0 = 4
✅  SUB 2 2 = 0
✅  SUB 2 7 = 0

LEQ := λab.IS0(SUB a b)

✅  LEQ 3 2 = F
✅  LEQ 3 3 = T
✅  LEQ 3 4 = T

eq := λab.AND (LEQ a b) (LEQ b a)

✅  EQ 4 6 = F
✅  EQ 7 3 = F
✅  EQ 5 5 = T
✅  EQ (ADD 3 6) (POW 3 2) = T

Blackbird := B′ := BBB


GT := B1 NOT LEQ

✅  GT 6 2 = T
✅  GT 4 4 = F
✅  GT 4 5 = F

FIB := λn.n (λfab.f b (ADD a b)) K 0 1

✅  FIB 0 = 0
✅  FIB 1 = 1
✅  FIB 2 = 1
✅  FIB 3 = 2
✅  FIB 4 = 3
✅  FIB 5 = 5
✅  FIB 6 = 8