Theoretical background of HOVM?

[ken-okabe]

I'd like to confirm the theoretical background of HOVM.

I've read;
#14 (comment) @leonardohn

But a target is in fact a machine. Take for instance the LLVM compilation targets like X86, ARM, SPIR-V or even WASM; They all resemble computer architectures that are either real hardware (as in X86 and ARM) or a virtual hardware (like SPIR-V or WASM). I agree that historically virtual machines are usually related to traditional hardware (sharing characteristics like using von Neumann-like architectures), but in this particular case, we are talking about an abstraction that doesn't have memory at all, just like original lambda calculus when compared to Turing machines. So, it doesn't even make sense talking about garbage collection inside this machine, unless when considering the implementation of this abstraction over bare metal hardware, which in turn also don't require garbage collection.

This is extremely interesting, especially;

in this particular case, we are talking about an abstraction that doesn't have memory at all, just like original lambda calculus when compared to Turing machines.

My assumption right now is this VM is a successor of

parallel_lambda_computer_tests

optlam -> Absal -> Symmetric-Interaction-Calculus
The Symmetric Interaction Calculus
->
EA-NET +
Elementary Affine Core (EA-CORE) (Specification)

FM-NET +
FM-CORE (Formality-Core)
Formality-Core/Whitepaper.md
Soonad/Whitepaper

->
HOVM

Am I correct?
Please let me know.

Thanks.

[leonardohn]

Just let me clarify something that I think might have confused some readers. In Turing machines, you do have a tape where all computations are performed, which is an essential part of the machine itself. On the other hand, in lambda calculus you have the input expression and the computation is performed by successively applying reduction rules, making the input expression to achieve its normal form.

Of course, realistically speaking, you need something to store this expression when emulating it in von Neumann based machines, and this is done using its memory, which is size bounded and hence you have a limit for which expressions can be computed. The thing is, the memory itself is not a core part of this computation scheme, so it doesn't make sense to talk about allocating memory inside a lambda expression. For this particular reason, the garbage collector is not a primitive inside this machine.

However, you do need to allocate memory when emulating this machine to contain any growing lambda expressions. So, an implementation of this emulator could use garbage collection to make things easier. But, as @VictorTaelin found out with the multiple implementations, you don't need garbage collection.

I hope I made the things clearer :)

[ken-okabe]

No worry, I think no one reading this kind of thread has been confused. We know the stuff.

[VictorTaelin]

Note: most of these things are old stepping stones to get where I am, and should mostly be ignored. What is currently up-to-date is:

• Absal: a reference interaction-net based optimal evaluator (https://github.com/victortaelin/abstract-algorithm)

• SIC: the same thing as Absal, except representing inets as scopeless terms. HOVM is based on that. (https://github.com/victortaelin/symmetric-interaction-calculus)

• HOVM: an efficient C compiler/runtime based on SIC's theory. (https://github.com/kindelia/hovm)

• Kind: is the proof language I'm working on, and will soon compile to HOVM. (https://github.com/kind-lang/kind)

• Kindelia: a decentralized computer that uses HOVM instead of the EVM. (https://github.com/kindelia/kindelia)

All the other things are past/outdated iterations of these concepts. Don't read these or you'll just get confused.

I'll answer the questions later.

[ken-okabe]

All right, I'm glad to be able to confirm HOVM is based on SIC's theory because reading your blog posts, I've had a strong feeling so far it's the ultimate conclusion for your lambda-calculus research so far.
Since FM-CORE (Formality-Core)=based on Absal/EA sounds still vital, I was confused.

Now the outline of the projects also in historical context is clear to me. Thank you.