Teoria tipului intuiționist

Teoria tipului intuiționist (cunoscută și sub numele de teoria tipului constructiv sau teoria tipului Martin-Löf ) este o teorie a tipurilor și o bază a matematicii alternative. A fost creat de Per Martin-Löf , un matematician și filosof suedez , care a publicat-o pentru prima dată în 1972. Există mai multe versiuni ale teoriei: Martin-Löf a propus variante intensionale , extensionale și inițial imprevizibile , dintre care paradoxul lui Girard a arătat inconsecvența, lăsând loc versiunilor predicative . Cu toate acestea, toate versiunile păstrează designul central al logicii constructive, utilizând tipuri dependente.

Proiecta

Martin-Löf a conceput teoria tipurilor bazată pe principiile constructivismului matematic . Constructivismul necesită orice demonstrație a existenței pentru a expune un „martor”. De exemplu, orice dovadă că există un număr prim mai mare de 1000 trebuie să identifice un număr specific care este atât prim cât și mai mare de 1000. Teoria tipului intuiționist a atins acest obiectiv prin interiorizarea interpretării BHK . O consecință interesantă este că dovezile devin obiecte matematice care pot fi examinate, comparate și manipulate.

Constructorii de tip au fost structurați pentru a urma o corespondență unu-la-unu cu conectivități logice. De exemplu, implicația logică ( $A\implies B$ ${\ displaystyle A \ implică B}$ ${\ displaystyle A \ implică B}$ ) corespunde tipului de funcție ( $A\mapsto B$ ${\ displaystyle A \ mapsto B}$ ${\ displaystyle A \ mapsto B}$ ). Această corespondență se numește izomorfism Curry-Howard . Teoriile tipurilor anterioare au urmat și acest izomorfism, dar cele ale lui Martin-Löf au fost primii care l-au extins la logica predicativă , introducând tipuri dependente .

Teoria tipurilor

Teoria tipului intuiționist are 3 tipuri finite, care sunt compuse folosind 5 constructori diferiți. Spre deosebire de teoriile de seturi, teoriile tipurilor nu sunt construite pe logica de prim ordin. Astfel, fiecare aspect al teoriei tipurilor are o interpretare dublă: atât ca obiect matematic, cât și ca componentă logică.

Dacă nu sunteți familiarizați cu teoria tipurilor și sunteți familiarizați cu teoria mulțimilor, un rezumat rapid este: Tipurile conțin termeni la fel cum mulțimile conțin elemente. Termenii aparțin unui singur tip. Termeni precum $2+2$ ${\ displaystyle 2 + 2}$ ${\ displaystyle 2 + 2}$ Și $2\cdot 2$ ${\ displaystyle 2 \ cdot 2}$ ${\ displaystyle 2 \ cdot 2}$ ei calculează („se rezumă la”) termeni canonici precum 4. Pentru mai multe detalii, consultați articolul despre teoria tipurilor.

Tipul 0, tipul 1 și tipul 2

Există trei tipuri finite: tipul 0 conține 0 termeni, tipul 1 conține un termen canonic, iar tipul 2 conține 2 termeni canonici.

Deoarece tipul 0 conține 0 termeni, se mai numește și tip gol . Este folosit pentru a reprezenta tot ce nu poate exista. De asemenea, este scris $\bot$ ${\ displaystyle \ bot}$ $\ bot$ și reprezintă propoziții refutabile (adică pentru care nu poate exista nicio dovadă). În consecință, negația este definită ca o funcție în $\bot$ ${\ displaystyle \ bot}$ $\ bot$ : $\neg A\ {\overset {\underset {\mathrm {def} }{}}{=}}\ A\mapsto \bot$ ${\ displaystyle \ neg A \ {\ overset {\ underset {\ mathrm {def}} {}} {=}} \ A \ mapsto \ bot}$ ${\ displaystyle \ neg A \ {\ overset {\ underset {\ mathrm {def}} {}} {=}} \ A \ mapsto \ bot}$ .

În mod similar, tipul 1 conține 1 termen canonic și reprezintă existența. Se mai numește și tip de unitate . Reprezintă adesea propoziții care pot fi dovedite, prin urmare, uneori este scris $\top$ ${\ displaystyle \ top}$ $\top$ .

În cele din urmă, tipul 2 conține 2 termeni canonici. Reprezintă o alegere clară între două valori. Este folosit pentru valorile booleene , dar nu și pentru propoziții. Propunerile sunt considerate a fi de tip 1 și pot fi refutabile (tip 0 ) sau nu pot fi demonstrabile sau refutabile ( legea terțului exclus nu este valabilă în teoria tipului intuiționist).

Constructor Σ

Tipurile contain conțin perechi ordonate. Ca și în cazul seturilor tipice de perechi ordonate, un tip describes descrie produsul cartezian ( $A\times B$ ${\ displaystyle A \ times B}$ $A \ ori B$ ) de alte două tipuri, $LA$ ${\ displaystyle A}$ $LA$ Și $B.$ ${\ displaystyle B}$ $B.$ . În mod logic, o astfel de pereche îngrijită ar avea o dovadă $LA$ ${\ displaystyle A}$ $LA$ și o dovadă a $B.$ ${\ displaystyle B}$ $B.$ , astfel încât să puteți vedea un tip written scris ca $A\wedge B$ ${\ displaystyle A \ wedge B}$ $A \ wedge B$ .

Tipurile Σ sunt mai puternice decât seturile tipice de perechi ordonate, datorită tastării dependente . În perechea ordonată, tipul celui de-al doilea termen poate depinde de valoarea primului termen. De exemplu, primul termen al perechii ar putea fi un număr natural, iar tipul celui de-al doilea termen ar putea fi un vector de lungime egal cu primul termen. Un astfel de tip ar fi scris astfel:

\sum _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)

{\ displaystyle \ sum _ {n {\ mathbin {:}} {\ mathbb {N}}} \ operatorname {Vec} ({\ mathbb {R}}, n)}

{\ displaystyle \ sum _ {n {\ mathbin {:}} {\ mathbb {N}}} \ operatorname {Vec} ({\ mathbb {R}}, n)}

Folosind terminologia teoriei mulțimilor, aceasta este similară cu uniunile disjuncte indexate ale mulțimilor. În cazul perechilor ordonate normale, tipul celui de-al doilea termen nu depinde de valoarea primului termen. Prin urmare, setul care descrie produsul cartezian ${\mathbb {N} }\times {\mathbb {R} }$ ${\ displaystyle {\ mathbb {N}} \ times {\ mathbb {R}}}$ ${\ displaystyle {\ mathbb {N}} \ times {\ mathbb {R}}}$ este scris ca:

\sum _{n{\mathbin {:}}{\mathbb {N} }}{\mathbb {R} }

{\ displaystyle \ sum _ {n {\ mathbin {:}} {\ mathbb {N}}} {\ mathbb {R}}}

{\ displaystyle \ sum _ {n {\ mathbin {:}} {\ mathbb {N}}} {\ mathbb {R}}}

Este important să rețineți că valoarea primului termen, $n$ ${\ displaystyle n}$ $n$ , nu depinde de tipul celui de-al doilea termen, ${\mathbb {R} }$ ${\ displaystyle {\ mathbb {R}}}$ ${{\ mathbb R}}$ .

Evident, tipurile Σ pot fi folosite pentru a construi tupluri mai mult timp în funcție de tipare, utilizate în matematică și înregistrări sau structuri , utilizate în majoritatea limbajelor de programare. Un exemplu de triplu tipat în mod dependent este compus din două numere întregi și o dovadă că primul este mai mic decât al doilea, descris de tipul:

\sum _{m{\mathbin {:}}{\mathbb {I} }}{\sum _{n{\mathbin {:}}{\mathbb {I} }}((m<n)={\text{True}})}

{\ displaystyle \ sum _ {m {\ mathbin {:}} {\ mathbb {I}}} {\ sum _ {n {\ mathbin {:}} {\ mathbb {I}}} ((m <n) = {\ text {True}})}}

{\ displaystyle \ sum _ {m {\ mathbin {:}} {\ mathbb {I}}} {\ sum _ {n {\ mathbin {:}} {\ mathbb {I}}} ((m <n) = {\ text {True}})}}

Tastarea dependentă permite tipurilor Σ să joace rolul de cuantificator existențial . Afirmația „există o $n$ ${\ displaystyle n}$ $n$ de tip $\mathbb {N}$ ${\ displaystyle \ mathbb {N}}$ $\ N$ , astfel încât $P(n)$ ${\ displaystyle P (n)}$ $P (n)$ este dovedit "devine genul de perechi ordonate în care primul termen este valoarea $n$ ${\ displaystyle n}$ $n$ iar al doilea este o demonstrație a $P(n)$ ${\ displaystyle P (n)}$ $P (n)$ . Rețineți că tipul celui de al doilea termen (dovezi ale $P(n)$ ${\ displaystyle P (n)}$ $P (n)$ ) depinde de valoarea primului element ( $n$ ${\ displaystyle n}$ $n$ ). Tipul său este:

\sum _{n{\mathbin {:}}{\mathbb {N} }}P(n)

{\ displaystyle \ sum _ {n {\ mathbin {:}} {\ mathbb {N}}} P (n)}

{\ displaystyle \ sum _ {n {\ mathbin {:}} {\ mathbb {N}}} P (n)}

Constructor Π

Tipurile Π reprezintă funcții. Ca și în cazul funcțiilor normale, acestea constau dintr-un tip de intrare și un tip de ieșire. Cu toate acestea, acestea sunt mai puternice decât funcțiile normale, deoarece tipul valorilor returnate poate depinde de valoarea de intrare. Funcțiile teoriei tipurilor sunt diferite de cele ale teoriei mulțimilor. În teoria seturilor, căutați valoarea argumentului într-un set de perechi ordonate. În teoria tipurilor, argumentul este plasat într-un termen și apoi se aplică calculul („reducere”) termenului.

De exemplu, un tip de funcție care, dat fiind un număr natural $n$ ${\ displaystyle n}$ $n$ , returnează un vector care conține $n$ ${\ displaystyle n}$ $n$ numere reale, este scris ca:

\prod _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)

{\ displaystyle \ prod _ {n {\ mathbin {:}} {\ mathbb {N}}} \ operatorname {Vec} ({\ mathbb {R}}, n)}

{\ displaystyle \ prod _ {n {\ mathbin {:}} {\ mathbb {N}}} \ operatorname {Vec} ({\ mathbb {R}}, n)}

Când tipul de ieșire nu depinde de valoarea de intrare, funcția este adesea scrisă pur și simplu cu a $\mapsto$ ${\ displaystyle \ mapsto}$ $\ mapsto$ . Asa, $\mathbb {N} \mapsto \mathbb {R}$ ${\ displaystyle \ mathbb {N} \ mapsto \ mathbb {R}}$ ${\ displaystyle \ mathbb {N} \ mapsto \ mathbb {R}}$ este genul de funcții de la numere naturale la numere reale. Tipurile Π corespund implicației logice. Propunerea $A\implies B$ ${\ displaystyle A \ implică B}$ ${\ displaystyle A \ implică B}$ se potrivește cu tipul $A\mapsto B$ ${\ displaystyle A \ mapsto B}$ ${\ displaystyle A \ mapsto B}$ , conținând funcții care acceptă dovezi ale lui A și returnează dovezi ale lui B. Acest tip ar putea fi scris mai consecvent ca:

\prod _{a{\mathbin {:}}A}B

{\ displaystyle \ prod _ {a {\ mathbin {:}} A} B}

{\ displaystyle \ prod _ {a {\ mathbin {:}} A} B}

Tipurile Π sunt, de asemenea, utilizate în logică pentru cuantificarea universală . Afirmația „pentru fiecare $n$ ${\ displaystyle n}$ $n$ de tip ${\mathbb {N} }$ ${\ displaystyle {\ mathbb {N}}}$ ${\ displaystyle {\ mathbb {N}}}$ , $P(n)$ ${\ displaystyle P (n)}$ $P (n)$ este dovedit "devine o funcție din $n$ ${\ displaystyle n}$ $n$ la demonstrațiile de $P(n)$ ${\ displaystyle P (n)}$ $P (n)$ . Prin urmare, i sa dat o valoare pentru $n$ ${\ displaystyle n}$ $n$ , funcția generează o dovadă că $P(n)$ ${\ displaystyle P (n)}$ $P (n)$ deține această valoare. Tipul este scris ca:

\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)

{\ displaystyle \ prod _ {n {\ mathbin {:}} {\ mathbb {N}}} P (n)}

{\ displaystyle \ prod _ {n {\ mathbin {:}} {\ mathbb {N}}} P (n)}

Producător =

= -Tipurile sunt create cu doi termeni. Având în vedere doi termeni precum $2+2$ ${\ displaystyle 2 + 2}$ ${\ displaystyle 2 + 2}$ Și $2\cdot 2$ ${\ displaystyle 2 \ cdot 2}$ ${\ displaystyle 2 \ cdot 2}$ , se poate crea un nou tip $2+2=2\cdot 2$ ${\ displaystyle 2 + 2 = 2 \ cdot 2}$ ${\ displaystyle 2 + 2 = 2 \ cdot 2}$ . Termenii noului tip arată că cuplul este redus la același termen canonic. Deci, din moment ce ambele $2+2$ ${\ displaystyle 2 + 2}$ ${\ displaystyle 2 + 2}$ Și $2\cdot 2$ ${\ displaystyle 2 \ cdot 2}$ ${\ displaystyle 2 \ cdot 2}$ sunt reduse la termenul canonic $4$ ${\ displaystyle 4}$ $4$ , va exista un astfel de termen $2+2=2\cdot 2$ ${\ displaystyle 2 + 2 = 2 \ cdot 2}$ ${\ displaystyle 2 + 2 = 2 \ cdot 2}$ . În teoria tipului intuiționist, există o singură modalitate de a crea termeni de = -tip, și anume prin reflexivitate :

\operatorname {refl} {\mathbin {:}}\prod _{a{\mathbin {:}}A}(a=a).

{\ displaystyle \ operatorname {refl} {\ mathbin {:}} \ prod _ {a {\ mathbin {:}} A} (a = a).}

{\ displaystyle \ operatorname {refl} {\ mathbin {:}} \ prod _ {a {\ mathbin {:}} A} (a = a).}

Puteți crea = -tipuri cum ar fi $1=2$ ${\ displaystyle 1 = 2}$ ${\ displaystyle 1 = 2}$ , în care termenii nu sunt reduși la același termen canonic, dar nu va fi posibil să se creeze termeni de acel tip. De fapt, dacă ai putea crea un termen ca $1=2$ ${\ displaystyle 1 = 2}$ ${\ displaystyle 1 = 2}$ , ai putea crea și un termen ca $\bot$ ${\ displaystyle \ bot}$ $\ bot$ care, dacă ar fi inserat într-o funcție, ar genera o funcție de tip $1=2\mapsto \bot$ ${\ displaystyle 1 = 2 \ mapsto \ bot}$ ${\ displaystyle 1 = 2 \ mapsto \ bot}$ . De cand $\ldots \mapsto \bot$ ${\ displaystyle \ ldots \ mapsto \ bot}$ ${\ displaystyle \ ldots \ mapsto \ bot}$ așa este definită negația, avem asta $\neg (1=2)$ ${\ displaystyle \ neg (1 = 2)}$ ${\ displaystyle \ neg (1 = 2)}$ , adică $1\neq 2$ ${\ displaystyle 1 \ neq 2}$ ${\ displaystyle 1 \ neq 2}$ .

Echivalența probelor este un domeniu activ de cercetare în teoria dovezilor și a condus la dezvoltarea teoriei tipului homotopic și a altor teorii de tip.

Tipuri inductive

Tipurile inductive permit crearea unor tipuri complexe, de auto-referință. De exemplu, o listă legată de numere naturale este o listă goală sau o pereche constând dintr-un număr natural și o altă listă legată. Tipurile inductive pot fi utilizate pentru a defini structuri matematice nelimitate, cum ar fi copaci, grafice etc. Într-adevăr, tipul numerelor naturale poate fi definit inductiv, fiind fiecare număr natural sau succesorul unui alt număr natural.

Tipurile inductive definesc noi constante, precum zero $0:\mathbb {N}$ ${\ displaystyle 0: \ mathbb {N}}$ ${\ displaystyle 0: \ mathbb {N}}$ și funcția succesorală $S:\mathbb {N} \mapsto \mathbb {N}$ ${\ displaystyle S: \ mathbb {N} \ mapsto \ mathbb {N}}$ ${\ displaystyle S: \ mathbb {N} \ mapsto \ mathbb {N}}$ . De cand $S.$ ${\ displaystyle S}$ $S.$ nu are definiție și nu poate fi evaluat folosind înlocuire, termeni precum $S(0)$ ${\ displaystyle S (0)}$ ${\ displaystyle S (0)}$ Și $S(S(S(0)))$ ${\ displaystyle S (S (S (0)))}$ ${\ displaystyle S (S (S (0)))}$ devin termenii canonici pentru numerele naturale.

Dovezile tipurilor inductive sunt posibile prin inducție . Fiecare tip inductiv are propria sa regulă inductivă. Pentru a dovedi un predicat $P(n)$ ${\ displaystyle P (n)}$ $P (n)$ pentru orice număr natural $n$ ${\ displaystyle n}$ $n$ , se utilizează următoarea regulă:

\mathbb {N} {\text{-elim}}:P(0)\mapsto \left(\prod _{n:\mathbb {N} }P(n)\mapsto P(S(n))\right)\mapsto \prod _{n:\mathbb {N} }P(n)

{\ displaystyle \ mathbb {N} {\ text {-elim}}: P (0) \ mapsto \ left (\ prod _ {n: \ mathbb {N}} P (n) \ mapsto P (S (n) ) \ right) \ mapsto \ prod _ {n: \ mathbb {N}} P (n)}

{\ displaystyle \ mathbb {N} {\ text {-elim}}: P (0) \ mapsto \ left (\ prod _ {n: \ mathbb {N}} P (n) \ mapsto P (S (n) ) \ right) \ mapsto \ prod _ {n: \ mathbb {N}} P (n)}

Tipurile inductive sunt definite în termeni de tipuri W, adică copacii bine întemeiați . Lucrările ulterioare în teoria tipurilor au generat tipuri coinductive, de inducție-recursivitate și de inducție-inducție pentru a lucra pe tipuri de auto-referențial de natură mai obscură. Tipurile inductive de ordin superior vă permit să definiți egalitatea între termeni.

Tipuri de universuri

Tipurile de universuri vă permit să construiți dovezi de toate tipurile create cu alți constructori de tip. Orice termen din tipul universului ${\mathcal {U}}_{0}$ ${\ displaystyle {\ mathcal {U}} _ {0}}$ ${\ displaystyle {\ mathcal {U}} _ {0}}$ poate fi mapat la un tip creat cu orice combinație de $0,1,2,\Sigma ,\Pi ,=$ ${\ displaystyle 0,1,2, \ Sigma, \ Pi, =}$ ${\ displaystyle 0,1,2, \ Sigma, \ Pi, =}$ iar constructorul inductiv. Cu toate acestea, pentru a evita paradoxurile, nu există un termen în ${\mathcal {U}}_{0}$ ${\ displaystyle {\ mathcal {U}} _ {0}}$ ${\ displaystyle {\ mathcal {U}} _ {0}}$ ce hartă în ${\mathcal {U}}_{0}$ ${\ displaystyle {\ mathcal {U}} _ {0}}$ ${\ displaystyle {\ mathcal {U}} _ {0}}$ .

Pentru a construi dovezi despre toți „băieții mici” e ${\mathcal {U}}_{0}$ ${\ displaystyle {\ mathcal {U}} _ {0}}$ ${\ displaystyle {\ mathcal {U}} _ {0}}$ , trebuie să utilizați ${\mathcal {U}}_{1}$ ${\ displaystyle {\ mathcal {U}} _ {1}}$ ${\ displaystyle {\ mathcal {U}} _ {1}}$ , care conține un termen pentru ${\mathcal {U}}_{0}$ ${\ displaystyle {\ mathcal {U}} _ {0}}$ ${\ displaystyle {\ mathcal {U}} _ {0}}$ , dar nu pentru el însuși. În mod similar, pentru ${\mathcal {U}}_{2}$ ${\ displaystyle {\ mathcal {U}} _ {2}}$ ${\ displaystyle {\ mathcal {U}} _ {2}}$ . Există o ierarhie predicativă pe universuri, deci pentru a cuantifica o dovadă pe o constantă $k$ ${\ displaystyle k}$ $k$ fixat pe universuri, trebuie să îl folosești ${\mathcal {U}}_{k+1}$ ${\ displaystyle {\ mathcal {U}} _ {k + 1}}$ ${\ displaystyle {\ mathcal {U}} _ {k + 1}}$ .

Tipurile de universuri sunt un aspect complicat al teoriilor tipurilor. Într-adevăr, a fost necesar să se modifice prima versiune a teoriei pentru a ține cont de paradoxul lui Girard . Cercetările ulterioare au atins subiecte precum „superuniversurile”, „universurile Mahlo” și universurile impredative.

Judecăți

Definiția formală a teoriei tipului intuiționist este scrisă folosind judecăți. De exemplu, în enunțul „dacă $LA$ ${\ displaystyle A}$ $LA$ este un tip și $B.$ ${\ displaystyle B}$ $B.$ este un tip, atunci $\textstyle \sum _{a:A}B$ ${\ displaystyle \ textstyle \ sum _ {a: A} B}$ ${\ displaystyle \ textstyle \ sum _ {a: A} B}$ este un tip "există judecăți" este un tip "," și "și" dacă ... atunci ... "Expresia $\textstyle \sum _{a:A}B$ ${\ displaystyle \ textstyle \ sum _ {a: A} B}$ ${\ displaystyle \ textstyle \ sum _ {a: A} B}$ nu este o judecată, dar este tipul care este definit.

Acest al doilea nivel al teoriei tipurilor poate fi confuz, în special în ceea ce privește egalitatea. Există o judecată cu privire la egalitatea de termeni, care ar putea fi afirmată $4=2+2$ ${\ displaystyle 4 = 2 + 2}$ ${\ displaystyle 4 = 2 + 2}$ , sau că doi termeni sunt reduși la același termen canonic. Există, de asemenea, o judecată cu privire la egalitatea tipurilor, $A=B$ ${\ displaystyle A = B}$ ${\ displaystyle A = B}$ , adică fiecare element de tip $LA$ ${\ displaystyle A}$ $LA$ este un element tip $B.$ ${\ displaystyle B}$ $B.$ si invers. La nivel de tip, există un tip $4=2+2$ ${\ displaystyle 4 = 2 + 2}$ ${\ displaystyle 4 = 2 + 2}$ , care conține termeni dacă există o dovadă că $4$ ${\ displaystyle 4}$ $4$ Și $2+2$ ${\ displaystyle 2 + 2}$ ${\ displaystyle 2 + 2}$ se reduc la aceeași valoare (desigur, termenii de acest tip sunt generați folosind judecata privind egalitatea de termeni). În cele din urmă, există un nivel meta-lingvistic de egalitate, deoarece folosim cuvântul „patru” și simbolul „ $4$ ${\ displaystyle 4}$ $4$ „pentru a se referi la termenul canonic $S(S(S(S(0))))$ ${\ displaystyle S (S (S (S (0))))}$ ${\ displaystyle S (S (S (S (0))))}$ . Sinonime precum acestea sunt numite „egale prin definiție” de Martin-Löf.

Următoarea descriere a hotărârilor se bazează pe discuțiile din Nordström, Petersson și Smith.

Teoria formală funcționează cu tipuri și obiecte .

Un tip este declarat de:

$A\ {\mathsf {Type}}$ ${\ displaystyle A \ {\ mathsf {Type}}}$ ${\ displaystyle A \ {\ mathsf {Type}}}$

Un obiect există și este de tip dacă:

$a{\mathbin {:}}A$ ${\ displaystyle a {\ mathbin {:}} A}$ ${\ displaystyle a {\ mathbin {:}} A}$

Obiectele pot fi aceleași

$a=b$ ${\ displaystyle a = b}$ $a = b$

iar tipurile pot fi aceleași

$A=B$ ${\ displaystyle A = B}$ ${\ displaystyle A = B}$

este declarat un tip care depinde de un obiect de alt tip

$(x{\mathbin {:}}A)B$ ${\ displaystyle (x {\ mathbin {:}} A) B}$ ${\ displaystyle (x {\ mathbin {:}} A) B}$

și îndepărtat pentru înlocuire

$B[x/a]$ ${\ displaystyle B [x / a]}$ ${\ displaystyle B [x / a]}$ , înlocuind variabila $X$ ${\ displaystyle x}$ $X$ cu obiectul $la$ ${\ displaystyle a}$ $la$ în $B.$ ${\ displaystyle B}$ $B.$ .

Un obiect care depinde de un obiect de alt tip poate fi scris în două moduri. Dacă obiectul este „abstract”, atunci este scris

$[x]b$ ${\ displaystyle [x] b}$ ${\ displaystyle [x] b}$

și îndepărtat pentru înlocuire

$b[x/a]$ ${\ displaystyle b [x / a]}$ ${\ displaystyle b [x / a]}$ , înlocuind variabila $X$ ${\ displaystyle x}$ $X$ cu obiectul $la$ ${\ displaystyle a}$ $la$ în $b$ ${\ displaystyle b}$ $b$ .

Un obiect dependent de un obiect poate fi, de asemenea, declarat ca o parte constantă a unui tip recursiv. Un exemplu de tip recursiv este:

$0{\mathbin {:}}\mathbb {N}$ ${\ displaystyle 0 {\ mathbin {:}} \ mathbb {N}}$ ${\ displaystyle 0 {\ mathbin {:}} \ mathbb {N}}$
$S{\mathbin {:}}\mathbb {N} \to \mathbb {N}$ ${\ displaystyle S {\ mathbin {:}} \ mathbb {N} \ to \ mathbb {N}}$ ${\ displaystyle S {\ mathbin {:}} \ mathbb {N} \ to \ mathbb {N}}$

Aici, $S.$ ${\ displaystyle S}$ $S.$ este un obiect dependent de un obiect constant. Nu este asociat cu o abstractizare. Constante le place $S.$ ${\ displaystyle S}$ $S.$ ele pot fi eliminate prin definirea egalităților. Aici, relația cu adunarea este definită folosind egalitatea și potrivirea modelelor pentru a gestiona natura recursivă a $S.$ ${\ displaystyle S}$ $S.$ :

{\begin{aligned}\operatorname {add} &{\mathbin {:}}\ (\mathbb {N} \times \mathbb {N} )\to \mathbb {N} \\\operatorname {add} (0,b)&=b\\\operatorname {add} (S(a),b)&=S(\operatorname {add} (a,b)))\end{aligned}}

{\ displaystyle {\ begin {align} \ operatorname {add} și {\ mathbin {:}} \ (\ mathbb {N} \ times \ mathbb {N}) \ to \ mathbb {N} \\\ operatorname {add } (0, b) & = b \\\ operatorname {add} (S (a), b) & = S (\ operatorname {add} (a, b))) \ end {align}}}

{\ displaystyle {\ begin {align} \ operatorname {add} și {\ mathbin {:}} \ (\ mathbb {N} \ times \ mathbb {N}) \ to \ mathbb {N} \\\ operatorname {add } (0, b) & = b \\\ operatorname {add} (S (a), b) & = S (\ operatorname {add} (a, b))) \ end {align}}}

$S.$ ${\ displaystyle S}$ $S.$ este manipulat ca o constantă opacă, nu are o structură internă de substituție.

Prin urmare, obiecte, tipuri și relații sunt utilizate pentru a exprima formulele teoriei. Următoarele stiluri de judecată sunt utilizate pentru a crea noi obiecte, tipuri și relații dintre cele existente:

$\Gamma \vdash \sigma \ {\mathsf {Tipo}}$ ${\ displaystyle \ Gamma \ vdash \ sigma \ {\ mathsf {Type}}}$ ${\ displaystyle \ Gamma \ vdash \ sigma \ {\ mathsf {Type}}}$	σ este un tip bine format în contextul Γ.
$\Gamma \vdash t{\mathbin {:}}\sigma$ ${\ displaystyle \ Gamma \ vdash t {\ mathbin {:}} \ sigma}$ ${\ displaystyle \ Gamma \ vdash t {\ mathbin {:}} \ sigma}$	t este un termen bine format de tip σ în contextul Γ.
$\Gamma \vdash \sigma \equiv \tau$ ${\ displaystyle \ Gamma \ vdash \ sigma \ equiv \ tau}$ ${\ displaystyle \ Gamma \ vdash \ sigma \ equiv \ tau}$	σ și τ sunt tipuri egale în contextul Γ.
$\Gamma \vdash t\equiv u{\mathbin {:}}\sigma$ ${\ displaystyle \ Gamma \ vdash t \ equiv u {\ mathbin {:}} \ sigma}$ ${\ displaystyle \ Gamma \ vdash t \ equiv u {\ mathbin {:}} \ sigma}$	„ t și u” sunt termeni egali de tip σ în contextul Γ.
$\vdash \Gamma \ {\mathsf {Contesto}}$ ${\ displaystyle \ vdash \ Gamma \ {\ mathsf {Context}}}$ ${\ displaystyle \ vdash \ Gamma \ {\ mathsf {Context}}}$	Γ este un context bine format al ipotezelor de tastare.

Prin convenție, există un tip care reprezintă toate celelalte tipuri. Se numește ${\mathcal {U}}$ ${\ displaystyle {\ mathcal {U}}}$ ${\ mathcal {U}}$ (sau $\operatorname {Set}$ ${\ displaystyle \ operatorname {Set}}$ ${\ displaystyle \ operatorname {Set}}$ ). De cand ${\mathcal {U}}$ ${\ displaystyle {\ mathcal {U}}}$ ${\ mathcal {U}}$ este un tip, membrii săi sunt obiecte. Există un tip de dependent $\operatorname {El}$ ${\ displaystyle \ operatorname {El}}$ ${\ displaystyle \ operatorname {El}}$ care leagă fiecare obiect de tipul corespunzător. În majoritatea textelor $\operatorname {El}$ ${\ displaystyle \ operatorname {El}}$ ${\ displaystyle \ operatorname {El}}$ nu se scrie niciodată. Din context, un cititor poate distinge aproape întotdeauna dacă $LA$ ${\ displaystyle A}$ $LA$ se referă la un tip sau dacă se referă la obiectul din ${\mathcal {U}}$ ${\ displaystyle {\ mathcal {U}}}$ ${\ mathcal {U}}$ care se potrivește cu tipul.

Aceasta este baza completă a teoriei. Orice altceva este derivat.

Pentru a implementa logica, fiecare propunere are propriul tip. Obiectele din aceste tipuri reprezintă diferite modalități posibile de a demonstra propoziția. Evident, dacă nu există dovezi pentru propoziție, atunci tipul nu conține obiecte. Operatori precum „și” și „sau”, care lucrează la propuneri, introduc noi tipuri și obiecte noi. Asa, $A\times B$ ${\ displaystyle A \ times B}$ ${\ displaystyle A \ times B}$ este un tip care depinde de tip $LA$ ${\ displaystyle A}$ $LA$ și tastați $B.$ ${\ displaystyle B}$ $B.$ . Obiectele de acel tip dependent sunt definite pentru a exista pentru fiecare pereche de obiecte ale $LA$ ${\ displaystyle A}$ $LA$ și de $B.$ ${\ displaystyle B}$ $B.$ . Evident, dacă $LA$ ${\ displaystyle A}$ $LA$ sau $B.$ ${\ displaystyle B}$ $B.$ sunt tipuri goale, apoi noul tip pe care îl reprezintă $A\times B$ ${\ displaystyle A \ times B}$ ${\ displaystyle A \ times B}$ este de asemenea gol.

Acest lucru se poate face pentru alte tipuri (booleeni, numere naturale etc.) și operatorii lor.

Modele categorice ale teoriei tipurilor

Folosind limbajul teoriei categoriilor , RAG Seely a introdus noțiunea de categorie locală carteziană închisă (CLCC) ca model de bază al teoriei tipurilor. Acest lucru a fost rafinat de Hofmann și Dybjer în Categorii cu familii sau Categorii cu atribute pe baza lucrărilor anterioare ale lui Cartmell. ^[1]

O categorie cu familii este o categorie C de contexte (unde obiectele sunt contexte și morfismele de context sunt substituții), împreună cu un functor $la$ ${\ displaystyle a}$ $la$ .

${\text{Fam(Set)}}$ ${\ displaystyle {\ text {Fam (Set)}}}$ ${\ displaystyle {\ text {Fam (Set)}}}$ este categoria familiilor de seturi , unde obiectele sunt perechi $(A,B)$ ${\ displaystyle (A, B)}$ ${\ displaystyle (A, B)}$ format dintr-un „set de indici” $LA$ ${\ displaystyle A}$ $LA$ și o funcție $B:X\mapsto A$ ${\ displaystyle B: X \ mapsto A}$ ${\ displaystyle B: X \ mapsto A}$ , iar morfismele sunt perechi de funcții $f:A\mapsto A'$ ${\ displaystyle f: A \ mapsto A '}$ ${\ displaystyle f: A \ mapsto A '}$ Și $g:X\mapsto X'$ ${\ displaystyle g: X \ mapsto X '}$ ${\ displaystyle g: X \ mapsto X '}$ , astfel încât $B'\circ g=f\circ B$ ${\ displaystyle B '\ circ g = f \ circ B}$ ${\ displaystyle B '\ circ g = f \ circ B}$ - cu alte cuvinte, $f$ ${\ displaystyle f}$ $f$ Hartă $B_{a}$ ${\ displaystyle B_ {a}}$ ${\ displaystyle B_ {a}}$ în $B_{a}$ ${\ displaystyle B_ {a}}$ ${\ displaystyle B_ {a}}$ .

Functorul $T.$ ${\ displaystyle T}$ $T.$ atribuie unui context $G.$ ${\ displaystyle G}$ $G.$ un set de tipuri $Ty(G)$ ${\ displaystyle Ty (G)}$ ${\ displaystyle Ty (G)}$ și, pentru fiecare $A:Ty(G)$ ${\ displaystyle A: Ty (G)}$ ${\ displaystyle A: Ty (G)}$ , un set de termeni $Tm(G,A)$ ${\ displaystyle Tm (G, A)}$ ${\ displaystyle Tm (G, A)}$ . Axiomele unui functor necesită ca acestea să fie în sinergie cu substituția. Înlocuitorul este de obicei scris în formă $LA f$ ${\ displaystyle Af}$ ${\ displaystyle Af}$ sau $la f$ ${\ displaystyle af}$ ${\ displaystyle af}$ , unde este $LA$ ${\ displaystyle A}$ $LA$ este un tip în $Ty(G)$ ${\ displaystyle Ty (G)}$ ${\ displaystyle Ty (G)}$ , $la$ ${\ displaystyle a}$ $la$ este un termen în $Tm(G,A)$ ${\ displaystyle Tm (G, A)}$ ${\ displaystyle Tm (G, A)}$ Și $f$ ${\ displaystyle f}$ $f$ este un înlocuitor de la $D.$ ${\ displaystyle D}$ $D.$ la $G.$ ${\ displaystyle G}$ $G.$ . Aici $Af:Ty(D)$ ${\ displaystyle Af: Ty (D)}$ ${\ displaystyle Af: Ty (D)}$ Și $af:Tm(D,Af)$ ${\ displaystyle af: Tm (D, Af)}$ ${\ displaystyle af: Tm (D, Af)}$ .

Categoria $C.$ ${\ displaystyle C}$ $C.$ trebuie să conțină un obiect terminal (contextul gol) și un obiect final pentru o formă de produs numită înțelegere sau extensie de context, în care elementul drept este un tip în contextul elementului stâng. De sine $G.$ ${\ displaystyle G}$ $G.$ este un context și $A:Ty(G)$ ${\ displaystyle A: Ty (G)}$ ${\ displaystyle A: Ty (G)}$ , atunci ar trebui să existe un obiect final $(G,A)$ ${\ displaystyle (G, A)}$ ${\ displaystyle (G, A)}$ între contexte $D.$ ${\ displaystyle D}$ $D.$ cu mapări $p:D\mapsto G$ ${\ displaystyle p: D \ mapsto G}$ ${\ displaystyle p: D \ mapsto G}$ , $q:Tm(D,Ap)$ ${\ displaystyle q: Tm (D, Ap)}$ ${\ displaystyle q: Tm (D, Ap)}$ .

O structură logică precum cea a lui Martin-Löf ia forma unor condiții de închidere pe seturi de tipuri și termeni dependenți de context: ar trebui să existe un tip pentru fiecare set și unul numit $\operatorname {Set}$ ${\ displaystyle \ operatorname {Set}}$ ${\ displaystyle \ operatorname {Set}}$ , în plus, tipurile ar trebui închise în raport cu sumele dependente și formele de produs, etc.

O teorie precum cea a mulțimilor predicative exprimă condițiile de închidere a tipurilor de mulțimi și a elementelor lor: acestea ar trebui închise în raport cu operațiile care reflectă suma și produsul dependente și în ceea ce privește diferitele forme de definiție inductivă.

Extensional versus intensional

O distincție cheie este teoria tipului extensional versus intensional . În cea extensională, egalitatea prin definiție (adică de calcul) nu este distinctă de echivalența logică, ceea ce necesită o dovadă. În consecință, sistemul de tip este indecidabil în teoria tipului extensional, deoarece programele din teorie s-ar putea să nu se termine. De exemplu, această teorie permite acordarea unui tip combinatorului Y , un exemplu detaliat al acestuia poate fi găsit în Programare în teoria tipurilor lui Martin-Löf de Nordstöm și Petersson. ^[2] Cu toate acestea, acest lucru nu împiedică teoria tipului extensional să fie o bază pentru un instrument practic, de exemplu NuPRL se bazează pe teoria respectivă. Din punct de vedere practic, nu există nicio diferență între un program care nu se încheie și un program care durează un milion de ani până la finalizare.

În contrast, în teoria tipului intensional sistemul de tip este decisiv , dar reprezentarea conceptelor matematice standard este oarecum mai greoaie, deoarece raționamentul intensional necesită utilizarea unor seturi extensionale sau construcții similare. Există multe obiecte matematice obișnuite cu care sunt greu de lucrat sau care nu pot fi reprezentate fără ele, cum ar fi numere întregi , numere raționale și numere reale . Numerele întregi și numerele raționale pot fi reprezentate fără a utiliza seturi extensionale, dar această reprezentare nu este ușor de manevrat. Numerele reale cauchy nu pot fi reprezentate fără ele. ^[3]

Teoria tipului homotopic este preocupată de rezolvarea acestei probleme. Permite definirea tipurilor inductive de ordin superior , care nu numai definesc constructori de ordinul întâi ( valori sau puncte ), ci și constructori de ordin superior, adică egalități între elemente ( arcuri ), egalități între egalități ( homotopii ), la infinit .

Implementări

Diferite forme de teorie de tip au fost implementate ca sisteme formale care stau la baza numeroșilor asistenți de probă . În timp ce multe se bazează pe ideile lui Per Martin-Löf, altele au adăugat funcționalitate, mai multe axiome sau medii filosofice diferite. De exemplu, sistemul NuPRL se bazează pe teoria tipului de calcul ^[4], iar Coq se bazează pe calculul construcțiilor (co) inductive . Tipurile dependente caracterizează și designul limbajelor de programare precum ATS , Cayenne , Epigram , Agda ^[5] și Idris . ^[6]

Teoriile tipului Martin-Löf

Pentru Martin-Löf a construit mai multe teorii ale tipurilor care au fost publicate de mai multe ori, unele dintre ele mult mai târziu că presele cu descrierea lor au devenit accesibile specialiștilor (inclusiv Jean-Yves Girard și Giovanni Sambin). Următoarea listă încearcă să enumere toate teoriile care au fost descrise în formă tipărită și să sublinieze caracteristicile cheie care le-au distins între ele. Toate aceste teorii aveau produse dependente, sume dependente, uniuni disjuncte, tipuri finite și numere naturale. Tutte le teorie avevano le stesse regole di riduzione, che non includevano la η-riduzione, né per i prodotti né per le somme dipendenti, fatta eccezione per MLTT79, in cui viene aggiunta la η-riduzione per i prodotti dipendenti.

MLTT71 è stata la prima teoria dei tipi creata da Per Martin-Löf . È apparsa in una prestampa nel 1971. Aveva un universo, ma questo universo conteneva il proprio nome al suo interno, ovvero era una teoria dei tipi con un "tipo nel tipo", come viene chiamato oggi. Jean-Yves Girard ha dimostrato che questo sistema era incoerente e la prestampa non è mai stata pubblicata.

MLTT72 è stata presentata in una prestampa del 1972, ora pubblicata. ^[7] Questa teoria aveva un universo V e nessun tipo identità. L'universo era "predicativo", nel senso che il prodotto dipendente di una famiglia di oggetti da V su un oggetto che non era in V, come ad esempio V stesso, non si considerava essere in V. L'universo era alla Russell, cioè, si scriveva direttamente "T∈V" e "t∈T" (Martin-Löf usa il segno "∈" invece del moderno ":"), senza il costruttore aggiuntivo "El".

MLTT73 fu la prima definizione di teoria dei tipi pubblicata da Per Martin-Löf (fu presentata al Logic Colloquium 73 e pubblicata nel 1975 ^[8] ). Esistono tipi identità che egli chiama "proposizioni", ma poiché non viene introdotta alcuna reale distinzione tra proposizioni e il resto dei tipi, il significato di ciò non è chiaro. È presente ciò che in seguito acquisisce il nome di J-eliminatore, ma ancora senza un nome (vedi pp. 94–95). C'è inoltre una sequenza infinita di universi V ₀ , ..., V _n , ... . Gli universi sono predicativi, alla Russell e non cumulativi ! Infatti, il corollario 3.10 a pag. 115 dice che se A∈V _m e B∈V _n sono tali che A e B sono convertibili, allora m = n. Ciò significa, ad esempio, che sarebbe difficile formulare l'univalenza in questa teoria - ci sono tipi riducibili in ciascuno dei V _i, ma non è chiaro come dichiararli uguali, poiché non ci sono tipi identità che collegano V _i e V _j per i ≠ j.

MLTT79 fu presentata nel 1979 e pubblicata nel 1982. ^[9] In questo articolo, Martin-Löf ha introdotto i quattro tipi base di giudizi per la teoria dei tipi dipendenti, che da allora è diventata fondamentale nello studio della meta-teoria di tali sistemi. Ha anche introdotto i contesti come un concetto separato (vedi p. 161). Ci sono tipi identità con il J-eliminatore (che era già apparso in MLTT73, ma senza avere questo nome), ma anche con la regola che rende la teoria "estensionale" (p. 169). Sono presenti anche i W-tipi e una sequenza infinita di universi predicativi che sono cumulativi .

Bibliopolis C'è una discussione su una teoria dei tipi nel libro Bibliopolis del 1984 ^[10] , ma è in qualche modo non ben specificata e non sembra rappresentare un particolare insieme di scelte, quindi non vi è alcuna specifica teoria dei tipi ad essa associata.

Note

^ ( EN ) Pierre Clairambault e Peter Dybjer, The biequivalence of locally cartesian closed categories and Martin-Löf type theories , in Mathematical Structures in Computer Science , vol. 24, n. 6, 2014, DOI : 10.1017/S0960129513000881 , ISSN 0960-1295 ( WC · ACNP ) , arXiv : 1112.3456 .
^ Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in Martin-Löf's Type Theory . Oxford University Press, p. 90.
^ Altenkirch, Thorsten, Thomas Anberrée, and Nuo Li. "Definable Quotients in Type Theory."
^ SF Allen, M. Bickford e RL Constable, Innovations in computational type theory using Nuprl , in Journal of Applied Logic , vol. 4, n. 4, 2006, pp. 428–469, DOI : 10.1016/j.jal.2005.10.005 .
^ Ulf Norell, Dependently Typed Programming in Agda , in Proceedings of the 4th International Workshop on Types in Language Design and Implementation , New York, NY, USA, ACM, 2009, pp. 1–2, DOI : 10.1145/1481861.1481862 , ISBN 978-1-60558-420-1 .
^ Edwin Brady, Idris, a general-purpose dependently typed programming language: Design and implementation , in Journal of Functional Programming , vol. 23, n. 5, 2013, pp. 552–593, DOI : 10.1017/S095679681300018X , ISSN 0956-7968 ( WC · ACNP ) .
^ Per Martin-Löf, An intuitionistic theory of types, Twenty-five years of constructive type theory (Venice,1995), Oxford Logic Guides, v. 36, pp. 127--172, Oxford Univ. Press, New York, 1998
^ Per Martin-Löf, An intuitionistic theory of types: predicative part, Logic Colloquium '73 (Bristol, 1973), 73--118. Studies in Logic and the Foundations of Mathematics, Vol. 80, North-Holland, Amsterdam,1975
^ Per Martin-Löf, Constructive mathematics and computer programming, Logic, methodology and philosophy of science, VI (Hannover, 1979), Stud. Logic Found. Math., v. 104, pp. 153--175, North-Holland, Amsterdam, 1982
^ Per Martin-Löf, Intuitionistic type theory, Studies in Proof Theory. Lecture Notes, v. 1, Notes by Giovanni Sambin, pp. iv+91, 1984

Bibliografia

Per Martin-Löf, Intuitionistic type theory ( PDF ), Sambin, Giovanni, Napoli, Bibliopolis, 1984, ISBN 978-88-7088-105-9 , OCLC 12731401 .
Per Martin-Löf's Notes, as recorded by Giovanni Sambin (1980)
Bengt Nordström, Kent Petersson e Jan M. Smith, Programming in Martin-Löf's Type Theory , Oxford University Press, 1990, ISBN 978-0-19-853814-1 .
Simon Thompson, Type Theory and Functional Programming , Addison-Wesley, 1991, ISBN 0-201-41667-0 .
Johan G. Granström, Treatise on Intuitionistic Type Theory , Springer, 2011, ISBN 978-94-007-1735-0 .
Note di Per Martin-Löf, registrato da Giovanni Sambin (1980)
Bengt Nordström, Kent Petersson e Jan M. Smith, Programming in Martin-Löf's Type Theory , Oxford University Press, 1990, ISBN 978-0-19-853814-1 . Bengt Nordström, Kent Petersson e Jan M. Smith, Programming in Martin-Löf's Type Theory , Oxford University Press, 1990, ISBN 978-0-19-853814-1 . Bengt Nordström, Kent Petersson e Jan M. Smith, Programming in Martin-Löf's Type Theory , Oxford University Press, 1990, ISBN 978-0-19-853814-1 .
Simon Thompson, Type Theory and Functional Programming , Addison-Wesley, 1991, ISBN 0-201-41667-0 . Simon Thompson, Type Theory and Functional Programming , Addison-Wesley, 1991, ISBN 0-201-41667-0 . Simon Thompson, Type Theory and Functional Programming , Addison-Wesley, 1991, ISBN 0-201-41667-0 .
Johan G. Granström, Treatise on Intuitionistic Type Theory , Springer, 2011, ISBN 978-94-007-1735-0 . Johan G. Granström, Treatise on Intuitionistic Type Theory , Springer, 2011, ISBN 978-94-007-1735-0 . Johan G. Granström, Treatise on Intuitionistic Type Theory , Springer, 2011, ISBN 978-94-007-1735-0 .

Voci correlate

Collegamenti esterni

EU Types Project: Tutorials - appunti e diapositive della Types Summer School 2005
n-Categories - Sketch of a Definition - lettera di John Baez e James Dolan a Ross Street, 29 novembre 1995

Portale Filosofia

Portale Informatica

Portale Matematica

[1] ( EN ) Pierre Clairambault e Peter Dybjer, The biequivalence of locally cartesian closed categories and Martin-Löf type theories , in Mathematical Structures in Computer Science , vol. 24, n. 6, 2014, DOI : 10.1017/S0960129513000881 , ISSN 0960-1295 ( WC · ACNP ) , arXiv : 1112.3456 .

[2] Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in Martin-Löf's Type Theory . Oxford University Press, p. 90.

[3] Altenkirch, Thorsten, Thomas Anberrée, and Nuo Li. "Definable Quotients in Type Theory."

[4] SF Allen, M. Bickford e RL Constable, Innovations in computational type theory using Nuprl , in Journal of Applied Logic , vol. 4, n. 4, 2006, pp. 428–469, DOI : 10.1016/j.jal.2005.10.005 .

[5] Ulf Norell, Dependently Typed Programming in Agda , in Proceedings of the 4th International Workshop on Types in Language Design and Implementation , New York, NY, USA, ACM, 2009, pp. 1–2, DOI : 10.1145/1481861.1481862 , ISBN 978-1-60558-420-1 .

[6] Edwin Brady, Idris, a general-purpose dependently typed programming language: Design and implementation , in Journal of Functional Programming , vol. 23, n. 5, 2013, pp. 552–593, DOI : 10.1017/S095679681300018X , ISSN 0956-7968 ( WC · ACNP ) .

[7] Per Martin-Löf, An intuitionistic theory of types, Twenty-five years of constructive type theory (Venice,1995), Oxford Logic Guides, v. 36, pp. 127--172, Oxford Univ. Press, New York, 1998

[8] Per Martin-Löf, An intuitionistic theory of types: predicative part, Logic Colloquium '73 (Bristol, 1973), 73--118. Studies in Logic and the Foundations of Mathematics, Vol. 80, North-Holland, Amsterdam,1975

[9] Per Martin-Löf, Constructive mathematics and computer programming, Logic, methodology and philosophy of science, VI (Hannover, 1979), Stud. Logic Found. Math., v. 104, pp. 153--175, North-Holland, Amsterdam, 1982

[MartinLöf1984-10] Per Martin-Löf, Intuitionistic type theory, Studies in Proof Theory. Lecture Notes, v. 1, Notes by Giovanni Sambin, pp. iv+91, 1984

[1]

[2]

[3]

[4],

[5]

[6]

[7]

[8]

[9]

[10]