A Shallow Embedding of Datalog in Lean
TLDR
A new DSL embeds Datalog into Lean, simplifying definitions and queries while ensuring bidirectional interoperability and automated theorem proving.
Key contributions
- Presents a shallow embedding of Datalog as a Domain Specific Language (DSL) within Lean.
- Ensures bidirectional interoperability between the new Datalog DSL and the Lean proof assistant.
- Automates translation of Datalog backward chaining queries into Lean theorems with tactic proofs.
Why it matters
This work matters by integrating Datalog's simplicity and established deduction with Lean's expressive proof assistance. It enables more succinct and understandable definitions and queries within Lean, bridging lightweight logic programming with powerful formal verification.
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.
📬 Weekly AI Paper Digest
Get the top 10 AI/ML arXiv papers from the week — summarized, scored, and delivered to your inbox every Monday.