Identity type

In type theory, a branch of mathematics, the identity type represents the concept of equality. It is also known as propositional equality to differentiate it from "judgemental equality". Equality in type theory is a complex topic and has been the subject of research, such as the field of homotopy type theory.[1]

Comparison with Judgemental Equality

The identity type is one of 2 different notions of equality in type theory.[2] The more fundamental notion is "judgemental equality", which is a judgement.

Beyond Judgemental Equality

The identity type can do more than what judgemental equality can do. It can be used to show "for all ", which is impossible to show with judgemental equality. This is accomplished by using the eliminator (or "recursor") of the natural numbers, known as "R".

The "R" function lets us define a new function on the natural numbers. That new function "P" is defined to be "(λ x:nat . x+1 = 1+x)". The other arguments act like the parts of an induction proof. The argument "PZ : P 0" becomes the base case "0+1 = 1+0", which is the term "refl nat 1". The argument "PS : P n → P (S n)" becomes the inductive case. Essentially, this says that when "x+1 = 1+x" has "x" replaced with a canonical value, the expression will be the same as "refl nat (x+1)".

Versions of the Identity Type

The identity type is complex and is the subject of research in type theory. While every version agrees on the constructor, "refl". Their properties and eliminator functions differ dramatically.

For "extensional" versions, any identity type can be converted into a judgemental equality. A computational version is known as "Axiom K" due to Thomas Streicher.[3] These are not very popular lately.

Complexity of Identity Type

Martin Hofmann and Thomas Streicher refuted the idea that type theory required all terms of the identity type to be the same.[4]

A popular branches of research into the identity type are homotopy type theory[5] and its cubical type theory.

References

  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. ^ Hofmann, Martin; Streicher, Thomas (July 1994). "The groupoid model refutes uniqueness of identity proofs". Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science. pp. 208–212. doi:10.1109/LICS.1994.316071. ISBN 0-8186-6310-3. S2CID 19496198.
  5. ^ Univalent Foundations Program (12 March 2013). Homotopy Type Theory. Institute for Advanced Study.

Content Disclaimer

Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.

  1. The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
  2. There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
  3. It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
  4. Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
  5. Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.