Victor Taelin VictorTaelin

Suppose you wanted to represent an 1D space in a pure functional language, i.e., with trees. Suppose that you also needed to shift the whole space left and right. An efficient way to do it would be to use a perfect binary tree to store locations, and bit-strings to represent paths. For example:

(((0 1) (2 3)) ((4 5) (6 7)))

The tree above would represent a space with 8 locations. Then, the path:

[1,0,0]

HOC - Thesis and Future Direction

At HOC, we believe Interaction Nets technology can lead to valuable market products. Two years ago, we raised $4 million to explore and validate this idea. During this period, we developed HVM and Bend—tools that significantly speed up functional and symbolic programs.

As we wrap up this research phase, we've identified the Symbolic AI market as our best opportunity. This market is rapidly growing, highly values computational efficiency, and aligns perfectly with HVM's strengths in

The Interaction Calculus

The Interaction Calculus (IC) is term rewriting system inspired by the Lambda Calculus (λC), but with some major differences:

Vars are affine: they can only occur up to one time.
Vars are global: they can occur anywhere in the program.
There is a new core primitive: the superposition.

An IC term is defined by the following grammar:

	data Uni : Set where
	U : Uni

	data ℕ : Set where
	Z : ℕ
	S : ℕ → ℕ

	data Vec (A : Set) : ℕ → Set where
	[] : ∀{n} → Vec A n
	_::_ : ∀{n} → A → Vec A n → Vec A (S n)

	-- Let's serialize lists of uints as follows:
	--
	-- <Uint> ::= 0 \| 1 <Uint>
	-- <List> ::= 0 \| 1 <Uint> <List>
	--
	-- For example, [1,2,3] serializes to '1 10 1 110 1 1110 0'.
	--
	-- Let f be a function that, given a number N, and a list of
	-- numbers XS, sets the Nth number on XS to 0. For example:
	-- - f(2, [0,1,2,3,4]) = [0,1,0,3,4]

	import Prelude.hvml

	// Types
	// -----

	// Type ::= ⊥ \| [Type]
	// - ⊥ = ⊥ = the Empty type
	// - [⊥] = ⊤ = the Unit type
	// - [[⊥]] = ℕ = the Nat type
	// - [[[⊥]]] = ℕ* = the List type

	import Control.Monad (when)
	import Data.Char (chr, ord)
	import Data.IORef
	import Data.Word
	import Debug.Trace
	import System.IO.Unsafe (unsafePerformIO)
	import Text.Parsec hiding (State)
	import qualified Data.IntMap.Strict as IntMap
	import qualified Data.Map as Map
	import qualified Text.Parsec as Parsec


	╭────────────────────────────────────────────╮
	│ ✻ Welcome to Claude Code research preview! │
	│ │
	│ /help for help │
	│ │
	│ cwd: /Users/v/vic/dev/IC │
	╰────────────────────────────────────────────╯

	! cat InteractionCalculus.md

	This is a debugging challenge.
	Read the document below, and identify the bug.

	---

	# The Interaction Calculus

	The Interaction Calculus (IC) is term rewriting system inspired by the Lambda
	Calculus (λC), but with some major differences:
	1. Vars are affine: they can only occur up to one time.