pith. sign in

arxiv: 2605.15406 · v1 · pith:O2T66WJJnew · submitted 2026-05-14 · 💻 cs.PL

Polymorphic Bottom-Up Weighted Relational Programming

Dmitri Volkov This is my paper

Pith reviewed 2026-05-19 14:46 UTC · model grok-4.3

classification 💻 cs.PL
keywords polymorphismrelational programmingbottom-up evaluationweighted relationscompilationsemiringprogramming languageslogic programming
0
0 comments X

The pith

Polymorphic semiringKanren programs compile to non-polymorphic versions via equality patterns and large instances while preserving semantics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces semiringKanren as a bottom-up weighted relational language and extends it to include polymorphism. It then defines a compilation process that rewrites polymorphic programs into non-polymorphic equivalents by inserting equality patterns and replacing each polymorphic relation with a sufficiently large concrete instance. This approach is shown to maintain both the original relational semantics and the weighting behavior across all inputs. The result matters because it offers a route to polymorphic code in bottom-up relational settings without requiring wholesale monomorphization of the program.

Core claim

The central claim is that a polymorphic extension of semiringKanren can be reduced to a non-polymorphic program by a method that uses equality patterns together with large-enough instances of each polymorphic relation, and that this reduction is semantics-preserving and weight-preserving, as established by a correctness proof.

What carries the argument

The compilation method that replaces polymorphic relations with equality patterns and sufficiently large concrete instances.

If this is right

  • Existing non-polymorphic bottom-up evaluators can now execute polymorphic programs after a single compilation step.
  • The weighting semantics of relational queries remain unchanged under the translation.
  • Polymorphism can be added to bottom-up relational languages without altering their core execution engines.
  • Code reuse across different relation arities becomes possible while retaining bottom-up efficiency.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same pattern-based instantiation technique could be adapted to other weighted logic programming systems that lack built-in polymorphism.
  • Automatic determination of minimal sufficient instance sizes might reduce the overhead of the compilation step in practice.
  • The method opens a path to polymorphic relational queries in domains such as probabilistic databases or constraint solving without full program expansion.

Load-bearing premise

Equality patterns together with large enough concrete instances of polymorphic relations are sufficient to reproduce the full semantics and weighting of the original polymorphic program on every input.

What would settle it

A specific polymorphic program and input for which the compiled non-polymorphic version yields different answers or different weights than the original polymorphic version.

Figures

Figures reproduced from arXiv: 2605.15406 by Dmitri Volkov.

Figure 2.1
Figure 2.1. Figure 2.1: Syntax for semiringKanren. ∆ ⊢ sole : Unit ∆ ⊢ v : τ1 ∆ ⊢ (left(Sum τ1 τ2) v) : (Sum τ1 τ2) ∆ ⊢ v : τ2 ∆ ⊢ (right(Sum τ1 τ2) v) : (Sum τ1 τ2) ∆ ⊢ v1 : τ1 ∆ ⊢ v2 : τ2 ∆ ⊢ (pair v1 v2) : (Prod τ1 τ2) ∆, x : τ ⊢ x : τ [PITH_FULL_IMAGE:figures/full_fig_p012_2_1.png] view at source ↗
Figure 2.2
Figure 2.2. Figure 2.2: Inference rules for value typing judgement. [PITH_FULL_IMAGE:figures/full_fig_p012_2_2.png] view at source ↗
Figure 2.3
Figure 2.3. Figure 2.3: Inference rules for goal typing judgement. [PITH_FULL_IMAGE:figures/full_fig_p013_2_3.png] view at source ↗
Figure 2.4
Figure 2.4. Figure 2.4: Inference rules for relation and program typing judgements. [PITH_FULL_IMAGE:figures/full_fig_p013_2_4.png] view at source ↗
Figure 2.5
Figure 2.5. Figure 2.5: Denotational semantics for types [PITH_FULL_IMAGE:figures/full_fig_p014_2_5.png] view at source ↗
Figure 2.6
Figure 2.6. Figure 2.6: Denotational semantics for values. J(conj g1 g2)K(γ; δ) = Jg1K(γ; δ) × Jg2K(γ; δ) J(disj g1 g2)K(γ; δ) = Jg1K(γ; δ) + Jg2K(γ; δ) J(fresh ((x : τ)) g)K(γ; δ) = X v∈JτK JgK(γ; δ, x 7→ v) J(== v1 v2)K(γ; δ) = ( 1 if Jv1K(δ) = Jv2K(δ) 0 if Jv1K(δ) ̸= Jv2K(δ) J(=/= v1 v2)K(γ; δ) = ( 1 if Jv1K(δ) ̸= Jv2K(δ) 0 if Jv1K(δ) = Jv2K(δ) J(R ⃗v)K(γ; δ) = γ(R)(J⃗vK(δ)) where ⃗v : ⃗τ J(factor r)K(γ; δ) = r [PITH_FULL_I… view at source ↗
Figure 2.7
Figure 2.7. Figure 2.7: Denotational semantics for goals. values for values that do not include variables. The denotation for values turns arbitrary values (which may contain variables) into concrete values. To this end, we take a value environment δ, consisting of entries of the form x 7→ v, where x is a variable name and v is a concrete value. For δ to be valid, each value entry x 7→ v should have a matching type entry x : τ … view at source ↗
Figure 2.8
Figure 2.8. Figure 2.8: Denotational semantics for relations and programs. [PITH_FULL_IMAGE:figures/full_fig_p016_2_8.png] view at source ↗
Figure 3.1
Figure 3.1. Figure 3.1: Syntax for polymorphic semiringKanren instances of polymorphic relations, where polymorphic relation calls with arbi￾trary type mappings are compiled to only use a single type mapping, with extra code generated at call sites to reconstruct the desired types. We first present the syntax and typing rules for semiringKanren extended with polymorphic relations. Next, we provide a semantics for polymorphic se… view at source ↗
Figure 3.2
Figure 3.2. Figure 3.2: Inference rules for polymorphic type validity judgement. [PITH_FULL_IMAGE:figures/full_fig_p021_3_2.png] view at source ↗
Figure 3.3
Figure 3.3. Figure 3.3: Inference rules for polymorphic value typing judgement. [PITH_FULL_IMAGE:figures/full_fig_p021_3_3.png] view at source ↗
Figure 3.4
Figure 3.4. Figure 3.4: Inference rules for polymorphic goal typing judgement. [PITH_FULL_IMAGE:figures/full_fig_p021_3_4.png] view at source ↗
Figure 3.5
Figure 3.5. Figure 3.5: Inference rules for polymorphic relation and program typing judge [PITH_FULL_IMAGE:figures/full_fig_p022_3_5.png] view at source ↗
Figure 3.6
Figure 3.6. Figure 3.6: Denotational semantics for types, again. [PITH_FULL_IMAGE:figures/full_fig_p023_3_6.png] view at source ↗
Figure 3.7
Figure 3.7. Figure 3.7: Denotational semantics for values, again. [PITH_FULL_IMAGE:figures/full_fig_p023_3_7.png] view at source ↗
Figure 3.8
Figure 3.8. Figure 3.8: Denotational semantics for polymorphic goals. [PITH_FULL_IMAGE:figures/full_fig_p024_3_8.png] view at source ↗
Figure 3.9
Figure 3.9. Figure 3.9: Denotational semantics for polymorphic relations and programs. [PITH_FULL_IMAGE:figures/full_fig_p024_3_9.png] view at source ↗
read the original abstract

This work presents a new approach for implementing polymorphism for bottom-up relational languages, without monomorphization. We begin by introducing semiringKanren, a bottom-up weighted relational programming language. We extend this base language to support polymorphism. We describe a new method to compile polymorphic semiringKanren programs into non-polymorphic ones, based on equality patterns and large-enough instances of polymorphic relations. We prove the correctness of this method. Finally, we consider existing work and suggest directions for future research.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper introduces semiringKanren, a bottom-up weighted relational programming language, extends it to support polymorphism, and presents a compilation method that translates polymorphic programs into non-polymorphic ones using equality patterns together with sufficiently large concrete instances of each polymorphic relation. A correctness proof is given that the compiled program preserves both the relational semantics and the semiring weighting of the original polymorphic program.

Significance. If the central claim holds, the result is significant because it supplies a parameter-free route to polymorphism in bottom-up relational languages that avoids the code-size explosion of full monomorphization while still guaranteeing semantic and weighting equivalence. The self-contained proof and the reduction to equality-pattern coverage constitute concrete, falsifiable strengths that distinguish the work from prior monomorphization-based approaches.

minor comments (3)
  1. [§3] §3 (definition of semiringKanren): the grammar and weighting rules are introduced without an explicit statement of the semiring axioms assumed; adding a short enumerated list would remove any ambiguity for readers unfamiliar with weighted logic programming.
  2. [§5] §5 (compilation): the notion of 'large-enough' instance size is defined operationally via equality-pattern coverage, but no explicit bound or algorithm for computing the required size is stated; a short paragraph or pseudocode fragment would make the construction fully constructive.
  3. [Related work] Related-work section: the comparison to monomorphization in miniKanren variants and to polymorphic type systems in logic programming is present but terse; one additional paragraph contrasting the equality-pattern technique with existing approaches would strengthen the novelty claim.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our work, the recognition of its potential significance in providing a parameter-free route to polymorphism, and the recommendation for minor revision. We are pleased that the self-contained proof and reduction to equality-pattern coverage are viewed as strengths.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines semiringKanren, extends it with polymorphism, presents a compilation method using equality patterns and sufficiently large concrete instances of polymorphic relations, and supplies an independent correctness proof for semantic and weighting preservation. No equation, definition, or central claim reduces by construction to a fitted input, self-citation chain, or prior result by the same authors; the argument is parameter-free and self-contained within the manuscript.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on standard assumptions about semiring semantics and relational evaluation order that are common in the field; no new free parameters or invented entities are introduced in the abstract.

axioms (1)
  • domain assumption The base semiringKanren language has well-defined bottom-up semantics over semirings.
    Invoked as the starting point before the polymorphic extension is defined.

pith-pipeline@v0.9.0 · 5590 in / 1241 out tokens · 93295 ms · 2026-05-19T14:46:50.623457+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages · 3 internal anchors

  1. [1]

    Convergence of datalog over (Pre-) Semir- ings

    Mahmoud Abo Khamis et al. “Convergence of datalog over (Pre-) Semir- ings”. In:J. ACM71.2 (Apr. 2024).issn: 0004-5411.doi:10 . 1145 / 3643027.url:https://doi.org/10.1145/3643027

    work page doi:10.1145/3643027 2024

  2. [2]

    Polymorphism in Datalog and Inheritance in a Metamodel

    Paolo Atzeni, Giorgio Gianforme, and Daniele Toti. “Polymorphism in Datalog and Inheritance in a Metamodel”. In:Foundations of Information and Knowledge Systems. Ed. by Sebastian Link and Henri Prade. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, pp. 114–132.isbn: 978-3- 642-11829-6

    work page 2010

  3. [3]

    Aaron Bembenek and Stephen Chong.FormuLog: Datalog for static anal- ysis involving logical formulae. 2018. arXiv:1809.06274 [cs.PL].url: https://arxiv.org/abs/1809.06274

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  4. [4]

    Testing Polymorphic Properties

    Jean-Philippe Bernardy, Patrik Jansson, and Koen Claessen. “Testing Polymorphic Properties”. In:Programming Languages and Systems. Ed. by Andrew D. Gordon. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, pp. 125–144.isbn: 978-3-642-11957-6

    work page 2010

  5. [5]

    miniKanren, live and un- tagged: quine generation via relational interpreters (programming pearl)

    William Byrd, Eric Holk, and Daniel Friedman. “miniKanren, live and un- tagged: quine generation via relational interpreters (programming pearl)”. In: (Sept. 2012).doi:10.1145/2661103.2661105

    work page doi:10.1145/2661103.2661105 2012

  6. [6]

    Byrd and Rebecca Swords.slpKanren

    William E. Byrd and Rebecca Swords.slpKanren. 2013.url:https : //github.com/webyrd/slpKanren

    work page 2013

  7. [7]

    Exact Recursive Probabilistic Programming

    David Chiang, Colin McDonald, and Chung-chieh Shan. “Exact Recursive Probabilistic Programming”. In:Proc. ACM Program. Lang.7.OOPSLA1 (Apr. 2023).doi:10.1145/3586050.url:https://doi.org/10.1145/ 3586050

    work page doi:10.1145/3586050.url:https://doi.org/10.1145/ 2023

  8. [8]

    Efficient Variational Inference in miniKanren with Weighted Model Counting

    Evan Donahue. “Efficient Variational Inference in miniKanren with Weighted Model Counting”. In:miniKanren and Relational Programming Work- shop. 2022.url:https://www.evandonahue.com/pdf/donahue_emkanren2022. pdf

    work page 2022

  9. [9]

    Goals as Constraints: Writing miniKanren Constraints in miniKanren

    Evan Donahue. “Goals as Constraints: Writing miniKanren Constraints in miniKanren”. In:Proceedings of the 2023 miniKanren and Relational Programming Workshop. Ed. by Nada Amin and William E. Byrd. Cam- bridge: Harvard Technical Report, 2023, pp. 1–12. 48

    work page 2023

  10. [10]

    λProlog: An extended logic programming language

    Amy Felty et al. “λProlog: An extended logic programming language”. In:9th International Conference on Automated Deduction. Ed. by Ewing Lusk and Ross Overbeek. Berlin, Heidelberg: Springer Berlin Heidelberg, 1988, pp. 754–755.isbn: 978-3-540-39216-3

    work page 1988

  11. [11]

    Declarative Programming via Term Rewrit- ing

    Matthew Francis-Landau. “Declarative Programming via Term Rewrit- ing”. PhD thesis. Johns Hopkins University, 2024.url:https://matthewfl. com/papers/mfl-dissertation.pdf

    work page 2024

  12. [12]

    Logic programs as types for logic programs

    T. Fruhwirth et al. “Logic programs as types for logic programs”. In:

    work page

  13. [13]

    1991, pp

    Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science. 1991, pp. 300–309.doi:10.1109/LICS.1991.151654

    work page doi:10.1109/lics.1991.151654 1991

  14. [14]

    Compressed and Parallelized Structured Tensor Algebra

    Mahdi Ghorbani et al. “Compressed and Parallelized Structured Tensor Algebra”. In:Proc. ACM Program. Lang.9.OOPSLA1 (Apr. 2025).doi: 10.1145/3720506.url:https://doi.org/10.1145/3720506

    work page doi:10.1145/3720506.url:https://doi.org/10.1145/3720506 2025

  15. [15]

    Provenance semirings

    Todd J. Green, Grigoris Karvounarakis, and Val Tannen. “Provenance semirings”. In:Proceedings of the Twenty-Sixth ACM SIGMOD-SIGACT- SIGART Symposium on Principles of Database Systems. PODS ’07. Bei- jing, China: Association for Computing Machinery, 2007, 31–40.isbn: 9781595936851.doi:10.1145/1265530.1265535.url:https://doi. org/10.1145/1265530.1265535

    work page doi:10.1145/1265530.1265535.url:https://doi 2007

  16. [16]

    Proceedings of the Twenty-Eighth Annual

    Lov K. Grover. “A fast quantum mechanical algorithm for database search”. In:Proceedings of the Twenty-Eighth Annual ACM Symposium on The- ory of Computing. STOC ’96. Philadelphia, Pennsylvania, USA: Associ- ation for Computing Machinery, 1996, 212–219.isbn: 0897917855.doi: 10.1145/237814.237866.url:https://doi.org/10.1145/237814. 237866

    work page doi:10.1145/237814.237866.url:https://doi.org/10.1145/237814 1996

  17. [17]

    stableKanren: Integrating Stable Model Semantics with miniKanren

    Xiangyu Guo, James Smith, and Ajay Bansal. “stableKanren: Integrating Stable Model Semantics with miniKanren”. In:Proceedings of the 25th International Symposium on Principles and Practice of Declarative Pro- gramming. PPDP ’23. Lisboa, Portugal: Association for Computing Ma- chinery, 2023.isbn: 9798400708121.doi:10 . 1145 / 3610612 . 3610617. url:https:/...

    work page doi:10.1145/3610612.3610617 2023

  18. [18]

    Nearly Macro-free microKan- ren

    Jason Hemann and Daniel P. Friedman. “Nearly Macro-free microKan- ren”. In:Trends in Functional Programming. Ed. by Stephen Chang. Cham: Springer Nature Switzerland, 2023, pp. 72–91.isbn: 978-3-031- 38938-2

    work page 2023

  19. [19]

    Typed Embedding of a Relational Language in OCaml

    Dmitrii Kosarev and Dmitry Boulytchev. “Typed Embedding of a Rela- tional Language in OCaml”. In: (2018).doi:10 . 48550 / ARXIV . 1805 . 11006.url:https://arxiv.org/abs/1805.11006

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  20. [20]

    2024.doi:10

    Nikolai Kudasov and Artem Starikov.typedKanren: Statically Typed Rela- tional Programming with Exhaustive Matching in Haskell. 2024.doi:10. 48550/ARXIV.2408.03170.url:https://arxiv.org/abs/2408.03170. 49

    work page arXiv 2024

  21. [21]

    Fixpoints for the masses: program- ming with first-class Datalog constraints

    Magnus Madsen and Ondˇ rej Lhot´ ak. “Fixpoints for the masses: program- ming with first-class Datalog constraints”. In:Proc. ACM Program. Lang. 4.OOPSLA (Nov. 2020).doi:10 . 1145 / 3428193.url:https : / / doi . org/10.1145/3428193

    work page doi:10.1145/3428193 2020

  22. [22]

    Inductive logic programming for natural language processing

    Raymond J. Mooney. “Inductive logic programming for natural language processing”. In:Inductive Logic Programming. Ed. by Stephen Muggleton. Berlin, Heidelberg: Springer Berlin Heidelberg, 1997, pp. 1–22.isbn: 978- 3-540-69583-7

    work page 1997

  23. [23]

    Functional Programming with Dat- alog

    Andr´ e Pacak and Sebastian Erdweg. “Functional Programming with Dat- alog”. In:36th European Conference on Object-Oriented Programming (ECOOP 2022). Ed. by Karim Ali and Jan Vitek. Vol. 222. Leibniz Inter- national Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik, 2022, 7:1–7:28.isbn: 978-3- 9597...

    work page 2022

  24. [24]

    Fabrizio Riguzzi.Foundations of probabilistic logic programming. en. River Publishers Series in Software Engineering. London, England: Taylor & Francis, Sept. 2022

    work page 2022

  25. [25]

    The execu- tion algorithm of mercury, an efficient purely declarative logic program- ming language

    Zoltan Somogyi, Fergus Henderson, and Thomas Conway. “The execu- tion algorithm of mercury, an efficient purely declarative logic program- ming language”. In:The Journal of Logic Programming29.1 (1996). High- Performance Implementations of Logic Programming Systems, pp. 17–64. issn: 0743-1066.doi:https : / / doi . org / 10 . 1016 / S0743 - 1066(96 ) 00068...

    work page 1996

  26. [26]

    Pixel Arrays: A fast and elementary method for solving nonlinear systems

    David I. Spivak et al.Pixel Arrays: A fast and elementary method for solv- ing nonlinear systems. 2017. arXiv:1609.00061 [math.NA].url:https: //arxiv.org/abs/1609.00061

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  27. [27]

    OLD resolution with tabulation

    Hisao Tamaki and Taisuke Sato. “OLD resolution with tabulation”. In: Third International Conference on Logic Programming. Ed. by Ehud Shapiro. Berlin, Heidelberg: Springer Berlin Heidelberg, 1986, pp. 84–98.isbn: 978- 3-540-39831-8

    work page 1986

  28. [28]

    Kodkod: A Relational Model Finder

    Emina Torlak and Daniel Jackson. “Kodkod: A Relational Model Finder”. In:Tools and Algorithms for the Construction and Analysis of Systems. Ed. by Orna Grumberg and Michael Huth. Berlin, Heidelberg: Springer Berlin Heidelberg, 2007, pp. 632–647.isbn: 978-3-540-71209-1

    work page 2007

  29. [29]

    The Aditi deductive database system

    Jayen Vaghanl et al. “The Aditi deductive database system”. In:The VLDB Journal3.2 (1994), pp. 245–288.doi:https : / / doi . org / 10 . 1007/BF01228882

    work page 1994

  30. [30]

    Dmitri Volkov, Yafei Yang, and Chung chieh Shan.Committing to the bit: Relational programming with semiring arrays and SAT solving. 2025. arXiv:2509.22614 [cs.PL].url:https://arxiv.org/abs/2509.22614. 50

    work page arXiv 2025

  31. [31]

    Various techniques used in connection with random digits

    John Von Neumann et al. “Various techniques used in connection with random digits”. In:John von Neumann, Collected Works5.768-770 (1963), p. 1

    work page 1963

  32. [32]

    Higher-order Logic Programming withλKanren

    MA Weixi, Kuang-Chen Lu, and Daniel P. Friedman. “Higher-order Logic Programming withλKanren”. In: 2020.url:https://minikanren.org/ workshop/2020/minikanren-2020-paper4.pdf

    work page 2020

  33. [33]

    probKanren: A Simple Probabilistic Extension for microKanren

    Robert Zinkov and William E Byrd. “probKanren: A Simple Probabilistic Extension for microKanren.” In:ICLP Workshops. 2021.url:https : //ceur-ws.org/Vol-2970/plppaper4.pdf. 51

    work page 2021