Research Summary on Implementing Functional Patterns by Synthesizing Inverse Functions

TL;DR

This paper explores synthesizing inverse functions within Curry, a lazy functional-logic language, enabling inversion of certain functions directly and providing methods for more complex cases using non-strict unification.

Contribution

It introduces a method for synthesizing inverse functions in Curry, including handling non-injective functions and extending inversion capabilities beyond simple cases.

Findings

Inverse functions derived for functions with non-linear right-hand sides

Inverse functions for functions without extra variables can be directly synthesized

Non-strict unification enables inversion of more complex functions

Abstract

In this research summary we present our recent work on implementing functional patterns with inverse functions in the lazy functional-logic programming language Curry. Our goal is the synthesis of the inverse of any given function in Curry itself. The setting of a functional-logic language especially allows the inversion of non-injective functions. In general, inverse computation is a non-trivial problem in lazy programming languages due to their non-strict semantics. We are so far able to directly derive the inverse function for a limited class of functions, namely those consisting of rules that do not involve both extra variables and non-linear right-hand sides. Because the synthesized definitions are based on standard code, known optimizations techniques can be applied to them. For all other functions we can still provide an inverse function by using non-strict unification.