Linearity by α-spine


Proof-of-concept code of an implementation of the α-spine strategy on certain term graphs (dags), generating as output dot-files of the term graphs. The concept proven by this code is that combinators / the lambda-calculus can be normalised in time and space linear in the number of leftmost-outermost steps, as presented and demonstrated at TERMGRAPH 2024 and HOR 2025. The default example in Main.java is c2 c2 (for c2 the Church numeral 2) which evaluates to c4 (the Church numeral 4) in 20 steps (including 2 α-steps) as visualised in the movie (1 graph per 5 seconds).