`is_isomorphic_to` should be named `is_alpha_equivalent`

[vchakhno]

Hello!

While browsing the sources, I came across the function is_isomorphic_to.
Turns out this function only tests the alpha-equivalence of two terms.

This function name is misleading: there exist terms that are isomorphic but not alpha-equivalent, such as the combinators for true and false. For such terms, that function returns false, when according to the name it should return true. Testing if two terms are isomorphic is a much harder problem than checking if they are alpha equivalent.

It seems to me like a misnomer and not a proper use of the term isomorphic. Mathematically, two objects A and B are said to be isomorphic if there exist a function from f: A -> B and its inverse g: B -> A such that f ∘ g = id_A and g ∘ f = id_B. That definition applies to a lot of lambda terms that are not alpha-equivalent.

I doubt this is something that actually trips up people, nor do I expect any change to the API, I just wanted to report it in case there ever is a new version, and to have eventual feedback as to why that function was named in this way.

Have a good day :D

[ljedrz]

Thanks for the issue!

I agree; I think this could be resolved without API breakage - the current implementation should be renamed to is_alpha_equivalent, and we can reintroduce is_isomorphic_to with the more correct, broader check (which would be almost identical, with the exception of (Var(_), Var(_)) => true if I'm not mistaken).

Please feel free to contribute a PR if you'd like to tackle this, otherwise I can do it when I have some free time.

[vchakhno]

Hi! Thank you for the swift response.

After some more thinking, I realized I don't actually know a coherent definition of isomorphism that makes sense for the untyped lambda calculus. Nor could I find one online either. Isomorphism is usually brought up in relation to types, for example in the context of simply typed lambda calculus.

I don't think simply ignoring the indices of variables is sufficient.
\a. \b. a b certainly doesn't feel isomorphic to \a. \b. a a but I'm struggling to come up with a concrete definition as to why exactly.

I'm afraid it may just be complete nonsense. As far as I know, there exist no notion of isomorphism for lambda terms.

[ljedrz]

That's fair - that being said, would you say that the name is still imprecise? It seems to me that structural isomorphism is more or less functionally the same as alpha-equivalence in the ULC.