interp: convert unary bu and serial-head bu to ¬

[eaburns]

Unary bu is negation if it's argument is an abstraction or if it's the head of a serial. We should convert it to a new Not node in the logic tree and print it using ¬.

[uakci]

That would sure be a nice thing to have, but that's not the way I'd go about doing it. Instead, I'd follow this 3-step plan:

1. Implement serial predicate expansion. (It isn't that hard, but it might be hard to integrate with the rest of the system.)
2. Expand the simplification algorithm with a map from strings to functions which map arrays of variable values to ASTs.
3. Simplify, simplify, simplify. (Apply transformations until the predicate of the predication isn't a key in the map, then descend recursively.)

To elaborate on (2.): the map would have regular predicate keys like "bu" which would map to functions like (for the example of unary bu) ‘if the first argument is a proposition, unpack it and wrap it in Not{}; otherwise, leave unchanged.’ (‘Leaving unchanged’ would be the mechanism for signalling to stop expanding/simplifying.) We could have similar transformations for mu, te, jeo (when x₂ is a verbatim property)…

[eaburns]

If I understand, your 2 is a generalization of bu expansion, allowing to add more expansions of other predicates. That sounds fine to me. I think we should treat this as orthogonal to serial predicate expansion, which I do agree we should also do (probably behind a flag to turn it on and off).

[uakci]

Yes, your understanding is correct. (Sorry, I was in a hurry and didn't have the time to write clearly.) It would also be more implementationally transparent than 200-line-long procedures like:

func simplify(stuff *Stuff) Things {
  switch stuff.predicate {
    case "bu":
      return simplify(simplifyBu(stuff))
    case "mu":
      return simplify(simplifyMu(stuff))
    … (149 more cases)
}

:) Currently fighting at the serial expander front.