What is hereditary substitution and why should I use it?

Question

What is hereditary substitutio,n and why should I use it?

I've been taking a look at hereditary substitution for my little programming language, because hereditary substitution is supposed to give a particularly clean categorical semantics for Cartesian categories, as you don't need to quotient by small step or big step relations.

I've run into a few issues that could use clarity, and need help with better examples and explanations.

I'm not sure how important this is, but for making substitution total, I've found multisubstitution of all the variables in the environment simpler.

In general, I've found making hereditary substitution total over undecorated terms that are not necessarily well-typed an annoying side issue. Using the option monad complicates stating and proving important properties like associativity.

I've also found hereditary substitution not so useful for logic programming fragment of my language which doesn't really admit straightforward big step semantics. Hereditary substitution seems to work best with values and particularly Cartesian closed categories. I am not really sure how hereditary substitution for substructural languages ought to work for example.

Eta expansion seems to rely on unique introductions for types. For example eta expansion for sum types isn't really clear to me.

In general, it's not clear to me why hereditary substitution is the way it is or how to extend it for very different languages.

Answer 1

First, eta for sums is not feasible, if you want to avoid quotients or conversion relations. I don't know about any description of eta-normal forms for sum types in the literature; the closest are "quasi-normal-forms" by Scherer. These support easy conversion checking, but still require an actual conversion relation. In any case, deciding eta for sum types is a large increase in formal complexity and it's probably not worth it for you. If you must have eta for sums, then the straightforward solution is to use non-normal syntax (with quotients or conversion relations), and perhaps postulate decidability of conversion.

The main point of hereditary substitution is essentially reverse mathematics: we're interested in simple "syntactic" termination measures for normalization.

• STLC can be normalized by induction on a lexicographic product of terms and types.
• Predicative System F can be normalized by induction on a lexicographic product of terms, types and multisets of universe levels.

However, if we don't care about reverse mathematics then there isn't really any reason to use hereditary substitution. Its suitability for reverse mathematics is what makes it more difficult to work with: if we use stronger metatheoretic features, we can implement normalization in more convenient ways. For example, logical relations use large elimination on syntactic types, and so does normalization-by-evaluation. Comparing hereditary substitution to NbE:

• It scales worse: it can't handle impredicativity, and it's not known if it works for dependent types.
• It's operationally less efficient.
• It's formally more difficult to handle, especially in proving correctness of normalization, which is required if we want to do slightly more interesting things, or if we want to show that our syntax of normal forms yields an initial model of some algebraic theory (e.g. cartesian closed categories, or simply typed categories-with-families).

If you want to skip quotients and conversion by only working with normal forms, it is not required to implement substitution as hereditary substitution; you can use pretty much any normalization algorithm. With NbE, substitution for normal terms is recovered by evaluating normal terms in the appropriate value environments, then quoting the result.

I'm not familiar with normalization for substructural theories; for these I note again that you are free to use any normalization algorithm for defining substitution on normal terms.

Answer 2

Just a note about sum types: it's fair to say that eta for sums is not yet tractable, but I'd strongly disagree with the claim that it's practically infeasible in general.

Regardless of whether they are NbE or hereditary substitution, all current algorithms for conversion of sum types are extraordinarily naive, and it would be really astonishing if they didn't exhibit terrible performance.

A good example of the (lame) state of the art is Thorsten Altenkirch and Tarmo Uustalu's 2004 paper, Normalization by evaluation for $\lambda^{\to2}$, which gives a simple NbE algorithm for the STLC with booleans.[1] To quote function types $\sigma \to \tau$, the algorithm in the paper enumerates all the normal forms of type $\sigma$! This is unavoidably exponentially bad (consider how many normal forms $\mathsf{bool} \times \ldots^n \times \mathsf{bool}$ will have), and is characteristic of basically all published algorithms for sum type conversion.

A genuinely good algorithm for sums would adopt ideas from BDDs or SAT solving, ensuring you only hit the exponential worst case much less often. No one has actually worked out the details of this approach, and until we actually try it, the folklore belief that conversion for sums is bad cannot be regarded as reliable.

[1] I should be clear that this is a really nice paper, and that my criticism is something the authors explicitly list as future work. But it's sufficiently well-written that it makes a really good example!