@amiloradovsky @rolltime It's been a while since I've done theory, and I'm not sure I fully understand your question.

You may be able to get somewhere with Rice's theorem, which says that you can't write a Turing machine that, by looking at the code of another Turing machine, determines any property of the language accepted by that other machine. The two exceptions are the property that all languages have and the property that no languages have. This is delightfully summarized as "anything that is not trivial is impossible".

@peterdrake @rolltime I think it has to deal with the "breadth" of the types A and B, and restrictions of f:

- When they're say finite then we may (theoretically) check for surjectivity and injectivity, and define the inverse as a (possibly huge) pattern-match on values of B. All in finite time by iteration on every element (though it may be impractical).
- When f is composed of only finite sums and products (with no quantifiers), we perhaps may project the products and case-analyse the sums. IIRC there's something called Indiscernibility of Identicals which seems to make it possible.
- When A and B are numeric and f is say linear.
- etc.

Conversely, if we translate one protocol (high-level) into another (low-level) with a FSM, we then write another FSM to translate it back, and check for validity along the way. There has to be a reason why the latter can't be automated.

I need to think more about it. Thanks for introducing me to the Rice's theorem.