A Shallow Embedding of Datalog in Lean

TL;DR

This paper presents a shallow embedding of Datalog as a DSL within Lean, enabling succinct logic programming and automatic theorem generation for queries.

Contribution

It introduces a novel Datalog embedding in Lean with bidirectional interoperability and tactic-based proof automation.

Findings

Successfully embedded Datalog in Lean as a DSL

Enabled automatic translation of queries into theorems with proofs

Demonstrated the approach with three example applications

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.