Retractions: A functional paradigm for logic programming.

*(English)*Zbl 0636.68012
TAPSOFT ’87, Proc. Int. Conf. Software development, Pisa/Italy 1987, Vol 2: Functional and logic programming and specifications, Lect. Notes Comput. Sci. 250, 260-275 (1987).

[For the entire collection see Zbl 0605.00016.]

The paper describes a model for a functional language integrating logic and functional programming. The approach is based on the concept of retraction of special set functions. Computable relations are defined as set retractions. To express retractions the paper introduces a functional language, which is first-order lambda-calculus. The Herbrand universe is used as the value domain of the language.

A Herband term is expressed in a functional way and is associated with a constant expression in the language. Unification of Herbrand terms can be obtained by application of set intersection to constant expressions. Computation of applications of retractions corresponds to resolution of queries. The language is defined without changes on the basic mechanism of functional language and can be supported by the reduction machines. The present approach is compared with other logic-functional integration mechanism.

The paper describes a model for a functional language integrating logic and functional programming. The approach is based on the concept of retraction of special set functions. Computable relations are defined as set retractions. To express retractions the paper introduces a functional language, which is first-order lambda-calculus. The Herbrand universe is used as the value domain of the language.

A Herband term is expressed in a functional way and is associated with a constant expression in the language. Unification of Herbrand terms can be obtained by application of set intersection to constant expressions. Computation of applications of retractions corresponds to resolution of queries. The language is defined without changes on the basic mechanism of functional language and can be supported by the reduction machines. The present approach is compared with other logic-functional integration mechanism.

Reviewer: A.Zhezherun

##### MSC:

68N01 | General topics in the theory of software |

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |

03B40 | Combinatory logic and lambda calculus |