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

UptoLike

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

порядков. В таком языке мы можем также ввести и какие-то новые кванторы, а не только
кванторы общности и существования.
Резюме
Формулывыражения, обозначающие высказывания в языке логики предикатов.
Сложные формулы строятся из более простых при помощи логических связок.
Логические связки применяются к высказываниям и в результате дают высказывание.
Логические связки делятся на связки исчисления высказываний (или пропозициональ-
ные) и кванторы.
2.3.4 Свободные и связанные переменные
Обсудим очень важные понятия свободной и связанной переменных. В античной
математике (формальные) переменные практически не использовались. Под влиянием
Виета в конце 16 столетия переменные стали стандартным инструментом математики.
Было, однако, много недоразумений по поводу природы переменных. Например, цело-
численная переменная была «изменяющейся величиной», которая иногда четна, иногда
нечетна и может быть «зафиксирована» на время доказательства. Такие сущности, однако,
не существуют.
Фреге и Пирс прояснили истинную природу переменных: этосинтаксические
объекты, и следует различать свободные и связанные переменные.
Свободная переменнаяэто синтаксический объект, встречающийся в некотором
контексте, вместо которого можно подставлять другие синтаксические объекты. Когда
терм, содержащий свободные переменные, интерпретируется в некоторой универсуме M,
нужно выбрать элементы предметной области M, чтобы интерпретировать эти перемен-
ные.
С другой стороны, связанные переменные не допускают ни подстановки, ни выбо-
ра интерпретации. В следующих примерах переменная x связанная:
.1;1
100
0
2
1
0
2
++
=x
xdxx
Если терм t подставляется (без предосторожностей) вместо свободных вхождений
переменной y в выражение AA(y), то некоторые переменные в t могут стать связанными.
Пусть A(y) – истинная формула
,)(
3
1
1
0
2
+=+
ydxyx
и пусть t x; тогда A(x) – ложная формула
.
)(
3
1
1
0
2
+=+
xdxxx
Это явление называется коллизией переменных.
Говорят, что подстановка терма t вместо y в A корректна, если никакая свободная
переменная терма t не становится связанной после подстановки t вместо (свободных вхо-
ждений) переменной y в A. Именно некорректная подстановка вызвала только что упомя-
нутую коллизию переменных. Переименовывая связанные переменные в A, мы всегда мо-
жем избежать коллизии переменных. Например, подстановка t x вместо y в формулу
3
1
1
0
2
)( +=+
yduyu
является корректной.
17