diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 946a1f898fc..b855d472eaa 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -34,6 +34,7 @@ set(SOUFFLE_SOURCES
     ast/FunctionalConstraint.cpp
     ast/IntrinsicFunctor.cpp
     ast/IterationCounter.cpp
+    ast/Lattice.cpp
     ast/Negation.cpp
     ast/NilConstant.cpp
     ast/Node.cpp
@@ -87,6 +88,7 @@ set(SOUFFLE_SOURCES
     ast/transform/GroundedTermsChecker.cpp
     ast/transform/GroundWitnesses.cpp
     ast/transform/InlineRelations.cpp
+    ast/transform/InsertLatticeOperations.cpp
     ast/transform/MagicSet.cpp
     ast/transform/MaterializeAggregationQueries.cpp
     ast/transform/MaterializeSingletonAggregation.cpp
diff --git a/src/MainDriver.cpp b/src/MainDriver.cpp
index 60c7c996f29..aa438f41b42 100644
--- a/src/MainDriver.cpp
+++ b/src/MainDriver.cpp
@@ -37,6 +37,7 @@
 #include "ast/transform/IOAttributes.h"
 #include "ast/transform/IODefaults.h"
 #include "ast/transform/InlineRelations.h"
+#include "ast/transform/InsertLatticeOperations.h"
 #include "ast/transform/MagicSet.h"
 #include "ast/transform/MaterializeAggregationQueries.h"
 #include "ast/transform/MaterializeSingletonAggregation.h"
@@ -479,6 +480,7 @@ Own<ast::transform::PipelineTransformer> astTransformationPipeline(Global& glb)
     // Main pipeline
     auto pipeline = mk<ast::transform::PipelineTransformer>(mk<ast::transform::ComponentChecker>(),
             mk<ast::transform::ComponentInstantiationTransformer>(),
+            mk<ast::transform::LatticeTransformer>(),
             mk<ast::transform::DebugDeltaRelationTransformer>(),
             mk<ast::transform::IODefaultsTransformer>(),
             mk<ast::transform::SimplifyAggregateTargetExpressionTransformer>(),
diff --git a/src/RelationTag.h b/src/RelationTag.h
index 5a850972533..c6d51ca00a3 100644
--- a/src/RelationTag.h
+++ b/src/RelationTag.h
@@ -58,7 +58,6 @@ enum class RelationRepresentation {
     BTREE,         // use btree data-structure
     BTREE_DELETE,  // use btree_delete data-structure
     EQREL,         // use union data-structure
-    PROVENANCE,    // use custom btree data-structure with provenance extras
     INFO,          // info relation for provenance
 };
 
@@ -168,7 +167,6 @@ inline std::ostream& operator<<(std::ostream& os, RelationRepresentation represe
         case RelationRepresentation::BTREE_DELETE: return os << "btree_delete";
         case RelationRepresentation::BRIE: return os << "brie";
         case RelationRepresentation::EQREL: return os << "eqrel";
-        case RelationRepresentation::PROVENANCE: return os << "provenance";
         case RelationRepresentation::INFO: return os << "info";
         case RelationRepresentation::DEFAULT: return os;
     }
diff --git a/src/ast/Attribute.cpp b/src/ast/Attribute.cpp
index a06fdab5d8e..f30afa45563 100644
--- a/src/ast/Attribute.cpp
+++ b/src/ast/Attribute.cpp
@@ -14,7 +14,10 @@
 namespace souffle::ast {
 
 Attribute::Attribute(std::string n, QualifiedName t, SrcLocation loc)
-        : Node(std::move(loc)), name(std::move(n)), typeName(std::move(t)) {}
+        : Node(std::move(loc)), name(std::move(n)), typeName(std::move(t)), isLattice(false) {}
+
+Attribute::Attribute(std::string n, QualifiedName t, bool isLattice, SrcLocation loc)
+        : Node(std::move(loc)), name(std::move(n)), typeName(std::move(t)), isLattice(isLattice) {}
 
 void Attribute::setTypeName(QualifiedName name) {
     typeName = std::move(name);
@@ -22,15 +25,18 @@ void Attribute::setTypeName(QualifiedName name) {
 
 void Attribute::print(std::ostream& os) const {
     os << name << ":" << typeName;
+    if (isLattice) {
+        os << "<>";
+    }
 }
 
 bool Attribute::equal(const Node& node) const {
     const auto& other = asAssert<Attribute>(node);
-    return name == other.name && typeName == other.typeName;
+    return name == other.name && typeName == other.typeName && isLattice == other.isLattice;
 }
 
 Attribute* Attribute::cloning() const {
-    return new Attribute(name, typeName, getSrcLoc());
+    return new Attribute(name, typeName, isLattice, getSrcLoc());
 }
 
 }  // namespace souffle::ast
diff --git a/src/ast/Attribute.h b/src/ast/Attribute.h
index ecea916c63f..9466af4805c 100644
--- a/src/ast/Attribute.h
+++ b/src/ast/Attribute.h
@@ -35,6 +35,7 @@ namespace souffle::ast {
 class Attribute : public Node {
 public:
     Attribute(std::string n, QualifiedName t, SrcLocation loc = {});
+    Attribute(std::string n, QualifiedName t, bool isLattice, SrcLocation loc = {});
 
     /** Return attribute name */
     const std::string& getName() const {
@@ -49,6 +50,10 @@ class Attribute : public Node {
     /** Set type name */
     void setTypeName(QualifiedName name);
 
+    bool getIsLattice() const {
+        return isLattice;
+    }
+
 protected:
     void print(std::ostream& os) const override;
 
@@ -63,6 +68,9 @@ class Attribute : public Node {
 
     /** Type name */
     QualifiedName typeName;
+
+    /** Is lattice element */
+    bool isLattice;
 };
 
 }  // namespace souffle::ast
diff --git a/src/ast/Component.cpp b/src/ast/Component.cpp
index 97129a06f36..f5356fdcff9 100644
--- a/src/ast/Component.cpp
+++ b/src/ast/Component.cpp
@@ -39,6 +39,15 @@ std::vector<Type*> Component::getTypes() const {
     return toPtrVector(types);
 }
 
+void Component::addLattice(Own<Lattice> t) {
+    assert(t != nullptr);
+    lattices.push_back(std::move(t));
+}
+
+std::vector<Lattice*> Component::getLattices() const {
+    return toPtrVector(lattices);
+}
+
 void Component::copyBaseComponents(const Component& other) {
     baseComponents = clone(other.baseComponents);
 }
diff --git a/src/ast/Component.h b/src/ast/Component.h
index 99befb86e92..a6debc78e24 100644
--- a/src/ast/Component.h
+++ b/src/ast/Component.h
@@ -20,6 +20,7 @@
 #include "ast/ComponentInit.h"
 #include "ast/ComponentType.h"
 #include "ast/Directive.h"
+#include "ast/Lattice.h"
 #include "ast/Node.h"
 #include "ast/Relation.h"
 #include "ast/Type.h"
@@ -64,6 +65,11 @@ class Component : public Node {
     /** Get types */
     std::vector<Type*> getTypes() const;
 
+    /** Add lattice */
+    void addLattice(Own<Lattice> lat);
+
+    std::vector<Lattice*> getLattices() const;
+
     /** Copy base components */
     void copyBaseComponents(const Component& other);
 
@@ -129,6 +135,9 @@ class Component : public Node {
     /** Types declarations */
     VecOwn<Type> types;
 
+    /** Types declarations */
+    VecOwn<Lattice> lattices;
+
     /** Relations */
     VecOwn<Relation> relations;
 
diff --git a/src/ast/Lattice.cpp b/src/ast/Lattice.cpp
new file mode 100644
index 00000000000..75c83b59ef6
--- /dev/null
+++ b/src/ast/Lattice.cpp
@@ -0,0 +1,107 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023, The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+#include "ast/Lattice.h"
+#include "souffle/utility/MiscUtil.h"
+#include "souffle/utility/StreamUtil.h"
+
+#include <utility>
+
+namespace souffle::ast {
+
+std::optional<LatticeOperator> latticeOperatorFromString(const std::string& str) {
+    if (str == "Bottom") return Bottom;
+    if (str == "Top") return Top;
+    if (str == "Lub") return Lub;
+    if (str == "Glb") return Glb;
+    if (str == "Leq") return Leq;
+    return std::nullopt;
+}
+
+std::string latticeOperatorToString(const LatticeOperator op) {
+    switch (op) {
+        case Bottom: return "Bottom";
+        case Top: return "Top";
+        case Lub: return "Lub";
+        case Glb: return "Glb";
+        case Leq: return "Leq";
+        default: assert(false && "unknown lattice operator");
+    }
+    return "";
+}
+
+Lattice::Lattice(QualifiedName name, std::map<LatticeOperator, Own<ast::Argument>> ops, SrcLocation loc)
+        : Node(std::move(loc)), name(std::move(name)), operators(std::move(ops)) {}
+
+void Lattice::setQualifiedName(QualifiedName name) {
+    this->name = std::move(name);
+}
+
+const std::map<LatticeOperator, const ast::Argument*> Lattice::getOperators() const {
+    std::map<LatticeOperator, const ast::Argument*> ops;
+    for (const auto& [op, arg] : operators) {
+        ops.emplace(std::make_pair(op, arg.get()));
+    }
+    return ops;
+}
+
+bool Lattice::hasGlb() const {
+    return operators.count(Glb) > 0;
+}
+
+bool Lattice::hasLub() const {
+    return operators.count(Lub) > 0;
+}
+
+bool Lattice::hasBottom() const {
+    return operators.count(Bottom) > 0;
+}
+
+bool Lattice::hasTop() const {
+    return operators.count(Top) > 0;
+}
+
+const ast::Argument* Lattice::getLub() const {
+    return operators.at(Lub).get();
+}
+
+const ast::Argument* Lattice::getGlb() const {
+    return operators.at(Glb).get();
+}
+
+const ast::Argument* Lattice::getBottom() const {
+    return operators.at(Bottom).get();
+}
+
+const ast::Argument* Lattice::getTop() const {
+    return operators.at(Top).get();
+}
+
+void Lattice::print(std::ostream& os) const {
+    os << ".lattice " << getQualifiedName() << " {\n   ";
+    bool first = true;
+    for (const auto& [op, arg] : operators) {
+        if (!first) {
+            os << ",\n   ";
+        }
+        os << latticeOperatorToString(op) << " -> " << *arg;
+        first = false;
+    }
+    os << "\n}";
+}
+
+bool Lattice::equal(const Node& node) const {
+    const auto& other = asAssert<Lattice>(node);
+    return getQualifiedName() == other.getQualifiedName() && equal_targets(operators, other.operators);
+}
+
+Lattice* Lattice::cloning() const {
+    return new Lattice(getQualifiedName(), clone(operators), getSrcLoc());
+}
+
+}  // namespace souffle::ast
diff --git a/src/ast/Lattice.h b/src/ast/Lattice.h
new file mode 100644
index 00000000000..71dcb1e970f
--- /dev/null
+++ b/src/ast/Lattice.h
@@ -0,0 +1,77 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023, The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file Lattice.h
+ *
+ * Defines the Lattice class
+ *
+ ***********************************************************************/
+
+#pragma once
+
+#include "ast/Argument.h"
+#include "ast/Node.h"
+#include "ast/QualifiedName.h"
+#include "parser/SrcLocation.h"
+
+#include <map>
+#include <optional>
+
+namespace souffle::ast {
+
+enum LatticeOperator { Bottom = 0, Top, Lub, Glb, Leq };
+
+std::optional<LatticeOperator> latticeOperatorFromString(const std::string& str);
+
+/**
+ *  @class Lattice
+ *  @brief An class to define Lattice attributes for a type
+ */
+class Lattice : public Node {
+public:
+    Lattice(QualifiedName name, std::map<LatticeOperator, Own<ast::Argument>> operators,
+            SrcLocation loc = {});
+
+    /** Return type name */
+    const QualifiedName& getQualifiedName() const {
+        return name;
+    }
+
+    /** Set type name */
+    void setQualifiedName(QualifiedName name);
+
+    const std::map<LatticeOperator, const ast::Argument*> getOperators() const;
+
+    bool hasGlb() const;
+    bool hasLub() const;
+    bool hasBottom() const;
+    bool hasTop() const;
+
+    const ast::Argument* getLub() const;
+    const ast::Argument* getGlb() const;
+    const ast::Argument* getBottom() const;
+    const ast::Argument* getTop() const;
+
+protected:
+    void print(std::ostream& os) const override;
+
+private:
+    bool equal(const Node& node) const override;
+
+    Lattice* cloning() const override;
+
+private:
+    /** type name */
+    QualifiedName name;
+
+    const std::map<LatticeOperator, Own<ast::Argument>> operators;
+};
+
+}  // namespace souffle::ast
diff --git a/src/ast/Program.cpp b/src/ast/Program.cpp
index d67db8fe53f..623c5d2ad90 100644
--- a/src/ast/Program.cpp
+++ b/src/ast/Program.cpp
@@ -118,6 +118,10 @@ std::vector<Type*> Program::getTypes() const {
     return toPtrVector(types);
 }
 
+std::vector<Lattice*> Program::getLattices() const {
+    return toPtrVector(lattices);
+}
+
 std::vector<Relation*> Program::getRelations() const {
     return toPtrVector(relations, &RelationInfo::decls);
 }
@@ -231,6 +235,15 @@ void Program::addType(Own<Type> type) {
     types.push_back(std::move(type));
 }
 
+void Program::addLattice(Own<Lattice> lattice) {
+    assert(lattice != nullptr);
+    [[maybe_unused]] auto* existingLattice = getIf(getLattices(), [&](const Lattice* current) {
+        return current->getQualifiedName() == lattice->getQualifiedName();
+    });
+    assert(existingLattice == nullptr && "Redefinition of lattice!");
+    lattices.push_back(std::move(lattice));
+}
+
 void Program::addPragma(Own<Pragma> pragma) {
     assert(pragma && "NULL pragma");
     pragmas.push_back(std::move(pragma));
@@ -259,6 +272,7 @@ void Program::apply(const NodeMapper& map) {
     mapAll(instantiations, map);
     mapAll(functors, map);
     mapAll(types, map);
+    mapAll(lattices, map);
     mapAll(relations, &RelationInfo::decls, map);
     mapAll(relations, &RelationInfo::clauses, map);
     mapAll(relations, &RelationInfo::directives, map);
@@ -271,6 +285,7 @@ Node::NodeVec Program::getChildren() const {
     append(res, makePtrRange(instantiations));
     append(res, makePtrRange(functors));
     append(res, makePtrRange(types));
+    append(res, makePtrRange(lattices));
     append(res, relations, &RelationInfo::decls);
     append(res, relations, &RelationInfo::clauses);
     append(res, relations, &RelationInfo::directives);
@@ -286,6 +301,7 @@ void Program::print(std::ostream& os) const {
     show(components);
     show(instantiations);
     show(types);
+    show(lattices);
     show(functors);
     show(getRelations());
     show(getClauses(), "\n\n");
@@ -300,6 +316,7 @@ bool Program::equal(const Node& node) const {
            equal_targets(instantiations, other.instantiations) &&
            equal_targets(functors, other.functors) &&
            equal_targets(types, other.types) &&
+           equal_targets(lattices, other.lattices) &&
            equal_targets_map(relations, other.relations, [](auto& a, auto& b) {
                 return  equal_targets(a.decls     , b.decls     ) &&
                         equal_targets(a.clauses   , b.clauses   ) &&
@@ -324,6 +341,7 @@ Program* Program::cloning() const {
     res->components = clone(components);
     res->instantiations = clone(instantiations);
     res->types = clone(types);
+    res->lattices = clone(lattices);
     res->functors = clone(functors);
     res->relations = clone(relations);
     return res;
diff --git a/src/ast/Program.h b/src/ast/Program.h
index c3475ef458d..b6544e9b978 100644
--- a/src/ast/Program.h
+++ b/src/ast/Program.h
@@ -109,6 +109,9 @@ class Program : public Node {
     /** Return types */
     std::vector<Type*> getTypes() const;
 
+    /** Return lattices */
+    std::vector<Lattice*> getLattices() const;
+
     /** Return relations */
     std::vector<Relation*> getRelations() const;
 
@@ -183,6 +186,9 @@ class Program : public Node {
     /** Add a type declaration */
     void addType(Own<Type> type);
 
+    /** Add a lattice declaration */
+    void addLattice(Own<Lattice> lattice);
+
     /**
      * Remove a clause by identity. The clause must be owned by the program.
      * It is not expected that there are useful cases where some are not owned, and it is often
@@ -240,6 +246,9 @@ class Program : public Node {
     /** Program types  */
     VecOwn<Type> types;
 
+    /** Program lattices */
+    VecOwn<Lattice> lattices;
+
     /** Program relation declartions, clauses, and directives */
     RelationInfoMap relations;
 
diff --git a/src/ast/Relation.h b/src/ast/Relation.h
index 4fb1aade201..64b8f774bed 100644
--- a/src/ast/Relation.h
+++ b/src/ast/Relation.h
@@ -54,6 +54,15 @@ class Relation : public Node {
         return attributes.size();
     }
 
+    /** Return the arity of this relation */
+    std::size_t getAuxiliaryArity() const {
+        std::size_t arity = 0;
+        for (const auto& a : attributes) {
+            arity += a->getIsLattice() ? 1 : 0;
+        }
+        return arity;
+    }
+
     /** Set relation attributes */
     void setAttributes(VecOwn<Attribute> attrs);
 
diff --git a/src/ast/analysis/Ground.cpp b/src/ast/analysis/Ground.cpp
index 52d7c94778e..bfb7ba184e7 100644
--- a/src/ast/analysis/Ground.cpp
+++ b/src/ast/analysis/Ground.cpp
@@ -154,8 +154,24 @@ BoolDisjunctConstraint imply(const std::vector<BoolDisjunctVar>& vars, const Boo
 struct GroundednessAnalysis : public ConstraintAnalysis<BoolDisjunctVar> {
     Program& program;
     std::set<const Atom*> ignore;
-
-    GroundednessAnalysis(const TranslationUnit& tu) : program(tu.getProgram()) {}
+    std::map<const QualifiedName, std::set<std::size_t>> latticeAttributes;
+    bool isLatticeTransformerPass;
+
+    GroundednessAnalysis(const TranslationUnit& tu, bool isLatticeTransformerPass)
+            : program(tu.getProgram()), isLatticeTransformerPass(isLatticeTransformerPass) {
+        if (isLatticeTransformerPass) {
+            for (const Relation* rel : program.getRelations()) {
+                const auto attributes = rel->getAttributes();
+                const auto& name = rel->getQualifiedName();
+                for (std::size_t i = 0; i < attributes.size(); i++) {
+                    if (attributes[i]->getIsLattice()) {
+                        const auto type = attributes[i]->getTypeName();
+                        latticeAttributes[name].insert(i);
+                    }
+                }
+            }
+        }
+    }
 
     // atoms are producing grounded variables
     void visit_(type_identity<Atom>, const Atom& cur) override {
@@ -164,9 +180,14 @@ struct GroundednessAnalysis : public ConstraintAnalysis<BoolDisjunctVar> {
             return;
         }
 
-        // all arguments are grounded
-        for (const auto& arg : cur.getArguments()) {
-            addConstraint(isTrue(getVar(arg)));
+        // all arguments are grounded except lattice arguments
+        const auto& name = cur.getQualifiedName();
+        const auto& args = cur.getArguments();
+        for (std::size_t i = 0; i < cur.getArity(); i++) {
+            if (!isLatticeTransformerPass || !latticeAttributes.count(name) ||
+                    !latticeAttributes[name].count(i)) {
+                addConstraint(isTrue(getVar(args[i])));
+            }
         }
     }
 
@@ -265,9 +286,10 @@ struct GroundednessAnalysis : public ConstraintAnalysis<BoolDisjunctVar> {
 /***
  * computes for variables in the clause whether they are grounded
  */
-std::map<const Argument*, bool> getGroundedTerms(const TranslationUnit& tu, const Clause& clause) {
+std::map<const Argument*, bool> getGroundedTerms(
+        const TranslationUnit& tu, const Clause& clause, bool isLatticeTransformerPass) {
     // run analysis on given clause
-    return GroundednessAnalysis(tu).analyse(clause);
+    return GroundednessAnalysis(tu, isLatticeTransformerPass).analyse(clause);
 }
 
 }  // namespace souffle::ast::analysis
diff --git a/src/ast/analysis/Ground.h b/src/ast/analysis/Ground.h
index f6ca7333d8d..8ac8689e35d 100644
--- a/src/ast/analysis/Ground.h
+++ b/src/ast/analysis/Ground.h
@@ -32,6 +32,7 @@ namespace souffle::ast::analysis {
  * @return a map mapping each contained argument to a boolean indicating
  *      whether the argument represents a grounded value or not
  */
-std::map<const Argument*, bool> getGroundedTerms(const TranslationUnit& tu, const Clause& clause);
+std::map<const Argument*, bool> getGroundedTerms(
+        const TranslationUnit& tu, const Clause& clause, bool isLatticeTransformerPass = false);
 
 }  // namespace souffle::ast::analysis
diff --git a/src/ast/transform/ComponentInstantiation.cpp b/src/ast/transform/ComponentInstantiation.cpp
index bf1e46b629c..69567ae0b29 100644
--- a/src/ast/transform/ComponentInstantiation.cpp
+++ b/src/ast/transform/ComponentInstantiation.cpp
@@ -23,6 +23,7 @@
 #include "ast/ComponentInit.h"
 #include "ast/ComponentType.h"
 #include "ast/Directive.h"
+#include "ast/Lattice.h"
 #include "ast/Node.h"
 #include "ast/Program.h"
 #include "ast/QualifiedName.h"
@@ -58,6 +59,7 @@ static const unsigned int MAX_INSTANTIATION_DEPTH = 100;
  */
 struct ComponentContent {
     VecOwn<ast::Type> types;
+    VecOwn<ast::Lattice> lattices;
     VecOwn<Relation> relations;
     VecOwn<Directive> directives;
     VecOwn<Clause> clauses;
@@ -77,6 +79,22 @@ struct ComponentContent {
         types.push_back(std::move(type));
     }
 
+    void add(Own<ast::Lattice>& lattice, ErrorReport& report) {
+        // add to result content (check existence first)
+        auto foundItem =
+                std::find_if(lattices.begin(), lattices.end(), [&](const Own<ast::Lattice>& element) {
+                    return (element->getQualifiedName() == lattice->getQualifiedName());
+                });
+        if (foundItem != lattices.end()) {
+            Diagnostic err(Diagnostic::Type::ERROR,
+                    DiagnosticMessage("Redefinition of lattice " + toString(lattice->getQualifiedName()),
+                            lattice->getSrcLoc()),
+                    {DiagnosticMessage("Previous definition", (*foundItem)->getSrcLoc())});
+            report.addDiagnostic(err);
+        }
+        lattices.push_back(std::move(lattice));
+    }
+
     void add(Own<Relation>& rel, ErrorReport& report) {
         // add to result content (check existence first)
         auto foundItem = std::find_if(relations.begin(), relations.end(), [&](const Own<Relation>& element) {
@@ -164,6 +182,11 @@ void collectContent(Program& program, const Component& component, const TypeBind
                     res.add(type, report);
                 }
 
+                // process lattices
+                for (auto& lattice : content.lattices) {
+                    res.add(lattice, report);
+                }
+
                 // process relations
                 for (auto& rel : content.relations) {
                     res.add(rel, report);
@@ -256,6 +279,17 @@ void collectContent(Program& program, const Component& component, const TypeBind
         res.add(type, report);
     }
 
+    for (const auto& cur : component.getLattices()) {
+        // create a clone
+        Own<ast::Lattice> lattice(clone(cur));
+
+        auto&& newName = binding.find(lattice->getQualifiedName());
+        if (!newName.empty()) {
+            lattice->setQualifiedName(newName);
+        }
+        res.add(lattice, report);
+    }
+
     // and the local relations
     // (replacing formal parameters with actual parameters)
     for (const auto& cur : component.getRelations()) {
@@ -355,6 +389,11 @@ ComponentContent getInstantiatedContent(Program& program, const ComponentInit& c
             res.add(type, report);
         }
 
+        // add types
+        for (auto& lattice : nestedContent.lattices) {
+            res.add(lattice, report);
+        }
+
         // add relations
         for (auto& rel : nestedContent.relations) {
             res.add(rel, report);
@@ -389,6 +428,11 @@ ComponentContent getInstantiatedContent(Program& program, const ComponentInit& c
         });
     }
 
+    for (const auto& cur : res.lattices) {
+        auto newName = componentInit.getInstanceName() + cur->getQualifiedName();
+        cur->setQualifiedName(newName);
+    }
+
     // update relation names
     std::map<QualifiedName, QualifiedName> relationNameMapping;
     for (const auto& cur : res.relations) {
@@ -552,6 +596,9 @@ bool ComponentInstantiationTransformer::transform(TranslationUnit& translationUn
         for (auto& type : content.types) {
             program.addType(std::move(type));
         }
+        for (auto& lattice : content.lattices) {
+            program.addLattice(std::move(lattice));
+        }
         for (auto& rel : content.relations) {
             program.addRelation(std::move(rel));
         }
diff --git a/src/ast/transform/InsertLatticeOperations.cpp b/src/ast/transform/InsertLatticeOperations.cpp
new file mode 100644
index 00000000000..e9e4e405bdf
--- /dev/null
+++ b/src/ast/transform/InsertLatticeOperations.cpp
@@ -0,0 +1,347 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023 The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file InsertLatticeOperations.cpp
+ *
+ * Implements AST transformation related to the support of lattices
+ *
+ ***********************************************************************/
+
+#include "ast/transform/InsertLatticeOperations.h"
+#include "ast/Atom.h"
+#include "ast/BinaryConstraint.h"
+#include "ast/Clause.h"
+#include "ast/Constraint.h"
+#include "ast/Negation.h"
+#include "ast/QualifiedName.h"
+#include "ast/UnnamedVariable.h"
+#include "ast/UserDefinedFunctor.h"
+#include "ast/Variable.h"
+#include "ast/analysis/Ground.h"
+#include "ast/utility/Visitor.h"
+#include <utility>
+
+namespace souffle::ast::transform {
+
+/*
+ * If a non-negated body atom has a lattice argument that is grounded by other atoms and constraints,
+ * e.g. `R(a, b, $B(x))`, then:
+ * - Given that `$B(x)` is a lattice argument:
+ *    `R(a, b, $B(x))` holds <=> the current value `lat` in `R(a, b, lat)` is greater or equal to `$B(x)` in
+ * the lattice Consequently, we must translate the atom `R(a, ,b $B(x))` into `R(a, b, lat), GLB(lat, $B(x)) =
+ * $B(x)` or `R(a, b, lat), LEQ($B(x), lat) != 0`.
+ */
+struct ReplaceGroundedLatticeArguments : public NodeMapper {
+    ReplaceGroundedLatticeArguments(std::map<const ast::Argument*, const ast::Lattice*>& toReplace,
+            VecOwn<ast::Literal>& newConstraints)
+            : toReplace(toReplace), newConstraints(newConstraints){};
+
+    Own<Node> operator()(Own<Node> node) const override {
+        if (auto arg = as<ast::Argument>(node)) {
+            if (toReplace.count(arg) > 0) {
+                Point p = arg->getSrcLoc().start;
+                std::string lat = "<lattice" + std::to_string(p.line) + "_" + std::to_string(p.column) + ">";
+                // add Glb constraint
+                assert(toReplace.count(arg) > 0);
+                const ast::Lattice* lattice = toReplace.at(arg);
+                assert(lattice->hasGlb());
+                auto glbName = as<UserDefinedFunctor>(lattice->getGlb())->getName();
+                VecOwn<Argument> args;
+                args.push_back(mk<Variable>(lat, arg->getSrcLoc()));
+                args.push_back(clone(arg));
+                auto glb = mk<UserDefinedFunctor>(glbName, std::move(args), arg->getSrcLoc());
+                newConstraints.push_back(mk<BinaryConstraint>(
+                        BinaryConstraintOp::EQ, std::move(glb), clone(arg), arg->getSrcLoc()));
+                return mk<Variable>(lat, arg->getSrcLoc());
+            } else {
+                return node;
+            }
+        }
+        node->apply(*this);
+        return node;
+    }
+
+private:
+    std::map<const ast::Argument*, const ast::Lattice*> toReplace;
+    VecOwn<ast::Literal>& newConstraints;
+};
+
+struct varInfo {
+    const ast::Lattice* lattice;
+    // lattice variables in body atoms
+    std::set<const ast::Variable*> variables;
+    // set of newly introduced variable names
+    std::set<std::string> glbs;
+};
+
+/*
+ * If a non-negated body atom has a lattice argument `x` that is not grounded,
+ * e.g. `R(a, b, x)`:
+ * Then, we gather all occurences of `x` that appear as lattice arguments,
+ * replace these occurences with distinct variable names `x_1`, `x_2`, ... `x_n`
+ * and we compute the GLB of all these occurences and store in variable `x`,
+ * and finally add the constraint `x != BOTTOM`.
+ * If the variable `x` is used in the atom head, it can remain unchanged.
+ * If some literals have constraints on `x`, e.g. `@myfunctor(x) > 0`:
+ * This means we would need to find the greatest lower bound of `x_1`, `x_2`, ... `x_n`
+ * verifying the constraints, which is not possible => the clause cannot be translated.
+ */
+struct ReplaceUngroundedLatticeArguments : public NodeMapper {
+    ReplaceUngroundedLatticeArguments(varInfo& infos) : infos(infos){};
+
+    Own<Node> operator()(Own<Node> node) const override {
+        if (auto arg = as<ast::Variable>(node)) {
+            if (infos.variables.count(arg) > 0) {
+                std::string varName;
+                varName = arg->getName() + "_<lattice" + std::to_string(infos.glbs.size()) + ">";
+                infos.glbs.insert(varName);
+                return mk<Variable>(varName, arg->getSrcLoc());
+            }
+        }
+        node->apply(*this);
+        return node;
+    }
+
+private:
+    varInfo& infos;
+};
+
+/*
+ * If a negated body atom has lattice argument `arg1, ..., argN`,
+ * e.g. `!R(a, b, arg1, arg2)`, then
+ * - the arguments `arg1`, ... `argN` must be bound by other atoms
+ * - We must translate the negated atom `!R(a, b, arg1, arg2)`
+ *   into the disjunction :
+ * (
+ *  !R(a, b, _, _) ;
+ *  R(a, b, lat1, _), GLB(lat1, arg1) = BOTTOM;
+ *  R(a, b, _, lat2), GLB(lat2, arg2) = BOTTOM
+ * )
+ */
+
+RuleBody LatticeTransformer::translateNegatedAtom(ast::Atom& atom) {
+    auto args = atom.getArguments();
+    auto range = latticeAttributes.equal_range(atom.getQualifiedName());
+
+    std::map<std::size_t, const QualifiedName> latticeIndexes;
+    for (auto it = range.first; it != range.second; it++) {
+        latticeIndexes.insert(it->second);
+    }
+
+    std::size_t arity = atom.getArity();
+    VecOwn<Argument> negatedArgs;
+    for (std::size_t i = 0; i < arity; i++) {
+        if (latticeIndexes.count(i)) {
+            negatedArgs.push_back(mk<UnnamedVariable>());
+        } else {
+            negatedArgs.push_back(clone(args[i]));
+        }
+    }
+    auto negated = mk<Atom>(atom.getQualifiedName(), std::move(negatedArgs), atom.getSrcLoc());
+    RuleBody body = RuleBody::atom(std::move(negated)).negated();
+
+    // create one disjunct per argument
+    for (const auto& [index, type] : latticeIndexes) {
+        const ast::Lattice* lattice = lattices.at(type);
+        VecOwn<Argument> arguments;
+        const auto& arg = args[index];
+        if (isA<UnnamedVariable>(arg)) {
+            continue;
+        }
+        const auto& sloc = arg->getSrcLoc();
+        std::string lat =
+                "<lattice" + std::to_string(sloc.start.line) + "_" + std::to_string(sloc.start.column) + ">";
+        for (std::size_t i = 0; i < arity; i++) {
+            if (latticeIndexes.count(i)) {
+                if (i == index) {
+                    arguments.push_back(mk<Variable>(lat));
+                } else {
+                    arguments.push_back(mk<UnnamedVariable>());
+                }
+            } else {
+                arguments.push_back(clone(args[i]));
+            }
+        }
+        VecOwn<Argument> glbArgs;
+        glbArgs.push_back(mk<Variable>(lat, sloc));
+        glbArgs.push_back(clone(arg));
+        auto glbName = as<UserDefinedFunctor>(lattice->getGlb())->getName();
+        auto glb = mk<UserDefinedFunctor>(glbName, std::move(glbArgs), sloc);
+        auto constraint = mk<BinaryConstraint>(
+                BinaryConstraintOp::EQ, std::move(glb), clone(lattice->getBottom()), sloc);
+        auto conjunct =
+                RuleBody::atom(mk<Atom>(atom.getQualifiedName(), std::move(arguments), atom.getSrcLoc()));
+        conjunct.conjunct(RuleBody::constraint(std::move(constraint)));
+        body.disjunct(std::move(conjunct));
+    }
+
+    return body;
+}
+
+bool LatticeTransformer::translateClause(
+        TranslationUnit& translationUnit, ErrorReport& report, ast::Clause* clause) {
+    bool changed;
+
+    // Set of atoms that are negated in the clause body and contain lattice arguments
+    std::set<const ast::Atom*> negatedLatticeAtoms;
+    // set of lattice arguments that are grounded, and their corresponding lattice
+    std::map<const ast::Argument*, const ast::Lattice*> groundedLatticeArguments;
+    // stores information on ungrounded lattice variable names
+    std::map<std::string, varInfo> ungroundedLatticeArguments;
+
+    // Compute grounded/ungrounded arguments
+    auto isGrounded = analysis::getGroundedTerms(translationUnit, *clause, true);
+
+    // Identify which body atoms are negated
+    std::set<const ast::Atom*> negated;
+    visit(clause->getBodyLiterals(), [&](const Negation& negation) { negated.insert(negation.getAtom()); });
+
+    // Identify lattice arguments in body atoms
+    visit(clause->getBodyLiterals(), [&](const Atom& atom) {
+        auto range = latticeAttributes.equal_range(atom.getQualifiedName());
+        auto args = atom.getArguments();
+        for (auto it = range.first; it != range.second; it++) {
+            const ast::Argument* arg = args[it->second.first];
+            assert(lattices.count(it->second.second) > 0);
+            const ast::Lattice* lattice = lattices.at(it->second.second);
+            if (isA<UnnamedVariable>(arg)) {
+                // nothing to do
+            } else if (negated.count(&atom)) {
+                negatedLatticeAtoms.insert(&atom);
+            } else if (isGrounded[arg]) {
+                groundedLatticeArguments.insert(std::make_pair(arg, lattice));
+            } else if (const auto* var = as<Variable>(arg)) {
+                ungroundedLatticeArguments[var->getName()].variables.insert(var);
+                ungroundedLatticeArguments[var->getName()].lattice = lattice;
+            } else {
+                report.addError("Lattice argument is not grounded", arg->getSrcLoc());
+            }
+        }
+    });
+
+    VecOwn<ast::Literal> constraints;
+
+    // Update grounded lattice arguments
+    ReplaceGroundedLatticeArguments update(groundedLatticeArguments, constraints);
+    for (auto* literal : clause->getBodyLiterals()) {
+        literal->apply(update);
+    }
+
+    // Update ungrounded lattice arguments
+    for (auto& it : ungroundedLatticeArguments) {
+        auto& infos = it.second;
+        auto& name = it.first;
+        if (infos.variables.size() > 1) {
+            changed = true;
+
+            // First, we must make sure that the ungrounded variables are only used as lattice arguments
+            visit(clause->getBodyLiterals(), [&](const Variable& variable) {
+                if (variable.getName() == name && !infos.variables.count(&variable)) {
+                    report.addError("Ungrounded lattice variable cannot be used in other literals",
+                            variable.getSrcLoc());
+                }
+            });
+
+            ReplaceUngroundedLatticeArguments update(infos);
+            for (auto* literal : clause->getBodyLiterals()) {
+                literal->apply(update);
+            }
+            // create new constraints
+            Own<Argument> glb;
+            const auto& lattice = infos.lattice;
+            assert(lattice->hasGlb());
+            auto glbName = as<UserDefinedFunctor>(lattice->getGlb())->getName();
+            for (const std::string& name : infos.glbs) {
+                if (!glb) {
+                    // first element
+                    glb = mk<Variable>(name, clause->getSrcLoc());
+                } else {
+                    VecOwn<Argument> args;
+                    args.push_back(mk<Variable>(name, clause->getSrcLoc()));
+                    args.push_back(std::move(glb));
+                    glb = mk<UserDefinedFunctor>(glbName, std::move(args), clause->getSrcLoc());
+                }
+            }
+            // x = GLB(...)
+            constraints.push_back(mk<BinaryConstraint>(BinaryConstraintOp::EQ,
+                    mk<Variable>(name, clause->getSrcLoc()), std::move(glb), clause->getSrcLoc()));
+            // x != BOTTOM
+            constraints.push_back(
+                    mk<BinaryConstraint>(BinaryConstraintOp::NE, mk<Variable>(name, clause->getSrcLoc()),
+                            clone(lattice->getBottom()), clause->getSrcLoc()));
+        }
+    }
+    clause->addToBody(std::move(constraints));
+
+    // updated negated atoms containing lattice arguments
+    if (!negatedLatticeAtoms.empty()) {
+        RuleBody body = RuleBody::getTrue();
+        for (const auto* lit : clause->getBodyLiterals()) {
+            if (const auto& neg = as<Negation>(lit)) {
+                body.conjunct(translateNegatedAtom(*neg->getAtom()));
+            } else if (const auto& atom = as<Atom>(lit)) {
+                body.conjunct(RuleBody::atom(clone(atom)));
+            } else if (const auto& cst = as<Constraint>(lit)) {
+                body.conjunct(RuleBody::constraint(clone(cst)));
+            } else {
+                assert(false && "unreachable");
+            }
+        }
+        VecOwn<Clause> clauses = body.toClauseBodies();
+        for (auto& c : clauses) {
+            c->setHead(clone(clause->getHead()));
+        }
+        translationUnit.getProgram().addClauses(std::move(clauses));
+        translationUnit.getProgram().removeClause(*clause);
+    }
+    return changed;
+}
+
+bool LatticeTransformer::transform(TranslationUnit& translationUnit) {
+    bool changed = false;
+    Program& program = translationUnit.getProgram();
+    ErrorReport& report = translationUnit.getErrorReport();
+
+    if (program.getLattices().empty()) {
+        return changed;
+    }
+
+    // populates map type name -> lattice
+    for (const ast::Lattice* lattice : program.getLattices()) {
+        // We ignore lattices lacking a definition for Glb and Bottom
+        if (lattice->hasGlb() && lattice->hasBottom()) {
+            lattices.emplace(lattice->getQualifiedName(), lattice);
+        }
+    }
+
+    for (const Relation* rel : program.getRelations()) {
+        const auto attributes = rel->getAttributes();
+        for (std::size_t i = 0; i < attributes.size(); i++) {
+            if (attributes[i]->getIsLattice()) {
+                const auto type = attributes[i]->getTypeName();
+                if (lattices.count(type)) {
+                    latticeAttributes.emplace(
+                            std::make_pair(rel->getQualifiedName(), std::make_pair(i, type)));
+                }
+            }
+        }
+    }
+    if (latticeAttributes.empty()) {
+        return false;
+    }
+
+    for (Clause* clause : program.getClauses()) {
+        changed |= translateClause(translationUnit, report, clause);
+    }
+
+    return changed;
+}
+
+}  // namespace souffle::ast::transform
diff --git a/src/ast/transform/InsertLatticeOperations.h b/src/ast/transform/InsertLatticeOperations.h
new file mode 100644
index 00000000000..aecb19a9ba0
--- /dev/null
+++ b/src/ast/transform/InsertLatticeOperations.h
@@ -0,0 +1,52 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023 The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file InsertLatticeOperations.h
+ *
+ * AST transformation related to the support of lattices
+ *
+ ***********************************************************************/
+
+#pragma once
+
+#include "ast/QualifiedName.h"
+#include "ast/TranslationUnit.h"
+#include "ast/transform/Transformer.h"
+#include "parser/ParserUtils.h"
+#include <set>
+#include <string>
+
+namespace souffle::ast::transform {
+
+/**
+ * Transformation pass to insert GLBs and checks != Bottom on lattice type attributes
+ */
+class LatticeTransformer : public Transformer {
+public:
+    std::string getName() const override {
+        return "InlineRelationsTransformer";
+    }
+
+private:
+    LatticeTransformer* cloning() const override {
+        return new LatticeTransformer();
+    }
+
+    bool translateClause(TranslationUnit& translationUnit, ErrorReport& report, ast::Clause* clause);
+
+    bool transform(TranslationUnit& translationUnit) override;
+
+    RuleBody translateNegatedAtom(ast::Atom& atom);
+
+    std::multimap<const QualifiedName, std::pair<std::size_t, const QualifiedName>> latticeAttributes;
+    std::map<const ast::QualifiedName, const ast::Lattice*> lattices;
+};
+
+}  // namespace souffle::ast::transform
diff --git a/src/ast/transform/SemanticChecker.cpp b/src/ast/transform/SemanticChecker.cpp
index 0e076159130..8d8c7ee9ba2 100644
--- a/src/ast/transform/SemanticChecker.cpp
+++ b/src/ast/transform/SemanticChecker.cpp
@@ -38,6 +38,7 @@
 #include "ast/IntrinsicAggregator.h"
 #include "ast/IntrinsicFunctor.h"
 #include "ast/IterationCounter.h"
+#include "ast/Lattice.h"
 #include "ast/Literal.h"
 #include "ast/Negation.h"
 #include "ast/NilConstant.h"
@@ -124,6 +125,7 @@ struct SemanticCheckerImpl {
     void checkRelationFunctionalDependencies(const Relation& relation);
     void checkRelation(const Relation& relation);
     void checkType(ast::Attribute const& attr, std::string const& name = {});
+    void checkLatticeDeclaration(const Lattice& lattice);
     void checkFunctorDeclaration(const FunctorDeclaration& decl);
 
     void checkNamespaces();
@@ -173,6 +175,9 @@ SemanticCheckerImpl::SemanticCheckerImpl(TranslationUnit& tu) : tu(tu) {
     for (auto* rel : program.getRelations()) {
         checkRelation(*rel);
     }
+    for (auto* lattice : program.getLattices()) {
+        checkLatticeDeclaration(*lattice);
+    }
     for (auto* clause : program.getClauses()) {
         checkClause(*clause);
     }
@@ -244,10 +249,10 @@ void SemanticCheckerImpl::checkAtom(const Clause& parent, const Atom& atom) {
         report.addError("Undefined relation " + toString(atom.getQualifiedName()), atom.getSrcLoc());
         return;
     }
-
-    if (r->getArity() != atom.getArity()) {
+    std::size_t arity = r->getArity();
+    if (arity != atom.getArity()) {
         report.addError("Mismatching arity of relation " + toString(atom.getQualifiedName()) + " (expected " +
-                                toString(r->getArity()) + ", got " + toString(atom.getArity()) + ")",
+                                toString(arity) + ", got " + toString(atom.getArity()) + ")",
                 atom.getSrcLoc());
     }
 
@@ -658,11 +663,43 @@ void SemanticCheckerImpl::checkFunctorDeclaration(const FunctorDeclaration& decl
     }
 }
 
+void SemanticCheckerImpl::checkLatticeDeclaration(const Lattice& lattice) {
+    const auto& name = lattice.getQualifiedName();
+    auto* existingType = getIf(
+            program.getTypes(), [&](const ast::Type* type) { return type->getQualifiedName() == name; });
+    if (!existingType) {
+        report.addError(tfm::format("Undefined type %s", name), lattice.getSrcLoc());
+    }
+    if (lattice.hasLub()) {
+        if (!isA<UserDefinedFunctor>(lattice.getLub())) {
+            report.addError(
+                    tfm::format("Lattice operator Lub must be a user-defined functor"), lattice.getSrcLoc());
+        }
+    } else {
+        report.addError(tfm::format("Lattice %s<> does not define Lub", name), lattice.getSrcLoc());
+    }
+    if (lattice.hasGlb()) {
+        if (!isA<UserDefinedFunctor>(lattice.getGlb())) {
+            report.addError(
+                    tfm::format("Lattice operator Glb must be a user-defined functor"), lattice.getSrcLoc());
+        }
+    } else {
+        report.addWarning(WarnType::LatticeMissingOperator,
+                tfm::format("Lattice %s<> does not define Glb", name), lattice.getSrcLoc());
+    }
+    if (!lattice.hasBottom()) {
+        report.addWarning(WarnType::LatticeMissingOperator,
+                tfm::format("Lattice %s<> does not define Bottom", name), lattice.getSrcLoc());
+    }
+}
+
 void SemanticCheckerImpl::checkRelationDeclaration(const Relation& relation) {
     const auto& attributes = relation.getAttributes();
-    assert(attributes.size() == relation.getArity() && "mismatching attribute size and arity");
+    const std::size_t arity = relation.getArity();
+    std::size_t firstAuxiliary = arity - relation.getAuxiliaryArity();
 
-    for (std::size_t i = 0; i < relation.getArity(); i++) {
+    assert(attributes.size() == arity && "mismatching attribute size and arity");
+    for (std::size_t i = 0; i < arity; i++) {
         Attribute* attr = attributes[i];
         checkType(*attr);
 
@@ -672,6 +709,25 @@ void SemanticCheckerImpl::checkRelationDeclaration(const Relation& relation) {
                 report.addError(tfm::format("Doubly defined attribute name %s", *attr), attr->getSrcLoc());
             }
         }
+
+        /* check that lattice elements are always the last */
+        if (i < firstAuxiliary && attr->getIsLattice()) {
+            report.addError(
+                    tfm::format(
+                            "Lattice attribute %s should be placed after all non-lattice attributes", *attr),
+                    attr->getSrcLoc());
+        }
+
+        /* check that lattice attributes have a correct lattice definition */
+        if (attr->getIsLattice()) {
+            const auto& typeName = attr->getTypeName();
+            auto* existingType = getIf(program.getLattices(),
+                    [&](const ast::Lattice* lattice) { return lattice->getQualifiedName() == typeName; });
+            if (!existingType) {
+                report.addError(
+                        tfm::format("Missing lattice definition for type %s", typeName), attr->getSrcLoc());
+            }
+        }
     }
 }
 
@@ -728,7 +784,21 @@ void SemanticCheckerImpl::checkRelation(const Relation& relation) {
     }
     if (relation.getRepresentation() == RelationRepresentation::BTREE_DELETE && relation.getArity() == 0) {
         report.addError("Subsumptive relation \"" + toString(relation.getQualifiedName()) +
-                                "\"  must not be a nullary relation",
+                                "\" must not be a nullary relation",
+                relation.getSrcLoc());
+    }
+
+    if (hasSubsumptiveRule && relation.getAuxiliaryArity()) {
+        report.addError("Relation \"" + toString(relation.getQualifiedName()) +
+                                "\" must not have both subsumptive rules and lattice arguments",
+                relation.getSrcLoc());
+    }
+
+    if (relation.getAuxiliaryArity() &&
+            (relation.getRepresentation() != RelationRepresentation::BTREE &&
+                    relation.getRepresentation() != RelationRepresentation::DEFAULT)) {
+        report.addError(
+                "Relation \"" + toString(relation.getQualifiedName()) + "\" must have a btree representation",
                 relation.getSrcLoc());
     }
 
diff --git a/src/ast/utility/Visitor.h b/src/ast/utility/Visitor.h
index 1b07687c275..beb08643e6d 100644
--- a/src/ast/utility/Visitor.h
+++ b/src/ast/utility/Visitor.h
@@ -39,6 +39,7 @@
 #include "ast/IntrinsicAggregator.h"
 #include "ast/IntrinsicFunctor.h"
 #include "ast/IterationCounter.h"
+#include "ast/Lattice.h"
 #include "ast/Literal.h"
 #include "ast/Negation.h"
 #include "ast/NilConstant.h"
@@ -185,6 +186,7 @@ struct Visitor : souffle::detail::VisitorBase<R, NodeType, Params...> {
     SOUFFLE_VISITOR_LINK(Relation, Node);
     SOUFFLE_VISITOR_LINK(Pragma, Node);
     SOUFFLE_VISITOR_LINK(FunctorDeclaration, Node);
+    SOUFFLE_VISITOR_LINK(ast::Lattice, Node);
 };
 }  // namespace souffle::ast
 
diff --git a/src/ast2ram/ClauseTranslator.h b/src/ast2ram/ClauseTranslator.h
index 93021f514f6..d157804276d 100644
--- a/src/ast2ram/ClauseTranslator.h
+++ b/src/ast2ram/ClauseTranslator.h
@@ -39,6 +39,8 @@ class TranslatorContext;
 enum TranslationMode {
     DEFAULT,
 
+    Auxiliary,
+
     // Subsumptive clauses
     //
     //   R(x0) <= R(x1) :- body.
diff --git a/src/ast2ram/provenance/UnitTranslator.cpp b/src/ast2ram/provenance/UnitTranslator.cpp
index 6c105d882d7..1691422c10d 100644
--- a/src/ast2ram/provenance/UnitTranslator.cpp
+++ b/src/ast2ram/provenance/UnitTranslator.cpp
@@ -24,12 +24,14 @@
 #include "ast2ram/utility/TranslatorContext.h"
 #include "ast2ram/utility/Utils.h"
 #include "ast2ram/utility/ValueIndex.h"
+#include "ram/AbstractOperator.h"
 #include "ram/Call.h"
 #include "ram/DebugInfo.h"
 #include "ram/ExistenceCheck.h"
 #include "ram/Expression.h"
 #include "ram/Filter.h"
 #include "ram/Insert.h"
+#include "ram/IntrinsicOperator.h"
 #include "ram/LogRelationTimer.h"
 #include "ram/MergeExtend.h"
 #include "ram/Negation.h"
@@ -69,18 +71,12 @@ Own<ram::Sequence> UnitTranslator::generateProgram(const ast::TranslationUnit& t
 
 Own<ram::Relation> UnitTranslator::createRamRelation(
         const ast::Relation* baseRelation, std::string ramRelationName) const {
-    auto arity = baseRelation->getArity();
+    auto relation = seminaive::UnitTranslator::createRamRelation(baseRelation, ramRelationName);
 
-    // All relations in a provenance program should have a provenance data structure
-    auto representation = RelationRepresentation::PROVENANCE;
-
-    // Add in base relation information
-    std::vector<std::string> attributeNames;
-    std::vector<std::string> attributeTypeQualifiers;
-    for (const auto& attribute : baseRelation->getAttributes()) {
-        attributeNames.push_back(attribute->getName());
-        attributeTypeQualifiers.push_back(context->getAttributeTypeQualifier(attribute->getTypeName()));
-    }
+    std::size_t arity = relation->getArity();
+    std::size_t auxiliaryArity = relation->getAuxiliaryArity();
+    std::vector<std::string> attributeNames = relation->getAttributeNames();
+    std::vector<std::string> attributeTypeQualifiers = relation->getAttributeTypes();
 
     // Add in provenance information
     attributeNames.push_back("@rule_number");
@@ -89,8 +85,8 @@ Own<ram::Relation> UnitTranslator::createRamRelation(
     attributeNames.push_back("@level_number");
     attributeTypeQualifiers.push_back("i:number");
 
-    return mk<ram::Relation>(
-            ramRelationName, arity + 2, 2, attributeNames, attributeTypeQualifiers, representation);
+    return mk<ram::Relation>(ramRelationName, arity + 2, auxiliaryArity + 2, attributeNames,
+            attributeTypeQualifiers, relation->getRepresentation());
 }
 
 std::string UnitTranslator::getInfoRelationName(const ast::Clause* clause) const {
diff --git a/src/ast2ram/seminaive/UnitTranslator.cpp b/src/ast2ram/seminaive/UnitTranslator.cpp
index 07b4fd9104c..164278f077f 100644
--- a/src/ast2ram/seminaive/UnitTranslator.cpp
+++ b/src/ast2ram/seminaive/UnitTranslator.cpp
@@ -20,12 +20,14 @@
 #include "ast/Relation.h"
 #include "ast/SubsumptiveClause.h"
 #include "ast/TranslationUnit.h"
+#include "ast/UserDefinedFunctor.h"
 #include "ast/analysis/TopologicallySortedSCCGraph.h"
 #include "ast/utility/Utils.h"
 #include "ast/utility/Visitor.h"
 #include "ast2ram/ClauseTranslator.h"
 #include "ast2ram/utility/TranslatorContext.h"
 #include "ast2ram/utility/Utils.h"
+#include "ram/Aggregate.h"
 #include "ram/Assign.h"
 #include "ram/Call.h"
 #include "ram/Clear.h"
@@ -60,7 +62,10 @@
 #include "ram/Swap.h"
 #include "ram/TranslationUnit.h"
 #include "ram/TupleElement.h"
+#include "ram/UndefValue.h"
 #include "ram/UnsignedConstant.h"
+#include "ram/UserDefinedAggregator.h"
+#include "ram/UserDefinedOperator.h"
 #include "ram/Variable.h"
 #include "ram/utility/Utils.h"
 #include "reports/DebugReport.h"
@@ -113,7 +118,8 @@ Own<ram::Statement> UnitTranslator::generateNonRecursiveRelation(const ast::Rela
         }
 
         // Translate clause
-        Own<ram::Statement> rule = context->translateNonRecursiveClause(*clause);
+        TranslationMode mode = rel.getAuxiliaryArity() > 0 ? Auxiliary : DEFAULT;
+        Own<ram::Statement> rule = context->translateNonRecursiveClause(*clause, mode);
 
         // Add logging
         if (glb->config().has("profile")) {
@@ -176,8 +182,16 @@ Own<ram::Statement> UnitTranslator::generateStratum(std::size_t scc) const {
         const auto* rel = *sccRelations.begin();
         appendStmt(current, generateNonRecursiveRelation(*rel));
 
+        // lub auxiliary arities using the @lub relation
+        if (rel->getAuxiliaryArity() > 0) {
+            std::string mainRelation = getConcreteRelationName(rel->getQualifiedName());
+            std::string newRelation = getNewRelationName(rel->getQualifiedName());
+            appendStmt(current, generateStratumLubSequence(*rel, newRelation, mainRelation));
+            appendStmt(current, mk<ram::Clear>(newRelation));
+        }
+
         // issue delete sequence for non-recursive subsumptions
-        appendStmt(current, generateNonRecursiveDelete(sccRelations));
+        appendStmt(current, generateNonRecursiveDelete(*rel));
     }
 
     // Get all non-recursive relation statements
@@ -404,50 +418,47 @@ VecOwn<ram::Statement> UnitTranslator::generateClauseVersions(
     return clauseVersions;
 }
 
-Own<ram::Statement> UnitTranslator::generateNonRecursiveDelete(const ast::RelationSet& scc) const {
+Own<ram::Statement> UnitTranslator::generateNonRecursiveDelete(const ast::Relation& rel) const {
     VecOwn<ram::Statement> code;
 
     // Generate code for non-recursive subsumption
-    for (const ast::Relation* rel : scc) {
-        if (!context->hasSubsumptiveClause(rel->getQualifiedName())) {
+    if (!context->hasSubsumptiveClause(rel.getQualifiedName())) {
+        return mk<ram::Sequence>(std::move(code));
+    }
+
+    std::string mainRelation = getConcreteRelationName(rel.getQualifiedName());
+    std::string deleteRelation = getDeleteRelationName(rel.getQualifiedName());
+
+    // Compute subsumptive deletions for non-recursive rules
+    for (auto clause : context->getProgram()->getClauses(rel)) {
+        if (!isA<ast::SubsumptiveClause>(clause)) {
             continue;
         }
 
-        std::string mainRelation = getConcreteRelationName(rel->getQualifiedName());
-        std::string deleteRelation = getDeleteRelationName(rel->getQualifiedName());
-
-        // Compute subsumptive deletions for non-recursive rules
-        for (auto clause : context->getProgram()->getClauses(*rel)) {
-            if (!isA<ast::SubsumptiveClause>(clause)) {
-                continue;
-            }
+        // Translate subsumptive clause
+        Own<ram::Statement> rule = context->translateNonRecursiveClause(*clause, SubsumeDeleteCurrentCurrent);
 
-            // Translate subsumptive clause
-            Own<ram::Statement> rule =
-                    context->translateNonRecursiveClause(*clause, SubsumeDeleteCurrentCurrent);
-
-            // Add logging for subsumptive clause
-            if (glb->config().has("profile")) {
-                const std::string& relationName = toString(rel->getQualifiedName());
-                const auto& srcLocation = clause->getSrcLoc();
-                const std::string clauseText = stringify(toString(*clause));
-                const std::string logTimerStatement =
-                        LogStatement::tNonrecursiveRule(relationName, srcLocation, clauseText);
-                rule = mk<ram::LogRelationTimer>(std::move(rule), logTimerStatement, mainRelation);
-            }
+        // Add logging for subsumptive clause
+        if (glb->config().has("profile")) {
+            const std::string& relationName = toString(rel.getQualifiedName());
+            const auto& srcLocation = clause->getSrcLoc();
+            const std::string clauseText = stringify(toString(*clause));
+            const std::string logTimerStatement =
+                    LogStatement::tNonrecursiveRule(relationName, srcLocation, clauseText);
+            rule = mk<ram::LogRelationTimer>(std::move(rule), logTimerStatement, mainRelation);
+        }
 
-            // Add debug info for subsumptive clause
-            std::ostringstream ds;
-            ds << toString(*clause) << "\nin file ";
-            ds << clause->getSrcLoc();
-            rule = mk<ram::DebugInfo>(std::move(rule), ds.str());
+        // Add debug info for subsumptive clause
+        std::ostringstream ds;
+        ds << toString(*clause) << "\nin file ";
+        ds << clause->getSrcLoc();
+        rule = mk<ram::DebugInfo>(std::move(rule), ds.str());
 
-            // Add subsumptive rule to result
-            appendStmt(code, std::move(rule));
-        }
-        appendStmt(code, mk<ram::Sequence>(generateEraseTuples(rel, mainRelation, deleteRelation),
-                                 mk<ram::Clear>(deleteRelation)));
+        // Add subsumptive rule to result
+        appendStmt(code, std::move(rule));
     }
+    appendStmt(code, mk<ram::Sequence>(generateEraseTuples(&rel, mainRelation, deleteRelation),
+                             mk<ram::Clear>(deleteRelation)));
     return mk<ram::Sequence>(std::move(code));
 }
 
@@ -459,11 +470,16 @@ Own<ram::Statement> UnitTranslator::generateStratumPreamble(const ast::RelationS
         std::string deltaRelation = getDeltaRelationName(rel->getQualifiedName());
         std::string mainRelation = getConcreteRelationName(rel->getQualifiedName());
         appendStmt(preamble, generateNonRecursiveRelation(*rel));
+        // lub tuples using the @lub relation
+        if (rel->getAuxiliaryArity() > 0) {
+            std::string newRelation = getNewRelationName(rel->getQualifiedName());
+            appendStmt(preamble, generateStratumLubSequence(*rel, newRelation, mainRelation));
+            appendStmt(preamble, mk<ram::Clear>(newRelation));
+        }
+        // Generate non recursive delete sequences for subsumptive rules
+        appendStmt(preamble, generateNonRecursiveDelete(*rel));
     }
 
-    // Generate non recursive delete sequences for subsumptive rules
-    appendStmt(preamble, generateNonRecursiveDelete(scc));
-
     // Generate code for priming relation
     for (const ast::Relation* rel : scc) {
         std::string deltaRelation = getDeltaRelationName(rel->getQualifiedName());
@@ -503,7 +519,11 @@ Own<ram::Statement> UnitTranslator::generateStratumTableUpdates(const ast::Relat
 
         // swap new and and delta relation and clear new relation afterwards (if not a subsumptive relation)
         Own<ram::Statement> updateRelTable;
-        if (!context->hasSubsumptiveClause(rel->getQualifiedName())) {
+        if (rel->getAuxiliaryArity() > 0) {
+            updateRelTable = mk<ram::Sequence>(mk<ram::Clear>(deltaRelation),
+                    generateStratumLubSequence(*rel, newRelation, deltaRelation),
+                    generateMergeRelations(rel, mainRelation, deltaRelation));
+        } else if (!context->hasSubsumptiveClause(rel->getQualifiedName())) {
             updateRelTable = mk<ram::Sequence>(generateMergeRelations(rel, mainRelation, newRelation),
                     mk<ram::Swap>(deltaRelation, newRelation), mk<ram::Clear>(newRelation));
         } else {
@@ -563,6 +583,120 @@ Own<ram::Statement> UnitTranslator::generateStratumLoopBody(const ast::RelationS
     return mk<ram::Sequence>(std::move(loopBody));
 }
 
+/// assuming the @new() relation is populated with new tuples, generate RAM code
+/// to populate the @delta() relation with the lubbed elements from @new()
+Own<ram::Statement> UnitTranslator::generateStratumLubSequence(
+        const ast::Relation& rel, const std::string& fromName, const std::string& toName) const {
+    VecOwn<ram::Statement> stmts;
+    assert(rel.getAuxiliaryArity() > 0);
+
+    auto attributes = rel.getAttributes();
+    std::string name = getConcreteRelationName(rel.getQualifiedName());
+    std::string lubName = getLubRelationName(rel.getQualifiedName());
+
+    const std::size_t arity = rel.getArity();
+    const std::size_t auxiliaryArity = rel.getAuxiliaryArity();
+
+    // Step 1 : populate @lub() from @new()
+    VecOwn<ram::Expression> values;
+
+    // index of the first auxiliary element of the relation
+    std::size_t firstAuxiliary = arity - auxiliaryArity;
+
+    for (std::size_t i = 0; i < arity; i++) {
+        if (i >= firstAuxiliary) {
+            values.push_back(mk<ram::TupleElement>(i - firstAuxiliary + 1, 0));
+        } else {
+            values.push_back(mk<ram::TupleElement>(0, i));
+        }
+    }
+    Own<ram::Operation> op = mk<ram::Insert>(lubName, std::move(values));
+
+    for (std::size_t i = arity; i >= firstAuxiliary + 1; i--) {
+        const auto type = attributes[i - 1]->getTypeName();
+        std::size_t level = i - firstAuxiliary;
+        auto aggregator = context->getLatticeTypeLubAggregator(type, mk<ram::TupleElement>(0, i - 1));
+        Own<ram::Condition> condition = mk<ram::Constraint>(
+                BinaryConstraintOp::NE, mk<ram::TupleElement>(level, i - 1), mk<ram::TupleElement>(0, i - 1));
+        for (std::size_t j = 0; j < attributes.size(); j++) {
+            if (attributes[j]->getIsLattice()) break;
+            condition = mk<ram::Conjunction>(std::move(condition),
+                    mk<ram::Constraint>(BinaryConstraintOp::EQ, mk<ram::TupleElement>(level, j),
+                            mk<ram::TupleElement>(0, j)));
+        }
+        op = mk<ram::Aggregate>(std::move(op), std::move(aggregator), fromName,
+                mk<ram::TupleElement>(level, i - 1), std::move(condition), level);
+    }
+
+    op = mk<ram::Scan>(fromName, 0, std::move(op));
+    appendStmt(stmts, mk<ram::Query>(std::move(op)));
+
+    // clear @new() now that we no longer need it
+    appendStmt(stmts, mk<ram::Clear>(fromName));
+
+    // Step 2 : populate @delta() from @lub() for tuples that have to be lubbed with @concrete
+
+    Own<ram::Condition> condition;
+    for (std::size_t i = 0; i < arity; i++) {
+        if (i < firstAuxiliary) {
+            values.push_back(mk<ram::TupleElement>(0, i));
+        } else {
+            assert(attributes[i]->getIsLattice());
+            const auto type = attributes[i]->getTypeName();
+            VecOwn<ram::Expression> args;
+            args.push_back(mk<ram::TupleElement>(0, i));
+            args.push_back(mk<ram::TupleElement>(1, i));
+            auto lub = context->getLatticeTypeLubFunctor(type, std::move(args));
+            auto cst = mk<ram::Constraint>(BinaryConstraintOp::EQ, mk<ram::TupleElement>(1, i), clone(lub));
+            if (condition) {
+                condition = mk<ram::Conjunction>(std::move(condition), std::move(cst));
+            } else {
+                condition = std::move(cst);
+            }
+            values.push_back(std::move(lub));
+        }
+    }
+    op = mk<ram::Insert>(toName, std::move(values));
+    op = mk<ram::Filter>(mk<ram::Negation>(std::move(condition)), std::move(op));
+
+    for (std::size_t i = 0; i < arity - auxiliaryArity; i++) {
+        auto cst = mk<ram::Constraint>(
+                BinaryConstraintOp::EQ, mk<ram::TupleElement>(0, i), mk<ram::TupleElement>(1, i));
+        if (condition) {
+            condition = mk<ram::Conjunction>(std::move(condition), std::move(cst));
+        } else {
+            condition = std::move(cst);
+        }
+    }
+    if (condition) {
+        op = mk<ram::Filter>(std::move(condition), std::move(op));
+    }
+    op = mk<ram::Scan>(name, 1, std::move(op));
+    op = mk<ram::Scan>(lubName, 0, std::move(op));
+    appendStmt(stmts, mk<ram::Query>(std::move(op)));
+
+    // Step 3 : populate @delta() from @lub() for tuples that have nothing to lub in @concrete
+    for (std::size_t i = 0; i < arity; i++) {
+        values.push_back(mk<ram::TupleElement>(0, i));
+    }
+    op = mk<ram::Insert>(toName, std::move(values));
+    for (std::size_t i = 0; i < arity; i++) {
+        if (i < firstAuxiliary) {
+            values.push_back(mk<ram::TupleElement>(0, i));
+        } else {
+            values.push_back(mk<ram::UndefValue>());
+        }
+    }
+    op = mk<ram::Filter>(mk<ram::Negation>(mk<ram::ExistenceCheck>(name, std::move(values))), std::move(op));
+    op = mk<ram::Scan>(lubName, 0, std::move(op));
+
+    appendStmt(stmts, mk<ram::Query>(std::move(op)));
+
+    appendStmt(stmts, mk<ram::Clear>(lubName));
+
+    return mk<ram::Sequence>(std::move(stmts));
+}
+
 Own<ram::Statement> UnitTranslator::generateStratumExitSequence(const ast::RelationSet& scc) const {
     // Helper function to add a new term to a conjunctive condition
     auto addCondition = [&](Own<ram::Condition>& cond, Own<ram::Condition> term) {
@@ -688,6 +822,10 @@ Own<ram::Statement> UnitTranslator::generateStoreRelation(const ast::Relation* r
 Own<ram::Relation> UnitTranslator::createRamRelation(
         const ast::Relation* baseRelation, std::string ramRelationName) const {
     auto arity = baseRelation->getArity();
+
+    bool mergeAuxiliary = (ramRelationName != getNewRelationName(baseRelation->getQualifiedName()));
+
+    auto auxArity = mergeAuxiliary ? baseRelation->getAuxiliaryArity() : 0;
     auto representation = baseRelation->getRepresentation();
     if (representation == RelationRepresentation::BTREE_DELETE && ramRelationName[0] == '@') {
         representation = RelationRepresentation::DEFAULT;
@@ -701,7 +839,7 @@ Own<ram::Relation> UnitTranslator::createRamRelation(
     }
 
     return mk<ram::Relation>(
-            ramRelationName, arity, 0, attributeNames, attributeTypeQualifiers, representation);
+            ramRelationName, arity, auxArity, attributeNames, attributeTypeQualifiers, representation);
 }
 
 VecOwn<ram::Relation> UnitTranslator::createRamRelations(const std::vector<std::size_t>& sccOrdering) const {
@@ -713,16 +851,24 @@ VecOwn<ram::Relation> UnitTranslator::createRamRelations(const std::vector<std::
             std::string mainName = getConcreteRelationName(rel->getQualifiedName());
             ramRelations.push_back(createRamRelation(rel, mainName));
 
+            if (rel->getAuxiliaryArity() > 0) {
+                // Add lub relation
+                std::string lubName = getLubRelationName(rel->getQualifiedName());
+                ramRelations.push_back(createRamRelation(rel, lubName));
+            }
+
+            if (isRecursive || rel->getAuxiliaryArity() > 0) {
+                // Add new relation
+                std::string newName = getNewRelationName(rel->getQualifiedName());
+                ramRelations.push_back(createRamRelation(rel, newName));
+            }
+
             // Recursive relations also require @delta and @new variants, with the same signature
             if (isRecursive) {
                 // Add delta relation
                 std::string deltaName = getDeltaRelationName(rel->getQualifiedName());
                 ramRelations.push_back(createRamRelation(rel, deltaName));
 
-                // Add new relation
-                std::string newName = getNewRelationName(rel->getQualifiedName());
-                ramRelations.push_back(createRamRelation(rel, newName));
-
                 // Add auxiliary relation for subsumption
                 if (context->hasSubsumptiveClause(rel->getQualifiedName())) {
                     // Add reject relation
diff --git a/src/ast2ram/seminaive/UnitTranslator.h b/src/ast2ram/seminaive/UnitTranslator.h
index 5c1400b2170..4499a1caa53 100644
--- a/src/ast2ram/seminaive/UnitTranslator.h
+++ b/src/ast2ram/seminaive/UnitTranslator.h
@@ -81,11 +81,13 @@ class UnitTranslator : public ast2ram::UnitTranslator {
     /** Low-level stratum translation */
     Own<ram::Statement> generateStratum(std::size_t scc) const;
     Own<ram::Statement> generateStratumPreamble(const ast::RelationSet& scc) const;
-    Own<ram::Statement> generateNonRecursiveDelete(const ast::RelationSet& scc) const;
+    Own<ram::Statement> generateNonRecursiveDelete(const ast::Relation& rel) const;
     Own<ram::Statement> generateStratumPostamble(const ast::RelationSet& scc) const;
     Own<ram::Statement> generateStratumLoopBody(const ast::RelationSet& scc) const;
     Own<ram::Statement> generateStratumTableUpdates(const ast::RelationSet& scc) const;
     Own<ram::Statement> generateStratumExitSequence(const ast::RelationSet& scc) const;
+    Own<ram::Statement> generateStratumLubSequence(
+            const ast::Relation& rel, const std::string& fromName, const std::string& toName) const;
 
     /** Other helper generations */
     virtual Own<ram::Statement> generateClearExpiredRelations(const ast::RelationSet& expiredRelations) const;
diff --git a/src/ast2ram/utility/TranslatorContext.cpp b/src/ast2ram/utility/TranslatorContext.cpp
index b7f677f3ef5..a9589307173 100644
--- a/src/ast2ram/utility/TranslatorContext.cpp
+++ b/src/ast2ram/utility/TranslatorContext.cpp
@@ -14,9 +14,12 @@
 
 #include "ast2ram/utility/TranslatorContext.h"
 #include "Global.h"
+#include "ast/Aggregator.h"
 #include "ast/Atom.h"
 #include "ast/BranchInit.h"
 #include "ast/Directive.h"
+#include "ast/Functor.h"
+#include "ast/IntrinsicFunctor.h"
 #include "ast/QualifiedName.h"
 #include "ast/SubsumptiveClause.h"
 #include "ast/TranslationUnit.h"
@@ -39,11 +42,18 @@
 #include "ast2ram/provenance/TranslationStrategy.h"
 #include "ast2ram/seminaive/TranslationStrategy.h"
 #include "ast2ram/utility/SipsMetric.h"
+#include "ram/AbstractOperator.h"
 #include "ram/Condition.h"
 #include "ram/Expression.h"
+#include "ram/IntrinsicAggregator.h"
+#include "ram/IntrinsicOperator.h"
 #include "ram/Statement.h"
+#include "ram/UndefValue.h"
+#include "ram/UserDefinedAggregator.h"
+#include "ram/UserDefinedOperator.h"
 #include "souffle/utility/FunctionalUtil.h"
 #include "souffle/utility/StringUtil.h"
+#include <optional>
 #include <set>
 
 namespace souffle::ast2ram {
@@ -96,6 +106,11 @@ TranslatorContext::TranslatorContext(const ast::TranslationUnit& tu) {
             deltaRel[program->getRelation(delta.value())] = rel;
         }
     }
+
+    // populates map type name -> lattice
+    for (const ast::Lattice* lattice : program->getLattices()) {
+        lattices.emplace(lattice->getQualifiedName(), lattice);
+    }
 }
 
 TranslatorContext::~TranslatorContext() = default;
@@ -113,6 +128,40 @@ std::string TranslatorContext::getAttributeTypeQualifier(const ast::QualifiedNam
     return getTypeQualifier(typeEnv->getType(name));
 }
 
+Own<ram::AbstractOperator> TranslatorContext::getLatticeTypeLubFunctor(
+        const ast::QualifiedName& typeName, VecOwn<ram::Expression> args) const {
+    const ast::Lattice* lattice = lattices.at(typeName);
+    if (const auto* lub = as<ast::UserDefinedFunctor>(lattice->getLub())) {
+        const auto typeAttributes = getFunctorParamTypeAtributes(*lub);
+        const auto returnAttribute = getFunctorReturnTypeAttribute(*lub);
+        bool stateful = isStatefulFunctor(*lub);
+        return mk<ram::UserDefinedOperator>(
+                lub->getName(), typeAttributes, returnAttribute, stateful, std::move(args));
+    } else if (const auto* lub = as<ast::IntrinsicFunctor>(lattice->getLub())) {
+        assert(false && lub && "intrinsic functors not yet supported in lattice");
+        // return mk<ram::IntrinsicOperator>(getOverloadedFunctorOp(lub->getBaseFunctionOp()),
+        // std::move(args));
+    }
+    assert(false);
+    return {};
+}
+
+Own<ram::Aggregator> TranslatorContext::getLatticeTypeLubAggregator(
+        const ast::QualifiedName& typeName, Own<ram::Expression> init) const {
+    const ast::Lattice* lattice = lattices.at(typeName);
+    if (const auto* lub = as<ast::UserDefinedFunctor>(lattice->getLub())) {
+        const auto typeAttributes = getFunctorParamTypeAtributes(*lub);
+        const auto returnAttribute = getFunctorReturnTypeAttribute(*lub);
+        bool stateful = isStatefulFunctor(*lub);
+        return mk<ram::UserDefinedAggregator>(
+                lub->getName(), std::move(init), typeAttributes, returnAttribute, stateful);
+    } else if (const auto* lub = as<ast::IntrinsicFunctor>(lattice->getLub())) {
+        assert(false && lub && "intrinsic aggregators not yet supported in lattice");
+    }
+    assert(false);
+    return {};
+}
+
 std::size_t TranslatorContext::getNumberOfSCCs() const {
     return sccGraph->getNumberOfSCCs();
 }
diff --git a/src/ast2ram/utility/TranslatorContext.h b/src/ast2ram/utility/TranslatorContext.h
index 0447068b7fd..0df1092586e 100644
--- a/src/ast2ram/utility/TranslatorContext.h
+++ b/src/ast2ram/utility/TranslatorContext.h
@@ -23,6 +23,7 @@
 #include "ast/analysis/ProfileUse.h"
 #include "ast/analysis/typesystem/Type.h"
 #include "ast2ram/ClauseTranslator.h"
+#include "ram/Aggregator.h"
 #include "souffle/BinaryConstraintOps.h"
 #include "souffle/TypeAttribute.h"
 #include "souffle/utility/ContainerUtil.h"
@@ -96,6 +97,11 @@ class TranslatorContext {
     bool hasSizeLimit(const ast::Relation* relation) const;
     std::size_t getSizeLimit(const ast::Relation* relation) const;
 
+    Own<ram::Aggregator> getLatticeTypeLubAggregator(
+            const ast::QualifiedName& typeName, Own<ram::Expression> init) const;
+    Own<ram::AbstractOperator> getLatticeTypeLubFunctor(
+            const ast::QualifiedName& typeName, VecOwn<ram::Expression> args) const;
+
     /** Associates a relation with its delta_debug relation if present */
     const ast::Relation* getDeltaDebugRelation(const ast::Relation* rel) const;
 
@@ -172,6 +178,7 @@ class TranslatorContext {
     Own<ast::SipsMetric> sipsMetric;
     Own<TranslationStrategy> translationStrategy;
     std::map<const ast::Relation*, const ast::Relation*> deltaRel;
+    std::map<const ast::QualifiedName, const ast::Lattice*> lattices;
 };
 
 }  // namespace souffle::ast2ram
diff --git a/src/ast2ram/utility/Utils.cpp b/src/ast2ram/utility/Utils.cpp
index 7ce90a3786d..d74ddd3a3b2 100644
--- a/src/ast2ram/utility/Utils.cpp
+++ b/src/ast2ram/utility/Utils.cpp
@@ -23,6 +23,7 @@
 #include "ast/UnnamedVariable.h"
 #include "ast/Variable.h"
 #include "ast/utility/Utils.h"
+#include "ast2ram/ClauseTranslator.h"
 #include "ast2ram/utility/Location.h"
 #include "ram/Clear.h"
 #include "ram/Condition.h"
@@ -77,6 +78,9 @@ std::string getAtomName(const ast::Clause& clause, const ast::Atom* atom,
     }
 
     if (!isRecursive) {
+        if (mode == Auxiliary && clause.getHead() == atom) {
+            return getNewRelationName(atom->getQualifiedName());
+        }
         return getConcreteRelationName(atom->getQualifiedName());
     }
     if (clause.getHead() == atom) {
@@ -100,6 +104,10 @@ std::string getNewRelationName(const ast::QualifiedName& name) {
     return getConcreteRelationName(name, "@new_");
 }
 
+std::string getLubRelationName(const ast::QualifiedName& name) {
+    return getConcreteRelationName(name, "@lub_");
+}
+
 std::string getRejectRelationName(const ast::QualifiedName& name) {
     return getConcreteRelationName(name, "@reject_");
 }
diff --git a/src/ast2ram/utility/Utils.h b/src/ast2ram/utility/Utils.h
index 65d1f5543f0..330488a40b2 100644
--- a/src/ast2ram/utility/Utils.h
+++ b/src/ast2ram/utility/Utils.h
@@ -54,6 +54,9 @@ std::string getDeltaRelationName(const ast::QualifiedName& name);
 /** Get the corresponding RAM 'new' relation name for the relation */
 std::string getNewRelationName(const ast::QualifiedName& name);
 
+/** Get the corresponding RAM 'lub' relation name for the relation */
+std::string getLubRelationName(const ast::QualifiedName& name);
+
 /** Get the corresponding RAM 'reject' relation name for the relation */
 std::string getRejectRelationName(const ast::QualifiedName& name);
 
diff --git a/src/include/souffle/datastructure/BTree.h b/src/include/souffle/datastructure/BTree.h
index 47d2bc8226d..72b4fc90105 100644
--- a/src/include/souffle/datastructure/BTree.h
+++ b/src/include/souffle/datastructure/BTree.h
@@ -91,8 +91,8 @@ class btree {
     /* -------------- updater utilities ------------- */
 
     mutable Updater upd;
-    void update(Key& old_k, const Key& new_k) {
-        upd.update(old_k, new_k);
+    bool update(Key& old_k, const Key& new_k) {
+        return upd.update(old_k, new_k);
     }
 
     /* -------------- the node type ----------------- */
@@ -1225,14 +1225,14 @@ class btree {
                     }
 
                     // update provenance information
-                    if (typeid(Comparator) != typeid(WeakComparator) && less(k, *pos)) {
+                    if (typeid(Comparator) != typeid(WeakComparator)) {
                         if (!cur->lock.try_upgrade_to_write(cur_lease)) {
                             // start again
                             return insert(k, hints);
                         }
-                        update(*pos, k);
+                        bool updated = update(*pos, k);
                         cur->lock.end_write();
-                        return true;
+                        return updated;
                     }
 
                     // we found the element => no check of lock necessary
@@ -1280,14 +1280,14 @@ class btree {
                 }
 
                 // update provenance information
-                if (typeid(Comparator) != typeid(WeakComparator) && less(k, *(pos - 1))) {
+                if (typeid(Comparator) != typeid(WeakComparator)) {
                     if (!cur->lock.try_upgrade_to_write(cur_lease)) {
                         // start again
                         return insert(k, hints);
                     }
-                    update(*(pos - 1), k);
+                    bool updated = update(*(pos - 1), k);
                     cur->lock.end_write();
-                    return true;
+                    return updated;
                 }
 
                 // we found the element => done
@@ -1432,9 +1432,8 @@ class btree {
                 // early exit for sets
                 if (isSet && pos != b && weak_equal(*pos, k)) {
                     // update provenance information
-                    if (typeid(Comparator) != typeid(WeakComparator) && less(k, *pos)) {
-                        update(*pos, k);
-                        return true;
+                    if (typeid(Comparator) != typeid(WeakComparator)) {
+                        return update(*pos, k);
                     }
 
                     return false;
@@ -1458,9 +1457,8 @@ class btree {
             // early exit for sets
             if (isSet && pos != a && weak_equal(*(pos - 1), k)) {
                 // update provenance information
-                if (typeid(Comparator) != typeid(WeakComparator) && less(k, *(pos - 1))) {
-                    update(*(pos - 1), k);
-                    return true;
+                if (typeid(Comparator) != typeid(WeakComparator)) {
+                    return update(*(pos - 1), k);
                 }
 
                 return false;
diff --git a/src/include/souffle/datastructure/BTreeDelete.h b/src/include/souffle/datastructure/BTreeDelete.h
index 745a3c12216..fc747ff1c46 100644
--- a/src/include/souffle/datastructure/BTreeDelete.h
+++ b/src/include/souffle/datastructure/BTreeDelete.h
@@ -92,8 +92,8 @@ class btree_delete {
     /* -------------- updater utilities ------------- */
 
     mutable Updater upd;
-    void update(Key& old_k, const Key& new_k) {
-        upd.update(old_k, new_k);
+    bool update(Key& old_k, const Key& new_k) {
+        return upd.update(old_k, new_k);
     }
 
     /* -------------- the node type ----------------- */
@@ -1278,14 +1278,14 @@ class btree_delete {
                     }
 
                     // update provenance information
-                    if (typeid(Comparator) != typeid(WeakComparator) && less(k, *pos)) {
+                    if (typeid(Comparator) != typeid(WeakComparator)) {
                         if (!cur->lock.try_upgrade_to_write(cur_lease)) {
                             // start again
                             return insert(k, hints);
                         }
-                        update(*pos, k);
+                        bool updated = update(*pos, k);
                         cur->lock.end_write();
-                        return true;
+                        return updated;
                     }
 
                     // we found the element => no check of lock necessary
@@ -1333,14 +1333,14 @@ class btree_delete {
                 }
 
                 // update provenance information
-                if (typeid(Comparator) != typeid(WeakComparator) && less(k, *(pos - 1))) {
+                if (typeid(Comparator) != typeid(WeakComparator)) {
                     if (!cur->lock.try_upgrade_to_write(cur_lease)) {
                         // start again
                         return insert(k, hints);
                     }
-                    update(*(pos - 1), k);
+                    bool updated = update(*(pos - 1), k);
                     cur->lock.end_write();
-                    return true;
+                    return updated;
                 }
 
                 // we found the element => done
@@ -1485,9 +1485,8 @@ class btree_delete {
                 // early exit for sets
                 if (isSet && pos != b && weak_equal(*pos, k)) {
                     // update provenance information
-                    if (typeid(Comparator) != typeid(WeakComparator) && less(k, *pos)) {
-                        update(*pos, k);
-                        return true;
+                    if (typeid(Comparator) != typeid(WeakComparator)) {
+                        return update(*pos, k);
                     }
 
                     return false;
@@ -1511,9 +1510,8 @@ class btree_delete {
             // early exit for sets
             if (isSet && pos != a && weak_equal(*(pos - 1), k)) {
                 // update provenance information
-                if (typeid(Comparator) != typeid(WeakComparator) && less(k, *(pos - 1))) {
-                    update(*(pos - 1), k);
-                    return true;
+                if (typeid(Comparator) != typeid(WeakComparator)) {
+                    return update(*(pos - 1), k);
                 }
 
                 return false;
diff --git a/src/include/souffle/datastructure/BTreeUtil.h b/src/include/souffle/datastructure/BTreeUtil.h
index bdf624fa5ca..164006005db 100644
--- a/src/include/souffle/datastructure/BTreeUtil.h
+++ b/src/include/souffle/datastructure/BTreeUtil.h
@@ -217,7 +217,9 @@ struct default_strategy<std::tuple<Ts...>> : public linear {};
  */
 template <typename T>
 struct updater {
-    void update(T& /* old_t */, const T& /* new_t */) {}
+    bool update(T& /* old_t */, const T& /* new_t */) {
+        return false;
+    }
 };
 
 }  // end of namespace detail
diff --git a/src/interpreter/BTreeDeleteIndex.cpp b/src/interpreter/BTreeDeleteIndex.cpp
index 1d51bbc172e..7275e3728e5 100644
--- a/src/interpreter/BTreeDeleteIndex.cpp
+++ b/src/interpreter/BTreeDeleteIndex.cpp
@@ -21,18 +21,15 @@
 
 namespace souffle::interpreter {
 
-#define CREATE_BTREE_DELETE_REL(Structure, Arity, ...)                                               \
-    case (Arity): {                                                                                  \
-        return mk<BtreeDeleteRelation<Arity>>(id.getAuxiliaryArity(), id.getName(), indexSelection); \
+#define CREATE_BTREE_DELETE_REL(Structure, Arity, AuxiliaryArity, ...)                       \
+    if (id.getArity() == Arity && id.getAuxiliaryArity() == AuxiliaryArity) {                \
+        return mk<BtreeDeleteRelation<Arity, AuxiliaryArity>>(id.getName(), indexSelection); \
     }
 
 Own<RelationWrapper> createBTreeDeleteRelation(
         const ram::Relation& id, const ram::analysis::IndexCluster& indexSelection) {
-    switch (id.getArity()) {
-        FOR_EACH_BTREE_DELETE(CREATE_BTREE_DELETE_REL);
-
-        default: fatal("Requested arity not yet supported. Feel free to add it.");
-    }
+    FOR_EACH_BTREE_DELETE(CREATE_BTREE_DELETE_REL);
+    fatal("Requested arity not yet supported. Feel free to add it.");
 }
 
 }  // namespace souffle::interpreter
diff --git a/src/interpreter/BTreeIndex.cpp b/src/interpreter/BTreeIndex.cpp
index 97127bf35f4..5a42aa6c491 100644
--- a/src/interpreter/BTreeIndex.cpp
+++ b/src/interpreter/BTreeIndex.cpp
@@ -21,19 +21,15 @@
 
 namespace souffle::interpreter {
 
-#define CREATE_BTREE_REL(Structure, Arity, ...)                        \
-    case (Arity): {                                                    \
-        return mk<Relation<Arity, interpreter::Btree>>(                \
-                id.getAuxiliaryArity(), id.getName(), indexSelection); \
+#define CREATE_BTREE_REL(Structure, Arity, AuxiliaryArity, ...)                                       \
+    if (id.getArity() == Arity && id.getAuxiliaryArity() == AuxiliaryArity) {                         \
+        return mk<Relation<Arity, AuxiliaryArity, interpreter::Btree>>(id.getName(), indexSelection); \
     }
 
 Own<RelationWrapper> createBTreeRelation(
         const ram::Relation& id, const ram::analysis::IndexCluster& indexSelection) {
-    switch (id.getArity()) {
-        FOR_EACH_BTREE(CREATE_BTREE_REL);
-
-        default: fatal("Requested arity not yet supported. Feel free to add it.");
-    }
+    FOR_EACH_BTREE(CREATE_BTREE_REL);
+    fatal("Requested arity not yet supported. Feel free to add it.");
 }
 
 }  // namespace souffle::interpreter
diff --git a/src/interpreter/Engine.cpp b/src/interpreter/Engine.cpp
index 521f7f9fc8e..27b57854640 100644
--- a/src/interpreter/Engine.cpp
+++ b/src/interpreter/Engine.cpp
@@ -359,13 +359,13 @@ void Engine::createRelation(const ram::Relation& id, const std::size_t idx) {
     }
 
     RelationHandle res;
-
-    if (id.getRepresentation() == RelationRepresentation::EQREL) {
+    bool hasProvenance = id.getArity() > 0 && id.getAttributeNames().back() == "@level_number";
+    if (hasProvenance) {
+        res = createProvenanceRelation(id, isa.getIndexSelection(id.getName()));
+    } else if (id.getRepresentation() == RelationRepresentation::EQREL) {
         res = createEqrelRelation(id, isa.getIndexSelection(id.getName()));
     } else if (id.getRepresentation() == RelationRepresentation::BTREE_DELETE) {
         res = createBTreeDeleteRelation(id, isa.getIndexSelection(id.getName()));
-    } else if (id.getRepresentation() == RelationRepresentation::PROVENANCE) {
-        res = createProvenanceRelation(id, isa.getIndexSelection(id.getName()));
     } else {
         res = createBTreeRelation(id, isa.getIndexSelection(id.getName()));
     }
@@ -527,9 +527,9 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
 
 // Overload CASE based on number of arguments.
 // CASE(Kind) -> BASE_CASE(Kind)
-// CASE(Kind, Structure, Arity) -> EXTEND_CASE(Kind, Structure, Arity)
-#define GET_MACRO(_1, _2, _3, NAME, ...) NAME
-#define CASE(...) GET_MACRO(__VA_ARGS__, EXTEND_CASE, _Dummy, BASE_CASE)(__VA_ARGS__)
+// CASE(Kind, Structure, Arity, AuxiliaryArity) -> EXTEND_CASE(Kind, Structure, Arity, AuxiliaryArity)
+#define GET_MACRO(_1, _2, _3, _4, NAME, ...) NAME
+#define CASE(...) GET_MACRO(__VA_ARGS__, EXTEND_CASE, _Dummy, _Dummy2, BASE_CASE)(__VA_ARGS__)
 
 #define BASE_CASE(Kind) \
     case (I_##Kind): {  \
@@ -537,12 +537,12 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
             [[maybe_unused]] const auto& shadow = *static_cast<const interpreter::Kind*>(node); \
             [[maybe_unused]] const auto& cur = *static_cast<const ram::Kind*>(node->getShadow());
 // EXTEND_CASE also defer the relation type
-#define EXTEND_CASE(Kind, Structure, Arity)    \
-    case (I_##Kind##_##Structure##_##Arity): { \
+#define EXTEND_CASE(Kind, Structure, Arity, AuxiliaryArity)       \
+    case (I_##Kind##_##Structure##_##Arity##_##AuxiliaryArity): { \
         return [&]() -> RamDomain { \
             [[maybe_unused]] const auto& shadow = *static_cast<const interpreter::Kind*>(node); \
             [[maybe_unused]] const auto& cur = *static_cast<const ram::Kind*>(node->getShadow());\
-            using RelType = Relation<Arity, interpreter::Structure>;
+            using RelType = Relation<Arity, AuxiliaryArity, interpreter::Structure>;
 #define ESAC(Kind) \
     }              \
     ();            \
@@ -986,8 +986,8 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
             return !execute(shadow.getChild(), ctxt);
         ESAC(Negation)
 
-#define EMPTINESS_CHECK(Structure, Arity, ...)                          \
-    CASE(EmptinessCheck, Structure, Arity)                              \
+#define EMPTINESS_CHECK(Structure, Arity, AuxiliaryArity, ...)          \
+    CASE(EmptinessCheck, Structure, Arity, AuxiliaryArity)              \
         const auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return rel.empty();                                             \
     ESAC(EmptinessCheck)
@@ -995,8 +995,8 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
         FOR_EACH(EMPTINESS_CHECK)
 #undef EMPTINESS_CHECK
 
-#define RELATION_SIZE(Structure, Arity, ...)                            \
-    CASE(RelationSize, Structure, Arity)                                \
+#define RELATION_SIZE(Structure, Arity, AuxiliaryArity, ...)            \
+    CASE(RelationSize, Structure, Arity, AuxiliaryArity)                \
         const auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return rel.size();                                              \
     ESAC(RelationSize)
@@ -1004,17 +1004,17 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
         FOR_EACH(RELATION_SIZE)
 #undef RELATION_SIZE
 
-#define EXISTENCE_CHECK(Structure, Arity, ...)            \
-    CASE(ExistenceCheck, Structure, Arity)                \
-        return evalExistenceCheck<RelType>(shadow, ctxt); \
+#define EXISTENCE_CHECK(Structure, Arity, AuxiliaryArity, ...) \
+    CASE(ExistenceCheck, Structure, Arity, AuxiliaryArity)     \
+        return evalExistenceCheck<RelType>(shadow, ctxt);      \
     ESAC(ExistenceCheck)
 
         FOR_EACH(EXISTENCE_CHECK)
 #undef EXISTENCE_CHECK
 
-#define PROVENANCE_EXISTENCE_CHECK(Structure, Arity, ...)           \
-    CASE(ProvenanceExistenceCheck, Structure, Arity)                \
-        return evalProvenanceExistenceCheck<RelType>(shadow, ctxt); \
+#define PROVENANCE_EXISTENCE_CHECK(Structure, Arity, AuxiliaryArity, ...) \
+    CASE(ProvenanceExistenceCheck, Structure, Arity, AuxiliaryArity)      \
+        return evalProvenanceExistenceCheck<RelType>(shadow, ctxt);       \
     ESAC(ProvenanceExistenceCheck)
 
         FOR_EACH_PROVENANCE(PROVENANCE_EXISTENCE_CHECK)
@@ -1135,8 +1135,8 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
             return result;
         ESAC(TupleOperation)
 
-#define SCAN(Structure, Arity, ...)                                     \
-    CASE(Scan, Structure, Arity)                                        \
+#define SCAN(Structure, Arity, AuxiliaryArity, ...)                     \
+    CASE(Scan, Structure, Arity, AuxiliaryArity)                        \
         const auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return evalScan(rel, cur, shadow, ctxt);                        \
     ESAC(Scan)
@@ -1144,24 +1144,24 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
         FOR_EACH(SCAN)
 #undef SCAN
 
-#define PARALLEL_SCAN(Structure, Arity, ...)                            \
-    CASE(ParallelScan, Structure, Arity)                                \
+#define PARALLEL_SCAN(Structure, Arity, AuxiliaryArity, ...)            \
+    CASE(ParallelScan, Structure, Arity, AuxiliaryArity)                \
         const auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return evalParallelScan(rel, cur, shadow, ctxt);                \
     ESAC(ParallelScan)
         FOR_EACH(PARALLEL_SCAN)
 #undef PARALLEL_SCAN
 
-#define INDEX_SCAN(Structure, Arity, ...)                 \
-    CASE(IndexScan, Structure, Arity)                     \
+#define INDEX_SCAN(Structure, Arity, AuxiliaryArity, ...) \
+    CASE(IndexScan, Structure, Arity, AuxiliaryArity)     \
         return evalIndexScan<RelType>(cur, shadow, ctxt); \
     ESAC(IndexScan)
 
         FOR_EACH(INDEX_SCAN)
 #undef INDEX_SCAN
 
-#define PARALLEL_INDEX_SCAN(Structure, Arity, ...)                      \
-    CASE(ParallelIndexScan, Structure, Arity)                           \
+#define PARALLEL_INDEX_SCAN(Structure, Arity, AuxiliaryArity, ...)      \
+    CASE(ParallelIndexScan, Structure, Arity, AuxiliaryArity)           \
         const auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return evalParallelIndexScan(rel, cur, shadow, ctxt);           \
     ESAC(ParallelIndexScan)
@@ -1169,8 +1169,8 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
         FOR_EACH(PARALLEL_INDEX_SCAN)
 #undef PARALLEL_INDEX_SCAN
 
-#define IFEXISTS(Structure, Arity, ...)                                 \
-    CASE(IfExists, Structure, Arity)                                    \
+#define IFEXISTS(Structure, Arity, AuxiliaryArity, ...)                 \
+    CASE(IfExists, Structure, Arity, AuxiliaryArity)                    \
         const auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return evalIfExists(rel, cur, shadow, ctxt);                    \
     ESAC(IfExists)
@@ -1178,8 +1178,8 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
         FOR_EACH(IFEXISTS)
 #undef IFEXISTS
 
-#define PARALLEL_IFEXISTS(Structure, Arity, ...)                        \
-    CASE(ParallelIfExists, Structure, Arity)                            \
+#define PARALLEL_IFEXISTS(Structure, Arity, AuxiliaryArity, ...)        \
+    CASE(ParallelIfExists, Structure, Arity, AuxiliaryArity)            \
         const auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return evalParallelIfExists(rel, cur, shadow, ctxt);            \
     ESAC(ParallelIfExists)
@@ -1187,16 +1187,16 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
         FOR_EACH(PARALLEL_IFEXISTS)
 #undef PARALLEL_IFEXISTS
 
-#define INDEX_IFEXISTS(Structure, Arity, ...)                 \
-    CASE(IndexIfExists, Structure, Arity)                     \
+#define INDEX_IFEXISTS(Structure, Arity, AuxiliaryArity, ...) \
+    CASE(IndexIfExists, Structure, Arity, AuxiliaryArity)     \
         return evalIndexIfExists<RelType>(cur, shadow, ctxt); \
     ESAC(IndexIfExists)
 
         FOR_EACH(INDEX_IFEXISTS)
 #undef INDEX_IFEXISTS
 
-#define PARALLEL_INDEX_IFEXISTS(Structure, Arity, ...)                  \
-    CASE(ParallelIndexIfExists, Structure, Arity)                       \
+#define PARALLEL_INDEX_IFEXISTS(Structure, Arity, AuxiliaryArity, ...)  \
+    CASE(ParallelIndexIfExists, Structure, Arity, AuxiliaryArity)       \
         const auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return evalParallelIndexIfExists(rel, cur, shadow, ctxt);       \
     ESAC(ParallelIndexIfExists)
@@ -1223,8 +1223,8 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
             return execute(shadow.getNestedOperation(), ctxt);
         ESAC(UnpackRecord)
 
-#define PARALLEL_AGGREGATE(Structure, Arity, ...)                       \
-    CASE(ParallelAggregate, Structure, Arity)                           \
+#define PARALLEL_AGGREGATE(Structure, Arity, AuxiliaryArity, ...)       \
+    CASE(ParallelAggregate, Structure, Arity, AuxiliaryArity)           \
         const auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return evalParallelAggregate(rel, cur, shadow, ctxt);           \
     ESAC(ParallelAggregate)
@@ -1232,8 +1232,8 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
         FOR_EACH(PARALLEL_AGGREGATE)
 #undef PARALLEL_AGGREGATE
 
-#define AGGREGATE(Structure, Arity, ...)                                \
-    CASE(Aggregate, Structure, Arity)                                   \
+#define AGGREGATE(Structure, Arity, AuxiliaryArity, ...)                \
+    CASE(Aggregate, Structure, Arity, AuxiliaryArity)                   \
         const auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return evalAggregate(cur, shadow, rel.scan(), ctxt);            \
     ESAC(Aggregate)
@@ -1241,16 +1241,16 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
         FOR_EACH(AGGREGATE)
 #undef AGGREGATE
 
-#define PARALLEL_INDEX_AGGREGATE(Structure, Arity, ...)                \
-    CASE(ParallelIndexAggregate, Structure, Arity)                     \
-        return evalParallelIndexAggregate<RelType>(cur, shadow, ctxt); \
+#define PARALLEL_INDEX_AGGREGATE(Structure, Arity, AuxiliaryArity, ...) \
+    CASE(ParallelIndexAggregate, Structure, Arity, AuxiliaryArity)      \
+        return evalParallelIndexAggregate<RelType>(cur, shadow, ctxt);  \
     ESAC(ParallelIndexAggregate)
 
         FOR_EACH(PARALLEL_INDEX_AGGREGATE)
 #undef PARALLEL_INDEX_AGGREGATE
 
-#define INDEX_AGGREGATE(Structure, Arity, ...)                 \
-    CASE(IndexAggregate, Structure, Arity)                     \
+#define INDEX_AGGREGATE(Structure, Arity, AuxiliaryArity, ...) \
+    CASE(IndexAggregate, Structure, Arity, AuxiliaryArity)     \
         return evalIndexAggregate<RelType>(cur, shadow, ctxt); \
     ESAC(IndexAggregate)
 
@@ -1283,8 +1283,8 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
             return result;
         ESAC(Filter)
 
-#define GUARDED_INSERT(Structure, Arity, ...)                     \
-    CASE(GuardedInsert, Structure, Arity)                         \
+#define GUARDED_INSERT(Structure, Arity, AuxiliaryArity, ...)     \
+    CASE(GuardedInsert, Structure, Arity, AuxiliaryArity)         \
         auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return evalGuardedInsert(rel, shadow, ctxt);              \
     ESAC(GuardedInsert)
@@ -1292,8 +1292,8 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
         FOR_EACH(GUARDED_INSERT)
 #undef GUARDED_INSERT
 
-#define INSERT(Structure, Arity, ...)                             \
-    CASE(Insert, Structure, Arity)                                \
+#define INSERT(Structure, Arity, AuxiliaryArity, ...)             \
+    CASE(Insert, Structure, Arity, AuxiliaryArity)                \
         auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return evalInsert(rel, shadow, ctxt);                     \
     ESAC(Insert)
@@ -1301,11 +1301,11 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
         FOR_EACH(INSERT)
 #undef INSERT
 
-#define ERASE(Structure, Arity, ...)                                                 \
-    CASE(Erase, Structure, Arity)                                                    \
-        void(static_cast<RelType*>(shadow.getRelation()));                           \
-        auto& rel = *static_cast<BtreeDeleteRelation<Arity>*>(shadow.getRelation()); \
-        return evalErase(rel, shadow, ctxt);                                         \
+#define ERASE(Structure, Arity, AuxiliaryArity, ...)                                                 \
+    CASE(Erase, Structure, Arity, AuxiliaryArity)                                                    \
+        void(static_cast<RelType*>(shadow.getRelation()));                                           \
+        auto& rel = *static_cast<BtreeDeleteRelation<Arity, AuxiliaryArity>*>(shadow.getRelation()); \
+        return evalErase(rel, shadow, ctxt);                                                         \
     ESAC(Erase)
 
         FOR_EACH_BTREE_DELETE(ERASE)
@@ -1369,8 +1369,8 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
             return execute(shadow.getChild(), ctxt);
         ESAC(DebugInfo)
 
-#define CLEAR(Structure, Arity, ...)                              \
-    CASE(Clear, Structure, Arity)                                 \
+#define CLEAR(Structure, Arity, AuxiliaryArity, ...)              \
+    CASE(Clear, Structure, Arity, AuxiliaryArity)                 \
         auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         rel.__purge();                                            \
         return true;                                              \
@@ -1379,8 +1379,8 @@ RamDomain Engine::execute(const Node* node, Context& ctxt) {
         FOR_EACH(CLEAR)
 #undef CLEAR
 
-#define ESTIMATEJOINSIZE(Structure, Arity, ...)                         \
-    CASE(EstimateJoinSize, Structure, Arity)                            \
+#define ESTIMATEJOINSIZE(Structure, Arity, AuxiliaryArity, ...)         \
+    CASE(EstimateJoinSize, Structure, Arity, AuxiliaryArity)            \
         const auto& rel = *static_cast<RelType*>(shadow.getRelation()); \
         return evalEstimateJoinSize<RelType>(rel, cur, shadow, ctxt);   \
     ESAC(EstimateJoinSize)
@@ -1945,7 +1945,7 @@ bool runNested(const ram::Aggregator& aggregator) {
             default: return false;
         }
     } else if (isA<ram::UserDefinedAggregator>(aggregator)) {
-        return false;
+        return true;
     }
     return false;
 }
diff --git a/src/interpreter/EqrelIndex.cpp b/src/interpreter/EqrelIndex.cpp
index 7a368c16e9a..b6aeef17e54 100644
--- a/src/interpreter/EqrelIndex.cpp
+++ b/src/interpreter/EqrelIndex.cpp
@@ -23,7 +23,8 @@ namespace souffle::interpreter {
 Own<RelationWrapper> createEqrelRelation(
         const ram::Relation& id, const ram::analysis::IndexCluster& indexSelection) {
     assert(id.getArity() == 2 && "Eqivalence relation must have arity size 2.");
-    return mk<EqrelRelation>(id.getAuxiliaryArity(), id.getName(), indexSelection);
+    assert(id.getAuxiliaryArity() == 0 && "Equivalence relation must have auxiliary arity size 0.");
+    return mk<EqrelRelation>(id.getName(), indexSelection);
 }
 
 }  // namespace souffle::interpreter
diff --git a/src/interpreter/Index.h b/src/interpreter/Index.h
index 3fc693de8b4..b2a35fc42a3 100644
--- a/src/interpreter/Index.h
+++ b/src/interpreter/Index.h
@@ -142,11 +142,13 @@ struct ViewWrapper {
 /**
  * An index is an abstraction of a data structure
  */
-template <std::size_t _Arity, template <std::size_t> typename Structure>
+template <std::size_t _Arity, std::size_t _AuxiliaryArity,
+        template <std::size_t, std::size_t> typename Structure>
 class Index {
 public:
     static constexpr std::size_t Arity = _Arity;
-    using Data = Structure<Arity>;
+    static constexpr std::size_t AuxiliaryArity = _AuxiliaryArity;
+    using Data = Structure<Arity, AuxiliaryArity>;
     using Tuple = typename souffle::Tuple<RamDomain, Arity>;
     using iterator = typename Data::iterator;
     using Hints = typename Data::operation_hints;
@@ -239,7 +241,7 @@ class Index {
     /**
      * Inserts all elements of the given index.
      */
-    void insert(const Index<Arity, Structure>& src) {
+    void insert(const Index<Arity, AuxiliaryArity, Structure>& src) {
         for (const auto& tuple : src) {
             this->insert(tuple);
         }
@@ -316,8 +318,8 @@ class Index {
  * A partial specialize template for nullary indexes.
  * No complex data structure is required.
  */
-template <template <std::size_t> typename Structure>
-class Index<0, Structure> {
+template <template <std::size_t, std::size_t> typename Structure>
+class Index<0, 0, Structure> {
 public:
     static constexpr std::size_t Arity = 0;
     using Tuple = typename souffle::Tuple<RamDomain, 0>;
@@ -452,9 +454,9 @@ class Index<0, Structure> {
 /**
  * For EqrelIndex we do inheritence since EqrelIndex only diff with one extra function.
  */
-class EqrelIndex : public interpreter::Index<2, Eqrel> {
+class EqrelIndex : public interpreter::Index<2, 0, Eqrel> {
 public:
-    using Index<2, Eqrel>::Index;
+    using Index<2, 0, Eqrel>::Index;
 
     /**
      * Extend this relation with another index, expanding this index and
@@ -475,12 +477,12 @@ class EqrelIndex : public interpreter::Index<2, Eqrel> {
 /**
  * A BtreeDelete index
  */
-template <std::size_t _Arity>
-class BtreeDeleteIndex : public interpreter::Index<_Arity, BtreeDelete> {
+template <std::size_t _Arity, std::size_t _AuxiliaryArity>
+class BtreeDeleteIndex : public interpreter::Index<_Arity, _AuxiliaryArity, BtreeDelete> {
 public:
-    using Index<_Arity, BtreeDelete>::Index;
-    using Index<_Arity, BtreeDelete>::data;
-    using Index<_Arity, BtreeDelete>::order;
+    using Index<_Arity, _AuxiliaryArity, BtreeDelete>::Index;
+    using Index<_Arity, _AuxiliaryArity, BtreeDelete>::data;
+    using Index<_Arity, _AuxiliaryArity, BtreeDelete>::order;
     using Tuple = typename souffle::Tuple<RamDomain, _Arity>;
 
     /**
diff --git a/src/interpreter/Node.h b/src/interpreter/Node.h
index de3c09a5763..1e07aa7eed4 100644
--- a/src/interpreter/Node.h
+++ b/src/interpreter/Node.h
@@ -117,8 +117,8 @@ struct RelationWrapper;
 
 #define SINGLE_TOKEN(tok) I_##tok,
 
-#define EXPAND_TOKEN(structure, arity, tok)\
-    I_##tok##_##structure##_##arity,
+#define EXPAND_TOKEN(structure, arity, auxiliaryArity, tok)\
+    I_##tok##_##structure##_##arity##_##auxiliaryArity,
 
 /*
  * Declares all the tokens.
@@ -134,30 +134,31 @@ enum NodeType {
 
 #define __TO_STRING(a) #a
 #define SINGLE_TOKEN_ENTRY(tok) {__TO_STRING(I_##tok), I_##tok},
-#define EXPAND_TOKEN_ENTRY(Structure, arity, tok) \
-    {__TO_STRING(I_##tok##_##Structure##_##arity), I_##tok##_##Structure##_##arity},
+#define EXPAND_TOKEN_ENTRY(Structure, arity, auxiliaryArity, tok) \
+    {__TO_STRING(I_##tok##_##Structure##_##arity##_##auxiliaryArity), I_##tok##_##Structure##_##arity##_##auxiliaryArity},
 
 /**
  * Construct interpreterNodeType by looking at the representation and the arity of the given rel.
  *
  * Add reflective from string to NodeType.
  */
-inline NodeType constructNodeType(Global& glb, std::string tokBase, const ram::Relation& rel) {
-    const bool isProvenance = glb.config().has("provenance");
+inline NodeType constructNodeType(Global&, std::string tokBase, const ram::Relation& rel) {
 
     static const std::unordered_map<std::string, NodeType> map = {
             FOR_EACH_INTERPRETER_TOKEN(SINGLE_TOKEN_ENTRY, EXPAND_TOKEN_ENTRY)
     };
 
     std::string arity = std::to_string(rel.getArity());
-    if (rel.getRepresentation() == RelationRepresentation::EQREL) {
-        return map.at("I_" + tokBase + "_Eqrel_" + arity);
+    std::string auxiliaryArity = std::to_string(rel.getAuxiliaryArity());
+    bool hasProvenance = rel.getArity() > 0 && rel.getAttributeNames().back() == "@level_number";
+    if (hasProvenance) {
+        return map.at("I_" + tokBase + "_Provenance_" + arity + "_" + auxiliaryArity);
+    } else if (rel.getRepresentation() == RelationRepresentation::EQREL) {
+        return map.at("I_" + tokBase + "_Eqrel_" + arity + "_" + auxiliaryArity);
     } else if(rel.getRepresentation() == RelationRepresentation::BTREE_DELETE) {
-        return map.at("I_" + tokBase + "_BtreeDelete_" + arity);
-    } else if (isProvenance) {
-        return map.at("I_" + tokBase + "_Provenance_" + arity);
+        return map.at("I_" + tokBase + "_BtreeDelete_" + arity + "_" + auxiliaryArity);
     } else  {
-        return map.at("I_" + tokBase + "_Btree_" + arity);
+        return map.at("I_" + tokBase + "_Btree_" + arity + "_" + auxiliaryArity);
     }
 
     fatal("Unrecognized node type: base:%s arity:%s.", tokBase, arity);
diff --git a/src/interpreter/ProvenanceIndex.cpp b/src/interpreter/ProvenanceIndex.cpp
index cb503f58107..3b770719a77 100644
--- a/src/interpreter/ProvenanceIndex.cpp
+++ b/src/interpreter/ProvenanceIndex.cpp
@@ -18,19 +18,15 @@
 
 namespace souffle::interpreter {
 
-#define CREATE_PROVENANCE_REL(Structure, Arity, ...)                   \
-    case (Arity): {                                                    \
-        return mk<Relation<Arity, interpreter::Provenance>>(           \
-                id.getAuxiliaryArity(), id.getName(), indexSelection); \
+#define CREATE_PROVENANCE_REL(Structure, Arity, AuxiliaryArity, ...)                                       \
+    if (id.getArity() == Arity && id.getAuxiliaryArity() == AuxiliaryArity) {                              \
+        return mk<Relation<Arity, AuxiliaryArity, interpreter::Provenance>>(id.getName(), indexSelection); \
     }
 
 Own<RelationWrapper> createProvenanceRelation(
         const ram::Relation& id, const ram::analysis::IndexCluster& indexSelection) {
-    switch (id.getArity()) {
-        FOR_EACH_PROVENANCE(CREATE_PROVENANCE_REL);
-
-        default: fatal("Requested arity not yet supported. Feel free to add it.");
-    }
+    FOR_EACH_PROVENANCE(CREATE_PROVENANCE_REL);
+    fatal("Requested arity not yet supported. Feel free to add it.");
 }
 
 }  // namespace souffle::interpreter
diff --git a/src/interpreter/Relation.h b/src/interpreter/Relation.h
index 8f0189b80c8..57b764cafb3 100644
--- a/src/interpreter/Relation.h
+++ b/src/interpreter/Relation.h
@@ -151,13 +151,15 @@ struct RelationWrapper {
 /**
  * A relation, composed of a collection of indexes.
  */
-template <std::size_t _Arity, template <std::size_t> typename Structure>
+template <std::size_t _Arity, std::size_t _AuxiliaryArity,
+        template <std::size_t, std::size_t> typename Structure>
 class Relation : public RelationWrapper {
 public:
     static constexpr std::size_t Arity = _Arity;
+    static constexpr std::size_t AuxiliaryArity = _AuxiliaryArity;
     using Attribute = std::size_t;
     using AttributeSet = std::set<Attribute>;
-    using Index = interpreter::Index<Arity, Structure>;
+    using Index = interpreter::Index<Arity, AuxiliaryArity, Structure>;
     using Tuple = souffle::Tuple<RamDomain, Arity>;
     using View = typename Index::View;
     using iterator = typename Index::iterator;
@@ -181,9 +183,8 @@ class Relation : public RelationWrapper {
     /**
      * Creates a relation, build all necessary indexes.
      */
-    Relation(std::size_t auxiliaryArity, const std::string& name,
-            const ram::analysis::IndexCluster& indexSelection)
-            : RelationWrapper(Arity, auxiliaryArity, name) {
+    Relation(const std::string& name, const ram::analysis::IndexCluster& indexSelection)
+            : RelationWrapper(Arity, AuxiliaryArity, name) {
         for (const auto& order : indexSelection.getAllOrders()) {
             ram::analysis::LexOrder fullOrder = order;
             // Expand the order to a total order
@@ -299,7 +300,7 @@ class Relation : public RelationWrapper {
     /**
      * Add all entries of the given relation to this relation.
      */
-    void insert(const Relation<Arity, Structure>& other) {
+    void insert(const Relation<Arity, AuxiliaryArity, Structure>& other) {
         for (const auto& tuple : other.scan()) {
             this->insert(tuple);
         }
@@ -354,7 +355,7 @@ class Relation : public RelationWrapper {
      * Swaps the content of this and the given relation, including the
      * installed indexes.
      */
-    void swap(Relation<Arity, Structure>& other) {
+    void swap(Relation<Arity, AuxiliaryArity, Structure>& other) {
         indexes.swap(other.indexes);
     }
 
@@ -393,9 +394,6 @@ class Relation : public RelationWrapper {
     }
 
 protected:
-    // Number of height parameters of relation
-    std::size_t auxiliaryArity;
-
     // a map of managed indexes
     VecOwn<Index> indexes;
 
@@ -403,19 +401,19 @@ class Relation : public RelationWrapper {
     Index* main;
 };
 
-template <std::size_t _Arity>
-class BtreeDeleteRelation : public Relation<_Arity, BtreeDelete> {
+template <std::size_t _Arity, std::size_t _AuxiliaryArity>
+class BtreeDeleteRelation : public Relation<_Arity, _AuxiliaryArity, BtreeDelete> {
 public:
-    using Relation<_Arity, BtreeDelete>::Relation;
-    using Relation<_Arity, BtreeDelete>::main;
-    using Relation<_Arity, BtreeDelete>::indexes;
+    using Relation<_Arity, _AuxiliaryArity, BtreeDelete>::Relation;
+    using Relation<_Arity, _AuxiliaryArity, BtreeDelete>::main;
+    using Relation<_Arity, _AuxiliaryArity, BtreeDelete>::indexes;
     using Tuple = souffle::Tuple<RamDomain, _Arity>;
 
     /**
      * Erase the given tuple from this relation.
      */
     bool erase(const Tuple& tuple) {
-        using DeleteIndex = BtreeDeleteIndex<_Arity>;
+        using DeleteIndex = BtreeDeleteIndex<_Arity, _AuxiliaryArity>;
         if (!(static_cast<DeleteIndex*>(main))->erase(tuple)) {
             return false;
         }
@@ -426,9 +424,9 @@ class BtreeDeleteRelation : public Relation<_Arity, BtreeDelete> {
     }
 };
 
-class EqrelRelation : public Relation<2, Eqrel> {
+class EqrelRelation : public Relation<2, 0, Eqrel> {
 public:
-    using Relation<2, Eqrel>::Relation;
+    using Relation<2, 0, Eqrel>::Relation;
 
     void extendAndInsert(const EqrelRelation& rel) {
         auto src = static_cast<EqrelIndex*>(this->main);
diff --git a/src/interpreter/Util.h b/src/interpreter/Util.h
index 7143ede39cf..60ea5e61e09 100644
--- a/src/interpreter/Util.h
+++ b/src/interpreter/Util.h
@@ -27,82 +27,91 @@
 namespace souffle::interpreter {
 // clang-format off
 
-#define FOR_EACH_PROVENANCE(func, ...) \
-    func(Provenance, 2, __VA_ARGS__)   \
-    func(Provenance, 3, __VA_ARGS__)   \
-    func(Provenance, 4, __VA_ARGS__)   \
-    func(Provenance, 5, __VA_ARGS__)   \
-    func(Provenance, 6, __VA_ARGS__)   \
-    func(Provenance, 7, __VA_ARGS__)   \
-    func(Provenance, 8, __VA_ARGS__)   \
-    func(Provenance, 9, __VA_ARGS__)   \
-    func(Provenance, 10, __VA_ARGS__)  \
-    func(Provenance, 11, __VA_ARGS__)  \
-    func(Provenance, 12, __VA_ARGS__)  \
-    func(Provenance, 13, __VA_ARGS__)  \
-    func(Provenance, 14, __VA_ARGS__)  \
-    func(Provenance, 15, __VA_ARGS__)  \
-    func(Provenance, 16, __VA_ARGS__)  \
-    func(Provenance, 17, __VA_ARGS__)  \
-    func(Provenance, 18, __VA_ARGS__)  \
-    func(Provenance, 19, __VA_ARGS__)  \
-    func(Provenance, 20, __VA_ARGS__)  \
-    func(Provenance, 21, __VA_ARGS__)  \
-    func(Provenance, 22, __VA_ARGS__)  \
-    func(Provenance, 23, __VA_ARGS__)  \
-    func(Provenance, 24, __VA_ARGS__)  \
-    func(Provenance, 25, __VA_ARGS__)  \
-    func(Provenance, 26, __VA_ARGS__)  \
-    func(Provenance, 27, __VA_ARGS__)  \
-    func(Provenance, 28, __VA_ARGS__)  \
-    func(Provenance, 29, __VA_ARGS__)  \
-    func(Provenance, 30, __VA_ARGS__)
 
+#define FOR_EACH_PROVENANCE(func, ...) \
+    func(Provenance, 2, 2, __VA_ARGS__)   \
+    func(Provenance, 3, 2, __VA_ARGS__)   \
+    func(Provenance, 4, 2, __VA_ARGS__)   \
+    func(Provenance, 5, 2, __VA_ARGS__)   \
+    func(Provenance, 6, 2, __VA_ARGS__)   \
+    func(Provenance, 7, 2, __VA_ARGS__)   \
+    func(Provenance, 8, 2, __VA_ARGS__)   \
+    func(Provenance, 9, 2, __VA_ARGS__)   \
+    func(Provenance, 10, 2, __VA_ARGS__)  \
+    func(Provenance, 11, 2, __VA_ARGS__)  \
+    func(Provenance, 12, 2, __VA_ARGS__)  \
+    func(Provenance, 13, 2, __VA_ARGS__)  \
+    func(Provenance, 14, 2, __VA_ARGS__)  \
+    func(Provenance, 15, 2, __VA_ARGS__)  \
+    func(Provenance, 16, 2, __VA_ARGS__)  \
+    func(Provenance, 17, 2, __VA_ARGS__)  \
+    func(Provenance, 18, 2, __VA_ARGS__)  \
+    func(Provenance, 19, 2, __VA_ARGS__)  \
+    func(Provenance, 20, 2, __VA_ARGS__)  \
+    func(Provenance, 21, 2, __VA_ARGS__)  \
+    func(Provenance, 22, 2, __VA_ARGS__)
 
 #define FOR_EACH_BTREE(func, ...)\
-    func(Btree, 0, __VA_ARGS__) \
-    func(Btree, 1, __VA_ARGS__) \
-    func(Btree, 2, __VA_ARGS__) \
-    func(Btree, 3, __VA_ARGS__) \
-    func(Btree, 4, __VA_ARGS__) \
-    func(Btree, 5, __VA_ARGS__) \
-    func(Btree, 6, __VA_ARGS__) \
-    func(Btree, 7, __VA_ARGS__) \
-    func(Btree, 8, __VA_ARGS__) \
-    func(Btree, 9, __VA_ARGS__) \
-    func(Btree, 10, __VA_ARGS__) \
-    func(Btree, 11, __VA_ARGS__) \
-    func(Btree, 12, __VA_ARGS__) \
-    func(Btree, 13, __VA_ARGS__) \
-    func(Btree, 14, __VA_ARGS__) \
-    func(Btree, 15, __VA_ARGS__) \
-    func(Btree, 16, __VA_ARGS__) \
-    func(Btree, 17, __VA_ARGS__) \
-    func(Btree, 18, __VA_ARGS__) \
-    func(Btree, 19, __VA_ARGS__) \
-    func(Btree, 20, __VA_ARGS__)
+    func(Btree, 0, 0, __VA_ARGS__) \
+    func(Btree, 1, 0, __VA_ARGS__) \
+    func(Btree, 2, 0, __VA_ARGS__) \
+    func(Btree, 3, 0, __VA_ARGS__) \
+    func(Btree, 4, 0, __VA_ARGS__) \
+    func(Btree, 5, 0, __VA_ARGS__) \
+    func(Btree, 6, 0, __VA_ARGS__) \
+    func(Btree, 7, 0, __VA_ARGS__) \
+    func(Btree, 8, 0, __VA_ARGS__) \
+    func(Btree, 9, 0, __VA_ARGS__) \
+    func(Btree, 10, 0, __VA_ARGS__) \
+    func(Btree, 11, 0, __VA_ARGS__) \
+    func(Btree, 12, 0, __VA_ARGS__) \
+    func(Btree, 13, 0, __VA_ARGS__) \
+    func(Btree, 14, 0, __VA_ARGS__) \
+    func(Btree, 15, 0, __VA_ARGS__) \
+    func(Btree, 16, 0, __VA_ARGS__) \
+    func(Btree, 17, 0, __VA_ARGS__) \
+    func(Btree, 18, 0, __VA_ARGS__) \
+    func(Btree, 19, 0, __VA_ARGS__) \
+    func(Btree, 20, 0, __VA_ARGS__) \
+    func(Btree, 1, 1, __VA_ARGS__)  \
+    func(Btree, 2, 1, __VA_ARGS__)  \
+    func(Btree, 2, 2, __VA_ARGS__)  \
+    func(Btree, 3, 1, __VA_ARGS__)  \
+    func(Btree, 3, 2, __VA_ARGS__)  \
+    func(Btree, 4, 1, __VA_ARGS__)  \
+    func(Btree, 4, 2, __VA_ARGS__)  \
+    func(Btree, 5, 1, __VA_ARGS__)  \
+    func(Btree, 5, 2, __VA_ARGS__)  \
+    func(Btree, 6, 1, __VA_ARGS__)  \
+    func(Btree, 6, 2, __VA_ARGS__)  \
+    func(Btree, 7, 1, __VA_ARGS__)  \
+    func(Btree, 7, 2, __VA_ARGS__)  \
+    func(Btree, 8, 1, __VA_ARGS__)  \
+    func(Btree, 8, 2, __VA_ARGS__)  \
+    func(Btree, 9, 1, __VA_ARGS__)  \
+    func(Btree, 9, 2, __VA_ARGS__)
 
 #define FOR_EACH_BTREE_DELETE(func, ...)\
-    func(BtreeDelete, 1, __VA_ARGS__) \
-    func(BtreeDelete, 2, __VA_ARGS__) \
-    func(BtreeDelete, 3, __VA_ARGS__) \
-    func(BtreeDelete, 4, __VA_ARGS__) \
-    func(BtreeDelete, 5, __VA_ARGS__) \
-    func(BtreeDelete, 6, __VA_ARGS__) \
-    func(BtreeDelete, 7, __VA_ARGS__) \
-    func(BtreeDelete, 8, __VA_ARGS__) \
-    func(BtreeDelete, 9, __VA_ARGS__) \
-    func(BtreeDelete, 10, __VA_ARGS__) \
-    func(BtreeDelete, 11, __VA_ARGS__) \
-    func(BtreeDelete, 12, __VA_ARGS__) \
-    func(BtreeDelete, 13, __VA_ARGS__) \
-    func(BtreeDelete, 14, __VA_ARGS__) \
-    func(BtreeDelete, 15, __VA_ARGS__) \
-    func(BtreeDelete, 16, __VA_ARGS__) \
-    func(BtreeDelete, 17, __VA_ARGS__) \
-    func(BtreeDelete, 18, __VA_ARGS__) \
-    func(BtreeDelete, 19, __VA_ARGS__) \
-    func(BtreeDelete, 20, __VA_ARGS__)
+    func(BtreeDelete, 1, 0, __VA_ARGS__) \
+    func(BtreeDelete, 2, 0, __VA_ARGS__) \
+    func(BtreeDelete, 3, 0, __VA_ARGS__) \
+    func(BtreeDelete, 4, 0, __VA_ARGS__) \
+    func(BtreeDelete, 5, 0, __VA_ARGS__) \
+    func(BtreeDelete, 6, 0, __VA_ARGS__) \
+    func(BtreeDelete, 7, 0, __VA_ARGS__) \
+    func(BtreeDelete, 8, 0, __VA_ARGS__) \
+    func(BtreeDelete, 9, 0, __VA_ARGS__) \
+    func(BtreeDelete, 10, 0, __VA_ARGS__) \
+    func(BtreeDelete, 11, 0, __VA_ARGS__) \
+    func(BtreeDelete, 12, 0, __VA_ARGS__) \
+    func(BtreeDelete, 13, 0, __VA_ARGS__) \
+    func(BtreeDelete, 14, 0, __VA_ARGS__) \
+    func(BtreeDelete, 15, 0, __VA_ARGS__) \
+    func(BtreeDelete, 16, 0, __VA_ARGS__) \
+    func(BtreeDelete, 17, 0, __VA_ARGS__) \
+    func(BtreeDelete, 18, 0, __VA_ARGS__) \
+    func(BtreeDelete, 19, 0, __VA_ARGS__) \
+    func(BtreeDelete, 20, 0, __VA_ARGS__)
 
 // Brie is disabled for now.
 #define FOR_EACH_BRIE(func, ...)
@@ -129,11 +138,11 @@ namespace souffle::interpreter {
     /* func(Brie, 20, __VA_ARGS__)   */
 
 #define FOR_EACH_EQREL(func, ...)\
-    func(Eqrel, 2, __VA_ARGS__)
+    func(Eqrel, 2, 0, __VA_ARGS__)
 
 #define FOR_EACH(func, ...)                 \
     FOR_EACH_BTREE(func, __VA_ARGS__)       \
-    FOR_EACH_BTREE_DELETE(func, __VA_ARGS__)       \
+    FOR_EACH_BTREE_DELETE(func, __VA_ARGS__)\
     FOR_EACH_BRIE(func, __VA_ARGS__)        \
     FOR_EACH_PROVENANCE(func, __VA_ARGS__)  \
     FOR_EACH_EQREL(func, __VA_ARGS__)
@@ -225,13 +234,6 @@ struct get_full_index<0> {
     using type = index<>;
 };
 
-// -- obtains a full provenance index for a given arity --
-template <unsigned arity>
-struct get_full_prov_index {
-    using type = typename extend<typename extend<typename get_full_index<arity - 2>::type, arity - 1>::type,
-            arity - 2>::type;
-};
-
 }  // namespace index_utils
 
 template <std::size_t Arity>
@@ -241,39 +243,64 @@ using t_tuple = typename souffle::Tuple<RamDomain, Arity>;
 template <std::size_t Arity>
 using comparator = typename index_utils::get_full_index<Arity>::type::comparator;
 
-template <std::size_t Arity>
-using prov_comparator = typename index_utils::get_full_prov_index<Arity>::type::comparator;
+// Updater
+template <std::size_t Arity, std::size_t AuxiliaryArity>
+struct Updater {
+    bool update(t_tuple<Arity>& old_t, const t_tuple<Arity>& new_t) {
+        bool changed = false;
+        // todo: expand for loop using templates
+        constexpr std::size_t firstAux = Arity - AuxiliaryArity - 1;
+        for (std::size_t i = firstAux; i < Arity; i++) {
+            if (old_t[i] != new_t[i]) {
+                changed = true;
+                old_t[i] = new_t[i];
+            }
+        }
+        return changed;
+    }
+};
 
-// Alias for btree_set
-template <std::size_t Arity>
-using Btree = btree_set<t_tuple<Arity>, comparator<Arity>>;
+// ProvenanceUpdater
+template <std::size_t Arity, std::size_t AuxiliaryArity>
+struct ProvenanceUpdater {
+    bool update(t_tuple<Arity>& old_t, const t_tuple<Arity>& new_t) {
+        constexpr std::size_t level = Arity - 1;
+        constexpr std::size_t rule = Arity - 2;
+        if (ramBitCast<RamSigned>(new_t[level]) < ramBitCast<RamSigned>(old_t[level]) ||
+                (ramBitCast<RamSigned>(new_t[level]) == ramBitCast<RamSigned>(old_t[level]) &&
+                        ramBitCast<RamSigned>(new_t[rule]) < ramBitCast<RamSigned>(old_t[rule]))) {
+            old_t[level] = new_t[level];
+            old_t[rule] = new_t[rule];
+            return true;
+        }
+        return false;
+    }
+};
 
 // Alias for btree_set
-template <std::size_t Arity>
-using BtreeDelete = btree_delete_set<t_tuple<Arity>, comparator<Arity>>;
+template <std::size_t Arity, std::size_t AuxiliaryArity>
+using Btree = btree_set<t_tuple<Arity>, comparator<Arity>, std::allocator<t_tuple<Arity>>, 256,
+        typename detail::default_strategy<t_tuple<Arity>>::type, comparator<Arity - AuxiliaryArity>,
+        Updater<Arity, AuxiliaryArity>>;
+
+// Alias for btree_delete_set
+template <std::size_t Arity, std::size_t AuxiliaryArity>
+using BtreeDelete = btree_delete_set<t_tuple<Arity>, comparator<Arity>, std::allocator<t_tuple<Arity>>, 256,
+        typename detail::default_strategy<t_tuple<Arity>>::type, comparator<Arity - AuxiliaryArity>,
+        Updater<Arity, AuxiliaryArity>>;
 
 // Alias for Trie
-template <std::size_t Arity>
+template <std::size_t Arity, std::size_t AuxiliaryArity>
 using Brie = Trie<Arity>;
 
-// Updater for Provenance
-template <std::size_t Arity>
-struct ProvenanceUpdater {
-    void update(t_tuple<Arity>& old_t, const t_tuple<Arity>& new_t) {
-        old_t[Arity - 2] = new_t[Arity - 2];
-        old_t[Arity - 1] = new_t[Arity - 1];
-    }
-};
-
-// Alias for Provenance
-template <std::size_t Arity>
-using Provenance = btree_set<t_tuple<Arity>, prov_comparator<Arity>, std::allocator<t_tuple<Arity>>, 256,
-        typename detail::default_strategy<t_tuple<Arity>>::type, comparator<Arity - 2>,
-        ProvenanceUpdater<Arity>>;
+template <std::size_t Arity, std::size_t AuxiliaryArity>
+using Provenance = btree_set<t_tuple<Arity>, comparator<Arity>, std::allocator<t_tuple<Arity>>, 256,
+        typename detail::default_strategy<t_tuple<Arity>>::type, comparator<Arity - AuxiliaryArity>,
+        ProvenanceUpdater<Arity, AuxiliaryArity>>;
 
 // Alias for Eqrel
 // Note: require Arity = 2.
-template <std::size_t Arity>
+template <std::size_t Arity, std::size_t AuxiliaryArity>
 using Eqrel = EquivalenceRelation<t_tuple<Arity>>;
 
 };  // namespace souffle::interpreter
diff --git a/src/interpreter/tests/interpreter_relation_test.cpp b/src/interpreter/tests/interpreter_relation_test.cpp
index b77d8dc32a8..4b788bb07e4 100644
--- a/src/interpreter/tests/interpreter_relation_test.cpp
+++ b/src/interpreter/tests/interpreter_relation_test.cpp
@@ -46,7 +46,7 @@ TEST(Relation0, Construction) {
     OrderCollection orders = {emptyOrder};
     IndexCluster indexSelection(mapping, searches, orders);
 
-    Relation<0, interpreter::Btree> rel(0, "test", indexSelection);
+    Relation<0, 0, interpreter::Btree> rel("test", indexSelection);
 
     souffle::Tuple<RamDomain, 0> tuple;
     // add some values
@@ -68,7 +68,7 @@ TEST(Relation0, Iteration) {
     OrderCollection orders = {emptyOrder};
     IndexCluster indexSelection(mapping, searches, orders);
 
-    Relation<0, interpreter::Btree> rel(0, "test", indexSelection);
+    Relation<0, 0, interpreter::Btree> rel("test", indexSelection);
     RelationWrapper* wrapper = &rel;
 
     souffle::Tuple<RamDomain, 0> tuple;
@@ -95,7 +95,7 @@ TEST(Relation1, Construction) {
     mapping.insert({existenceCheck, fullOrder});
     IndexCluster indexSelection(mapping, searches, orders);
 
-    Relation<1, interpreter::Btree> rel(0, "test", indexSelection);
+    Relation<1, 0, interpreter::Btree> rel("test", indexSelection);
     RelInterface relInt(rel, symbolTable, "test", {"i"}, {"i"}, 0);
 
     tuple d1(&relInt, {1});
@@ -124,7 +124,7 @@ TEST(Basic, Iteration) {
     mapping.insert({existenceCheck, fullOrder});
     IndexCluster indexSelection(mapping, searches, orders);
 
-    Relation<1, interpreter::Btree> rel(0, "test", indexSelection);
+    Relation<1, 0, interpreter::Btree> rel("test", indexSelection);
     RelInterface relInt(rel, symbolTable, "test", {"i"}, {"i"}, 0);
 
     // add some values
@@ -159,7 +159,7 @@ TEST(Independence, Iteration) {
     mapping.insert({existenceCheck, fullOrder});
     IndexCluster indexSelection(mapping, searches, orders);
 
-    Relation<1, interpreter::Btree> rel(0, "test", indexSelection);
+    Relation<1, 0, interpreter::Btree> rel("test", indexSelection);
     RelInterface relInt(rel, symbolTable, "test", {"i"}, {"i"}, 0);
 
     // add a value
@@ -195,7 +195,7 @@ TEST(IndependentMoving, Iteration) {
     mapping.insert({existenceCheck, fullOrder});
     IndexCluster indexSelection(mapping, searches, orders);
 
-    Relation<1, interpreter::Btree> rel(0, "test", indexSelection);
+    Relation<1, 0, interpreter::Btree> rel("test", indexSelection);
     RelInterface relInt(rel, symbolTable, "test", {"i"}, {"i"}, 0);
 
     // add a value
@@ -226,7 +226,7 @@ TEST(IndependentCopying, Iteration) {
     mapping.insert({existenceCheck, fullOrder});
     IndexCluster indexSelection(mapping, searches, orders);
 
-    Relation<1, interpreter::Btree> rel(0, "test", indexSelection);
+    Relation<1, 0, interpreter::Btree> rel("test", indexSelection);
     RelInterface relInt(rel, symbolTable, "test", {"i"}, {"i"}, 0);
 
     // add a value
@@ -258,7 +258,7 @@ TEST(Reordering, Iteration) {
     mapping.insert({existenceCheck, fullOrder});
     IndexCluster indexSelection(mapping, searches, orders);
 
-    Relation<3, interpreter::Btree> rel(0, "test", indexSelection);
+    Relation<3, 0, interpreter::Btree> rel("test", indexSelection);
     souffle::Tuple<RamDomain, 3> tuple{0, 1, 2};
     rel.insert(tuple);
 
diff --git a/src/parser/Helper.h b/src/parser/Helper.h
index 658c5eaac30..dc554ca6082 100644
--- a/src/parser/Helper.h
+++ b/src/parser/Helper.h
@@ -17,6 +17,7 @@
 #pragma once
 
 #include <cstddef>
+#include <map>
 #include <utility>
 #include <vector>
 
@@ -153,6 +154,34 @@ struct Mov<std::vector<A>> {
         return value.empty();
     }
 };
+
+template <typename K, typename V>
+struct Mov<std::map<K, V>> {
+    mutable std::map<K, V> value;
+
+    Mov() = default;
+    Mov(Mov&&) = default;
+    template <typename B>
+    Mov(B value) : value(std::move(value)) {}
+
+    // CRIMES AGAINST COMPUTING HAPPENS HERE
+    // HACK: Pretend you can copy it, but actually move it. Keeps Bison 3.0.2 happy.
+    Mov(const Mov& x) : value(std::move(x.value)) {}
+    Mov& operator=(Mov x) {
+        value = std::move(x.value);
+        return *this;
+    }
+
+    // detach/convert implicitly.
+    operator std::map<K, V>() {
+        return std::move(value);
+    }
+
+    void emplace(std::pair<K, V> p) {
+        value.emplace(std::make_pair(p.first, std::move(p.second)));
+    }
+};
+
 }  // namespace parser
 
 template <typename A>
diff --git a/src/parser/ParserDriver.cpp b/src/parser/ParserDriver.cpp
index 7d28fede85f..28aa8ecc6e2 100644
--- a/src/parser/ParserDriver.cpp
+++ b/src/parser/ParserDriver.cpp
@@ -245,6 +245,21 @@ void ParserDriver::addType(Own<ast::Type> type) {
     }
 }
 
+void ParserDriver::addLattice(Own<ast::Lattice> lattice) {
+    ast::Program& program = translationUnit->getProgram();
+    const auto& name = lattice->getQualifiedName();
+    auto* existingLattice = getIf(program.getLattices(),
+            [&](const ast::Lattice* current) { return current->getQualifiedName() == name; });
+    if (existingLattice != nullptr) {
+        Diagnostic err(Diagnostic::Type::ERROR,
+                DiagnosticMessage("Redefinition of lattice " + toString(name), lattice->getSrcLoc()),
+                {DiagnosticMessage("Previous definition", existingLattice->getSrcLoc())});
+        translationUnit->getErrorReport().addDiagnostic(err);
+    } else {
+        program.addLattice(std::move(lattice));
+    }
+}
+
 void ParserDriver::addClause(Own<ast::Clause> c) {
     ast::Program& program = translationUnit->getProgram();
     program.addClause(std::move(c));
diff --git a/src/parser/ParserDriver.h b/src/parser/ParserDriver.h
index d2c2bc3aafd..2f4924e4dff 100644
--- a/src/parser/ParserDriver.h
+++ b/src/parser/ParserDriver.h
@@ -24,6 +24,7 @@
 #include "ast/Counter.h"
 #include "ast/Directive.h"
 #include "ast/FunctorDeclaration.h"
+#include "ast/Lattice.h"
 #include "ast/Pragma.h"
 #include "ast/QualifiedName.h"
 #include "ast/Relation.h"
@@ -54,6 +55,7 @@ class ParserDriver {
     void addType(Own<ast::Type> type);
     void addClause(Own<ast::Clause> c);
     void addComponent(Own<ast::Component> c);
+    void addLattice(Own<ast::Lattice> l);
     void addInstantiation(Own<ast::ComponentInit> ci);
     void addPragma(Own<ast::Pragma> p);
 
diff --git a/src/parser/parser.yy b/src/parser/parser.yy
index 73942f7943a..82f0a0898e3 100644
--- a/src/parser/parser.yy
+++ b/src/parser/parser.yy
@@ -60,6 +60,7 @@
     #include "ast/FunctorDeclaration.h"
     #include "ast/IntrinsicFunctor.h"
     #include "ast/IterationCounter.h"
+    #include "ast/Lattice.h"
     #include "ast/Literal.h"
     #include "ast/NilConstant.h"
     #include "ast/NumericConstant.h"
@@ -87,6 +88,7 @@
     #include <ostream>
     #include <string>
     #include <vector>
+    #include <map>
 
     using namespace souffle;
 
@@ -165,10 +167,12 @@
 %token INPUT_DECL                "input directives declaration"
 %token OUTPUT_DECL               "output directives declaration"
 %token DEBUG_DELTA               "debug_delta"
+%token UNIQUE                    "unique"
 %token PRINTSIZE_DECL            "printsize directives declaration"
 %token LIMITSIZE_DECL            "limitsize directives declaration"
 %token OVERRIDE                  "override rules of super-component"
 %token TYPE                      "type declaration"
+%token LATTICE                   "lattice declaration"
 %token COMPONENT                 "component declaration"
 %token INSTANTIATE               "component instantiation"
 %token NUMBER_TYPE               "numeric type declaration"
@@ -214,6 +218,7 @@
 %token LE                        "<="
 %token GE                        ">="
 %token NE                        "!="
+%token MAPSTO                    "->"
 %token BW_AND                    "band"
 %token BW_OR                     "bor"
 %token BW_XOR                    "bxor"
@@ -283,7 +288,9 @@
 %type <Mov<std::vector<ast::QualifiedName>>>   union_type_list
 %type <Mov<VecOwn<ast::BranchType>>>    adt_branch_list
 %type <Mov<Own<ast::BranchType>>>       adt_branch
-
+%type <Mov<Own<ast::Lattice>>>                 lattice_decl
+%type <Mov<std::pair<ast::LatticeOperator, Own<ast::Argument>>>>                 lattice_operator
+%type <Mov<std::map<ast::LatticeOperator, Own<ast::Argument>>>>      lattice_operator_list
 /* -- Operator precedence -- */
 %left L_OR
 %left L_XOR
@@ -345,6 +352,10 @@ unit
     {
       driver.addType($type_decl);
     }
+  | unit lattice_decl
+    {
+      driver.addLattice($lattice_decl);
+    }
   | unit functor_decl
     {
       driver.addFunctorDeclaration($functor_decl);
@@ -460,6 +471,37 @@ adt_branch
     }
   ;
 
+/**
+ * Lattice Declarations
+ */
+
+lattice_decl
+  : LATTICE IDENT[name] LT GT LBRACE lattice_operator_list RBRACE
+    {
+      $$ = mk<ast::Lattice>($name, std::move($lattice_operator_list), @$);
+    }
+
+lattice_operator_list
+  :  lattice_operator COMMA lattice_operator_list
+    {
+      $$ = $3;
+      $$.emplace($lattice_operator);
+    }
+  | lattice_operator
+    {
+      $$.emplace($lattice_operator);
+    }
+
+lattice_operator
+  : IDENT MAPSTO arg
+    {
+      auto op = ast::latticeOperatorFromString($IDENT);
+      if (!op.has_value()) {
+        driver.error(@$, "Lattice operator not recognized");
+      }
+      $$ = std::make_pair(op.value(), std::move($arg));
+    }
+
 /**
  * Relations
  */
@@ -553,6 +595,10 @@ attribute
     {
       $$ = mk<ast::Attribute>($name, $type, @type);
     }
+  | IDENT[name] COLON qualified_name[type] LT GT
+    {
+      $$ = mk<ast::Attribute>($name, $type, true, @type);
+    }
   ;
 
 /**
@@ -1351,6 +1397,11 @@ component_body
       $$ = $1;
       $$->addType($2);
     }
+  | component_body lattice_decl
+    {
+      $$ = $1;
+      $$->addLattice($2);
+    }
   | component_body relation_decl
     {
       $$ = $1;
diff --git a/src/parser/scanner.ll b/src/parser/scanner.ll
index 025a507d126..4cca18e4f97 100644
--- a/src/parser/scanner.ll
+++ b/src/parser/scanner.ll
@@ -147,6 +147,7 @@ WS [ \t\r\v\f]
 ".override"/{WS}                      { return yy::parser::make_OVERRIDE(yylloc); }
 ".pragma"/{WS}                        { return yy::parser::make_PRAGMA(yylloc); }
 ".plan"/{WS}                          { return yy::parser::make_PLAN(yylloc); }
+".lattice"/{WS}                       { return yy::parser::make_LATTICE(yylloc); }
 ".include"                            {
                                         yyinfo.LastIncludeDirectiveLoc = yylloc;
                                         BEGIN(INCLUDE);
@@ -240,6 +241,7 @@ WS [ \t\r\v\f]
 "]"                                   { return yy::parser::make_RBRACKET(yylloc); }
 "$"                                   { return yy::parser::make_DOLLAR(yylloc); }
 "+"                                   { return yy::parser::make_PLUS(yylloc); }
+"->"                                  { return yy::parser::make_MAPSTO(yylloc); }
 "-"                                   { return yy::parser::make_MINUS(yylloc); }
 "("                                   { return yy::parser::make_LPAREN(yylloc); }
 ")"                                   { return yy::parser::make_RPAREN(yylloc); }
diff --git a/src/ram/Relation.h b/src/ram/Relation.h
index 2dbf6b77ff6..4da66151320 100644
--- a/src/ram/Relation.h
+++ b/src/ram/Relation.h
@@ -16,6 +16,7 @@
 #pragma once
 
 #include "RelationTag.h"
+#include "ram/AbstractOperator.h"
 #include "ram/Node.h"
 #include "souffle/utility/ContainerUtil.h"
 #include "souffle/utility/MiscUtil.h"
diff --git a/src/ram/transform/MakeIndex.cpp b/src/ram/transform/MakeIndex.cpp
index 7f60a83aac4..c40cd9c07eb 100644
--- a/src/ram/transform/MakeIndex.cpp
+++ b/src/ram/transform/MakeIndex.cpp
@@ -88,12 +88,13 @@ ExpressionPair MakeIndexTransformer::getExpressionPair(
 // Retrieves the <expr1> <= Tuple[level, element] <= <expr2> part of the constraint as a pair { <expr1>,
 // <expr2> }
 ExpressionPair MakeIndexTransformer::getLowerUpperExpression(Condition* c, std::size_t& element,
-        const std::optional<std::size_t>& identifier, RelationRepresentation rep) {
+        const std::optional<std::size_t>& identifier, const ram::Relation& rel) {
     if (auto* binRelOp = as<Constraint>(c)) {
         const bool interpreter = !glb->config().has("compile") && !glb->config().has("dl-program") &&
                                  !glb->config().has("generate") && !glb->config().has("generate-many") &&
                                  !glb->config().has("swig");
-        bool provenance = rep == RelationRepresentation::PROVENANCE;
+        bool provenance = rel.getAuxiliaryArity() > 0;  // rep == RelationRepresentation::PROVENANCE;
+        auto rep = rel.getRepresentation();
         bool btree = (rep == RelationRepresentation::BTREE || rep == RelationRepresentation::DEFAULT ||
                       rep == RelationRepresentation::BTREE_DELETE);
         auto op = binRelOp->getOperator();
@@ -139,9 +140,8 @@ ExpressionPair MakeIndexTransformer::getLowerUpperExpression(Condition* c, std::
     return {mk<UndefValue>(), mk<UndefValue>()};
 }
 
-Own<Condition> MakeIndexTransformer::constructPattern(const std::vector<std::string>& attributeTypes,
-        RamPattern& queryPattern, bool& indexable, VecOwn<Condition> conditionList, std::size_t identifier,
-        RelationRepresentation rep) {
+Own<Condition> MakeIndexTransformer::constructPattern(const ram::Relation& rel, RamPattern& queryPattern,
+        bool& indexable, VecOwn<Condition> conditionList, std::size_t identifier) {
     // Remaining conditions which cannot be handled by an index
     Own<Condition> condition;
     auto addCondition = [&](Own<Condition> c) {
@@ -286,7 +286,7 @@ Own<Condition> MakeIndexTransformer::constructPattern(const std::vector<std::str
         Own<Expression> lowerExpression;
         Own<Expression> upperExpression;
         std::tie(lowerExpression, upperExpression) =
-                getLowerUpperExpression(cond.get(), element, identifier, rep);
+                getLowerUpperExpression(cond.get(), element, identifier, rel);
 
         // we have new bounds if at least one is defined
         if (!isUndefValue(lowerExpression.get()) || !isUndefValue(upperExpression.get())) {
@@ -313,7 +313,7 @@ Own<Condition> MakeIndexTransformer::constructPattern(const std::vector<std::str
                 continue;
             }
 
-            auto type = attributeTypes[element];
+            auto type = rel.getAttributeTypes()[element];
             indexable = true;
             if (firstConstraint) {
                 // equality
@@ -414,8 +414,8 @@ Own<Operation> MakeIndexTransformer::rewriteAggregate(const Aggregate* agg) {
         }
 
         bool indexable = false;
-        Own<Condition> condition = constructPattern(rel.getAttributeTypes(), queryPattern, indexable,
-                toConjunctionList(&agg->getCondition()), identifier, rel.getRepresentation());
+        Own<Condition> condition = constructPattern(
+                rel, queryPattern, indexable, toConjunctionList(&agg->getCondition()), identifier);
         if (indexable) {
             return mk<IndexAggregate>(clone(agg->getOperation()), clone(agg->getAggregator()),
                     agg->getRelation(), clone(agg->getExpression()), std::move(condition),
@@ -436,8 +436,8 @@ Own<Operation> MakeIndexTransformer::rewriteScan(const Scan* scan) {
         }
 
         bool indexable = false;
-        Own<Condition> condition = constructPattern(rel.getAttributeTypes(), queryPattern, indexable,
-                toConjunctionList(&filter->getCondition()), identifier, rel.getRepresentation());
+        Own<Condition> condition = constructPattern(
+                rel, queryPattern, indexable, toConjunctionList(&filter->getCondition()), identifier);
         if (indexable) {
             Own<Operation> op = clone(filter->getOperation());
             if (!isTrue(condition.get())) {
@@ -461,8 +461,8 @@ Own<Operation> MakeIndexTransformer::rewriteIndexScan(const IndexScan* iscan) {
 
         bool indexable = false;
         // strengthen the pattern with construct pattern
-        Own<Condition> condition = constructPattern(rel.getAttributeTypes(), strengthenedPattern, indexable,
-                toConjunctionList(&filter->getCondition()), identifier, rel.getRepresentation());
+        Own<Condition> condition = constructPattern(
+                rel, strengthenedPattern, indexable, toConjunctionList(&filter->getCondition()), identifier);
 
         if (indexable) {
             // Merge Index Pattern here
diff --git a/src/ram/transform/MakeIndex.h b/src/ram/transform/MakeIndex.h
index 96cb4237521..4c3508510bf 100644
--- a/src/ram/transform/MakeIndex.h
+++ b/src/ram/transform/MakeIndex.h
@@ -82,7 +82,7 @@ class MakeIndexTransformer : public Transformer {
     ExpressionPair getExpressionPair(
             const Constraint* binRelOp, std::size_t& element, const std::optional<std::size_t>& identifier);
     ExpressionPair getLowerUpperExpression(Condition* c, std::size_t& element,
-            const std::optional<std::size_t>& level, RelationRepresentation rep);
+            const std::optional<std::size_t>& level, const ram::Relation& rel);
 
     /**
      * @param AttributeTypes to indicate type of each attribute in the relation
@@ -93,9 +93,8 @@ class MakeIndexTransformer : public Transformer {
      * @param RelationRepresentation identifying the data structure
      * @result Remaining conditions that could not be transformed to an index
      */
-    Own<Condition> constructPattern(const std::vector<std::string>& attributeTypes, RamPattern& queryPattern,
-            bool& indexable, VecOwn<Condition> conditionList, std::size_t identifier,
-            RelationRepresentation rep);
+    Own<Condition> constructPattern(const ram::Relation& rel, RamPattern& queryPattern, bool& indexable,
+            VecOwn<Condition> conditionList, std::size_t identifier);
 
     /**
      * @brief Rewrite a scan operation to an indexed scan operation
diff --git a/src/reports/ErrorReport.h b/src/reports/ErrorReport.h
index 5f3c2ee0f3a..a9294cd2cd3 100644
--- a/src/reports/ErrorReport.h
+++ b/src/reports/ErrorReport.h
@@ -149,6 +149,7 @@ enum class WarnType : std::size_t {
     DeprecatedTypeDecl,
     DeprecatedQualifier,
     DollarSign,
+    LatticeMissingOperator,
     NoRulesNorFacts,
     NoSubsumptiveRule,
     // This last element is used as the size parameter to std::bitset in the
diff --git a/src/synthesiser/Relation.cpp b/src/synthesiser/Relation.cpp
index 5924e5f3737..27a12a66911 100644
--- a/src/synthesiser/Relation.cpp
+++ b/src/synthesiser/Relation.cpp
@@ -48,15 +48,16 @@ Own<Relation> Relation::getSynthesiserRelation(
         const ram::Relation& ramRel, const ram::analysis::IndexCluster& indexSelection) {
     Relation* rel;
 
+    bool hasProvenance = ramRel.getArity() > 0 && ramRel.getAttributeNames().back() == "@level_number";
     // Handle the qualifier in souffle code
-    if (ramRel.getRepresentation() == RelationRepresentation::PROVENANCE) {
-        rel = new DirectRelation(ramRel, indexSelection, true, false);
+    if (ramRel.getAuxiliaryArity() > 0) {
+        rel = new DirectRelation(ramRel, indexSelection, true, hasProvenance, false);
     } else if (ramRel.isNullary()) {
         rel = new NullaryRelation(ramRel, indexSelection);
     } else if (ramRel.getRepresentation() == RelationRepresentation::BTREE) {
-        rel = new DirectRelation(ramRel, indexSelection, false, false);
+        rel = new DirectRelation(ramRel, indexSelection, false, false, false);
     } else if (ramRel.getRepresentation() == RelationRepresentation::BTREE_DELETE) {
-        rel = new DirectRelation(ramRel, indexSelection, false, true);
+        rel = new DirectRelation(ramRel, indexSelection, false, false, true);
     } else if (ramRel.getRepresentation() == RelationRepresentation::BRIE) {
         rel = new BrieRelation(ramRel, indexSelection);
     } else if (ramRel.getRepresentation() == RelationRepresentation::EQREL) {
@@ -68,7 +69,7 @@ Own<Relation> Relation::getSynthesiserRelation(
         if (ramRel.getArity() > 6) {
             rel = new IndirectRelation(ramRel, indexSelection);
         } else {
-            rel = new DirectRelation(ramRel, indexSelection, false, false);
+            rel = new DirectRelation(ramRel, indexSelection, false, false, false);
         }
     }
 
@@ -137,7 +138,7 @@ void DirectRelation::computeIndices() {
         // we must expand all search orders to be full indices,
         // since weak/strong comparators and updaters need this,
         // and also add provenance annotations to the indices
-        if (isProvenance || hasErase) {
+        if (hasAuxiliary || hasErase) {
             // expand index to be full
             for (std::size_t i = 0; i < getArity() - relation.getAuxiliaryArity(); i++) {
                 if (curIndexElems.find(i) == curIndexElems.end()) {
@@ -145,21 +146,18 @@ void DirectRelation::computeIndices() {
                 }
             }
 
-            if (isProvenance) {
+            if (hasAuxiliary) {
                 // remove any provenance annotations already in the index order
-                if (curIndexElems.find(getArity() - relation.getAuxiliaryArity() + 1) !=
-                        curIndexElems.end()) {
-                    ind.erase(
-                            std::find(ind.begin(), ind.end(), getArity() - relation.getAuxiliaryArity() + 1));
+                std::size_t n = getArity() - relation.getAuxiliaryArity();
+                for (std::size_t i = n; i < getArity(); i++) {
+                    if (curIndexElems.find(i) != curIndexElems.end()) {
+                        ind.erase(std::find(ind.begin(), ind.end(), i));
+                    }
                 }
-
-                if (curIndexElems.find(getArity() - relation.getAuxiliaryArity()) != curIndexElems.end()) {
-                    ind.erase(std::find(ind.begin(), ind.end(), getArity() - relation.getAuxiliaryArity()));
-                }
-
                 // add provenance annotations to the index, but in reverse order
-                ind.push_back(getArity() - relation.getAuxiliaryArity() + 1);
-                ind.push_back(getArity() - relation.getAuxiliaryArity());
+                for (std::size_t i = getArity(); i > n; i--) {
+                    ind.push_back(i - 1);
+                }
             }
             masterIndex = 0;
         } else if (ind.size() == getArity()) {
@@ -182,11 +180,8 @@ std::string DirectRelation::getTypeNamespace() {
     }
 
     std::stringstream res;
-    if (hasErase) {
-        res << "t_btree_delete_";
-    } else {
-        res << "t_btree_";
-    }
+    res << "t_btree_";
+    res << hasErase << hasAuxiliary << hasProvenance << "_";
     res << getTypeAttributeString(relation.getAttributeTypes(), attributesUsed);
 
     for (auto& ind : getIndices()) {
@@ -233,13 +228,33 @@ void DirectRelation::generateTypeStruct(GenDb& db) {
     decl << "using t_tuple = Tuple<RamDomain, " << arity << ">;\n";
 
     // generate an updater class for provenance
-    if (isProvenance) {
+    if (hasAuxiliary) {
         decl << "struct updater {\n";
-        decl << "void update(t_tuple& old_t, const t_tuple& new_t) {\n";
-
-        for (std::size_t i = arity - auxiliaryArity; i < arity; i++) {
-            decl << "old_t[" << i << "] = new_t[" << i << "];\n";
+        decl << "bool update(t_tuple& old_t, const t_tuple& new_t) {\n";
+        decl << "bool changed = false;\n";
+        if (hasProvenance) {
+            assert(auxiliaryArity == 2);
+            auto rule = arity - 2;
+            auto level = arity - 1;
+            decl << "if (ramBitCast<RamSigned>(new_t[" << level << "]) < ramBitCast<RamSigned>(old_t["
+                 << level << "])"
+                 << " || (ramBitCast<RamSigned>(new_t[" << level << "]) == ramBitCast<RamSigned>(old_t["
+                 << level << "])"
+                 << " && ramBitCast<RamSigned>(new_t[" << rule << "]) < ramBitCast<RamSigned>(old_t[" << rule
+                 << "]))) {\n";
+            decl << "    old_t[" << rule << "] = new_t[" << rule << "];\n";
+            decl << "    old_t[" << level << "] = new_t[" << level << "];\n";
+            decl << "    changed = true;\n";
+            decl << "}\n";
+        } else {
+            for (std::size_t i = arity - auxiliaryArity; i < arity; i++) {
+                decl << "if (old_t[" << i << "] != new_t[" << i << "]) {\n";
+                decl << "    changed = true;\n";
+                decl << "    old_t[" << i << "] = new_t[" << i << "];\n";
+                decl << "}\n";
+            }
         }
+        decl << "return changed;\n";
 
         decl << "}\n";
         decl << "};\n";
@@ -324,7 +339,7 @@ void DirectRelation::generateTypeStruct(GenDb& db) {
         // for provenance, all indices must be full so we use btree_set
         // also strong/weak comparators and updater methods
 
-        if (isProvenance) {
+        if (hasAuxiliary) {
             std::string comparator_aux;
             if (provenanceIndexNumbers.find(i) == provenanceIndexNumbers.end()) {
                 // index for bottom up phase
diff --git a/src/synthesiser/Relation.h b/src/synthesiser/Relation.h
index 255b752a294..c38f36434ee 100644
--- a/src/synthesiser/Relation.h
+++ b/src/synthesiser/Relation.h
@@ -115,8 +115,9 @@ class InfoRelation : public Relation {
 class DirectRelation : public Relation {
 public:
     DirectRelation(const ram::Relation& ramRel, const ram::analysis::IndexCluster& indexSelection,
-            bool isProvenance, bool hasErase)
-            : Relation(ramRel, indexSelection), isProvenance(isProvenance), hasErase(hasErase) {}
+            bool hasAuxiliary, bool hasProvenance, bool hasErase)
+            : Relation(ramRel, indexSelection), hasAuxiliary(hasAuxiliary), hasProvenance(hasProvenance),
+              hasErase(hasErase) {}
 
     void computeIndices() override;
     std::string getTypeNamespace();
@@ -124,7 +125,8 @@ class DirectRelation : public Relation {
     void generateTypeStruct(GenDb& db) override;
 
 private:
-    const bool isProvenance;
+    const bool hasAuxiliary;
+    const bool hasProvenance;
     const bool hasErase;
 };
 
diff --git a/src/synthesiser/Synthesiser.cpp b/src/synthesiser/Synthesiser.cpp
index 44bf3f2977a..cf26e0aafdf 100644
--- a/src/synthesiser/Synthesiser.cpp
+++ b/src/synthesiser/Synthesiser.cpp
@@ -1200,7 +1200,7 @@ void Synthesiser::emitCode(std::ostream& out, const Statement& stmt) {
                     default: return false;
                 }
             } else if (isA<ram::UserDefinedAggregator>(aggregator)) {
-                return false;
+                return true;
             }
             fatal("Unhandled aggregate operation");
         }
diff --git a/tests/interface/CMakeLists.txt b/tests/interface/CMakeLists.txt
index 2b52bc3e30b..d4770d53b39 100644
--- a/tests/interface/CMakeLists.txt
+++ b/tests/interface/CMakeLists.txt
@@ -9,6 +9,9 @@ add_subdirectory(aggregates)
 add_subdirectory(functors)
 add_subdirectory(graph_coloring)
 add_subdirectory(pathseq)
+add_subdirectory(lattice1)
+add_subdirectory(lattice2)
+add_subdirectory(lattice3)
 
 # swig test which will run python, java or both
 function(SOUFFLE_POSITIVE_FUNCTOR_TEST TEST_NAME)
@@ -159,6 +162,9 @@ souffle_positive_functor_test(aggregates CATEGORY interface)
 souffle_positive_functor_test(functors CATEGORY interface)
 souffle_positive_functor_test(pathseq CATEGORY interface)
 souffle_positive_functor_test(graph_coloring CATEGORY interface)
+souffle_positive_functor_test(lattice1 CATEGORY interface)
+souffle_positive_functor_test(lattice2 CATEGORY interface)
+souffle_positive_functor_test(lattice3 CATEGORY interface)
 souffle_positive_cpp_test(contain_insert)
 souffle_positive_cpp_test(get_symboltabletype)
 souffle_positive_cpp_test(insert_for)
diff --git a/tests/interface/lattice1/CMakeLists.txt b/tests/interface/lattice1/CMakeLists.txt
new file mode 100644
index 00000000000..6de0382c4d2
--- /dev/null
+++ b/tests/interface/lattice1/CMakeLists.txt
@@ -0,0 +1,43 @@
+# Souffle - A Datalog Compiler
+# Copyright (c) 2022 The Souffle Developers. All rights reserved
+# Licensed under the Universal Permissive License v 1.0 as shown at:
+# - https://opensource.org/licenses/UPL
+# - <souffle root>/licenses/SOUFFLE-UPL.txt
+
+add_library(lattice1functors SHARED functors.cpp)
+target_include_directories(lattice1functors PRIVATE "${CMAKE_SOURCE_DIR}/src/include")
+
+target_compile_features(lattice1functors
+                        PUBLIC cxx_std_17)
+
+set_target_properties(lattice1functors PROPERTIES CXX_EXTENSIONS OFF)
+set_target_properties(lattice1functors PROPERTIES OUTPUT_NAME "functors")
+set_target_properties(lattice1functors PROPERTIES WINDOWS_EXPORT_ALL_SYMBOLS ON)
+
+if (OPENMP_FOUND)
+    target_link_libraries(lattice1functors PUBLIC OpenMP::OpenMP_CXX)
+endif()
+
+if (Threads_FOUND)
+  target_link_libraries(lattice1functors PUBLIC Threads::Threads)
+endif ()
+
+if (NOT MSVC)
+target_compile_options(lattice1functors
+                       PUBLIC "-Wall;-Wextra;-Werror;-fwrapv")
+else ()
+  target_compile_options(lattice1functors PUBLIC /W3 /WX)
+endif()
+
+if (WIN32)
+  # Prefix all shared libraries with 'lib'.
+  set(CMAKE_SHARED_LIBRARY_PREFIX "lib")
+
+  # Prefix all static libraries with 'lib'.
+  set(CMAKE_STATIC_LIBRARY_PREFIX "lib")
+endif ()
+
+if (SOUFFLE_DOMAIN_64BIT)
+    target_compile_definitions(lattice1functors
+                               PUBLIC RAM_DOMAIN_SIZE=64)
+endif()
diff --git a/tests/interface/lattice1/Values.csv b/tests/interface/lattice1/Values.csv
new file mode 100644
index 00000000000..16c75e9b56e
--- /dev/null
+++ b/tests/interface/lattice1/Values.csv
@@ -0,0 +1,8 @@
+start	v	$I($Cst(0), $Cst(0))
+start_to_head	v	$I($Cst(0), $Cst(0))
+head	v	$I($Cst(0), $Cst(102))
+cond	v	$I($Cst(0), $Cst(100))
+incr	v	$I($Cst(2), $Cst(102))
+incr_to_head	v	$I($Cst(2), $Cst(102))
+not cond	v	$I($Cst(101), $Cst(102))
+end	v	$I($Cst(101), $Cst(102))
diff --git a/tests/interface/lattice1/functors.cpp b/tests/interface/lattice1/functors.cpp
new file mode 100644
index 00000000000..0705f98c0a7
--- /dev/null
+++ b/tests/interface/lattice1/functors.cpp
@@ -0,0 +1,137 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023, The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file functors.cpp
+ *
+ ***********************************************************************/
+
+#include "souffle/RecordTable.h"
+#include "souffle/SymbolTable.h"
+#include <cassert>
+
+extern "C" {
+
+enum Z { Cst = 0, Inf, MinusInf };
+enum Interval { Bottom = 0, I };
+
+souffle::RamDomain minZ(souffle::RecordTable* recordTable, souffle::RamDomain arg1, souffle::RamDomain arg2) {
+    const souffle::RamDomain* t1 = recordTable->unpack(arg1, 2);
+    const souffle::RamDomain* t2 = recordTable->unpack(arg2, 2);
+    if (t1[0] == MinusInf) {
+        return arg1;
+    }
+    if (t2[0] == MinusInf) {
+        return arg2;
+    }
+    if (t1[0] == Inf) {
+        return arg2;
+    }
+    if (t2[0] == Inf) {
+        return arg1;
+    }
+    if (t2[1] < t1[1]) {
+        return arg2;
+    }
+    return arg1;
+}
+
+souffle::RamDomain maxZ(souffle::RecordTable* recordTable, souffle::RamDomain arg1, souffle::RamDomain arg2) {
+    const souffle::RamDomain* t1 = recordTable->unpack(arg1, 2);
+    const souffle::RamDomain* t2 = recordTable->unpack(arg2, 2);
+    if (t1[0] == MinusInf) {
+        return arg2;
+    }
+    if (t2[0] == MinusInf) {
+        return arg1;
+    }
+    if (t1[0] == Inf) {
+        return arg1;
+    }
+    if (t2[0] == Inf) {
+        return arg2;
+    }
+    if (t2[1] < t1[1]) {
+        return arg1;
+    }
+    return arg2;
+}
+
+souffle::RamDomain plusZ(souffle::RecordTable* recordTable, souffle::RamDomain arg, souffle::RamDomain x) {
+    const souffle::RamDomain* t = recordTable->unpack(arg, 2);
+    if (t[0] == MinusInf || t[0] == Inf) {
+        return arg;
+    }
+
+    const souffle::RamDomain res[2] = {Cst, t[1] + x};
+    return recordTable->pack(res, 2);
+}
+
+souffle::RamDomain lub(souffle::SymbolTable*, souffle::RecordTable* recordTable, souffle::RamDomain arg1,
+        souffle::RamDomain arg2) {
+    const souffle::RamDomain* a1 = recordTable->unpack(arg1, 2);
+    const souffle::RamDomain* a2 = recordTable->unpack(arg2, 2);
+
+    if (a1[0] == Bottom) return arg2;
+    if (a2[0] == Bottom) return arg1;
+
+    const souffle::RamDomain* t1 = recordTable->unpack(a1[1], 2);
+    const souffle::RamDomain* t2 = recordTable->unpack(a2[1], 2);
+
+    const auto lb = minZ(recordTable, t1[0], t2[0]);
+    const auto ub = maxZ(recordTable, t1[1], t2[1]);
+
+    const souffle::RamDomain res[2] = {lb, ub};
+    const souffle::RamDomain interval[2] = {I, recordTable->pack(res, 2)};
+    return recordTable->pack(interval, 2);
+}
+
+souffle::RamDomain glb(souffle::SymbolTable*, souffle::RecordTable* recordTable, souffle::RamDomain arg1,
+        souffle::RamDomain arg2) {
+    const souffle::RamDomain* a1 = recordTable->unpack(arg1, 2);
+    const souffle::RamDomain* a2 = recordTable->unpack(arg2, 2);
+
+    if (a1[0] == Bottom) return arg1;
+    if (a2[0] == Bottom) return arg2;
+
+    const souffle::RamDomain* t1 = recordTable->unpack(a1[1], 2);
+    const souffle::RamDomain* t2 = recordTable->unpack(a2[1], 2);
+
+    const auto lb = maxZ(recordTable, t1[0], t2[0]);
+    const auto ub = minZ(recordTable, t1[1], t2[1]);
+
+    const souffle::RamDomain* lower = recordTable->unpack(lb, 2);
+    const souffle::RamDomain* upper = recordTable->unpack(ub, 2);
+    if (lower[0] == Cst && upper[0] == Cst && lower[1] > upper[1]) {
+        // bottom
+        const souffle::RamDomain bottom[2] = {Bottom, 1};
+        return recordTable->pack(bottom, 2);
+    }
+
+    const souffle::RamDomain res[2] = {lb, ub};
+    const souffle::RamDomain interval[2] = {I, recordTable->pack(res, 2)};
+    return recordTable->pack(interval, 2);
+}
+
+souffle::RamDomain incr(souffle::SymbolTable*, souffle::RecordTable* recordTable, souffle::RamDomain arg,
+        souffle::RamDomain x) {
+    const souffle::RamDomain* a = recordTable->unpack(arg, 2);
+
+    if (a[0] == Bottom) return arg;
+    const souffle::RamDomain* t = recordTable->unpack(a[1], 2);
+
+    const auto lb = plusZ(recordTable, t[0], x);
+    const auto ub = plusZ(recordTable, t[1], x);
+
+    const souffle::RamDomain res[2] = {lb, ub};
+    const souffle::RamDomain interval[2] = {I, recordTable->pack(res, 2)};
+    return recordTable->pack(interval, 2);
+}
+
+}  // end of extern "C"
diff --git a/tests/interface/lattice1/lattice1.dl b/tests/interface/lattice1/lattice1.dl
new file mode 100644
index 00000000000..a4ff7878be6
--- /dev/null
+++ b/tests/interface/lattice1/lattice1.dl
@@ -0,0 +1,79 @@
+// Souffle - A Datalog Compiler
+// Copyright (c) 2023, The Souffle Developers. All rights reserved
+// Licensed under the Universal Permissive License v 1.0 as shown at:
+// - https://opensource.org/licenses/UPL
+// - <souffle root>/licenses/SOUFFLE-UPL.txt
+
+
+.type Z = Cst{n:number} | Inf{} | MinusInf{}
+.type Interval = Bottom{} | I{lb:Z, ub:Z}
+
+.functor lub(a:Interval, b:Interval):Interval stateful
+.functor glb(a:Interval, b:Interval):Interval stateful
+.functor incr(i:Interval, x:number):Interval stateful
+
+.lattice Interval<> {
+    Bottom -> $Bottom(),
+    Top    -> $I($MinusInf(), $Inf()),
+    Lub    -> @lub(_,_),
+    Glb    -> @glb(_,_)
+}
+
+// Simple Interval Analysis for analyzing value ranges of program variables
+
+.type Node <: symbol
+.type Variable <: symbol
+.decl Edge(n:Node,succ: Node)
+.decl Set_Value(n:Node,v:Variable, value:number)
+.decl Increment_Value(n:Node,v:Variable,inc:number)
+.decl Restrict_Value(n:Node, v:Variable, i:Interval<>)
+
+/* Encoding the program:
+v = 0;
+while(v <= 100) {
+    v = v + 2;
+}
+*/
+Edge("start","start_to_head").
+Edge("start_to_head", "head").
+Edge("head","cond").
+Edge("cond","incr").
+Edge("incr","incr_to_head").
+Edge("incr_to_head","head").
+Edge("head","not cond").
+Edge("not cond","end").
+
+Set_Value("start","v", 0).
+Restrict_Value("cond","v", $I($MinusInf(), $Cst(100))).
+Restrict_Value("not cond","v", $I($Cst(101), $Inf())).
+Increment_Value("incr", "v", 2).
+
+// Possible values for v after statement n, expressed with an interval
+// for instance: Values("head", "v", [0, 50])
+.decl Values(
+    n:Node,
+    v:Variable,
+    i:Interval<>)
+
+.output Values()
+
+Values(n, v, $I($Cst(x), $Cst(x))) :-
+    Set_Value(n, v, x).
+
+Values(n, v, i) :-
+    Values(pred, v, i),
+    Edge(pred, n),
+    !Set_Value(n, v, _),
+    !Increment_Value(n, v, _),
+    !Restrict_Value(n, v, _).
+
+Values(n, v, @incr(i, x)) :-
+    Values(pred, v, i),
+    Edge(pred, n),
+    Increment_Value(n, v, x).
+
+Values(n, v, x) :-
+    Values(pred, v, x),
+    Edge(pred, n),
+    Restrict_Value(n, v, x).
+
diff --git a/tests/interface/lattice1/lattice1.err b/tests/interface/lattice1/lattice1.err
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/interface/lattice1/lattice1.out b/tests/interface/lattice1/lattice1.out
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/interface/lattice2/CMakeLists.txt b/tests/interface/lattice2/CMakeLists.txt
new file mode 100644
index 00000000000..2b14ef68ebb
--- /dev/null
+++ b/tests/interface/lattice2/CMakeLists.txt
@@ -0,0 +1,43 @@
+# Souffle - A Datalog Compiler
+# Copyright (c) 2022 The Souffle Developers. All rights reserved
+# Licensed under the Universal Permissive License v 1.0 as shown at:
+# - https://opensource.org/licenses/UPL
+# - <souffle root>/licenses/SOUFFLE-UPL.txt
+
+add_library(lattice2functors SHARED functors.cpp)
+target_include_directories(lattice2functors PRIVATE "${CMAKE_SOURCE_DIR}/src/include")
+
+target_compile_features(lattice2functors
+                        PUBLIC cxx_std_17)
+
+set_target_properties(lattice2functors PROPERTIES CXX_EXTENSIONS OFF)
+set_target_properties(lattice2functors PROPERTIES OUTPUT_NAME "functors")
+set_target_properties(lattice2functors PROPERTIES WINDOWS_EXPORT_ALL_SYMBOLS ON)
+
+if (OPENMP_FOUND)
+    target_link_libraries(lattice2functors PUBLIC OpenMP::OpenMP_CXX)
+endif()
+
+if (Threads_FOUND)
+  target_link_libraries(lattice2functors PUBLIC Threads::Threads)
+endif ()
+
+if (NOT MSVC)
+target_compile_options(lattice2functors
+                       PUBLIC "-Wall;-Wextra;-Werror;-fwrapv")
+else ()
+  target_compile_options(lattice2functors PUBLIC /W3 /WX)
+endif()
+
+if (WIN32)
+  # Prefix all shared libraries with 'lib'.
+  set(CMAKE_SHARED_LIBRARY_PREFIX "lib")
+
+  # Prefix all static libraries with 'lib'.
+  set(CMAKE_STATIC_LIBRARY_PREFIX "lib")
+endif ()
+
+if (SOUFFLE_DOMAIN_64BIT)
+    target_compile_definitions(lattice2functors
+                               PUBLIC RAM_DOMAIN_SIZE=64)
+endif()
diff --git a/tests/interface/lattice2/ex1.R.csv b/tests/interface/lattice2/ex1.R.csv
new file mode 100644
index 00000000000..6a68ec4b2dc
--- /dev/null
+++ b/tests/interface/lattice2/ex1.R.csv
@@ -0,0 +1,3 @@
+pos	$Positive
+neg	$Negative
+top	$Top
diff --git a/tests/interface/lattice2/ex1.R2.csv b/tests/interface/lattice2/ex1.R2.csv
new file mode 100644
index 00000000000..84416fe1876
--- /dev/null
+++ b/tests/interface/lattice2/ex1.R2.csv
@@ -0,0 +1,2 @@
+pos
+top
diff --git a/tests/interface/lattice2/ex1.R3.csv b/tests/interface/lattice2/ex1.R3.csv
new file mode 100644
index 00000000000..8b1acc12b63
--- /dev/null
+++ b/tests/interface/lattice2/ex1.R3.csv
@@ -0,0 +1,10 @@
+0
+1
+2
+3
+4
+5
+6
+7
+8
+9
diff --git a/tests/interface/lattice2/functors.cpp b/tests/interface/lattice2/functors.cpp
new file mode 100644
index 00000000000..2f3d5ca984d
--- /dev/null
+++ b/tests/interface/lattice2/functors.cpp
@@ -0,0 +1,44 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023, The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file functors.cpp
+ *
+ ***********************************************************************/
+
+#include "souffle/RecordTable.h"
+#include "souffle/SymbolTable.h"
+#include <cassert>
+
+extern "C" {
+
+enum Sign { Bottom = 0, Negative, Positive, Top, Zero };
+
+souffle::RamDomain lub([[maybe_unused]] souffle::SymbolTable* symbolTable,
+        [[maybe_unused]] souffle::RecordTable* recordTable, souffle::RamDomain arg1,
+        souffle::RamDomain arg2) {
+    if (arg1 == Bottom) return arg2;
+    if (arg2 == Bottom) return arg1;
+    if (arg1 == arg2) return arg1;
+    return Top;
+}
+
+souffle::RamDomain glb([[maybe_unused]] souffle::SymbolTable* symbolTable,
+        [[maybe_unused]] souffle::RecordTable* recordTable, souffle::RamDomain arg1,
+        souffle::RamDomain arg2) {
+    if (arg1 == Bottom) return Bottom;
+    if (arg2 == Bottom) return Bottom;
+    if (arg1 == Top) return arg2;
+    if (arg2 == Top) return arg1;
+    if (arg1 == arg2) return arg1;
+    if (arg1 == arg2) return arg1;
+    return Bottom;
+}
+
+}  // end of extern "C"
diff --git a/tests/interface/lattice2/lattice2.dl b/tests/interface/lattice2/lattice2.dl
new file mode 100644
index 00000000000..aeda74ba150
--- /dev/null
+++ b/tests/interface/lattice2/lattice2.dl
@@ -0,0 +1,69 @@
+// Souffle - A Datalog Compiler
+// Copyright (c) 2021, The Souffle Developers. All rights reserved
+// Licensed under the Universal Permissive License v 1.0 as shown at:
+// - https://opensource.org/licenses/UPL
+// - <souffle root>/licenses/SOUFFLE-UPL.txt
+
+
+.type Sign =
+    Bottom{}
+  | Negative{}
+  | Positive{}
+  | Top{}
+  | Zero{}
+
+.functor lub(a:Sign, b:Sign):Sign stateful
+.functor glb(a:Sign, b:Sign):Sign stateful
+
+.lattice Sign<> {
+    Bottom -> $Bottom(),
+    Top -> $Top(),
+    Lub -> @lub(_,_),
+    Glb -> @glb(_,_)
+}
+
+.comp _ex1 {
+
+    .decl N(n:number)
+
+    N(x) :- x = range(-10, 10).
+
+    .decl S(n:number, s:Sign<>)
+
+    S(n, s) :-
+        N(n),
+        (
+            n = 0, s = $Zero();
+            n > 0, s = $Positive();
+            n < 0, s = $Negative()
+        ).
+
+    .decl R(n:symbol, s:Sign<>)
+    .output R()
+
+    R("pos", s) :-
+        S(x, s), x > 0.
+
+    R("neg", s) :-
+        S(x, s), x < 0.
+
+    R("top", s) :-
+        S(_, s).
+
+    .decl R2(n:symbol)
+    .output R2()
+
+    R2(x) :-
+        R(x, $Positive()).
+
+    // testing negation
+
+    .decl R3(n:number)
+    .output R3()
+
+    R3(x) :-
+        N(x),
+        !S(x, $Negative()).
+
+}
+.init ex1 = _ex1
diff --git a/tests/interface/lattice2/lattice2.err b/tests/interface/lattice2/lattice2.err
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/interface/lattice2/lattice2.out b/tests/interface/lattice2/lattice2.out
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/interface/lattice3/CMakeLists.txt b/tests/interface/lattice3/CMakeLists.txt
new file mode 100644
index 00000000000..1564473f70a
--- /dev/null
+++ b/tests/interface/lattice3/CMakeLists.txt
@@ -0,0 +1,43 @@
+# Souffle - A Datalog Compiler
+# Copyright (c) 2022 The Souffle Developers. All rights reserved
+# Licensed under the Universal Permissive License v 1.0 as shown at:
+# - https://opensource.org/licenses/UPL
+# - <souffle root>/licenses/SOUFFLE-UPL.txt
+
+add_library(lattice3functors SHARED functors.cpp)
+target_include_directories(lattice3functors PRIVATE "${CMAKE_SOURCE_DIR}/src/include")
+
+target_compile_features(lattice3functors
+                        PUBLIC cxx_std_17)
+
+set_target_properties(lattice3functors PROPERTIES CXX_EXTENSIONS OFF)
+set_target_properties(lattice3functors PROPERTIES OUTPUT_NAME "functors")
+set_target_properties(lattice3functors PROPERTIES WINDOWS_EXPORT_ALL_SYMBOLS ON)
+
+if (OPENMP_FOUND)
+    target_link_libraries(lattice3functors PUBLIC OpenMP::OpenMP_CXX)
+endif()
+
+if (Threads_FOUND)
+  target_link_libraries(lattice3functors PUBLIC Threads::Threads)
+endif ()
+
+if (NOT MSVC)
+target_compile_options(lattice3functors
+                       PUBLIC "-Wall;-Wextra;-Werror;-fwrapv")
+else ()
+  target_compile_options(lattice3functors PUBLIC /W3 /WX)
+endif()
+
+if (WIN32)
+  # Prefix all shared libraries with 'lib'.
+  set(CMAKE_SHARED_LIBRARY_PREFIX "lib")
+
+  # Prefix all static libraries with 'lib'.
+  set(CMAKE_STATIC_LIBRARY_PREFIX "lib")
+endif ()
+
+if (SOUFFLE_DOMAIN_64BIT)
+    target_compile_definitions(lattice3functors
+                               PUBLIC RAM_DOMAIN_SIZE=64)
+endif()
diff --git a/tests/interface/lattice3/ex1.R.csv b/tests/interface/lattice3/ex1.R.csv
new file mode 100644
index 00000000000..b3fc5720d42
--- /dev/null
+++ b/tests/interface/lattice3/ex1.R.csv
@@ -0,0 +1 @@
+42	[0, 30]	[1, 10]
diff --git a/tests/interface/lattice3/ex2.R.csv b/tests/interface/lattice3/ex2.R.csv
new file mode 100644
index 00000000000..1ccbf910a1b
--- /dev/null
+++ b/tests/interface/lattice3/ex2.R.csv
@@ -0,0 +1 @@
+42	[0, 40]	[0, 40]
diff --git a/tests/interface/lattice3/ex3.R.csv b/tests/interface/lattice3/ex3.R.csv
new file mode 100644
index 00000000000..7b2954fbadc
--- /dev/null
+++ b/tests/interface/lattice3/ex3.R.csv
@@ -0,0 +1 @@
+0	[50, 100]
diff --git a/tests/interface/lattice3/ex4.C.csv b/tests/interface/lattice3/ex4.C.csv
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/interface/lattice3/ex4.R.csv b/tests/interface/lattice3/ex4.R.csv
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/interface/lattice3/functors.cpp b/tests/interface/lattice3/functors.cpp
new file mode 100644
index 00000000000..cbbdb1545bc
--- /dev/null
+++ b/tests/interface/lattice3/functors.cpp
@@ -0,0 +1,42 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023, The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file functors.cpp
+ *
+ ***********************************************************************/
+
+#include "souffle/RecordTable.h"
+#include "souffle/SymbolTable.h"
+#include <cassert>
+
+extern "C" {
+
+souffle::RamDomain lub([[maybe_unused]] souffle::SymbolTable* symbolTable, souffle::RecordTable* recordTable,
+        souffle::RamDomain arg1, souffle::RamDomain arg2) {
+    const souffle::RamDomain* t1 = recordTable->unpack(arg1, 2);
+    const souffle::RamDomain* t2 = recordTable->unpack(arg2, 2);
+    const souffle::RamDomain res[2] = {std::min(t1[0], t2[0]), std::max(t1[1], t2[1])};
+    return recordTable->pack(res, 2);
+}
+
+souffle::RamDomain glb([[maybe_unused]] souffle::SymbolTable* symbolTable, souffle::RecordTable* recordTable,
+        souffle::RamDomain arg1, souffle::RamDomain arg2) {
+    const souffle::RamDomain* t1 = recordTable->unpack(arg1, 2);
+    const souffle::RamDomain* t2 = recordTable->unpack(arg2, 2);
+    souffle::RamDomain res[2] = {std::max(t1[0], t2[0]), std::min(t1[1], t2[1])};
+    if (res[0] > res[1]) {
+        // bottom
+        res[0] = 0;
+        res[1] = -1;
+    }
+    return recordTable->pack(res, 2);
+}
+
+}  // end of extern "C"
diff --git a/tests/interface/lattice3/lattice3.dl b/tests/interface/lattice3/lattice3.dl
new file mode 100644
index 00000000000..3acfd764ecb
--- /dev/null
+++ b/tests/interface/lattice3/lattice3.dl
@@ -0,0 +1,99 @@
+// Souffle - A Datalog Compiler
+// Copyright (c) 2023, The Souffle Developers. All rights reserved
+// Licensed under the Universal Permissive License v 1.0 as shown at:
+// - https://opensource.org/licenses/UPL
+// - <souffle root>/licenses/SOUFFLE-UPL.txt
+
+.type Interval = [lb:number, ub:number]
+.functor lub(a:Interval, b:Interval):Interval stateful
+.functor glb(a:Interval, b:Interval):Interval stateful
+
+.init ex1 = _ex1
+.init ex2 = _ex2
+.init ex3 = _ex3
+.init ex4 = _ex4
+
+.lattice Interval<> {
+    Bottom -> [0, -1],
+    Lub    -> @lub(_,_),
+    Glb    -> @glb(_,_)
+}
+
+.comp _ex1 {
+    // testing lub on a non-recursive relation Y
+    .decl X(x:number)
+
+    .decl R(
+        x:number,
+        i:Interval<>,
+        j:Interval<>)
+    .output R()
+
+    X(42).
+
+    R(x, [20, 30], [1, 2]),
+    R(x, [0, 10], [6,10]) :-
+        X(x).
+}
+
+.comp _ex2 {
+    // testing lub on a recursive relation Y with non-recursive clauses
+    .decl X(x:number)
+
+    .decl R(
+        x:number,
+        i:Interval<>,
+        j:Interval<>)
+    .output R()
+
+    X(42).
+
+    R(x, [20, 30], [1, 40]),
+    R(x, [0, 10], [6,10]) :-
+        X(x).
+
+    R(x, b, a) :-
+        R(x, a, b).
+
+}
+
+.comp _ex3 {
+    // testing glb
+    .decl X(x:number, i:Interval<>)
+    .decl Y(x:number, i:Interval<>)
+    .decl R(x:number, i:Interval<>)
+    .output R()
+
+    X(0, [0,100]).
+    Y(0, [50, 150]).
+
+    R(x, i) :-
+        X(x, i),
+        Y(x, i).
+
+}
+
+.comp _ex4 {
+    // testing glb
+    .decl X(i:Interval<>)
+    .decl Y(i:Interval)
+    .decl R(i:Interval<>)
+    .output R()
+
+    X([0,100]).
+    Y([50, 150]).
+
+    R(i) :-
+        X(i),
+        Y(i).
+
+    .decl A(i:Interval<>)
+    .decl B(i:Interval<>)
+    .decl C(i:Interval<>)
+    .output C()
+
+    A([-10, -1]).
+    B([1, 100]).
+    C(i) :- A(i), B(i).
+
+}
\ No newline at end of file
diff --git a/tests/interface/lattice3/lattice3.err b/tests/interface/lattice3/lattice3.err
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/interface/lattice3/lattice3.out b/tests/interface/lattice3/lattice3.out
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/semantic/leq/leq.dl b/tests/semantic/leq/leq.dl
index b0ec1779457..36f19d26781 100644
--- a/tests/semantic/leq/leq.dl
+++ b/tests/semantic/leq/leq.dl
@@ -79,4 +79,4 @@ Values(n, v, [lb, ub]) :-
     Values(n, v, [lb1, ub1]),
     Values(n, v, [lb2, ub2]),
     lb = min(lb1, lb2),
-    ub = max(ub1, ub2).
+    ub = max(ub1, ub2).
\ No newline at end of file
diff --git a/tests/semantic/subsumption/subsumption.err b/tests/semantic/subsumption/subsumption.err
index b70f4490eee..9d1eed8c90f 100644
--- a/tests/semantic/subsumption/subsumption.err
+++ b/tests/semantic/subsumption/subsumption.err
@@ -1,4 +1,4 @@
-Error: Subsumptive relation "A"  must not be a nullary relation in file subsumption.dl at line 9
+Error: Subsumptive relation "A" must not be a nullary relation in file subsumption.dl at line 9
 .decl A() btree_delete
 ------^----------------
 Warning: No subsumptive rule for relation C in file subsumption.dl at line 17