Математическое введение в декларативное программирование. Зюзысов В.М. - 22 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

Составители: 

Рубрика: 

xU–Rx является аксиомой, когда x состоит только из тире (каждое из двух вхождений x
замещает одинаковое число тире).
Правило вывода (схема):
Пусть x, y и z – строчки, состоящие только из тире. Пусть xUyRz является теоремой. Тогда
xUy–Rzx также будет теоремой.
Задача. Найдите разрешающий алгоритм для теорем UR.
Выберем следующую интерпретацию системы UR.
Универсум – множество целых положительных чисел. •
•
•
•
•
•
•
•
•
•
Последовательность, состоящая из n тире, интерпретируется как число n.
P интерпретируется как символ ×.
R интерпретируется как символ =.
Нетрудно убедиться, что указанная интерпретация теореме xUyRz ставит в соответ-
ствие истинное утверждение о целых положительных числах «x×y=z» и поэтому данная
интерпретация является моделью системы UR.
Формальная система PR1
Алфавит: {P, R, –}
Выражения – элементы {P, R, –}*.
Формулы – строки вида xPyRz, где x, y и z – строчки, состоящие только из тире.
Схемы аксиом:
1. xP–Rx– является аксиомой, когда x состоит только из тире (каждое из двух вхожде-
ний x замещает одинаковое число тире).
2. xP–Rx является аксиомой, когда x состоит только из тире (каждое из двух вхожде-
ний x замещает одинаковое число тире).
Правило вывода (схема):
Пусть x, y и z – строчки, состоящие только из тире. Пусть xPyRz является теоремой. Тогда
xPy–Rz– также будет теоремой.
Задача. Найдите разрешающий алгоритм для теорем PR1.
Рассмотрим различные интерпретации системы PR1.
1. Выберем интерпретацию системы PR1 такую же, как для PR.
Универсум – множество целых положительных чисел.
Последовательность, состоящая из n тире, интерпретируется как число n.
P интерпретируется как символ +.
R интерпретируется как символ =.
Указанная интерпретация теореме xPyRz ставит в соответствие утверждение о це-
лых положительных числах «x+y=z». Но эти утверждения могут быть и ложными, поэтому
данная интерпретация не является моделью системы PR1.
2. Вторая интерпретация системы PR1 отличается от первой только тем, как интер-
претируется символ R.
R интерпретируется как «равняется или больше на 1».
Указанная интерпретация теореме xPyRz ставит в соответствие истинное утвержде-
ние о целых положительных числах «x+y=z+1 ∨ x+y=z» и поэтому данная интерпретация
является моделью системы PR1. Более того, любое истинное утверждение «x+y=z+1 ∨
x+y=z» описывается в виде теоремы xPyRz теории PR1.
3. В последней интерпретации символ R понимается снова по-другому.
R интерпретируется как символ ≥».
Указанная интерпретация теореме xPyRz ставит в соответствие истинное утвержде-
ние о целых положительных числах «x+y≥z»и поэтому данная интерпретация является мо-
делью системы PR1. Но мы сейчас имеем существенное отличие от предыдущей интер-
претации: не все истинные утверждения вида x+y≥z являются теоремами в PR1. Так,
например, формула --P-R- имеет истинную интерпретацию 2+1 ≥ 1, но это не теорема.
22

Страницы