We present a deterministic small-step operational semantics for miniKanren that explicitly represents the evolving search tree during execution. This semantics models interleaving and goal scheduling with fine granularity, exposing each evaluation step—goal activation, suspension, resumption, and success. This approach supports reasoning about miniKanren’s interleaving search behavior, helping users understand surprising answer orders and operational effects. A reference implementation undergirds an interactive visualizer that renders the search tree as it develops and lets users step through execution; we treat this tool as a consumer and demonstration of the semantics. Our semantics and tool are illustrated by example and validated through property-based testing.
Given the increased importance of physical AI, reliable planning in dynamic environments remains a critical function of embodied systems. In particular, care must be taken in how they interact with situations outside the boundaries of their training. While planning languages such as PDDL or STRIPS tend to be highly problem-dependent, LLMs can be applied to broader and more general tasks in dynamic environments, but remain prone to hallucinations. Logic-based systems, in contrast, provide frameworks for a wide variety of problems and offer justifications for complete and correct plans, but offer no explanation when they cannot generate a plan. For example, VECSR, a planning system based on the s(CASP) answer set programming system, can create plans for unseen tasks by generalizing from a small number of training tasks. However, this generalization is limited to tasks achievable with actions learned during training. To address this limitation, we propose and build the Counterfactual Generation Module, which exploits the justification framework of s(CASP) to identify counterfactuals for unachievable tasks. These counterfactuals allow us to detect missing actions that should be incorporated into VECSR’s knowledge base to enable task completion. We validate our proposal by asking VECSR to generate action plans for 55 tasks outside the 10 it was trained on. For 16 tasks, VECSR could not produce plans, and the counterfactuals “identified” the actions that need to be learned to complete 13 of them. Next, we evaluated 56 plans generated by GPT-4o, observing that the module’s assessment of plan correctness corresponded to human evaluation, supporting that the module itself is correct.
We unify functional and logic programming by treating predicates as functions equipped with their support: the set of inputs whose output is nonzero. Datalog, for instance, is a language of finitely supported boolean functions. Finite support allows representing functions as input-output tables. Generalizing from boolean functions to other pointed sets neatly handles aggregation and weighted logic programming. We refer to the combination of finitely supported functions, represented as data, with higher order functions, represented as code, as finite functional programming. We give a simple type system to check finite support, using graded effects to check variable grounding and relevance types to model pointed sets.
This paper introduces a logic programming language called Demonic Dynamic Logic Programming. It is based on the ground, Demonic fragment of propositional dynamic logic, a well-studied program logic. Syntax, operational semantics and proof-theoretic semantics are presented. The theoretical foundations are validated by proving theorems such as soundness and existence of uniform proofs. Applications to two-player mathematical games are discussed and a pursuit-evasion game on a graph is presented as a concrete example. By bringing program logic and logic programming together, we hope to improve reasoning about imperative programs within logic programs. Future work is discussed, including extensions to game logic which hold the potential to generate winning strategies of games.
Playing with monoids and discovering for oneself how frequently they turn up in various guises and how much is expressed by them is a delight. Not only it brightens the day of important but frankly boring data analytics. Not only it challenges to discover efficient (with the constant time and space operation) monoids, which demands ingenuity. In the words of Guy Steele, inventing efficient associative combining operators is a very big deal. An efficient monoid opens up parallel implementations not just parallel but embarrassingly parallel: The input sequence arbitrarily partitioned among workers, all running in parallel with no races, dependencies or even memory bank conflicts. This is the ideal for multi-core, GPU or distributed processing. In this paper we show why monoids are a big deal, and also a big fun even more than expected. Horner rule and Boyer-Moore majority voting commonly regarded as prototypically inherently sequential turn out monoids, and hence embarrassingly parallelizable. As we generalize monoids to observable monoids, we discover a new, vertical way to combine them, enabling efficient iterated grouping and aggregation directly on raw deserialized (big) data, on multicore or multi-processor.
