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

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 1: Linia 1:
Klasa NSN przytoczona poniżej spełnia aksjomaty liczbnaturalnych 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.
 
------
 
------
  
Linia 46: Linia 46:
 
::  (* 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;
begin (* main *)
+
'''begin''' (* main *)
:  zero := new NSN(0, 0,1);
+
:  zero := '''new''' NSN(0, 0,1);
:  one := new NSN(1,0,1);
+
:  one := '''new''' NSN(1,0,1);
 
    
 
    
end
+
'''end'''

Wersja z 11:39, 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.


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