## Abstract

The computational content of constructive metric completeness is the operator that computes limits of Cauchy sequences. It can be used to 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. However, it is not obvious how nondeterministic metric completeness should be formalized.

We extend previous work on the formalization of exact real computation by primitive properties of nondeterminism. We show that by these properties, various forms of nondeterministic metric completeness can be derived without extending the axiomatic structure of constructive real numbers. We further implement our theory in the Coq proof assistant and use Coq’s code extraction features to extract efficient exact real computation programs using several forms of nondeterministic computation.

We extend previous work on the formalization of exact real computation by primitive properties of nondeterminism. We show that by these properties, various forms of nondeterministic metric completeness can be derived without extending the axiomatic structure of constructive real numbers. We further implement our theory in the Coq proof assistant and use Coq’s code extraction features to extract efficient exact real computation programs using several forms of nondeterministic computation.

Original language | English |
---|---|

Title of host publication | NASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings |

Subtitle of host publication | 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings |

Editors | Jyotirmoy V. Deshmukh, Klaus Havelund, Ivan Perez |

Publisher | Springer |

Pages | 771-789 |

Number of pages | 19 |

ISBN (Electronic) | 978-3-031-06773-0 |

ISBN (Print) | 978-3-031-06772-3 |

DOIs | |

Publication status | Published - 20 May 2022 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 13260 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

## Keywords

- Constructive real numbers
- Exact real number computation
- Formal proofs
- Nondeterminism
- Program extraction