SK Logic in Egglog

http://www.chriswarbo.net/blog/2024-02-25-sk_logic_in_egglog_1.html

by chriswarbo • 2 years ago

12 1 2 years ago

chriswarbo• 2 years ago

This ended up being four parts:

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...

SK Logic in Egglog

Related Stories