Niestandardowy model liczb naturalnych

Klasa NSN przytoczona poniżej spełnia aksjomaty liczb naturalnych z operacją dodawania, ale wykonywanie algorytmu Euklidesa w środowisku zdefiniowanym przez tę klasę nie zawsze kończy się po skończonej liczbie kroków. Czego dowodzi ten przykład? Do udowodnienia poprawności algorytmu Euklidesa potrzebny jest inny zestaw własności (niezmienników, aksjomatów) liczb naturalnych. Poniżej przytoczone specyfikacje (interface, aksjomatyzacje) liczb naturalnych nie wystarczają.

---

program NonstandardNaturalNumbers;

unit NSN: Nat class(cecha,licznik, mianownik: integer);

unit virtual add: function(m: NSN) : NSN;

begin

result:= new NSN(cecha+m.cecha, licznik*m.mianownik+mianownik*m.licznik)

end add;

unit virtual isequal: function(n: NSN): Boolean;

begin

result := (cecha=m.cecha) and (licznik*m.mianownik=mianownik*m.licznik)

end isequal;

begin

if licznik=0 and cecha <0 then raise Exception fi;

if licznik < 0 then raise Exception fi;

if mianownik =0 then raise Exception fi

end NSN;

unit Nat: class; (* specyfikacja 1sza *)

unit virtual add: function(x:Nat): Nat; end add;

unit virtual isequal: function(x:Nat): Boolean; end isequal;

(* -------------------------------------------------------- *)

(* forall n in Nat, not( n.add(one).isequal(zero)

forall n,m in Nat not n.isequal(m) implies not n.add(one).isequal(m.add(one))

dla kazdej formuły alpha(x)

{alpha(x/zero) and forall n [alpha(n) implies alpha(n.add(one))]} implies forall n alpha(n)

*)

end Nat;

unit Nat2: class; (* specyfikacja 2sza *)

unit virtual add: function(x:Nat): Nat; end add;

unit virtual isequal: function(x:Nat): Boolean; end isequal;

(* INVARIANTS *)

(* -------------------------------------------------------- *)

(* forall n in Nat, not( n.add(one).isequal(zero)

forall n,m in Nat not n.isequal(m) implies not n.add(one).isequal(m.add(one))

INNY SCHEMAT zob. A. Grzegorczyk Zarys Arytmetyki Teoretycznej, PWN, Warszawa, 1971, str.239

*)

end Nat2;

(* Tw. Te dwie specyfikacje są równoważne i zupełne *)

var (* final *) zero, one: Nat;

begin (* main *)

zero := new NSN(0, 0,1);

one := new NSN(1,0,1);

end