什么是集合體
編輯在數學中,集合體(X,~)是一個配備有等價關系~的集合(或類型)X。擬集也可稱為E集、主教集或擴展集。集合體尤其在證明理論和數學的類型理論基礎中被研究。在數學中,當人們在一個集合上定義一個等價關系時,通常會立即形成商集(將等價變成平等)。相反,當必須保持同一性和等價性之間的差異時,可以使用集合體,通常是用擴展的平等(原始集合上的平等)和擴展的平等(等價關系,或商集合上的平等)來解釋。
證明理論
編輯在證明理論中,特別是基于庫里-霍華德對應關系的構造數學的證明理論中,人們常常將一個數學命題與它的證明集(如果有的話)聯系起來。當然,一個給定的命題可能有許多證明;根據證明無關性原則,通常只有命題的真實性才是重要的,而不是哪一個證明被使用。然而,庫里-霍華德對應關系可以把證明變成算法,而算法之間的差異往往是重要的。因此,證明理論家可能更傾向于將一個命題與一個證明的集合體相識別,如果證明可以通過β轉換或類似的方式相互轉換,則認為它們是等價的。
類型理論
編輯在數學的類型理論基礎中,setoids可能被用于缺乏商數類型的類型理論中,以模擬一般的數學集合。例如,在佩爾-馬丁-勒夫的直覺類型理論中,沒有實數的類型,只有有理數的規則考奇序列的類型。因此,要在馬丁-洛夫的框架內進行實數分析,就必須使用一個實數集合體,即具有通常的等價概念的有規律的考奇序列類型。實數的謂詞和函數需要為正則Cauchy序列定義,并證明其與等價關系兼容。通常(盡管這取決于所使用的類型理論),選擇公理對于類型之間的函數(擴展函數)是成立的,但對于集合體之間的函數(擴展函數)則不成立。集合一詞被不同程度地用作類型的同義詞或setoid的同義詞。
構造數學
編輯在構造數學中,人們常常把一個具有不等價關系而不是等價關系的集合體稱為構造集合體。有時人們也考慮使用部分等價關系或部分不等價關系的部分集合體。(例如,見Barthe等人,第1節)
內容由匿名用戶提供,本內容不代表www.gelinmeiz.com立場,內容投訴舉報請聯系www.gelinmeiz.com客服。如若轉載,請注明出處:http://www.gelinmeiz.com/170810/