Are there any formal systems or programming languages in which its only possible to define functions that have inverses?

Consider an algorithm $$f(x)$$.

Are there formal systems or programming languages that only allow $$f(x)$$ to be defined if $$f^-1(x)$$ exists?

• Do you want to find $f^{-1}$ or to know if it exists? Aug 15, 2022 at 21:42
• I'd like to know that given $f$, $f^-1$ exists, and then produce it, all automatically Aug 15, 2022 at 22:00
• How is $f$ specified as input? What are the domain and range of $f$? What do you mean by "possible"? Are you asking whether the problem is decidable? If you want to produce it automatically, that should be mentioned in the question. Please edit your question to clarify what you are asking.
– D.W.
Aug 15, 2022 at 22:39
• I still don't understand. If you want an algorithm for deciding some problem, what are the inputs to the algorithm, and what is the desired output? Is the input a Turing machine or algorithm that defines $f$? Is $f^{-1}$ also provided as input? What does it mean for $f^{-1}(f(x))=x$ to mean if the algorithm for $f$ or $f^{-1}$ doesn't halt on its input? What do you mean by 'given it..."? You might want to break this down into multiple smaller sentences.
– D.W.
Aug 16, 2022 at 2:23
• Sounds like an XY question. Better tell us what you are trying to achieve. This said, you are quite free to work with "the set of the invertible functions". As regards a programming language based on this concept, I have strong doubts about any usefulness it could have.
– user16034
Aug 16, 2022 at 14:39