«Представление знание с помощью гомотопической теории типов»; проблема в эпистемологии, не в синтаксисе
Работа Андрея Родина «Knowledge Representation with HoTT» — об использовании гомотопической теории типов для представления знания. Я слабо владею теорий типов на теоретическом уровне, чтобы обсуждать специфические моменты именно предлагаемого формализма, но сам автор обращается к эпистемологии, и тут у меня есть замечания.
В сообществах, связанных с KR, бытует надежда, что для продвижения в области обязательно нужна некая новая хитрая синтаксическая структура и связанный с ней вычислительный формализм. Линейные формулы разных логик, графы и мультиграфы, вектора и матрицы, как средства представления перепробовали, но дело сильно не продвигается.
Мой тезис в том, что главная проблема не в отсутствии вычислительного формализма синтаксического уровня — как из одни буковок/формул получать другие. Проблема в качестве ontological commitments и symbol grounding (но на самом деле ещё дальше) — в оптике, в методе нарезки мира на области, которые связываются со значками, с элементами формализма, включая — и это критично — те, что обычно существуют на периферии или за пределами фокуса рассмотрения, вроде знака =.
Сложность находится в самом подходе к эпистемологическому вводу-выводе из модели, в том как дёшево получать достаточное разнообразие переносимых состояний, отражающих сверхсложные предметные области (как юриспруденция, мон амур). Для относительно простых областей и простых задач существующие подходы формализмы могут удовлетворительно работать, но они очевидно плохо масштабируются.
На мой взгляд, ключ к проблеме лежит не в вычислительном синтаксисе; и не в вычислительно семантике, вроде единственной правильной онтологии или методе социализации многих; а как минимум в области вычислительной эпистемологии — методе управления и вычисления метаонтологических параметров, базальных состояний, определяющих качество концептуального различения. Для сверхсложных областей не менее чем такой уровень абстрагирования может что-то решить. Именно поэтому многие теоретики быстро выпрыгивают в эпистемологические вопросы при конструировании онтологий для таких областей, и делают уже достаточно давно — Хукстра и Брюкер позиционировали FOLaw / LRI-Core как эпистемологический фреймвок уже в 2004, а Йерденфорс обозначил проблему концептуальной репрезентации как эпистемологическую в 2000.
Родин также начинает с этого, и, насколько я могу понять, реализует что-то вида метапаттернистского или метаконнекционистского подхода на аппарате HoTT. Отлично, но это, на мой взгляд, не многое добавляет к иным попыткам сделать примерно то же самое — уловить многомасштабные паттерны/гомотопии — в иных синтаксисах. Упомянутый ввод-вывод, а точнее — метапараметры (или связь с надсистемой в СИ-терминах), особо не прорабатываются, и это сильно ограничивает — любой метод, не только KR over HoTT. Редкий и интересный фокус в этой работе — это «The new interpretation of equality in HoTT», но подробности в тексте не раскрыты.
Обоснованная истинная вера в JTB, берётся, как не предполагающая альтернатив. Но уже именно эта святая троица становится камнем преткновения.
Проскальзывает интересная ссылка на Jukus et al. 2013 с очень действие-центричным определением знания; меня заинтриговало, но не могу найти источник.