Some formal proofs of isomorphy and discontinuity

Florian Steinberg (1) , Holger Thies (2)

1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
2 Kyushu University

In computable analysis a representation for a space X is a partial surjective mapping from the Baire space N N to X, i.e., a function δ : ⊆ N N → X. A pair X = (X, δ X) of a space and its representation is called a represented space and an element ϕ of Baire space is called name of x ∈ X if δ(ϕ) = x. Through a representation the notions of computability and continuity of operators on Baire space can be transfered to any represented space X. Popular topics in computable analysis are proving mathematical problems computable or, if this is impossible, classifying their degree of incomputability [BG11, BDBP12, PS18]. A problem that often appears in such classifications is closed choice, where the task is "given a non-empty closed set A ∈ A(X) select an element a ∈ A". Here, a closed subset of a represented space is given by specifying positive information about its complement. Thus, for most choices of X, this task is uncomputable and even discontinuous. More formally, A(X) is defined by use of the space of open subsets O(X), which in turn (following for instance [Pau16]) can abstractly be described as the space of continuous functions from X to the Sierpi´nskiSierpi´nski space S. Here, S has the two point set {⊥, } as underlying set and the total function δ S specified by δ S (ϕ) = ⇐⇒ ∃n ∈ N ϕ(n) = 0 as representation. The function space construction from computable analysis [Wei00, Definition 3.3.13] provides a representation [δ X → δ S ] of the continuous functions from X to S and we call the resulting represented space S X. Next, identify a subset U of X with its characteristic function χ U : X → S, χ U (x) := if x ∈ U, ⊥ otherwise. Conveniently, χ U is continuous if and only if U is open and therefore O(X) can be identified with S X. Finally, A(X) is represented as the complements of opens, i.e., following the above δ A(X) (ϕ) = A ⇐⇒ [δ X → δ S ](ϕ) = χ X\A. The task of closed choice on X is formalized as finding a realizer (in the sense of function realizabilty) of the multivalued function C X : ⊆ A(X) X defined by C X (A) := A. Or in words: a is an acceptable return value of C X on input A if and only if a is an element of A. Note that this in particular means that the domain of C X are the non-empty subsets of X and that a realizer can behave arbitrarily outside of the domain, i.e., no solution needs to be produced in this case. The function space construction is quite complicated and for concrete spaces it is often possible to use simpler representations. For instance, one may make use of the fact that there exist infinite products and indeed n∈N X is isomorphic to the function space X N .

Domaines: Informatique et langage [cs.CL]

Florian Steinberg, Holger Thies. Some formal proofs of isomorphy and discontinuity. MLA 2019 - Third Workshop on Mathematical Logic and its Applications, Mar 2019, Nancy, France. ⟨hal-02019174⟩