Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 3 of 3
I’m wondering if there’s been a study of unification and anti-unification of HoTT types? Or even maybe depedent type theory? I’ve looked around but haven’t been able to find a good reference. I’ve found papers on anti-unification for other type systems, such as [1] [2] but not having much luck generalizing them to HoTT.
Unification seems a bit more straightforward, but anti-unification (or least general generalization) of two types has flummoxed me. The problem is in introducing a variable to take the place of two types that are not equivalent and can no longer be split up. For example, take the following two types:
A:≡Σx:XP(x)
B:≡Σx:XQ(x)
Our aim in anti-unification is to find a type C that would unify with both A and B by means of variable substitution. If following the algorithm in [1], we’d first recognize that both A and B use the same constructor (of the Sigma type), so we would drill down one level and attempt to anti-unify (or generalize) the two arguments. The first argument is the same for both, so we can copy that straight to C. However, the second argument is now an expression which is invoking two different predicates of type X→U. In a traditional anti-unification algorithm, we would define a new variable that would be substituted with either P(x) or Q(x) when unifying C with A and B.
Here however, there seems to be more than one option. Calling this new variable y, we could have y:U or y:X→U. There could even be more options if P(x) and Q(x) weren’t of the same type. Let’s assume Q:Y→U. Then we could have y:(X→U)+(Y→U).
Even if making one of these choices, the formulation of C eludes me. Do we write C:≡Σx:XΣf:X→Uf(x), or C:≡Πf:X→UΣx:Xf(x), or something else? Any help or direction would be much appreciated!
There’s a 1991 LICS paper by Frank Pfenning, Unification and Anti-Unification in the Calculus of Constructions, which should be helpful. Anti-unification is in Sec. 5 with the discussion of binders on p. 8.
I haven’t read the details, but my guess would be that we simply get C≡∑x:XY(x), where Y:X→U is a fresh variable.
Thanks Ulrik. I found that paper to be incomprehensible due to the unfamiliar notation, but I’ll give it another go.
1 to 3 of 3