SQL Goal Compiler

This notebook demonstrates how to translate a TypedLogic theory plus a query or goal into SQL.

The examples use an in-memory SQLite database so the generated SQL is executed end to end.

Setup

The SQL compiler is a regular TypedLogic compiler. PredicateBinding tells the compiler which SQL table and columns back an extensional predicate.

import sqlite3

from typedlogic import And, Forall, Implies, NegationAsFailure, Not, PredicateDefinition, SentenceGroup, Term, Theory, Variable
from typedlogic.compilers.sql_compiler import PredicateBinding, SQLCompiler, SQLCompilerConfig
from typedlogic.datamodel import SentenceGroupType


def fetchall(sql: str, setup: list[str] | None = None) -> list[tuple]:
    """Run SQL in a fresh in-memory SQLite database."""
    connection = sqlite3.connect(":memory:")
    try:
        for statement in setup or []:
            connection.execute(statement)
        return list(connection.execute(sql))
    finally:
        connection.close()


compiler = SQLCompiler()

Rules As Views

This theory defines Ancestor from Parent. The recursive rule is compiled as a recursive common table expression.

x = Variable("x")
y = Variable("y")
z = Variable("z")

family_theory = Theory(
    predicate_definitions=[
        PredicateDefinition("Parent", {"parent": "str", "child": "str"}),
        PredicateDefinition("Ancestor", {"ancestor": "str", "descendant": "str"}),
    ]
)
family_theory.add(Forall([x, y], Implies(Term("Parent", x, y), Term("Ancestor", x, y))))
family_theory.add(
    Forall(
        [x, y, z],
        Implies(And(Term("Ancestor", x, y), Term("Parent", y, z)), Term("Ancestor", x, z)),
    )
)

ancestor_sql = compiler.compile(
    family_theory,
    goal=Term("Ancestor", "Alice", Variable("who")),
    bindings={"Parent": PredicateBinding("parent_edges", {"parent": "src", "child": "dst"})},
)
print(ancestor_sql)

fetchall(
    ancestor_sql,
    [
        "CREATE TABLE parent_edges (src TEXT, dst TEXT)",
        "INSERT INTO parent_edges VALUES ('Alice', 'Bob'), ('Bob', 'Carol'), ('Carol', 'Dana')",
    ],
)

Inline Unit Clauses

Ground facts do not require table bindings. They become inline CTE branches.

person_theory = Theory(predicate_definitions=[PredicateDefinition("Person", {"name": "str"})])
person_theory.add(Term("Person", "Alice"))
person_theory.add(Term("Person", "Bob"))

person_sql = compiler.compile(person_theory, goal=Term("Person", Variable("name")))
print(person_sql)
fetchall(person_sql)

Goal Sentence Groups

If no explicit goal is supplied, the compiler uses goal sentence groups from the theory.

goal_theory = Theory(predicate_definitions=[PredicateDefinition("Person", {"name": "str"})])
goal_theory.add(Term("Person", "Alice"))
goal_theory.sentence_groups.append(
    SentenceGroup(name="goals", group_type=SentenceGroupType.GOAL, sentences=[Term("Person", Variable("name"))])
)

goal_sql = compiler.compile(goal_theory)
print(goal_sql)
fetchall(goal_sql.removesuffix(";"))

Negation As Failure

Negated body atoms are emitted as correlated NOT EXISTS subqueries.

eligibility_theory = Theory(
    predicate_definitions=[
        PredicateDefinition("Person", {"name": "str"}),
        PredicateDefinition("Blocked", {"name": "str"}),
        PredicateDefinition("Eligible", {"name": "str"}),
    ]
)
eligibility_theory.add(
    Forall([x], Implies(And(Term("Person", x), NegationAsFailure(Term("Blocked", x))), Term("Eligible", x)))
)

eligible_sql = compiler.compile(
    eligibility_theory,
    goal=Term("Eligible", Variable("name")),
    bindings={"Person": "people", "Blocked": "blocked"},
)
print(eligible_sql)
fetchall(
    eligible_sql,
    [
        "CREATE TABLE people (name TEXT)",
        "CREATE TABLE blocked (name TEXT)",
        "INSERT INTO people VALUES ('Alice'), ('Bob')",
        "INSERT INTO blocked VALUES ('Bob')",
    ],
)

Constraint Checks

First-order denial constraints compile to validation queries. A returned row is a violation witness.

constraint_theory = Theory(
    predicate_definitions=[
        PredicateDefinition("Cat", {"name": "str"}),
        PredicateDefinition("Dog", {"name": "str"}),
    ]
)
constraint_theory.add(Forall([x], Not(And(Term("Cat", x), Term("Dog", x)))))

[constraint_sql] = compiler.compile_constraints(
    constraint_theory,
    config=SQLCompilerConfig(bindings={"Cat": PredicateBinding("cats"), "Dog": PredicateBinding("dogs")}),
)
print(constraint_sql)
fetchall(
    constraint_sql,
    [
        "CREATE TABLE cats (name TEXT)",
        "CREATE TABLE dogs (name TEXT)",
        "INSERT INTO cats VALUES ('Jules'), ('Milo')",
        "INSERT INTO dogs VALUES ('Milo'), ('Rex')",
    ],
)