Niestandardowy model liczb naturalnych - Historia wersji

AndrzejSalwicki o 09:35, 7 mar 2013

2013-03-07T09:35:49Z

2013-03-05T11:32:44Z

‎Przypisy

2013-02-21T13:47:44Z

‎Przykład wykazujący, że algorytm Euklidesa w modelu niestandardowym nie zatrzymuje się.

2013-02-21T12:50:39Z

‎Przykład wykazujący, że algorytm Euklidesa w modelu niestandardowym nie zatrzymuje się.

2013-02-21T12:47:20Z

‎Przykład wykazujący, że algorytm Euklidesa w modelu niestandardowym nie zatrzymuje się.

2013-02-21T12:40:04Z

‎Przykład wykazujący, że algorytm Euklidesa w modelu niestandardowym nie zatrzymuje się.

2013-02-21T12:31:17Z

2013-02-21T12:21:51Z

2013-02-20T13:33:12Z

2013-02-20T13:17:44Z

@@ Linia 7: / Linia 7: @@
 ° Model niestandardowy może być programowalny. (że nie zawsze tak jest dowodzi
-'''Twierdzenie''' Tennenbauma:
+::'''Twierdzenie''' Tennenbauma:
-''Jeśli model arytmetyki z dodawaniem i mnożeniem jest programowalny, to jest modelem standardowym''.
+::''Jeśli model arytmetyki z dodawaniem i mnożeniem jest programowalny, to jest modelem standardowym''.
 ------

@@ Linia 77: / Linia 77: @@
 n:=x; m:=y;
-'''while''' \neg n.isequal(m)
+'''while''' not n.isequal(m)
 '''do'''
 ::<math>\color{red}\mathbf{Oznaczenie}\ niech\ l=max(n,m)  </math>

@@ Linia 81: / Linia 81: @@
 ::<math>\color{red}\mathbf{Oznaczenie}\ niech\ l=max(n,m)  </math>
 :r:=0;
-:'''while''' \neg r.isequal(n) '''and''' \neg r.isequal(m)
+:'''while''' not r.isequal(n) '''and''' not r.isequal(m)
 :'''do'''
 ::r:=r.add(one)
@@ Linia 88: / Linia 88: @@
 ::<math>\color{blue}\mathbf{Stwierdzenie}\ (n<m \wedge m=max(n,m) \vee m<n \wedge n=max(n,m)) </math>
 :q:=0;
-:'''while''' \neg r.isequal(max)
+:'''while''' not r.isequal(max)
 :'''do'''
 ::r:= r.add(one); q:=q.add(one)

@@ Linia 72: / Linia 72: @@
 (* 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>
+::<math>\color{blue}\mathbf{Deklaracje: }\ typ(x, y, n, m, r, q, max)=NSN\ \land\ typ(n\_mniejsze)=Boolean  </math>
 (* Wynik:  nwd(x,y)  *)

← poprzednia wersja		Wersja z 12:40, 21 lut 2013
Linia 69:		Linia 69:

	Po pierwsze, trzeba nasz algorytm przepisać tak by jego środowiskiem była klasa NSN. Nie jest to trudne.		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''' \neg n.isequal(m)
		+	'''do'''
		+	::<math>\color{red}\mathbf{Oznaczenie}\ niech\ l=max(n,m) </math>
		+	:r:=0;
		+	:'''while''' \neg r.isequal(n) '''and''' \neg 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''' \neg 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)

@@ Linia 66: / Linia 66: @@
 Dowód można znaleźć w książce Andrzeja Grzegorczyka.
-== 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ę. ==
 Po pierwsze, trzeba nasz algorytm przepisać tak by jego środowiskiem była klasa NSN. Nie jest to trudne.

@@ Linia 3: / Linia 3: @@
 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 <ref>''inaczej'', interfejsy, aksjomatyzacje</ref> Nat i Nat2 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ą.
 ------