ВУЗ: Не указан
Категория: Не указан
Дисциплина: Не указана
Добавлен: 18.10.2024
Просмотров: 14
Скачиваний: 0
ВНИМАНИЕ! Если данный файл нарушает Ваши авторские права, то обязательно сообщите нам.
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Порожденные подмодели
Порожденные подмодели
-3
-2
-1 0
1 2
3
M = (Z, <)
-3
-2
-1 0
0 1
2 3
M
−
M
+
Если M
−
, u |= φ, то M, u |= φ?
Нет:
M
−
, 0 |= ⊥, но M, 0 6|= ⊥
Если M
+
, u |= φ, то M, u |= φ?
Да:
M
+
— подмодель M, замкнутая относительно отношения достижимости.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Порожденные подмодели
Порожденные подмодели
-3
-2
-1 0
1 2
3
M = (Z, <)
-3
-2
-1 0
0 1
2 3
M
−
M
+
Если M
−
, u |= φ, то M, u |= φ?
Нет:
M
−
, 0 |= ⊥, но M, 0 6|= ⊥
Если M
+
, u |= φ, то M, u |= φ?
Да:
M
+
— подмодель M, замкнутая относительно отношения достижимости.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Порожденные подмодели
Порожденные подмодели
Базовый модальный язык
Определение
M
0
= (W
0
, R
0
, V
0
) —
подмодель
M = (W , R, V ), если
W
0
⊆ W
R
0
= R ∩ (W
0
× W
0
)
V
0
(p)
= V (p) ∩ W
0
для всех переменных p
Определение (M
0
M)
M
0
= (W
0
, R
0
, V
0
) —
порожденная подмодель
M = (W , R, V ),
если M
0
— подмодель M и
w ∈ W
0
и Rwv
⇒
v ∈ W
0
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Порожденные подмодели
Порожденные подмодели
Общий случай
Определение
M
0
= (W
0
, R
0 4
, V
0
)
4∈τ
—
подмодель
M = (W , R
4
, V )
4∈τ
:
W
0
⊆ W
R
0 4
= R
4
∩ W
0n
для всех 4 ∈ τ арности n − 1
V
0
(p)
= V (p) ∩ W
0
для всех переменных p
Определение (M
0
M)
M
0
= (W
0
, R
0 4
, V
0
)
4∈τ
—
порожденная подмодель
M = (W , R
4
, V )
4∈τ
, если M
0
— подмодель M и
∀4 ∈ τ :
w ∈ W
0
и R
4
ww
1
. . . w
n
⇒
w
1
. . . w
n
∈ W
0
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Порожденные подмодели
Порожденные подмодели
Определение
Подмодель
M,
порожденная множеством возможных миров
X ⊆ M, — наименьшая порожденная подмодель M,
содержащая все миры из X .
Определение
Корневая подмодель
M — подмодель M, порожденная множеством, сотоящим из одного возможного мира, который называется корнем этой подмодели.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Порожденные подмодели
Порожденные подмодели
Утверждение (Истинность формулы инвариантна относительно порожденных подмоделей)
Пусть τ — модальный тип сходства и M
0
M — τ -модели.
Тогда для любой модальной формулы φ и любого элемента
w из M
0
верно
M
, w |= φ ⇐⇒ M
0
, w |= φ.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Морфизмы
Морфизм
— отображение, сохраняющее структурные свойства
Какие морфизмы гарантируют инвариантность истинности формул?
Гомоморфизмы
— нет
Сильные гомоморфизмы
— да (но это слишком сильно)
Ограниченные морфизмы
— да
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Гомоморфизмы
Определение (f : M → M
0
)
Пусть τ — модальный тип сходства, а M и M
0
— τ -модели.
Гомоморфизм
f из M в M
0
— это функция f из W в W
0
:
1
Если w ∈ V (p), то f (w) ∈ V
0
(p) для любой переменной p
и любого мира w из M.
2
Если (w
0
, . . . , w
n
) ∈ R
4
, то (f (w
0
), . . . , f (w
n
)) ∈ R
0 4
для любых n ≥ 0, n-арного оператора 4 ∈ τ и кортежа w из
n + 1 элементов M (условие гомоморфизма).
M называется областью отправления
, а M
0
—
областью назначения гомоморфизма.
Условие гомоморфизма для базового модального языка:
Rwu ⇒ R
0
f (w)f (u)
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Гомоморфизмы
Определение (f : M → M
0
)
Пусть τ — модальный тип сходства, а M и M
0
— τ -модели.
Гомоморфизм
f из M в M
0
— это функция f из W в W
0
:
1
Если w ∈ V (p), то f (w) ∈ V
0
(p) для любой переменной p
и любого мира w из M.
2
Если (w
0
, . . . , w
n
) ∈ R
4
, то (f (w
0
), . . . , f (w
n
)) ∈ R
0 4
для любых n ≥ 0, n-арного оператора 4 ∈ τ и кортежа w из
n + 1 элементов M (условие гомоморфизма).
M называется областью отправления
, а M
0
—
областью назначения гомоморфизма.
Условие гомоморфизма для базового модального языка:
Rwu ⇒ R
0
f (w)f (u)
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Гомоморфизмы
Определение (f : M → M
0
)
Пусть τ — модальный тип сходства, а M и M
0
— τ -модели.
Гомоморфизм
f из M в M
0
— это функция f из W в W
0
:
1
Если w ∈ V (p), то f (w) ∈ V
0
(p) для любой переменной p
и любого мира w из M.
2
Если (w
0
, . . . , w
n
) ∈ R
4
, то (f (w
0
), . . . , f (w
n
)) ∈ R
0 4
для любых n ≥ 0, n-арного оператора 4 ∈ τ и кортежа w из
n + 1 элементов M (условие гомоморфизма).
M называется областью отправления
, а M
0
—
областью назначения гомоморфизма.
Условие гомоморфизма для базового модального языка:
Rwu ⇒ R
0
f (w)f (u)
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Сильные гомоморфизмы
Модальные формулы не инварианты относительно гомоморфизмов.
Заменив условия (1) и (2) на эквивалентности, получим определение сильного гомоморфизма
Условие сильного гомоморфизма для базового модального языка:
Rwu ⇔ R
0
f (w)f (u)
Связи, задаваемые отношением, сохраняются в обе стороны
M ∼
= M
0
: Модель M
изоморфна модели M
0
, если существует биективный сильный гомоморфизм из M в
M
0
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Сильные гомоморфизмы
Модальные формулы не инварианты относительно гомоморфизмов.
Заменив условия (1) и (2) на эквивалентности, получим определение сильного гомоморфизма
Условие сильного гомоморфизма для базового модального языка:
Rwu ⇔ R
0
f (w)f (u)
Связи, задаваемые отношением, сохраняются в обе стороны
M ∼
= M
0
: Модель M
изоморфна модели M
0
, если существует биективный сильный гомоморфизм из M в
M
0
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Сильные гомоморфизмы
Модальные формулы не инварианты относительно гомоморфизмов.
Заменив условия (1) и (2) на эквивалентности, получим определение сильного гомоморфизма
Условие сильного гомоморфизма для базового модального языка:
Rwu ⇔ R
0
f (w)f (u)
Связи, задаваемые отношением, сохраняются в обе стороны
M ∼
= M
0
: Модель M
изоморфна модели M
0
, если существует биективный сильный гомоморфизм из M в
M
0
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Сильные гомоморфизмы
Модальные формулы не инварианты относительно гомоморфизмов.
Заменив условия (1) и (2) на эквивалентности, получим определение сильного гомоморфизма
Условие сильного гомоморфизма для базового модального языка:
Rwu ⇔ R
0
f (w)f (u)
Связи, задаваемые отношением, сохраняются в обе стороны
M ∼
= M
0
: Модель M
изоморфна модели M
0
, если существует биективный сильный гомоморфизм из M в
M
0
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Сильные гомоморфизмы
Модальные формулы не инварианты относительно гомоморфизмов.
Заменив условия (1) и (2) на эквивалентности, получим определение сильного гомоморфизма
Условие сильного гомоморфизма для базового модального языка:
Rwu ⇔ R
0
f (w)f (u)
Связи, задаваемые отношением, сохраняются в обе стороны
M ∼
= M
0
: Модель M
изоморфна модели M
0
, если существует биективный сильный гомоморфизм из M в
M
0
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Сильные гомоморфизмы
Утверждение
Пусть τ — модальный тип сходства, а M и M
0
— τ -модели.
Тогда:
1
Для любых элементов w из M и w
0
из M
0
, если существует сюръективный сильный гомоморфизм
f : M → M
0
, такой что f (w) = w
0
, то w и w
0
модально эквивалентны.
2
Если M ∼
= M
0
, то M
! M
0
Доказательство.
1
Индукцией по φ.
2
Непосредственно следует из (1).
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Слишком сильные гомоморфизмы
Как и везде в математике, изоморфные структуры являются математически идентичными —
неразличимыми.
Многие морфизмы, гарантирующие инвариантность модальных формул, не являются сильными гомоморфизмами.
Важно, чтобы некоторые характеристики области назначения морфизма были отражены в структуре области отправления морфизма.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Ограниченные морфизмы
Определение (Базовый случай)
Пусть M = (W , R, V ) и M
0
= (W
0
, R
0
, V
0
) — модели базового модального языка. Отображение f : M → M
0
является ограниченным морфизмом
, если:
1
В w и в f (w) истинны одни и те же переменные.
2
f является гомоморфизмом относительно R:
если Rwv, то R
0
f (w)f (v).
3
Если R
0
f (w)v
0
, то существует v, для которого Rwv и
f (v) = v
0
(
обратное условие
).
Если существует сюръективный ограниченный морфизм из
M в M
0
, то пишем
M
M
0
.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Ограниченные морфизмы
Пример
0 1
2 3
4 5
e
o
p
p
p
p
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Ограниченные морфизмы
Определение (Общий случай)
Пусть M и M
0
— τ -модели. Отображение f : M → M
0
является ограниченным морфизмом
, если:
1
В w и в f (w) истинны одни и те же переменные.
2
Если R
4
wv
1
. . . v
n
, то R
0 4
f (w)f (v
1
) . . . f (v
n
) для всех
4 ∈ τ .
3
Если R
0 4
f (w)v
0 1
. . . v
0
n
, то существуют v
1
, . . . , v
n
, для которых R
4
wv
1
. . . v
n
и f (v
i
) = v
0
i
(для 1 ≤ i ≤ n).
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Ограниченные морфизмы
Логика стрелок
M = (W , C , R, I , V )
M
0
= (W
0
, C
0
, R
0
, I
0
, V
0
)
W = Z × Z
W
0
= Z
Cxyz ⇐⇒ x
0
= y
0
, y
1
= z
0
и z
1
= x
1
C
0
xyz ⇐⇒ x = y + z
Rxy ⇐⇒ x
0
= y
1
и y
0
= x
1
R
0
xy ⇐⇒ x = −y
Ix ⇐⇒ x
0
= x
1
I
0
x ⇐⇒ x = 0
V (p) = {(x
0
, x
1
) | x
1
− x
0
— четно}
V
0
(p) = {x ∈ Z | x — четно}
Ограниченный морфизм f : M → M
0
f (z) = z
1
− z
0
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Морфизмы для модальных языков
Ограниченные морфизмы
Логика стрелок
M = (W , C , R, I , V )
M
0
= (W
0
, C
0
, R
0
, I
0
, V
0
)
W = Z × Z
W
0
= Z
Cxyz ⇐⇒ x
0
= y
0
, y
1
= z
0
и z
1
= x
1
C
0
xyz ⇐⇒ x = y + z
Rxy ⇐⇒ x
0
= y
1
и y
0
= x
1
R
0
xy ⇐⇒ x = −y
Ix ⇐⇒ x
0
= x
1
I
0
x ⇐⇒ x = 0
V (p) = {(x
0
, x
1
) | x
1
− x
0
— четно}
V
0
(p) = {x ∈ Z | x — четно}
Ограниченный морфизм f : M → M
0
f (z) = z
1
− z
0
Неклассические логики и представление знаний
ВШЭ