Solving the mystery behind Abstract Algorithm’s magical optimizations

1. Optimizable functions are those that fuse when self-composed

True  = λt. λf. t
False = λt. λf. f
not_a = λb. (b False True)
not_b = λb. λt. λf. (b f t)
Complexity (total rewrites) of applying “not” N times to True
  • norm(not_a.not_a): λb. (b (λt.λf.f) (λt.λf.t) (λt.λf.f) (λt.λf.t))
  • norm(not_b.not_b): λb. λt. λf. (b t f)
Nil   =         λc. λn. n
Cons = λh. λt. λc. λn. c h (t c n)
map_a = λf. λl. l (λh. λt. Cons (f h) t) Nil
map_b = λf. λl. λc. λn. l (λh. λt. c (f h) t) n
list = Cons True (Cons False (Cons True (Cons False Nil)))
Complexity (total rewrites) of applying “map” N times to a list of 4 elements

2. Exponentiation by squaring = composition by sharing

# Computing 13^8 with repeated multiplication13^2 = 13 * 13 = 169
13^3 = 13 * 169 = 2197
13^4 = 13 * 2197 = 28561
13^5 = 13 * 28561 = 371293
13^6 = 13 * 371293 = 4826809
13^7 = 13 * 4826809 = 62748517
13^8 = 13 * 62748517 = 815730721
# Computing 13^8 with exponentiation by squaring13^2 = 13 * 13 = 169
13^4 = 169 * 169 = 28561
13^8 = 28561 * 28561 = 815730721
# Computing not^8(t) with repeated applicationnot^2(t) = (λb.λf.λt. b f t) . (λb.λf.λt. b f t) = (λb.λf.λt. b t f)
not^3(t) = (λb.λf.λt. b f t) . (λb.λf.λt. b t f) = (λb.λf.λt. b f t)
not^4(t) = (λb.λf.λt. b f t) . (λb.λf.λt. b f t) = (λb.λf.λt. b t f)
not^5(t) = (λb.λf.λt. b f t) . (λb.λf.λt. b t f) = (λb.λf.λt. b f t)
not^6(t) = (λb.λf.λt. b f t) . (λb.λf.λt. b f t) = (λb.λf.λt. b t f)
not^7(t) = (λb.λf.λt. b f t) . (λb.λf.λt. b t f) = (λb.λf.λt. b f t)
not^8(t) = (λb.λf.λt. b f t) . (λb.λf.λt. b f t) = (λb.λf.λt. b t f)
# Computing not^8(t) with composition by sharingnot^2(t) = (λb.λf.λt. b f t) . (λb.λf.λt. b f t) = (λb.λf.λt. b t f)
not^4(t) = (λb.λf.λt. b t f) . (λb.λf.λt. b t f) = (λb.λf.λt. b t f)
not^8(t) = (λb.λf.λt. b t f) . (λb.λf.λt. b t f) = (λb.λf.λt. b t f)
# Computing not^8(x) with repeated applicationnot^2(x) = not . not = id 
not^3(x) = not . id = not
not^4(x) = not . not = id
not^5(x) = not . id = not
not^6(x) = not . not = id
not^7(x) = not . id = not
not^8(x) = not . not = id
# Computing not^8(x) with composition by sharingnot^2(x) = not . not = id
not^4(x) = id . id = id
not^8(x) = id . id = id

3. Absal performs runtime fusion

Rewrite rules of interaction combinators, a type of interaction net

But what about the negative complexity stuff?

-- Normal form of `inc`:
λa. λb. λc. λd. (((a c) λe. (b λf. λg. λh. (((e g) λi. (f λj.
λk. λl. (((i k) λm. (j m)) l))) h))) d)
-- Normal form of `inc . inc`:
λa. λb. λc. λd. (((a λe. (b λf. λg. λh. (((e g) λi. (f λj. λk
. λl. (((i k) λm. (j m)) l))) h))) λe. (c λf. λg. λh. (((e g)
λi. (f λj. λk. λl. (((i k) λm. (j m)) l))) h))) d)
-- Normal form of `inc . inc . inc`:
λa. λb. λc. λd. (((a λe. (c λf. λg. λh. (((e g) λi. (f λj. λk
. λl. (((i k) λm. (j m)) l))) h))) λe. (b λf. λg. λh. (((e λi
. (f λj. λk. λl. (((i k) λm. (j m)) l))) λi. (g λj. λk. λl. (
((i k) λm. (j m)) l))) h))) d)
--------------------------------------------------------------- Normal form of `copy . inc`:
λa. (((a λb. λc. λd. λe. (d (((b λf. λg. λh. λi. (g (((f λj.
λk. λl. λm. (k j)) λj. λk. λl. λm. (l j)) λj. λk. λl. l))) λf
. λg. λh. λi. (h (((f λj. λk. λl. λm. (k j)) λj. λk. λl. λm.
(l j)) λj. λk. λl. l))) λf. λg. λh. h))) λb. λc. λd. λe. (c (
((b λf. λg. λh. λi. (h (((f λj. λk. λl. λm. (k j)) λj. λk. λl
. λm. (l j)) λj. λk. λl. l))) λf. λg. λh. λi. (g (((f λj. λk.
λl. λm. (l j)) λj. λk. λl. λm. (k j)) λj. λk. λl. l))) λf. λg
. λh. h))) λb. λc. λd. d)
-- Normal form of `copy . inc . inc`:
λa. (((a λb. λc. λd. λe. (c (((b λf. λg. λh. λi. (h (((f λj.
λk. λl. λm. (k j)) λj. λk. λl. λm. (l j)) λj. λk. λl. l))) λf
. λg. λh. λi. (g (((f λj. λk. λl. λm. (l j)) λj. λk. λl. λm.
(k j)) λj. λk. λl. l))) λf. λg. λh. h))) λb. λc. λd. λe. (d (
((b λf. λg. λh. λi. (h (((f λj. λk. λl. λm. (k j)) λj. λk. λl
. λm. (l j)) λj. λk. λl. l))) λf. λg. λh. λi. (g (((f λj. λk.
λl. λm. (l j)) λj. λk. λl. λm. (k j)) λj. λk. λl. l))) λf. λg
. λh. h))) λb. λc. λd. d)
-- Normal form of `copy . inc . inc . inc`:
λa. (((a λb. λc. λd. λe. (d (((b λf. λg. λh. λi. (h (((f λj.
λk. λl. λm. (k j)) λj. λk. λl. λm. (l j)) λj. λk. λl. l))) λf
. λg. λh. λi. (g (((f λj. λk. λl. λm. (l j)) λj. λk. λl. λm.
(k j)) λj. λk. λl. l))) λf. λg. λh. h))) λb. λc. λd. λe. (c (
((b λf. λg. λh. λi. (g (((f λj. λk. λl. λm. (l j)) λj. λk. λl
. λm. (k j)) λj. λk. λl. l))) λf. λg. λh. λi. (h (((f λj. λk.
λl. λm. (l j)) λj. λk. λl. λm. (k j)) λj. λk. λl. l))) λf. λg
. λh. h))) λb. λc. λd. d)
-- Note: using a fixed depth of 3 for better visualization

Conclusion

tl;dr

λf1. λx. 
let f2 = f1 . f1 in
let f4 = f2 . f2 in
let f8 = f4 . f4 in
let f16 = f8 . f8 in
f16 (f4 (f1 x))

tl;dr tl;dr

--

--

--

I’m something that possibly exists

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

NBA playoff win chances via Bayesian inference

HHL: Solving Linear Systems of Equations with Quantum Computing

When Bayes, Ockham, and Shannon come together to define machine learning

Exact Diagonalization Put Briefly.

A Shot of Scotch #4: Göring Gambit | Chess Openings Explained

A Shot of Scotch #4: Göring Gambit | Chess Openings Explained

Scientific Computation using Matlab: Week 1

Understanding Geometric and Inverse Binomial distribution

Monty Hall Problem solved with Python

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Victor Maia

Victor Maia

I’m something that possibly exists

More from Medium

3 Fundamentals of Enums in Rust

Haskell basics: Expressions and Equations

Data Structures in Typescript and Rust with Borsh

Part #2: How to read WASM