Prompt for an agent

Stream: Equational

[Michael Bucko]

I tried to equip an agent with tools and a prompt. I guess the prompt is far from perfect. How about we add this kind of prompt file to the repo so that everyone could - to a certain extent - reproduce the thought process used in this project using bots?

// Initialize the set of generators G for the free magma M
G = { g1, g2, ..., gn }
M = FreeMagma(G)

// Define the theory T with a set of laws L
L = { law1, law2, ..., lawN }

// Derive rewrite rules R from the laws L
R = deriveRewriteRules(L)

// Initialize implications I and anti-implications AI
I = { implication1, implication2, ..., implicationM }
AI = { antiImplication1, antiImplication2, ..., antiImplicationK }

// Initialize the E-Graph with elements from M
EGraph = new EGraph()
EGraph.addElements(M.elements)

// Equality Saturation Loop with Rewriting and Implications
do {
    changes = false

    // Apply simple rewriting rules
    for each rule in R {
        if EGraph.apply(rule) {
            changes = true
        }
    }

    // Apply implications to introduce new equalities
    for each implication in I {
        if EGraph.apply(implication) {
            changes = true
        }
    }

    // Prevent invalid reductions using anti-implications
    for each antiImplication in AI {
        if EGraph.detect(antiImplication) {
            EGraph.prevent(antiImplication)
        }
    }

} while changes == true

// Handle infinite models by processing finite subsets
if M.isInfinite() {
    subsets = M.generateFiniteSubsets()
    for each subset in subsets {
        processFiniteSubset(subset)
    }
} else {
    // For finite magmas, find normal forms directly
    for each element in M {
        normalForm = EGraph.findNormalForm(element)
        print("Normal form of", element, "is", normalForm)
    }
}

// Function Definitions

function deriveRewriteRules(L) {
    R = empty set
    for each law in L {
        // Convert laws into bidirectional rewrite rules
        R.add(convertToRewriteRule(law))
    }
    return R
}

function processFiniteSubset(subset) {
    // Create a local E-Graph for the subset
    localEGraph = new EGraph()
    localEGraph.addElements(subset.elements)

    // Repeat the equality saturation loop on the subset
    do {
        localChanges = false

        // Apply rewriting rules
        for each rule in R {
            if localEGraph.apply(rule) {
                localChanges = true
            }
        }

        // Apply implications
        for each implication in I {
            if localEGraph.apply(implication) {
                localChanges = true
            }
        }

        // Handle anti-implications
        for each antiImplication in AI {
            if localEGraph.detect(antiImplication) {
                localEGraph.prevent(antiImplication)
            }
        }

    } while localChanges == true

    // Find normal forms in the subset
    for each element in subset {
        normalForm = localEGraph.findNormalForm(element)
        print("Normal form of", element, "in subset is", normalForm)
    }
}

function convertToRewriteRule(law) {
    // Convert a law into a pair of rewrite rules (forward and backward)
    ruleForward = createRule(law.leftSide, law.rightSide)
    ruleBackward = createRule(law.rightSide, law.leftSide)
    return { ruleForward, ruleBackward }
}

function createRule(pattern, replacement) {
    // Create a rewrite rule from a pattern to a replacement
    return new RewriteRule(pattern, replacement)
}

function EGraph.apply(rule) {
    // Apply a rewrite rule or implication to the E-Graph
    applied = false
    for each equivalenceClass in EGraph {
        if equivalenceClass.matches(rule.pattern) {
            equivalenceClass.add(rule.replacement)
            applied = true
        }
    }
    return applied
}

function EGraph.detect(antiImplication) {
    // Detect if an anti-implication pattern exists in the E-Graph
    for each equivalenceClass in EGraph {
        if equivalenceClass.matches(antiImplication.pattern) {
            return true
        }
    }
    return false
}

function EGraph.prevent(antiImplication) {
    // Prevent certain reductions based on anti-implications
    EGraph.removePattern(antiImplication.pattern)
}

function EGraph.findNormalForm(element) {
    // Find the simplest form of an element based on the E-Graph
    return element.getMinimalRepresentative()
}