아이덴티티 타입

Identity type

유형 이론에서, 동일 유형은 평등 개념을 나타냅니다.그것은 또한 "사법적 평등"과 구별되는 명제적 평등이라고도 알려져 있다.유형 이론의 평등은 복잡한 주제이며 호모토피 유형 [1]이론의 분야와 같은 연구 주제였다.

평등한 판단과의 비교

동일 유형은 유형 [2]이론에서 평등에 대한 두 가지 다른 개념 중 하나입니다.더 근본적인 개념은 판단력인 "판단력 평등"이다.

평등을 넘어서는

아이덴티티 타입은 판단적 평등이 할 수 있는 것보다 더 많은 것을 할 수 있다.이는 "x + +x {\x}"를 표시하기 위해 사용할 수 있으며, 이는 판단상의 평등성으로는 나타낼 수 없습니다.이는 "R"로 알려진 자연수의 제거기(또는 "재귀자")를 사용하여 수행됩니다.

"R" 함수는 자연수에 새로운 함수를 정의해 봅시다.이 새로운 함수 "P"는 "(x:nat . x+1 = 1+x)로 정의됩니다.다른 주장은 유도 증명의 일부처럼 작용합니다."PZ : P 0" 인수는 "0+1 = 1+0" 이 됩니다.이것은 "refl nat 1"이라는 용어입니다."PS : P n → \displaystyle \to } \to P (S n)" 인수는 유도 대소문자가 됩니다.기본적으로 이것은 "x+1 = 1+x"가 "x"를 표준값으로 대체했을 때 표현식은 "refl nat (x+1)"과 동일함을 의미합니다.

ID 유형 버전

정체성은 복잡하고 유형 이론의 연구 주제이다.모든 버전이 컨스트럭터에 동의하지만 "refl"입니다.특성과 제거기 기능은 크게 다릅니다.

"확장" 버전의 경우 모든 ID 유형을 판별 평등으로 변환할 수 있습니다.컴퓨터 버전은 Thomas Streicher에 [3]의해 "Axiom K"로 알려져 있습니다.이것들은 요즘 별로 인기가 없어요.

아이덴티티 타입의 복잡성

마틴 호프만과 토마스 스트라이커는 아이디 타입이론은 아이디 타입의 모든 용어가 [4]동일해야 한다고 반박했다.

정체성에 대한 인기 있는 연구 분야는 호모토피형[5] 이론과 그 입체형 이론이다.

레퍼런스

  1. ^ "Identity Type". nLab. Retrieved 19 January 2022.
  2. ^ Martin-Löf, Per (June 1980). Intuitionistic Type Theory (PDF).
  3. ^ Streicher, Thomas (1993). Investigations into intensional type theory (PDF).
  4. ^ Hoffman, Martin; Streicher, Thomas (July 1994). "The groupoid model refutes uniqueness of identity proofs". Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science.
  5. ^ Univalent Foundations Program. Homotopy Type Theory. Institute for Advanced Study.