While attempting to formalize some basic properties of STLC I fell into a very deep rabbit hole revolving around substitutions. Apparently there are a few different ways to go about it, including explicit substitutions, parallel substitutions, and traditional named substitutions.
on paper, named substitutions are quite easy to work with and reason about. However maintaining well-typedness, well-scopedness, and avoiding captures seems like a lot of bookkeeping for a formalization. Explicit substitutions are an intriguing approach but apparently make it trickier to talk about normalization, so I'm quite wary of using them.
Lastly there are parallel substitutions. Those seem a lot cleaner and more elegant compared to the previous two options, they arise naturally from the category of contexts, and they can be encoded easily in Agda as an inductive definition - a substitution $\theta : \Gamma\to\Delta$ is merely a list of terms of "shape" $\Delta$ all typed under $\Gamma$. So, for the past few weeks, I tried approaching those in numerous ways. My most successful attempt so far has been inspired by McBride's "kits", mildly extended with some extra axioms (I just added them as necessary so far so there might still be missing):
- $wk\;(vr\;x) ≡ vr\;(\mathsf{vs}\;x)$
- $tm\circ vr ≡ \mathsf{var}$
with notation similar to the reference.
As a way to define substitutions, it is great. However, I am still having a hard time actually proving theorems about this representation. Mainly composition of substitutions is extremely inconvenient to work with. Here's my attempt:
_⨾_ : ∀{Γ Δ Φ} → Subs Γ Δ → Subs Δ Φ → Subs Γ Φ
∙ ⨾ η = ∙
(θ , e) ⨾ η = (θ ⨾ η) , (e [ η ])
Composition is defined only on substitutions, and it seems like I need separate composition operators for renaming-renaming, renaming-substitution, and substitution-renaming in order to keep everything compatible. Also the asymmetry of the definition makes things like associativity and left-identity to be a lot more painful than I'd like.
I already encountered the Autosubst project which seems to have a similar goal and similar approach to what I've been doing so far, except they knew what they were doing. My main takeaway from this is that the rabbit hole goes deeper than I anticipated. I'd rather not outsource my substitutions to an external library, at least not yet, because my main goal is to learn how the fornalization works. The most devastating part is how seemingly simple this task seems at first!
Parallel substitutions are far too complicated to reason about by hand, and none of the other options seem viable for computerized mathematics. Are there different ways to tackle parallel substitutions? Or any other ways to represent substitutions, that are both precise and not tedious to work with?
