math. logic question 

Is there a theorem that there is no generic algorithm turning a function f: A -> B into it's inverse g: B -> A, where A and B are say small types? Something along the usual lines of reducing it to the halting problem.

Context: I'm just wondering about whether/why writing tests (by hand) ever makes sense.

math. logic question 

@amiloradovsky @peterdrake

I have been wondering about this but didn’t know who to ask. Just connected with a CS prof who might be able to weigh in. Sorry to ping you Peter but I am dying to know and my google-fu is failing me.

math. logic question 

@rolltime @amiloradovsky Is it sufficient to note that some functions, like the absolute value function, have no inverse?

re: math. logic question 

@peterdrake @rolltime Perhaps I meant decidability — an inverse or a proof that there is none in finite time. Also considering set-valued functions there is always an inverse, speaking non-constructively.
Follow

re: math. logic question 

@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".

re: math. logic question 

@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.
Sign in to participate in the conversation
CleverLibre Social

CleverLibre Social is an inclusive social instance for open discussion, learning, and community.
All cultures welcome.
Hate speech and harassment strictly forbidden.