Part 3 continues with Haskell, looking at the statistics of our property checks and tweaks them to explore more thoroughly. Eventually the problem was uncovered: allowing symbolic/meta variables to occur inside the expressions we were checking for equality http://www.chriswarbo.net/blog/2024-04-02-sk_logic_in_egglog...
Part 4 takes these lessons back to egglog, to give a sound implementation of extensional equality; showing how it can be used for higher-level reasoning, with an example of Church-encoded boolean operators http://www.chriswarbo.net/blog/2024-05-10-sk_logic_in_egglog...
Part 1 (TFA) is an intro to Egglog, with both a trivial example and an ordinary SK/combinatory logic implementation (a la functional programming) http://www.chriswarbo.net/blog/2024-02-25-sk_logic_in_egglog...
Part 2 switches to Haskell, to investigate a problem in my egglog implementation of extensional-equality, explaining the symbolic execution approach it was based on http://www.chriswarbo.net/blog/2024-03-17-sk_logic_in_egglog...
Part 3 continues with Haskell, looking at the statistics of our property checks and tweaks them to explore more thoroughly. Eventually the problem was uncovered: allowing symbolic/meta variables to occur inside the expressions we were checking for equality http://www.chriswarbo.net/blog/2024-04-02-sk_logic_in_egglog...
Part 4 takes these lessons back to egglog, to give a sound implementation of extensional equality; showing how it can be used for higher-level reasoning, with an example of Church-encoded boolean operators http://www.chriswarbo.net/blog/2024-05-10-sk_logic_in_egglog...