miniKanren is famously small, but its implementations are not semantically simple. Can we understand those semantics as exactly the sum of their parts?

Researchers have explored many miniKanren designs, making different choices about search and control; in these alternative presentations we can find a common semantic substrate, and then isolate what each choice contributes. We organize a reduction semantics for miniKanren as a lattice-like family of complete semantic presentations. A relational core forms the base; delay and disjunction extend it independently; their join gives search. Hoisting, scheduling, and relation-call placement occupy other dimensions of the design space. We model miniKanren’s nondeterministic computation as deterministic transformations of an evolving search tree.

We echo Danvy and collaborators by following a refocusing, transition compression, fixed point fusion pipeline to give each such presentation a path to a corresponding big-step abstract machine. Fresh-variable representation cuts across this family and suggests a way to make these machines “leaner”. A proof-relevant structural account records scope and ownership in the search tree; an environment-localized account carries that information in each state; and the familiar counter-based implementation encodes it with numeric variables and an allocation counter.

The resulting picture offers another way to explain how traditional embedded implementation approaches compute.

Jason Hemann is an Assistant Professor of Computer Science in the Department of Mathematics and Computer Science at Seton Hall University. Hemann’s research interests include functional and logic programming DSLs. He focuses on embeddings and extensions to support logic programming in numerous host languages, transforming functional programs to relational ones, and teaching languages to support DSL programming. His microKanren model has inspired scores of implementations – more than 150, in over 50 host languages. Jason’s other interests concern novel uses of logic programming and symbolic constraint systems and typesafe embeddings of logic languages.

Jason’s research interests blend together with his teaching. His research questions tend to emerge from his teaching, and his results make it back into the classroom. An example of this approach can be found in his recently published textbook “The Reasoned Schemer, 2nd Edition”. He has been teaching in various capacities for over 15 years, including pre-college STEM programs, private professional training programs, and university courses at undergraduate and graduate levels. His awards include “Associate Instructor of the Year” at Indiana University.

Prior to joining SHU, Jason held Teaching Professor and Lecturer positions at Northeastern University and the Rose-Hulman Institute of Technology. Jason earned his Ph.D. in 2020 from the School of Informatics, Computing, and Engineering at Indiana University as part of the programming language research community and under the supervision of Dan Friedman. He earned his master’s in computer science from the School of Informatics and Computing at Indiana University, and both of his bachelor’s in computer science and philosophy and a bachelor of arts in history at Trinity University in San Antonio, Texas.