Неразличимые доказательства: по определению, но без аксиомы К

38 Просмотры

Спасибо! Поделитесь с друзьями!

Вам не понравилось видео. Спасибо за то что поделились своим мнением!

Издатель Nov 5, 2020

Не секрет, что формализация математики, логики, языков программирования, а также верификация программ с использованием теории типов наталкивается на сложности работы с иерархией равенств в теории типов. Научный фольклор не случайно пестрит упоминаниями "геенны сетоидной". При этом, чем больше термов вычислительно равны, т.е. неразличимы в используемой формальной системе, тем проще с ней работать на практике -- как в смысле сокращения ручного труда, так и увеличения производительности проверки типов, например, при использовании рефлексивных доказательств. В особенности это справедливо для термов, интерпретируемых как доказательства неразличимости высказываний. Однако, безыскусное внедрение неразличимости доказательств в теорию типов приводит либо к потере разрешимости проверки типов, либо к потере совместимости с другими расширениями базовой теории, такими как унивалентность.

Первая часть доклада подготовит почву для освещения основной темы: в частности будет рассмотрена структура вселенных в системе интерактивных доказательств Coq. Во второй части пойдет речь об относительно недавно добавленной экспериментальной вселенной строгих высказываний SProp с неразличимыми по определению доказательствами. При этом сохраняются перечисленные выше желательные свойства и показывается неадекватность известного подхода одиночной элиминации во вселенной Prop для настоящей проблемы. Также будет показана связь SProp с другими вселенными на простых примерах.

Докладчик: Антон Трунов

Материалы

1. "Definitional proof-irrelevance without K" - G. Gilbert, J. Cockx, M. Sozeau, N. Tabareau (2019), https://dl.acm.org/doi/10.1145/329031

2. The Coq Reference Manual: https://coq.github.io/doc/master/refman/addendum/sprop.html