archived some pages, edited SECD page a little bit

master
Rachel Lambda Samuelsson 2022-12-09 20:14:17 +01:00
parent 344262db2a
commit a8cfcb9437
3 changed files with 5 additions and 5 deletions

View File

@ -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.
<!--more-->
{% 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