Sun Sep 15 02:29:55 CEST 2024
narrator: revisiting the Euclid's algorithm... One part was x->y->|x-y| which I implemented as
x->y->(x dec y) inc (y dec x)
(btw I hate succ/pred, it's only there to scare newbies away from FP)
dec is derived somewhere around here but I can't find the record. it was identical to half below...
so I noticed that x dec y can be writted as T dec x y and y dec x as V dec x y
(here V x y z = z x y, impleemented as BCT, and T x y = y x implemented as CI)
so how do I write T inc (T dec x y) (V dec x y) in a compact form?..
F f g h x y = f (g x y) (h x y)
= f (Tg (Vx y)) (Th (Vx y))
= B(f (Tg (V x y))) (Th) (V x y)
= B(B f (Tg) (V x y)) (Th) (V x y)
= BB(B f (Tg)) (V x y) (Th) (V x y)
= C(BB(B f (Tg))) (Th) (V x y)(V x y)
= W(C(BB(B f (Tg))) (Th)) (V x y)
= BBB(W(C(BB(B f (Tg))) (Th))) V x y
// convert 2 args fun <-> unary fun:
C(BBB)V f x y -> f(V x y)
Tf (V x y) = f x y
narrator: my previous euclids kept hanging despite all lazy stuff like C(K(WI)) x y
and BCC x y z put into them. So I decided to write if in such a way that it never
runs then/else without calculating the condition first.
The ++ mark stands for putting the partial computation into the interpreter and getting
expected result.
if cond then else x = (cond x)(!slow then x)(!slow else x)
if cond then else x = cond x then else x
= C cond then x else x
= C(C cond then) else x x
= W(C(C cond then) else) x ++
if cond then else = W(C(C cond then) else)
= BW(C(C cond then)) else
= BW(BC(C cond) then) else
= B(BW)(BC(C cond)) then else
= B(BW)(B(BC)C cond) then else
= B(B(BW))(B(BC)C) cond then else
half (again)
sub3 x y z n = n x y z
= V x y n z
= C(V x y) z n
= BBBCV x y z n ++
half n = n x acc carry
x acc carry = carry (inc (acc A)) (acc K)
= V(B inc acc A) (acc K) carry
= V(C(B inc) A acc) (TK acc) carry
= BV(C(B inc) A) acc (TK acc) carry
= C(BV(C(B inc) A)) (TK acc) acc carry
= B(C(BV(C(B inc) A))) (TK) acc acc carry
= W(B(C(BV(C(B inc) A))) (TK)) acc carry ++
carry(0) = KI
acc(0) = K(KI)
half = B !nat (BBBCV (W(B(C(BV(C(B (SB)) (KI)))) (TK))) (K(KI)) (KI)) ++
narrator: the nonstandard !nat above is a pseudocombinator that passes a pair of free variables
to its argument and counts the number of applications in the result and returns a "native" Church
numeral of form x->y->x(...n times...(x(y))...) that also appears as just the number when stringified.
collatz conjecture iteration (x' = x mod 2 ? 3 * x + 1 : x/2) was derived around here
to verify the if term works as it should.
Sun Sep 15 03:31:42 CEST 2024
euclid 2.0
euc euc x y = y == 0 ? x : euc euc y |x - y|
euc f = C(BBB)V (if (izzero y) (x) (!slow f f y (delta x y)))
narrator: Here I'm omitting the (not so) obvious way of deriving a recursive function
(basically a pedestrian Y combinator):
f x = foo f x; f = g g; g g x = foo (g g) x; h g x = foo (g g) x; h = g->x->foo (g g) x
and we can now calculate h as a nonrecursive term and h h gives a recursive function
with the required properties.
This of course lacks some mathematical rigor but is okayish for computations...
izzero y = izzero (V x y (KI))
= B izzero (V x y) (KI)
= C(B izzero1)(KI) (V x y) ++
then (V x y) = x
then = TK
else (V x y) = f f y (delta x y)
arg = V x y
y = TA arg
delta x y = Tdelta arg
narrator: now the fun starts!
narrator: dbl stands for x->y->x x implemented as C(K(WI))
else arg = f f y (delta x y)
= f f (TA arg) (T delta arg)
= dbl f arg (TA arg) (T delta arg)
= B (dbl f arg) (TA) arg (T delta arg)
= BB (dbl f) arg (TA) arg (T delta arg)
= C(BB (dbl f)) (TA) arg arg (T delta arg)
= W(C(BB (dbl f)) (TA)) arg (T delta arg)
= C(W(C(BB (dbl f)) (TA))) (T delta arg) arg
= B(C(W(C(BB (dbl f)) (TA)))) (T delta) arg arg
= W(B(C(W(C(BB (dbl f)) (TA)))) (T delta)) arg ++
// ... (extract f)
else = W(B(C(W(C(BB (dbl f)) (TA)))) (T delta))
= W(CB(T delta)(C(W(C(BB (dbl f)) (TA)))))
= W(CB(T delta)(C(W(CC(TA)(BB (dbl f))))))
= W(CB(T delta)(C(W(CC(TA)(B(BB) dbl f)))))
= W(CB(T delta)(C(W(B(CC(TA))(B(BB) dbl) f))))
= W(CB(T delta)(C(BW(B(CC(TA))(B(BB) dbl)) f)))
= W(CB(T delta)(BC(BW(B(CC(TA))(B(BB) dbl))) f))
= W(B(CB(T delta))(BC(BW(B(CC(TA))(B(BB) dbl)))) f)
= BW(B(CB(T delta))(BC(BW(B(CC(TA))(B(BB) dbl))))) f
// ++
euc f = C(BBB)V (if (C(B izzero)(KI)) (TK) (BW(B(CB(T delta))(BC(BW(B(CC(TA))(B(BB) dbl))))) f))
= C(BBB)V (B(if (C(B izzero)(KI)) (TK)) (BW(B(CB(T delta))(BC(BW(B(CC(TA))(B(BB) dbl)))))) f)
= B (C(BBB)V) (B(if (C(B izzero)(KI)) (TK)) (BW(B(CB(T delta))(BC(BW(B(CC(TA))(B(BB) dbl))))))) f
narrator: and it worked!