|
07.10.2010, 07:19:21
#36886055
Ссылка:
Ссылка на сообщение:
Ссылка с названием темы:
Ссылка на профиль пользователя:
|
|
|
Участник
Сообщения: 36 906
Рейтинг:
120
/ 0
|
|
|
|
любое натуральное имеет вид 1 + 1 + 1 + ... + 1
plus(1,plus(1,...,plus(1,1)...)
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
14.
15.
16.
17.
18.
19.
20.
21.
22.
23.
24.
25.
26.
27.
28.
29.
30.
31.
32.
33.
34.
35.
36.
37.
38.
39.
40.
41.
42.
43.
44.
45.
46.
47.
48.
49.
50.
51.
52.
53.
54.
55.
56.
57.
58.
59.
60.
61.
62.
63.
64.
65.
66.
67.
68.
69.
70.
71.
72.
73.
74.
75.
76.
77.
78.
79.
80.
81.
82.
83.
84.
85.
86.
87.
88.
89.
90.
91.
92.
93.
94.
95.
96.
97.
98.
99.
100.
101.
102.
103.
104.
105.
106.
107.
108.
109.
110.
111.
112.
113.
114.
115.
116.
0.6. НАТУРАЛЬНЫЕ, ЦЕЛЫЕ И ВЕЩЕСТВЕННЫЕ
Введем типы натуральных (UInt), целых (Int) и вещественных
(Real) чисел и наметим доказательство того, что в определенном
выше смысле тип целых не является подтипом вещественных и,
поэтому, класс целых не может быть наследован из класса
вещественных.
0.6.1. Тип натуральных чисел
В этой версии будем строить множество натуральных чисел
начиная с 0.
Спецификация множество натуральных чисел с системой аксиом
Пеано.
scheme PEANO =
class
type -- обозначили тип натуральных N
N
value
7
zero : N, -- завели величину zero
succ: N -> N -- величина - функция из N в N
axiom
[first_is_zero]
all n : N :- -- для каждого натурального n
~(succ(n) is zero) -- применение succ(n) не есть zero
,[linear_order]
all n1, n2 : N :-
(succ(n1) is succ(n2)) => (n1 is n2)
, [induction]
all p : N -> Bool :- -- для любого предиката
(p(zero) / (all n : N :- p(n) => p(succ(n)))) =>
(all n : N :- p(n))
end
--
-- ~ отрицание
-- :- выполняется
-- => влечет
-- / логическое и
--
-- exist квантор существования
--
--
Множеством натуральных чисел N по построению будут все
последовательные применения функции succ
zero,
succ(zero),
succ(succ(zero)),
succ(succ(succ(zero))),
...
К аксиомам Пеано добавим операцию сложения.
PEANO -- подключение схемы PEANO
scheme NAT =
extend PEANO with
class
value
plus : N >< N -> N -- вводим функции (операции) сложить
,
mult : N >< N -> N -- и умножить
axiom
[plus_zero]
all n : N :-
plus(n, zero) is n
,
[plus_succ]
all n1, n2 : N :-
plus(n1, succ(n2)) is succ(plus(n1, n2))
,
[mult_zero]
all n : N :-
mult(n, zero) is zero
,
[mult_succ]
all n1, n2 : N :-
mult(n1, succ(n2)) is plus(mult(n1, n2), n1)
end
через 1 обозначим символ succ(zero) и покажем, что любое
8
число из N может быть представлено в виде
plus(1,plus(1,...,plus(1,1)...))
Рассмотрим succ(1). По аксиоме plus\_zero
succ(1) = succ(plus(1,zero)
По аксиоме plus\_succ
succ(plus(1,zero) = plus(1, succ(zero)) = plus( 1, 1)
то есть,
[2]
succ(1) = plus(1,1)
Следующее число succ(succ(1)). По доказанному равенству 2
succ(succ(1)) = succ(plus(1,1))
Далее по plus\_succ и по 2 получаем
[2_1]
succ(plus(1,1)) = plus (1, succ(1)) = plus(1, plus(1,1))
В сухом остатке равенство
[3]
succ(succ(1)) = plus(1, plus(1,1))
Последний раз для числа succ(succ(succ(1)))
succ(succ(succ(1))) = succ( plus(1, plus(1,1)))
и с учетом 2\_1
succ( plus(1, plus(1,1))) = plus (1, succ(plus(1,1))) =
= plus(1, plus(1, plus(1,1)))
По видимому, не затруднит применить принцип матиндукции
(аксиома induction) и доказать требуемое свойство.
|
|
|
