А.Власов. "Нижнеуровневая масштабируемая реализация...
-
Upload
anatoly-levenchuk -
Category
Technology
-
view
729 -
download
5
description
Transcript of А.Власов. "Нижнеуровневая масштабируемая реализация...
![Page 1: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/1.jpg)
Уровни работы с ISO 15926
«Ассемблер» ISO 15926:2 - EXPRESS actual_individual, class_of_class
Аксиомы ISO 15926:7 - First Order Logic ActualIndididual(x) → PossibleIndividual(x)
«Темплейты» ISO 15926:7 (FOL/rewriting) ApprovalTriple(x, y, z) ↔ Approval(x) &
hasApproved(x, y) & hasApprover(x, z) OIM (Object Information Model) Domain specific templates???
DSL — internal/external (e.g. Python)
![Page 2: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/2.jpg)
Историческая перспектива
«Ассемблер» 15926:2 слишком сложен для неспециалистов
Решение — ввели «темплейты» 15926:7 fact oriented определены поверх аксиоматики на языке
First Order Logic (Prover9) аксиомы/темплейты нормативны в 15926:7,
т.е. де-факто reference implementation Альтеранативный вариант — ISO 15926:8
реализация поверх OWL Широкий набор OWL инструментария
![Page 3: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/3.jpg)
Проверка целостности
Основа реализации — проверка целостности описаний
К примеру, исключить случаи, когда ActualIndividual одновременно является ClassOfIndividual
«Референсная» проверка — относительно аксиоматики 15926:7
«Разворачиваем» темплейты Проверяем, что полученный набор
утверждений выполним относительно аксиоматики
![Page 4: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/4.jpg)
Проверка целостности с помощью логик
FOL provers (или model finders) e.g. Prover9 (and lots of others)
Трансляция в DL logics Provers: FaCT++, Pellet, RacerPro, HermiT
Трансляция в SAT (propositional logics) Не уверен, что всегда возможна прямая
трансляци, но можно использовать incremental подход
Другие логики HOL/Type-theory Избыточно, но удобно для встраивания в
языки и для мета-теор. целей
![Page 5: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/5.jpg)
Зачем делать свою реализацию?
Производительность/масштабируемость FOL слишком мощная для 15926:7: гибко, но
медленно К примеру, тормозит на абстрактных класс из-за недетерминизма (OR-branching) Большие размеры моделей O(a*n)/O(b*n2) для унарных/бинарных
предикатов Все описание обрабатывается одновременно возможно разбиение на подзадачи
![Page 6: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/6.jpg)
Зачем делать свою реализацию? (продолжение)
Поиск и индексация в хранилищах данных опирается на те же структуры данных
Создание инструментария и DSL Быстрая проверка на ошибки критична для
юзабилити Сообщения об ошибках К примеру, Осман уже реализовал :)
Мега-мета-проект: 15926L :)
![Page 7: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/7.jpg)
Общая идея алгоритмов проверки целостности
Пытаемся строить модель/интерпретацию для описания
для каждого класса (отношения) задаем список инстансов (пар), которые ему принадлежат
Проверяем (конечную) модель на соответствие аксиомам
Медленно, нужны оптимизации сотни предикатов/1000+ аксиом бинарные отношения - O(n2) недетерминизм
Надо учитывать особенности аксиоматики
![Page 8: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/8.jpg)
Построение модели
• T — теория (аксиомы), F — формула вида & | (плюс предикаты и константы)∃
• Берем все константы — исходное множество инстансов
• F преобразуем дизъюнктивную форму вида (A&B&C)|(D&E&F)|..|(X&Y&Z)– Or-branching — экспонента в worst-case
• Перебираем конъюнкты A(a)&B(b)&C(d)– Исходное множество утверждений– Выводим новые, используя аксиомы– Если модель непротиворечива - win
• Все конъюнкты противоречивы - fail
![Page 9: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/9.jpg)
Построение модели (аксиомы)
• A(x)&..&B(x) → C(x)– Если все A(a)..B(a) есть в текущей
модели, добавляем C(a)• A(x)&..&B(x) → C(x)|D(x)
– Or-branching– Дважды-экспоненциально в worst-case!
• ~(A(x)&..B(x))– Эквивалентно A(x)&..&B(x) → False– Если аксиома применима — противоречие
• A(x)&..&B(x) → u Φ(u,x)∃– Добавляем новые инстансы в модель– Потенциально неограниченные модели!– В 15926:2 к счастью ограниченны :)
![Page 10: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/10.jpg)
Особенности аксиоматики 15926:2
Единственный источник конфликтов disjoint аксиомы (one_of(Class1, Class2 etc))
Достаточно конечных моделей намекается в стандарте :)
Похоже можно избавится от бинарных отношений (e.g. hasClassifier(x,y))
Резко сокращает размеры моделей «Линейные» (компактные) модели В стандарте не намекается, но скорее всего :)
Недетерминизм в основном вызван трансляцией abstract class, но не только
![Page 11: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/11.jpg)
Альтернативный вариант
Проверка целостности как проверка типов некоторого языка программирования
Изначально так и примерно и было — EXPRESS language
Удобнее для встраивания в DSL Проблемы с использованием сущ. языков Множественное наследование Oneof (далеко не во всех языках) Недетерминизм Abstract class трансляция
![Page 12: А.Власов. "Нижнеуровневая масштабируемая реализация ISO15926"](https://reader036.fdocumento.com/reader036/viewer/2022082704/558d1765d8b42afb408b4687/html5/thumbnails/12.jpg)
Алтернативный вариант (продолжение)
Осман уже что-то сделал :) Скорее всего проблемы с недетерминизмом
Оптизимации алгоритма Инкрементальный (проверяем по частям) Компактные модели оптимизации недетерминизма оптимизации AND-branhing, быстрые
проверки конфликтов Хранилище данных Можно сделать эффективнее чем triple-store