巨大数.v

(* 巨大数 *)

Print nat.

Definition 十 := 10.

Fixpoint plus (n m:nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.

Fixpoint mult (n m:nat) : nat :=
match n with
| O => 0
| S n' => plus m (mult n' m)
end.

Fixpoint pow (n m:nat) : nat :=
match m with
| O => 1
| S m' => mult n (pow n m')
end.

Eval compute in (plus 1 1).
Eval compute in (mult 3 3).
Eval compute in (pow 3 3).
Eval compute in (pow 4 4).
Eval compute in (pow 10 2).
Eval compute in (pow 10 4).

Definition 無量大数 :nat := pow 10 68.

Fixpoint fold (f : nat -> nat) (n m:nat) : nat :=
match m with
| O => n
| S m' => f (fold f n m')
end.

Fixpoint hyper (n a b : nat) : nat :=
match n with
| O => plus a b
| S n' => match b with
 | O => 1
 | S b' => fold (hyper n' a) a b'
end
end.

Eval compute in (hyper 0 0 5).
Eval compute in (hyper 0 3 5).
Eval compute in (hyper 1 3 5).
Eval compute in (hyper 1 2 3).
Eval compute in (hyper 2 3 3).
Eval compute in (hyper 2 3 4).
Eval compute in (hyper 2 4 3).

Eval compute in (hyper 3 5 2).
Eval compute in (hyper 3 2 2).
Eval compute in (hyper 3 2 3).
Eval compute in (hyper 3 3 2).

Definition G (n:nat) : nat  := hyper (S n) 3 3.
Definition グラハム数 : nat := fold G 4 64.