System typu czystego

Nierozwiązany problem w informatyce :

Udowodnij lub obal hipotezę Barendregta–Geuversa–Klopa.

(więcej nierozwiązanych problemów w informatyce)

W gałęziach logiki matematycznej znanych jako teoria dowodu i teoria typów , system czystych typów ( PTS ), wcześniej znany jako uogólniony system typów ( GTS ), jest formą typowanego rachunku lambda , która pozwala na dowolną liczbę rodzajów i zależności między którekolwiek z nich. Schemat można postrzegać jako uogólnienie kostki lambda Barendregta w tym sensie, że wszystkie narożniki sześcianu można przedstawić jako instancje PTS z tylko dwoma rodzajami . Faktycznie Barendregt (1991) umieścił swoją kostkę w tej scenerii. Systemy typu czystego mogą przesłaniać rozróżnienie pomiędzy typy i terminy oraz zwijają hierarchię typów , jak ma to miejsce w przypadku rachunku konstrukcji , ale generalnie tak nie jest, np. po prostu wpisany rachunek lambda pozwala, aby tylko terminy były zależne od terminów.

Systemy typu czystego zostały wprowadzone niezależnie przez Stefano Berardi (1988) i Jana Terlouwa (1989). Barendregt omówił je szczegółowo w swoich kolejnych artykułach. W swojej pracy doktorskiej Berardi zdefiniował sześcian logiki konstrukcyjnej podobny do kostki lambda (te specyfikacje są niezależne). Modyfikacja tej kostki została później nazwana przez Geuversa kostką L, który w swojej pracy doktorskiej rozszerzył korespondencję Curry’ego – Howarda na to ustawienie. Opierając się na tych pomysłach, Barthe i inni zdefiniowali klasyczne systemy czystego typu ( CPTS ), dodając podwójną negację operator. Podobnie w 1998 r. Tijn Borghuis wprowadził modalne systemy czystego typu ( MPTS ). Roorda omówił zastosowanie systemów czystego typu do programowania funkcjonalnego ; a Roorda i Jeuring zaproponowali język programowania oparty na systemach czystych typów.

Wiadomo, że wszystkie układy z kostki lambda wykazują silne działanie normalizujące . Systemy typu czystego w ogóle nie muszą być, na przykład System U z paradoksu Girarda nie jest. (Z grubsza rzecz biorąc, Girard znalazł czyste systemy, w których można wyrazić zdanie „typy tworzą typ”.) Co więcej, wszystkie znane przykłady systemów czystych typów, które nie są silnie normalizujące, nie są nawet (słabo) normalizujące: zawierają wyrażenia , które nie mają postaci normalnych , podobnie jak rachunek lambda bez typu ^{[ potrzebne źródło ]} . Głównym otwartym problemem w tej dziedzinie jest to, czy zawsze tak jest, tj. czy (słabo) normalizujący PTS zawsze ma silną właściwość normalizacyjną. Jest to znane jako hipoteza Barendregta – Geuversa – Klopa (nazwana na cześć Henka Barendregta , Hermana Geuversa i Jana Willema Klopa ).

Definicja

System czystych typów jest zdefiniowany przez potrójną, gdzie ${\ Textstyle ({\ mathcal {S}}, {\ mathcal {A}}, {\ mathcal {R}}$ $)$ $zbiorem$ jest zbiorem sortów, aksjomatów, ${\ Textstyle {\ mathcal {R}} \ subseteq {\ mathcal {S}} ^ {3}}$ to zbiór zasad. Pisanie w systemach czystych typów jest określone przez następujące zasady, gdzie jest to dowolny rodzaj: ${\textstyle s}$

${\ Displaystyle {\ Frac {(s_ {1}, s_ {2}) \ in {\ mathcal {A}}} {\ vdash s_ {1}:s_{2}}}\quad {\text{(aksjomat)}}}$

${\ Displaystyle {\ Frac {\ Gamma \ vdash A: s \ quad x \ notin {\ tekst {dom}} ( \Gamma )}{\Gamma ,x:A\vdash x:A}}\quad {\text{(start)}}}$

${\ Displaystyle {\ Frac {\ Gamma \ vdash A: B \ quad \ Gamma \ vdash C: s\quad x\notin {\text{dom}}(\Gamma )}{\Gamma ,x:C\vdash A:B}}\quad {\text{(osłabienie)}}}$

${\ Displaystyle {\ Frac {\ Gamma \ vdash A: s_ {1} \ quad \ Gamma, x: A \ vdash B: s_ {2} \ quad (s_ {1}, s_ {2}, s_ {3} )\in {\mathcal {R}}}{\Gamma \vdash \Pi x:AB:s_{3}}}\quad {\text{(produkt)}}}$

${\ Displaystyle {\ Frac {\ Gamma \ vdash C: \ Pi x: AB \ quad \ Gamma \ vdash a: A} \Gamma \vdash Ca:B[x:=a]}}\quad {\text{(aplikacja)}}}$

${\ Displaystyle {\ Frac {\ Gamma, x: A \ vdash b: B \ quad \ Gamma \ vdash \ Pi x: AB: s} {\ Gamma \ vdash \ lambda x: Ab: \ Pi x :AB}}\quad {\text{(abstrakcja)}}}$

${\ Displaystyle {\ Frac {\ Gamma \ vdash A: B \ quad B = _ {\ beta} B” \quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(konwersja)}}}$

Wdrożenia

Następujące języki programowania mają systemy typu czystego: ^{[ potrzebne źródło ]}

SZAŁWIA
Krwawnik
Henek 2000

Zobacz też

System U – przykład niespójnego PTS
Rachunek λμ wykorzystuje inne podejście do kontroli niż CPTS

Notatki

Berardi, Stefano (1988). Ku matematycznej analizie rachunku konstrukcji Coquanda – Hueta i innych układów w kostce Barendregta (raport techniczny). Wydział Informatyki, CMU i Dipartimento Matematica, Universita di Torino. CMU-CS-88-131.
Terlouw, J. (1989). „Een nadere bewijstheoretische analiz van GSTT” (w języku niderlandzkim). Holandia: Uniwersytet w Nijmegen. {{ cite Journal }} : Cite Journal wymaga |journal= ( pomoc )

Dalsza lektura

Schmidt, David A. (1994). „§ 8.3 Uogólnione systemy typów” . Struktura typowych języków programowania . MIT Press. s. 255–8. ISBN 0-262-19349-3 .

Linki zewnętrzne

System czystego typu w n Lab
Jones, Roger Bishop (1999). „Przegląd systemów Pure Type” .