Faster evaluation from TermState for elements

[siddhartha-gadgil]

• This is the current bottleneck in #283
• There are obvious inefficiencies: for instance the distibution for Funcs is calcluated each time, and only needs to be calculated once.
• Indeed, computing a distribution is not needed, we should more directly look up for a term state.
• For terms with given type we can group in advance (maybe as a method in TermState)
• The trickiest case is the one involving unification, where it is typically nt worth computing unless needed. Here it is best to memoize in a mutable map.

[siddhartha-gadgil]

This may have been the reason why local-tangent-provers were very slow even with depth bounds.

[bollu]

What is a local-tangent-prover?

[siddhartha-gadgil]

My own ad-hoc name, but the idea is:

• generally distributions are generated using a recursive formula, including products (and semi-direct products).
• in the tangent case, we take the derivatives of the recursive formulas, in the sense that we generate with a base distribution and a tangent distribution (the latter very simple, perhaps only a single vector), with the equations only recursive in the tangent distribution part (e.g. base cannot be used in both sides of a product).
• LocalProver and LocalTangentProver are just pipelines for setup and generation.

[bollu]

• I don't know what it means to take a semi-direct product of distributions. I only know how to take a semi-direct product of semigroups (in the most general case). Can you please describe what you mean?

• So we have a differential manifold worth of formulae? And in the tangent case, we can take directional derivatives of formulae along other formulae?

[siddhartha-gadgil]

I should have said fibre product not semi-direct product. I am using terms loosely but I believe it is exactly the categorical fibre product. We do have an infinite dimensional manifold formed by probability distributions, but when I say tangent I mean we have a recursive equation to start with and use the derivative of this, with Liebnitz rule for differentiation. The derivative is just formal, i.e. we only use Liebnitz rule and linearity (so this is a derivation)

[siddhartha-gadgil]

The commit a0cd984122c35071 has fixed this.