_____ _
|  ___(_)_ ____   __
| |_  | | '_ \ \ / /
|  _| | | | | \ V /
|_|   |_|_| |_|\_/

finv: a partial inverter for a first-order functional language (v0.1b)

This is a simple implementation (less than 500 lines of code) of a partial inverter for first-order functional programs. It has been developed by Jesús Almendros and Germán Vidal. Total inversion implies transforming a function like 
add(zero,y) = y
add(succ(x),y) = succ(add(x,y))
into a new function, say iadd, defined as follows: 
iadd(y) = (zero,y)
iadd(succ(w)) = let (x,y)=iadd(w) in (succ(x),y)
However, such total inversions are not always useful. In this case, for instance, the resulting function contains overlapping left-hand sides (which prevents its correct use in a functional language like Haskell).

In contrast, we define a partial inversion method. Partial inversion allows us to leave some input arguments in the inverted function. It is more flexible: total inversion is a particular case. For instance, the function add above can be partially inverted w.r.t. its first argument, i.e., we want to obtain a new function, say add_1, such that 

add_1(t,t1) = t2    iff    add(t1,t2) = t
for all values t1, t2, and t. Function add_1 can be defined as follows: 
add_1(y,zero) = y
add_1(succ(w),succ(x)) = add_1(w,x)
Clearly, function add_1 implements the subtraction on natural numbers.

A technical description of the method can be found in this paper.

The prototype implementation has been implemented in Prolog and can be found here: finv.tgz. It includes the source code of the partial inversion method ( inversion.pl), some examples (examples.pl) and a README file (README). The system has only been tested in SWI Prolog so far; try other Prolog environments at your own risk...

In order to run the partial inverter, you can follow these steps:

Once the program is loaded into Prolog, the user can load in a functional program from a file using the predicate loadf/1. The functional program should be written according to the following syntax for rules: 

  lhs := rhs.
Function and constructor symbols start with a lowercase letter and variables start with an uppercase letter (i.e., typical Prolog notation). Function definitions may also include type declarations. For instance, the above function add can be defined as follows: 
  add :: nat -> nat -> nat.

  add(0,X)    := X.
  add(s(X),Y) := s(add(X,Y)).
Arbitrary data types (like nat above) can also be defined by the user. For instance, natural numbers and lists can be defined as follows 
  datatype nat     ::= 0   | s(nat). 
  datatype list(A) ::= nil | (A : list(A)).
Partial inversion is then started by executing a goal of the form 
  ?- invert(function_name, input_parameters_list).
For instance, if we type in the following goal 
  ?- invert(add,[1]).
we get the partially inverted program: 
  add_inv(A,0)       =: A.
  add_inv(s(A),s(B)) =: add_inv(A,B).
where the partial inversion of the given function is denoted by add_inv and the symbol ":=" is replaced by "=:" in the rules.

A web interface for the partial inverter is available here so that you can easily test the system.

Please report any bug or comment to gvidal (at) dsic (dot) upv (dot) es.