Die Subtraktion ist funktional vollständig | orlp.net

28.09.2023

Genauer gesagt ist die IEEE-754-Gleitkommasubtraktion funktional abgeschlossen. Das bedeutet, dass Sie jede binäre Schaltung nur mithilfe der Gleitkommasubtraktion erstellen können.

Um zu sehen, wie das geht, müssen wir ganz unten beginnen. Ich zitiere den IEEE 754-2019-Standard, Abschnitt 6.3:

6.3 Das Vorzeichenbit

[…] Wenn weder die Eingaben noch das Ergebnis NaN sind, […]; das Vorzeichen einer Summe oder einer als Summe $x+(−y)$ betrachteten Differenz $x−y$ unterscheidet sich höchstens von einem der Vorzeichen der Summanden; […]. Diese Regeln gelten auch dann, wenn Operanden oder Ergebnisse null oder unendlich sind.

Wenn die Summe zweier Operanden mit entgegengesetzten Vorzeichen (oder die Differenz zweier Operanden mit gleichen Vorzeichen) genau Null ist, muss das Vorzeichen dieser Summe (oder Differenz) unter allen Rundungsrichtungsattributen außer $+0$ sein roundTowardNegative; Unter diesem Attribut muss das Vorzeichen einer exakten Nullsumme (oder Differenz) $−0$ sein.

Lassen Sie uns das analysieren.

1. Eine Subtraktion $x – y$ wird als Summe $x + (-y)$ betrachtet.
2. Null kann ein Vorzeichen haben, $-0$ und $0$ sind unterschiedliche Einheiten (obwohl sie beim Testen gleich sind). ==).
3. Wenn beide Summanden das gleiche Vorzeichen haben, muss die Ausgabe dieses Vorzeichen haben. Für $x – y$ bedeutet dies jedoch, dass $x$ und $y$ vorhanden sind anders Vorzeichen: Die Ausgabe muss das Vorzeichen von $x$ haben.
4. Wenn $x$ und $y$ das gleiche Vorzeichen haben und $x – y$ Null ist, beträgt die Ausgabe für alle Rundungsmodi außer $+0$ roundTowardNegativedann wird es $-0$ sein.

Nun, da der Standardrundungsmodus in praktisch jedem Kontext gilt roundTiesToEven, davon gehen wir von nun an aus. Allerdings funktioniert auch für alles analog
roundTowardNegative.

Was bringt uns das also, wenn wir Nullen subtrahieren?

-0 - -0 = +0  # Same sign, must be +0.
-0 - +0 = -0  # Different signs, sign from first argument.
+0 - -0 = +0  # Different signs, sign from first argument.
+0 - +0 = +0  # Same sign, must be +0.

Interessant … Was wäre, wenn wir sagen würden, dass $-0$ falsch und $+0$ wahr ist?

A B | O
----+--
0 0 | 1
0 1 | 0
1 0 | 1
1 1 | 1

Unsere resultierende Wahrheitstabelle entspricht ${A \vee \neg B}$ oder ${B \to A}$ (auch als IMPLY-Gatter bekannt, allerdings mit vertauschten Argumenten). Es stellt sich heraus, dass diese Wahrheitstabelle funktional vollständig ist, was bedeutet, dass wir beliebige Schaltkreise nur mit diesem Gatter erstellen können. Technisch gesehen ist es nur dann funktional vollständig, wenn Zugriff auf die Konstante false gewährt wird. Dies ist notwendig, um ein NOT-Gatter zu erzeugen, und NOT + IMPLY ist ein funktional vollständiger Satz. Ich kenne jedoch keinen besseren Begriff für „funktionell vollständig, wenn Zugriff auf einen konstanten Wert gewährt wird“.

Lassen Sie uns eine Demo in Python erstellen. Zuerst definieren wir unsere Konstanten und ermöglichen uns, sie schön auszudrucken:

import math

f_false = -0.0
f_true = 0.0
f_repr = lambda x: True if math.copysign(1, x) > 0 else False

Wir können jetzt ein NICHT-Gatter erstellen, indem wir die Tatsache nutzen, dass $-0 – x$ das Vorzeichen von Null $x$ umdreht:

f_not = lambda x: f_false - x

Lasst uns das testen:

>>> f_repr(f_not(f_false))
True
>>> f_repr(f_not(f_true))
False

Großartig! Wir können auch ein ODER-Gatter erstellen, indem wir beachten, dass wir immer $+0$ (wahr) erhalten, wenn wir das Vorzeichen des zweiten Arguments vor dem Subtrahieren umdrehen, es sei denn, beide Argumente sind $-0$ (falsch):

f_or = lambda a, b: a - f_not(b)

Lass es uns testen:

>>> f_repr(f_or(f_false, f_false))
False
>>> f_repr(f_or(f_true,  f_false))
True
>>> f_repr(f_or(f_false, f_true))
True
>>> f_repr(f_or(f_true, f_true))
True

Nachdem wir nun ODER und NICHT haben, können wir alle anderen Gatter erstellen, z. B.:

f_and = lambda a, b: f_not(f_or(f_not(a), f_not(b)))
f_xor = lambda a, b: f_or(f_and(f_not(a), b), f_and(a, f_not(b)))

>>> f_repr(f_and(f_false, f_false))
False
>>> f_repr(f_and(f_true,  f_false))
False
>>> f_repr(f_and(f_false, f_true))
False
>>> f_repr(f_and(f_true, f_true))
True

>>> f_repr(f_xor(f_false, f_false))
False
>>> f_repr(f_xor(f_true,  f_false))
True
>>> f_repr(f_xor(f_false, f_true))
True
>>> f_repr(f_xor(f_true, f_true))
False

Sie haben vielleicht schon von Soft-Float-Softwareimplementierungen von Gleitkommazahlen mit Ganzzahlen gehört. Stellen wir das auf den Kopf: eine ganzzahlige Implementierung in Software, die nur Gleitkommaoperationen verwendet. Machen wir es in Rust, damit wir uns die endgültige Assembly-Ausgabe ansehen können, um zu sehen, wie furchtbar langsam großartig ist es.

type Bit = f32;
const ZERO: Bit = -0.0;
const ONE: Bit = 0.0;

fn not(x: Bit) -> Bit { ZERO - x }
fn or(a: Bit, b: Bit) -> Bit { a - not(b) }
fn and(a: Bit, b: Bit) -> Bit { not(or(not(a), not(b))) }
fn xor(a: Bit, b: Bit) -> Bit { or(and(not(a), b), and(a, not(b))) }
fn adder(a: Bit, b: Bit, c: Bit) -> (Bit, Bit) {
    let s = xor(xor(a, b), c);
    let c = or(and(xor(a, b), c), and(a, b));
    (s, c)
}

type SoftU8 = [Bit; 8];

pub fn softu8_add(a: SoftU8, b: SoftU8) -> SoftU8 {
    let (s0, c) = adder(a[0], b[0], ZERO);
    let (s1, c) = adder(a[1], b[1], c);
    let (s2, c) = adder(a[2], b[2], c);
    let (s3, c) = adder(a[3], b[3], c);
    let (s4, c) = adder(a[4], b[4], c);
    let (s5, c) = adder(a[5], b[5], c);
    let (s6, c) = adder(a[6], b[6], c);
    let (s7, _) = adder(a[7], b[7], c);
    [s0, s1, s2, s3, s4, s5, s6, s7]
}

// Hmm? u8? What's that? Shhhh....
pub fn to_softu8(x: u8) -> SoftU8 {
    std::array::from_fn(|i| if (x >> i) & 1 == 1 { ONE } else { ZERO })
}

pub fn from_softu8(x: SoftU8) -> u8 {
    (0..8).filter(|i| x[*i].signum() > 0.0).map(|i| 1 << i).sum()
}

fn main() {
    let a = to_softu8(23);
    let b = to_softu8(19);
    println!("{}", from_softu8(softu8_add(a, b)));
}

Es ist schrecklich, aber es funktioniert, es druckt brav 42. Und es nur benötigte $\ca. 120$ Gleitkommaanweisungen, um zwei 8-Bit-Ganzzahlen hinzuzufügen:

example::softu8_add:
        mov     rax, rdi
        movups  xmm2, xmmword ptr [rsi]
        movups  xmm0, xmmword ptr [rdx]
        movaps  xmm3, xmm2
        subps   xmm3, xmm0
        movaps  xmm4, xmm0
        subps   xmm4, xmm2
        movaps  xmm1, xmmword ptr [rip + .LCPI0_0]
        xorps   xmm4, xmm1
        subps   xmm4, xmm3
        xorps   xmm3, xmm3
        subss   xmm3, xmm4
        movaps  xmm6, xmm0
        xorps   xmm6, xmm1
        subss   xmm6, xmm2
        xorps   xmm6, xmm1
        subss   xmm6, xmm3
        movaps  xmm3, xmm4
        shufps  xmm3, xmm4, 85
        movaps  xmm5, xmm6
        subss   xmm5, xmm3
        xorps   xmm5, xmm1
        movaps  xmm10, xmm6
        xorps   xmm10, xmm1
        subss   xmm10, xmm3
        movaps  xmm7, xmm0
        shufps  xmm7, xmm0, 85
        xorps   xmm7, xmm1
        movaps  xmm3, xmm2
        shufps  xmm3, xmm2, 85
        subss   xmm7, xmm3
        xorps   xmm7, xmm1
        movaps  xmm8, xmm4
        unpckhpd        xmm8, xmm4
        movaps  xmm3, xmm0
        unpckhpd        xmm3, xmm0
        xorps   xmm3, xmm1
        movaps  xmm9, xmm2
        unpckhpd        xmm9, xmm2
        subss   xmm3, xmm9
        xorps   xmm3, xmm1
        xorps   xmm11, xmm11
        movaps  xmm9, xmm4
        shufps  xmm9, xmm4, 255
        subss   xmm7, xmm10
        movaps  xmm10, xmm7
        xorps   xmm10, xmm1
        subss   xmm10, xmm8
        subss   xmm3, xmm10
        unpcklps        xmm7, xmm3
        shufps  xmm6, xmm7, 64
        addps   xmm11, xmm4
        movlhps xmm5, xmm4
        subps   xmm4, xmm6
        movss   xmm4, xmm11
        subps   xmm7, xmm8
        xorps   xmm7, xmm1
        shufps  xmm5, xmm7, 66
        subps   xmm5, xmm4
        xorps   xmm3, xmm1
        subss   xmm3, xmm9
        shufps  xmm0, xmm0, 255
        xorps   xmm0, xmm1
        shufps  xmm2, xmm2, 255
        subss   xmm0, xmm2
        xorps   xmm0, xmm1
        movups  xmmword ptr [rdi], xmm5
        movups  xmm2, xmmword ptr [rdx + 16]
        movaps  xmm5, xmm2
        xorps   xmm5, xmm1
        movups  xmm7, xmmword ptr [rsi + 16]
        subss   xmm5, xmm7
        xorps   xmm5, xmm1
        movaps  xmm4, xmm2
        shufps  xmm4, xmm2, 85
        xorps   xmm4, xmm1
        movaps  xmm6, xmm2
        movaps  xmm8, xmm7
        movaps  xmm9, xmm7
        subps   xmm9, xmm2
        subps   xmm2, xmm7
        shufps  xmm7, xmm7, 85
        subss   xmm4, xmm7
        xorps   xmm4, xmm1
        movhlps xmm6, xmm6
        xorps   xmm6, xmm1
        movhlps xmm8, xmm8
        subss   xmm6, xmm8
        xorps   xmm6, xmm1
        xorps   xmm2, xmm1
        subps   xmm2, xmm9
        subss   xmm0, xmm3
        movaps  xmm3, xmm0
        xorps   xmm3, xmm1
        subss   xmm3, xmm2
        subss   xmm5, xmm3
        unpcklps        xmm0, xmm5
        xorps   xmm5, xmm1
        movaps  xmm3, xmm2
        shufps  xmm3, xmm2, 85
        subss   xmm5, xmm3
        subss   xmm4, xmm5
        movaps  xmm3, xmm4
        xorps   xmm3, xmm1
        movaps  xmm5, xmm2
        unpckhpd        xmm5, xmm2
        subss   xmm3, xmm5
        subss   xmm6, xmm3
        unpcklps        xmm4, xmm6
        movlhps xmm0, xmm4
        movaps  xmm3, xmm2
        subps   xmm3, xmm0
        subps   xmm0, xmm2
        xorps   xmm0, xmm1
        subps   xmm0, xmm3
        movups  xmmword ptr [rdi + 16], xmm0
        ret