Normalization by Evaluation (NbE for short) done in Python. The only test example I've provided shows how the algorithm handles normalization of the term (2 3), encoded ala Church.

$ pytest tests/ -s
. tests/test_runner.py λ f. λ x. (f (f (f (f (f x)))))  # aka 5