The Symmetric Interaction Calculus
(Update: renamed to Symmetric Interaction Calculus.)
This is another post about the Abstract Algorithm. In it, I’ll explain why there is a mismatch between it and the λ-Calculus. I’ll develop a new language on which that mismatch doesn’t exist, the Symmetric Interaction Calculus (SIC). I’ll briefly explain how all terms of that language can be optimally reduced with the Abstract Algorithm, and how all intermediate steps of that reduction correspond to a SIC term. Finally, I’ll hint a direct isomorphism between the SIC and Symmetric Interaction Combinators, rendering the former as a mere textual interpretation of the later. If you want a short specification and explanation, check out the Rust implementation. If you want a wordy dissertation, stay with me as I carefully explain what it means and how I got there.
If you’re out of the loop, the Abstract Algorithm is a machinery capable of evaluating functional programs optimally. It is not only asymptotically faster than JavaScript, Scheme, Haskell or any other language that has lambdas, as explained on my previous post, but it is also actually efficient: we’re reaching 150m rewrites/s in a GTX 1080 with a massively parallel OpenCL implementation, which makes it faster than GHC even for “normal” programs. Finally, it has a clear cost model, which makes it well suited as the foundation of a decentralized VM; a functional counterpart of the EVM.
With so many good things, one might wonder why it was not previously. One of the main reasons is it doesn’t actually evaluate every program of the λ-calculus. For some input programs, it, instead, simply fails to halt, or even returns downright wrong results; in this issue I present an example. Moreover, even λ-terms that succeed to reduce pass through intermediate representations that correspond to no λ-term at all. This suggests a mismatch between the Abstract Algorithm and the λ-calculus. But there are workarounds:
1. Modify the abstract algorithm to cover all λ-terms.
If the abstract algorithm doesn’t cover all terms, can’t we change it so that it does? That sounds like a reasonable solution, but doing so requires extending the graphical representation of λ-terms with new nodes and reduction rules; the so-called “oracle”. As it turns out, after decades of research, nobody figured out an efficient oracle. That is, the asymptotics are the same, but the practical performance of the algorithm goes downhill because rewrite counts are increased by large constants. Here is a visualization:
This table compares the number of graph rewrite rules (thus, time) required to evaluate certain terms in 5 different implementations; 4 of them with some oracle, and one without, here called Absal. The less rewrites, the better. As you can see, the oracle-free version outperforms most implementations by 2 to 3 orders of magnitude. YALE comes close, but its rewrite rules are much more complex, so it is still at least 10x slower in practice. That huge difference makes the whole algorithm too inefficient in practice.
2. Use a subset of the λ-calculus that works.
The proposal is to use the algorithm without an oracle (i.e., incomplete, but efficient), and restrict our term language to only be able to express terms that are compatible with it. The most promising way to do it is to shift to a different underlying logic: Elementary Affine Logic, which essentially stratifies terms in “layers”, preventing a term to duplicate another term in the same level, making it Absal-compatible. Two examples: untyped and typed.
This proposal is particularly interesting because of its nice normalization properties. EAL is not only strongly normalizing, but its complexity is predictable, even for the untyped language. Because of that, a type theory based on EAL could even have type-level recursion without becoming inconsistent! Sadly, programming with EAL is awkward at best. It requires programmers to write explicit duplications with very unfamiliar restrictions. Some common programming idioms are even impossible: nested for-loops, for example. You must instead unroll all loops in your programs. As an illustration, here is addition in EAL Calculus of Constructions:
λ (a : Nat) ->
λ (b : Nat) ->
Λ (P : *) ->
λ (s : ! (P -> P)) ->
let S = s in
let f = a P |S in
let g = b P |S in
| λ z : P ->
f (g z)Compare to the same thing on the pure Calculus of Constructions (Morte):
λ (a : Nat) ->
λ (b : Nat) ->
λ (P : *) ->
λ (S : P -> P) ->
λ (z : P) ->
a P S (b P S)As you can see, the later is much simpler.
3. A new option: rethink the λ-calculus?
So, extending the Abstract Algorithm to cover all lambda terms ruins its efficiency, and restricting the λ-calculus to be Absal-compatible makes it hard to program with. What now?
For one, we know there are things λ-terms can do that Absal can’t. But the converse is also true: there are things Absal can do that λ-terms can’t! For example, it has no problems expressing abstractions whose variables occur outside of their own bodies, which makes no sense on the λ-calculus. Here is an idea: what if, instead of restricting the λ-calculus to the subset that works with Absal, we fundamentally changed it, making both systems match perfectly? That’s what I’ll do here.
But, before, let’s forget the Abstract Algorithm altogether and try an exercise. Imagine you took a time machine all the way to 1928 and was in charge of inventing λ-calculus, but, this time, with one constraint: reduction rules must be constant-time operations. How would you do it?
Developing a new λ-calculus
To restate our mission, we’re back to 1928 and we’ll try to implement the λ-calculus; that is, a general model of computation based on the notion of functions and substitutions; as if we were its original inventors, except we’re constrained to only use constant-time operations. We’ll completely ignore the abstract algorithm and develop such calculus by itself.
1. Starting point: affine λ-calculus
Let’s start by defining a syntax with functions, variables and function application:
term
= λx. term -- function
| (term term) -- application
| x -- variableAnd now let’s define a reduction rule for λ-application:
Lambda application:
((λx. body) arg) ~> body[x <~ arg]a ~> b means a reduces to b
a[b <~ c] means all occurrences of b in a are replaced by c
And, well, that’s it. We invented the λ-calculus. Damn, that was easy. But that doesn’t complete our mission. Application, as defined, is not a constant-time operation. First, because the substitution procedure must traverse over body, which can have any arbitrary size. Second, because it must fully copy arg for each occurrence of x. If implemented naively, that’s a quadratic amount of work. Beta-reduction does way too many things at the same time and, thus, isn’t allowed.
Here is a quick solution: let’s only allow variables to occur once. This allows two optimizations: first, the λ can keep a pointer to the occurrence of its variable, so, there’s no need for a traversal. Second, since the variable only occurs once, we can merely redirect the reference of var to point to arg. That makes application a constant-time operation! As an example, here is the full execution of fst (1, 2):
(λp. p (λa. λb. a)) (λt. t 1 2)
------------------------------- lambda application
(λt. t 1 2) (λa. λb. a)
----------------------- lambda application
(λa. λb. a) 1 2
--------------- lambda application
(λb. 1) 2
--------- lambda application
12. Going scopeless
The language we have so far is the Affine λ-calculus, and it is a subset of both the λ-calculus and the SIC. Now, paths will diverge, as we’ll do something the λ-calculus is not capable of. Recall our definition of application:
Lambda application:
((λx. body) arg) ~> body[x <~ arg]a ~> b means a reduces to b
a[b <~ c] means all occurrences of a in b are replaced by c
Previously, it meant that every occurrence of x was replaced by arg inside body. But since now there is only one occurrence of var, then applications merely move something to another location. If that is the case, lambdas act more like “redirectors” than “functions”. As such, one might wonder: what if we allowed x to occur outside of the function body? That’s what we’ll do, updating the definition of application to:
Lambda application:
((λx. body) arg) ~> body
x <~ arga ~> b means a reduces to b
a <~ b means a is replaced by b
Does that break the world? Not really. It is still a computing model with unambiguous reduction rules. We just removed the notion of scope. As soon as a function is applied to an argument, the occurrence of its variable is replaced by an argument, wherever that argument is, even outside itself. Here is an example:
λt. t a b ((λa. λb. λc. c) 1 2 3)
--------------------------------- lambda application
λt. t 1 b ((λb. λc. c) 2 3)
--------------------------- lambda application
λt. t 1 2 ((λc. c) 3)
--------------------- lambda application
λt. t 1 2 3Notice how the first two applications of the inner function moved its argument to outside its own body. At this point, you may be asking why, to which I reply, why do we even had a scope to begin with? One may argue adding it is an arbitrary, artificial limitation. In any case, there seems to be no other way: see this S.O. question to understand. Either we give up of lambdas, duplications, constant-time operations or closed scopes. To have the first 3, closed scopes must be abandoned.
3. Copying
The language we have so far is quite weird. In a sense, it is more powerful than the λ-calculus, because applications can move arguments to outside the function’s scope. Yet, it is much less powerful, because of the lack of duplication. In fact, it is not even Turing-complete and terminates after a constant number of applications. As such, it doesn’t work as a general model of computation, which is what we’re aiming for. How can we improve that?
3.a. Global definitions
Let’s first try extending our language with a primitive for global definitions:
term
= λx. term -- function
| (term term) -- application
| x -- variable
| x = term -- definitionLambda application:
((λx. body) arg) ~> body
x <~ argCopy:
x = t ~>
all x <~ ta ~> b means a reduces to b
a <~ b means a is replaced by b
That is, we now have an additional syntax, x = t, which, in the same “scopeless” vibe, globally replaces all occurrences of x by t. This gives us freedom to duplicate anything, anywhere! Here is an example of it in action:
term = λf. λx. f x
λt. t term term
--------------- global copy
λt. t (λf. λx. f x) (λf. λx. f x)That is, in order to copy the term λf. λx. f x, we simply gave it a name, then used that name twice on the main term. Obviously, we can’t actually do that, as we already agreed copying isn’t a constant-time operation. What now?
3.b. Incremental copy
Here’s the plan: let’s instead copy incrementally. Mind this example:
term = λf. λx. f x
λt. t term term
---------------
term = λx. f x
λt. t (λf. term) (λf. term)Here, we took a single λf out of the term = ... line, and duplicated it before each occurrence of term. That’s a good start, but now there are two λf. Having two lambdas with the same variable is a problem because applying one will force the other to be applied the same thing, and leaves a hanging λf with no matching occurrence. That’s a bug. To fix that, let’s rename the introduced variables:
term = λf. λx. f x
λt. t term term
--------------- lambda copy
term = λx. f x
λt. t (λf0. term) (λf1. term)That’s better, but what about the occurrence of f? Now it is left unbound. We could replace it by f0, but then f1 would be unbound. If we replace it by f1, then f0 would be unbound. Either way that’d be a bug. The problem here is that, after copying a λ, the “same” bound variable will exist in two different places, but its occurrence remains in a single place. What we need here is a way to reverse duplication. That is, since a duplication allows one lambda to be in two places at the same time, then we need a way to store two variables in one place at the same time.
3.c. The superposition primitive
To solve this issue, we’ll introduce a last primitive to our language, superposition, which is represented by A & B.
term
= λx. term -- function
| (term term) -- application
| x -- variable
| x = term -- definition
| term & term -- superpositionThen, in order to incrementally copy a lambda λf, we first rename its bound variables, duplicate it as λf0 and λf1, move each copy to its target location, and then replace the variable f by f0 & f1, which means it is now linked to two lambdas at the same time. We also restrict x in a definition to occur at most twice, otherwise duplication wouldn’t be a constant-time operation anymore. Here’s the written rule:
Lambda copy:
(v = λx. body) ~> v = body
v <~ (λx0. v)
v <~ (λx1. v)
x <~ (x0 & x1)As bizarre as it may look, think of it as imaginary numbers. Remember how i was defined as sqrt(-1) in order to make algebra complete and allow every polynomial have a root? Here, superposed A & B was defined to make our reduction complete and allow every term to have reduction. Both constructs make no intuitive sense, but are nether less useful to make formulas work, and are eventually cancelled out. Note that v appears twice here to reflect the fact it can occur twice. With it, we can proceed with our reduction:
term = λf. λx. f x
λt. t term term
--------------- lambda copy
term = λx. (f0 & f1) x
λt. t (λf0. term) (λf1. term)
----------------------------- lambda copy
term = (f0 & f1) (x0 & x1)
λt. t (λf0. λx0. term) (λf1. λx1. term)Except now we are already stuck. There is now a superposed application of (f0 & f1) to (x0 & x1). So, what happens when we apply two superposed functions to a single argument? Right: we get a superposed application of each function to two copies of the argument! Makes sense, no?
Sobreposed application:
((f0 & f1) x) ~> f0 K & f1 K
<~ K = xWith that, we can move on:
term = λf. λx. f x
λt. t term term
--------------- lambda copy
term = λx. (f0 & f1) x
λt. t (λf0. term) (λf1. term)
----------------------------- lambda copy
term = (f0 & f1) (x0 & x1)
λt. t (λf0. λx0. term) (λf1. λx1. term)
--------------------------------------- superposed application
K = x0 & x1
term = f0 K & f1 K
λt. t (λf0. λx0. term) (λf1. λf1. term)Now we’re stuck with two superposed copies. How do we copy two superposed values? There are two reasonable answers: either we copy the superposition, which may lead to a super-superposition, or we undo the superposition, moving each superposed value to each target location. For now, that’s what we’ll do:
Superposed copy:
(v = x0 & x1) ~>
v <~ x0
v <~ x1With this, we can further proceed:
term = λf. λx. f x
λt. t term term
--------------- lambda copy
term = λx. (f0 & f1) x
λt. t (λf0. term) (λf1. term)
----------------------------- lambda copy
term = (f0 & f1) (x0 & x1)
λt. t (λf0. λx0. term) (λf1. λx1. term)
--------------------------------------- superposed application
K = x0 & x1
term = f0 K & f1 K
λt. t (λf0. λx0. term) (λf1. λx1. term)
--------------------------------------- superposed copy
term = f0 x0 & f1 x1
λt. t (λf0. λx0. term) (λf1. λx1. term)
--------------------------------------- superposed copy
λt. t (λf0. λx0. f0 x0) (λf1. λx1. f1 x1)And now we’re done! The result is the same we got with the global copy , except now it was done incrementally with O(1) operations. The Symmetric Interaction Calculus is now complete. Here is the whole thing:
The Symmetric Interaction Calculusterm
= λx. term -- function
| (term term) -- application
| x -- variable
| x = term -- definition
| term & term -- superpositionLambda application:
((λx. body) arg) ~> body
x <~ argSuperposed application:
((f0 & f1) x) ~> f0 K & f1 K
<~ K = xLambda copy:
(v = λx. body) ~> v = body
v <~ (λx0. v)
v <~ (λx1. v)
x <~ (x0 & x1)Superposed copy:
(v = x0 & x1) ~>
v <~ x0
v <~ x1a ~> b means a reduces to b
a <~ b means a is replaced by b
As you can see, this calculus was developed independently, with no relationship to the abstract algorithm at all. Each part of the language was added as either an intuitive reasoning or an immediate need. One could argue that Alonzo Church could have come up with this instead of the λ-calculus, if only he was constrained by having only constant-time operations. Or perhaps that’s a bit of a stretch, but I’d still argue this is calculus is very unartificial.
Relationship to Absal and Interaction Combinators
As you could expect, that new take on the λ-calculus is fully compatible with the Abstract Algorithm, i.e., every one of its term can be reduced. The reason is that the problematic scenario, i.e., a “duplication of a duplication”, is “solved” by simply considering it part of the semantics of the language. That is, when a duplication node duplicates itself on the interaction net, that’s not an error anymore, but has an meaning: it merely undoes the superposed expression a & b. This is what allows Absal to always output the correct reduction of a SIC input. Not only that, but every intermediate steps of the interaction net reduction correspond to a single textual term.
That calculus is also quite powerful, being Turing-complete. That’s because it is directly isomorphic to Symmetric Interaction Combinators. If you haven’t read that paper, I’d strongly suggest you to, as that is, in my opinion, the most elegant model of computation I’ve seen. That means every Symmetric Interaction Net can be interpreted as an SIC term, and vice-versa; and each graph rewrite corresponds to one rule on the calculus.
Note that, since there is no rule to duplicate a superposed value, SIC corresponds to the abstract algorithm with only one “fan” node. That is, it is impossible to duplicate a duplication. To make it more powerful, we could just extend definitions and superpositions with labels. That’d allow us to duplicate duplications (and to have layers of superposed superpositions), giving us all the sharing power I’ve observed in my previous posts.
I’d love to show how all of it works with some animations, and to attempt writing some proofs, but this story is already quite big as is and I’m quite tired at this point. If you wanna hear more about this, feel free to follow me on Twitter. It is quite dead right now, but I’ll be using it whenever I have something new to show off. All in all, I’m really glad to have figured out a way to use the abstract algorithm that is superior to “write a λ-term and hope it works”. Here is a working implementation. For fun, here is the full reduction of a recursive Scott-encoded 2*2, each section corresponding to a single step:
b = λc.λd.(c λe.λf.(e λg.λh.h))
a = λi.((i λj.λk.λl.(k λm.λn.(m (a j)))) λo.λp.p)
(a b)
----------------
c = λd.λe.(d λf.λg.(f λh.λi.i))
b = (((j & a) λk.λl.λm.(l λn.λo.(n (λp.b k)))) λp.λq.q)
(λa.b c)
----------------
a = (((b & c) λd.λe.λf.(e λg.λh.(g (λi.a d)))) λi.λj.j)
c = λk.λl.(k λm.λn.(m λo.λp.p))
a
----------------
a = (((b c) & (d c)) λe.λf.f)
d = λg.λh.(g λi.λj.(i λk.λl.l))
c = λm.λn.λo.(n λp.λq.(p (λr.a m)))
a
----------------
a = (((b c) d) & ((e c) d))
e = λf.λg.(f λh.λi.(h λj.λk.k))
d = λl.λm.m
c = λn.λo.λp.(o λq.λr.(q (λs.a n)))
a
----------------
c = λd.λe.e
b = λf.λg.λh.(g λi.λj.(i (λk.((k b) c) f)))
a = λl.λm.(l λn.λo.(n λp.λq.q))
((a b) c)
----------------
d = λe.λf.f
c = λg.λh.λi.(h λj.λk.(j (λl.((l c) d) g)))
b = λm.((a & n) λo.λp.(o λq.λr.r))
((λa.b c) d)
----------------
b = λc.λd.d
a = λe.((f & g) λh.λi.(h λj.λk.k))
f = λl.λm.λn.(m λo.λp.(o (λq.((q f) b) l)))
(a b)
----------------
c = λd.λe.e
b = ((f & g) λh.λi.(h λj.λk.k))
f = λl.λm.λn.(m λo.λp.(o (λq.((q f) c) l)))
(λa.b c)
----------------
a = ((b & c) λd.λe.(d λf.λg.g))
b = λh.λi.λj.(i λk.λl.(k (λm.((m b) n) h)))
n = λo.λp.p
a
----------------
a = ((b c) & (d c))
c = λe.λf.(e λg.λh.h)
b = λi.λj.λk.(j λl.λm.(l (λn.((n b) o) i)))
o = λp.λq.q
a
----------------
b = λc.λd.(c λe.λf.f)
a = λg.λh.λi.(h λj.λk.(j (λl.((l a) m) g)))
m = λn.λo.o
(a b)
----------------
c = λd.λe.(d λf.λg.g)
b = λh.λi.(h λj.λk.(j (λl.((l λm.b) n) (m & a))))
n = λo.λp.p
(λa.b c)
----------------
a = λb.λc.(b λd.λe.(d (λf.((f λg.a) h) (g & i))))
i = λj.λk.(j λl.λm.m)
h = λn.λo.o
a
----------------
b = λc.((d & a) λe.λf.(e (λg.((g λh.λi.b) i) (h & j))))
j = λk.λl.(k λm.λn.n)
i = λo.λp.p
λa.b
----------------
b = λc.((d e) & (a e))
e = λf.λg.(f (λh.((h λi.λj.b) j) (i & k)))
k = λl.λm.(l λn.λo.o)
j = λp.λq.q
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e & g) (λi.((i λj.λk.b) k) (j & l)))
l = λm.λn.(m λo.λp.p)
k = λq.λr.r
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e i) & (g i))
i = (λj.((j λk.λl.b) l) (k & m))
m = λn.λo.(n λp.λq.q)
l = λr.λs.s
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e i) & (g i))
i = (((j & k) λl.λl.b) l)
l = λm.λn.n
k = λo.λp.(o λq.λr.r)
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e i) & (g i))
i = (((j k) & (l k)) m)
m = λn.λo.o
l = λp.λq.(p λr.λs.s)
k = λt.λt.b
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e i) & (g i))
i = (((j k) l) & ((m k) l))
m = λn.λo.(n λp.λq.q)
l = r
r = λs.λt.t
k = λu.λu.b
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e ((i j) k)) & (g ((l j) k)))
l = λm.λn.(m λo.λp.p)
k = q
q = λr.λs.s
j = λt.λt.b
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e ((i j) k)) & (g ((λl.m j) k)))
m = λn.((l & o) λp.λq.q)
k = r
r = λs.λt.t
j = λu.λu.b
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e ((i j) k)) & (g (l k)))
l = λm.((j & n) λo.λp.p)
k = q
q = λr.λs.s
j = λt.λt.b
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e ((i j) k)) & (g (λl.m k)))
m = ((j & n) λo.λp.p)
k = q
q = λr.λs.s
j = λt.λt.b
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e ((i j) k)) & (g l))
l = ((j & m) λn.λo.o)
k = p
p = λq.λr.r
j = λs.λs.b
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e ((i j) k)) & (g l))
l = ((j m) & (n m))
m = λo.λp.p
k = q
q = λr.λs.s
j = λt.λt.b
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e ((i j) k)) & (g (j l)))
l = λm.λn.n
k = o
o = λp.λq.q
j = λr.λr.b
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e (((i & j) λk.k) l)) & (g (λm.k m)))
m = λn.λo.o
l = p
p = λq.λr.r
k = λs.b
λa.b
----------------
b = λc.((d λe.f) & (a λg.f))
f = λh.((e (((i & j) λk.k) l)) & (g k))
l = m
m = λn.λo.o
k = λp.b
j = λp.λq.q
λa.b
----------------
b = λc.(((d & e) λf.g) & (a λh.g))
g = λi.((f (((j & k) λl.λl.l) m)) & (h λn.l))
m = n
n = λo.λp.p
l = b
k = λq.λr.r
λa.b
----------------
b = λc.(((d e) & (f e)) & (a λg.h))
h = λi.((j (((k & l) λm.λm.m) n)) & (g λo.m))
n = o
o = λp.λq.q
m = b
l = λr.λs.s
e = λt.h
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e & h) (((l & m) λn.λn.n) o)) & (i λp.n))
o = p
p = λq.λr.r
n = b
m = λs.λt.t
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e l) & (h l)) & (i λm.m))
m = b
l = (((n & o) λp.λp.m) p)
p = q
q = λr.λs.s
o = λt.λu.u
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e l) & (h l)) & (i λm.m))
m = b
l = (((n o) & (p o)) q)
q = r
r = λs.λt.t
p = λu.λv.v
o = λw.λw.m
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e l) & (h l)) & (i λm.m))
m = b
l = (((n o) p) & ((q o) p))
q = λr.λs.s
p = t
t = u
u = λv.λw.w
o = λx.λx.m
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) n)) & (h ((o m) n))) & (i λp.p))
p = b
o = λq.λr.r
n = s
s = t
t = λu.λv.v
m = λw.λw.p
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) n)) & (h ((λo.p m) n))) & (i λq.q))
q = b
p = λr.r
n = s
s = t
t = λu.λv.v
m = λw.λw.q
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) n)) & (h (o n))) & (i λp.p))
p = b
o = λq.q
n = r
r = s
s = λt.λu.u
m = λv.λv.p
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) n)) & (h (λo.p n))) & (i λq.q))
q = b
p = (o & r)
n = s
s = t
t = λu.λv.v
m = λw.λw.q
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) n)) & (h o)) & (i λp.p))
p = b
o = (n & q)
n = r
r = s
s = λt.λu.u
m = λv.λv.p
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) n)) & (h n)) & (i λo.o))
o = b
n = p
p = q
q = λr.λs.s
m = λt.λt.o
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) n)) & (h n)) & (i λo.o))
o = b
n = p
p = λq.r
r = λs.s
m = λt.λt.o
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) n)) & (h n)) & (i λo.o))
o = b
n = λp.q
q = r
r = λs.s
m = λt.λt.o
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.o)) & (h λp.o)) & (i λq.q))
q = b
o = r
r = s
s = λt.t
m = λu.λu.q
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.o)) & (h λp.o)) & (i λq.q))
q = b
o = r
r = s
s = λt.t
m = λu.λu.q
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.o)) & (h λp.o)) & (i λq.q))
q = b
o = r
r = s
s = λt.t
m = λu.λu.q
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.o)) & (h λp.o)) & (i λq.q))
q = b
o = r
r = s
s = λt.t
m = λu.λu.q
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.o)) & (h λp.o)) & (i λq.q))
q = b
o = r
r = s
s = λt.t
m = λu.λu.q
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.o)) & (h λp.o)) & (i λq.q))
q = b
o = r
r = s
s = λt.t
m = λu.λu.q
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.o)) & (h λp.o)) & (i λq.q))
q = b
o = r
r = s
s = λt.t
m = λu.λu.q
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.o)) & (h λp.o)) & (i λq.q))
q = b
o = r
r = λs.t
t = (s & u)
m = λv.λv.q
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.o)) & (h λp.o)) & (i λq.q))
q = b
o = λr.s
s = t
t = ((r & u) & v)
m = λw.λw.q
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.λo.p)) & (h λq.λr.p)) & (i λs.s))
s = b
p = t
t = u
u = (((o & r) & v) & w)
m = λx.λx.s
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.λo.p)) & (h λq.λr.p)) & (i λs.s))
s = b
p = t
t = ((o & r) & u)
m = λv.λv.s
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.λo.p)) & (h λq.λr.p)) & (i λs.s))
s = b
p = (o & r)
m = λt.λt.s
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.j))
j = λk.(((e ((l m) λn.λo.o)) & (h λp.λq.q)) & (i λr.r))
r = b
m = λs.λs.r
f = j
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.λj.k))
k = (((e ((l m) λn.λo.o)) & (h λp.λq.q)) & (i λr.r))
r = b
m = λs.λs.r
f = λs.k
λa.b
----------------
b = λc.(((d λe.f) & (g λh.f)) & (a λi.λj.(i λk.k)))
k = b
f = λl.((e ((m n) λo.λp.p)) & (h λq.λr.r))
n = λs.λs.k
λa.b
----------------
b = λc.(((d λe.λf.g) & (h λi.λj.g)) & (a λk.λl.(k λm.m)))
m = b
g = ((e ((n o) λp.λq.q)) & (i λr.λs.s))
o = λt.λt.m
λa.b
----------------
b = λc.(((d λe.λf.(e ((g h) λi.λj.j))) & (k λl.λm.(l λn.λo.o))) & (a λp.λq.(p λr.r)))
r = b
h = λs.λs.r
λa.b
----------------
b = λc.(((d λe.λf.(e ((g h) λi.λj.j))) & (k λl.λm.(l λn.λo.o))) & (a λp.λq.(p λr.r)))
r = b
h = λs.λs.r
λa.b
----------------
b = λc.(((d λe.λf.(e ((g h) λi.λj.j))) & (k λl.λm.(l λn.λo.o))) & (a λp.λq.(p λr.r)))
r = b
h = λs.λs.r
λa.b
----------------
b = λc.(((d λe.λf.(e ((g h) λi.λj.j))) & (k λl.λm.(l λn.λo.o))) & (a λp.λq.(p λr.r)))
r = b
h = λs.λs.r
λa.b
----------------
b = λc.(((d λe.λf.(e ((g h) λi.λj.j))) & (k λl.λm.(l λn.λo.o))) & (a λp.λq.(p λr.r)))
r = b
h = λs.λs.r
λa.b
----------------
c = (((d λe.λf.(e ((g h) λi.λj.j))) & (k λl.λm.(l λn.λo.o))) & (a λp.λq.(p λr.r)))
r = λs.c
h = λt.λt.r
λa.λb.c
----------------
f = λg.((h λi.λj.(i ((k l) λm.λn.n))) & (e λo.λp.(o λq.λr.r)))
l = λs.λs.f
λa.λb.(a λc.λd.(c λe.f))
----------------
g = ((h λi.λj.(i ((k l) λm.λn.n))) & (e λo.λp.(o λq.λr.r)))
l = λs.λs.λs.g
λa.λb.(a λc.λd.(c λe.λf.g))
----------------
λa.λb.(a λc.λd.(c λe.λf.(e λg.λh.(g λi.λj.j))))