zbMATH — the first resource for mathematics

Proving failure in functional logic programs. (English) Zbl 0983.68503
Lloyd, John (ed.) et al., Computational logic - CL 2000. 1st international conference, London, GB, July 24-28, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1861, 179-193 (2000).
Summary: How to extract negative information from programs is an important issue in logic programming. Here we address the problem for functional logic programs, from a proof-theoretic perspective. The starting point of our work is CRWL (Constructor based ReWriting Logic), a well established theoretical framework for functional logic programming, whose fundamental notion is that of non-strict non-deterministic function. We present a proof calculus, CRWLF, which is able to deduce negative information from CRWL-programs. In particular, CRWLF is able to prove ‘finite’ failure of reduction within CRWL.
For the entire collection see [Zbl 0941.00011].

68N17 Logic programming
68N18 Functional programming and lambda calculus