Free variables and subexpressions in higher-order meta logic
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.
KeywordsLogic Program Logic Programming Free Variable Parent Term Logic Programming Language
Unable to display preview. Download preview PDF.
- 2.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.Google Scholar
- 3.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.Google Scholar
- 6.P. M. Hill and J. G. Gallagher. Meta-programming in logic programming. Technical Report Report 94.22, University of Leeds, firstname.lastname@example.org, August 1994. To appear in Vol. 5 of the Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press.Google Scholar
- 8.Chuck Liang. Substitution, Unification and Generalization in Meta-Logic. PhD thesis, University of Pennsylvania, September 1995.Google Scholar
- 9.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.Google Scholar
- 10.R. McDowell and D. Miller. A logic for reasoning with higher-order abstract syntax. In Symposium on Logic in Computer Science. IEEE, 1997.Google Scholar
- 11.Dale Miller. Abstractions in logic programming. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 329–359. Academic Press, 1990.Google Scholar
- 13.Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, pages 321–358, 1992.Google Scholar
- 15.Tobias Nipkow. Higher-order critical pairs. In G. Kahn, editor, Sixth Annual Symposium on Logic in Computer Science, pages 342–349. IEEE, July 1991.Google Scholar
- 17.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.Google Scholar