Lösung

[1unitedpower]

@Rolf B hat die Aufgabe sehr elegant gelöst. Meine eigene Lösung stinkt dagegen ziemlich ab.

Meine Lösung basiert auf einer binaryIncrement-Funktion, die eine binäre Zahl um 1 erhöht.

function unaryToBinary(n: UNat) : BNat {
  return (n.tag === 'zero') ? zero : binaryIncrement(unaryToBinary(n.pred))
}

Für die binaryIncrement Funktion brauchte ich zwei Helfer-Funktionen. Die erste Funktion testet, ob alle Ziffern b1 sind. In dem Fall muss bei der Addition nämlich eine neue Ziffer am Anfang hinzugefügt werden.

function binaryOverflow(n : BNat) : boolean {
  return (n.tag === 'zero') ? true :
         (n.tag === 'B0')   ? false :
         /*n.tag === 'B1'*/   binaryOverflow(n.pred)
}

Die zweite Helfer-Funktion setzt alle Ziffern einer Binärzahl auf b0.

function binaryNullify(n: BNat) : BNat {
  return (n.tag === 'zero') ? zero : b0(binaryNullify(n.pred))
}

Die Additions-Funktion muss dann vier Fälle unterscheiden:

function binaryIncrement(n : BNat) : BNat {
  return (binaryOverflow(n)) ? b1(binaryNullify(n)) :
         (n.tag === 'B0' && binaryOverflow(n.pred)) ? b1(n.pred) :
         (n.tag === 'B0') ? b0(binaryIncrement(n.pred)) :
         (n.tag === 'B1') ? b1(binaryIncrement(n.pred)) : undefined
}

Das ist sozusagen die Grundschulmethode. Sie ist nicht besonders effizient, weil sich bei der Addition mit Eins im schlimmsten Fall alle Ziffern ändern können. Die Addition mit 1 ist also keine konstante Operation, sondern brauch O(log(n)). Die Gesamtlaufzeit der Konvertierung liegt deshalb bei O(n * log(n)).

---

@Rolf B hat einen Linear-Laufzeit-Algorithmus implementiert, der nicht auf der Addition mit 1 basiert, sondern auf der Multiplikation mit 2.

Dafür hat er zunächst eine Helfer-Funktion geschrieben, die eine unäre Zahl durch 2 teilt und sich den Rest der Division merkt.

type UQuotRem = { q: UNat, r: UNat } // Ergebnistyp einer Division mit Rest


function halfValue(n : UNat) : UQuotRem  {
  if (n.tag === 'zero')
    return { q: zero, r: zero };

  if (n.pred.tag === 'zero')
    return { q: zero, r: u0(zero)};

  const half = halfValue(n.pred.pred);
  return { q: u0(half.q), r: half.r}
}

Die unary2binary-Funktion sah dann wie folgt aus.

function unaryToBinary(n: UNat) : BNat {
  return u2b(zero, n);

  function u2b(b: BNat, u: UNat) : BNat {
    if (u.tag === 'zero')
      return b;

    const half = halfValue(u);
    return (half.r.tag === 'zero') ?
              u2b(b0(b), half.q) :      // u war gerade
              u2b(b1(b), half.q);       // u war ungerade
  }
}

Der Vorteil ist ganz klar, dass die Mulitplikation mit 2 eine konstante Operation für die binären Zahlen ist. So ergibt sich für Rolfs Lösung eine Gesamtlaufzeit für die Konvertierung von O(n).