Visa enkel post

dc.contributor.authorMannaa, Bassel
dc.date.accessioned2016-10-06T10:57:06Z
dc.date.available2016-10-06T10:57:06Z
dc.date.issued2016-10-06
dc.identifier.isbn978-91-628-9985-1 (Print)
dc.identifier.isbn978-91-628-9986-8 (PDF)
dc.identifier.urihttp://hdl.handle.net/2077/48250
dc.description.abstractIn 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.sv
dc.language.isoengsv
dc.relation.ispartofseries135Dsv
dc.relation.haspartMannaa, B. and Coquand, T. [2013], ‘Dynamic newton-puiseux theo- rem’, J. Logic & Analysis 5.sv
dc.relation.haspartMannaa, 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.sv
dc.relation.haspartCoquand, 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.sv
dc.subjectNewton–Puiseux theoremsv
dc.subjectAlgebraic curvesv
dc.subjectSheaf modelsv
dc.subjectDynamic evaluationsv
dc.subjectType theorysv
dc.subjectMarkov’s Principlesv
dc.subjectForcingsv
dc.titleSheaf Semantics in Constructive Algebra and Type Theorysv
dc.typeText
dc.type.svepDoctoral thesis
dc.gup.mailbassel.mannaa@gmail.comsv
dc.type.degreeDoctor of Philosophysv
dc.gup.originGöteborgs universitet. IT-fakultetensv
dc.gup.departmentDepartment of Computer Science and Engineering ; Institutionen för data- och informationstekniksv
dc.citation.doiITF
dc.gup.defenceplace10:00 EDIT building, Chalmers, room EAsv
dc.gup.defencedate2016-10-28


Filer under denna titel

Thumbnail
Thumbnail

Dokumentet tillhör följande samling(ar)

Visa enkel post