TY - GEN

T1 - Continuous and monotone machines

AU - Konečný, Michal

AU - Steinberg, Florian

AU - Thies, Holger

PY - 2020/8/1

Y1 - 2020/8/1

N2 - We investigate a variant of the fuel-based approach to modeling diverging computation in type theories and use it to abstractly capture the essence of oracle Turing machines. The resulting objects we call continuous machines. We prove that it is possible to translate back and forth between such machines and names in the standard function encoding used in computable analysis. Put differently, among the operators on Baire space, exactly the partial continuous ones are implementable by continuous machines and the data that such a machine provides is a description of the operator as a sequentially realizable functional. Continuous machines are naturally formulated in type theories and we have formalized our findings in Coq as part of Incone, a Coq library for computable analysis. The correctness proofs use a classical meta-theory with countable choice. Along the way we formally prove some known results such as the existence of a self-modulating modulus of continuity for partial continuous operators on Baire space. To illustrate their versatility we use continuous machines to specify some algorithms that operate on objects that cannot be fully described by finite means, such as real numbers and functions. We present particularly simple algorithms for finding the multiplicative inverse of a real number and for composition of partial continuous operators on Baire space. Some of the simplicity is achieved by utilizing the fact that continuous machines are compatible with multivalued semantics.

AB - We investigate a variant of the fuel-based approach to modeling diverging computation in type theories and use it to abstractly capture the essence of oracle Turing machines. The resulting objects we call continuous machines. We prove that it is possible to translate back and forth between such machines and names in the standard function encoding used in computable analysis. Put differently, among the operators on Baire space, exactly the partial continuous ones are implementable by continuous machines and the data that such a machine provides is a description of the operator as a sequentially realizable functional. Continuous machines are naturally formulated in type theories and we have formalized our findings in Coq as part of Incone, a Coq library for computable analysis. The correctness proofs use a classical meta-theory with countable choice. Along the way we formally prove some known results such as the existence of a self-modulating modulus of continuity for partial continuous operators on Baire space. To illustrate their versatility we use continuous machines to specify some algorithms that operate on objects that cannot be fully described by finite means, such as real numbers and functions. We present particularly simple algorithms for finding the multiplicative inverse of a real number and for composition of partial continuous operators on Baire space. Some of the simplicity is achieved by utilizing the fact that continuous machines are compatible with multivalued semantics.

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

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

U2 - 10.4230/LIPIcs.MFCS.2020.56

DO - 10.4230/LIPIcs.MFCS.2020.56

M3 - Conference contribution

AN - SCOPUS:85090508781

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020

A2 - Esparza, Javier

A2 - Kral�, Daniel

A2 - Kral�, Daniel

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020

Y2 - 25 August 2020 through 26 August 2020

ER -