Тип сквоша
Ця стаття містить перелік посилань, але походження тверджень у ній залишається незрозумілим через практично повну відсутність внутрішньотекстових джерел-виносок. (8 лютого 2021) |
Тип сквоша (пропозиційне обрізання) — тип, який «стискає» або «обрізає» тип до пропозиційної секвенції у гомотопічній теорії типів. Позначається подвійною вертикальною рискою .
Визначення
ред.Для будь-якого терму типу існує пропозиційне обрізання , де — образ у Її можна розглядати як формальну операцію, яка робить рівними усі терми, які належать до даного типу («населяють» його). Інший випадок, де для будь-яких має місце гарантує, що — пропозиція.
Принцип рекурсії для полягає у тому, що якщо — пропозиція та то існує індукована функція така, що для усіх Іншими словами, будь-яка пропозиція слідує з Таким чином, пропозиція не містить більше інформації, ніж факт належності (населеності) Завдяки пропозиційному обрізанню можна розширити логіку простих пропозицій, щоб охопити диз'юнкцію й квантор існування. Зокрема, проста пропозиційна версія « або » яка не «запам'ятовує» інформацію про те, який диз'юнкт є істинним. Принцип рекурсії для обрізання має на увазі, що можна провести аналіз на випадок при спробі доказати просту пропозицію. Іншими словами, якщо — пропозиція, то для визначення достатньо побудувати функцію
Якщо проста пропозиція, то В силу для справедливе Припустимо, що сімейство типів таке, що
- для будь-якого тип є простою пропозицією та
- для будь-якого має місце
Тоді
Можна визначити предикат такий, що є простою пропозицією. Тоді з елемента отримується елемент такий, що тому з можна побудувати і тому, що може бути отриманий елемент з
Таким чином, вибір єдиний.
Якщо ми хочемо визначити функцію та в залежності від елемента доказати просто існування декотрого необхідно визначити елемент з шляхом допрацювання аргументу для унікального існування як у теорії типів. У теорії множин ця проблема вирішується застосуванням аксіоми вибору, яка допомагає вибрати необхідні елементи. Таким чином, якщо не є множиною (наприклад, універсумом ), то не існує узгодженої форми вибору, яка дозволила б просто вибрати елемент з для кожного для використання у визначенні
Аксіома вибору
ред.Запис у звичайній нотації
перепишеться
де «існує таке, що » записується як Це еквівалентно формулюванню, що для будь-якої множини та будь-якого такого, що кожне є множиною, має місце де Та навпаки, та
Це відповідає відомій еквівалентній формі класичної аксіоми вибору, а саме:
Дано набір непорожніх множин, їхній декартів добуток є непорожньою множиною.
Програмування
ред.Пропозиційне обрізання дозволяє перевести тип \Type у пропозицію \Prop. У мові Arend є спеціальні універсуми \Prop та \Set, які складаються з пропозицій та множин, відповідно. Якщо відомо, що тип А міститься у \Prop (або \Set), то доказ відповідної властивості isProp (або isSet) у Arend може бути отриманий за допомогою вбудованої до прелюдії аксіоми Path.inProp:
\func inProp {A : \Prop} : \Pi (a a' : A) -> a = a'
Посилання
ред.- Homotopy Type Theory [Архівовано 5 травня 2019 у Wayback Machine.]
- nLab [Архівовано 24 лютого 2021 у Wayback Machine.]