12
$\begingroup$

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.

$\endgroup$
1

2 Answers 2

11
$\begingroup$

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.

$\endgroup$
8
  • 2
    $\begingroup$ @Couchy hereditary substitution must have a decreasing measure on types and/or universes when processing a neutral spine (iterated application to a variable). Impredicativity precludes any such measure. For example, in System F, $\mathsf{id}\,(\forall\,a.\,a \to a)\,\mathsf{id}$ has definitionally the same type as $\mathsf{id}$. So it's possible to have a cycle in types when applying a term to successive arguments. $\endgroup$ Mar 27, 2022 at 19:50
  • 2
    $\begingroup$ Alternatively, we can note that impredicative System F has much greater proof-theoretic strength than the predicative MLTT which can host hereditary substitution. So we shouldn't expect that hereditary substitution works for System F. $\endgroup$ Mar 27, 2022 at 19:56
  • 1
    $\begingroup$ @AndrásKovács Hold on, shouldn't the actual algorithm still terminate? Just the termination proof can't use a simple lexicographic syntactic check any more? Not so advantageous in that case and not sure how you'd prove termination though. $\endgroup$ Mar 28, 2022 at 1:12
  • 1
    $\begingroup$ @MolossusSpondee the algorithm terminates, but the termination is not provable in MLTT. $\endgroup$ Mar 28, 2022 at 6:42
  • 1
    $\begingroup$ @Couchy No, System F has weaker consistency strength but greater proof-theoretic strength than predicative MLTT. MLTT proves System F consistent, but doesn't prove it normalizing. $\endgroup$ Mar 28, 2022 at 6:45
6
$\begingroup$

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!

$\endgroup$
9
  • $\begingroup$ I made no claim about practical feasibility, only about feasibility of formalization in OP's desired quotient/conversion-free style. $\endgroup$ Mar 28, 2022 at 9:09
  • $\begingroup$ If memory serves, Arbob Ahmed and Bob Harper worked out a focusing-based normal-forms presentation for sums in WMM 2007. The idea was to use multifocusing plus variable ordering (a la BDDs) to get unique normal forms. Unfortunately this was never properly published. $\endgroup$ Mar 28, 2022 at 11:01
  • 1
    $\begingroup$ @MolossusSpondee: that totally works! In my comment I meant coproduct types when I wrote sum. They require the ability to branch, and have pattern-matching-style eliminators with a complex set of commuting conversions. $\endgroup$ Mar 29, 2022 at 12:58
  • 1
    $\begingroup$ Yes: $f(b) \triangleq \mathsf{if}\,b\,\mathsf{then}\,f(\mathsf{true})\,\mathsf{else}\,f(\mathsf{false})$ $\endgroup$ Mar 30, 2022 at 10:51
  • 1
    $\begingroup$ Related to the work of Arbob and Bob, there is also some similar subsequent work by Munch-Maccagnoni and Scherer: hal.inria.fr/hal-01160579. $\endgroup$ Mar 30, 2022 at 12:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.