Abstract syntax and logic programming

Abstract. When writing programs to manipulate structures such as algebraic ex-pressions, logical formulas, proofs, and programs, it is highly desirable to take the linear, human-oriented, concrete syntax of these structures and parse them into a more comput at ion-oriented syntax. For a wide variety of manipulations, concrete syntax contains too much useless information ( e.g., keywords and white space) while impor-tant-informat ion is not explicitly represented (e.g., function-argument relations and the scope of operators). In parse trees, much of the semantically useless information is removed while other relationships, such as between function and argument, are made more explicit. Unfortunately, parse trees do not adequately address important notions of object-level syntax, such as bound and free object-variables, scopes, alphabetic changes of bound variables, and object-level substitution. I will argue here that the abstract syn-tax of such objects should be organized around a-equivalence classes of A-terms instead of parse trees. Incorporating this notion of abstract syntax into programming languages is an interesting challenge. This paper briefly describes a logic programming language that directly supports this notion of syntax. An example specifications in this program