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

Z Lem
Skocz do: nawigacji, wyszukiwania
 
(Nie pokazano 13 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 1: Linia 1:
 
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.
 
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?
 
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ą.  
+
 
 +
Do udowodnienia poprawności algorytmu Euklidesa potrzebny jest inny zestaw własności (''inaczej'', niezmienników, aksjomatów) liczb naturalnych. Poniżej przytoczone specyfikacje <ref>''inaczej'', interfejsy, aksjomatyzacje</ref> 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''.
 
------
 
------
  
Linia 46: Linia 53:
 
:  end Nat2;  
 
:  end Nat2;  
 
    
 
    
::  (* Tw. Te dwie specyfikacje są równoważne i zupełne  *)
+
::  (* '''Tw'''. Te dwie specyfikacje są równoważne i zupełne  *)
 
    
 
    
 
:  '''var''' (* final *) zero, one: Nat;
 
:  '''var''' (* final *) zero, one: Nat;
Linia 56: Linia 63:
 
-------
 
-------
 
'''Twierdzenie'''
 
'''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''.
+
''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.
 
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<m \wedge m=max(n,m) \vee m<n \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 < 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) < \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/>

Aktualna wersja na dzień 10:35, 7 mar 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

  1. inaczej, interfejsy, aksjomatyzacje