Sistem U - System U

Olarak matematiksel mantık , sistem, U ve sistem, U ^- olan saf tip sistemler , bir yani özel formları, yazılı lambda hesap keyfi bir sayı olan sıralar , önermeler ve kurallarına (ya da sıralar arasındaki bağımlılıklar). Her ikisinin de 1972'de Jean-Yves Girard tarafından tutarsız olduğu kanıtlandı . Bu sonuç, Martin-Löf'ün orijinal 1971 tipi teorisinin , Girard'ın paradoksunun kullandığı aynı "Tipte Tip" davranışına izin verdiği için tutarsız olduğunun anlaşılmasına yol açtı .

Resmi tanımlama

Sistem U, saf tip bir sistem olarak tanımlanır.

• üç çeşit ; ${\ displaystyle \ {\ ast, \ kare, \ üçgen \}}$
• iki aksiyom ; ve ${\ displaystyle \ {\ ast: \ kare, \ kare: \ üçgen \}}$
• beş kural . ${\ displaystyle \ {(\ ast, \ ast), (\ kare, \ ast), (\ kare, \ kare), (\ üçgen, \ ast), (\ üçgen, \ kare) \}}$

Sistem U ^- kural haricinde aynı şekilde tanımlanır . ${\ displaystyle (\ üçgen, \ ast)}$

Sıralar ve geleneksel olarak sırasıyla " Tür " ve " Tür " olarak adlandırılır; sıralamanın belirli bir adı yoktur. İki aksiyonları çeşitleri (içinde türleri tutulmasını tarif olarak) ve çeşitleri ( ). Sezgisel olarak, türler , terimlerin doğasında bir hiyerarşiyi tanımlar. ${\ displaystyle \ ast}$${\ displaystyle \ kare}$${\ displaystyle \ üçgen}$${\ displaystyle \ ast: \ kare}$${\ displaystyle \ üçgen}$${\ displaystyle \ kare: \ üçgen}$

1. Tüm değerlerin bir türü vardır , örneğin bir temel tür ( örneğin " b bir boolean" olarak okunur ) veya bir (bağımlı) işlev türü ( ör . " F , doğal sayılardan boolelere bir işlevdir " olarak okunur ). ${\ displaystyle b: \ mathrm {Bool}}$ ${\ displaystyle f: \ mathrm {Nat} \ - \ mathrm {Bool}}$
2. ${\ displaystyle \ ast}$ bu tür tüm türlerin türüdür ( " t bir türdür" olarak okunur ). Dan biz gibi daha fazla terim, inşa edebilirsiniz hangi tür tekli tip düzey operatörlerin ( örn olarak okunur “ Liste olduğunu, bir polimorfik tipi türlerinden türlerine bir fonksiyondur”). Kurallar, yeni türleri nasıl oluşturabileceğimizi kısıtlıyor. ${\ displaystyle t: \ ast}$${\ displaystyle \ ast}$${\ displaystyle \ ast \ ila \ ast}$ ${\ displaystyle \ mathrm {Liste}: \ ast \ ila \ ast}$
3. ${\ displaystyle \ kare}$ bu tür tüm türlerin türüdür ( " k bir türdür" olarak okunur ). Benzer şekilde, kuralların izin verdiğine göre ilgili terimleri oluşturabiliriz. ${\ displaystyle k: \ kare}$
4. ${\ displaystyle \ üçgen}$ bu tür tüm terimlerin türüdür.

Kurallar, türler arasındaki bağımlılıkları yönetir: değerlerin değerlere ( işlevlere ) bağlı olabileceğini, değerlerin türlere bağlı olmasına izin verdiğini (çok biçimlilik ), türlerin türlere bağlı olmasına izin verdiğini ( tür operatörleri ) vb. Söyler. ${\ displaystyle (\ ast, \ ast)}$${\ displaystyle (\ kare, \ ast)}$${\ displaystyle (\ kare, \ kare)}$

Girard'ın paradoksu

Sistem U ve U tanımları ^- atanmasını sağlar polimorfik tür için genel kurucular gibi klasik polimorfik lambda taşlarının, terimlerin polimorfik türlerine benzer şekilde Sistem F . Böyle bir genel kurucuya bir örnek (burada k , bir tür değişkeni belirtir) olabilir

${\ displaystyle \ lambda k ^ {\ square} \ lambda \ alpha ^ {k \ to k} \ lambda \ beta ^ {k} \!. \ alpha (\ alpha \ beta) \;: \; \ Pi k: \ kare ((k \ - k) \ - k \ - k)}$ .

Bu mekanizma, türle bir terim oluşturmak için yeterlidir , bu da her türün yerleşik olduğunu ima eder . By Curry-Howard yazışma , bu her mantıksal önermeler sistemin tutarsız yapar olma kanıtlanabilir, eşdeğerdir. ${\ displaystyle (\ forall p: \ ast, p) = \ bot}$

Girard paradoksu olan tip-teorik bir analog Russell'ın paradoksu içinde küme teorisinin .

Referanslar

daha fazla okuma

• Barendregt, Henk (1992). "Lambda calculi türleri" . S. Abramsky'de; D. Gabbay; T. Maibaum (editörler). Bilgisayar Bilimlerinde Mantık El Kitabı . Oxford Science Publications . sayfa 117–309.
• Coquand, Thierry (1986). "Girard'ın paradoksunun bir analizi". Bilgisayar Bilimlerinde Mantık . IEEE Computer Society Press. s. 227–236.