Jakie są negatywne konsekwencje rozszerzenia CIC o aksjomaty?

Czy to prawda, że ​​dodanie aksjomatów do CIC może mieć negatywny wpływ na zawartość obliczeniową definicji i twierdzeń? I zrozumieć, że w normalnych zachowań teoria, wszelkie zamknięte termin zostanie zredukowany do kanonicznej normalnej postaci, na przykład w przypadku jest prawdziwy, wówczas n może obniżać się okres postaci ( s U c c . . . ( A u c c ( 0 ) ) ) . Ale postulując aksjomat - powiedzmy aksjomat ekstensywności funkcji - po prostu dodajemy nową stałą do systemu$n : \mathbb{N}$$n$$(succ ... (succ (0)))$funext

to po prostu „magicznie” da dowód z dowolnego dowodu Π x : A f ( x ) = g ( x ) , bez żadnego znaczenia obliczeniowego ( w tym sensie, że nie możemy wyodrębnić z nich żadnego kodu? )$f = g$$\Pi_{x : A} f (x) = g (x)$

Ale dlaczego to „złe”?

Ponieważ funextprzeczytałem w tym wpisie coq i pytaniu o przepływ matematyki , że spowoduje to utratę przez system kanoniczności lub decydujące sprawdzanie. Wpis w coq wydaje się być dobrym przykładem, ale nadal chciałbym trochę więcej referencji na ten temat - i jakoś nie mogę ich znaleźć.

W jaki sposób dodanie dodatkowych aksjomatów może powodować gorsze zachowanie CIC? Wszelkie praktyczne przykłady byłyby świetne. (Na przykład aksjomat Univalence?) Obawiam się, że to pytanie jest zbyt miękkie, ale gdyby ktoś mógł rzucić nieco światła na te kwestie lub podać mi jakieś referencje, byłoby świetnie!

PS: Wpis o coq wspomina, że ​​„Thierry Coquand zauważył już, że dopasowanie wzorców w rodzinach intensywnych jest niespójne z ekstensywnością w połowie lat 90-tych”. Czy ktoś wie, w którym papierze czy coś?

Jednym z pierwszych powodów odrzucenia aksjomatów jest to, że mogą być niespójne. Nawet dla aksjomatów, które okazały się spójne, niektóre z nich mają interpretację obliczeniową (wiemy, jak rozszerzyć dla nich równość definicyjną za pomocą zasady redukcji), a niektóre nie - łamią kanoniczność. Jest to „złe” z różnych powodów:

• Teoretycznie kanoniczność pozwala udowodnić różne wartości twojego języka bez konieczności przechodzenia do konkretnego modelu. To bardzo satysfakcjonująca właściwość myślenia o systemie; w szczególności popiera twierdzenia o prawdziwym świecie - możemy myśleć o nattypie sformalizowanym w systemie jako naprawdę „liczbach naturalnych”, ponieważ możemy udowodnić, że jego zamknięci normalni mieszkańcy naprawdę są liczbami naturalnymi. W przeciwnym razie łatwo pomyśleć , że poprawnie wymodelowałeś coś w systemie, ale faktycznie pracujesz z różnymi obiektami.

• W praktyce redukcja jest głównym atutem teorii typów zależnych, ponieważ ułatwia dowód. Udowodnienie równości zdań może być dowolnie trudne, a udowodnienie równości definicji jest (rzadziej możliwe), ale znacznie łatwiejsze, ponieważ termin dowodu jest trywialny. Mówiąc bardziej ogólnie, obliczenia są kluczowym aspektem doświadczenia użytkownika asystenta dowodu i często definiuje się rzeczy tak, aby zmniejszały się prawidłowo, zgodnie z oczekiwaniami. (Nie potrzebujesz aksjomatów, aby utrudnić obliczenia; na przykład użycie zasady konwersji równości zdań może już blokować redukcje). Cały biznes dowodu przez refleksjęopiera się na wykorzystaniu obliczeń do pomocy dowodom. Jest to duża różnica w sile i wygodzie w porównaniu z innymi asystentami dowodowymi opartymi na logice (np. HOL-light, który obsługuje tylko rozumowanie równości; lub patrz Zombie na inne podejście), i przy użyciu niesprawdzonych aksjomatów lub innych stylów programowania, może wydostać cię z tej strefy komfortu.

Aby zrozumieć, dlaczego przedłużanie twierdzenia twierdzeniem o niektóre aksjomaty może powodować problemy, warto również zobaczyć, kiedy jest to łagodne. Przychodzą mi na myśl dwa przypadki i oba mają związek z tym, że nie dbamy o zachowanie obliczeniowe postulatów.

• W Teorii Typów Obserwacyjnych można postulować dowód dowolnej zgodności Propbez utraty kanoniczności. Rzeczywiście, wszystkie dowody są uważane za równe, a system egzekwuje to, całkowicie odmawiając spojrzenia na warunki. W konsekwencji fakt, że dowód został zbudowany ręcznie lub po prostu postulowany, nie ma znaczenia. Typowym przykładem może być dowód „spójności”: jeśli mamy dowód, eqże w A = B : Typeprzypadku dowolnego trodzaju A, t == coerce A B eq tgdzie coercepo prostu przenosi się termin wzdłuż dowodu równości.

• W MLTT można postulować dowolny spójny ujemny aksjomat bez utraty kanoniczności . Intuicja za tym stoi, że aksjomaty ujemne (aksjomaty formy A -> False) są zawsze używane tylko do odrzucenia nieistotnych gałęzi. Jeśli aksjomat jest spójny, wówczas można go stosować tylko w gałęziach, które rzeczywiście są nieistotne i dlatego nigdy nie zostaną uwzględnione przy ocenie warunków.

Praktyczny przykład źle zachowującego się aksjomatu, pytasz, a co z tym?

 0 = 1

Dokument Coquanda, o którym mowa, może być [1], gdzie pokazuje, że zależny ITT (intuicyjna teoria typów Martina-Löfa) rozszerzony o dopasowanie wzorca pozwala udowodnić UIP (aksjomat unikalności dowodów tożsamości ). Później Streicher i Hoffmann [2] przedstawiają model ITT, który fałszuje UIP. Dlatego dopasowanie wzorca nie jest konserwatywnym rozszerzeniem ITT.

1. T. Coquand, Dopasowywanie wzorców z typami zależnymi .

2. M. Hofmann, T. Streicher, Grupoidowa interpretacja teorii typów .