Co sprawia, że ​​język (i jego system typów) jest w stanie udowodnić twierdzenia o swoich terminach?

Niedawno próbowałem zaimplementować Cedille-Core Aarona , minimalistyczny język programowania zdolny do udowodnienia twierdzeń matematycznych na temat własnych terminów. Udowodniłem również indukcję dla typów danych zakodowanych na λ, co wyjaśniło, dlaczego jego rozszerzenia byłyby konieczne.

Nie mówiąc już o tym, wciąż zastanawiam się, skąd pochodzą te rozszerzenia. Dlaczego są tacy, jacy są? Co je usprawiedliwia? Wiem na przykład, że niektóre rozszerzenia, takie jak rekurencja, rujnują język jako system dowodów. Gdybym zdecydował się rozszerzyć CoC na inne prymitywy, jak mam to uzasadnić? Rozumiem, że dowód normalizacji jest konieczny, ale to nie dowodzi, że te prymitywne „mają sens”.

Krótko mówiąc, co konkretnie kwalifikuje język (i jego system typów) jako system zdolny do udowodnienia twierdzeń o własnych terminach?

[Następuje autoreklama, ale myślę, że jest to istotne.]

$t$$u$$t \equiv u$$t$$u$$\forall v, (\lambda x.x)\;v \equiv v$

Oczywiście można również założyć równoważności, a istnieje kilka różnych form kwantyfikatorów (typowane / nietypowe, uniwersalne / egzystencjalne). Tego mechanizmu można użyć do uzasadnienia dowolnego programu (nie trzeba ich potwierdzać, że kończą, a nawet pisać). Jedynym ograniczeniem jest to, że programy używane jako dowody muszą zostać udowodnione przez system (arbitralna rekurencja ogólna prowadzi do niespójności).

Oto kilka referencji, jeśli chcesz to sprawdzić:

• https://lepigre.fr/files/docs/lepigre2017_pml2.pdf (najnowszy artykuł z przykładami)
• https://tel.archives-ouvertes.fr/tel-01590363 (praca doktorska w języku angielskim)
• https://github.com/rlepigre/pml (implementacja języka)