Abstract Syntax and Logic Programming
Abstract Syntax and Logic Programming
复制标题
抽象语法和逻辑编程
DOI：
10.1007/3-540-55460-2_24
复制
发表时间：
1990
期刊：
影响因子：
--
通讯作者：
D. Miller
中科院分区：
文献类型：
--
作者：
D. Miller
当编写程序来操纵诸如代数表达式、逻辑公式、证明和程序之类的结构时，将这些结构的线性的、面向人的、具体的语法解析成更面向计算的语法是非常理想的。对于各种各样的操作，具体的语法包含太多无用的信息(例如，关键字和空格)，而重要的信息没有明确地表示(例如，函数-参数关系和运算符的范围)。在语法分析树中，许多语义上无用的信息被删除，而其他关系，如函数和参数之间的关系，则变得更加明确。遗憾的是，解析树不能充分解决对象级语法的重要概念，例如绑定和释放对象变量、作用域、绑定变量的字母更改和对象级替换。我将在这里争辩说，这些对象的抽象语法应该围绕α术语的λ等价类来组织，而不是语法分析树。将抽象语法的概念结合到编程语言中是一个有趣的挑战。本文简要描述了一种直接支持这种语法概念的逻辑程序设计语言。给出了该编程语言的一个实例规范，以说明其处理对象级语法的方法。给出了该逻辑程序设计语言的模型论语义。
When writing programs to manipulate structures such as algebraic expressions, 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 computation-oriented syntax. For a wide variety of manipulations, concrete syntax contains too much useless information (e.g., keywords and white space) while important information 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 theabstract syntaxof such objects should be organized aroundα-equivalence classes of λ-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 programming language is presented to illustrate its approach to handling object-level syntax. A model theoretic semantics for this logic programming language is also presented.
LLPTTP：使用线性逻辑编程语言编译器的定理证明器
DOI：
--
发表时间：
2003
期刊：
Computer Software 20-5
影响因子：
--
作者：
N.Tamura;M.Banbara
通讯作者：
M.Banbara