A term like nat -> nat can be expressed as 2 different graphs in memory:
(->)
/ \
nat nat
and
(->)
/ \
\ /
nat
In the second graph the occurrences of nat are shared, so it takes less memory.
When the terms get deeper the size of the graph with maximal sharing
can be logarithmic in the size of the term seen as a tree (the tree has no sharing).
For instance (nat -> nat) -> (nat -> nat) can be shared as
(->)
/ \
\ /
(->)
/ \
\ /
nat
taking 3 nodes instead of 7.
This project provides a plugin to print debug information about how
Rocq’s terms are structured in memory.
(Note: currently Rocq only uses in-memory sharing to reduce memory usage and
shortcut some equality tests.)