Aussagenlogische Formel Implikation Umformen mit Everywhere

In dieser Aufgabe verwenden wir einige Vorschau Eigenschaften aus Java 15.

Gegeben sei ein Datentyp für aussagenlogische Formeln.

public interface Logic{
  static record Var(String n) implements Logic{}
  static record Neg(Logic f) implements Logic{}
  static record Implication(Logic l,Logic r) implements Logic{}
  static record And(Logic l,Logic r) implements Logic{}
  static record Or(Logic l,Logic r) implements Logic{}

Innerhalb der Schnittstelle für logische Formeln gibt es jetzt zusätzlich eine Methode, die in der Lage ist, alle Teilformeln in der dargestellten Formel durch eine Funktionsanwendung zu ersetzen:

  default Logic everywhere(Function<Logic,Logic> f){
    var result = f.apply(this);
    if (result instanceof Neg n) return f.apply(new Neg(n.f.everywhere(f)));
    if (result instanceof Or n) return  f.apply(new Or(n.l.everywhere(f),n.r.everywhere(f)));
    if (result instanceof And n) return f.apply(new And(n.l.everywhere(f),n.r.everywhere(f)));
    if (result instanceof Implication n) return f.apply(new Implication(n.l.everywhere(f),n.r.everywhere(f)));
    if (result instanceof Var v) return v;
    throw new RuntimeException("unknown Logic class: "+this);
  }
}

Implementieren Sie die Methode zur Ersetzung von Implikationen in Disjunktionen nach der bekannten Umformung (A → B) wird zu (¬A ∨ B), indem Sie mit Hilfe der Methode everywhere eine Funktion, die Implikationen auf top-level Ebene in eine Disjunktion umwandelt.

Jetzt brauchen Sie also nicht mehr rekursiv in die Teilformeln zu schauen. Dieses macht die Methode everywhere dann für Sie.