6 files changed, 89 insertions, 31 deletions
diff --git a/docs/index.html b/docs/index.html
index a66c96c..4b5bc6e 100644
--- a/docs/index.html
+++ b/docs/index.html
@@ -57,11 +57,14 @@
 
       <div class="left">
         <pre class="code">
-<span class="repl">></span> <span class="com">:time</span> <span class="symbol">factorial</span> <span class="ternary">(+30)</span>
-<span class="time">0.15 seconds</span></pre>
+<span class="repl">></span> <span class="com">:time</span> <span class="symbol">factorial</span> <span class="ternary">(+42)</span>
+<span class="time">0.01 seconds</span></pre>
       </div>
       <div class="right">
-        <p>Efficient call-by-need reduction using abstract machines.</p>
+        <p>
+          <a href="wiki/technical/performance/">Efficient</a> reduction using
+          abstract machines and higher-order encodings.
+        </p>
       </div>
 
       <div class="left">
@@ -90,10 +93,29 @@ hello world!</pre
       </div>
       <div class="right">
         <p>
-          Compilation to Tromp's binary lambda calculus.<br />
+          <a href="wiki/coding/compilation/">Compilation</a> to Tromp's binary
+          lambda calculus.<br />
           Support for byte and ASCII encoding.
         </p>
       </div>
+
+      <div class="left">
+        <p>
+          <a href="wiki/coding/meta-programming/">Meta-programming</a><br />
+          and self-interpretation.
+        </p>
+      </div>
+      <div class="right">
+        <pre class="code">
+<span class="repl">></span> <span class="symbol">length</span> <span class="meta">`</span><span class="symbol">factorial</span>
+<span class="repl">></span> <span class="mixfix">!</span><span class="left-app">(</span><span class="symbol">swap</span> <span class="meta">`</span><span class="left-app">(</span><span class="unary">(+2u)</span> <span class="unary">(+3u)</span><span class="right-app">))</span>
+<span class="repl">></span> <span class="symbol">lhs</span> <span class="left-app">(</span><span class="symbol">blc→meta</span> <span class="string">"010000100000110"</span><span class="right-app">)</span></span>
+</pre>
+        <!-- <span class="repl">></span> <span class="mixfix">∏</span> <span class="ternary">(+1)</span> <span class="mixfix">→</span> <span class="ternary">(+3)</span> <span class="mixfix">|</span> <span class="symbol">++‣</span> -->
+        <!-- <span class="repl">></span> <span class="symbol">number!</span> <span class="mixfix"><$></span> <span class="left-app">(</span><span class="symbol">lines</span> <span class="string">"42\n25"</span><span class="right-app">)</span> -->
+        <!-- <span class="repl">></span> <span class="term"><span class="symbol">sum</span> (<span class="symbol">take</span> <span class="ternary">(+3)</span> (<span class="symbol">repeat</span> <span class="ternary">(+4)</span>))</span> -->
+        <!-- <span class="repl">></span> <span class="binary">(+10b)</span> <span class="mixfix">⋀!</span> <span class="binary">(+12b)</span></pre> -->
+      </div>
     </div>
 
     <div class="bar big">
diff --git a/docs/script.js b/docs/script.js
index 5859c55..0b147f5 100644
--- a/docs/script.js
+++ b/docs/script.js
@@ -37,6 +37,7 @@ describe("header", "[0] is the identity operation. It returns the first argument
 describe("index", "This number references the nth abstraction, starting counting from the inside. These 'De Bruijn indices' replace the concept of variables in lambda calculus.");
 describe("left-abs", "The opening bracket of a function abstraction. It's basically the equivalent of the λ in lambda calculus.");
 describe("left-app", "The opening bracket of a function application.");
+describe("meta", "This is the quote operator. It converts any given expression to bruijn's meta encoding. The meta encoding can be used for self modification and can be turned back to normal bruijn code.");
 describe("mixfix", "This is a mixfix operator. They can be defined like …*… where the … can then be any other term. You can use them without the … as a notation of function application.");
 describe("repl", "This indicates a REPL input.");
 describe("right-abs", "The closing bracket of a function abstraction.");
@@ -46,5 +47,6 @@ describe("string", "Syntactic sugar for a list of binary encoded chars.")
 describe("symbol", "This substitutes a previously defined term (for example from the standard library).");
 describe("ternary", "Syntactic sugar for a balanced ternary number representation using abstractions as data. Needs a sign and brackets to differentiate it from De Bruijn indices.");
 describe("time", "Incredibly fast for lambda calculus standards.");
+describe("unary", "Syntactic sugar for a unary number representation using abstractions as data. This is commonly also known as a Church numeral. Needs a sign and brackets to differentiate it from De Bruijn indices.");
 
 document.body.addEventListener("click", clearPopups, true)
diff --git a/docs/style.css b/docs/style.css
index 1739f58..60e8fe5 100644
--- a/docs/style.css
+++ b/docs/style.css
@@ -180,7 +180,7 @@ a {
 	color: #ff64bd;
 }
 
-.code .ternary, .code .binary {
+.code .ternary, .code .binary, .code .unary {
 	color: #b1ee13;
 }
 
@@ -199,3 +199,7 @@ a {
 .code .index {
 	color: #ff5050;
 }
+
+.code .meta {
+	color: #ff94ff;
+}
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