LAMBDALG: Higher order algebraic specification language
Typed functional languages like ML or Haskel do not allow algebraic definitions of abtract data types and operators although they may employ a very rich machinery for defining polymorphic recursive functions of a higher type. On the other hand, equational languages like OBJ allow arbitrary (first order) algebraic definitions, but they do not have the full-power of parametricity given by ML polylmorphism nor functional definitions of higher types. Under these circumstances it is very attractive to combined these two different kinds of languages to host both features. Then the unified language would allow easy definitions of quite complex objects in a simple declarative style. LAMBDALG is a specification language which hosts both these features. The computation model (operational semantics) of LAMBDALG is based on the combined system of polymorphic typed lambda calculus and the first order and restricted higher order term rewriting in [Jouannaud-Okada 91]. As a high-level specification language, LAMBDALG integrates the OBJ3 style module based algebraic specification language [Goguen-Winkler 88] and the ML style polymorphic typed functional language [Harper et al. 86]. Algebraic definition of abstract data types and context-sensitive definitions of operators can be directly executed, in contrast to the traditional ML-style languages or their extensions (eg. [Mitchell et al. 90]).
KeywordsSpecification Language Operational Semantic High Type Functional Language Abstract Data Type
Unable to display preview. Download preview PDF.
- [Breazu-Tannen 91].Val Breazu-Tannen and Jean Gallier. Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science, 1991. (The former version in ICALP'89)Google Scholar
- [Cardelli-Mitchell 89].L. Cardelli and J.C. Mitchell. Operations on records. In Math. Foundations of Prog. Lang. Semantics. 1989.Google Scholar
- [Dershowitz-Okada 91].N. Dershowitz and M. Okada. A rationale for conditional equational programming. Theoretical Computer Science, 1991.Google Scholar
- [Futatsugi et al. 85].K. Futatsugi, J. Goguen, Jean-Pierre Jouannaud, and J. Meseguer. Principles of OBJ2. ACM POPL'85 Google Scholar
- [Goguen et al. 85].J. Goguen, Jean-Pierre Jouannaud, and J. Meseguer. Operational semantics for first-order algebra. ICALP'85, Springe LNCS 194 Google Scholar
- [Goguen-Winkler 88].J. A. Goguen, T. Winkler. Introducing OBJ3. Technical Report SRI-CSL-88-9, Computer Science Laboratory, SRI International, 1988.Google Scholar
- [Gui-Okada 93].Y. Gui and M. Okada. System Description of LAMBDALG, LPAR'93. (Logic Programming and Automated Reasoning, 1993).Google Scholar
- [Harper et al. 86].R. Harper, D. MacQueen, and R. Milner. Standard ML, LFCS Report Series, ECS-LFCS-86-2, 1986.Google Scholar
- [Jouannaud-Okada 91].J. Jouannaud, M. Okada. A computation model for executable higher-order algebraic specification languages. Proc. 6th IEEE LICS. 1991.Google Scholar
- [Mitchell et al. 90].J. Mitchell, S. Meldal, and N. Madhav. An extension of standard ML modules with subtyping and inheritance. ACM POPL'90 Google Scholar
- [Okada 89]M. Okada. Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewriting system. ACM ISSAC 89 Google Scholar
- [Okada 93]M. Okada. Type-theoretic term rewriting theory. Technical report. Logic & Formal Methods Lab, Concordia University, 1993.Google Scholar