Informatik zum Dienstag

[1unitedpower]

Ich arbeite gerade an einer kleinen Programmiersprache, die keine Datentypen für Zahlen kennt. Aber man kann sie innerhalb der Sprache definieren. Bspw. wie die Peano-Zahlen:

1. 0 kodiert eine natürliche Zahl.
2. Falls n eine natürliche Zahl kodiert, so auch u0(n).

Das entspricht der unären Kodierung einer Zahl. Die Zahl 3 wird bspw. durch u0(u0(u0(0))) kodiert. Das Symbol u0 repräsentiert die einzige Ziffer des unären Zahlensystems. Es ist wichtig zwischen der Ziffer u0 und dem Terminal-Symbol 0 zu unterscheiden.

Nun ist die unäre Kodierung nicht besonders Speicher- oder Rechen-freundlich. Deshalb möchte man unäre Zahlen manchmal in die Binärdarstellung bringen bevor man damit rechnet. Eine Definition könnte bspw. so lauten:

1. 0 kodiert eine natürliche Zahl.
2. Falls n eine natürliche Zahl kodiert, so auch b0(n) und b1(n).

Die Zahl 5 wird bspw. durch b1(b0(b1(0))) kodiert. b1 entspricht der binären Ziffer 1 und b0 der binären Ziffer 0.

Die Aufgabe ist es, einen Algorithmus zu programmieren, der eine unär kodierte Zahl in eine Binärdarstellung umkodiert, ohne dabei auf die eingebauten Zahlendatentypen der Programmiersprache zurück zugreifen.

Ich habe bei Stackblitz eine TypeScript-Vorlage für die Aufgabe angelegt, die Funktion unaryToBinary muss noch mit leben gefüllt werden. Die Vorlage enthält bereits Definitionen für das Terminal-Symbol 0 und die unären und binären Ziffern.

const zero = {tag: 'zero'} // Das Terminal-Symbol 0

const u0 = (pred) => ({tag: 'U0', pred}) // Die unäre Ziffer 0

const b0 = (pred) => ({tag: 'B0', pred}) // Die binäre Ziffer 0
const b1 = (pred) => ({tag: 'B1', pred}) // Die binäre Ziffer 1


// Beispiele
const unaryThree = u0(u0(u0(zero)))
const binaryFive = b1(b0(b1(zero)))

Außerdem enthält die Vorlage einige Helferfunktionen und ein paar Typ-Definitionen, die die Aufgabe einfacher machen sollen. Wer mit Typen nicht so viel anfangen kann, darf sie natürlich auch löschen.

[Rolf B]

Hallo 1unitedpower,

ohne deine Helferfunktionen wüsste man zu wenig.

Frage wäre gewesen: n sei die Binärcodierung einer natürlichen Zahl und val(n) der Zahlenwert dazu. Ist dann val(b0(n)) == val(n) oder val(b0(n)) == 2*val(n)? Meint: Setzt b0(n) ein neues most significant bit oder ein neues least significant. Dein Helper macht klar: es ist ersteres.

Frage ist aber auch: Ist die rekursive Darstellung der unären und binären Codierung vorgegeben? Oder darf ich auch eine andere Implementierung der Peano- oder Binärcodierung benutzen, solange ich dabei keine Zahlen verwende? Ich denke da an ein Array, auf das ich push, pop, shift oder unshift anwenden könnte.

Allgemeiner gefragt: Welchen Funktionsumfang hat deine zahlenlose Sprache? JavaScript minus Number? Oder noch weniger?

Und ich nehme mal an, dass binaryLength bei der Implementierung von unaryToBinary nicht als Helper zur Verfügung steht, gelle?

Rolf

[1unitedpower]

ohne deine Helferfunktionen wüsste man zu wenig.

Frage wäre gewesen: n sei die Binärcodierung einer natürlichen Zahl und val(n) der Zahlenwert dazu. Ist dann val(b0(n)) == val(n) oder val(b0(n)) == 2*val(n)? Meint: Setzt b0(n) ein neues most significant bit oder ein neues least significant. Dein Helper macht klar: es ist ersteres.

Stimmt, danke für die Ergänzung.

Frage ist aber auch: Ist die rekursive Darstellung der unären und binären Codierung vorgegeben? Oder darf ich auch eine andere Implementierung der Peano- oder Binärcodierung benutzen, solange ich dabei keine Zahlen verwende? Ich denke da an ein Array, auf das ich push, pop, shift oder unshift anwenden könnte.

Ich bin auch gespannt auf Lösungen mit alternativen Definitionen für die Kodierungen. Die Vorlage war eine reine Hilfestellung und muss nicht benutzt werden.

Allgemeiner gefragt: Welchen Funktionsumfang hat deine zahlenlose Sprache? JavaScript minus Number? Oder noch weniger?

Meine Sprache ist noch dramatisch reduzierter, sie ist ein rein akademisches Experiment, das würde hier aber zu weit führen. Sie dient als prototypsche Sprache, um die Curry-Howard Korrespondenz auf kombinatorische Logik auszuweiten. Das wäre von praktischem Nutzen für die Implementierung von Compilern für funktionale Programmiersprachen und (semi-)automatischen Beweisassistenten. Die Sprache eignet sich nicht wirklich, um darin zu programmieren, sie ist mehr eine Zwischensprache, wie WebAssembly oder die JVM, die unter der Haube von Programmiersprachen benutzt wird. Beim Entwickeln von Fallballbeispielen bin ich kürzlich auf dieses Problem der Umkodierungen gestoßten und dachte mir, das hat einen Rätsel-Charakter und könnte vielleicht jemanden aus dem Forum Spaß machen. Deshalb habe ich TypeScript/JavaScript als Sprache für die Aufgabe gewählt, weil damit wohl viele Selfler vertraut sind.

Und ich nehme mal an, dass binaryLength bei der Implementierung von unaryToBinary nicht als Helper zur Verfügung steht, gelle?

Korrekt, die Funktion benutzt ja unter der Haube JavaScript nativen number-Typen.

[Rolf B]

Hallo 1unitedpower,

ok, hab eine Lösung basierend auf deinen Typen.

Benutzte Sprachfeatures: Abfragen (if und ?:), Funktionsaufruf mit Parametern, Rekursion, Bilden von Tupeln, Test auf Gleichheit, Merken von Werten in const-Speicherplätzen. Das war's.

Alternative Implementierungen zu verwenden ist so eine Sache. Angesichts deiner u0/b0/b1 Funktionen, die die Werte definieren, ist die rekursive Konstruktion fast schon vorgegeben. Heute habe ich dafür keinen Nerv mehr.

Ich stolpere - rein logisch - vor allem über eine dusselige Eigenschaft von b0 (value als Shortcut für binaryToNumber):

Es ist: value(n) == value(b0(n)), d.h. b0(n) codiert die gleiche natürliche Zahl wie n.

Aber n und b0(n) sind nicht gleich, denn: value(b1(n)) != value(b1(b0(n)))

Hatten wir das Thema mit führenden Nullen, die Durcheinander anrichten, letztens nicht schonmal bei den milliardenstelligen Ziffernfolgen?

Am liebsten wäre mir ja, wenn diese Definitionen gelten würden, mit value(n) als der von n codierte Zahlenwert:

b0(zero)     := zero
value(b0(n)) := 2*value(n)
value(b1(n)) := 2*value(n)+1

Aber ob damit unaryTobinary so einfach realisierbar ist, hmmm. Spieglein, Spiegelein...

Rolf

[1unitedpower]

ok, hab eine Lösung basierend auf deinen Typen.

Sehr schöne Lösung übrigens. Mal wieder effizienter als meine eigene 😉

Ich stolpere - rein logisch - vor allem über eine dusselige Eigenschaft von b0 (value als Shortcut für binaryToNumber):

Es ist: value(n) == value(b0(n)), d.h. b0(n) codiert die gleiche natürliche Zahl wie n.

Aber n und b0(n) sind nicht gleich, denn: value(b1(n)) != value(b1(b0(n)))

Man könnte das Problem auch auf Typ-Ebene beseitigen, indem man die binären Zahlen so beschränkt, dass an der signifikanteste Position immer die Ziffer b1 stehen muss. Dann hätte man eine normalisierte, eindeutige Kodierung. In TypeScript:

type BNatSuffix = Zero | B0 | B1 // Binärzahlen mit potenziell führenden Nullen
type BNat = Zero | B1            // Normalisierte Binärzahlen

Die Definitionen müssten entsprechend angepasst werden.

Hatten wir das Thema mit führenden Nullen, die Durcheinander anrichten, letztens nicht schonmal bei den milliardenstelligen Ziffernfolgen?

Am liebsten wäre mir ja, wenn diese Definitionen gelten würden, mit value(n) als der von n codierte Zahlenwert:

b0(zero)     := zero
value(b0(n)) := 2*value(n)
value(b1(n)) := 2*value(n)+1

Das löst auf jeden Fall das Problem, dass du oben beschrieben hast (ich gehe mal davon aus, dass die erste Zeile value(zero) = 0 lauten sollte). Die Binärkodierung ist damit aber auch nicht eindeutig: Jede Zahl kann dann beliebig viele abschließende b0-Ziffern haben.

[Rolf B]

Hallo 1unitedpower,

ich gehe mal davon aus, dass die erste Zeile value(zero) = 0 lauten sollte

Hm. Darüber musste ich erstmal nachdenken. Mein b0(zero) := zero soll aussagen, dass ich eine Binärcodierung nicht mit einer 0 beginnen kann. Versuche ich es, passiert einfach nichts. Es verbietet allerdings auch die Konstruktion eines Codes für den Wert 0, das habe ich übersehen. Das ist bei deiner Typdefinition ebenfalls der Fall.

Die Binärkodierung ist damit aber auch nicht eindeutig

Das Witzige ist, dass die Forderung value(b0(n)) := 2*value(n) überhaupt nichts über die Art des Codes aussagt. Es verlangt nur, dass die Operation b0 einen Code liefert, dessen Wert dem Doppelten des Ausgangscodes entspricht. Das kann man dadurch implementieren, indem man an eine Binärzahl eine 0 anhängt. Oder anders, irgendwie, tief in einer Blackbox, z.b. unär codiert durch Verdoppeln der Ziffern. Aber nehmen wir an, b0 und b1 konstruieren eine Liste aus Einsen und Nullen. Dann kann ich eben nicht beliebig viele Nullen anhängen, ohne den Wert zu verändern.

Also lassen wir das, das ufert aus.

Rolf

[Rolf B]

Hallo 1unitedpower,

by the way braucht man binaryLength gar nicht. Das verleitet nur zum cheaten. Man muss nur binaryToNumber etwas umgestalten:

function binaryToNumber(n : BNat) : number {
  return b2n(0, n);

  function b2n(val: number, n: BNat) : number {
    if (n.tag === 'zero') return val;
    return b2n(2*val + (n.tag === 'B1' ? 1 : 0), n.pred);
  }
}

Die Abfrage n.tag === 'zero' statt n === zero hilft TypeScript bei der korrekten Typdiskriminierung. Ich könnte sonst n.pred nicht verwenden.

Warum hast Du eigentlich Zero, U0, B0 und B1 als interface definiert und nicht als type? Ich habe ja von TypeScript fast gar keine Ahnung...

Rolf

[1unitedpower]

Hallo 1unitedpower,

by the way braucht man binaryLength gar nicht. Das verleitet nur zum cheaten. Man muss nur binaryToNumber etwas umgestalten:

function binaryToNumber(n : BNat) : number {
  return b2n(0, n);

  function b2n(val: number, n: BNat) : number {
    if (n.tag === 'zero') return val;
    return b2n(2*val + (n.tag === 'B1' ? 1 : 0), n.pred);
  }
}

Sehr gut, gefällt mir wesentlich besser als meine eigene Implementierung. Du sparst nicht nur die wiederholte Berechnung der Länge, sondern hast auch noch einen tail-rekursiven Ansatz und sparst darurch Platz auf dem Callstack.

Die Abfrage n.tag === 'zero' statt n === zero hilft TypeScript bei der korrekten Typdiskriminierung. Ich könnte sonst n.pred nicht verwenden.

Seltsam, dass die Typ-Verfeinerung in einem Fall klappt und im anderen nicht.

Warum hast Du eigentlich Zero, U0, B0 und B1 als interface definiert und nicht als type? Ich habe ja von TypeScript fast gar keine Ahnung…

Da habe ich mir nichts bei gedacht, für die Vorlage ist das wohl äquivalent. Eine type-Deklaration wäre wohl sogar etwas schöner, weil intuitiver, gewesen.

[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).

[Rolf B]

Hallo 1unitedpower,

mit Komplexitätsbestimmungen bin ich auf Kriegsfuß. Es hat mich jetzt etwas Überlegung gekostet, warum eine Schachtelung von zwei Schleifen lineare Laufzeit haben sollte 🥴

Aber ist schon klar. Für die erste Binärziffer gibt's n/2 Durchläufe im Halbierer. Für die zweite sind es n/4, und so weiter, in Summe irgendwas zwischen n/2 und n.

Rolf

[1unitedpower]

Aber ist schon klar. Für die erste Binärziffer gibt's n/2 Durchläufe im Halbierer. Für die zweite sind es n/4, und so weiter, in Summe irgendwas zwischen n/2 und n.

Genau, die Summe n/2 + n/4 + n/8 + … konvergiert gegen n. Man kann sogar zeigen, dass dein Algorithmus hinsichtlich Laufzeit nicht zu überbieten ist. Wenn es einen Algorithmus mit geringerer Laufzeitschranke gäbe, würde er nicht alle Ziffern der Eingabe lesen, das heißt, er würde manche Eingaben nicht unterscheiden können und falsche Ergebnisse liefern (da die zu berechnende Funktion bijektiv ist). Für eine korrekte Lösung ist O(n) deshalb optimal.