+
+ Before | After |
+
+ Control | Env | Stack | Control | Env | Stack |
+
+
+ Const i : c | e | s | c | e | i : s |
+
+
+ Global i : c | e | s | c | e | Globals[i] : s |
+
+
+ Local i : c | e | s | c | e | e[i] : s |
+
+
+ Closure n a : $c_1$ ... $c_n$ : c | e | s | c | e | Closure a {e} [$c_1$ ... $c_n$] : s |
+
+
+ App : c | e | Closure {e'} [c'] : v : s | c' | v : e' | Closure$^0$ {e} [c] : s |
+
+
+ App : c | e | Closure$^n$ {e'} [c'] : v : s | c | e | Closure$^{n - 1}$ {v : e'} [c'] : s |
+
+
+ Ret : c | e | v : Closure$^0$ \{e'\} [c'] : s | c' | e' | v : s |
+
+
+ Dup : c | e | v : s | c | e | v : v : s |
+
+
+ Add : c | e | v : s | c | e | v + v : s |
+
+
+
+### An example
+
+Consider the following lambda expression:
+
+$(\lambda f.\lambda g.\lambda x. f(gx)) (\lambda x. x + 1) (\lambda x. x + 1) 0$
+
+It composes a lambda which increments its input by one with an identical lambda and then applies 0 to the result. In order to run this on our SECD machine it must first be rewritten with De Brujin index notation.
+
+$(\lambda \lambda \lambda \#2(\#1\#0)) (\lambda 1 + \#1) (\lambda 1 + \#1)0$
+
+Now in order to create an instruction tape for the SECD machine it must be rewritten, using Closure as lambdas, Local $\#i$ for variables and keeping in mind to explicitly apply to and return from lambdas. Additionally it will have to be written in postfix form due to the nature of stack based machines. After performing these actions the expression has been transformed into the following tape:
+
+$Const 0 : Closure [ Const 1 : Local \#0 : Add : Ret ] : Closure [ Const 1 : Local \#0 : Add : Ret ] :$
+$Closure^3 [ Local \#0 : Local \#1 : App : Local \#2 : App : Ret ] : App : App : App$
+
+Reading this (or one of the previous lambda expressions) backwards you should be able to convince yourself of the validity of this translation.
+
+This can now directly be translated into a list of instructions for the Haskell machine implementation.
+
+```
+[ Const 0, Closure 1 4, Const 1, Local 0, Add, Ret, Dup
+, Closure 3 6, Local 0, Local 1, App, Local 2, App, Ret
+, App, App, App]
+```
+
+Which can then be evaluated in order to yield the normalized expression.
+```
+λ eval [] [ Const 0, Closure 1 4, Const 1, Local 0, Add, Ret, Dup
+ , Closure 3 6, Local 0, Local 1, App, Local 2, App, Ret
+ , App, App, App]
+
+[I 2]
+```
+
+As expected, the expression reduces to 2.
+
+## What's next?
+
+In the future I plan to create a specification for an instruction set which allows for meaningful computations as well as IO. Then I wish to define an instruction encoding and binary object file format. Once all this is done an efficient C implementation could be written. Ideally I would also write a compiler to said binary format from something a bit user friendlier. Perhaps an untyped, or simply typed lambda calculus.
+
+## The Haskell source
+
+The implementation itself is trivial and is little more than a Haskell translation of the instruction table above. It's ugly, it doesn't do error handling and is little more than a demonstration piece.
+
+```
+module SECD where
+
+data Inst
+ = Const Int
+ | Global Int
+ | Local Int
+ | Closure Int Int -- args, scope
+ | App
+ | Ret
+ | Dup
+ | Add
+ deriving (Eq, Show)
+
+data Val
+ = I Int
+ | Clo Int [Val] [Inst] -- args env code
+ deriving (Eq, Show)
+
+vadd :: Val -> Val -> Val
+vadd (I x1) (I x2) = I (x1 + x2)
+vadd _ _ = error "attempted addition with closure"
+
+data SEC = SEC [Val] [Val] [Inst] [Val] -- stack, environment, control, global
+ deriving Show
+
+-- | Takes a global env, a list of instructions and returns and int
+eval :: [Val] -> [Inst] -> [Val]
+eval globals insts = go (SEC [] [] insts globals)
+ where
+ go :: SEC -> [Val]
+ go sec@(SEC stack env control global) = case control of
+ [] -> stack
+ (x:xs) -> case x of
+ Const i -> go (SEC (I i:stack) env xs global)
+ Global i -> go (SEC (global !! i:stack) env xs global)
+ Local i -> go (SEC (env !! i:stack) env xs global)
+ Closure a s -> go (SEC (Clo a env (take s xs):stack) env (drop s xs) global)
+ Ret -> let (v:(Clo 0 e c):st) = stack in go (SEC (v:st) e c global)
+ App -> case stack of
+ (Clo 1 e c:v:st) -> go (SEC (Clo 0 env xs:st) (v:e) c global)
+ (Clo n e c:v:st) -> go (SEC (Clo (n-1) (v:e) c:st) env xs global)
+
+ Dup -> let (v:st) = stack in go (SEC (v:v:st) env xs global)
+ Add -> let (x1:x2:st) = stack in go (SEC (vadd x1 x2:st) env xs global)
+```
+
+## Licensing Information
+
+Feel free to use any of the code or concepts here in your own projects! The code can be considered free of copyright and all notions of liability and/or warranty.
+
+## See Also
+
+[Modern SECD Machine, University of Calgary](https://pages.cpsc.ucalgary.ca/~robin/class/521/lectures_lambda/secd.pdf) - Gave me the idea to scrap the D stack.
+
+[SECD machine, Wikipedia](https://en.wikipedia.org/wiki/SECD_machine)
diff --git a/assets/css/main.scss b/assets/css/main.scss
index 57d0b1c..242dcd6 100644
--- a/assets/css/main.scss
+++ b/assets/css/main.scss
@@ -49,6 +49,15 @@ body {
background-color: $background;
}
+img {
+ max-width: 100%;
+}
+
+figcaption {
+ text-align: center;
+ color: $text;
+}
+
@import url(https://cdn.jsdelivr.net/npm/firacode@6.2.0/distr/fira_code.css);
code, .Agda { font-family: 'Fira Code', monospace; }
diff --git a/assets/img/clibreboot-holes.png b/assets/img/clibreboot-holes.png
new file mode 100644
index 0000000..3020de4
Binary files /dev/null and b/assets/img/clibreboot-holes.png differ
diff --git a/assets/img/clibreboot.png b/assets/img/clibreboot.png
new file mode 100644
index 0000000..194ca6e
Binary files /dev/null and b/assets/img/clibreboot.png differ