A universal algorithm for Krull's theorem
| Autor: | Thomas Powell, Franziskus Wiesnet, Peter Schuster |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: |
Krull's theorem
Program extraction Constructive algebra 0102 computer and information sciences 01 natural sciences Theoretical Computer Science Boolean prime ideal theorem Countable set 0101 mathematics Abstract algebra Valuation (algebra) Mathematics Lemma (mathematics) Recursion Maximal ideals Mathematics::Commutative Algebra 010102 general mathematics Computer Science Applications TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics 010201 computation theory & mathematics Proof theory Krull's theorem Maximal ideals Program extraction Constructive algebra Algorithm Information Systems |
| Zdroj: | Powell, T, Schuster, P & Wiesnet, F 2022, ' A universal algorithm for Krull's theorem ', Information and Computation, vol. 287, 104761 . https://doi.org/10.1016/j.ic.2021.104761 |
| DOI: | 10.1016/j.ic.2021.104761 |
| Popis: | We give a computational interpretation to an abstract formulation of Krull's theorem, by analysing its classical proof based on Zorn's lemma. Our approach is inspired by proof theory, and uses a form of update recursion to replace the existence of maximal ideals. Our main result allows us to derive, in a uniform way, algorithms which compute witnesses for existential theorems in countable abstract algebra. We give a number of concrete examples of this phenomenon, including the prime ideal theorem and Krull's theorem on valuation rings. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|