Logic and functional programming by retractions: Operational semantics. (English) Zbl 0666.68012

Bellia, M.

RAIRO, Inf. Théor. Appl. 22, No. 4, 395-436 (1988).

In a previous paper of the author [ibid. 22, No.3, 271-310 (1988; Zbl 0666.68011)] considered was the definition of a functional language integrating logic and functional programming. The approach was based on the concept of retraction on some Cartesian product of the Herbrandt universe. A Herbrandt term was associated with a constant expression in the language. Unification of Herbrand terms can be obtained by application of the set intersection to constant expression. The semantics was defined in an abstract way.
The author clarifies the operational semantics of the set operators. The operational semantics is defined in two distinct ways. The first definition inherits from predicative languages and corresponds to the unification algorithm. The second definition is a more conventional one for functional languages. It defines a system of reduction rules which reduces constant expressions to the normal forms, and a system of rules which reduces expressions to constant expressions without the set intersection operator. Thus the language can be supported by the reduction machines.

Reviewer: S.S.Starchenko

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68N01	General topics in the theory of software
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

logic programming; functional programming; retraction; Herbrandt universe; operational semantics; unification; reduction rules

Citations:

Zbl 0666.68011

References:

[1]	K. R. APT and M. H. VAN EMDEM, Contribution to the Theory of Logic Programming, J. ACM, Vol. 29, 1982, pp. 841-862. Zbl0483.68004 MR666781 · Zbl 0483.68004
[2]	M. BELLIA, E. DAMERL, P. DEGANO, G. LEVI and M. MARTELLI, A Formal Model for Lazy Implementation of a PROLOG Compatible Functional Language. In Implementations of PROLOG, J. A.CAMPBELL Ed., Ellis Horwood, 1984, pp. 309-326.
[3]	M. BELLIA, Logic and Functional Programming by Retractions, RAIRO Inf. Théorique et Applications, Vol. 22, 1988, pp. Zbl0666.68011 MR963593 · Zbl 0666.68011
[4]	K. BERKLING, Reduction Languages for Reduction Machines, Proc. 2nd Int. Symp. on Computer Architectures, IEEE Comp. Society Press, 1975, pp. 133-140.
[5]	K. BERKLING, J. A. ROBINSON and E. E. SIBERT, A Proposal for a Fifth Generation Logic and Functional Programming System, based on Highly Parallel Reduction Machine Architecture, Syracuse University, November 1982.
[6]	K. BERKLING, Epsilon-reduction : Another view of Unification, CASE Center, Syracuse University, 1985.
[7]	N. DERSHOWITZ, Ordering for Term-rewriting Systems, Theoretical Computer Science, Vol. 17, 1982. pp. 279-301. Zbl0525.68054 MR648438 · Zbl 0525.68054
[8]	D. FRIEDMAN and D. WISE, CONS Should not Evaluate its Arguments. In Automata, Languages and Programming P, S. MICHELSON Ed., Edinburgh Univ. Press, 1977, pp. 256-284. Zbl0461.68023 · Zbl 0461.68023
[9]	P. HENDERSON and J. H. MORRIS, A Lazy Evaluator, Proc. Third ACM Symp. on Principles of Programming Languages, 1976, pp. 95-103.
[10]	P. HENDERSON, Functional Programming, Application and Implementation, Prentice-Hall, Englewood Cliffs, N.J., 1980. Zbl0426.68059 · Zbl 0426.68059
[11]	G. HUET and D. C. OPPEN, Equations and Rewrite Rules. A survey. INRIA Tech, Report 15, also as SRI Rep. STAN-CS-8O-785, january 1980.
[12]	R. A. KOWALSKI, Predicate Logic as a Programming Language, Proc. IFIP Congress, 1974, pp. 569-574. Zbl0297.68006 MR428765 · Zbl 0297.68006
[13]	A. MARTELLI and U. MONTANARI, An Efficient Unification Algorithm, ACM TOPLAS, Vol. 4, 1982, pp. 258-282. Zbl0478.68093 · Zbl 0478.68093
[14]	M. J. O’DONNELL, Computing in System Described by Equations, LNCS 50, Springer-Verlag, Berlin, 1977. Zbl0421.68038 MR483644 · Zbl 0421.68038
[15]	M. S. PATERSON and M. N. WEGMAN, Linear Unification, J. Comp. System Science, Vol. 16, 1978, pp. 158-167. Zbl0371.68013 MR483794 · Zbl 0371.68013
[16]	J. E. STOY, Denotational Semantics, The Scott-Strachey Approach to Programming Languages, MIT Press, Cambridge, 1977. Zbl0503.68059 MR488969 · Zbl 0503.68059
[17]	P. C. TRELEAVEN, Computer Architecture for Functional Programming, In Functional Programming and its Applications, J. Darlington. P. HENDERSON and D. A. TURNER Eds., Cambridge Univ. Press, 1982, pp. 281-306.