[HN Gopher] SK Logic in Egglog
       ___________________________________________________________________
        
       SK Logic in Egglog
        
       Author : chriswarbo
       Score  : 8 points
       Date   : 2024-05-10 11:04 UTC (1 days ago)
        
 (HTM) web link (www.chriswarbo.net)
 (TXT) w3m dump (www.chriswarbo.net)
        
       | chriswarbo wrote:
       | 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...
        
       ___________________________________________________________________
       (page generated 2024-05-11 23:01 UTC)