This repo provides an easy way to use an HVM1 version from the dup_labels branch. Note that HVM1 is deprecated in favor of HVM2 and bend. The only reason to use it is to experiment with lazy SUP nodes. See

• Fast Discrete Program Search with HVM Superpositions (SUP nodes) - finding ADD-CARRY
• Solving SAT via interaction net superpositions

Usage:

1. Install Nix.
2. Get a shell with hvm1 with SUP labels available via nix --experimental-features 'nix-command flakes' shell github:johannesCmayer/HVM1-SUP-Flake.
3. Use HVM, e.g. hvm1 run -t 1 "(+ 2 3)" or hvm1 run -d true -t 1 "(+ 2 3)" to see all reduction steps.

Try the example on the first page of An Algorithm for Optimal Lambda Calculus Reduction to see the optimal reduction with dup nodes in action:

hvm1 run -d true -t 1 "((λg (g(g(λx x))))
                        (λh ((λf (f(f(λz z))))
                             (λw (h(w(λy y)))))))"

To run the finding ADD-CARRY code do:

wget 'https://gist.githubusercontent.com/VictorTaelin/d5c318348aaee7033eb3d18b0b0ace34/raw/5055c1e17c54675d32a35245892a234333f8f194/fast_dps_add_carry.hvm1'
hvm1 run -c true -t 1 -f fast_dps_add_carry.hvm1 "Main"

-t 1 makes HVM use a single thread (There is a bug in the parallizer of HVM).

-c true makes HVM output performance statistics.

See the HVM1 guide for more (have GPT read it and then try to understand the source code here by asking questions).