| 翻訳と辞書 |
Setoid
In mathematics, a setoid (also called an E-set) is a set (or type) equipped with an equivalence relation.
Setoids are studied especially in proof theory and in type-theoretic foundations of mathematics. Often in mathematics, when one defines an equivalence relation on a set, one immediately forms the quotient set (turning equivalence into equality). In contrast, setoids may be used when a difference between identity and equivalence must be maintained, often with an interpretation of intensional equality (the equality on the original set) and extensional equality (the equivalence relation, or the equality on the quotient set).
==Proof theory==
In proof theory, particularly the proof theory of constructive mathematics based on the Curry–Howard correspondence, one often identifies a mathematical proposition with its set of proofs (if any). A given proposition may have many proofs, of course; according to the principle of proof irrelevance, normally only the truth of the proposition matters, not which proof was used. However, the Curry–Howard correspondence can turn proofs into algorithms, and differences between algorithms are often important. So proof theorists may prefer to identify a proposition with a ''setoid'' of proofs, considering proofs equivalent if they can be converted into one another through beta conversion or the like.
抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』
■ウィキペディアで「Setoid」の詳細全文を読む
スポンサード リンク
| 翻訳と辞書 : 翻訳のためのインターネットリソース |
Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.
|
|