Abstract
This paper addresses the problem of how to represent free variables and subexpressions involving Β-bindings. The aim is to apply what is known as higher-order abstract syntax to higher-order term rewriting systems. Directly applying Β-reduction for the purpose of subterm-replacement is incompatible with the requirements of term-rewriting. A new meta-level representation of subterms is developed that will allow term-rewriting systems to be formulated in a higher-order meta logic.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76(2/3):95–120, February/March 1988.
JoËlle Despeyroux, Amy Felty, and André Hirschowitz. Higher-order abstract syntax in Coq. In Second International Conference on Typed Lambda Calculi and Applications, pages 124–138. Springer-Verlag Lecture Notes in Computer Science, April 1995.
Amy Felty. A logic programming approach to implementing higher-order term rewriting. In Lars-Henrik Eriksson, Lars HallnÄs, and Peter Schroeder-Heister, editors, Proceedings of the January 1991 Workshop on Extensions to Logic Programming, volume 596 of Lecture Notes in Artificial Intelligence, pages 135–161. Springer-Verlag, 1992.
Amy Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11(1):43–81, August 1993.
John Hannan. Extended natural semantics. Journal of Functional Programming, 3(2):123–152, April 1993.
P. M. Hill and J. G. Gallagher. Meta-programming in logic programming. Technical Report Report 94.22, University of Leeds, hill@scs.leeds.ac.uk, August 1994. To appear in Vol. 5 of the Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press.
Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.
Chuck Liang. Substitution, Unification and Generalization in Meta-Logic. PhD thesis, University of Pennsylvania, September 1995.
Chuck Liang. Let-polymorphism and eager type schemes. In TAPSOFT '97: Theory and Practice of Software Development, pages 490–501. Springer Verlag LNCS Vol. 1214, 1997.
R. McDowell and D. Miller. A logic for reasoning with higher-order abstract syntax. In Symposium on Logic in Computer Science. IEEE, 1997.
Dale Miller. Abstractions in logic programming. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 329–359. Academic Press, 1990.
Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.
Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, pages 321–358, 1992.
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.
Tobias Nipkow. Higher-order critical pairs. In G. Kahn, editor, Sixth Annual Symposium on Logic in Computer Science, pages 342–349. IEEE, July 1991.
Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–397, September 1989.
Frank Pfenning and Conal Elliot. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199–208. ACM Press, June 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liang, C. (1998). Free variables and subexpressions in higher-order meta logic. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055141
Download citation
DOI: https://doi.org/10.1007/BFb0055141
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64987-8
Online ISBN: 978-3-540-49801-8
eBook Packages: Springer Book Archive