Relational Programming in miniKanren: Techniques, Applications, and Implementations

The promise of logic programming is that programs can be written <italic>relationally</italic>, without distinguishing between input and output arguments. Relational programs are remarkably flexible&mdash;for example, a relational type-inferencer also performs type checking and type inhabitation, while a relational theorem prover generates theorems as well as proofs and can even be used as a simple proof assistant. Unfortunately, writing relational programs is difficult, and requires many interesting and unusual tools and techniques. For example, a relational interpreter for a subset of Scheme might use nominal unification to support variable binding and scope, Constraint Logic Programming over Finite Domains (CLP(FD)) to implement relational arithmetic, and tabling to improve termination behavior. In this dissertation I present <italic>miniKanren</italic>, a family of languages specifically designed for relational programming, and which supports a variety of relational idioms and techniques. I show how miniKanren can be used to write interesting relational programs, including an extremely flexible lean tableau theorem prover and a novel constraint-free binary arithmetic system with strong termination guarantees. I also present interesting and practical techniques used to implement miniKanren, including a nominal unifier that uses triangular rather than idempotent substitutions and a novel &ldquo;walk&rdquo;-based algorithm for variable lookup in triangular substitutions. The result of this research is a family of languages that supports a variety of relational idioms and techniques, making it feasible and useful to write interesting programs as relations.

Grantor dc:publisher

[Bloomington, Ind.] : Indiana University

Year dc:date.issued

2010

Author dc:creator

• Byrd, William E.

Advisor dc:contributor.advisor

• Friedman, Daniel P

• relational programming
• miniKanren
• logic programming
• Scheme

Statement dc:rights

• This work is licensed under the Creative Commons Attribution-By 3.0 Unported License

Licence dc:rights.uri

• http://creativecommons.org/licenses/by/3.0/

Language dc:language.iso

EN

Handle dc:identifier.uri

https://hdl.handle.net/2022/8777

OAI identifier oai:identifier

oai:scholarworks.iu.edu:2022/8777