arxiv: 2605.02113 · v1 · submitted 2026-05-04 · 💻 cs.SE · cs.PL

Recognition: 2 theorem links

· Lean Theorem

A Shallow Embedding of Datalog in Lean

Ramy Shahin

Authors on Pith no claims yet

Pith reviewed 2026-05-08 18:58 UTC · model grok-4.3

classification 💻 cs.SE cs.PL

keywords DatalogLeanshallow embeddingDSLbackward chaininglogic programmingtheorem proving

0 comments

The pith

A shallow embedding lets Datalog rules and queries run inside Lean as theorems with automatic proofs.

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

The paper designs and implements Datalog as a shallow DSL in Lean to allow more succinct and understandable logic programs than in Lean alone. The design prioritizes bidirectional interoperability so Datalog code can interact with Lean code. Backward chaining queries are converted automatically into Lean theorems that come with tactic-based proofs. This is demonstrated with three simple examples showing practical use.

Core claim

The shallow embedding of Datalog in Lean supports rules and facts in the Datalog style while translating backward chaining queries into theorems with tactic proofs, preserving the ability to interoperate with full Lean.

What carries the argument

The shallow Datalog DSL with automatic query-to-theorem translation and tactic proofs.

If this is right

Datalog programs can be mixed with Lean code for hybrid reasoning.
Queries gain access to Lean's proof capabilities without extra work.
The approach keeps Datalog's efficiency for deduction while using Lean's environment.
Examples confirm it works for basic cases like rule-based inference.

Where Pith is reading between the lines

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

Such an embedding might allow verifying Datalog programs formally within Lean.
It could connect to larger formalizations of databases or AI reasoning systems.
Further work could test scalability with larger rule sets or integrate with Lean's existing libraries for math and verification.

Load-bearing premise

The embedding preserves Datalog semantics exactly and the query translations are sound and complete for the supported features.

What would settle it

Finding a Datalog program and query where the generated Lean theorem is false according to standard Datalog semantics or cannot be proved by the tactics.

Figures

Figures reproduced from arXiv: 2605.02113 by Ramy Shahin.

**Figure 1.** Figure 1: Graph reachability example in the Soufflé Datalog syntax. (in the syntax of the Soufflé Datalog engine [14]) encodes a directed graph in terms of its node labels as strings, and edges between nodes. The example starts with the declaration of two relations: edge and path (lines 1-2). The edge relation has two fields: from, the source of a directed edge in the graph, and to, the target node of the edge. In t… view at source ↗

**Figure 2.** Figure 2: Graph reachability example in Lean. Curry-Howard correspondence, theorems in Lean are types, and their proofs are terms of those types view at source ↗

**Figure 3.** Figure 3: Grammar of the Lean DSL. and the body are separated by ’:-’, and rule definition ends with ’.’. A list of identifiers (<identList>) is a comma-separated sequence of Lean identifiers. A DSL statement (<Statement>) is a fact, query, rule, or a use statement. Facts, queries, and rules can also be prefixed with a label (a Lean identifier followed by ’:’). A use statement specifies a list of Lean identifiers, e… view at source ↗

**Figure 4.** Figure 4: Reachability example. In lines 6-7, rules r1 and r2 recursively define a path within a graph. There is a path between x and y if there is an edge between x and y (rule r1), or if there is a path between x and z, and an edge between z and y (rule r2). In lines 8-10, three facts (f1, f2, and f3) are defined, one fact for each edge in the graph. The first query in line 12 (q0) checks whether there is a path b… view at source ↗

**Figure 6.** Figure 6: The rectangle objects are created using the Rect.mk constructor, which is automatically created by Lean for the Rect structure. In this example, rect1 overlaps with both rect2 and rect3, while rect2 and rect3 do not overlap with each other. The most straightforward way to check if two rectangles overlap is to enumerate the cases where they do not overlap, and negate the disjunction of those cases. Given t… view at source ↗

**Figure 5.** Figure 5: Overlapping rectangles example. 4.2 Overlapping Rectangles Given two rectangles in a 2-dimensional integer coordinate space (with the top-left corner at coordinate (0,0)), this example checks whether the two rectangles overlap ( view at source ↗

**Figure 7.** Figure 7: Function differentiation example. that given x ∈ F, the derivative of f at x is f’. For example, the Mathlib theorem hasDerivAt_sin is of type hasDerivAt_sin (x : R) : HasDerivAt sin (cos x) x stating that for all real values x, the derivative of sin x is cos x view at source ↗

read the original abstract

Datalog is a lightweight logic programming language, based on the logic of Horn clauses. Lean, on the other hand, is a proof assistant system and language based on the Calculus of Inductive Constructions (CIC). Datalog is more constrained and less expressive than Lean but has a long history of established deduction algorithms. Writing definitions and queries in the Datalog fragment of Lean would be more succinct and understandable than writing them in Lean itself. This paper outlines the design and implementation of a shallow embedding of Datalog as a Domain Specific Language (DSL) on top of Lean. Bidirectional interoperability between the Datalog DSL and Lean is a primary goal of this design. In addition to rules and facts, backward chaining queries are automatically translated into theorems with tactic-based proofs. The paper also includes three simple examples of how the DSL can be used.

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.

Desk Editor's Note private letter to a colleague

A concrete shallow Datalog DSL in Lean with auto-generated theorems, but the tactic soundness is asserted rather than shown.

read the letter

The paper delivers a working shallow embedding of Datalog as a Lean DSL, with rules and facts written directly in a compact syntax and backward-chaining queries turned into Lean theorems via custom tactics. Bidirectional interoperability is the main design goal, so you can move between the Datalog fragment and full Lean proofs without leaving the same file. Three small examples illustrate the idea and show that the syntax stays close to standard Datalog while still type-checking in CIC. That combination of shallow embedding plus automatic theorem generation for this particular logic fragment is the piece that is new relative to earlier embeddings of other logics in Lean or Coq. The implementation itself looks practical for anyone who already lives in Lean and occasionally wants succinct rule-based definitions instead of writing out inductive predicates by hand. The code and examples are the real contribution here. The main gap is verification. The central claim is that the generated proofs are sound and complete for the supported Datalog fragment, yet the text gives no semantic-preservation argument, no machine-checked meta-proof, and only the three toy examples. Without that, it is hard to know whether the tactics faithfully implement the least fixed-point semantics or whether they silently over- or under-approximate derivability on larger programs. Citation coverage of prior Lean DSL work and Datalog solvers is adequate but not deep. This is useful reading for Lean developers who build or use domain-specific reasoning tools inside the prover. A referee could give concrete feedback on the tactic implementation and on how much extra verification would be needed to make the interoperability claim solid. I would send it to review.

Referee Report

2 major / 2 minor

Summary. The paper presents the design and implementation of a shallow embedding of Datalog as a DSL within the Lean proof assistant. The embedding supports Datalog rules and facts with a focus on bidirectional interoperability with Lean. Backward-chaining queries are automatically translated into Lean theorems that are discharged via custom tactics. The approach is demonstrated through three simple examples.

Significance. If the embedding preserves Datalog semantics and the tactic translations are sound, the work would offer a practical bridge between Datalog's efficient minimal-model deduction and Lean's CIC-based reasoning, allowing more concise logic programs inside a proof assistant while retaining access to Lean's libraries. The shallow embedding is a notable design choice that could enable direct reuse of Lean terms.

major comments (2)

[Implementation of query translation and tactic proofs] The central claim of automatic translation of backward-chaining queries into sound Lean theorems with tactic proofs is unsupported. The manuscript provides only three simple examples and supplies neither an informal semantic-preservation argument nor any machine-checked verification that the tactics correctly implement Datalog's least fixed-point semantics (immediate-consequence operator) without over- or under-approximation.
[Design of the shallow embedding] Bidirectional interoperability is listed as a primary design goal, yet no concrete mechanism or correctness argument is given for translating Lean terms or proofs back into the Datalog DSL while preserving the shallow character of the embedding.

minor comments (2)

The abstract and introduction could more explicitly state the supported fragment of Datalog (e.g., stratification, negation, or arithmetic) to clarify the scope of the automatic translation.
Figure or code listings illustrating the generated theorems and tactics would improve readability of the three examples.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for their thoughtful and constructive review. We address each major comment below, providing clarifications where possible and indicating planned revisions to strengthen the manuscript.

read point-by-point responses

Referee: [Implementation of query translation and tactic proofs] The central claim of automatic translation of backward-chaining queries into sound Lean theorems with tactic proofs is unsupported. The manuscript provides only three simple examples and supplies neither an informal semantic-preservation argument nor any machine-checked verification that the tactics correctly implement Datalog's least fixed-point semantics (immediate-consequence operator) without over- or under-approximation.

Authors: We agree that the current presentation relies on three illustrative examples without an accompanying informal argument or formal verification, which leaves the soundness claim insufficiently supported. In the revised version we will add a concise informal semantic-preservation argument that relates the backward-chaining translation to repeated applications of the immediate-consequence operator on the Herbrand base, showing that the supported fragment yields exactly the least fixed point for the given examples. We will also document the tactic implementation more explicitly to indicate why it does not over- or under-approximate within that fragment. A complete machine-checked proof of tactic soundness is not feasible within the scope of this paper and is left as future work. revision: partial
Referee: [Design of the shallow embedding] Bidirectional interoperability is listed as a primary design goal, yet no concrete mechanism or correctness argument is given for translating Lean terms or proofs back into the Datalog DSL while preserving the shallow character of the embedding.

Authors: The shallow embedding encodes Datalog rules directly as Lean propositions, which already permits Lean terms to appear inside Datalog rules. The reverse direction (Lean to Datalog) is performed by a small set of Lean macros that pattern-match on compatible expressions and emit the corresponding Datalog syntax without allocating new semantic objects. We will expand the manuscript with a concrete description of these macros, an example of converting a Lean term or proof fragment back into Datalog syntax, and a short argument that the translation preserves shallowness because it operates only on the existing Lean term structure rather than introducing an intermediate representation. revision: yes

standing simulated objections not resolved

A machine-checked verification that the custom tactics correctly realize Datalog's least fixed-point semantics without approximation.

Circularity Check

0 steps flagged

No circularity: implementation paper without derivation chain or fitted predictions

full rationale

The manuscript describes the design and implementation of a shallow Datalog DSL in Lean, with bidirectional interoperability and automatic translation of backward-chaining queries into tactic-proved theorems. It supplies three examples but advances no equations, predictions, or first-principles results whose validity could reduce to self-definition, fitted inputs, or self-citation chains. The central interoperability claim is presented as an engineering outcome verified by concrete usage rather than by any mathematical identity that collapses to its own inputs. No load-bearing steps match the enumerated circularity patterns; the work is therefore self-contained as a software artifact.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper is an implementation report; the central claim rests on the unstated assumption that the embedding preserves Datalog semantics.

axioms (1)

domain assumption Datalog semantics are preserved under the shallow embedding into Lean
Required for the DSL to be a faithful and useful representation of Datalog.

pith-pipeline@v0.9.0 · 5429 in / 1128 out tokens · 70338 ms · 2026-05-08T18:58:58.485987+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

31 extracted references · 10 canonical work pages

[1]

Michael Abbott, Thorsten Altenkirch, and Neil Ghani. 2005. Contain- ers: Constructing strictly positive types.Theoretical Computer Science 342, 1 (2005), 3 – 27. doi:10.1016/j.tcs.2005.06.002Applied Semantics: Selected Topics

work page doi:10.1016/j.tcs.2005.06.002applied 2005
[2]

Michael Arntzenius and Neel Krishnaswami. 2019. Seminaïve evalua- tion for a higher-order functional language.Proceedings of the ACM on Programming Languages4, POPL (2019), 1–28

2019
[3]

Krishnaswami

Michael Arntzenius and Neelakantan R. Krishnaswami. 2016. Datafun: A Functional Datalog. InProceedings of the 21st ACM SIGPLAN Interna- tional Conference on Functional Programming(Nara, Japan)(ICFP 2016). Association for Computing Machinery, New York, NY, USA, 214–227. doi:10.1145/2951913.2951948

work page doi:10.1145/2951913.2951948 2016
[4]

Pierre-Léo Bégay, Pierre Crégut, and Jean-François Monin. 2021. De- veloping and certifying Datalog optimizations in Coq/MathComp. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. 163–177

2021
[5]

Aaron Bembenek, Michael Greenberg, and Stephen Chong. 2020. For- mulog: Datalog for SMT-Based Static Analysis.Proc. ACM Program. Lang.4, OOPSLA, Article 141 (Nov. 2020), 31 pages. doi:10.1145/ 3428209

2020
[6]

Véronique Benzaken, Évelyne Contejean, and Stefania Dumbrava
[7]

InInternational Conference on Interactive Theorem Proving

Certifying standard and stratified Datalog inference engines in SSReflect. InInternational Conference on Interactive Theorem Proving. Springer, 171–188
[8]

2010.Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions (1st ed.)

Yves Bertot and Pierre Castran. 2010.Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions (1st ed.). Springer Publishing Company, Incorporated

2010
[9]

Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly Declarative Specification of Sophisticated Points-to Analyses. InProceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications(Orlando, Florida, USA)(OOPSLA ’09). ACM, New York, NY, USA, 243–262. doi:10.1145/1640089.1640108

work page doi:10.1145/1640089.1640108 2009
[10]

S. Ceri, G. Gottlob, and L. Tanca. 1989. What you always wanted to know about Datalog (and never dared to ask).IEEE Transactions on Knowledge and Data Engineering1, 1 (March 1989), 146–166. doi:10. 1109/69.43410

1989
[11]

Stefano Ceri, Georg Gottlob, and Letizia Tanca. 1990. Logic Program- ming and Databases: An Overview.Logic Programming and Databases (1990), 1–15

1990
[12]

Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, and Andrew M. Wells. 2024. Cedar: A New Lan- guage for Expressive, Fast, Safe, and Analyzable Authorization.Proc. ACM Program. Lang.8, OOPSLA1, A...

work page doi:10.1145/3649835 2024
[13]

Norbert Fuhr. 1995. Probabilistic datalog—a logic for powerful retrieval methods. InProceedings of the 18th annual international ACM SIGIR conference on Research and development in information retrieval. 282– 290

1995
[14]

Neville Grech and Yannis Smaragdakis. 2017. P/Taint: Unified Points- to and Taint Analysis.Proc. ACM Program. Lang.1, OOPSLA, Article 102 (Oct. 2017), 28 pages. doi:10.1145/3133926

work page doi:10.1145/3133926 2017
[15]

Herbert Jordan, Bernhard Scholz, and Pavle Subotić. 2016. Soufflé: On Synthesis of Program Analyzers. InComputer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham, 422–430

2016
[16]

Markus Kusano and Chao Wang. 2016. Flow-Sensitive Composition of Thread-Modular Abstract Interpretation. InProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering(Seattle, WA, USA)(FSE 2016). Association for Computing Machinery, New York, NY, USA, 799–809. doi:10.1145/2950290.2950291

work page doi:10.1145/2950290.2950291 2016
[17]

Markus Kusano and Chao Wang. 2017. Thread-Modular Static Analysis for Relaxed Memory Models. InProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering(Paderborn, Germany) (ESEC/FSE 2017). Association for Computing Machinery, New York, NY, USA, 337–348. doi:10.1145/3106237.3106243

work page doi:10.1145/3106237.3106243 2017
[18]

Lam, John Whaley, V

Monica S. Lam, John Whaley, V. Benjamin Livshits, Michael C. Mar- tin, Dzintars Avots, Michael Carbin, and Christopher Unkel. 2005. Context-Sensitive Program Analysis as Database Queries. InProceed- ings of the Twenty-Fourth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems(Baltimore, Maryland)(PODS ’05). Association for Computing Machi...

work page doi:10.1145/1065167.1065169 2005
[19]

Magnus Madsen, Ming-Ho Yee, and Ondřej Lhoták. 2016. From Dat- alog to Flix: A Declarative Language for Fixed Points on Lattices. In SLE ’26, July 02–03, 2026, Rennes, France Ramy Shahin Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation(Santa Barbara, CA, USA)(PLDI ’16). ACM, New York, NY, USA, 194–208. doi:1...

work page doi:10.1145/2908080.2908096 2016
[20]

The mathlib Community. 2020. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Cer- tified Programs and Proofs(New Orleans, LA, USA)(CPP 2020). As- sociation for Computing Machinery, New York, NY, USA, 367–381. doi:10.1145/3372885.3373824

work page doi:10.1145/3372885.3373824 2020
[21]

Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. InAutomated Deduction – CADE 28, André Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham, 625–635

2021
[22]

Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002.Is- abelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, Berlin, Heidelberg

2002
[23]

Frank Pfenning and Christine Paulin-Mohring. 1990. Inductively de- fined types in the Calculus of Constructions. InMathematical Founda- tions of Programming Semantics, M. Main, A. Melton, M. Mislove, and D. Schmidt (Eds.). Springer-Verlag, New York, NY, 209–228

1990
[24]

Leonid Ryzhyk and Mihai Budiu. 2019. Differential Datalog.Datalog 2 (2019), 4–5

2019
[25]

Ramy Shahin, Murad Akhundov, and Marsha Chechik. 2022. Annota- tive Software Product Line Analysis Using Variability-Aware Datalog. IEEE Transactions on Software Engineering49, 3 (2022), 1323–1341

2022
[26]

Ramy Shahin and Marsha Chechik. 2020. Variability-aware datalog. In International Symposium on Practical Aspects of Declarative Languages. Springer, 213–221

2020
[27]

Ramy Shahin, Sahar Kokaly, and Marsha Chechik. 2021. Towards certified analysis of software product line safety cases. InInternational Conference on Computer Safety, Reliability, and Security. Springer, 130– 145

2021
[28]

Ramy Shahin, Rafael Toledo, Robert Hackman, Ramesh S, Joanne M Atlee, and Marsha Chechik. 2023. Applying declarative analysis to industrial automotive software product line models.Empirical Software Engineering28, 2 (2023), 40

2023
[29]

Chungha Sung, Markus Kusano, and Chao Wang. 2017. Modular Verification of Interrupt-Driven Software. InProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering (Urbana-Champaign, IL, USA)(ASE 2017). IEEE Press, 206–216

2017
[30]

Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. 2025. Verifying datalog reasoning with Lean. In16th Inter- national Conference on Interactive Theorem Proving (ITP 2025). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 36–1

2025
[31]

Torin Viger, Logan Murphy, Alessio Di Sandro, Ramy Shahin, and Marsha Chechik. 2021. A lean approach to building valid model-based safety arguments. In2021 ACM/IEEE 24th International Conference on Model Driven Engineering Languages and Systems (MODELS). IEEE, 194–204

2021