Niestandardowy model liczb naturalnych: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
(Przykład wykazujący, że algorytm Euklidesa w modelu niestandardowym nie zatrzymuje się.)
(Przykład wykazujący, że algorytm Euklidesa w modelu niestandardowym nie zatrzymuje się.)
Linia 77: Linia 77:
 
n:=x; m:=y;
 
n:=x; m:=y;
  
'''while''' \neg n.isequal(m)   
+
'''while''' not n.isequal(m)   
 
'''do'''
 
'''do'''
 
::<math>\color{red}\mathbf{Oznaczenie}\ niech\ l=max(n,m)  </math>
 
::<math>\color{red}\mathbf{Oznaczenie}\ niech\ l=max(n,m)  </math>

Wersja z 14:47, 21 lut 2013

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 [1] 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. (* Algorytm Euklidesa inaczej, zauważ, że w tym algorytmie jedyna operacja jest dodaj jeden, jedynym predykatem jest równość. *)

(* Dane: x>0 i y>0 liczby naturalne *)

[math]\color{blue}\mathbf{Deklaracje: }\ typ(x, y, n, m, r, q, max)=NSN\ \land\ typ(n\_mniejsze)=Boolean [/math]

(* Wynik: nwd(x,y) *)

n:=x; m:=y;

while not n.isequal(m) do

[math]\color{red}\mathbf{Oznaczenie}\ niech\ l=max(n,m) [/math]
r:=0;
while not r.isequal(n) and not r.isequal(m)
do
r:=r.add(one)
od;
if r.isequal(n) then n_miejsze:=true; max:=m else n_mniejsze:=false; max:=n fi;
[math]\color{blue}\mathbf{Stwierdzenie}\ (n\ltm \wedge m=max(n,m) \vee m\ltn \wedge n=max(n,m)) [/math]
q:=0;
while not r.isequal(max)
do
r:= r.add(one); q:=q.add(one)
od;
[math]\color{blue}\mathbf{Stwierdzenie}\ q = |m-n| \land (1 \leq q \lt max(n,m))\land r=max(n,m) [/math]
if n_mniejsze then m:=q else n := q fi
[math]\color{blue}\mathbf{Stwierdzenie}\ max(n,m) \lt \color{red}l [/math]

od ( wynik = n)


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\>
Błąd rozszerzenia cite: Istnieje znacznik <ref>, ale nie odnaleziono znacznika <references/>