# 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.