Axiomatic Reals and Certified Efficient Exact Real Computation

Michal Konečný; Sewon Park; Holger Thies

doi:10.1007/978-3-030-88853-4_16

Axiomatic Reals and Certified Efficient Exact Real Computation

Michal Konečný, Sewon Park, Holger Thies

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

Abstract

We introduce a new axiomatization of the constructive real numbers in a dependent type theory.
Our main motivation is to provide a sound and simple to use backend for verifying algorithms for exact real number computation and the extraction of efficient certified programs from our proofs.
We prove the soundness of our formalization with regards to the standard realizability interpretation from computable analysis.
We further show how to relate our theory to a classical formalization of the reals to allow certain non-computational parts of correctness proofs to be non-constructive.
We demonstrate the feasibility of our theory by implementing it in the Coq proof assistant and present several natural examples.
From the examples we can automatically extract Haskell programs that use the exact real computation framework AERN for efficiently performing exact operations on real numbers.
In experiments, the extracted programs behave similarly to native implementations in AERN in terms of running time.

Original language	English
Title of host publication	Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Proceedings
Subtitle of host publication	27th International Workshop, WoLLIC 2021
Editors	Alexandra Silva, Renata Wassermann, Ruy de Queiroz
Place of Publication	Berlin / Heidelberg
Publisher	Springer
Pages	252-268
Number of pages	17
Volume	13038
ISBN (Print)	978-3-030-88852-7
DOIs	https://doi.org/10.1007/978-3-030-88853-4_16
Publication status	Published - 17 Nov 2021
Event	27th International Workshop, WoLLIC 2021 - Duration: 5 Oct 2021 → 8 Oct 2021

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13038 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	27th International Workshop, WoLLIC 2021
Period	5/10/21 → 8/10/21

Bibliographical note

© Springer Nature B.V. 2021. The final publication is available at Springer via https://doi.org/10.1007/978-3-030-88853-4_16

Funding Information:
Holger Thies is supported by JSPS KAKENHI Grant Number JP20K19744. Sewon Park is supported by the National Research Foundation of Korea (NRF) grants funded by the Korea government (No. NRF-2016K1A3A7A03950702, NRF-2017R1E1A1A03071032 (MSIT) & No. NRF-2017R1D1A1B05031658 (MOE)).

Keywords

Constructive real numbers
Exact real number computation
Formal proofs
Program extraction

Access to Document

10.1007/978-3-030-88853-4_16

Axiomatic Reals and Certified Efficient Exact Real Computation
© Springer Nature B.V. 2021. The final publication is available at Springer via https://doi.org/10.1007/978-3-030-88853-4_16
Accepted author manuscript, 367 KB

Cite this

Konečný, M., Park, S., & Thies, H. (2021). Axiomatic Reals and Certified Efficient Exact Real Computation. In A. Silva, R. Wassermann, & R. de Queiroz (Eds.), Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Proceedings: 27th International Workshop, WoLLIC 2021 (Vol. 13038, pp. 252-268). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13038 LNCS). Springer. https://doi.org/10.1007/978-3-030-88853-4_16

Konečný, Michal ; Park, Sewon ; Thies, Holger. / Axiomatic Reals and Certified Efficient Exact Real Computation. Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Proceedings: 27th International Workshop, WoLLIC 2021. editor / Alexandra Silva ; Renata Wassermann ; Ruy de Queiroz. Vol. 13038 Berlin / Heidelberg : Springer, 2021. pp. 252-268 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{19e7688059234c6b8b85fb848035803a,

title = "Axiomatic Reals and Certified Efficient Exact Real Computation",

abstract = "We introduce a new axiomatization of the constructive real numbers in a dependent type theory.Our main motivation is to provide a sound and simple to use backend for verifying algorithms for exact real number computation and the extraction of efficient certified programs from our proofs.We prove the soundness of our formalization with regards to the standard realizability interpretation from computable analysis.We further show how to relate our theory to a classical formalization of the reals to allow certain non-computational parts of correctness proofs to be non-constructive.We demonstrate the feasibility of our theory by implementing it in the Coq proof assistant and present several natural examples.From the examples we can automatically extract Haskell programs that use the exact real computation framework AERN for efficiently performing exact operations on real numbers.In experiments, the extracted programs behave similarly to native implementations in AERN in terms of running time.",

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

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

note = "{\textcopyright} Springer Nature B.V. 2021. The final publication is available at Springer via https://doi.org/10.1007/978-3-030-88853-4_16 Funding Information: Holger Thies is supported by JSPS KAKENHI Grant Number JP20K19744. Sewon Park is supported by the National Research Foundation of Korea (NRF) grants funded by the Korea government (No. NRF-2016K1A3A7A03950702, NRF-2017R1E1A1A03071032 (MSIT) & No. NRF-2017R1D1A1B05031658 (MOE)). ; 27th International Workshop, WoLLIC 2021 ; Conference date: 05-10-2021 Through 08-10-2021",

year = "2021",

month = nov,

day = "17",

doi = "10.1007/978-3-030-88853-4_16",

language = "English",

isbn = "978-3-030-88852-7",

volume = "13038",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "252--268",

editor = "Alexandra Silva and Renata Wassermann and {de Queiroz}, Ruy",

booktitle = "Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Proceedings",

address = "Germany",

}

Konečný, M, Park, S & Thies, H 2021, Axiomatic Reals and Certified Efficient Exact Real Computation. in A Silva, R Wassermann & R de Queiroz (eds), Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Proceedings: 27th International Workshop, WoLLIC 2021. vol. 13038, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13038 LNCS, Springer, Berlin / Heidelberg, pp. 252-268, 27th International Workshop, WoLLIC 2021, 5/10/21. https://doi.org/10.1007/978-3-030-88853-4_16

Axiomatic Reals and Certified Efficient Exact Real Computation. / Konečný, Michal; Park, Sewon; Thies, Holger.
Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Proceedings: 27th International Workshop, WoLLIC 2021. ed. / Alexandra Silva; Renata Wassermann; Ruy de Queiroz. Vol. 13038 Berlin / Heidelberg: Springer, 2021. p. 252-268 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13038 LNCS).

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

TY - GEN

T1 - Axiomatic Reals and Certified Efficient Exact Real Computation

AU - Konečný, Michal

AU - Park, Sewon

AU - Thies, Holger

N1 - © Springer Nature B.V. 2021. The final publication is available at Springer via https://doi.org/10.1007/978-3-030-88853-4_16 Funding Information: Holger Thies is supported by JSPS KAKENHI Grant Number JP20K19744. Sewon Park is supported by the National Research Foundation of Korea (NRF) grants funded by the Korea government (No. NRF-2016K1A3A7A03950702, NRF-2017R1E1A1A03071032 (MSIT) & No. NRF-2017R1D1A1B05031658 (MOE)).

PY - 2021/11/17

Y1 - 2021/11/17

N2 - We introduce a new axiomatization of the constructive real numbers in a dependent type theory.Our main motivation is to provide a sound and simple to use backend for verifying algorithms for exact real number computation and the extraction of efficient certified programs from our proofs.We prove the soundness of our formalization with regards to the standard realizability interpretation from computable analysis.We further show how to relate our theory to a classical formalization of the reals to allow certain non-computational parts of correctness proofs to be non-constructive.We demonstrate the feasibility of our theory by implementing it in the Coq proof assistant and present several natural examples.From the examples we can automatically extract Haskell programs that use the exact real computation framework AERN for efficiently performing exact operations on real numbers.In experiments, the extracted programs behave similarly to native implementations in AERN in terms of running time.

AB - We introduce a new axiomatization of the constructive real numbers in a dependent type theory.Our main motivation is to provide a sound and simple to use backend for verifying algorithms for exact real number computation and the extraction of efficient certified programs from our proofs.We prove the soundness of our formalization with regards to the standard realizability interpretation from computable analysis.We further show how to relate our theory to a classical formalization of the reals to allow certain non-computational parts of correctness proofs to be non-constructive.We demonstrate the feasibility of our theory by implementing it in the Coq proof assistant and present several natural examples.From the examples we can automatically extract Haskell programs that use the exact real computation framework AERN for efficiently performing exact operations on real numbers.In experiments, the extracted programs behave similarly to native implementations in AERN in terms of running time.

KW - Constructive real numbers

KW - Exact real number computation

KW - Formal proofs

KW - Program extraction

UR - https://www.springer.com/gp/book/9783030888527

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

U2 - 10.1007/978-3-030-88853-4_16

DO - 10.1007/978-3-030-88853-4_16

M3 - Conference publication

SN - 978-3-030-88852-7

VL - 13038

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 252

EP - 268

BT - Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Proceedings

A2 - Silva, Alexandra

A2 - Wassermann, Renata

A2 - de Queiroz, Ruy

PB - Springer

CY - Berlin / Heidelberg

T2 - 27th International Workshop, WoLLIC 2021

Y2 - 5 October 2021 through 8 October 2021

ER -

Konečný M, Park S, Thies H. Axiomatic Reals and Certified Efficient Exact Real Computation. In Silva A, Wassermann R, de Queiroz R, editors, Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Proceedings: 27th International Workshop, WoLLIC 2021. Vol. 13038. Berlin / Heidelberg: Springer. 2021. p. 252-268. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2021 Oct 6. doi: 10.1007/978-3-030-88853-4_16

Axiomatic Reals and Certified Efficient Exact Real Computation

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this