Is there a built-in structural equivalence and alpha-equivalence comparison between two K terms?
Since there's a substitution module that appears to do alpha-conversion, I was wondering if there's one for equivalence.
If there isn't one, is it possible to define such a function in a way abstracted from the specific syntax being checked? For instance, using the parser's binder annotations to check any two terms, however the grammar defines them.</div
You appear to be referring to the KVar sort, the SUBSTITUTION module, and the binder attribute, which together are used to implement variable-capture aware substitution in languages which depend on this, such as the lambda calculus. Currently, the behavior of ==K with respect to terms that contain binders is that two binders will only compare equal if they have the same name for the term bound. Unlike free variables and occurrences of bound variables within binders, which compare equal iff they refer to the same variable, the names of the variables in the binders themselves are not (currently) alpha-conversion aware and will be compared on the basis of their names. Thus, for example,
lambda x . x will compare equal to
lambda x . x, but not to
lambda y . y.
With that being said, nothing stops you from writing a function that traverses an expression containing binders and normalizes the names of its variables. You could then call this on two different terms and compare the result from each using ==K. The resulting comparison would then compare whether two expressions are equal modulo renaming. One simple way of doing this is to rename the variable of every binder with the number of levels of nested binders it is under, for example,
lambda _1 . ((lambda _2 . _2) (lambda _2 . _1)).
Please feel free to file an issue on GitHub if you try this approach and run into crashes or behavior you think is incorrect. I will prioritize fixing any bugs that are reported.</div