컨텐츠 시작
학술대회/행사
초록검색
| 제출번호(No.) | 0163 |
|---|---|
| 분류(Section) | Special Session |
| 분과(Session) | (SS-02) Mathematical Logic and Its Applications (SS-02) |
| 영문제목 (Title(Eng.)) |
Multivalued functions in a dependent type theory |
| 저자(Author(s)) |
Andrej Bauer1, Philipp G. Haselwarter1, Sewon Park2, Egbert Rijke1 University of Ljubljana1, KAIST2 |
| 초록본문(Abstract) | We present a dependent type theory which faithfully expresses the multivalued functions from computable analysis, with the aid of a \emph{multi-value} monad $M$, such that the function type $A \to M B$ represents precisely the (computable) multivalued functions from $A$ to $B$. By applying the monad $M$ to dependent sums and coproducts we obtain the ability to express within type theory statements of the form “there exists …” and “A or B” in the sense of classical logic. Our type theory is dependent type theory with propositional truncation, extended with a type for classical propositions $\mathsf{cprop}$. We prove that $\mathsf{cprop}$ induces a construction which, assuming propositional extensionality, satisfies the universal property of double-negation sheafification. Thus, within our constructive type theory there is a universe of classical types. Using the double-negation sheafification and a small number of other principles, such as Markov principle, we may construct the classical real numbers, while the standard part of type theory can be used to construct the intuitionistic real numbers, as a subfield of the classical ones, as well as multi-valued operations known from computable analysis and exact real number computation. Our axiomatization has a realizability interpretation in the category of assemblies, through which the results in the type theory may be automatically translated to computable analysis. |
| 분류기호 (MSC number(s)) |
03F60 |
| 키워드(Keyword(s)) | Computable analysis, dependent type theory, realizability, categorical interpretation |
| 강연 형태 (Language of Session (Talk)) |
English |