Den Mathematikern Richard Dedekind und Giuseppe Peano gelang Ende des 19. Jahrhunderts erstmals eine strenge Definition der natürlichen Zahlen. Ihr Vorgehen baut auf dem Gedankengang auf, dass jede natürliche Zahl einen Nachfolger besitzt. Sie nutzen die Nachfolgerabbildung, um die arithmetischen Operationen rekursiv zu definieren. Die wesentliche Schwierigkeit, die sich dabei stellt, ist das Prinzip der Induktion, das die Grundlage für das fundamentale Beweisverfahren vollständige Induktion bildet. Das Prinzip wird durch das Induktionsaxiom abgesichert, das letzte und komplizierteste Axiom in Peanos System.
Dieses Kapitel beschäftigt sich mit der Darstellung der natürlichen Zahlen als Typen. Zur Vorbereitung wollen wir die Zahlen aber erst einmal als Werte darstellen. Bei beiden Unterfangen wird die Vorgehensweise von Dedekind und Peano genutzt.
Es bezeichne Zero die Zahl null und
Succ bzw. succ als Abkürzung von successor
die Nachfolgerabbildung. Man stellt die natürlichen Zahlen als
Enumeration dar:
#[derive(Clone, PartialEq, Eq, Debug)]
enum Nat {
Zero,
Succ(Box<Nat>)
}
use Nat::{Zero, Succ};
fn succ(a: Nat) -> Nat {Succ(Box::new(a))}
Die Addition ist rekursiv definiert als
0 + b := b,
succ(a) + b := succ(a + b).
Man kann sie direkt so implementieren:
fn add(a: Nat, b: Nat) -> Nat {
match a {
Zero => b,
Succ(a) => succ(add(*a, b))
}
}
Nun lässt sich berechnen, ob 1 + 1 = 2 gilt:
fn main() {
let one = succ(Zero);
let two = succ(one.clone());
assert_eq!(add(one.clone(), one), two);
}
Eine weniger umständliche Formulierung ergibt sich durch Kodierung
der natürlichen Zahlen als Werte des Typs u32. Bei dieser
entfällt leider die Durchführbarkeit, auf das Muster
Succ(a) abgleichen zu können. Wir überlegen uns dazu,
dass dies bisher geklappt hat, weil Succ eine injektive
Abbildung ist. Allgemein gehört zu jeder Enum-Variante eine einbettende
Injektion. Daher können wir die Umkehrabbildung mit Ausnahme der Null
für alle natürlichen Zahlen definieren und mit dieser arbeiten. Sie sei
mit pred als Abkürzung für predecessor bezeichnet.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
struct Nat(u32);
fn succ(a: Nat) -> Nat {Nat(a.0 + 1)}
fn pred(a: Nat) -> Nat {
if a.0 == 0 {unreachable!()} else {Nat(a.0 - 1)}
}
fn add(a: Nat, b: Nat) -> Nat {
match a {
Nat(0) => b,
a => succ(add(pred(a), b))
}
}
fn main() {
assert_eq!(add(Nat(1), Nat(1)), Nat(2));
}
Wir wollen nun dazu übergehen, die natürlichen Zahlen als Typen
darzustellen. Die Nachfolgerabbildung Succ wird hierbei
zu einen Typkonstruktor, der dem Typ N dessen Nachfolger
Succ<N> zuordnet. Es muss außerdem der Typ
Zero vorhanden sein, der die Null darstellt.
Zudem möchten wir ausdrücken können, dass ein Typparameter zu den
natürlichen Zahlen gehören soll. Wir definieren daher einen Trait
Nat und implementieren diesen für alle natürlichen
Zahlen. Obwohl nicht unbedingt notwendig, ist es praktisch, außerdem
eine assoziierte Konstante VALUE zum Trait hinzuzufügen,
mit der sich der Typ zur Kompilierzeit in dessen Entsprechung als Zahl
umwandeln lässt.
struct Zero;
struct Succ<N>(N);
trait Nat {const VALUE: u32;}
impl Nat for Zero {const VALUE: u32 = 0;}
impl<N: Nat> Nat for Succ<N> {
const VALUE: u32 = N::VALUE + 1;
}
Alternativ lässt sich Zero als leere Enumeration
enum Zero {} definieren, die die Erstellung
von Werten unmöglich macht. Absurderweise kann man Werte dennoch
mittels PhantomData erstellen. Für das erzeugte
Maschinenprogramm ergibt sich dabei kein Unterschied, weil
Zero bezüglich struct Zero; bereits keine
Information trägt, also kein Artefakt im Maschinenprogramm hinterlässt.
Kurze Rekapitulation. Die Addition ist rekursiv definiert als
0 + b := b,
succ(a) + b := succ(a + b).
Um diese Rekursion implementieren zu können, definiert man als Hilfsmittel einen
trait Plus mit dem rechten Summand als Parameter und
assoziiertem Typ Value als Wert der Addition.
trait Plus<B> {type Value;}
type Add<A, B> = <A as Plus<B>>::Value;
impl<B: Nat> Plus<B> for Zero {
type Value = B;
}
impl<A: Nat + Plus<B>, B: Nat> Plus<B> for Succ<A> {
type Value = Succ<Add<A, B>>;
}
Die Multiplikation ist rekursiv definiert als
0⋅b := 0,
succ(a)⋅b := a⋅b + b.
Die Potenzierung ist rekursiv definiert als
a0 := 1,
asucc(n) := a⋅an.
Die Rekursion wird analog zur Addition implementiert.
trait Times<B> {type Value;}
type Mul<A, B> = <A as Times<B>>::Value;
impl<B: Nat> Times<B> for Zero {
type Value = Zero;
}
impl<A: Nat + Times<B>, B: Nat> Times<B> for Succ<A>
where Mul<A, B>: Plus<B>
{
type Value = Add<Mul<A, B>, B>;
}
trait ExpBase<A> {type Value;}
type Pow<A, N> = <N as ExpBase<A>>::Value;
impl<A: Nat> ExpBase<A> for Zero {
type Value = Succ<Zero>;
}
impl<A: Nat, N: Nat + ExpBase<A>> ExpBase<A> for Succ<N>
where A: Times<Pow<A, N>>
{
type Value = Mul<A, Pow<A, N>>;
}
Mit den drei Operationen Add, Mul,
Pow lässt sich nun, wenngleich ein wenig umständlich,
jede natürliche Zahl im Stellenwertsystem darstellen.
Das folgende Beispiel zeigt die Darstellung der Zahl 360 im
Dezimalsystem.
type P0 = Zero;
type P1 = Succ<P0>;
type P2 = Succ<P1>;
type P3 = Succ<P2>;
type P4 = Succ<P3>;
type P5 = Succ<P4>;
type P6 = Succ<P5>;
type P7 = Succ<P6>;
type P8 = Succ<P7>;
type P9 = Succ<P8>;
type P10 = Succ<P9>;
fn main() {
type P360 = Add<Mul<P3, Pow<P10, P2>>, Mul<P6, P10>>;
println!("{}", P360::VALUE);
}
Das P soll hierbei für plus stehen. Fügt man
später negative Zahlen hinzu, kann man sie dann
M1, M2
usw. für −1, −2 usw. nennen.
Mit den natürlichen Zahlen lassen sich Größen durch die Dimension parametrisieren, ohne Konstanten als Typparameter heranziehen zu müssen.
Die Definition von Nat sollte zu Nat: Copy
modifiziert werden, damit die Größen Copy sein können.
Der Einfachheit halber wird der Typ Quantity lediglich
durch Dimensionen zur Basis Länge parametrisiert.
mod quantities {
use super::{Nat, Plus, P1, P2};
use std::ops::{Add, Mul};
use std::marker::PhantomData as Ph;
use std::fmt;
#[derive(Clone, Copy)]
pub(super) struct Quantity<L: Nat> {
value: f64, dim: Ph<L>
}
impl<L: Nat> Add<Quantity<L>> for Quantity<L> {
type Output = Quantity<L>;
fn add(self, y: Quantity<L>) -> Self::Output {
Quantity {value: self.value + y.value, dim: Ph}
}
}
impl<L: Nat> Mul<Quantity<L>> for f64 {
type Output = Quantity<L>;
fn mul(self, y: Quantity<L>) -> Self::Output {
Quantity {value: self*y.value, dim: Ph}
}
}
impl<L1: Nat, L2: Nat> Mul<Quantity<L2>> for Quantity<L1>
where L1: Plus<L2>, super::Add<L1, L2>: Nat
{
type Output = Quantity<super::Add<L1, L2>>;
fn mul(self, y: Quantity<L2>) -> Self::Output {
Quantity {value: self.value*y.value, dim: Ph}
}
}
impl<N: Nat> fmt::Display for Quantity<N> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(f, "{} m^{}", self.value, N::VALUE)
}
}
pub(super) type Length = Quantity<P1>;
pub(super) type Area = Quantity<P2>;
pub(super) struct Meter;
impl Mul<Meter> for f64 {
type Output = Length;
fn mul(self, _rhs: Meter) -> Self::Output {
Quantity {value: self, dim: Ph}
}
}
}
use quantities::{Length, Area, Meter};
use std::f64::consts::PI;
fn circle_area(radius: Length) -> Area {
PI*radius*radius
}
fn main() {
println!("{}", circle_area(2.0*Meter));
}
Dieses Beispiel zeigt bereits auf, dass die gemachten Konstruktionen
nicht nur eine »akademische Spielerei« darstellen, sondern tatsächliche
Bedeutung für die Typsicherheit haben können. Allerdings macht
die allgemeine Verfügbarkeit von Konstanten als Typparameter
die Konstruktion von Nat für diesen Zweck entbehrlich.
Um den Compiler prüfen zu lassen, ob zwei natürliche Zahlen oder allgemeiner zwei Typen gleich sind, bietet sich der folgende Trick an, den wir in ein Makro verpacken.
macro_rules! assert_type_eq {
($t1:ty, $t2:ty) => {
const _: Option<$t1> = Option::<$t2>::None;
}
}
assert_type_eq!(P3, Add<P1, P2>);
Dabei wurde zunutze gemacht, dass Option::None keine
Daten trägt. Insofern kann man ebensogut PhantomData
heranziehen.
use std::marker::PhantomData as Ph;
macro_rules! assert_type_eq {
($t1:ty, $t2:ty) => {
const _: Ph<$t1> = Ph::<$t2>;
}
}
Auf diese Weise sind aber lediglich konkrete Typen vergleichbar.
Mathematisch interessante Fragen wie die nach der
die allgemeinen Gleichheit von Add<A, B> und
Add<B, A> lassen sich so nicht beantworten.
Für einige Spezialfälle wie
∀n ∈ ℕ: 0 + n = n
findet sich unschwer ein prüfendes Programm. Es genügt dafür, einen Kontext zu erstellen, der die allquantifizierte Variable enthält. Eine mögliche Formulierung ist:
fn context<N: Nat>(n: N) -> Add<Zero, N> {n}
oder:
fn context<N: Nat>() {
let _: Option<Add<Zero, N>> = Option::<N>::None;
}
oder auch:
trait Context<N: Nat> {
const C: Option<Add<Zero, N>> = Option::<N>::None;
}
Diese Methodik schlägt allerdings bereits bei einer unscheinbaren Aussage wie
∀n ∈ ℕ: n + 0 = n
fehl. Der Beweis dieser Aussage ist nämlich induktiv zu führen, wofür das Induktionsaxiom benötigt wird. Der Induktionsschritt ist eigentlich ein Kinderspiel, nämlich
succ(n) + 0 = succ(n + 0) = succ(n),
wobei die erste Gleichung gemäß der Definition der Addition und die zweite Gleichung gemäß der Induktionsvoraussetzung gilt. Der Induktionsanfang ist mit 0 + 0 = 0 noch banaler. Das Induktionsaxiom sichert nun ab, dass die Aussage somit bereits für alle natürlichen Zahlen gilt, oder die Kette der Dominosteine ohne Ausnahmen purzelt, wie man sich das auch immer veranschaulichen mag.
Damit das Induktionsaxiom dies schafft, muss es die Existenz von Parallelstrukturen verhindern, das wären Dominosteine neben der Kette, die nicht von der Kettenreaktion betroffen sind. Bei uns ist das Axiom jedoch abhanden. Tatsächlich können wir eine solche Parallelstruktur herstellen und damit Schabernack treiben. Es genügt ein einziger Stein bzw. ein einziger Typ dafür:
struct A0;
impl Nat for A0 {}
impl<B: Nat> Plus<B> for A0 {
type Value = B;
}
Mit dieser Definition gilt Add<A0, Zero> = Zero,
womit die Setzung N:=A0 ein Gegenbeispiel zu
Add<N, Zero> = N erbringt.