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

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 3: Linia 3:
 
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 (''inaczej'' 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 (''inaczej'', interfejsy, aksjomatyzacje) liczb naturalnych nie wystarczają.  
 
------
 
------
  

Wersja z 13:08, 20 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?

Do udowodnienia poprawności algorytmu Euklidesa potrzebny jest inny zestaw własności (inaczej, niezmienników, aksjomatów) liczb naturalnych. Poniżej przytoczone specyfikacje (inaczej, interfejsy, 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


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.