A universal algorithm for Krull's theorem

被引：2

作者：

Powell, Thomas ^{[1
]}

Schuster, Peter ^{[2
]}

Wiesnet, Franziskus ^{[2
,3
,4
]}

机构：

[1] Univ Bath, Dept Comp Sci, Bath BA2 7AY, Avon, England

[2] Univ Verona, Dept Comp Sci, Str Grazie 15, I-37134 Verona, Italy

[3] Univ Trento, Dept Math, Via Sommarive 14, I-38123 Povo, Italy

[4] Ludwig Maximilians Univ Munchen, Dept Math, Theresienstr 39, D-80333 Munich, Germany

来源：

INFORMATION AND COMPUTATION | 2022年 / 287卷

关键词：

Krull's theorem; Maximal ideals; Program extraction; Constructive algebra; ELIMINATING DISJUNCTIONS; CUT ELIMINATION; BAR RECURSION; ALGEBRA; SYSTEMS;

D O I：

10.1016/j.ic.2021.104761

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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. (C) 2021 Elsevier Inc. All rights reserved.

引用

页数：21

共 63 条

[1] INTERACTIVE LEARNING-BASED REALIZABILITY FOR HEYTING ARITHMETIC WITH EM1 [J].

Aschieri, Federico ;

Berardi, Stefano .

LOGICAL METHODS IN COMPUTER SCIENCE, 2010, 6 (03)

[2] Polynomials and radical ideals [J].

Banaschewski, B ;

Vermeulen, JJC .

JOURNAL OF PURE AND APPLIED ALGEBRA, 1996, 113 (03) :219-227

[3] A computational interpretation of open induction [J].

Berger, U .

19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, :326-334

[4] A Randomized Trial of Intraarterial Treatment for Acute Ischemic Stroke [J].

Berkhemer, O. A. ;

Fransen, P. S. S. ;

Beumer, D. ;

van den Berg, L. A. ;

Lingsma, H. F. ;

Yoo, A. J. ;

Schonewille, W. J. ;

Vos, J. A. ;

Nederkoorn, P. J. ;

Wermer, M. J. H. ;

van Walderveen, M. A. A. ;

Staals, J. ;

Hofmeijer, J. ;

van Oostayen, J. A. ;

Nijeholt, G. J. Lycklama A. ;

Boiten, J. ;

Brouwer, P. A. ;

Emmer, B. J. ;

de Bruijn, S. F. ;

van Dijk, L. C. ;

Kappelle, L. J. ;

Lo, R. H. ;

Van Dijk, E. J. ;

de Vries, J. ;

de Kort, P. L. M. ;

van Rooij, W. J. J. ;

van den Berg, J. S. P. ;

van Hasselt, B. A. A. M. ;

Aerden, L. A. M. ;

Dallinga, R. J. ;

Visser, M. C. ;

Bot, J. C. J. ;

Vroomen, P. C. ;

Eshghi, O. ;

Schreuder, T. H. C. M. L. ;

Heijboer, R. J. J. ;

Keizer, K. ;

Tielbeek, A. V. ;

den Hertog, H. M. ;

Gerrits, D. G. ;

van den Berg-Vos, R. M. ;

Karas, G. B. ;

Steyerberg, E. W. ;

Flach, H. Z. ;

Marquering, H. A. ;

Sprengers, M. E. S. ;

Jenniskens, S. F. M. ;

Beenen, L. F. M. ;

van den Berg, R. ;

Koudstaal, P. J. .

NEW ENGLAND JOURNAL OF MEDICINE, 2015, 372 (01) :11-20

[5]

Cederquist J, 2000, LECT NOTES LOGIC, V13, P127

[6] Valuations and Dedekind's Prague theorem [J].

Coquand, T ;

Persson, H .

JOURNAL OF PURE AND APPLIED ALGEBRA, 2001, 155 (2-3) :121-129

[7]

Coquand T., 2003, Revue des Mathematiques de lenseignement Superieur, V113, P25

[8] A logical approach to abstract algebra [J].

Coquand, Thierry ;

Lombardi, Henri .

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2006, 16 (05) :885-900

[9] LATTICE-ORDERED GROUPS GENERATED BY AN ORDERED GROUP AND REGULAR SYSTEMS OF IDEALS [J].

Coquand, Thierry ;

Lombardi, Henri ;

Neuwirth, Stefan .

ROCKY MOUNTAIN JOURNAL OF MATHEMATICS, 2019, 49 (05) :1449-1489

[10] Space of valuations [J].

Coquand, Thierry .

ANNALS OF PURE AND APPLIED LOGIC, 2009, 157 (2-3) :97-109

← 1 2 3 4 5 6 7 →