System U

W logice matematycznej System U i System U ⁻ są systemami typu czystego , tj. specjalnymi formami typowanego rachunku lambda z dowolną liczbą sortowań , aksjomatów i reguł (lub zależności między sortowaniami). W 1972 r. Jean-Yves Girard udowodnił, że oba są niespójne. Wynik ten doprowadził do uświadomienia sobie, że oryginalna teoria typów Martina-Löfa z 1971 r. był niespójny, ponieważ pozwalał na takie samo zachowanie typu „wpisz w typie”, które wykorzystuje paradoks Girarda.

Definicja formalna

System U jest zdefiniowany jako system typu czystego z

• trzy rodzaje ${\ Displaystyle \ {\ ast, \ kwadrat, \ trójkąt \}}$ ;
• dwa aksjomaty ${\ Displaystyle \ {\ ast: \ kwadrat, \ kwadrat: \ trójkąt \}}$ ; I
• pięć reguł ${\ Displaystyle \ {(\ ast, \ ast), (\ kwadrat, \ast ),(\kwadrat ,\kwadrat ),(\trójkąt ,\ast ),(\trójkąt ,\kwadrat )\}}$ .

System U ^- jest zdefiniowany tak samo, z wyjątkiem reguły ${\ Displaystyle (\ trójkąt, \ ast)}$ .

Rodzaje $”$ są umownie nazywane odpowiednio „Typem $;$ i „ Rodzajem sortowanie nie ma określonej $.$ Te dwa aksjomaty opisują zawieranie typów w rodzajach ( $\ Displaystyle \ trójkąt$ i rodzajach w $}$ ( $Displaystyle \ kwadrat: \ trójkąt}$ ). Intuicyjnie, rodzaje opisują hierarchię w naturze terminów.

1. Wszystkie wartości mają typ , taki $odczytywany$ typ podstawowy ( . jako „ ${\ Displaystyle f: \ operatorname {Nat} \ do \ operatorname {Bool}}$ jest wartością logiczną ”) lub (zależny) typ funkcji . jest odczytywane jako „ f jest funkcją od liczb naturalnych do logicznych”).
2. ${\ displaystyle \ ast}$ jest rodzajem wszystkich takich typów ( ${\ displaystyle t: \ ast}$ jest odczytywane jako „ t jest typem”). ∗ $\ displaystyle \ ast}$ możemy zbudować więcej terminów, takich jak ${\ displaystyle \ ast \ do \ ast},$ który jest rodzajem jednoargumentowych operatorów na poziomie typu ( np. ${ \displaystyle \mathrm {Lista} :\ast \to \ast }$ jest odczytywane jako „ Lista jest funkcją od typów do typów”, czyli typem polimorficznym). Zasady ograniczają sposób, w jaki możemy tworzyć nowe rodzaje.
3. ${\ Displaystyle \ kwadrat}$ jest rodzajem wszystkich takich rodzajów ( ${\ Displaystyle k: \ kwadrat}$ jest odczytywane jako „ k jest rodzajem”). Podobnie możemy budować terminy pokrewne, zgodnie z tym, na co pozwalają reguły.
4. ${\ displaystyle \ trójkąt}$ to rodzaj wszystkich takich terminów.

Reguły rządzą zależnościami między sortowaniami: ${\ Displaystyle (\ ast, \ ast)}$ mówi, że wartości mogą zależeć od wartości ( funkcji ), ${\ Displaystyle (\ kwadrat, \ ast )}$$na zależność$ zależność wartości od typów ( polimorfizm ) , od typów ( operatory typów ) i tak dalej

Paradoks Girarda

Definicje Systemu U i U ⁻ pozwalają na przypisanie rodzajów polimorficznych do ogólnych konstruktorów analogicznie do polimorficznych typów terminów w klasycznych polimorficznych rachunkach lambda, takich jak System F . Przykładem takiego ogólnego konstruktora może być (gdzie k oznacza rodzaj zmiennej)

${\ Displaystyle \ lambda k ^ {\ kwadrat} \ lambda \ alfa ^ {k \ do k} \ lambda \ beta ^ {k }\!.\alpha (\alpha \beta )\;:\;\Pi k:\square ((k\to k)\to k\to k)}$ .

$)$$do$ terminu o typie typu co każdy typ jest zamieszkany . Zgodnie z korespondencją Curry'ego – Howarda jest to równoważne z możliwością udowodnienia wszystkich twierdzeń logicznych, co czyni system niespójnym.

Paradoks Girarda jest teoriotypowym odpowiednikiem paradoksu Russella w teorii mnogości .

Dalsza lektura

• Barendregt, Henk (1992). „Rachunki lambda z typami” . W S. Abramskim; D. Gabbay; T. Maibaum (red.). Podręcznik logiki w informatyce . Publikacje naukowe z Oksfordu . s. 117–309.
• Coquand, Thierry (1986). „Analiza paradoksu Girarda”. Logika w informatyce . IEEE Computer Society Press. s. 227–236.