Inverse and Implicit Functions in Domain Theory

We construct a domain-theoretic calculus for Lipschitz and differentiable functions, which includes addition, subtraction and composition. We then develop a domaintheoretic version of the inverse function theorem for a Lipschitz function, in which the inverse function is obtained as a fixed point of a Scott continuous functional and is approximated by step functions. In the case of a C1 function, the inverse and its derivative are obtained as the least fixed point of a single Scott continuous functional on the domain of differentiable functions and are approximated by two sequences of step functions, which are effectively computed from two increasing sequences of step functions respectively converging to the original function and its derivative. In this case, we also effectively obtain an increasing sequence of polynomial step functions whose lower and upper bounds converge in the C1 norm to the inverse function. A similar result holds for implicit functions, which combined with the...

• Type: Conference
• Year: 2005
• Where: LICS
• Authors: Abbas Edalat, Dirk Pattinson
• Keywords: Computer Science, Inverse Function, Inverse Function Theorem, LICS 2005, Step Functions