The formal definition of the runtime is needed.

[Heimdell]

I want to make an interpreter - so it can fail with a trace of what it tried to do, and one I can play with.

I also want to make a HM-like typechecker (probably with some extensions).

For that, I need a formal definition of whats going on. This looks like Landin's INs, but with "superposition nodes", which - as I understand it - is a good way to not have an oracle which ruins everything. I kinda understand how they work from HOW.md, but not quite.

How are the s and r from {s r} linked to \x., where s and r are clones of b from \x.b?

I also don't get how Era nodes reduce. Do they replace everything they go in with Era nodes, while ~deleting~ returning themselves to freelist?

[VictorTaelin]

We'd like to implement a mathematical definition in Kind-Lang, from the Symmetric Interaction Calculus, which would also allow to prove theorems about it. Would that work for your plans?

Not sure I get the question. s and r from {s r} aren't really related to λx. {a b} is a superposition, which is a different primitive from lambdas. When you copy a lambda λx, two new lambdas are created, λx0 and λx1, and the old occurrence of x is replaced by {x0 x1}. That's basically how lambdas are related to superpositions, but, other than that, they're just different things. A superposition just stores two expressions, that can be anything, just like a pair would.

The reduction rules of Era are unspecified; I should add them later. One thing to note is that HVM is, in many senses, just an efficient (and extended) implementation of Symmetric Interaction Combinators, by Damiano Mazza. In other words, SIC is to HVM as the λ-calculus is to Haskell.

[Heimdell]

Thank you for an explanation! Will wait for formalisation.

So, when duplicating a function, HVM performs a substitution over the function body twice, and then puts function parts into superpositions?

[VictorTaelin]

Not quite, the rule is as described:

dup a b = λx(body)
------------------ Dup-Lam
a <- λx0(b0)
b <- λx1(b1)
x <- {x0 x1}
dup b0 b1 = body

So, in order to duplicate a function λx(body) incrementally as a and b:

1. Duplicate incrementally the body as b0 and b1

2. Create two brand-new lambda nodes, λx0(b0) and λx1(b1)

3. Substitute a and b by these brand-new lambda nodes

4. Substitute x by the sobreposition {x0 x1}

That's it. Node that this is a constant-time, constant-space operation. It allocates 4 nodes (two lambdas, one superposition and one duplication). And it does exactly 3 substitutions (which is also a constant-time operation). The body itself isn't on the substitutions though (but x, which becomes {x0 x1}, may be inside it, obviously)

[bsless]

A single place where all the rules are written down will go a long way towards formalization and implementations (including how dup nodes are evaluated and when)

[VictorTaelin]

HOW.md has that. It doesn't work for you?

[bsless]

Probably just me being slow. Since the file specifies it is still a wip I couldn't know that all the rules there are a comprehensive list. Maybe a slight restructuring could help with this in the future. A list of all the rules, followed by an explanation and example for each rule

[Andrew-Fryer]

After reading How.md, I wrote my own little Python interpreter (which is mostly working). I found it is a bit vague on why we need the second Dup Sup rule and how HVM decides to use each Dup-Sup rule. After reading runtime.c and compiler.rs, I believe I understand that each dup that exists implicitly in the input program is tagged at compile time (https://github.com/Kindelia/HVM/blob/master/src/compiler.rs#L263) with an id (called col) that is passed around at runtime. Iff the col of a Dup and a Sup (called Par) are different, we use the second Dup-Sup rule.

Is that right? Does anyone have an example of a sequence of reductions that uses the second Dup-Sup rule? (Otherwise, I'll try to fabricate one...)

[VictorTaelin]

That is so cool. Godo job.

Yes, that is right. HVM tags each brand-new DUP node with a globally unique ID (col), so that every DUP duplicated from that one is considered part of the same family, and will not duplicate each-other, but annihilate instead. That also happens with SUP nodes.

let a = λx λt (t x x)
(Pair a a)

This will use both DUP rules. The first one because the clone needs to complete, so the DUPs must eventually annihilate. The second one, because the DUP from let a needs to clone the DUP from the x variable cloning.