## Sheaf Semantics in Constructive Algebra and Type Theory

##### Abstract

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.

##### Parts of work

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.

##### Degree

Doctor of Philosophy

##### University

Göteborgs universitet. IT-fakulteten

##### Institution

Department of Computer Science and Engineering ; Institutionen för data- och informationsteknik

##### Disputation

10:00 EDIT building, Chalmers, room EA

##### Date of defence

2016-10-28

bassel.mannaa@gmail.com

##### Date

2016-10-06##### Author

Mannaa, Bassel

##### Keywords

Newton–Puiseux theorem

Algebraic curve

Sheaf model

Dynamic evaluation

Type theory

Markov’s Principle

Forcing

##### Publication type

Doctoral thesis

##### ISBN

978-91-628-9985-1 (Print)

978-91-628-9986-8 (PDF)

##### Series/Report no.

135D

##### Language

eng