세토이드

수학에서 setoid(X, ~)는 등가 관계가 ~가 장착된 set(또는 타입) X이다. setoid는 E-set, Bishop set 또는 extension set라고도 할 수 있다.^[1]

세토이드는 특히 증명 이론과 수학의 유형 이데올로기적 기초에서 연구된다.수학에서 흔히, 집합에 동등성 관계를 정의할 때, 즉시 등가 집합을 형성한다(등가성을 동등성으로 변환).대조적으로, 세토이드는 종종 강도적 평등(원래 집합의 평등)과 확장적 평등(균등성 관계 또는 몫 집합의 평등)에 대한 해석과 함께, 정체성과 동등성 사이의 차이가 유지되어야 할 때 사용될 수 있다.

증명 이론

증명 이론, 특히 Curry-Howard 통신에 기초한 건설 수학의 증명 이론에서는 종종 수학 명제를 증명 집합으로 식별한다(있는 경우).주어진 명제는 물론 많은 증거를 가지고 있을 수 있다; 증명 비합리성의 원칙에 따르면, 일반적으로 어떤 증명이 사용되었는지가 아니라 명제의 진실만이 중요하다.그러나 Curry-Howard 서신은 증거를 알고리즘으로 바꿀 수 있으며 알고리즘 간의 차이가 중요한 경우가 많다.따라서 증명 이론가들은 베타 변환 등을 통해 서로 변환될 수 있는 경우 동등한 증거를 고려하여 증명서를 한 세트로이드로 명제를 식별하는 것을 선호할 수 있다.

유형론

수학의 유형-이론적 기초에서, 일반 수학 세트를 모형화하기 위한 지수 유형이 부족한 유형 이론에 세토이드를 사용할 수 있다.예를 들어 페르 마르틴 뢰프의 직관적 유형 이론에서는 실수의 유형이 없고, 오직 이성적인 숫자의 규칙적인 코치 시퀀스의 유형만 존재한다.따라서 마틴 뢰프의 틀에서 실제 분석을 하기 위해서는 일반적인 동등성 개념을 갖춘 규칙적인 코치 시퀀스의 유형인 실수의 집합체(setoid of real number)로 작업해야 한다.실제 숫자의 술어와 함수는 규칙적인 Cauchy 시퀀스에 대해 정의되어야 하며 동등성 관계와 호환되는 것으로 증명되어야 한다.전형적으로(사용하는 형식 이론에 따라 달라지지만) 선택 공리는 유형 간 함수(직관 함수)에 대해서는 유지되지만, 세토이드 간 함수(확장 함수)에는 유지되지 않는다.^{[clarification needed]}"set"이라는 용어는 "type"의 동의어 또는 "setoid"^[2]의 동의어로 다양하게 사용된다.

건설수학

건설 수학에서는 흔히 건설적인 세토이드라고 불리는 동등성 관계 대신 차별성 관계가 있는 세토이드를 택한다.때로는 부분적 등가관계나 부분적 분리성을 이용한 부분적 세토이드를 고려하기도 한다.(예: 참조)Barthe 등, 섹션 1)

참고 항목

• 조로이드

메모들

참조

• Hofmann, Martin (1995), "A simple model for quotient types", Typed lambda calculi and applications (Edinburgh, 1995), Lecture Notes in Comput. Sci., vol. 902, Berlin: Springer, pp. 216–234, CiteSeerX 10.1.1.55.4629, doi:10.1007/BFb0014055, ISBN 978-3-540-59048-4, MR 1477985.
• Barthe, Gilles; Capretta, Venanzio; Pons, Olivier (2003), "Setoids in type theory" (PDF), Journal of Functional Programming, 13 (2): 261–293, doi:10.1017/S0956796802004501, MR 1985376.

외부 링크

• Coq에서의 세토이드 구현
• setoid in nLab
• nLab을 설정한 비숍