Boş tip

Boş tipi olduğu tip teori hiçbir değer içeren bir türü.

Genellikle bot ( alt tipte ), sembol ( ) veya ASCII yaklaşımı _ | _ ile kısaltılır . Bazen sıfır türü olarak da adlandırılır . Üst tip veya ünite tipi ile karıştırılmamalıdır . Üst tür , bir sistemin tüm değerlerini içerir. Birim türünün tek bir değeri vardır. $\ bot$

Boş tip genellikle aşağıdaki durumlarda kullanılır:

Sahte olduğunu belirtmek için. Bu tanımlar ve ifade etmek için kullanılabilir olumsuzluk aksiyomu ex falso sonraki Maddeleri Quodlibet : herhangi bir teklif için : . Bu aksiyomun reddettiği asgari mantık dışında , boş tip, sonuç olarak, saçmalığa, sistemin tutarsızlığına işaret eder. $P$ $\ bot \ 'dan P'ye$
Bir işlevin veya hesaplamanın farklılık gösterdiğini belirtmek için ; başka bir deyişle, arayan kişiye bir sonuç vermez. Bu, programın bitmeyeceği anlamına gelmez; bir işlev , arayana geri dönmeden sonlandırılabilir veya normal dönüş dışında bir yöntemle, örneğin bir devam ettirme yoluyla çıkabilir .
Bir hatayı belirtmek için; bu, esas olarak, hatalar arasındaki ayrımların önemli olmadığı teorik dillerde gerçekleşir. Kullanışlı programlama dilleri bunun yerine istisna işlemeyi kullanır.

Kullanım örnekleri

Horoz

Coq yazılımı , standart kitaplığındaki boş türü şu şekilde tanımlar:

Inductive False : Prop :=.

Buna karşılık, birim türü olduğunu

Inductive True : Prop := I : True.

Dilin açıklamasına girmeden, bunun tür için I : Truebir kurucu olduğunu görürüz True. Tersine, Falsesomutlaştırmayı engelleyecek bir kurucunun yokluğu, başka bir deyişle, tipte bir nesne oluşturulamaz False ; Bu bir şans çünkü, Curry-Howard'ın yazışmasına göre , bu türden bir nesne, mantığın tutarsızlığının bir kanıtı olarak asimile olacaktı.

Tanımı Falseotomatik olarak aksiyomu ex falso sequitur quodlibet'i oluşturur :

False_ind : forall P : Prop, False -> P

Olumsuzluk basitçe şu şekilde tanımlanır:

Definition not (A:Prop) := A -> False.

Haskell

Gelen Haskell anahtar tanımlanmamış olan sonuç boş türüne sahip bir hesaplama temsil eder. Yürütme sırasında tanımsız olarak değerlendirmeye çalışmak , programı sonlandırır.

İlgili Makaleler

Kaynak

(tr) Bu makale kısmen veya tamamen alınır İngilizce Vikipedi başlıklı makalesinde " Bottom_type " ( yazarların listesini görmek ) .

Dış bağlantılar

(tr) Türler ve Programlama Dilleri , Benjamin Pierce (MIT Press 2002) [1]