αProlog:: A logic programming language with names, binding and α-equivalence

被引:50
作者
Cheney, J [1 ]
Urban, C
机构
[1] Cornell Univ, Ithaca, NY 14853 USA
[2] Univ Cambridge, Cambridge CB2 1TN, England
来源
LOGIC PROGRAMMING, PROCEEDINGS | 2004年 / 3132卷
关键词
D O I
10.1007/978-3-540-27775-0_19
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
There are two well-known approaches to programming with names, binding, and equivalence up to consistent renaming: representing names and bindings as concrete identifiers in a first-order language (such as Prolog), or encoding names and bindings as variables and abstractions in a higher-order language (such as lambdaProlog). However, both approaches have drawbacks: the former often involves stateful name-generation and requires manual definitions for alpha-equivalence and capture-avoiding substitution, and the latter is semantically very complicated, so reasoning about programs written using either approach can be very difficult. Gabbay and Pitts have developed a new approach to encoding abstract syntax with binding based on primitive operations of name-swapping and freshness. This paper presents alphaProlog, a logic programming language that uses this approach, along with several illustrative example programs and an operational semantics.
引用
收藏
页码:269 / 283
页数:15
相关论文
共 26 条
[1]  
Abel A., 2001, ELECT NOTES THEORETI, V58
[2]  
CHENEY J, 2004, IN PRESS P 31 INT C
[3]  
De Bruijn N. G., 1972, INDAG MATH, V34, P381, DOI DOI 10.1016/1385-7258(72)90034-0
[4]  
Despeyroux J., 1995, Typed Lambda Calculi and Applications. Second International Conference on Typed Lambda Calculi and Applications, TLCA '95. Proceedings, P124, DOI 10.1007/BFb0014049
[5]  
FIORE MP, 1999, LICS, V1999, P193
[6]   A new approach to abstract syntax with variable binding [J].
Gabbay, Murdoch J. ;
Pitts, Andrew M. .
Formal Aspects of Computing, 2002, 13 (3-5) :341-363
[7]  
GABBAY MJ, 2003, 35 YEARS AUTOMATH
[8]  
GABBAY MJ, 2004, IN PRESS P 19 ANN IE
[9]  
HAMANA M, 2001, LECT NOTES COMPUTER, V2215, P243
[10]  
Hofmann M., 1999, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), P204, DOI 10.1109/LICS.1999.782616