Meta-variables move de Bruijn indexes across scopes #16

Ptival · 2025-02-06T22:00:18Z

As a heads up, I'm working on a patch to UVMHS that would attach delayed substitutions to meta-variables.
Essentially at the moment, meta-variables are scope-unaware, and so substituting ⌊0⌋ for 𝔪:x in:

𝔪:x (λ y → 𝔪:x)

yields:

⌊0⌋ (λ y → ⌊0⌋)

which is likely not what you'd want, and makes meta-variables somewhat unfit for unification algorithms.

The fix would essentially attach a substitution to meta-variables, so that the above term should now be constructed as (picking a somewhat arbitrary syntax for the attached delayed substitution):

𝔪:x (λ y → 𝔪:[↑1]x)

and meta-variable substitution would thus yield:

⌊0⌋ (λ y → ⌊1⌋)

which is likely what you intended.

This heads up is:

to get alignment on this change,
especially noting that this change requires modifying the type of variables from the unparameterized 𝕐 to a version parameterized by its scope and its term language, i.e. 𝕐 s t.

I expect the second point to be the most intrusive for users of 𝕐, though ideally you always know which s and t a variable is about and you're not mixing up variables between different scope types or term types.

I'm not quite close to proposing this patch, but I want to give people some time to think about whether this won't mess their code.

The text was updated successfully, but these errors were encountered:

Ptival · 2025-02-06T22:28:18Z

It turns out we were punning expression variables and type variables in Oxide.

I believe we do it at a level where we are no longer using meta-variables, so I will likely add a helper:

cast𝕐 ∷ 𝕐 s a → 𝕐 s b

such that it lets you reuse named/global variables, but will fail on metavariables.

Ptival · 2025-03-06T18:55:53Z

I have a tentative solution for this problem, yet, the majority of the issues are in getting the tests to still pass after this change.

The crux of the problem is that we now have all sorts of ways things can be structurally different but semantically the same. This makes the equality tests we want tedious to write.

Here are a couple of ways in which equivalent things look different:

DSubst

For DSubst, we have three fields, that we can call "shift", "elems" and "intros".
DSubst 2 [a, b] 5 stands for the substitution that maps [0, 1, 2, 3, 4, 5, 6, …] to:
[0, 1, a, b, 9, 10, 11, …]
where the first two indices are left as-is, the next arguments are set to a, b, and all subsequent indices are bumped by 5.

There are at least 3 ways in which different DSubsts can correspond to the same effective substitution:

Some heading "elems" might be doing exactly what "shift" would do.
Some tailing "elems" might be doing exactly what "intros" would do.
When "elems" is empty and "intros" is zero, any amount of "shifts" is the same as no shifts at all.

That is, we want to equate:

DSubst 2 [2, 3, 4] 2 with DSubst 5 [] 2,
DSubst 2 [4, 5, 6] 2 with DSusbt 2 [] 2,
DSusbt n [] 0 with DSubst 0 [] 0 for any n.

SSubstElem

In the DSubst paragraph, I wrote the "elems" as numbers, but really they are values of type SSubstElem, which has two constructors:

Var_SSE, which contains a de Bruijn index, and,
Trm_SSE, which contains a SusbtElem, which itself may contain a user expression with some shifts.

This introduces more things to equate:

A Trm_SSE (SubstElem null (\() → None)) should be treated the same as a Var_SSE <current_index> when it appears in the "elems" of a DSusbt,
A Trm_SSE (SubstElem null (\() → Some <embedded expression variable containing some de Bruijn index i>)) should be treated the same as Var_SSE i when it appears in the "elems" of a DSusbt.

GSubst

When comparing GSubsts, which contains two dictionaries, one might be tempted to do a key-wise value comparison.
However, in practice, the usage of GSusbt within Susbt is such that the absence of some keys should be equated with the presence of that key mapping to a neutral value.

That is, in the case of Susbt, the following gsubstSubsts should be equated:

{}, (empty dictionary)
{⟨(), None⟩ ↦ …some DSubst that is equivalent to DSubst 0 [] 0… }
because the None key corresponds to substitutions for de Bruijn variables.

Likewise, keys that attach a null substitution to some named variable should also be ignorable, equating:

{}, (empty dictionary)
{⟨(), Some "variableName"⟩ ↦ …some DSubst that is equivalent to DSubst 0 [] 0… }

I have written a set of helpers to check for "equivalence" of DSusbt/SSubstElem/GSubst/Subst/ULCExps, in the context of ULCExp. It could almost all be generic, apart from the fact that the object language will likely embed a "variable" constructor, which may contain de Bruijn indices we'd want to notice when equating the "elems".

davdar · 2025-04-15T22:24:37Z

I'm starting to poke at this.

Currently fancy variables 𝕐 contain nameless (De Bruijn) variables DVar, named variables NVar, global variables GVar, and meta-variables MVar. And your comment above mentions the fact that this is annoying when you want to use some of these variable types, but not meta-variables.

So I'm planning to split this into two variable types, one that is the same but without meta-variables, and one that includes meta-variables and is isomorphic to the current type.

I also think it's very doable to have an equality operator that coincides with extensional equality, so I'll work on that next.

Ptival self-assigned this Feb 6, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Meta-variables move de Bruijn indexes across scopes #16

Meta-variables move de Bruijn indexes across scopes #16

Meta-variables move de Bruijn indexes across scopes #16

Meta-variables move de Bruijn indexes across scopes #16

Comments

DSubst

SSubstElem

GSubst