Abstract for "Definite Clause Grammars for Parsing Higher-Order Syntax"
Definite Clause Grammars for Parsing Higher-Order Syntax
Amy Felty. Presented at the 1993 International Symposium on Logic Programming, October 1993.

Abstract: The higher-order logic programming language lambda Prolog contains the simply-typed lambda-terms as its basic data structures. These terms can be used to elegantly express the higher-order abstract syntax of objects that include notions of bound variables such as formulas, proofs, and programs. Current implementations of lambda Prolog, however, have no provision for a programmer to provide a concrete syntax for a particular object-level language. Such a capability is desirable, for example, in implementing an interactive theorem prover. Providing the user with a familiar syntax for the logic being implemented can greatly enhance interaction. In this paper, we extend the Definite Clause Grammar formalism of Prolog to a typed higher-order version in lambda Prolog and show how such grammars can be applied to the problem of parsing concrete syntax into higher-order syntax. We also present a program for translating grammar specifications to lambda Prolog programs. These programs serve as parsers for the specified languages. This translation is itself presented as a lambda Prolog program.