HVM SIC Succ(0) aka 0 + 1
So you may have heard of a potentially mind boggling tech that is HVM. Underlying the runtime is an alternative universal model of computation - Interaction Combinators.
Okay I'm rambling, the goal of this post is being an addendum to Zicklag's primer for Interaction Calculus. I will showcase a larger example of figuring out how to do 0 + 1, technically succ(0).
Prerequisuites
- Grasp on Interaction Nets, Zicklag's post is a great primer
- Lambda Calculus syntax familiarity. A smooth introduction can be found here
Let's get started.
Laying the Notation
To start let's define my notation because I made mine a bit more special because I'm a bit special.
Instead of zicklag's agent symbols, I'm gonna use a separate one for lambda functions vs lambda applications, e.g:
I wrote over the duplication symbol so you can see my handwriting.
Chekhov's Erase Node
Zicklag puts in the following in his blog post.
Note: For the sake of the examples below, we don’t need to use erasers, so we’re going to leave them out for now. In concept, an eraser is a node with only one port that deletes anything that’s plugged into it, so it is easy to imagine how it might play into things after we understand constructors and duplicators.
I am too dumb so I didn't understand easily, so if you're like me we're gonna find out how it works.
Counting for Beginners
Let's define 0, 1 and 2 (annotated edition) via Church encoding. I'd almost suggest you to make an attempt with a bit of pen and paper and check with my answer to get a greater feel
Note the floating f on Zero, is that an artifact of Zero or something sus?
Speaking of sus here's my succ function
An Example Reduction
Here you can see me apply succ onto zero. Recall that lambda and application nodes are the same and thus will get annihilated upon interaction. For convenience a refresher for the rules again.
Bruh moment, an inconsistency?
These two ones don't look the same!
There's an unnecessary duplication node
As you can guess we are missing the Erase node. Technically these 2 nets can be interpreted the same despite looking different. That is the key point. One use of erase nodes is to hook them up to unused parameters.
Thus we have 2 options to sqaure these two nets. Hook that floating f1 to an erase node, or just remove it for succinctness.
Below I attach the erase node (a flat line) for the floating f on Zero.
Finally, an interactive example!
Behold, a visualised version of the net reduction using t6's useful tool!
Ending Hook
We have learnt two things:
- Erase Nodes can be used to attach to unused arguments
- There is ambiguity Interaction Nets, 2 nets can be observationally the same
This begs the following questions:
- How do we convert to and from lambda calculus to interaction nets?
- How do I make the worst calculator in the world?
You may find out these answers in a later post!!!
Stay tuned.