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?

1° Do udowodnienia poprawności algorytmu Euklidesa potrzebny jest inny zestaw własności (inaczej, niezmienników, aksjomatów) liczb naturalnych. Poniżej przytoczone specyfikacje Nat i Nat2 liczb naturalnych nie wystarczają.

2° Model niestandardowy może być programowalny. (że nie zawsze tak jest dowodzi

Twierdzenie Tennenbauma: Jeśli model arytmetyki z dodawaniem i mnożeniem jest programowalny, to jest modelem standardowym.

---

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

---

Twierdzenie Zbiór obiektów klasy NSN wraz z metodami .add i .isequal spełnia aksjomaty liczb naturalnych z dodawaniem, w tym wszystkie formuły schematu indukcji.

Dowód można znaleźć w książce Andrzeja Grzegorczyka. == Przykład wykazujący, że algorytm Euklidesa w modelu niestandardowym nie zatrzymuje się.

Po pierwsze, trzeba nasz algorytm przepisać tak by jego środowiskiem była klasa NSN. Nie jest to trudne.

Niech

x:= new NSN(12,0,1); y := new NSN(15, 1,2);

Teraz, spróbujmy obliczyć NWD(x,y). Łatwo widać, że w tym przypadku obliczenie będzie nieskończone lub bardziej realistycznie: obliczenie może być kontynuowane dowolnie długo.

Przypisy

<references\>