“Let us Calculate”: Leibniz, Llull, and the Computational Imagination (2016)

The Leibniz rule is probably the single most important one for mathematically sound programming. He was a real dreamer.

It’s odd how hard it is to search for, but one formulation is

  x=y  =>  f.x=f.y

In this case the dot is the function application operator. Note that this is a logical or syntactic rule and not an operational one. It’s saying that you can freely substitute, for all f, with renaming, the function body of f in equations of x and y.