×

First-order constrained lambda calculus. (English) Zbl 0893.03002

Baader, Franz (ed.) et al., Frontiers of combining systems. First international workshop, Munich, Germany, March 26–29, 1996. Dordrecht: Kluwer Academic Publishers. Appl. Log. Ser. 3, 339-356 (1996).
Summary: In earlier publications of the authors a calculus which extends the traditional lambda calculus by the addition of constraints was presented. The constraints can be used passively for restricting the range of variables and actively for computing solutions of goals. Here we present an extension of that calculus obtained by adding existential quantifiers and new rules for handling the new terms. This avoids the problem of shared variables and gives a very smoothly working language. We present a proof of the Church-Rosser property and the denotational semantics of the whole calculus.
For the entire collection see [Zbl 0885.00046].

MSC:

03B40 Combinatory logic and lambda calculus
03B70 Logic in computer science
68Q55 Semantics in the theory of computing
68N01 General topics in the theory of software

Citations:

Zbl 0864.68062
PDFBibTeX XMLCite