Fork me on GitHub
#meander
<
2022-04-06
>
jgdavey14:04:50

Looking through the logs for an elegant to pull up (simplify) nested boolean logic. For example, a program like this:

``(and aa (and bb cc) dd (or ee (and ff))``
would simplify to:
``(and aa bb cc dd (or ee ff))``

jgdavey14:04:26

``````(m/rewrite
program

;; single arg and/or unnest
((m/or and or) ?single-arg)
?single-arg

;; pull up nested ands, recursively
(and . (m/or (m/cata (and . !arg ...)) (m/cata !arg)) ...)
(and . !arg ...)

;; recurse
((m/cata !x) ...)
(!x ...)

;; stop
?x ?x)``````
Maybe something like this? ^

Jimmy Miller14:04:21

Something like that could probably work. When I’ve made logic simplifiers in the past, I always followed a structure like this. Made it nice and explicit what the rules for simplification were imo.

``````(defn reduce-logic [prop]
(m/rewrite prop
(or true ?x) true
(or ?x true) true
(or false ?x) ?x
(or ?x false) ?x
?x ?x))

(defn recursive-reduce [prop]
(m/match prop
(?op ?x ?y) (reduce-logic (list ?op (recursive-reduce ?x) (recursive-reduce ?y)))
(?op ?x) (reduce-logic (list ?op (recursive-reduce ?x)))
?x ?x))

(recursive-reduce '(or true true))
(recursive-reduce '(or true x))
(recursive-reduce '(or false x))
(recursive-reduce '(or (or (or false false) x) false))
(recursive-reduce '(or (or (or true false) x) false))``````

Jimmy Miller14:04:08

I have some haskell code that uses this exact structure, just with more rules https://github.com/jimmyhmiller/PlayGround/blob/master/logic.hs

jgdavey14:04:03

Oh, nice, I dig the explicit recursion. Seems easy to follow

Jimmy Miller14:04:17

Yeah, that is always the tricky bit is not infinite looping. This structure prevents you from having to think about that. In, fact I actually have an unnecessary cata. Let me remove that

Jimmy Miller14:04:08

Yeah, so everything in reduce-logic does not recurse at all. It is just the basic rules for simplification.