Abstract
Functional logic languages incorporate logic programming capabilities of constraint solving within a functional language framework. We consider a prototypical functional logic language which supports definite descriptions, i.e., terms of the form “the x such that p”. Its semantics is defined in terms of flat ordered structures with ⊥ and ⊺ elements. These elements are used to represent the absence and ambiguity, respectively, of objects denoted by descriptions. We provide an equational axiomatization of the language and show that it is complete for this semantics.
Bronsard was supported by NSERC, Canada, and FCAR, Canada
The work by Reddy was supported by a grant from Motorola Corp.
Preview
Unable to display preview. Download preview PDF.
References
F. L. Bauer. The Munich Project CIP. Volume 292 of LNCS, Springer-Verlag, Berlin, 1987.
F. Bronsard. Program Synthesis in a Functional Logic Language. (forthcoming Ph.D. proposal), University of Illinois, 1990.
S. L. Bloom and R. Tindell. Varieties of “if-then-else”. SIAM J. Computing, 12(4):677–707, 1983.
N. Dershowitz. Computing with rewrite systems. Technical Report ATR-83(8478)-1, Information Sciences Research Office, The Aerospace Corp., El Segundo, CA., January 1983.
J. Darlington, A. J. Field, and H. Pull. The unification of functional and logic languages. In D. DeGroot and G. Lindstrom, editors, Logic Programming: Functions, Relations and Equations, pages 37–70, Prentice-Hall, 1986.
J. Darlington and Y. K. Guo. Unification of functional and logic languages — Towards constraint functional programming. In TENCON Special Session on Functional Languages: Theory and Applications, Bombay, India, Nov 1989.
M. Fay. First-order unification in an equational theory. In Fourth Workshop on Automated Deduction, pages 161–167, Austin, Texas, 1979.
J. A. Goguen and J. Meseguer. Equality, types, modules and generics for logic programming. In Proc. 2nd Intern. Logic Prog. Conf., Uppsala, pages 115–125, 1984.
I. Guessarian and J. Meseguer. On the axiomatisation of “if-then-else”. SIAM J. Computing, 16(2):332–357, Apr 1987.
D. Hilbert and W. Ackermann. Principles of Mathematical Logic. Chelsea Pub. Co., New York, 1950. translated by L. M. Hammond, G. G. Leckie, and F. Steinhardt.
J-M. Hullot. Canonical forms and unification. In Conf. on Automated Deduction, pages 318–334, 1980.
E.C. Leisenring. Mathematical Logic and Hilbert's ε-symbol. Gordon and Breach Science Publishers, NY, 1969.
G. Lindstrom. Functional programming and the logical variable. In ACM Symp. on Princ. of Program. Languages, 1985.
R.S. Nikhil, K. Pingali, and Arvind. Id Nouveau. Technical Report CSG 265, MIT, 1986.
G. Pottinger. Ulysses: Logical Foundations of the Definition Facility. Technical Report TR 11-9, Odyssey Research Associates, Jan 1988.
U. S. Reddy. Narrowing as the operational semantics of functional languages. In Symp. on Logic Program., pages 138–151, IEEE, Boston, 1985.
U. S. Reddy. Logic Languages based on Functions: Semantics and Implementation. Technical Report UIUCDCS-R-86-1305, Univ. Illinois at Urbana-Champaign, 1986. Ph.D. thesis done at Univ. of Utah.
U. S. Reddy. On the relationship between logic and functional languages. In D. DeGroot and G. Lindstrom, editors, Logic Programming: Functions, Relations and Equations, pages 3–36, Prentice-Hall, 1986.
U. S. Reddy. Functional logic languages, Part I. In Graph Reduction, pages 401–425, Springer-Verlag, 1987. (Lecture Notes in Computer Science, Vol 279).
U. S. Reddy. Design principles for an interactive program derivation system. In Proc. AAAI-88 Workshop on Automating Software Design, pages 145–155, AAAI, 1988.
U. S. Reddy. Transformational derivation of programs using the Focus system. In Symp. Practical Software Development Environments, pages 163–172, ACM, December 1988.
U. S. Reddy. Rewriting techniques for program synthesis. In N. Dershowitz, editor, Rewriting Techniques and Appl., pages 388–403, Springer-Verlag, 1989. (LNCS Vol. 355).
J. R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity and associativity. Journal of the ACM, 21(4):622–642, 1974.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bronsard, F., Reddy, U.S. (1990). Axiomatization of a functional logic language. In: Kirchner, H., Wechler, W. (eds) Algebraic and Logic Programming. ALP 1990. Lecture Notes in Computer Science, vol 463. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53162-9_33
Download citation
DOI: https://doi.org/10.1007/3-540-53162-9_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53162-3
Online ISBN: 978-3-540-46738-0
eBook Packages: Springer Book Archive