Bottom type
http://dbpedia.org/resource/Bottom_type
In type theory, a theory within mathematical logic, the bottom type of a type system is the type that is a subtype of all other types. Where such a type exists, it is often represented with the up tack (⊥) symbol. When the bottom type is empty, a function whose return type is bottom cannot return any value, not even the lone value of a unit type. In such a language, the bottom type may therefore be known as the zero or never type. In the Curry–Howard correspondence, an empty type corresponds to falsity.
rdf:langString
ボトム型（ボトムがた、英: Bottom type）とは、型理論や数理論理学において値を持たない型のことである。ゼロ型または空型とも呼ばれ、アップタック記号（⊥）で表記される。戻り値の型がボトム型である関数は、いかなる値も返さない。カリー＝ハワード同型対応ではボトム型は偽に対応する。
rdf:langString
Le type vide est en théorie des types un type qui ne comporte pas de valeurs. On l'abrège communément par bot (de bottom type), le symbole ou par l'approximation ASCII _|_.On l'appelle aussi parfois type zéro. Il ne faut pas le confondre avec le type top ou le type unité. Le type top comprend toutes les valeurs d'un système. Le type unité a une seule valeur. On utilise souvent le type vide dans les cas suivants :
rdf:langString
Низший тип (нулевой тип, пустой тип) — объект, использующийся в некоторых теориях типов и языках программирования, соответствующий типу без значений. Стандартное математическое обозначение —. В рамках соответствия Карри — Ховарда низший тип соответствует логической ложной формуле. В системах, предусматривающих , низший тип является подтипом всех типов; при этом обратное может быть неверно — в некоторых вариантах подтип всех типов не обязательно будет низшим. В некоторых системах типов вводится двойственное понятие — высший тип, охватывающий все возможные значения в системе.
rdf:langString
rdf:langString
Bottom type
rdf:langString
Type vide
rdf:langString
ボトム型
rdf:langString
Низший тип
xsd:integer
3893287
xsd:integer
1118658669
rdf:langString
In type theory, a theory within mathematical logic, the bottom type of a type system is the type that is a subtype of all other types. Where such a type exists, it is often represented with the up tack (⊥) symbol. When the bottom type is empty, a function whose return type is bottom cannot return any value, not even the lone value of a unit type. In such a language, the bottom type may therefore be known as the zero or never type. In the Curry–Howard correspondence, an empty type corresponds to falsity.
rdf:langString
Le type vide est en théorie des types un type qui ne comporte pas de valeurs. On l'abrège communément par bot (de bottom type), le symbole ou par l'approximation ASCII _|_.On l'appelle aussi parfois type zéro. Il ne faut pas le confondre avec le type top ou le type unité. Le type top comprend toutes les valeurs d'un système. Le type unité a une seule valeur. On utilise souvent le type vide dans les cas suivants :
* Pour signifier le faux. Il peut être employé pour définir la négation et exprimer l'axiome ex falso sequitur quodlibet : Pour toute proposition : . Hormis en logique minimale que rejette cet axiome, le type vide désigne donc par voie de conséquence, l'absurdité, l'état d'incohérence du système.
* Pour signaler qu'une fonction ou un calcul diverge ; en d'autres termes, il ne retourne pas de résultat à l'appelant. Cela ne signifie pas nécessairement que le programme ne se termine pas ; une fonction peut terminer sans retourner à son appelant, ou sortir par un moyen autre qu'un retour normal, par exemple via une continuation.
* Pour indiquer une erreur ; cela arrive principalement dans des langages théoriques dans lesquels les distinctions entre les erreurs ne sont pas importantes. Les langages de programmation pratiques utilisent une gestion d'exceptions à la place.
rdf:langString
ボトム型（ボトムがた、英: Bottom type）とは、型理論や数理論理学において値を持たない型のことである。ゼロ型または空型とも呼ばれ、アップタック記号（⊥）で表記される。戻り値の型がボトム型である関数は、いかなる値も返さない。カリー＝ハワード同型対応ではボトム型は偽に対応する。
rdf:langString
Низший тип (нулевой тип, пустой тип) — объект, использующийся в некоторых теориях типов и языках программирования, соответствующий типу без значений. Стандартное математическое обозначение —. В рамках соответствия Карри — Ховарда низший тип соответствует логической ложной формуле. В системах, предусматривающих , низший тип является подтипом всех типов; при этом обратное может быть неверно — в некоторых вариантах подтип всех типов не обязательно будет низшим. В некоторых системах типов вводится двойственное понятие — высший тип, охватывающий все возможные значения в системе. В программировании низший тип в качестве возвращаемого значения функции часто используется чтобы показать расходимость функции: когда функция не возвращает никаких результатов вызывающей стороне. Поддерживаются в Haskell (начиная с версии 2010), Common Lisp (символ NIL), Scala (Nothing; также используется для ковариантности параметризованных типов), Rust (экспериментальный тип данных, обозначаемый как !; присутствует в сигнатуре функций, которые гарантированно не возвращают значений, например, при вызове panic! или бесконечном цикле, и как возвращаемый тип для операторов потока управления, таких как break и return), Ceylon (Nothing), Julia (Union{}), TypeScript (never), JavaScript с аннотациями (!Null), PHP (never), Python (typing.NoReturn), Kotlin (Nothing), Elm (Never), D (noreturn).
xsd:nonNegativeInteger
8939