Инвариантность модальных формул
 Скачать 1.26 Mb.
|
|
Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Неклассические логики и представление знаний Бисимуляция Отделение прикладной математики и информатики Высшая школа экономики Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Модальная эквивалентность Определение (w ! w 0 ) Миры w ∈ M и w 0 ∈ M 0 называются модально эквивалентными , если их теории совпадают: {φ | M, w |= φ} = {φ | M 0 , w 0 |= φ} Определение (M ! M 0 ) Модели M и M 0 называются модально эквивалентными , если их теории совпадают: {φ | M |= φ} = {φ | M 0 |= φ} Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение v1 v2 v3 v4 w M N v1 v2 v3 v4 w M ] N Если N, u |= φ, то M ] N, u |= φ? Если M ] N, u |= φ и u ∈ N, то N, u |= φ? Да: истинность в модели инвариантна относительно операции дизъюнктного объединения. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение v1 v2 v3 v4 w M N v1 v2 v3 v4 w M ] N Если N, u |= φ, то M ] N, u |= φ? Если M ] N, u |= φ и u ∈ N, то N, u |= φ? Да: истинность в модели инвариантна относительно операции дизъюнктного объединения. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение v1 v2 v3 v4 w M N v1 v2 v3 v4 w M ] N Если N, u |= φ, то M ] N, u |= φ? Если M ] N, u |= φ и u ∈ N, то N, u |= φ? Да: истинность в модели инвариантна относительно операции дизъюнктного объединения. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение v1 v2 v3 v4 w M N v1 v2 v3 v4 w M ] N Если N, u |= φ, то M ] N, u |= φ? Если M ] N, u |= φ и u ∈ N, то N, u |= φ? Да: истинность в модели инвариантна относительно операции дизъюнктного объединения. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение v1 v2 v3 v4 w M N v1 v2 v3 v4 w M ] N Если N, u |= φ, то M ] N, u |= φ? Если M ] N, u |= φ и u ∈ N, то N, u |= φ? Да: истинность в модели инвариантна относительно операции дизъюнктного объединения. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение Модели называются непересекающимися , если их носители не содержат общих элементов. Определение (Базовый случай) Дизъюнктное объединение непересекающихся моделей M i = (W i , R i , V i )(i ∈ I ): ] i M i = (W , R, V ) W = S i∈I W i R = S i∈I R i V (p) = S i∈I V i (p) для всех переменных p Дизъюнктное объединение пересекающихся моделей строится по их непересекающимся изоморфным копиям. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение Модели называются непересекающимися , если их носители не содержат общих элементов. Определение (τ -модели) Дизъюнктное объединение непересекающихся однотипных τ -моделей M i = (W i , R 4i , V i ) 4∈τ (i ∈ I ) : ] i M i = (W , R 4 , V ) 4∈τ W = S i∈I W i R 4 = S i∈I R 4i для всех 4 ∈ τ V (p) = S i∈I V i (p) для всех переменных p Дизъюнктное объединение пересекающихся моделей строится по их непересекающимся изоморфным копиям. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение Определение (τ -модели) Дизъюнктное объединение непересекающихся однотипных τ -моделей M i = (W i , R 4i , V i ) 4∈τ (i ∈ I ) : ] i M i = (W , R 4 , V ) 4∈τ W = S i∈I W i R 4 = S i∈I R 4i для всех 4 ∈ τ V (p) = S i∈I V i (p) для всех переменных p Дизъюнктное объединение пересекающихся моделей строится по их непересекающимся изоморфным копиям. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение Утверждение (Истинность формулы инвариантна относительно дизъюнктного объединения) Пусть τ — модальный тип сходства и M i — τ -модели для всех i ∈ I . Тогда для любой модальной формулы φ, любого i ∈ I и любого элемента w из M i верно M i , w |= φ ⇐⇒ ] j∈I M j , w |= φ. Доказательство. Докажем по индукции по φ для базового типа сходства. Пусть M = (W , R, V ) = U j∈I M j Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение Доказательство. Докажем по индукции по φ для базового типа сходства. Пусть M = (W , R, V ) = U j∈I M j p : M i , w |= φ ⇔ w ∈ V i (p) ⇔ w ∈ V (p) ⇔ M, w |= φ ⊥ : M i , w 6|= ⊥ и M, w 6|= ⊥ Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение Доказательство. Докажем по индукции по φ для базового типа сходства. Пусть M = (W , R, V ) = U j∈I M j p : M i , w |= φ ⇔ w ∈ V i (p) ⇔ w ∈ V (p) ⇔ M, w |= φ ⊥ : M i , w 6|= ⊥ и M, w 6|= ⊥ Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение Доказательство. Докажем по индукции по φ для базового типа сходства. Пусть M = (W , R, V ) = U j∈I M j Пусть утверждение верно для формулы с ≤ n связками. Покажем, что оно верно и для формулы с n + 1 связками. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение Доказательство. Докажем по индукции по φ для базового типа сходства. Пусть M = (W , R, V ) = U j∈I M j Пусть утверждение верно для формулы с ≤ n связками. Покажем, что оно верно и для формулы с n + 1 связками. Для ¬ψ и ψ ∨ θ доказательство тривиально. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение Доказательство. Докажем по индукции по φ для базового типа сходства. Пусть M = (W , R, V ) = U j∈I M j Пусть утверждение верно для формулы с ≤ n связками. Покажем, что оно верно и для формулы с n + 1 связками. Пусть M i , w |= ♦ψ Есть v ∈ W i , такой что R i wv и M i , v |= ψ M , v |= ψ (по индукции) M , w |= ♦ψ (т.к. Rwv) Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Дизъюнктное объединение Доказательство. Докажем по индукции по φ для базового типа сходства. Пусть M = (W , R, V ) = U j∈I M j Пусть утверждение верно для формулы с ≤ n связками. Покажем, что оно верно и для формулы с n + 1 связками. Пусть M, w |= ♦ψ для некоторого w ∈ W i Есть v ∈ W , такой что Rwv и M, v |= ψ R i wv (по определению R и т.к. модели непересекающиеся) v ∈ W i M i , v |= ψ (по индукции) M i , w |= ♦ψ (т.к. R i wv) Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Использование дизъюнктного объединения Двойственные глобальные модальные операторы E и A: M , w |= E φ ⇐⇒ M, v |= φ для некоторого v ∈ M M , w |= Aφ ⇐⇒ M, v |= φ для всех v ∈ M Можно ли определить E и A синтаксически в базовом модальном языке (через ♦)? Пусть α(p) — формула базового языка, соответствующая Ap: M , w |= α(p) ⇐⇒ M |= p Рассмотрим M 1 и M 2 , такие что M 1 |= p и M 2 |= ¬p w ∈ M 1 ⇒ M 1 , w |= α(p) ⇒ M 1 U M 2 , w |= α(p) ⇒ ∀v ∈ M 2 : M 2 , v |= p ⇒ M 2 |= p Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Использование дизъюнктного объединения Двойственные глобальные модальные операторы E и A: M , w |= E φ ⇐⇒ M, v |= φ для некоторого v ∈ M M , w |= Aφ ⇐⇒ M, v |= φ для всех v ∈ M Можно ли определить E и A синтаксически в базовом модальном языке (через ♦)? Пусть α(p) — формула базового языка, соответствующая Ap: M , w |= α(p) ⇐⇒ M |= p Рассмотрим M 1 и M 2 , такие что M 1 |= p и M 2 |= ¬p w ∈ M 1 ⇒ M 1 , w |= α(p) ⇒ M 1 U M 2 , w |= α(p) ⇒ ∀v ∈ M 2 : M 2 , v |= p ⇒ M 2 |= p Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Дизъюнктное объединение Использование дизъюнктного объединения Двойственные глобальные модальные операторы E и A: M , w |= E φ ⇐⇒ M, v |= φ для некоторого v ∈ M M , w |= Aφ ⇐⇒ M, v |= φ для всех v ∈ M Можно ли определить E и A синтаксически в базовом модальном языке (через ♦)? Пусть α(p) — формула базового языка, соответствующая Ap: M , w |= α(p) ⇐⇒ M |= p Рассмотрим M 1 и M 2 , такие что M 1 |= p и M 2 |= ¬p w ∈ M 1 ⇒ M 1 , w |= α(p) ⇒ M 1 U M 2 , w |= α(p) ⇒ ∀v ∈ M 2 : M 2 , v |= p ⇒ M 2 |= p Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Порожденные подмодели Порожденные подмодели -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, замкнутая относительно отношения достижимости. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Порожденные подмодели Порожденные подмодели -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, замкнутая относительно отношения достижимости. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Порожденные подмодели Порожденные подмодели -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 Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Бисимуляция Определение (Z : M - M 0 ) Пусть M = (W , R 4 , V ) 4∈τ и M 0 = (W 0 , R 0 4 , V 0 ) 4∈τ — τ -модели. Непустое отношение Z ⊆ W × W 0 является бисимуляцией между M и M 0 , если выполняются условия: 1 Если Zww 0 , то в w и в w 0 истинны одни и те же переменные. 2 Если Zww 0 и R 4 wv 1 . . . v n , то существуют v 0 1 , . . . , v 0 n , такие что R 0 4 w 0 v 0 1 . . . v 0 n и v i Zv 0 i (для 1 ≤ i ≤ n). 3 Если Zww 0 и R 0 4 w 0 v 0 1 . . . v 0 n , то существуют v 1 , . . . , v n , для которых R 4 wv 1 . . . v n и Zv i v 0 i (для 1 ≤ i ≤ n). Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Бисимуляция Бисимуляция — обобщение ограниченного морфизма. Истинность модальных формул инвариантна относительно бисимуляции: w - w 0 ⇒ w ! w 0 w - w 0 — существует бисимуляция Z : M - M 0 , такая что Zww 0 (w ∈ M, w 0 ∈ M 0 ) Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Бисимуляция и логика первого порядка Формулы логики первого порядка не инвариантны относительно бисимуляции: 0 1 2 3 4 5 e o p p p p ∃x∃y(R(x, y) & ¬R(y, x)) Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Модальная эквивалентность без бисимуляции w w' M N w 6 - w 0 , но w ! w 0 Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Теорема Хеннесси – Милнера Определение Модель M имеет конечный образ , если множество {(v 1 , . . . , v n ) | Ruv 1 . . . v n } конечно для всякого мира u и всякого отношения R из M. Теорема Если M и M 0 — τ -модели с конечным образом, то для любых w ∈ M и w 0 ∈ M 0 w - w 0 ⇐⇒ w ! w 0 Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Теорема Хеннесси – Милнера Доказательство. ⇐ Докажем, что ! — бисимуляция. Пусть w ! w 0 и Rwv, но не существует v 0 , такого что R 0 w 0 v 0 и v ! v 0 S 0 = {u 0 | R 0 w 0 u 0 } S 0 6= ∅ (т.к. M, w |= ♦> и w ! w 0 ) S 0 = {w 0 1 , . . . , w 0 n } (т.к. M 0 — модель с конечным образом) По предположению для каждого w 0 i ∈ S 0 найдется ψ i , такая что M, v |= ψ i и M 0 , w 0 i 6|= ψ i M , w |= ♦(ψ 1 & · · · & ψ n ) и M 0 , w 0 6|= ♦(ψ 1 & · · · & ψ n ) w 6 ! w 0 — противоречие Обратное условие бисимуляции доказывается так же. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Теорема Хеннесси – Милнера Доказательство. ⇐ Докажем, что ! — бисимуляция. Пусть w ! w 0 и Rwv, но не существует v 0 , такого что R 0 w 0 v 0 и v ! v 0 S 0 = {u 0 | R 0 w 0 u 0 } S 0 6= ∅ (т.к. M, w |= ♦> и w ! w 0 ) S 0 = {w 0 1 , . . . , w 0 n } (т.к. M 0 — модель с конечным образом) По предположению для каждого w 0 i ∈ S 0 найдется ψ i , такая что M, v |= ψ i и M 0 , w 0 i 6|= ψ i M , w |= ♦(ψ 1 & · · · & ψ n ) и M 0 , w 0 6|= ♦(ψ 1 & · · · & ψ n ) w 6 ! w 0 — противоречие Обратное условие бисимуляции доказывается так же. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Теорема Хеннесси – Милнера Доказательство. ⇐ Докажем, что ! — бисимуляция. Пусть w ! w 0 и Rwv, но не существует v 0 , такого что R 0 w 0 v 0 и v ! v 0 S 0 = {u 0 | R 0 w 0 u 0 } S 0 6= ∅ (т.к. M, w |= ♦> и w ! w 0 ) S 0 = {w 0 1 , . . . , w 0 n } (т.к. M 0 — модель с конечным образом) По предположению для каждого w 0 i ∈ S 0 найдется ψ i , такая что M, v |= ψ i и M 0 , w 0 i 6|= ψ i M , w |= ♦(ψ 1 & · · · & ψ n ) и M 0 , w 0 6|= ♦(ψ 1 & · · · & ψ n ) w 6 ! w 0 — противоречие Обратное условие бисимуляции доказывается так же. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Теорема Хеннесси – Милнера Доказательство. ⇐ Докажем, что ! — бисимуляция. Пусть w ! w 0 и Rwv, но не существует v 0 , такого что R 0 w 0 v 0 и v ! v 0 S 0 = {u 0 | R 0 w 0 u 0 } S 0 6= ∅ (т.к. M, w |= ♦> и w ! w 0 ) S 0 = {w 0 1 , . . . , w 0 n } (т.к. M 0 — модель с конечным образом) По предположению для каждого w 0 i ∈ S 0 найдется ψ i , такая что M, v |= ψ i и M 0 , w 0 i 6|= ψ i M , w |= ♦(ψ 1 & · · · & ψ n ) и M 0 , w 0 6|= ♦(ψ 1 & · · · & ψ n ) w 6 ! w 0 — противоречие Обратное условие бисимуляции доказывается так же. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Теорема Хеннесси – Милнера Доказательство. ⇐ Докажем, что ! — бисимуляция. Пусть w ! w 0 и Rwv, но не существует v 0 , такого что R 0 w 0 v 0 и v ! v 0 S 0 = {u 0 | R 0 w 0 u 0 } S 0 6= ∅ (т.к. M, w |= ♦> и w ! w 0 ) S 0 = {w 0 1 , . . . , w 0 n } (т.к. M 0 — модель с конечным образом) По предположению для каждого w 0 i ∈ S 0 найдется ψ i , такая что M, v |= ψ i и M 0 , w 0 i 6|= ψ i M , w |= ♦(ψ 1 & · · · & ψ n ) и M 0 , w 0 6|= ♦(ψ 1 & · · · & ψ n ) w 6 ! w 0 — противоречие Обратное условие бисимуляции доказывается так же. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Теорема Хеннесси – Милнера Доказательство. ⇐ Докажем, что ! — бисимуляция. Пусть w ! w 0 и Rwv, но не существует v 0 , такого что R 0 w 0 v 0 и v ! v 0 S 0 = {u 0 | R 0 w 0 u 0 } S 0 6= ∅ (т.к. M, w |= ♦> и w ! w 0 ) S 0 = {w 0 1 , . . . , w 0 n } (т.к. M 0 — модель с конечным образом) По предположению для каждого w 0 i ∈ S 0 найдется ψ i , такая что M, v |= ψ i и M 0 , w 0 i 6|= ψ i M , w |= ♦(ψ 1 & · · · & ψ n ) и M 0 , w 0 6|= ♦(ψ 1 & · · · & ψ n ) w 6 ! w 0 — противоречие Обратное условие бисимуляции доказывается так же. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Свойство конечной модели Определение Модальный тип τ обладает свойством конечной модели относительно класса τ -моделей M, если всякая τ -формула φ, выполнимая в некоторой модели из M, выполнима и в некоторой конечной модели из M. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Фильтрация Подформулы Определение Множество формул Σ замкнуто относительно взятия подформул , если: φ ∨ ψ ∈ Σ ⇒ φ ∈ Σ и ψ ∈ Σ ¬φ ∈ Σ ⇒ φ ∈ Σ 4(φ 1 , . . . , φ n ) ∈ Σ ⇒ φ 1 ∈ Σ, . . . , φ n ∈ Σ Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Фильтрация Фильтрация M f Σ по Σ = {♦p, p} 0 4 3 1 2 p, q p p p Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Фильтрация Фильтрация M f Σ по Σ = {♦p, p} |0| 0 4 3 1 2 p, q p p p |1| W f — один мир для каждого набора значений формул из Σ Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Фильтрация Фильтрация M f Σ по Σ = {♦p, p} |0| 0 4 3 1 2 p, q p p p |1| p V f (p) = {|w| | M, w |= p} для всех переменных из Σ Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Фильтрация Фильтрация M f Σ по Σ = {♦p, p} |0| 0 4 3 1 2 p, q p p p |1| p Rwv ⇒ R f |w||v| R f |w||v|, ♦φ ∈ Σ и M, v |= φ ⇒ M, w |= ♦φ Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Фильтрация Фильтрация M f Σ по Σ = {♦p, p} |0| 0 4 3 1 2 p, q p p p |1| p Фильтрация является гомоморфизмом, но не всегда является ограниченным морфизмом. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Фильтрация Размер фильтрации Утверждение Фильтрация по множеству формул Σ, замкнутому относительно взятия подформул, содержит не более 2 |Σ| элементов. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Фильтрация Теорема о фильтрации для базового модального языка Теорема Пусть M f Σ — фильтрация M по множеству формул Σ, замкнутому относительно взятия подформул. Тогда для любых φ ∈ Σ и w ∈ M M , w |= φ ⇐⇒ M f Σ , |w| |= φ. Доказательство. Индукция по φ. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Фильтрация Свойство конечной модели Теорема Если формула базового модального языка φ выполнима, то она выполнима и в конечной модели, содержащей не более 2 m возможных миров, где m — количество подформул формулы φ. Доказательство. Если φ выполнима в модели M, то φ выполнима в любой фильтрации M по множеству всех подформул φ. Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Упражнение Докажите, что истинность темпоральных формул инвариантна относительно темпоральной бисимуляции. Пусть M и M 0 — конечные корневые темпоральные модели с корнями w и w 0 . Докажите, что если в w и w 0 истинны одни и те же формулы, то существует темпоральная бисимуляция, связывающая w и w 0 Неклассические логики и представление знаний ВШЭ Инвариантность модальных формул Бисимуляция Конечные модели Упражнения Упражнение Докажите, что истинность темпоральных формул инвариантна относительно темпоральной бисимуляции. Пусть M и M 0 — конечные корневые темпоральные модели с корнями w и w 0 . Докажите, что если в w и w 0 истинны одни и те же формулы, то существует темпоральная бисимуляция, связывающая w и w 0 Неклассические логики и представление знаний ВШЭ |