HVM Superposition Node Program Search Flake

Link post

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

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

No comments.