I expected to see mention of the Church-Rosser theorem, which may have just turned 90 years old. Pretty good vintage for a comp sci theorem.

Anyway the way I learned it is:

* for a given lambda expression, all evaluation orders which reduce to a normal form will reduce to the same normal form.

* if a lambda expression has a normal form, the 'lazy' way (normal order, leftmost-outermost-reduction, call-by-name, call-by-need) will find it.

Actually on re-reading, the article did mention confluence of the untyped lambda calculus, but only went as far as saying that the different evaluation order leads to different termination results, which is not quite as strong as saying the lazy way will find the terminating path if it exists.

https://codeberg.org/veqq/declarative-dsls is built around a query language working on tables/dataframes, hashmaps, arrays, strings etc. in the same way. I ended up allowing things like :where :group-by etc. in `select` go in any order and then allowing you to use ->> macros to micromanage the execution order.

A quick skim of the article suggests it's a study of the implications of allowing query planning in programs which are notionally finite but may have unbounded computation. Interesting.

See also https://dhall-lang.org/