컨텐츠 시작
학술대회/행사
초록검색
| 제출번호(No.) | 0087 |
|---|---|
| 분류(Section) | Special Session |
| 분과(Session) | (SS-04) Mathematical Logic and Its Applications (SS-04) |
| 영문제목 (Title(Eng.)) |
Nondeterminism in constructive metric completeness |
| 저자(Author(s)) |
Michal Konečný1, Sewon Park2, Holger Thies3 Aston University, UK1, KAIST, Korea2, Kyoto University, Japan3 |
| 초록본문(Abstract) | The computational content of constructive metric completeness is the operator that computes limits of Cauchy sequences. Using it, we can construct certified programs that compute interesting transcendental real numbers from sequences of approximations. The desired nondeterministic version of it would be to nondeterministically compute real numbers from nondeterministic approximations. An example is to compute a square root (nondeterministically picked amongst the multiple square roots) of a complex number by nondeterministic approximations. However, it is not obvious how this nondeterministic metric completeness can be and should be formalized. In this talk, we specify some primitive properties of the nondeterminism monad in the category of assemblies over Kleene's second algebra. It can be used together with ordinary metric completeness to realize nondeterministic metric completeness. We suggest that there is no need to extend the axiomatic structure of constructive real numbers in order to have nondeterministic metric completeness. |
| 분류기호 (MSC number(s)) |
03F60 |
| 키워드(Keyword(s)) | computable analysis, axiomatic real numbers, nondeterminism, categorical interpretation, realizability |
| 강연 형태 (Language of Session (Talk)) |
English |