Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorNima
• CommentTimeSep 26th 2021
• (edited Sep 26th 2021)

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 :\equiv \Sigma_{x:X} P(x)$

$B :\equiv \Sigma_{x:X} Q(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 \rightarrow 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 \rightarrow U$. There could even be more options if $P(x)$ and $Q(x)$ weren’t of the same type. Let’s assume $Q: Y \rightarrow U$. Then we could have $y: (X \rightarrow U) + (Y \rightarrow U)$.

Even if making one of these choices, the formulation of $C$ eludes me. Do we write $C :\equiv \Sigma_{x:X} \Sigma_{f: X \rightarrow U} f(x)$, or $C :\equiv \Pi_{f: X \rightarrow U} \Sigma_{x:X} f(x)$, or something else? Any help or direction would be much appreciated!

• CommentRowNumber2.
• CommentAuthorUlrik
• CommentTimeSep 27th 2021

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 \equiv \sum_{x:X}Y(x)$, where $Y : X \to U$ is a fresh variable.

• CommentRowNumber3.
• CommentAuthorNima
• CommentTimeSep 27th 2021

Thanks Ulrik. I found that paper to be incomprehensible due to the unfamiliar notation, but I’ll give it another go.