Variants of Variants and the Finite Variant Property
Andrew Cholewa, José Meseguer, Santiago Escobar · 2014
Variants and the finite variant property were originally introduced about a decade ago by Hurbert Comon-Lundh and Stephanie Delaune to reason about equational theories that commonly appear in cryptographic protocol analysis. Since that time, two additional notions of variants have been developed: one by Santiago Escobar, Jose Meseguer, and Ralf Sasse, and one by Stefan Ciobâcǎ. Though it seems intuitively clear that all three notions capture the same essential idea, their relationships to each other have never been rigorously analyzed. Therefore, we decided to do just that. In the process, we encountered an unexpected subtlety with respect to the finite variant property, the term signature of a theory, and the boundedness property. We also provide a simple semi-decision procedure for checking if an equational theory has the finite variant property, by analzying terms of the form f(x1 : s1, . . . , xn : sn) for all function symbols f : s1, . . . , sn → s in the signature, where x1, . . . , xn are distinct variables.