I think I can help rephrase the problem so it can help other people provide their solutions:
giving the following rewriting rules
+(x, [] y) --> [] (=>(x, y))
implement a (probably OCaml) program that rewrites an input form until no further rewrites can be applied and output it.
an example trace of execution is
+(p,+(q,[] z)) --> +(p, [](=>(q, z))) --> [](=>(p,=>(q,z)))
Here’s my personal comments:
I think a naive solution is having a recursive function does the pattern match and rewriting, and apply it until the result stays the same.
And welcome to ocaml discuss!
probably more context on the problem can be helpful, I guess this is some kind of logical formulas, but I’m not a proper logician so I cannot identify what kind of logical system these symbols are from.