{"id":{"repo_id":"iu","oai_identifier":"oai:scholarworks.iu.edu:2022/8777"},"canonical_url":"https://search.dev.ndltd.org/etd/iu/oai:scholarworks.iu.edu:2022/8777","repository":{"repo_id":"iu","name":"Indiana University","base_url":"https://scholarworks.iu.edu/iuswrrest/oai/request"},"display":{"title":"Relational Programming in miniKanren: Techniques, Applications, and Implementations","abstract":"The promise of logic programming is that programs can be written relationally, without distinguishing between input and output arguments. Relational programs are remarkably flexible—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 miniKanren, 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 “walk”-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.","abstract_html":"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—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 “walk”-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.","abstract_has_math":false,"creators":["Byrd, William E."],"institution":"[Bloomington, Ind.] : Indiana University","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Friedman, Daniel P"],"committee_chairs":[],"committee_members":[],"year":2010,"date_issued":"2010-06-16","date_published":"2010-06-16","updated_at":"2026-07-24T02:40:11Z","subjects":["relational programming","miniKanren","logic programming","Scheme"],"languages":["EN"],"rights":["This work is licensed under the Creative Commons Attribution-By 3.0 Unported License"],"rights_urls":["http://creativecommons.org/licenses/by/3.0/"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2022/8777","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Friedman, Daniel P"]},{"key":"dc:creator","label":"Author","values":["Byrd, William E."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2010-06-16T17:43:40Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2011-05-14T11:54:55Z"]},{"key":"dc:date.issued","label":"Date","values":["2010-06-16"]},{"key":"dc:publisher","label":"Institution","values":["[Bloomington, Ind.] : Indiana University"]},{"key":"dc:type","label":"Dc Type","values":["Doctoral Dissertation"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["relational programming","miniKanren","logic programming","Scheme"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["EN"]},{"key":"dc:rights","label":"Dc Rights","values":["This work is licensed under the Creative Commons Attribution-By 3.0 Unported License"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://creativecommons.org/licenses/by/3.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/2022/8777"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis (Ph.D.) - Indiana University, Computer Sciences, 2009"]},{"key":"dc:description.abstract","label":"Abstract","values":["The promise of logic programming is that programs can be written relationally, without distinguishing between input and output arguments. Relational programs are remarkably flexible—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 miniKanren, 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 “walk”-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."]},{"key":"dc:title","label":"Title","values":["Relational Programming in miniKanren: Techniques, Applications, and Implementations"]}]}],"canonical_facts":{"dc:contributor.advisor":["Friedman, Daniel P"],"dc:creator":["Byrd, William E."],"dc:date.accessioned":["2010-06-16T17:43:40Z"],"dc:date.available":["2011-05-14T11:54:55Z"],"dc:date.issued":["2010-06-16"],"dc:description":["Thesis (Ph.D.) - Indiana University, Computer Sciences, 2009"],"dc:description.abstract":["The promise of logic programming is that programs can be written relationally, without distinguishing between input and output arguments. Relational programs are remarkably flexible—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 miniKanren, 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 “walk”-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."],"dc:identifier.uri":["https://hdl.handle.net/2022/8777"],"dc:language.iso":["EN"],"dc:publisher":["[Bloomington, Ind.] : Indiana University"],"dc:rights":["This work is licensed under the Creative Commons Attribution-By 3.0 Unported License"],"dc:rights.uri":["http://creativecommons.org/licenses/by/3.0/"],"dc:subject":["relational programming","miniKanren","logic programming","Scheme"],"dc:title":["Relational Programming in miniKanren: Techniques, Applications, and Implementations"],"dc:type":["Doctoral Dissertation"]},"updated_at":"2026-07-24T02:40:11Z"}