Lightweight Functional Logic Meta-Programming

被引:3
作者
Amin, Nada [1 ]
Byrd, William E. [2 ]
Rompf, Tiark [3 ]
机构
[1] Harvard Univ, Cambridge, MA 02138 USA
[2] Univ Alabama Birmingham, Birmingham, AL 35294 USA
[3] Purdue Univ, W Lafayette, IN 47907 USA
来源
PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2019 | 2019年 / 11893卷
基金
美国国家科学基金会; 美国国家卫生研究院;
关键词
D O I
10.1007/978-3-030-34175-6_12
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Meta-interpreters in Prolog are a powerful and elegant way to implement language extensions and non-standard semantics. But how can we bring the benefits of Prolog-style meta-interpreters to systems that combine functional and logic programming? In Prolog, a program can access its own structure via reflection, and meta-interpreters are simple to implement because the "pure" core language is small. Can we achieve similar elegance and power for larger systems that combine different paradigms? In this paper, we present a particular kind of functional logic metaprogramming, based on embedding a small first-order logic system in an expressive host language. Embedded logic engines are not new, as exemplified by various systems including miniKanren in Scheme and LogicT in Haskell. However, previous embedded systems generally lack metaprogramming capabilities in the sense of meta-interpretation. Indeed, shallow embeddings usually do not support reflection. Instead of relying on reflection for meta-programming, we show how to adapt popular multi-stage programming techniques to a logic programming setting and use the embedded logic to generate reified firstorder structures, which are again simple to interpret. Our system has an appealing power-to-weight ratio, based on the simple and general notion of dynamically scoped mutable variables. We also show how, in many cases, non-standard semantics can be realized without explicit reification and interpretation, but instead by customizing program execution through the host language. As a key example, we extend our system with a tabling/memoization facility. The need to interact with mutable variables renders this a highly nontrivial challenge, and the crucial insight is to extract symbolic representations of their side effects from memoized rules. We demonstrate that multiple independent semantic modifications can be combined successfully in our system, for example tabling and tracing.
引用
收藏
页码:225 / 243
页数:19
相关论文
共 37 条
[1]  
Alvis C.E, 2011, SCHEME
[2]  
Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14
[3]  
Bowen K.A., 1982, Logic Programming, P153
[4]  
Byrd W.E., 2017, PACML 1 ICFP, V8
[5]  
Byrd W.E., 2012, SCHEME
[6]  
Byrd W.E, 2009, RELATIONAL PROGRAMMI
[7]  
Carro M., 2011, TABLED LOGIC PROGRAM
[8]   HILOG - A FOUNDATION FOR HIGHER-ORDER LOGIC PROGRAMMING [J].
CHEN, WD ;
KIFER, M ;
WARREN, DS .
JOURNAL OF LOGIC PROGRAMMING, 1993, 15 (03) :187-230
[9]  
Claessen K, 2000, ELECT NOTES THEOR CO, V41, P37
[10]  
Codish M, 2002, LECT NOTES COMPUT SC, V2566, P109