Sewon's Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Nondeterminism in constructive metric completeness ======

  * Michal Konečný (Aston University, UK), Sewon Park (KAIST, Korea), Holger Thies (Kyoto University, Japan)

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.

  * https://www.kms.or.kr/conference/abstract/search_view.html?num=7977&uid=74&start=0&sort=sortDate&period=74&cate=&etitle=&key_word=&au_name=&au_ename=Sewon%20park&au_office=&au_eoffice=&mode=search&section=