вот спецификация натуральных чисел
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.
--
-- операция сравнения '=' и ключевое слово 'is'
-- имеют различный смысл, но в этом примере смысл практически совпадает.
-- если в схеме появляются "глобальные переменные" - множество
-- всех глобальных переменных наз. состояние - то операция = и
-- is будут иметь различный смысл. is означает равно для всех состояний
--
scheme PEANO =
class
type -- завели тип N
N
value
zero : N, -- завели величину zero
-- (это не переменная, нельзя присваивать)
succ: N -> N -- величина - функция из N в N
axiom
[first_is_zero] --
-- квантор всеобщности
all n : N :- -- n - это обозначение
~(succ(n) is zero) -- для каждого n результат 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 квантор существования
--
--
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.
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
причем тут неопределенные термины время, устойчивость, объекты и всякая такая фигня?
К чему они там в спецификации? Там только функции и множества есть и этого достаточно
