Added higher order reducer

3 files changed, 56 insertions, 26 deletions

diff --git a/docs/wiki_src/introduction/philosophy.md b/docs/wiki_src/introduction/philosophy.md
new file mode 100644
index 0000000..4c70a94
--- /dev/null
+++ b/docs/wiki_src/introduction/philosophy.md
@@ -0,0 +1,8 @@
+# Philosophy
+
+-   minimal, proven core
+-   small, expressive functions
+-   style consistency
+-   API consistency
+-   implicit parallelisation
+-   shared evaluation
diff --git a/docs/wiki_src/technical/performance.md b/docs/wiki_src/technical/performance.md
index 002a6b8..709affe 100644
--- a/docs/wiki_src/technical/performance.md
+++ b/docs/wiki_src/technical/performance.md
@@ -1,24 +1,18 @@
 # Performance
 
-The reduction of lambda calculus is (practically) not very efficient. As
-an extension, bruijn also suffers from bad performance.
+In general, the reduction of practical programs encoded in lambda
+calculus is not very efficient when compared to traditional programming
+languages. We do, however, work a lot on making the performance as
+comparable as possible:
 
-Bruijn's interpreter works by substituting the entire program into one
-huge lambda calculus term that will then get reduced by the
-[reducer](reduction.md). As a result, many equivalent terms get
-evaluated multiple times (although some of this is solved by bruijn's
-call-by-need reduction strategy). We currently work on a solution that
-reduces all equivalent terms as one, which turns out is not actually
-that trivial. Follow the [blog](https://text.marvinborner.de) to keep up
-to date with the development.
-
-Aside from that, bruijn is still much faster than most of the hobby
-programming languages based on pure lambda calculus. This is because of
-the [RKNL reducer](reduction.md) and our choice of default [number/byte
-encodings](../coding/data-structures.md).
-
-``` bruijn
-> :import std/Math .
-> :time fac (+30)
-0.15 seconds
-```
+-   We have different reducers and constantly benchmark and improve them
+    in order to find the most efficient method of reduction. Read more
+    about our [reducer choices](reduction.md).
+-   Bruijn uses efficient data structures by default. For example, for
+    nary numbers we use results of Torben Mogensens investigations (as
+    described in [number/byte encodings](../coding/data-structures.md)).
+-   The lambda calculus optimizers
+    [BLoC](https://github.com/marvinborner/bloc) and
+    [BLoCade](https://github.com/marvinborner/blocade) are directly
+    integrated into bruijn and can be enabled optionally (see
+    [compilation](../coding/compilation.md))
diff --git a/docs/wiki_src/technical/reduction.md b/docs/wiki_src/technical/reduction.md
index 97bd78f..ef21180 100644
--- a/docs/wiki_src/technical/reduction.md
+++ b/docs/wiki_src/technical/reduction.md
@@ -1,10 +1,38 @@
 # Reduction
 
-Bruijn uses the RKNL abstract machine reducer[^1]. RKNL uses the
-call-by-need reduction strategy, similar to Haskell and other functional
-programming languages. For you this means that you have efficient
-support for [laziness](../coding/laziness.md) with generally less
-redundant reductions.
+Bruijn supports several reducers that can be chosen using its
+`--reducer` flag.
+
+## HigherOrder [`(source)`](https://github.com/marvinborner/bruijn/blob/main/src/Reducer/HigherOrder.hs)
+
+HigherOrder reduction is one of the simplest reducers. By translating
+the entire expression to a higher-order representation, we can abuse
+Haskell's internal reduction implementation in our favour. Aside from
+conversion from/to the higher-order encoding, this reducer does
+basically nothing special.
+
+## RKNL [`(source)`](https://github.com/marvinborner/bruijn/blob/main/src/Reducer/RKNL.hs)
+
+RKNL[^1] is an abstract machine for reducing lambda calculus. It uses
+the call-by-need reduction strategy, similar to Haskell and other
+functional programming languages. For you this means that you have
+efficient support for [laziness](../coding/laziness.md) with generally
+less redundant reductions.
+
+## ION [`(source)`](https://github.com/marvinborner/bruijn/blob/main/src/Reducer/ION.hs)
+
+[The ION machine](https://crypto.stanford.edu/~blynn/compiler/ION.html)
+was created by Benn Lynn as a reducer for a hypothetical functional
+stack machine computer. We convert the lambda calculus term to
+combinatory logic using [Kiselyov
+translation](https://crypto.stanford.edu/~blynn/lambda/kiselyov.html),
+set up a "virtual" machine with the combinators, and let it run until
+the stack has reached its end.
+
+Most of the work was done by John Tromp in his
+[nf.c](https://github.com/tromp/AIT/commits/master/nf.c). The
+translation to Haskell and its integration into bruijn was mainly done
+as an experiment on performance.
 
 [^1]: [Biernacka, Małgorzata, Witold Charatonik, and Tomasz Drab. "A
     simple and efficient implementation of strong call by need by an