Certified Computation of Nondeterministic Limits

Michal Konečný; Sewon Park; Holger Thies

doi:10.1007/978-3-031-06773-0_41

Certified Computation of Nondeterministic Limits

Michal Konečný, Sewon Park, Holger Thies

Research output: Chapter in Book/Published conference output › Conference publication

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.

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	https://doi.org/10.1007/978-3-031-06773-0_41
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

Access to Document

10.1007/978-3-031-06773-0_41

Cite this

Konečný, M., Park, S., & Thies, H. (2022). Certified Computation of Nondeterministic Limits. In J. V. Deshmukh, K. Havelund, & I. Perez (Eds.), NASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings (pp. 771-789). (Lecture Notes in Computer Science; Vol. 13260). Springer. https://doi.org/10.1007/978-3-031-06773-0_41

Konečný, Michal ; Park, Sewon ; Thies, Holger. / Certified Computation of Nondeterministic Limits. NASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings. editor / Jyotirmoy V. Deshmukh ; Klaus Havelund ; Ivan Perez. Springer, 2022. pp. 771-789 (Lecture Notes in Computer Science).

@inproceedings{9749b1f7cbf04f59a6623bcbf90789b1,

title = "Certified Computation of Nondeterministic Limits",

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{\textquoteright}s code extraction features to extract efficient exact real computation programs using several forms of nondeterministic computation.",

keywords = "Constructive real numbers, Exact real number computation, Formal proofs, Nondeterminism, Program extraction",

author = "Michal Kone{\v c}n{\'y} and Sewon Park and Holger Thies",

year = "2022",

month = may,

day = "20",

doi = "10.1007/978-3-031-06773-0_41",

language = "English",

isbn = "978-3-031-06772-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "771--789",

editor = "Deshmukh, {Jyotirmoy V.} and Klaus Havelund and Ivan Perez",

booktitle = "NASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings",

address = "Germany",

}

Konečný, M, Park, S & Thies, H 2022, Certified Computation of Nondeterministic Limits. in JV Deshmukh, K Havelund & I Perez (eds), NASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13260, Springer, pp. 771-789. https://doi.org/10.1007/978-3-031-06773-0_41

Certified Computation of Nondeterministic Limits. / Konečný, Michal; Park, Sewon; Thies, Holger.
NASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings. ed. / Jyotirmoy V. Deshmukh; Klaus Havelund; Ivan Perez. Springer, 2022. p. 771-789 (Lecture Notes in Computer Science; Vol. 13260).

Research output: Chapter in Book/Published conference output › Conference publication

TY - GEN

T1 - Certified Computation of Nondeterministic Limits

AU - Konečný, Michal

AU - Park, Sewon

AU - Thies, Holger

PY - 2022/5/20

Y1 - 2022/5/20

N2 - 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.

AB - 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.

KW - Constructive real numbers

KW - Exact real number computation

KW - Formal proofs

KW - Nondeterminism

KW - Program extraction

UR - http://www.scopus.com/inward/record.url?scp=85131150060&partnerID=8YFLogxK

UR - https://link.springer.com/chapter/10.1007/978-3-031-06773-0_41

U2 - 10.1007/978-3-031-06773-0_41

DO - 10.1007/978-3-031-06773-0_41

M3 - Conference publication

SN - 978-3-031-06772-3

T3 - Lecture Notes in Computer Science

SP - 771

EP - 789

BT - NASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings

A2 - Deshmukh, Jyotirmoy V.

A2 - Havelund, Klaus

A2 - Perez, Ivan

PB - Springer

ER -

Konečný M, Park S, Thies H. Certified Computation of Nondeterministic Limits. In Deshmukh JV, Havelund K, Perez I, editors, NASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings. Springer. 2022. p. 771-789. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-06773-0_41