Sezgisel tip teorisi - Intuitionistic type theory

Sezgisel tip teorisi ( yapıcı tip teorisi veya Martin-Löf tipi teori olarak da bilinir ), bir tip teorisi ve matematiğin alternatif bir temelidir . Intuitionistic tip teorisi tarafından yaratıldı Per Martin-Löf , bir İsveçli matematikçi ve filozof tipi teorisinin birden sürümü vardır ilk 1972'de yayınladıktan: Martin-Löf hem önerdi intensional ve genişlemeli teorinin varyantlarını ve erken impredicative versiyonlarını, tarafından tutarsız olduğu gösterilmiştir Girard paradoks , yol verdi yüklem sürümleri. Ancak, tüm sürümler, bağımlı türleri kullanarak yapıcı mantığın temel tasarımını korur.

Tasarım

Martin-Löf, tip teorisini matematiksel yapılandırmacılık ilkeleri üzerine tasarladı . Konstrüktivizm, bir "tanık" içermesi için herhangi bir varoluş kanıtı gerektirir. Bu nedenle, "1000'den büyük bir asal vardır" kanıtının hem asal hem de 1000'den büyük belirli bir sayı tanımlaması gerekir. Sezgisel tip teorisi, bu tasarım hedefini BHK yorumunu içselleştirerek gerçekleştirdi . İlginç bir sonuç, ispatların incelenebilen, karşılaştırılabilen ve manipüle edilebilen matematiksel nesneler haline gelmesidir.

Sezgisel tip teorisinin tip oluşturucuları, mantıksal bağlaçlarla bire bir yazışmaları takip etmek için inşa edildi. Örneğin, implication ( ) adlı mantıksal bağlaç , bir işlevin ( ) türüne karşılık gelir . Bu yazışmaya Curry-Howard izomorfizmi denir . Önceki tip teorileri de bu eşbiçimliliği izlemişti, ancak Martin-Löf'ünki, bağımlı türleri tanıtarak onu yüklem mantığını genişleten ilk kişiydi . ${\displaystyle A\implies B}$${\displaystyle A\to B}$

Tip teorisi

Sezgisel tip teorisi, daha sonra 5 farklı tip kurucu kullanılarak oluşturulan 3 sonlu tipe sahiptir. Küme teorilerinden farklı olarak, tip teorileri Frege'ninki gibi bir mantığın üzerine inşa edilmez . Bu nedenle, tip teorisinin her özelliği, hem matematiğin hem de mantığın bir özelliği olarak çifte görev yapar.

Tip teorisine aşina değilseniz ve küme teorisini biliyorsanız, kısa bir özet şudur: Tipler, tıpkı kümelerin öğeleri içerdiği gibi terimler içerir. Terimler tek bir türe aittir. Gibi terimler ve hesaplamalar ("azaltma"), 4 gibi standart terimlere indirgenir. Daha fazla bilgi için Tür teorisi hakkındaki makaleye bakın .${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$

0 tip, 1 tip ve 2 tip

3 sonlu tip vardır: 0 tipi 0 terim içerir. 1 tip 1 kanonik terimi içermektedir. Ve 2 tipi 2 kurallı terim içerir.

Çünkü 0 0 yazın koşullarını içeren, aynı zamanda denir boş tipi . Var olmayan her şeyi temsil etmek için kullanılır. Ayrıca yazılmıştır ve kanıtlanamayan her şeyi temsil eder. (Yani, bunun bir kanıtı olamaz.) Sonuç olarak, olumsuzlama ona bir fonksiyon olarak tanımlanır: . ${\displaystyle \bot }$${\displaystyle \neg A:=A\to \bot }$

Aynı şekilde 1 tipi de 1 kanonik terim içerir ve varlığı temsil eder. Ayrıca birim tipi olarak da adlandırılır . Genellikle kanıtlanabilen önermeleri temsil eder ve bu nedenle bazen yazılır . ${\displaystyle \top }$

Son olarak, 2 tipi 2 kurallı terim içerir. İki değer arasında kesin bir seçimi temsil eder. Bu kullanılan Boole değerler ancak değil önermeler. Önermeler 1 tipi olarak kabul edilir ve hiçbir zaman ispatı olmadığı ispatlanabilir ( 0 tipi) veya her iki şekilde de ispatlanamayabilir. ( Dışlanan Orta Yasası, sezgisel tip teorisindeki önermeler için geçerli değildir.)

Σ tür yapıcı

Σ-tipleri sıralı çiftleri içerir. Tipik sıralı çift (veya 2 demet) türlerinde olduğu gibi, bir Σ-tipi, diğer iki türün Kartezyen çarpımını , , ve . Mantıksal olarak, böyle sıralı bir çift, 'nin bir ispatını ve bir ispatını tutardı , bu nedenle böyle bir türün şeklinde yazıldığını görebiliriz . ${\displaystyle A\times B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A\wedge B}$

Σ türleri, bağımlı yazma nedeniyle tipik sıralı çift türlerinden daha güçlüdür . Sıralı ikilide, ikinci terimin türü, birinci terimin değerine bağlı olabilir. Örneğin, çiftin ilk terimi bir doğal sayı olabilir ve ikinci terimin türü, birinci terime eşit uzunlukta bir vektör olabilir. Böyle bir tür yazılır:

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

Küme teorisi terminolojisini kullanarak, bu, kümelerin dizinlenmiş ayrık birleşimlerine benzer . Olağan sıralı çiftler durumunda, ikinci terimin türü, birinci terimin değerine bağlı değildir. Böylece kartezyen çarpımı tanımlayan tip yazılır: ${\displaystyle {\mathbb {N} }\times {\mathbb {R} }}$

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

Burada, birinci terimin değerinin, , ikinci terimin türüne bağlı olmadığını belirtmek önemlidir . ${\displaystyle n}$${\displaystyle {\mathbb {R} }}$

Açıkçası, Σ-tipleri, matematikte kullanılan ve çoğu programlama dilinde kullanılan kayıtlar veya yapılarda kullanılan daha uzun bağımlı-tipi kümeler oluşturmak için kullanılabilir. Bağımlı olarak yazılan 3'lü kümeye bir örnek, iki tam sayı ve birinci tamsayının, tür tarafından açıklanan ikinci tamsayıdan daha küçük olduğunun kanıtıdır:

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

Bağımlı tipleme, Σ-türlerinin varoluşsal niceleyici rolüne hizmet etmesine izin verir . Açıklamada "Bir vardır Çeşidi , böyle ilk öğe değeridir sipariş çiftlerinin türünü olur kanıtlanmış" Çeşidi ve ikinci öğenin bir kanıtıdır . İkinci öğenin tipinin (kanıtlarının ) sıralı ikilinin ( ) ilk kısmındaki değere bağlı olduğuna dikkat edin . Türü şöyle olurdu: ${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle P(n)}$${\displaystyle n}$

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

Π tür yapıcı

Π-tipleri fonksiyonlar içerir. Tipik fonksiyon tiplerinde olduğu gibi, bir giriş tipi ve bir çıkış tipinden oluşurlar. Bununla birlikte, tipik işlev türlerinden daha güçlüdürler, çünkü dönüş türü giriş değerine bağlı olabilir. Tip teorisindeki fonksiyonlar küme teorisinden farklıdır. Küme teorisinde, argümanın değerini bir dizi sıralı çiftte ararsınız. Tip teorisinde, argüman bir terimle değiştirilir ve daha sonra terime hesaplama ("indirgeme") uygulanır.

Örnek olarak, bir doğal sayı verildiğinde , gerçek sayılar içeren bir vektör döndüren bir fonksiyonun türü şöyle yazılır: ${\displaystyle n}$${\displaystyle n}$

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

Çıkış tipi giriş değerine bağlı olmadığında, fonksiyon tipi genellikle basitçe bir . Böylece, doğal sayılardan gerçek sayılara kadar olan fonksiyonların türüdür. Bu tür Π-tipleri mantıksal çıkarımlara karşılık gelir. Mantıksal önerme , A'nın kanıtlarını alan ve B'nin kanıtlarını döndüren işlevleri içeren türe karşılık gelir . Bu tür daha tutarlı bir şekilde şu şekilde yazılabilir: ${\displaystyle \to }$${\displaystyle {\mathbb {N} }\to {\mathbb {R} }}$${\displaystyle A\implies B}$${\displaystyle A\to B}$

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

Π-tipleri ayrıca evrensel niceleme için mantıkta kullanılır . "Her için deyim Çeşidi , kanıtlanmış" bir işlev haline Çeşidi delillerine karşı . Böylece, verilen fonksiyon için değer, o değer için geçerli olan bir kanıt üretir . tip olurdu ${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle P()}$

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

= tür yapıcı

=-türleri iki terimden oluşturulur. ve gibi iki terim verildiğinde , yeni bir tür oluşturabilirsiniz . Bu yeni türün terimleri, çiftin aynı kanonik terime indirgediğinin kanıtlarını temsil eder. Böylece, hem ve hem de kurallı terimi hesapladığından , türünde bir terim olacaktır . Sezgisel tip teorisinde, =-türlerini ifade etmenin tek bir yolu vardır ve bu, refleksivitedir : ${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$${\displaystyle 2+2=2\cdot 2}$${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$${\displaystyle 4}$${\displaystyle 2+2=2\cdot 2}$

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

Terimlerin aynı kurallı terime indirgenmediği gibi =-türleri oluşturmak mümkündür , ancak bu yeni türden terimler oluşturamazsınız. Aslında, terimini oluşturabilseydiniz, terimini de oluşturabilirsiniz . Bunu bir işleve koymak, türde bir işlev oluşturur . Sezgisel tip teorisi olumsuzlamayı bu şekilde tanımladığı için, ya da sonunda, . ${\displaystyle 1=2}$${\displaystyle 1=2}$${\displaystyle \bot }$${\displaystyle 1=2\to \bot }$${\displaystyle \ldots \to \bot }$${\displaystyle \neg (1=2)}$${\displaystyle 1\neq 2}$

İspatların eşitliği, ispat teorisinde aktif bir araştırma alanıdır ve homotopi tipi teori ve diğer tip teorilerin geliştirilmesine yol açmıştır .

endüktif tipler

Endüktif türler, karmaşık, kendine referanslı türlerin oluşturulmasına izin verir. Örneğin, bağlantılı bir doğal sayılar listesi ya boş bir listedir ya da bir doğal sayı ve başka bir bağlantılı liste çiftidir. Endüktif türler, ağaçlar, grafikler vb. gibi sınırsız matematiksel yapıları tanımlamak için kullanılabilir. Aslında, doğal sayılar türü , başka bir doğal sayının ardılı veya ardılı olan bir tümevarım türü olarak tanımlanabilir . ${\displaystyle 0}$

Endüktif türler, sıfır ve ardıl işlevi gibi yeni sabitleri tanımlar . Yana bir tanım yoktur ve ikamesi ile değerlendirilemez, terimler gibi ve doğal sayıların kanonik terimleri haline gelir. ${\displaystyle 0{\mathbin {:}}{\mathbb {N} }}$${\displaystyle S{\mathbin {:}}{\mathbb {N} }\to {\mathbb {N} }}$${\displaystyle S}$${\displaystyle S0}$${\displaystyle SSS0}$

Endüktif türlerinde ispatlar ile mümkün kılınmıştır indüksiyonu . Her yeni tümevarım türü, kendi tümevarım kuralıyla birlikte gelir. Her doğal sayı için bir yüklemi kanıtlamak için aşağıdaki kuralı kullanırsınız: ${\displaystyle P()}$

${\displaystyle {\operatorname {{\mathbb {N} }-elim} }\,{\mathbin {:}}P(0)\,\to \left(\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)\to P(S(n))\right)\to \prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)}$

Sezgisel tip teorisindeki tümevarımsal tipler, sağlam temelli ağaçların tipi olan W-tipleri ile tanımlanır . Daha sonra tip teorisindeki çalışmalar, daha belirsiz öz-gönderimli türler üzerinde çalışmak için tümevarımlı türler, tümevarım-özyineleme ve tümevarım-tümevarım üretti. Daha yüksek endüktif türler , terimler arasında eşitliğin tanımlanmasına izin verir.

evren türleri

Evren türleri, diğer tür kurucuları ile oluşturulan tüm türler hakkında ispatların yazılmasına izin verir. Evren türündeki her terim , tümevarımlı tür oluşturucu ile herhangi bir kombinasyonu ile oluşturulan bir türe eşlenebilir . Ancak önlemek çelişkiye yol, hiçbir terim yoktur bu haritalar . ${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle 0,1,2,\Sigma ,\Pi ,=,}$${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{0}}$

Tüm "küçük türleri" hakkında deliller yazmak ve için , kullanmak gerekir yönelik bir terimi içeren işlevi gören , ancak kendisi için . Benzer şekilde, için . Evrenlerin tahmine dayalı bir hiyerarşisi vardır , bu nedenle herhangi bir sabit sabit evren üzerinde bir kanıtı ölçmek için kullanabilirsiniz . ${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{1}}$${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{1}}$${\displaystyle {\mathcal {U}}_{2}}$${\displaystyle k}$${\displaystyle {\mathcal {U}}_{k+1}}$

Evren türleri, tür teorilerinin zor bir özelliğidir. Martin-Löf'ün orijinal tip teorisi, Girard'ın paradoksunu hesaba katmak için değiştirilmek zorundaydı . Daha sonraki araştırmalar, "süper evrenler", "Mahlo evrenler" ve varsayımsal evrenler gibi konuları kapsıyordu.

yargılar

Sezgisel tip teorisinin resmi tanımı, yargılar kullanılarak yazılmıştır. Örneğin, "if bir tür ve bir tür ise o zaman bir türdür" ifadesinde " bir türdür", "ve" ve "eğer ... o zaman ..." yargıları vardır. İfade bir yargı değildir; tanımlanan türdür. ${\displaystyle A}$${\displaystyle B}$${\displaystyle \textstyle \sum _{a:A}B}$${\displaystyle \textstyle \sum _{a:A}B}$

Tip teorisinin bu ikinci seviyesi, özellikle eşitlik söz konusu olduğunda kafa karıştırıcı olabilir. Denebilecek bir eşitlik terimi yargısı vardır . İki terimin aynı kanonik terime indirgendiği bir ifadedir. Ayrıca bir tür eşitliği yargısı vardır, diyelim ki bu , her öğesinin türün bir öğesi olduğu anlamına gelir ve bunun tersi de geçerlidir. Tip düzeyinde, bir tür vardır ve bunun bir kanıtı varsa ve aynı değere indirilirse terimleri içerir . (Açıkçası, bu tür terimler eşitlik yargısı kullanılarak oluşturulur.) Son olarak, İngilizce dilinde bir eşitlik düzeyi vardır, çünkü "dört" kelimesini ve " " sembolünü standart terimi ifade etmek için kullanırız . Bunun gibi eş anlamlılar Martin-Löf tarafından "kesinlikle eşittir" olarak adlandırılır. ${\displaystyle 4=2+2}$${\displaystyle A=B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle 4=2+2}$${\displaystyle 4}$${\displaystyle 2+2}$${\displaystyle 4}$${\displaystyle SSSS0}$

Aşağıdaki yargıların açıklaması Nordström, Petersson ve Smith'teki tartışmaya dayanmaktadır.

Biçimsel teori, türler ve nesnelerle çalışır .

Bir tür tarafından bildirilir:

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

Aşağıdaki durumlarda bir nesne vardır ve bir türdedir:

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

Nesneler eşit olabilir

• ${\displaystyle a=b}$

ve türleri eşit olabilir

• ${\displaystyle A=B}$

Başka bir türden bir nesneye bağlı olan bir tür bildirildi

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

ve ikame ile kaldırıldı

• ${\displaystyle B[x/a]}$, Değişken değiştirilmesi nesne ile de .${\displaystyle x}$${\displaystyle a}$${\displaystyle B}$

Başka bir türden bir nesneye bağlı olan bir nesne iki şekilde yapılabilir. Nesne "soyutlanmış" ise, yazılır

• ${\displaystyle [x]b}$

ve ikame ile kaldırıldı

• ${\displaystyle b[x/a]}$, Değişken değiştirilmesi nesne ile de .${\displaystyle x}$${\displaystyle a}$${\displaystyle b}$

Nesneye bağlı nesne, özyinelemeli bir türün parçası olarak sabit olarak da bildirilebilir. Özyinelemeli türe bir örnek:

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

Burada, nesneye bağlı olarak sabit bir nesnedir. Bir soyutlama ile ilişkili değildir. Gibi sabitler eşitlik tanımlanarak kaldırılabilir. Burada toplama ile olan ilişki, aşağıdakilerin özyinelemeli yönünü ele almak için eşitlik ve kalıp eşleştirme kullanılarak tanımlanır : ${\displaystyle S}$${\displaystyle S}$${\displaystyle S}$

${\displaystyle {\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 S}$ opak bir sabit olarak manipüle edilir - ikame için dahili bir yapısı yoktur.

Yani nesneler ve türler ve bu ilişkiler teoride formülleri ifade etmek için kullanılır. Mevcut olanlardan yeni nesneler, türler ve ilişkiler yaratmak için aşağıdaki yargı stilleri kullanılır:

${\displaystyle \Gamma \vdash \sigma \ {\mathsf {Type}}}$	σ , Γ bağlamında iyi biçimlendirilmiş bir türdür.
${\displaystyle \Gamma \vdash t{\mathbin {:}}\sigma }$	t , Γ bağlamında σ türünde iyi biçimlendirilmiş bir terimdir .
${\displaystyle \Gamma \vdash \sigma \equiv \tau }$	σ ve τ , Γ bağlamında eşit türlerdir.
${\displaystyle \Gamma \vdash t\equiv u{\mathbin {:}}\sigma }$	t ve u , Γ bağlamında yargısal olarak eşit σ tipi terimlerdir .
${\displaystyle \vdash \Gamma \ {\mathsf {Context}}}$	Γ, varsayımları yazmak için iyi biçimlendirilmiş bir bağlamdır.

Geleneksel olarak, diğer tüm türleri temsil eden bir tür vardır. (veya ) denir . Yana türüdür; üyesi nesnelerdir. Her nesneyi karşılık gelen türüne eşleyen bağımlı bir tür vardır. Çoğu metinde asla yazılmaz. İfadenin bağlamından, bir okuyucu hemen hemen her zaman bir türe atıfta bulunup bulunmadığını veya türe karşılık gelen nesneye atıfta bulunup bulunmadığını söyleyebilir . ${\displaystyle {\mathcal {U}}}$${\displaystyle \operatorname {Set} }$${\displaystyle {\mathcal {U}}}$${\displaystyle \operatorname {El} }$${\displaystyle \operatorname {El} }$${\displaystyle A}$${\displaystyle {\mathcal {U}}}$

Bu, teorinin tam temelidir. Diğer her şey türetilmiştir.

Mantığı uygulamak için her önermeye kendi türü verilir. Bu türlerdeki nesneler, önermeyi kanıtlamanın farklı olası yollarını temsil eder. Açıktır ki, önerme için bir kanıt yoksa, türün içinde nesne yoktur. Önermeler üzerinde çalışan "ve" ve "veya" gibi operatörler yeni türler ve yeni nesneler sunar. Yani türüne bağlıdır türüdür ve tip . Bu bağımlı türdeki nesneler, ve içindeki her nesne çifti için var olacak şekilde tanımlanır . Açıktır ki, ispatı yoksa veya yoksa ve boş bir tipse, temsil eden yeni tip de boştur. ${\displaystyle A\times B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A\times B}$

Bu, diğer türler (booleans, doğal sayılar, vb.) ve operatörleri için yapılabilir.

Tip teorisinin kategorik modelleri

Dilini kullanarak kategori teorisi , RAG Seely bir kavramını tanıttı lokal kartezyen kapalı kategori tipi teorisinin temel model olarak (LCCC). Bu, Hofmann ve Dybjer tarafından, Cartmell'in daha önceki çalışmasına dayalı olarak Aileleri Olan Kategoriler veya Nitelikleri Olan Kategoriler olarak geliştirilmiştir .

Aileleri ile bir kategori, bir kategorisi Cı birlikte bir funktoru ile, (ki buradaki objeler bağlamlarda, ve bağlam morfizimler ikamelerdir) bağlamların T  : C ^op → Fam ( Set ).

Fam ( Küme ), nesnelerin bir "dizin kümesi" A ve bir B : X → A fonksiyonunun çiftleri olduğu ve morfizmlerin f  : A → A' ve g  : X → fonksiyon çiftleri olduğu Küme ailelerinin kategorisidir. X ' öyle ki, B' _° gr = f _° B , diğer bir deyişle, - f harita B _bir için oda _{g ( a )} . ${\displaystyle (A,B)}$

Funktoru T bir bağlama atar G bir dizi türleri ve her biri için , bir dizi terim. Bir işlev için aksiyomlar, bunların ikame ile uyumlu bir şekilde oynamasını gerektirir. Değişiklik genellikle form yazılır Af veya af , bir de bir tür olan ve bir de bir terimdir ve f den yapılan bir substitusyondur D için G . Burada ve . ${\displaystyle Ty(G)}$${\displaystyle A:Ty(G)}$${\displaystyle Tm(G,A)}$${\displaystyle Ty(G)}$${\displaystyle Tm(G,A)}$${\displaystyle Af:Ty(D)}$${\displaystyle af:Tm(D,Af)}$

C kategorisi , bir uç nesne (boş bağlam) ve sağ öğenin sol öğe bağlamında bir tür olduğu anlama veya bağlam uzantısı adı verilen bir ürün biçimi için son bir nesne içermelidir. Eğer G bir bağlam ve daha sonra bir amacı olmalıdır bağlamlar arasında nihai D dönüşümler ile p  : D → G , q  : Tm ( D, Ap ). ${\displaystyle A:Ty(G)}$${\displaystyle (G,A)}$

Martin-Löf'ünki gibi mantıksal bir çerçeve, bağlama bağlı tür ve terim kümeleri üzerinde kapatma koşulları biçimini alır: Küme adında bir tür olması ve her küme için bir tür olması, türlerin formları altında kapatılması gerekir. bağımlı toplam ve ürün vb.

Tahmini küme teorisi gibi bir teori, küme türleri ve öğeleri üzerindeki kapatma koşullarını ifade eder: kümelerin bağımlı toplamı ve çarpımı yansıtan işlemler altında ve çeşitli tümevarımsal tanım biçimleri altında kapatılması gerektiği.

Genişletmeye karşı yoğun

Temel bir ayrımdır uzatıcı vs intensional tip teorisi. Genişlemeli tip teorisinde, tanımsal (yani hesaplamalı) eşitlik, ispat gerektiren önermesel eşitlikten ayırt edilmez. Sonuç olarak, teorideki programlar sona ermeyebileceğinden , genişlemeli tip teorisinde tip kontrolü kararsız hale gelir . Örneğin, böyle bir teori Y-birleştiriciye bir tip verilmesine izin verir , bunun ayrıntılı bir örneği Nordstöm ve Petersson Programming'de Martin-Löf's Type Theory'de bulunabilir . Ancak bu, genişlemeli tip teorisinin pratik bir araç için bir temel olmasını engellemez, örneğin, NuPRL genişlemeli tip teorisine dayanır.

İntensional tip kuramı aksine tür denetimi olduğunu Karar verilebilen , ama intensional mantık kullanılarak gerektirdiği için, standart matematiksel konseptleri, biraz daha külfetlidir setoids veya benzeri yapılar. Tamsayılar , rasyonel sayılar ve gerçek sayılar gibi, üzerinde çalışılması zor olan veya bu olmadan temsil edilemeyen birçok yaygın matematiksel nesne vardır . Tamsayılar ve rasyonel sayılar, setoidler olmadan temsil edilebilir, ancak bu gösterimle çalışmak kolay değildir. Cauchy gerçek sayılar bu olmadan temsil edilemez.

Homotopi tipi teori bu sorunu çözmeye çalışır. Bu, tanımlamak bir sağlar yüksek indüktif türleri birinci dereceden kurucular (tanımlamaz, yalnızca değer veya noktalar ), ancak daha yüksek dereceli kurucular, örneğin, eşitlikler elemanları arasında ( yollar ), eşitliklerde arasında (eşitlikler homotopies ), sonsuza .

Tip teorisinin uygulamaları

Bir dizi ispat yardımcısının altında yatan resmi sistemler olarak farklı tip teorisi biçimleri uygulanmıştır . Birçoğu Per Martin-Löf'ün fikirlerine dayansa da, birçoğu ek özellikler, daha fazla aksiyom veya farklı felsefi geçmişe sahiptir. Örneğin, NuPRL sistemi hesaplamalı tip teorisine dayanır ve Coq (ko)indüktif yapıların hesabını temel alır . Bağımlı türler ayrıca ATS , Cayenne , Epigram , Agda ve Idris gibi programlama dillerinin tasarımında da yer alır .

Martin-Löf tipi teoriler

Per Martin-Löf , çeşitli zamanlarda yayınlanan çeşitli tip teoriler inşa etti, bazıları açıklamalarıyla birlikte ön baskıların uzmanlar tarafından erişilebilir hale gelmesinden çok daha sonra (diğerleri arasında Jean-Yves Girard ve Giovanni Sambin). Aşağıdaki liste, basılı biçimde açıklanan tüm teorileri listelemeye ve onları birbirinden ayıran temel özellikleri çizmeye çalışmaktadır. Tüm bu teorilerin bağımlı ürünleri, bağımlı toplamları, ayrık birlikleri, sonlu türleri ve doğal sayıları vardı. Tüm teoriler, bağımlı ürünler için η-indirgenmesinin eklendiği MLTT79 dışında, ne bağımlı ürünler için ne de bağımlı toplamlar için η-indirgenmesini içermeyen aynı indirgeme kurallarına sahipti.

MLTT71 , Per Martin-Löf tarafından oluşturulan tip teorilerin ilkiydi. 1971'de bir ön baskıda ortaya çıktı. Tek bir evreni vardı ama bu evrenin kendi içinde bir adı vardı, yani bugün "Type in Type" olarak adlandırılan bir tip teorisiydi. Jean-Yves Girard , bu sistemin tutarsız olduğunu ve ön baskının hiçbir zaman yayınlanmadığını göstermiştir.

MLTT72 , şu anda yayınlanmış olan 1972 tarihli bir ön baskıda sunuldu. Bu teorinin tek bir evren V'si vardı ve hiçbir kimlik türü yoktu. Evren, bir nesne ailesinin V'den V'de olmayan bir nesneye bağımlı ürününün, örneğin V'nin kendisi gibi, V'de olduğu varsayılmaması anlamında "tahmin ediciydi". Russell, yani, "El" gibi ek kurucu olmadan doğrudan "T∈V" ve "t∈T" yazılır (Martin-Löf, modern ":" yerine "∈" işaretini kullanır).

MLTT73 , Per Martin-Löf'ün yayınladığı tip teorisinin ilk tanımıydı (Logic Colloquium 73'te sunuldu ve 1975'te yayınlandı). "Önermeler" olarak adlandırdığı özdeşlik türleri vardır, ancak önermeler ile geri kalan türler arasında gerçek bir ayrım yapılmadığı için bunun anlamı belirsizdir. Daha sonra J-eliminator adını alan ama henüz adı olmayan bir şey var (bkz. s. 94-95). Bu teoride sonsuz bir evren dizisi vardır V ₀ , ..., V _n , ... . Evrenler tahmin edicidir, a-la Russell ve birikimli değildir ! Aslında, Sonuç 3.10 s. 115, eğer A∈V _m ve B∈V _n , A ve B dönüştürülebilir olacak şekilde ise m  =  n olduğunu söylüyor . Bu araçlar, örneğin, bu univalence formüle edilmesi zor olacağını teorinin orada V her büzülebilir türleri _ı ancak V bağlanması herhangi bir kimlik türleri vardır çünkü eşit olacak şekilde bunları yayınlama belirsizdir, _I ve V _j için ben ≠ j .

MLTT79 1979'da sunuldu ve 1982'de yayınlandı. Bu yazıda, Martin-Löf, bu tür sistemlerin meta-teorisinin çalışmasında o zamandan beri temel hale gelen bağımlı tip teorisi için dört temel yargı türünü tanıttı. Ayrıca bağlamları içinde ayrı bir kavram olarak tanıttı (bkz. s. 161). J-eliminator ile (MLTT73'te daha önce yer alan ama orada bu isme sahip olmayan) özdeşlik türleri olduğu gibi, teoriyi "uzaylı" yapan kuralı da vardır (s. 169). W tipleri var. Kümülatif olan sonsuz bir yüklem evrenleri dizisi vardır .

Bibliopolis : 1984 tarihli Bibliopolis kitabında bir tip teorisi tartışması vardır, ancak bu biraz açık uçludur ve belirli bir dizi seçimi temsil etmiyor gibi görünmektedir ve bu nedenle onunla ilişkili belirli bir tip teorisi yoktur.

Ayrıca bakınız

• Sezgisel mantık
• Yazılan lambda hesabı

Notlar

Referanslar

• Martin-Löf, Per (1984). Sezgisel tip teorisi (PDF) . Sambin, Giovanni. Napoli: Bibliopolis. ISBN'si 978-8870881059. OCLC  12731401 .

daha fazla okuma

• Per Martin-Löf's Notes, Giovanni Sambin tarafından kaydedildiği gibi (1980)
• Nordström, Bengt; Peterson, Kent; Smith, Jan M. (1990). Martin-Löf'ün Tip Teorisinde Programlama . Oxford Üniversitesi Yayınları. ISBN'si 9780198538141.
• Thompson, Simon (1991). Tip Teorisi ve Fonksiyonel Programlama . Addison-Wesley. ISBN'si 0-201-41667-0.
• Granström, Johan G. (2011). Sezgisel Tip Teorisi Üzerine İnceleme . Springer. ISBN'si 978-94-007-1735-0.

Dış bağlantılar

• AB Türleri Projesi: Öğreticiler – Türler Yaz Okulu 2005'ten ders notları ve slaytlar
• n-Categories - Sketch of a Definition – John Baez ve James Dolan'dan Ross Street'e mektup , 29 Kasım 1995