×

A theory of binding structures and applications to rewriting. (English) Zbl 0783.68089

Summary: We present a theory of binding structures, and give examples of its application to rewriting. We define the set of binding structures as an abstract algebra, and define a general notion of parametrized homomorphism. A variety of operations on binding structures are presented as homomorphisms, and a collection of properties useful for developing applications is given. Three applications are presented: a generalized notion of term rewriting; a theory of unification for binding structures; and a set of structures and primitive rules intended to serve as a basis for design of rewriting components for (quantified) first-order reasoning systems.

MSC:

68Q99 Theory of computing
08A70 Applications of universal algebra in computer science
68W30 Symbolic computation and algebraic computation
68P05 Data structures
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Cardelli, L.; Curien, P.-L.; Lévy, J.-J., Explicit substitutions, Proc. 17th Ann. ACM Symp. on Principles of Programming Languages, 31-46 (1990)
[2] Barendregt, H., The Lambda Calculus: Its Syntax and Semantics (1981), North-Holland: North-Holland Amsterdam · Zbl 0467.03010
[3] Broy, M.; Wirsing, M.; Pepper, P., On the algebraic definition of programming languages, ACM TOPLAS, 9, 1, 54-99 (1987) · Zbl 0627.68009
[4] Curtis, P., Algorithms: the PCL code walker, Lisp Pointers, 3, 1, 50-61 (1990)
[5] de Bruijn, N. G., Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indag. Math., 34, 381-392 (1972) · Zbl 0253.68007
[6] Ehrig, M.; Baldamus, H.; Cornelius, F., Theory of algebraic module specifications including behavioural semantics, constraints, and aspects of generalized morphisms, Proc. 2nd Internat. Conf. on Algebraic Methodology and Software Technology, AMAST91, 101-126 (1991)
[7] Gallier, J. H.; Snyder, W., Designing unification procedures using transformations: a survey, EATCS Bulletin, 40, 273-326 (1990) · Zbl 0744.68112
[8] Griffin, T., Formal account of notational definition, (Ph.D. Thesis (1988), Cornell University)
[9] Griffin, T., Notational definition-a formal account, (Proc. 3rd Ann. Symp. on Logic in Computer Science (1988), IEEE)
[10] Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, (Proc. Symp. on Logic in Computer Science (1987), IEEE), 194-204
[11] Higgins, P. J., Algebras with a scheme of operators, Math. Nachr., 27, 115-132 (1963/1964) · Zbl 0117.25903
[12] Huet, G.; Lang, B., Proving and applying program transformations expressed with second-order patterns, Acta Inform., 11, 31-55 (1978) · Zbl 0389.68008
[13] Ketonen, J., EKL: A mathematically oriented proof checker, (Shostak, R. E., Proc. 7th Internat. Conf. on Automated Deduction, Vol. 170 (1984), Springer: Springer Berlin), 65-79, Lecture Notes in Computer Science
[14] Ketonen, J. A.; Weening, J., EKL: An interactive proof checker, (Tech. Report CS Report STAN-CS-84-1006 (1984), Stanford University)
[15] Klop, J., Combinatory Reduction Systems (1980), Mathematisch Centrum: Mathematisch Centrum Amsterdam, Number 127 in Mathematical Centre Tracts · Zbl 0466.03006
[16] Mason, I. A.; Talcott, C. L., Equivalence in functional languages with effects, J. Funct. Prog., 1, 3, 297-327 (1991) · Zbl 0941.68540
[17] Mason, I. A.; Talcott, C. L., Program transformation for configuring components, (Proc. Symp. on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’91 (1991), ACM: ACM New York), 297-308
[18] Mason, I. A.; Talcott, C. L., Inferring the equivalence of functional programs that mutate data, Theoret. Comput. Sci., 105, 167-215 (1992) · Zbl 0768.68092
[19] Meseguer, J., Rewriting as a unified model of concurrency, (Proc. Concur ’90 Conf.. Proc. Concur ’90 Conf., Amsterdam. Proc. Concur ’90 Conf.. Proc. Concur ’90 Conf., Amsterdam, Lecture Notes in Computer Science, Vol. 458 (1990), Springer: Springer Berlin), 384-400
[20] Miller, D., A logic programming language with lambda abstraction, function variables, and simple unification, (Schroeder-Heister, P., Extensions of Logic Programming. Extensions of Logic Programming, Lecture Notes in Computer Scince, Vol. 475 (1991), Springer: Springer Berlin), 253-281 · Zbl 1502.68070
[21] Moggi, E., Notions of computation and monads, Informat. and Comput., 93, 55-92 (1991) · Zbl 0723.68073
[22] Nadathur, G.; Miller, D., An overview of λ Prolog, Proc. 5th Internat. Conf. on Logic Programming, 810-827 (1989)
[23] Nipkow, T., Higher-order critical pairs, (Proc. 6th Annual Symp. on Logic in Computer Science (1991), IEE: IEE New York)
[24] Pfenning, F.; Elliot, C., Higher-order abstract syntax, Proc. ACM SIGPLAN ’88 Conf. on Programming Language Design and Implementation (1988)
[25] Rus, T., Algebraic construction of compilers, Theoret. Comput. Sci., 90, 271-308 (1991) · Zbl 0746.68023
[26] Talcott, C. L., Binding structures, (Lifschitz, V., Artificial Intelligence and Mathematical Theory of Computation (1991), Academic Press: Academic Press New York) · Zbl 0755.68083
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.