Computing Publications

Publications Home » On the synthesis of function inverses

On the synthesis of function inverses

Peter G. Harrison, Hessam Khoshnevisan

Journal Article
Acta Informatica
Volume 29
Issue 3
pp.211–239
March, 1992
Springer Verlag
DOI 10.1007/BF01185679
Abstract

We present a method for synthesising recursive inverses for first-order functions. Since inverse functions are not, in general, single-valued, we introduce a powerdomain to define their semantics, in terms of which we express their transformation into recursive form. First, inverses that require unification at run-time are synthesised and these are then optimised by term-rewriting based on a set of axioms that facilitates a form of compile-time unification. The optimisations reduce the dependency on run-time unification, in many instances removing it entirely to give a recursive inverse. The efficiency of the use of relations in two modes is thereby improved, so enhencing extended functional languages endowed with logical variables and narrowing semantics. Our function-level, axiomatised system is more generally applicable than previous approaches to this type of optimis tion, and in general induces more mechanisable transformation systems.

Keywords
AESOP
BibTEX file for the publication
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.