System av ren typ
Bevisa eller motbevisa Barendregt–Geuvers–Klop gissningen.
Inom de grenar av matematisk logik som kallas bevisteori och typteori är ett rent typsystem ( PTS ), tidigare känt som ett generaliserat typsystem ( GTS ), en form av maskinskriven lambdakalkyl som tillåter ett godtyckligt antal sorter och beroenden mellan någon av dessa. Ramverket kan ses som en generalisering av Barendregts lambdakub , i den meningen att alla hörn av kuben kan representeras som instanser av en PTS med bara två sorters . Faktum är att Barendregt (1991) ramade in sin kub i denna miljö. Rentypsystem kan skymma distinktionen mellan typer och termer och kollapsa typhierarkin , som är fallet med konstruktionskalkylen, men detta är inte generellt fallet, t.ex. tillåter den enkelt skrivna lambdakalkylen endast termer att bero på termer.
System av ren typ introducerades oberoende av Stefano Berardi (1988) och Jan Terlouw (1989). Barendregt diskuterade dem utförligt i sina efterföljande tidningar. I sin doktorsavhandling definierade Berardi en kub av konstruktiv logik som liknar lambdakuben (dessa specifikationer är icke-beroende). En modifiering av denna kub kallades senare L-kuben av Geuvers, som i sin doktorsavhandling utökade Curry-Howard-korrespondensen till denna miljö. Baserat på dessa idéer definierade Barthe och andra klassiska system av ren typ ( CPTS ) genom att lägga till en dubbel negationsoperator . På samma sätt introducerade Tijn Borghuis 1998 modala ren typsystem ( MPTS ). Roorda har diskuterat tillämpningen av system av ren typ för funktionell programmering ; och Roorda och Jeuring har föreslagit ett programmeringsspråk baserat på rena typsystem.
Systemen från lambdakuben är alla kända för att vara starkt normaliserande . System av ren typ behöver inte vara det, till exempel är det inte System U från Girards paradox . ( Girard hittade grovt sett rena system där man kan uttrycka meningen "typerna bildar en typ".) Dessutom är alla kända exempel på rena typsystem som inte är starkt normaliserande inte ens (svagt) normaliserande : de innehåller uttryck som har inte normala former , precis som den otypade lambdakalkylen [ citat behövs ] . Det är ett stort öppet problem på området om så alltid är fallet, dvs om en (svagt) normaliserande PTS alltid har den starka normaliseringsegenskapen. Detta är känt som Barendregt-Geuvers-Klop-förmodan (uppkallad efter Henk Barendregt , Herman Geuvers och Jan Willem Klop ).
Definition
Ett system av ren typ definieras av en trippel där är mängden sorter, är mängden axiom, och är uppsättningen regler. Att skriva i rena typsystem bestäms av följande regler, där är vilken sort som helst:
Genomföranden
Följande programmeringsspråk har system av ren typ: [ citat behövs ]
- SALVIA
- Rölleka
- Henk 2000
Se även
- System U – ett exempel på en inkonsekvent PTS
- λμ-kalkyl använder en annan metod för kontroll än CPTS
Anteckningar
- Berardi, Stefano (1988). Mot en matematisk analys av Coquand–Huet-kalkylen för konstruktioner och de andra systemen i Barendregts kub ( Teknisk rapport). Institutionen för datavetenskap, CMU och Dipartimento Matematica, Universita di Torino. CMU-CS-88-131.
-
Terlouw, J. (1989). "Een nadere bewijstheoretische analys av GSTTs" (på holländska). Nederländerna: Universitetet i Nijmegen.
{{ citera journal }}
: Citera journal kräver|journal=
( hjälp )
Vidare läsning
- Schmidt, David A. (1994). "§ 8.3 Generaliserade typsystem" . Strukturen för maskinskrivna programmeringsspråk . MIT Press. s. 255–8. ISBN 0-262-19349-3 .
externa länkar
- Rent typsystem på n Lab
- Jones, Roger Bishop (1999). "Översikt över Pure Type Systems" .