SK in egglog: part 4, extensional equality

Posted on 2024-05-10 by Chris Warburton

This post continues my explorations with egglog, using it to implement SK logic. Here’s the code so far, with some ruleset annotations sprinkled in to give us more control over what to run:

;; Applicative combinatory logic. We use (C "foo") for constants, which will
;; show up in the e-graph and output of egglog.
(datatype Com
          (App Com Com)
          (C String))

;; Base combinators S and K
(let S (C "S"))
(let K (C "K"))

;; Example combinator
(let I (App (App S K) K))

;; Rewrite rules for running SK expressions
(ruleset reduce)
(rewrite      (App (App K x) y)    x                         :ruleset reduce)
(rewrite (App (App (App S x) y) z) (App (App x z) (App y z)) :ruleset reduce)

A note on infinite loops and recursion

Modelling a Turing-complete system like SK requires care, to reach the desired results whilst avoiding infinite recursion. The SK reduction rules are the main danger, since they will attempt to “run” every expression in the database, so we need to avoid expressions which blow up.

Note that e-graphs are perfectly happy with infinite cycles, for example the following expression omega will be reduced by the S rule, but ends up back where it started after a few steps; that’s normally considered an “infinite loop”, but egglog’s cumulative approach keeps track of all the states, and stops as soon as the pattern repeats a previous form:

(let sii   (App (App S I) I))
(let omega (App sii sii))

;; A "saturate" schedule will keep running until the database stops changing
(run-schedule (saturate reduce))
(check (= omega (App (App I sii) (App I sii))))

Output…

[INFO ] Declared sort Com.
[INFO ] Declared function App.
[INFO ] Declared function C.
[INFO ] Declared ruleset reduce.
[INFO ] Declared rule (rewrite (App (App K x) y) x).
[INFO ] Declared rule (rewrite (App (App (App S x) y) z) (App (App x z) (App y z))).
[INFO ] Ran schedule (seq (saturate (seq (run reduce)))).
[INFO ] Report: Rule (rule ((= rewrite_var__ (App (App K x) y)))       ((union rewrite_var__ x))     ...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((= rewrite_var__ (App (App (App S x) y) z)))       ((union rewrite_var__ ...: search 0.000s, apply 0.000s, num matches 4
    Ruleset reduce: search 0.000s, apply 0.000s, rebuild 0.000s
    
[INFO ] Checked fact [Eq([Var((), ResolvedVar { name: "omega", sort: EqSort { name: "Com" } }), Call((), Func(FuncType { name: "App", input: [EqSort { name: "Com" }, EqSort { name: "Com" }], output: EqSort { name: "Com" }, is_datatype: true, has_default: false }), [Call((), Func(FuncType { name: "App", input: [EqSort { name: "Com" }, EqSort { name: "Com" }], output: EqSort { name: "Com" }, is_datatype: true, has_default: false }), [Var((), ResolvedVar { name: "I", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "sii", sort: EqSort { name: "Com" } })]), Call((), Func(FuncType { name: "App", input: [EqSort { name: "Com" }, EqSort { name: "Com" }], output: EqSort { name: "Com" }, is_datatype: true, has_default: false }), [Var((), ResolvedVar { name: "I", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "sii", sort: EqSort { name: "Com" } })])])])].

Representing symbols

The last couple of installments explored the idea of extensionality, using Haskell to uncover a problem I was running into in egglog. The cause turned out to be using symbolic inputs to check if expressions agreed, when those expressions may have already contained those symbols. Now we’re switching back to egglog, our first task is to distinguish expressions that contain such uninterpreted symbols.

We’ll represent uninterpreted symbols numerically. One way to do this is using a unary/Peano-style encoding, with a “zeroth symbol” and a function for the “successor symbol”. However, egglog has numbers built-in via its i64 sort, so we might as well use those (they’re also backed by efficient Rust code)! We’ll turn these i64 values into Com values using an egglog function called V (for Variable; since we’re already using S for something else):

(function V (i64) Com)

We’ll avoid defining any outputs for V, so it remains uninterpreted: that way egglog can treat (V 0), (V 1), etc. as Com values, but it cannot make any further assumptions about their structure or relationships.

We’ll still use the idea of a “successor symbol”, but that can now be an ordinary function that increments our i64 value:

(ruleset symbols)
(function bumpSymbols (Com) Com)

(rewrite (bumpSymbols (V n)) (V (+ n 1))
         :ruleset symbols)

We’ll also generalise this to work on any Com value. As the name suggests, it will propagate recursively through the tree structure of a Com expression, using the above rewrite to increment all of the symbols it contains:

(birewrite (bumpSymbols (App x y))
           (App (bumpSymbols x) (bumpSymbols y))
           :when ((bumpSymbols x) (bumpSymbols y))
           :ruleset symbols)

The condition :when ((bumpSymbols x) (bumpSymbols y)) ensures termination, by only acting on expressions that already appear in the database. It’s important that this uses birewrite, since we want to ensure uses of bumpSymbols get propagated down through sub-expressions; but we also need known expressions to coalesce their bumpSymbols wrappers upwards, for our rules to match on.

Finally, bumpSymbols does nothing to leaves, since they contain no symbols:

(birewrite (bumpSymbols (C x)) (C x)
           :ruleset symbols)

Aside: “printf debugging” in egglog…

When we execute an egglog script, it can be difficult to know what it’s doing: e.g. if some incorrect fact appears, we want some trace of the rules which lead to it. Support for “proofs” may help, and this seems to be on egglog’s wishlist, but it’s not yet available (as of 2024-04-24).

For very simple rules, we can sometimes reformulate them so each rule puts a marker in its output. However, this can get pretty complicated and tedious for larger rulesets; and requires effectively re-implementing many parts of egglog inside itself, which wastes a lot of time.

If we just want to see that some rule has fired, we can use an extract action to emit a message. The argument to extract can be any expression: the most useful are plain strings (to indicate what’s happened) and variables (to see what values are being processed). For example, if we want to see how many symbolic values we’re creating, the following variant of the above rewrite will show us:

(rule ((bumpSymbols (V n)))
      ((let bumped (V (+ n 1)))
       (extract "Bumped to:")
       (extract bumped)
       (union (bumpSymbols (V n)) bumped))
      :ruleset symbols)

For example, populating the database with some seed values and running until saturation:

(bumpSymbols (App I (V 0)))
(run-schedule (saturate reduce symbols))

[INFO ] Declared sort Com.
[INFO ] Declared function App.
[INFO ] Declared function C.
[INFO ] Declared ruleset reduce.
[INFO ] Declared rule (rewrite (App (App K x) y) x).
[INFO ] Declared rule (rewrite (App (App (App S x) y) z) (App (App x z) (App y z))).
[INFO ] Declared function V.
[INFO ] Declared ruleset symbols.
[INFO ] Declared function bumpSymbols.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))<=.
[INFO ] Declared rule (rule ((bumpSymbols (V n)))
          ((let bumped (V (+ n 1)))
           (extract 'Bumped to:' 0)
           (extract bumped 0)
           (union (bumpSymbols (V n)) bumped))
             ).
[INFO ] extracted with cost 1: "Bumped to:"
[INFO ] extracted with cost 2: (V 1)
[INFO ] Ran schedule (seq (saturate (seq (run reduce) (run symbols)))).
[INFO ] Report: Rule (rule ((= rewrite_var__ (App (bumpSymbols x) (bumpSymbols y)))        (bumpSymbo...: search 0.001s, apply 0.000s, num matches 11
    Rule (rule ((= rewrite_var__ (App (App (App S x) y) z)))       ((union rewrite_var__ ...: search 0.001s, apply 0.000s, num matches 7
    Rule (rule ((bumpSymbols (V n)))       ((let bumped (V (+ n 1)))        (extract "Bum...: search 0.000s, apply 0.000s, num matches 1
    Rule (rule ((= rewrite_var__ (C x)))       ((union rewrite_var__ (bumpSymbols (C x)))...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((= rewrite_var__ (bumpSymbols (C x))))       ((union rewrite_var__ (C x))...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((= rewrite_var__ (bumpSymbols (App x y)))        (bumpSymbols x)        (...: search 0.003s, apply 0.000s, num matches 11
    Rule (rule ((= rewrite_var__ (App (App K x) y)))       ((union rewrite_var__ x))     ...: search 0.006s, apply 0.000s, num matches 5
    Ruleset reduce: search 0.007s, apply 0.000s, rebuild 0.000s
    Ruleset symbols: search 0.004s, apply 0.000s, rebuild 0.000s
    
"Bumped to:"
(V 1)

Counting symbolic arguments

Extensional equality tells us that when two expressions like (App (App foo (V a)) (V b)) and (App (App bar (V a)) (V b)) are equal, then foo and bar are equal; as long as neither contains (V a) or (V b). This is a bit trickier to represent in egglog, since we’re dealing with e-graphs rather than specific terms; yet there’s a remarkably simple way to capture the essence of this situation, by counting symbolic arguments. Here’s the function we’ll use:

(function symbolicArgCount (Com) i64 :merge (min old new))

We’ll explain the :merge clause in a moment (it’s required to avoid ambiguity). First we’ll define the base case, that expressions involving no symbols will have a symbolicArgCount of zero:

(rule ((= (bumpSymbols x) x))
      ((set (symbolicArgCount x) 0))
      :ruleset symbols)

The pre-condition here requires that bumpSymbols leaves x unchanged: we’ll say that such values are “concrete”. We know any Com of the form (C x) is concrete, since that’s stated by one of the rules above; and from this we know S and K are concrete. The rules for bumpSymbols also make (App x y) concrete when both x and y are concrete. To see this, consider what happens to (bumpSymbols (App x y)): the rules for bumpSymbols say that is equal to (App (bumpSymbols x) (bumpSymbols y)); since we’re assuming x and y are concrete (i.e. unaffected by bumpSymbols) this equals (App x y), which is the argument we originally gave to bumpSymbols; hence (App x y) is unaffected by bumpSymbols, and therefore is concrete. ∎

Larger counts occur when we apply an expression to a symbol which doesn’t occur in that expression. We can ensure this using bumpSymbols: since its result has all its symbols incremented, we know that it cannot contain the first symbol (V 0):

(rule ((= n (symbolicArgCount x))
       (App x y))
      ((set (symbolicArgCount (App (bumpSymbols x) (V 0)))
            (+ 1 n)))
      :ruleset symbols)

In this case we have two pre-conditions: (App x y) requires that our database already contains x applied to something, which ensures the recursive pattern (App (bumpSymbols x) (V 0)), (App (App (bumpSymbols (bumpSymbols x)) (V 1)) (V 0)), etc. will eventually terminate. Secondly, we avoid using (+ 1 (symbolicArgCount x)), since that can again lead to infinite recursion; instead we use (= n (symbolicArgCount x)) to restrict our matches to values whose symbolicArgCount has already been calculated.

This definition of symbolicArgCount does two things for us: firstly, it is only defined for expressions which apply a concrete expression to some number of symbols with decrementing indices, e.g. (App (App (App (App S K) (V 2)) (V 1)) (V 0)); secondly, in the cases where it’s defined, it tells us how many symbols there are.

There’s an interesting subtlety here, since it’s really equivalence classes that are concrete, and those may contain symbolic values! For example, consider the following expression:

(let expr (App K S))

We can check that this is concrete (i.e. unchanged by bumpSymbols), and hence that its symbolicArgCount is 0:

(run-schedule (saturate reduce symbols))
(check (= (bumpSymbols expr) expr))
(extract (symbolicArgCount expr))

Stderr…

[INFO ] Declared sort Com.
[INFO ] Declared function App.
[INFO ] Declared function C.
[INFO ] Declared ruleset reduce.
[INFO ] Declared rule (rewrite (App (App K x) y) x).
[INFO ] Declared rule (rewrite (App (App (App S x) y) z) (App (App x z) (App y z))).
[INFO ] Declared function V.
[INFO ] Declared ruleset symbols.
[INFO ] Declared function bumpSymbols.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (V n)) (V (+ n 1))).
[INFO ] Declared function symbolicArgCount.
[INFO ] Declared rule (rule ((= (bumpSymbols x) x))
          ((set (symbolicArgCount x) 0))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Ran schedule (seq (saturate (seq (run reduce) (run symbols)))).
[INFO ] Report: Rule (rule ((= (bumpSymbols x) x))       ((set (symbolicArgCount x) 0))          ): search 0.000s, apply 0.000s, num matches 10
    Rule (rule ((= n (symbolicArgCount x))        (App x y))       ((set (symbolicArgCoun...: search 0.000s, apply 0.000s, num matches 35
    Rule (rule ((= rewrite_var__ (bumpSymbols (V n))))       ((union rewrite_var__ (V (+ ...: search 0.000s, apply 0.000s, num matches 3
    Rule (rule ((= rewrite_var__ (C x)))       ((union rewrite_var__ (bumpSymbols (C x)))...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((= n (symbolicArgCount x))        (App x y)        (= v0___ (+ 1 n)))    ...: search 0.000s, apply 0.000s, num matches 35
    Rule (rule ((= rewrite_var__ (bumpSymbols (C x))))       ((union rewrite_var__ (C x))...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((= rewrite_var__ (bumpSymbols (App x y)))        (bumpSymbols x)        (...: search 0.002s, apply 0.000s, num matches 27
    Rule (rule ((= rewrite_var__ (App (bumpSymbols x) (bumpSymbols y)))        (bumpSymbo...: search 0.001s, apply 0.000s, num matches 23
    Rule (rule ((= rewrite_var__ (App (App K x) y)))       ((union rewrite_var__ x))     ...: search 0.002s, apply 0.000s, num matches 16
    Rule (rule ((= rewrite_var__ (App (App (App S x) y) z)))       ((union rewrite_var__ ...: search 0.002s, apply 0.000s, num matches 13
    Ruleset reduce: search 0.004s, apply 0.000s, rebuild 0.000s
    Ruleset symbols: search 0.005s, apply 0.001s, rebuild 0.000s
    
[INFO ] Checked fact [Eq([Call((), Func(FuncType { name: "bumpSymbols", input: [EqSort { name: "Com" }], output: EqSort { name: "Com" }, is_datatype: true, has_default: false }), [Var((), ResolvedVar { name: "expr", sort: EqSort { name: "Com" } })]), Var((), ResolvedVar { name: "expr", sort: EqSort { name: "Com" } })])].
[INFO ] extracted with cost 1: 0

So far so good. Now let’s apply it to a symbolic argument, matching the second rule for symbolicArgCount:

(let symbolic (App (bumpSymbols expr) (V 0)))

According to that rule, we would expect (symbolicArgCount symbolic) to be (+ 1 (symbolicArgCount expr)), and hence to return 1:

(run-schedule (saturate reduce symbols))
(extract (symbolicArgCount symbolic))

Stderr…

[INFO ] Declared sort Com.
[INFO ] Declared function App.
[INFO ] Declared function C.
[INFO ] Declared ruleset reduce.
[INFO ] Declared rule (rewrite (App (App K x) y) x).
[INFO ] Declared rule (rewrite (App (App (App S x) y) z) (App (App x z) (App y z))).
[INFO ] Declared function V.
[INFO ] Declared ruleset symbols.
[INFO ] Declared function bumpSymbols.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (V n)) (V (+ n 1))).
[INFO ] Declared function symbolicArgCount.
[INFO ] Declared rule (rule ((= (bumpSymbols x) x))
          ((set (symbolicArgCount x) 0))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Ran schedule (seq (saturate (seq (run reduce) (run symbols)))).
[INFO ] Report: Rule (rule ((= (bumpSymbols x) x))       ((set (symbolicArgCount x) 0))          ): search 0.000s, apply 0.000s, num matches 11
    Rule (rule ((= rewrite_var__ (App (App K x) y)))       ((union rewrite_var__ x))     ...: search 0.001s, apply 0.000s, num matches 22
    Rule (rule ((= rewrite_var__ (C x)))       ((union rewrite_var__ (bumpSymbols (C x)))...: search 0.000s, apply 0.000s, num matches 3
    Rule (rule ((= rewrite_var__ (bumpSymbols (C x))))       ((union rewrite_var__ (C x))...: search 0.000s, apply 0.000s, num matches 3
    Rule (rule ((= n (symbolicArgCount x))        (App x y)        (= v0___ (+ 1 n)))    ...: search 0.000s, apply 0.000s, num matches 39
    Rule (rule ((= rewrite_var__ (bumpSymbols (App x y)))        (bumpSymbols x)        (...: search 0.001s, apply 0.000s, num matches 31
    Rule (rule ((= rewrite_var__ (bumpSymbols (V n))))       ((union rewrite_var__ (V (+ ...: search 0.002s, apply 0.000s, num matches 3
    Rule (rule ((= rewrite_var__ (App (App (App S x) y) z)))       ((union rewrite_var__ ...: search 0.003s, apply 0.000s, num matches 13
    Rule (rule ((= rewrite_var__ (App (bumpSymbols x) (bumpSymbols y)))        (bumpSymbo...: search 0.004s, apply 0.000s, num matches 27
    Rule (rule ((= n (symbolicArgCount x))        (App x y))       ((set (symbolicArgCoun...: search 0.005s, apply 0.000s, num matches 39
    Ruleset reduce: search 0.004s, apply 0.000s, rebuild 0.000s
    Ruleset symbols: search 0.013s, apply 0.001s, rebuild 0.006s
    
[INFO ] extracted with cost 1: 0

Uh oh, we got 0 instead! Remember that (bumpSymbols (App K S)) is equal to (App K S) (since it’s concrete), and the reduction rule for K says that (App (App K S) (V 0)) is equal to S. Since egglog functions are applied to equivalence classes, rather than particular terms, the value of (symbolicArgCount symbolic) must be the same as (symbolicArgCount S), and the latter is clearly 0. We fix this ambiguity using the :merge parameter in the definition of symbolicArgCount: when equal inputs give unequal results, like 0 and 1 in this case, the :merge expression is used, with the conflicting values bound to the names old and new. We use min to choose the smaller value (in this case 0), since that is a property of the class. Larger values are more arbitrary, e.g. in this case the value 1 is due to matching an expression that SK will ultimately discard, and hence seems less fundamental.

Now that we have a working definition of symbolicArgCount, we have enough information to finally implement extensional equality!

Extensional equality

We’ll re-use the trick employed by the second symbolicArgCount rule, that (bumpSymbols foo) is guaranteed to not contain (V 0) (at least, in no place that can affect its result; it may still appear in the equivalence classes due to reduction rules, like in the symbolic example).

If two such expressions are equal when applied to (V 0), their definitions must be inherently equal independent of argument (since bumpSymbols ensures independence from (V 0) syntactically; and its behaviour as an inert, uninterpreted symbol ensures independence semantically). That proves they are equal for any argument, and hence they are extensionally equal:

(ruleset extensional)
(rule ((= (App (bumpSymbols x) (V 0))
          (App (bumpSymbols y) (V 0)))
       (= (symbolicArgCount x)
          (symbolicArgCount y)))
      ((union x y))
      :ruleset extensional)

This rule also requires both expressions to have the same symbolicArgCount, which ensures that the underlying expressions begin with a concrete part (since that’s what we really care about), and that they have the same arity. For arities greater than one, this rule will work backwards recursively: using equality with n arguments to assert equality with n-1 arguments, and so on until their concrete parts become equal.

Ignored arguments

One way that two expressions can be extensionally equal is if they ignore the only terms at which they differ. For example, the K reduction rule discards its second argument; hence expressions which only differ in the second argument to K will be equal, like (App (App K (V 0)) (V 1)) and (App (App K (V 0)) (V 2)). Of course, that doesn’t require extensionality, since such expressions are equal due to that reduction rule (in this example, both expressions are equal to (V 0)).

Yet this simple analysis can be pushed a little further, if we note those expressions which will discard their next argument. We can represent this with an ignoresArg relation:

(ruleset ignored)
(relation ignoresArg (Com))

This relation will be useful to augment the existing extensionality rules, which are limited by their pre-conditions (in order to avoid infinite recursion!). We’ve already seen one way that expressions can ignore their next argument:

(rule ((App K x))
      ((ignoresArg (App K x)))
      :ruleset ignored)

A more sophisticated form uses the S rule to delay the construction of reducible expressions; waiting for some further argument to be applied. Consider the following example:

;; Declare an unspecified, concrete Com value
(declare foo Com)
(union (bumpSymbols foo) foo)

;; Two distinct ways of reducing to foo when applied to another argument
(let kFoo1 (App K foo))
(let kFoo2 (App (App S (App K (App K foo))) I))

Neither of these expressions is reducible, but they are extensionally equal, since they agree on one argument:

(App kFoo1 (V 0)) reduces to foo via the K rule
(App kFoo2 (V 0)) reduces to (App (App (App K (App K foo)) (V 0)) (App I (V 0))) via the S rule, then via the K rule to (App (App K foo) (App I (V 0))), and again to foo.

(In fact, the I argument at the end of kFoo2 is also ignored during reduction!) We can spot this behaviour by noting that if (ignoresArg (App f x)) for all x, then (ignoresArg (App S f)). To see this, give the latter a couple more arguments (App (App (App S f) a) b), so it reduces to (App (App f b) (App a b)): we’re assuming that (App f b) ignores its next argument, making (App a b) irrelevant. Since that’s the only occurence of a, its value is also ignored; and a is the next argument of (App S f). ∎

(rule ((ignoresArg (App (bumpSymbols f) (V 0))))
      ((ignoresArg (App S f)))
      :ruleset ignored)

(rule ((ignoresArg (App f x))
       (App S f))
      ((App (bumpSymbols f) (V 0)))
      :ruleset ignored)

Ignoring the third argument of S is less common, since it only happens when both of the first and second arguments ignore it:

(rule ((ignoresArg x)
       (ignoresArg y)
       (App (App S x) y))
      ((ignoresArg (App (App S x) y)))
      :ruleset ignored)

Finally, we can tell egglog that all applications of an an expression which ignoresArg are (extensionally) equal:

(rule ((= x (App f a))
       (= y (App f b))
       (ignoresArg f))
      ((union x y))
      :ruleset ignored)

This is enough to make our example expressions equal:

(App kFoo2 (V 0))  ;; Apply kFoo2 to something, to satisfy pre-conditions
(run-schedule (repeat 8 (seq reduce symbols extensional ignored)))
(check (= kFoo1 kFoo2))

Output…

[INFO ] Declared sort Com.
[INFO ] Declared function App.
[INFO ] Declared function C.
[INFO ] Declared ruleset reduce.
[INFO ] Declared rule (rewrite (App (App K x) y) x).
[INFO ] Declared rule (rewrite (App (App (App S x) y) z) (App (App x z) (App y z))).
[INFO ] Declared function V.
[INFO ] Declared ruleset symbols.
[INFO ] Declared function bumpSymbols.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (V n)) (V (+ n 1))).
[INFO ] Declared function symbolicArgCount.
[INFO ] Declared rule (rule ((= (bumpSymbols x) x))
          ((set (symbolicArgCount x) 0))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared ruleset extensional.
[INFO ] Declared rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))
           (= (symbolicArgCount x) (symbolicArgCount y)))
          ((union x y))
             ).
[INFO ] Declared ruleset ignored.
[INFO ] Declared function ignoresArg.
[INFO ] Declared rule (rule ((App K x))
          ((ignoresArg (App K x)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App (bumpSymbols f) (V 0))))
          ((ignoresArg (App S f)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App f x))
           (App S f))
          ((App (bumpSymbols f) (V 0)))
             ).
[INFO ] Declared rule (rule ((ignoresArg x)
           (ignoresArg y)
           (App (App S x) y))
          ((ignoresArg (App (App S x) y)))
             ).
[INFO ] Declared rule (rule ((= x (App f a))
           (= y (App f b))
           (ignoresArg f))
          ((union x y))
             ).
[INFO ] Declared function v1___.
[INFO ] Ran schedule (seq (repeat 8 (seq (seq (run reduce) (run symbols) (run extensional) (run ignored))))).
[INFO ] Report: Rule (rule ((= x (App f a))        (= y (App f b))        (ignoresArg f))       ((uni...: search 0.001s, apply 0.000s, num matches 136
    Rule (rule ((= (bumpSymbols x) x))       ((set (symbolicArgCount x) 0))          ): search 0.000s, apply 0.000s, num matches 16
    Rule (rule ((App K x))       ((ignoresArg (App K x)))          ): search 0.000s, apply 0.000s, num matches 15
    Rule (rule ((= rewrite_var__ (bumpSymbols (C x))))       ((union rewrite_var__ (C x))...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((= rewrite_var__ (bumpSymbols (V n))))       ((union rewrite_var__ (V (+ ...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((ignoresArg (App (bumpSymbols f) (V 0))))       ((ignoresArg (App S f))) ...: search 0.001s, apply 0.000s, num matches 4
    Rule (rule ((= rewrite_var__ (App (bumpSymbols x) (bumpSymbols y)))        (bumpSymbo...: search 0.001s, apply 0.000s, num matches 28
    Rule (rule ((= rewrite_var__ (C x)))       ((union rewrite_var__ (bumpSymbols (C x)))...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((= rewrite_var__ (bumpSymbols (App x y)))        (bumpSymbols x)        (...: search 0.001s, apply 0.000s, num matches 32
    Rule (rule ((= n (symbolicArgCount x))        (App x y)        (= v0___ (+ 1 n)))    ...: search 0.000s, apply 0.000s, num matches 57
    Rule (rule ((= n (symbolicArgCount x))        (App x y))       ((set (symbolicArgCoun...: search 0.002s, apply 0.000s, num matches 57
    Rule (rule ((ignoresArg x)        (ignoresArg y)        (App (App S x) y))       ((ig...: search 0.004s, apply 0.000s, num matches 0
    Rule (rule ((= rewrite_var__ (App (App (App S x) y) z)))       ((union rewrite_var__ ...: search 0.004s, apply 0.000s, num matches 31
    Rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))        (= (sy...: search 0.006s, apply 0.000s, num matches 23
    Rule (rule ((ignoresArg (App f x))        (App S f))       ((App (bumpSymbols f) (V 0...: search 0.007s, apply 0.000s, num matches 17
    Rule (rule ((= rewrite_var__ (App (App K x) y)))       ((union rewrite_var__ x))     ...: search 0.009s, apply 0.000s, num matches 19
    Ruleset extensional: search 0.006s, apply 0.000s, rebuild 0.004s
    Ruleset ignored: search 0.012s, apply 0.000s, rebuild 0.000s
    Ruleset reduce: search 0.013s, apply 0.000s, rebuild 0.000s
    Ruleset symbols: search 0.004s, apply 0.000s, rebuild 0.000s
    
[INFO ] Checked fact [Eq([Var((), ResolvedVar { name: "kFoo1", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "kFoo2", sort: EqSort { name: "Com" } })])].

Another test for these rules is the identity combinator I, which we defined as (App (App S K) K). However, that second K is ignored, so any other expression should be usable in its place:

(let I1 (App (App S K) K))
(let I2 (App (App S K) S))
(let I3 (App (App S K) I))
(let I4 (App (App S K) (V 0)))

(run-schedule (saturate reduce symbols extensional ignored))
(check
  (= I I1)
  (= I I2)
  (= I I3)
  (= I I4))

Output…

[INFO ] Declared sort Com.
[INFO ] Declared function App.
[INFO ] Declared function C.
[INFO ] Declared ruleset reduce.
[INFO ] Declared rule (rewrite (App (App K x) y) x).
[INFO ] Declared rule (rewrite (App (App (App S x) y) z) (App (App x z) (App y z))).
[INFO ] Declared function V.
[INFO ] Declared ruleset symbols.
[INFO ] Declared function bumpSymbols.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (V n)) (V (+ n 1))).
[INFO ] Declared function symbolicArgCount.
[INFO ] Declared rule (rule ((= (bumpSymbols x) x))
          ((set (symbolicArgCount x) 0))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared ruleset extensional.
[INFO ] Declared rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))
           (= (symbolicArgCount x) (symbolicArgCount y)))
          ((union x y))
             ).
[INFO ] Declared ruleset ignored.
[INFO ] Declared function ignoresArg.
[INFO ] Declared rule (rule ((App K x))
          ((ignoresArg (App K x)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App (bumpSymbols f) (V 0))))
          ((ignoresArg (App S f)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App f x))
           (App S f))
          ((App (bumpSymbols f) (V 0)))
             ).
[INFO ] Declared rule (rule ((ignoresArg x)
           (ignoresArg y)
           (App (App S x) y))
          ((ignoresArg (App (App S x) y)))
             ).
[INFO ] Declared rule (rule ((= x (App f a))
           (= y (App f b))
           (ignoresArg f))
          ((union x y))
             ).
[INFO ] Ran schedule (seq (saturate (seq (run reduce) (run symbols) (run extensional) (run ignored)))).
[INFO ] Report: Rule (rule ((= rewrite_var__ (bumpSymbols (App x y)))        (bumpSymbols x)        (...: search 0.001s, apply 0.000s, num matches 59
    Rule (rule ((= n (symbolicArgCount x))        (App x y)        (= v0___ (+ 1 n)))    ...: search 0.001s, apply 0.000s, num matches 69
    Rule (rule ((= rewrite_var__ (bumpSymbols (C x))))       ((union rewrite_var__ (C x))...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((ignoresArg x)        (ignoresArg y)        (App (App S x) y))       ((ig...: search 0.001s, apply 0.000s, num matches 0
    Rule (rule ((= (bumpSymbols x) x))       ((set (symbolicArgCount x) 0))          ): search 0.000s, apply 0.000s, num matches 12
    Rule (rule ((= rewrite_var__ (bumpSymbols (V n))))       ((union rewrite_var__ (V (+ ...: search 0.000s, apply 0.000s, num matches 3
    Rule (rule ((= n (symbolicArgCount x))        (App x y))       ((set (symbolicArgCoun...: search 0.000s, apply 0.000s, num matches 69
    Rule (rule ((= rewrite_var__ (App (App (App S x) y) z)))       ((union rewrite_var__ ...: search 0.001s, apply 0.000s, num matches 48
    Rule (rule ((ignoresArg (App (bumpSymbols f) (V 0))))       ((ignoresArg (App S f))) ...: search 0.001s, apply 0.000s, num matches 2
    Rule (rule ((ignoresArg (App f x))        (App S f))       ((App (bumpSymbols f) (V 0...: search 0.001s, apply 0.000s, num matches 6
    Rule (rule ((= rewrite_var__ (App (App K x) y)))       ((union rewrite_var__ x))     ...: search 0.001s, apply 0.000s, num matches 42
    Rule (rule ((= rewrite_var__ (C x)))       ((union rewrite_var__ (bumpSymbols (C x)))...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((= x (App f a))        (= y (App f b))        (ignoresArg f))       ((uni...: search 0.002s, apply 0.000s, num matches 313
    Rule (rule ((= rewrite_var__ (App (bumpSymbols x) (bumpSymbols y)))        (bumpSymbo...: search 0.001s, apply 0.000s, num matches 54
    Rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))        (= (sy...: search 0.002s, apply 0.000s, num matches 19
    Rule (rule ((App K x))       ((ignoresArg (App K x)))          ): search 0.002s, apply 0.000s, num matches 8
    Ruleset extensional: search 0.003s, apply 0.000s, rebuild 0.000s
    Ruleset ignored: search 0.006s, apply 0.000s, rebuild 0.000s
    Ruleset reduce: search 0.001s, apply 0.000s, rebuild 0.000s
    Ruleset symbols: search 0.004s, apply 0.001s, rebuild 0.000s
    
[INFO ] Checked fact [Eq([Var((), ResolvedVar { name: "I", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "I1", sort: EqSort { name: "Com" } })]), Eq([Var((), ResolvedVar { name: "I", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "I2", sort: EqSort { name: "Com" } })]), Eq([Var((), ResolvedVar { name: "I", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "I3", sort: EqSort { name: "Com" } })]), Eq([Var((), ResolvedVar { name: "I", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "I4", sort: EqSort { name: "Com" } })])].

Boolean logic

Extensional equality extends beyond simply ignoring arguments: expressions which use their arguments in equal ways are also extensionally equal. We’ll test this using the following encoding of boolean logic, where (App (App TRUE x) y) reduces to x and (App (App FALSE x) y) reduces to y:

(let TRUE  K)
(let FALSE (App S K))

Boolean operations, such as NOT, AND and OR, can be encoded as SK expressions which, when applied to such encoded booleans, reduce to one or the other of those encoded booleans.

NOT

Here’s a definition of NOT:

(let NOT (App (App S (App (App S (App K S))
                          (App (App S (App K K))
                               S)))
              (App K K)))

It’s chosen such that its application to TRUE agrees with FALSE:

(let notTrue       (App NOT TRUE))
(let notTrueResult (App (App notTrue (V 1)) (V 0)))
(let   falseResult (App (App FALSE   (V 1)) (V 0)))

And its application to FALSE agrees with TRUE:

(let notFalse       (App NOT FALSE))
(let notFalseResult (App (App notFalse (V 1)) (V 0)))
(let     trueResult (App (App TRUE     (V 1)) (V 0)))

These expressions seem to cause our rules to diverge, so we’ll only run them 10 times:

(run-schedule (repeat 10 (seq reduce symbols extensional ignored)))

First we’ll check that our rules are consistent:

(check (!= TRUE FALSE))

Then we can check the behaviour of notTrue and notFalse:

(check
  (= falseResult (V 0))
  (= falseResult notTrueResult))

(check
  (= trueResult (V 1))
  (= trueResult notFalseResult))

Since these expressions agree on two inputs, our extensional equality rules should make them equal:

(check (= FALSE notTrue))

(check (= TRUE notFalse))

Output…

I’ve written the notTrue and notFalse code into separate files. Here’s the output from the notTrue examples:

[INFO ] Declared sort Com.
[INFO ] Declared function App.
[INFO ] Declared function C.
[INFO ] Declared ruleset reduce.
[INFO ] Declared rule (rewrite (App (App K x) y) x).
[INFO ] Declared rule (rewrite (App (App (App S x) y) z) (App (App x z) (App y z))).
[INFO ] Declared function V.
[INFO ] Declared ruleset symbols.
[INFO ] Declared function bumpSymbols.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (V n)) (V (+ n 1))).
[INFO ] Declared function symbolicArgCount.
[INFO ] Declared rule (rule ((= (bumpSymbols x) x))
          ((set (symbolicArgCount x) 0))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared ruleset extensional.
[INFO ] Declared rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))
           (= (symbolicArgCount x) (symbolicArgCount y)))
          ((union x y))
             ).
[INFO ] Declared ruleset ignored.
[INFO ] Declared function ignoresArg.
[INFO ] Declared rule (rule ((App K x))
          ((ignoresArg (App K x)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App (bumpSymbols f) (V 0))))
          ((ignoresArg (App S f)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App f x))
           (App S f))
          ((App (bumpSymbols f) (V 0)))
             ).
[INFO ] Declared rule (rule ((ignoresArg x)
           (ignoresArg y)
           (App (App S x) y))
          ((ignoresArg (App (App S x) y)))
             ).
[INFO ] Declared rule (rule ((= x (App f a))
           (= y (App f b))
           (ignoresArg f))
          ((union x y))
             ).
[INFO ] Ran schedule (seq (repeat 10 (seq (seq (run reduce) (run symbols) (run extensional) (run ignored))))).
[INFO ] Report: Rule (rule ((= rewrite_var__ (App (App K x) y)))       ((union rewrite_var__ x))     ...: search 0.001s, apply 0.000s, num matches 59
    Rule (rule ((= rewrite_var__ (bumpSymbols (C x))))       ((union rewrite_var__ (C x))...: search 0.000s, apply 0.000s, num matches 5
    Rule (rule ((ignoresArg x)        (ignoresArg y)        (App (App S x) y))       ((ig...: search 0.001s, apply 0.000s, num matches 2
    Rule (rule ((= (bumpSymbols x) x))       ((set (symbolicArgCount x) 0))          ): search 0.000s, apply 0.000s, num matches 27
    Rule (rule ((ignoresArg (App f x))        (App S f))       ((App (bumpSymbols f) (V 0...: search 0.001s, apply 0.000s, num matches 51
    Rule (rule ((= n (symbolicArgCount x))        (App x y))       ((set (symbolicArgCoun...: search 0.001s, apply 0.000s, num matches 203
    Rule (rule ((ignoresArg (App (bumpSymbols f) (V 0))))       ((ignoresArg (App S f))) ...: search 0.001s, apply 0.000s, num matches 7
    Rule (rule ((= rewrite_var__ (App (App (App S x) y) z)))       ((union rewrite_var__ ...: search 0.001s, apply 0.000s, num matches 150
    Rule (rule ((= rewrite_var__ (C x)))       ((union rewrite_var__ (bumpSymbols (C x)))...: search 0.000s, apply 0.000s, num matches 6
    Rule (rule ((= n (symbolicArgCount x))        (App x y)        (= v0___ (+ 1 n)))    ...: search 0.001s, apply 0.000s, num matches 203
    Rule (rule ((= x (App f a))        (= y (App f b))        (ignoresArg f))       ((uni...: search 0.001s, apply 0.000s, num matches 1281
    Rule (rule ((= rewrite_var__ (bumpSymbols (V n))))       ((union rewrite_var__ (V (+ ...: search 0.002s, apply 0.000s, num matches 3
    Rule (rule ((= rewrite_var__ (App (bumpSymbols x) (bumpSymbols y)))        (bumpSymbo...: search 0.002s, apply 0.000s, num matches 106
    Rule (rule ((= rewrite_var__ (bumpSymbols (App x y)))        (bumpSymbols x)        (...: search 0.002s, apply 0.000s, num matches 85
    Rule (rule ((App K x))       ((ignoresArg (App K x)))          ): search 0.000s, apply 0.008s, num matches 30
    Rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))        (= (sy...: search 0.020s, apply 0.000s, num matches 39
    Ruleset extensional: search 0.020s, apply 0.000s, rebuild 0.000s
    Ruleset ignored: search 0.004s, apply 0.009s, rebuild 0.000s
    Ruleset reduce: search 0.002s, apply 0.000s, rebuild 0.000s
    Ruleset symbols: search 0.007s, apply 0.001s, rebuild 0.000s
    
[INFO ] Checked fact [Fact(Call((), Primitive(SpecializedPrimitive { primitive: Prim(!=), input: [EqSort { name: "Com" }, EqSort { name: "Com" }], output: UnitSort { name: "Unit" } }), [Var((), ResolvedVar { name: "TRUE", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "FALSE", sort: EqSort { name: "Com" } })]))].
[INFO ] Checked fact [Eq([Var((), ResolvedVar { name: "falseResult", sort: EqSort { name: "Com" } }), Call((), Func(FuncType { name: "V", input: [I64Sort { name: "i64" }], output: EqSort { name: "Com" }, is_datatype: true, has_default: false }), [Lit((), Int(0))])]), Eq([Var((), ResolvedVar { name: "falseResult", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "notTrueResult", sort: EqSort { name: "Com" } })])].
[INFO ] Checked fact [Eq([Var((), ResolvedVar { name: "FALSE", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "notTrue", sort: EqSort { name: "Com" } })])].

Here’s the output for notFalse

[INFO ] Declared sort Com.
[INFO ] Declared function App.
[INFO ] Declared function C.
[INFO ] Declared ruleset reduce.
[INFO ] Declared rule (rewrite (App (App K x) y) x).
[INFO ] Declared rule (rewrite (App (App (App S x) y) z) (App (App x z) (App y z))).
[INFO ] Declared function V.
[INFO ] Declared ruleset symbols.
[INFO ] Declared function bumpSymbols.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (V n)) (V (+ n 1))).
[INFO ] Declared function symbolicArgCount.
[INFO ] Declared rule (rule ((= (bumpSymbols x) x))
          ((set (symbolicArgCount x) 0))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared ruleset extensional.
[INFO ] Declared rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))
           (= (symbolicArgCount x) (symbolicArgCount y)))
          ((union x y))
             ).
[INFO ] Declared ruleset ignored.
[INFO ] Declared function ignoresArg.
[INFO ] Declared rule (rule ((App K x))
          ((ignoresArg (App K x)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App (bumpSymbols f) (V 0))))
          ((ignoresArg (App S f)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App f x))
           (App S f))
          ((App (bumpSymbols f) (V 0)))
             ).
[INFO ] Declared rule (rule ((ignoresArg x)
           (ignoresArg y)
           (App (App S x) y))
          ((ignoresArg (App (App S x) y)))
             ).
[INFO ] Declared rule (rule ((= x (App f a))
           (= y (App f b))
           (ignoresArg f))
          ((union x y))
             ).
[INFO ] Ran schedule (seq (repeat 10 (seq (seq (run reduce) (run symbols) (run extensional) (run ignored))))).
[INFO ] Report: Rule (rule ((= rewrite_var__ (App (App K x) y)))       ((union rewrite_var__ x))     ...: search 0.000s, apply 0.000s, num matches 49
    Rule (rule ((= rewrite_var__ (bumpSymbols (C x))))       ((union rewrite_var__ (C x))...: search 0.000s, apply 0.000s, num matches 5
    Rule (rule ((ignoresArg x)        (ignoresArg y)        (App (App S x) y))       ((ig...: search 0.001s, apply 0.000s, num matches 5
    Rule (rule ((= (bumpSymbols x) x))       ((set (symbolicArgCount x) 0))          ): search 0.000s, apply 0.000s, num matches 27
    Rule (rule ((ignoresArg (App (bumpSymbols f) (V 0))))       ((ignoresArg (App S f))) ...: search 0.001s, apply 0.000s, num matches 6
    Rule (rule ((= rewrite_var__ (bumpSymbols (V n))))       ((union rewrite_var__ (V (+ ...: search 0.000s, apply 0.000s, num matches 3
    Rule (rule ((= n (symbolicArgCount x))        (App x y))       ((set (symbolicArgCoun...: search 0.000s, apply 0.000s, num matches 131
    Rule (rule ((ignoresArg (App f x))        (App S f))       ((App (bumpSymbols f) (V 0...: search 0.001s, apply 0.000s, num matches 24
    Rule (rule ((App K x))       ((ignoresArg (App K x)))          ): search 0.000s, apply 0.000s, num matches 24
    Rule (rule ((= rewrite_var__ (C x)))       ((union rewrite_var__ (bumpSymbols (C x)))...: search 0.000s, apply 0.000s, num matches 6
    Rule (rule ((= n (symbolicArgCount x))        (App x y)        (= v0___ (+ 1 n)))    ...: search 0.001s, apply 0.000s, num matches 131
    Rule (rule ((= rewrite_var__ (App (bumpSymbols x) (bumpSymbols y)))        (bumpSymbo...: search 0.001s, apply 0.000s, num matches 67
    Rule (rule ((= rewrite_var__ (App (App (App S x) y) z)))       ((union rewrite_var__ ...: search 0.001s, apply 0.000s, num matches 55
    Rule (rule ((= x (App f a))        (= y (App f b))        (ignoresArg f))       ((uni...: search 0.001s, apply 0.000s, num matches 263
    Rule (rule ((= rewrite_var__ (bumpSymbols (App x y)))        (bumpSymbols x)        (...: search 0.001s, apply 0.000s, num matches 72
    Rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))        (= (sy...: search 0.006s, apply 0.000s, num matches 47
    Ruleset extensional: search 0.006s, apply 0.000s, rebuild 0.000s
    Ruleset ignored: search 0.004s, apply 0.000s, rebuild 0.000s
    Ruleset reduce: search 0.002s, apply 0.000s, rebuild 0.000s
    Ruleset symbols: search 0.004s, apply 0.001s, rebuild 0.000s
    
[INFO ] Checked fact [Fact(Call((), Primitive(SpecializedPrimitive { primitive: Prim(!=), input: [EqSort { name: "Com" }, EqSort { name: "Com" }], output: UnitSort { name: "Unit" } }), [Var((), ResolvedVar { name: "TRUE", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "FALSE", sort: EqSort { name: "Com" } })]))].
[INFO ] Checked fact [Eq([Var((), ResolvedVar { name: "trueResult", sort: EqSort { name: "Com" } }), Call((), Func(FuncType { name: "V", input: [I64Sort { name: "i64" }], output: EqSort { name: "Com" }, is_datatype: true, has_default: false }), [Lit((), Int(1))])]), Eq([Var((), ResolvedVar { name: "trueResult", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "notFalseResult", sort: EqSort { name: "Com" } })])].
[INFO ] Checked fact [Eq([Var((), ResolvedVar { name: "TRUE", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "notFalse", sort: EqSort { name: "Com" } })])].

AND

Here is boolean AND:

(let AND (App (App S S) (App K (App K FALSE))))

We can specify its behaviour on four arguments: if the first two are TRUE, it returns the third (i.e. it equals TRUE); otherwise it returns the fourth (equalling FALSE). Thanks to extensional equality, we can test this using only values of the first argument:

(let andTrue  (App AND TRUE ))
(let andFalse (App AND FALSE))

(App (App (App andFalse (V 2)) (V 1)) (V 0))
(App (App (App andTrue  (V 2)) (V 1)) (V 0))

(run-schedule (repeat 10 (seq reduce symbols extensional ignored)))

To see this, notice that the behaviour of andFalse does not depend on its next argument: it will always act like FALSE, and hence andFalse should equal (App K FALSE):

(check (= (App K FALSE) andFalse))

Likewise, the behaviour of andTrue is entirely determined by its next argument: hence it should be equal to I:

(check (= I andTrue))

Output…

[INFO ] Declared sort Com.
[INFO ] Declared function App.
[INFO ] Declared function C.
[INFO ] Declared ruleset reduce.
[INFO ] Declared rule (rewrite (App (App K x) y) x).
[INFO ] Declared rule (rewrite (App (App (App S x) y) z) (App (App x z) (App y z))).
[INFO ] Declared function V.
[INFO ] Declared ruleset symbols.
[INFO ] Declared function bumpSymbols.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (V n)) (V (+ n 1))).
[INFO ] Declared function symbolicArgCount.
[INFO ] Declared rule (rule ((= (bumpSymbols x) x))
          ((set (symbolicArgCount x) 0))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared ruleset extensional.
[INFO ] Declared rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))
           (= (symbolicArgCount x) (symbolicArgCount y)))
          ((union x y))
             ).
[INFO ] Declared ruleset ignored.
[INFO ] Declared function ignoresArg.
[INFO ] Declared rule (rule ((App K x))
          ((ignoresArg (App K x)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App (bumpSymbols f) (V 0))))
          ((ignoresArg (App S f)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App f x))
           (App S f))
          ((App (bumpSymbols f) (V 0)))
             ).
[INFO ] Declared rule (rule ((ignoresArg x)
           (ignoresArg y)
           (App (App S x) y))
          ((ignoresArg (App (App S x) y)))
             ).
[INFO ] Declared rule (rule ((= x (App f a))
           (= y (App f b))
           (ignoresArg f))
          ((union x y))
             ).
[INFO ] Ran schedule (seq (repeat 10 (seq (seq (run reduce) (run symbols) (run extensional) (run ignored))))).
[INFO ] Report: Rule (rule ((= rewrite_var__ (C x)))       ((union rewrite_var__ (bumpSymbols (C x)))...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((= rewrite_var__ (bumpSymbols (C x))))       ((union rewrite_var__ (C x))...: search 0.000s, apply 0.000s, num matches 2
    Rule (rule ((= rewrite_var__ (bumpSymbols (V n))))       ((union rewrite_var__ (V (+ ...: search 0.000s, apply 0.000s, num matches 3
    Rule (rule ((App K x))       ((ignoresArg (App K x)))          ): search 0.000s, apply 0.000s, num matches 20
    Rule (rule ((ignoresArg (App f x))        (App S f))       ((App (bumpSymbols f) (V 0...: search 0.001s, apply 0.000s, num matches 46
    Rule (rule ((= n (symbolicArgCount x))        (App x y))       ((set (symbolicArgCoun...: search 0.001s, apply 0.000s, num matches 184
    Rule (rule ((ignoresArg x)        (ignoresArg y)        (App (App S x) y))       ((ig...: search 0.001s, apply 0.000s, num matches 3
    Rule (rule ((= rewrite_var__ (App (App (App S x) y) z)))       ((union rewrite_var__ ...: search 0.001s, apply 0.000s, num matches 131
    Rule (rule ((= (bumpSymbols x) x))       ((set (symbolicArgCount x) 0))          ): search 0.000s, apply 0.000s, num matches 22
    Rule (rule ((= n (symbolicArgCount x))        (App x y)        (= v0___ (+ 1 n)))    ...: search 0.001s, apply 0.000s, num matches 184
    Rule (rule ((= rewrite_var__ (bumpSymbols (App x y)))        (bumpSymbols x)        (...: search 0.001s, apply 0.000s, num matches 112
    Rule (rule ((ignoresArg (App (bumpSymbols f) (V 0))))       ((ignoresArg (App S f))) ...: search 0.003s, apply 0.000s, num matches 6
    Rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))        (= (sy...: search 0.004s, apply 0.000s, num matches 39
    Rule (rule ((= x (App f a))        (= y (App f b))        (ignoresArg f))       ((uni...: search 0.006s, apply 0.000s, num matches 1455
    Rule (rule ((= rewrite_var__ (App (bumpSymbols x) (bumpSymbols y)))        (bumpSymbo...: search 0.010s, apply 0.000s, num matches 117
    Rule (rule ((= rewrite_var__ (App (App K x) y)))       ((union rewrite_var__ x))     ...: search 0.011s, apply 0.000s, num matches 98
    Ruleset extensional: search 0.004s, apply 0.000s, rebuild 0.000s
    Ruleset ignored: search 0.011s, apply 0.007s, rebuild 0.000s
    Ruleset reduce: search 0.012s, apply 0.000s, rebuild 0.000s
    Ruleset symbols: search 0.014s, apply 0.001s, rebuild 0.000s
    
[INFO ] Checked fact [Eq([Call((), Func(FuncType { name: "App", input: [EqSort { name: "Com" }, EqSort { name: "Com" }], output: EqSort { name: "Com" }, is_datatype: true, has_default: false }), [Var((), ResolvedVar { name: "K", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "FALSE", sort: EqSort { name: "Com" } })]), Var((), ResolvedVar { name: "andFalse", sort: EqSort { name: "Com" } })])].
[INFO ] Checked fact [Eq([Var((), ResolvedVar { name: "I", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "andTrue", sort: EqSort { name: "Com" } })])].

OR

We can characterise boolean OR in a similar way:

(let OR (App (App S I) (App K TRUE)))

(let orTrue  (App OR  TRUE ))
(let orFalse (App OR  FALSE))

(App (App (App orTrue  (V 2)) (V 1)) (V 0))
(App (App (App orFalse (V 2)) (V 1)) (V 0))

(run-schedule (saturate reduce symbols extensional))

This time, orTrue ignores its next argument:

(check (= (App K TRUE) orTrue))

Whilst orFalse depends entirely on its next argument:

(check (= I orFalse))

Output…

[INFO ] Declared sort Com.
[INFO ] Declared function App.
[INFO ] Declared function C.
[INFO ] Declared ruleset reduce.
[INFO ] Declared rule (rewrite (App (App K x) y) x).
[INFO ] Declared rule (rewrite (App (App (App S x) y) z) (App (App x z) (App y z))).
[INFO ] Declared function V.
[INFO ] Declared ruleset symbols.
[INFO ] Declared function bumpSymbols.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (App x y)) (App (bumpSymbols x) (bumpSymbols y)) :when ((bumpSymbols x) (bumpSymbols y)))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))=>.
[INFO ] Declared rule (rewrite (bumpSymbols (C x)) (C x))<=.
[INFO ] Declared rule (rewrite (bumpSymbols (V n)) (V (+ n 1))).
[INFO ] Declared function symbolicArgCount.
[INFO ] Declared rule (rule ((= (bumpSymbols x) x))
          ((set (symbolicArgCount x) 0))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared rule (rule ((= n (symbolicArgCount x))
           (App x y))
          ((set (symbolicArgCount (App (bumpSymbols x) (V 0))) (+ 1 n)))
             ).
[INFO ] Declared ruleset extensional.
[INFO ] Declared rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))
           (= (symbolicArgCount x) (symbolicArgCount y)))
          ((union x y))
             ).
[INFO ] Declared ruleset ignored.
[INFO ] Declared function ignoresArg.
[INFO ] Declared rule (rule ((App K x))
          ((ignoresArg (App K x)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App (bumpSymbols f) (V 0))))
          ((ignoresArg (App S f)))
             ).
[INFO ] Declared rule (rule ((ignoresArg (App f x))
           (App S f))
          ((App (bumpSymbols f) (V 0)))
             ).
[INFO ] Declared rule (rule ((ignoresArg x)
           (ignoresArg y)
           (App (App S x) y))
          ((ignoresArg (App (App S x) y)))
             ).
[INFO ] Declared rule (rule ((= x (App f a))
           (= y (App f b))
           (ignoresArg f))
          ((union x y))
             ).
[INFO ] Ran schedule (seq (saturate (seq (run reduce) (run symbols) (run extensional)))).
[INFO ] Report: Rule (rule ((= (bumpSymbols x) x))       ((set (symbolicArgCount x) 0))          ): search 0.000s, apply 0.000s, num matches 16
    Rule (rule ((= n (symbolicArgCount x))        (App x y))       ((set (symbolicArgCoun...: search 0.000s, apply 0.000s, num matches 82
    Rule (rule ((= rewrite_var__ (bumpSymbols (V n))))       ((union rewrite_var__ (V (+ ...: search 0.000s, apply 0.000s, num matches 3
    Rule (rule ((= rewrite_var__ (bumpSymbols (C x))))       ((union rewrite_var__ (C x))...: search 0.000s, apply 0.000s, num matches 5
    Rule (rule ((= rewrite_var__ (C x)))       ((union rewrite_var__ (bumpSymbols (C x)))...: search 0.000s, apply 0.000s, num matches 6
    Rule (rule ((= rewrite_var__ (App (App (App S x) y) z)))       ((union rewrite_var__ ...: search 0.001s, apply 0.000s, num matches 42
    Rule (rule ((= (App (bumpSymbols x) (V 0)) (App (bumpSymbols y) (V 0)))        (= (sy...: search 0.003s, apply 0.000s, num matches 27
    Rule (rule ((= rewrite_var__ (App (App K x) y)))       ((union rewrite_var__ x))     ...: search 0.003s, apply 0.000s, num matches 53
    Rule (rule ((= n (symbolicArgCount x))        (App x y)        (= v0___ (+ 1 n)))    ...: search 0.004s, apply 0.000s, num matches 82
    Rule (rule ((= rewrite_var__ (bumpSymbols (App x y)))        (bumpSymbols x)        (...: search 0.004s, apply 0.000s, num matches 63
    Rule (rule ((= rewrite_var__ (App (bumpSymbols x) (bumpSymbols y)))        (bumpSymbo...: search 0.006s, apply 0.000s, num matches 61
    Ruleset extensional: search 0.003s, apply 0.000s, rebuild 0.000s
    Ruleset reduce: search 0.004s, apply 0.000s, rebuild 0.000s
    Ruleset symbols: search 0.016s, apply 0.001s, rebuild 0.000s
    
[INFO ] Checked fact [Eq([Call((), Func(FuncType { name: "App", input: [EqSort { name: "Com" }, EqSort { name: "Com" }], output: EqSort { name: "Com" }, is_datatype: true, has_default: false }), [Var((), ResolvedVar { name: "K", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "TRUE", sort: EqSort { name: "Com" } })]), Var((), ResolvedVar { name: "orTrue", sort: EqSort { name: "Com" } })])].
[INFO ] Checked fact [Eq([Var((), ResolvedVar { name: "I", sort: EqSort { name: "Com" } }), Var((), ResolvedVar { name: "orFalse", sort: EqSort { name: "Com" } })])].

Conclusion

I’ve finally achieved what I wanted from my first foray into egglog: an encoding of SK combinatory logic which can automatically discover extensional equality. It took a few attempts and a bit of head-scratching, to discover that our naïve symbolic execution was making inconsistent inferences; and to come up with a symbol-counting mechanism to avoid this.

Overall I’m quite happy, since I’ve learned a bit more about SK, symbolic execution and the treatment of free variables. I’ve also learned a lot about egglog, and this experience has sharpened some of the vague ideas I’d been considering for it. Hopefully I can get something more “serious” working in the not-too-distant future!