diff --git a/_posts/2019-11-30-libreboot.md b/_archive/2019-11-30-libreboot.md similarity index 100% rename from _posts/2019-11-30-libreboot.md rename to _archive/2019-11-30-libreboot.md diff --git a/_posts/2020-09-16-go_download_a_car.md b/_archive/2020-09-16-go_download_a_car.md similarity index 100% rename from _posts/2020-09-16-go_download_a_car.md rename to _archive/2020-09-16-go_download_a_car.md diff --git a/_posts/2021-12-10-secd1.md b/_posts/2021-12-10-secd.md similarity index 89% rename from _posts/2021-12-10-secd1.md rename to _posts/2021-12-10-secd.md index 9b319b5..3f55d6b 100644 --- a/_posts/2021-12-10-secd1.md +++ b/_posts/2021-12-10-secd.md @@ -1,10 +1,10 @@ --- layout: post -title: "A first look at SECD machines" +title: "A look at SECD machines" --- -The SECD machine is a virtual machine designed to evaluate lambda expressions. It's purpose is to be a more natural goal for compilers than assembly while maintaining reasonable execution speed. In this blog post you will get a quick intro to SECD machines and an overview of a simple implementation. +The SECD machine is a virtual machine designed to evaluate lambda expressions. It's purpose is to be a more natural goal for compilers than assembly while maintaining reasonable execution speed. In this blog post I will give you a quick intro to SECD machines and an overview of a simple implementation. {% katexmm %} @@ -21,7 +21,7 @@ $$\lambda x.x \xRightarrow[]{\text{De Brujin}} \lambda \#0$$ $$\lambda f.\lambda g.\lambda x. f(gx) \xRightarrow[]{\text{De Brujin}} \lambda\lambda\lambda \#2(\#1\#0)$$ -The benefit in using De Brujin notation is that, rather than a balanced binary tree, a stack may be used for the environment. A variable is then an index into the environment. An additional benifit is that the machine does not need to concern itself with alpha equivalence. As a side-note, counting conventionally starts at $\#1$, not $\#0$, however in a virtual machine counting from $\#0$ is, of course, much more natural. +The benefit in using De Brujin notation is that, rather than a map, a dynamic array may be used for the environment, with variables being idecies into said array. An additional benifit is that the machine does not need to concern itself with alpha equivalence. As a side-note, counting conventionally starts at $\#1$, not $\#0$, however in a virtual machine counting from $\#0$ is, of course, much more natural. The second improvement to be made is to "dump" the dump stack. Rather than using the dump stack the current state will be pushed onto the stack as a closure which the return instruction can then restore when exiting a lambda. @@ -152,11 +152,11 @@ 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. +While this is a functional implementation, it does have a few fatal flaws. First of, it's usage of linked lists. While more natural in haskell a real SECD machine should of course use arrays to achieve constant variable lookup time. Second is the perhaps more obvious lack of features, to implement an interesting language one would need a more complete instruction set. Third is the representation of the tape. In a real-world SECD machine one would have a succint binary representation, allowing for simple compact storage of programs and speedy execution. ## 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. +The implementation itself is trivial and is little more than a Haskell translation of the instruction table above. ```haskell module SECD where