research-article

A small embedding of logic programming with a simple complete search

Authors:

Daniel P. Friedman,

William E. Byrd,

Matthew MightAuthors Info & Claims

DLS 2016: Proceedings of the 12th Symposium on Dynamic Languages

Pages 96 - 107

https://doi.org/10.1145/2989225.2989230

Published: 01 November 2016 Publication History

Abstract

We present a straightforward, call-by-value embedding of a small logic programming language with a simple complete search. We construct the entire language in 54 lines of Racket---half of which implement unification. We then layer over it, in 43 lines, a reconstruction of an existing logic programming language, miniKanren, and attest to our implementation's pedagogical value. Evidence suggests our combination of expressiveness, concision, and elegance is compelling: since microKanren's release, it has spawned over 50 embeddings in over two dozen host languages, including Go, Haskell, Prolog and Smalltalk.

References

[1]

Franz Baader and Wayne Snyder. Unification theory. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 445–532. Elsevier and MIT Press, 2001.

[2]

Isaac Balbin and Koenraad Lecot. Logic Programming: A Classified Bibliography. Springer Science & Business Media, 2012.

Digital Library

[3]

Michel Billaud. Prolog Control Structures: a Formalization and its Applications. In K. Fuhi and M. Nivat, editors, Programming of Future Generation Computers, pages 57–73. Elsevier Science Publishers, 1988.

Digital Library

[4]

William E. Byrd and Daniel P. Friedman. αKanren: A Fresh Name in Nominal Logic Programming. In Scheme 8, pages 79–90 (see also http://webyrd.net/alphamk/alphamk.pdf for improvements ), 2007.

[5]

William E. Byrd, Eric Holk, and Daniel P. Friedman. miniKanren, Live and Untagged: Quine Generation via Relational Interpreters (Programming Pearl). In Scheme 12, September 2012.

Digital Library

[6]

Venanzio Capretta. General recursion via coinductive types. Logical Methods in Computer Science, 1(2), 2005.

[7]

Mats Carlsson. On implementing Prolog in functional programming. New Generation Computing, 2(4):347–359, 1984.

[8]

Matthew Flatt and PLT. Reference: Racket. Technical Report PLT-TR-2010-1, PLT Design Inc., 2010. http:// racket-lang.org/tr1/.

[9]

Andreas Fordan. Projection in Constraint Logic Programming. Ios Press, 1999.

[10]

Daniel P. Friedman and Oleg Kiselyov. A declarative applicative logic programming system, 2005.

[11]

Daniel P. Friedman, William E. Byrd, and Oleg Kiselyov. The Reasoned Schemer. MIT Press, Cambridge, MA, 2005.

Digital Library

[12]

Steven E. Ganz, Daniel P. Friedman, and Mitchell Wand. Trampolined Style. In Proc. 4th ICFP, pages 18–27. ACM, 1999.

Digital Library

[13]

Jason Hemann and Daniel P. Friedman. µKanren: A minimal functional core for relational programming. In Scheme 13, 2013.

[14]

Jason Hemann and Daniel P. Friedman. A framework for extending microkanren with constraints. In Scheme 15, 2015.

[15]

Forthcoming.

[16]

Ralf Hinze. Deriving backtracking monad transformers. In ACM SIGPLAN Notices, volume 35, pages 186–197. ACM, 2000.

Digital Library

[17]

Ralf Hinze. Prolog’s control constructs in a functional setting: Axioms and implementation. International Journal of Foundations of Computer Science, 12(02):125–170, 2001.

[18]

Joxan Jaffar, Michael J. Maher, Peter J. Stuckey, and Roland HC Yap. Output in CLP(R). In Fifth Generation Computing Systems, pages 987–995, 1992.

[19]

Oleg Kiselyov. The taste of logic programming, 2006.

[20]

Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry. Backtracking, interleaving, and terminating monad transformers: (functional pearl). In Olivier Danvy and Benjamin C. Pierce, editors, Proceedings of the 10th ACM SIGPLAN ICFP, pages 192–203. ACM, September 2005.

Digital Library

[21]

H. J. Komorowski. QLOG: The programming environment for PROLOG in LISP. In K. L. Clark et al., editors, Logic Programming, pages 315–324. Academic Press, 1982.

[22]

Robert A. Kowalski. Logic for Problem Solving. North-Holland/Elsevier, 1979.

Digital Library

[23]

Ramana Kumar. Mechanising Aspects of miniKanren in HOL, 2010. Australian National University. Bachelors thesis.

[24]

Lee Naish. Pruning in logic programming. Technical report, Technical Report 95/16, Department of Computer Science, University of Melbourne, June 1995.

[25]

Joseph P. Near, William E. Byrd, and Daniel P. Friedman. αleanTAP : A declarative theorem prover for first-order classical logic.

[26]

John Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM (JACM), 12(1):23– 41, 1965.

Digital Library

[27]

Silvija Seres. The Algebra of Logic Programming. PhD thesis, University of Oxford, 2001.

[28]

Olin Shivers. List Library. Scheme Request for Implementation. SRFI-1, 1999.

[29]

Ben A. Sijtsma. On the productivity of recursive list definitions. ACM Trans. Program. Lang. Syst., 11(4):633–649, October 1989.

Digital Library

[30]

JM Spivey and Silvija Seres. Embedding Prolog in Haskell. In E. Meier, editor, Haskell 99, 1999.

Cited By

Prott KTeegen FChristiansen J(2023)Embedding Functional Logic Programming in Haskell via a Compiler PluginPractical Aspects of Declarative Languages10.1007/978-3-031-24841-2_3(37-55)Online publication date: 8-Jan-2023
https://doi.org/10.1007/978-3-031-24841-2_3
Rozplokhas DVyatkin ABoulytchev D(2020)Certified Semantics for Relational ProgrammingProgramming Languages and Systems10.1007/978-3-030-64437-6_9(167-185)Online publication date: 24-Nov-2020
https://doi.org/10.1007/978-3-030-64437-6_9
Kosarev DBoulytchev D(2018)Typed Embedding of a Relational Language in OCamlElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.285.1285(1-22)Online publication date: 31-Dec-2018
https://doi.org/10.4204/EPTCS.285.1
Show More Cited By

Index Terms

A small embedding of logic programming with a simple complete search
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types

Recommendations

A unified approach to solving seven programming problems (functional pearl)

We present seven programming challenges in Racket, and an elegant, unified approach to solving them using constraint logic programming in miniKanren.
Backtracking, interleaving, and terminating monad transformers: (functional pearl)
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

We design and implement a library for adding backtracking computations to any Haskell monad. Inspired by logic programming, our library provides, in addition to the operations required by the MonadPlus interface, constructs for fair disjunctions, fair ...
miniKanren, live and untagged: quine generation via relational interpreters (programming pearl)
Scheme '12: Proceedings of the 2012 Annual Workshop on Scheme and Functional Programming

We present relational interpreters for several subsets of Scheme, written in the pure logic programming language miniKanren. We demonstrate these interpreters running "backwards"---that is, generating programs that evaluate to a specified value---and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DLS 2016: Proceedings of the 12th Symposium on Dynamic Languages

November 2016

131 pages

ISBN:9781450344456

DOI:10.1145/2989225

Program Chair:
Roberto Ierusalimschy
PUC-Rio, Brazil

ACM SIGPLAN Notices Volume 52, Issue 2
DLS '16
February 2017
131 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3093334
Editor:
Matthew Fluet
Issue’s Table of Contents

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGAda: ACM Special Interest Group on Ada Programming Language

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '16

Sponsor:

SIGPLAN

SPLASH '16: Conference on Systems, Programming, Languages, and Applications: Software for Humanity

November 1, 2016

Amsterdam, Netherlands

Acceptance Rates

Overall Acceptance Rate 32 of 77 submissions, 42%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
446
Total Downloads

Downloads (Last 12 months)14
Downloads (Last 6 weeks)4

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Prott KTeegen FChristiansen J(2023)Embedding Functional Logic Programming in Haskell via a Compiler PluginPractical Aspects of Declarative Languages10.1007/978-3-031-24841-2_3(37-55)Online publication date: 8-Jan-2023
https://doi.org/10.1007/978-3-031-24841-2_3
Rozplokhas DVyatkin ABoulytchev D(2020)Certified Semantics for Relational ProgrammingProgramming Languages and Systems10.1007/978-3-030-64437-6_9(167-185)Online publication date: 24-Nov-2020
https://doi.org/10.1007/978-3-030-64437-6_9
Kosarev DBoulytchev D(2018)Typed Embedding of a Relational Language in OCamlElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.285.1285(1-22)Online publication date: 31-Dec-2018
https://doi.org/10.4204/EPTCS.285.1
Rozplokhas DBoulytchev DSabel DThiemann P(2018)Improving Refutational Completeness of Relational Search via Divergence TestProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236958(1-13)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236958
Hemann JFriedman D(2017)A Framework for Extending microKanren with ConstraintsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.234.10234(135-149)Online publication date: 1-Jan-2017
https://doi.org/10.4204/EPTCS.234.10
Rozplokhas DBoulytchev DSabel DThiemann P(2018)Improving Refutational Completeness of Relational Search via Divergence TestProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236958(1-13)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236958
Lozov PVyatkin ABoulytchev D(2018)Typed Relational ConversionTrends in Functional Programming10.1007/978-3-319-89719-6_3(39-58)Online publication date: 19-Apr-2018
https://doi.org/10.1007/978-3-319-89719-6_3

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents