2026-09-18T17:59:10Zhttps://gupea.ub.gu.se/server/oai/request

oai:gupea.ub.gu.se:2077/482502016-10-07T01:33:34Zcom_2077_18218com_2077_4716com_2077_10556col_2077_18219col_2077_10557

Mannaa, Bassel 2016-10-06T10:57:06Z 2016-10-06T10:57:06Z 2016-10-06 978-91-628-9985-1 (Print) 978-91-628-9986-8 (PDF) http://hdl.handle.net/2077/48250 In this thesis we present two applications of sheaf semantics. The first is to give constructive proof of Newton-Puiseux theorem. The second is to show the independence of Markov's principle from type theory. In the first part we study Newton-Puiseux algorithm from a constructive point of view. This is the algorithm used for computing the Puiseux expansions of a plane algebraic curve defined by an affine equation over an algebraically closed field. The termination of this algorithm is usually justified by non-constructive means. By adding a separability condition we obtain a variant of the algorithm, the termination of which is justified constructively in characteristic 0. To eliminate the assumption of an algebraically closed base field we present a constructive interpretation of the existence of the separable algebraic closure of a field by building, in a constructive metatheory, a suitable sheaf model where there is such separable algebraic closure. Consequently, one can use this interpretation to extract computational content from proofs involving this assumption. The theorem of Newton-Puiseux is one example. We then can find Puiseux expansions of an algebraic curve defined over a non-algebraically closed field K of characteristic 0. The expansions are given as a fractional power series over a finite dimensional K-algebra. In the second part we show that Markov's principle is independent from type theory. The underlying idea is that Markov's principle does not hold in the topos of sheaves over Cantor space. The presentation in this part is purely syntactical. We build an extension of type theory where the judgments are indexed by basic compact opens of Cantor space. We give an interpretation for this extension of type theory by way of computability predicate and relation. We can then show that Markov's principle is not derivable in this extension and consequently not derivable in type theory. eng 135D Mannaa, B. and Coquand, T. [2013], ‘Dynamic newton-puiseux theo- rem’, J. Logic & Analysis 5. Mannaa, B. and Coquand, T. [2014], A sheaf model of the algebraic closure, in P. Oliva, ed., ‘Proceedings Fifth International Workshop on Classical Logic and Computation, Vienna, Austria, July 13, 2014’, Vol. 164 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, pp. 18–32. Coquand, T. and Mannaa, B. [2016], The independence of markov’s principle in type theory, in ‘1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal’, pp. 17:1–17:18. Newton–Puiseux theorem Algebraic curve Sheaf model Dynamic evaluation Type theory Markov’s Principle Forcing Sheaf Semantics in Constructive Algebra and Type Theory Text Doctoral thesis Doctor of Philosophy bassel.mannaa@gmail.com Göteborgs universitet. IT-fakulteten Department of Computer Science and Engineering ; Institutionen för data- och informationsteknik 10:00 EDIT building, Chalmers, room EA 2016-10-28 ITF open.access