###### Abstract

Working in a semi-constructive logical system that supports the extraction of
concurrent programs, we extract a program inverting non-singular real valued
matrices from a constructive proof based on Gaussian elimination. Concurrency
is used for efficient pivoting, that is, for finding an entry that is apart
from zero in a non-null vector of real numbers.

##  Chapter 0 Concurrent Gaussian elimination

###  1 Introduction

A salient feature of constructive mathematics[1, 2, 3], which attracts
mathematicians, logicians, philosophers, and computer scientists,
independently of their foundational position, is the fact that its notions are
computationally meaningful and its proofs give rise to concrete realizations
of computations, that is, programs. Manifestations of this ability to ‘extract
programs’ can be found, for example, in constructive type theories, functional
interpretation and theories of realizability. Using computer implementations
of constructive type theory, such as Nuprl [4], Coq [5] and Agda[6], or
systems supporting realizability, such as Isabelle/HOL [7], and Minlog [8],
substantial case studies have been undertaken that demonstrate the usefulness
and scalability of program extraction.

The exploration of the scope and limits of program extraction is an active
field of research that has led to many interesting results regarding the
partial inclusion of classical logic [9, 10, 11] and mathematical principles
such as various forms of choice [12, 13, 14, 15, 16] and induction principles
[15, 17, 18, 19]. The benefit of program extraction is not only that extracted
programs come automatically with formal correctness proofs but also that
important additional properties of programs concerning computational
complexity, totality and typability can be obtained.

An important paradigm in modern computing technology, that has only recently
been connected with program extraction, is _concurrency_ , that is, the
ability to run several ‘threads’ of computations independently and
asynchronously but allowing them to interact in a number of ways. Concurrency
poses big challenges to computer science, since, on the one hand, it is
indispensable for running computer systems efficiently on a range of different
tasks simultaneously, on the other hand the (often nondeterministic) behaviour
of such systems is very difficult to control.

In[20], a semi-constructive logical system ($\mathrm{CFP}$, Concurrent Fixed
Point Logic) for the extraction of concurrent programs was introduced and
applied to extract a program that converts between two different exact
representations of real numbers. Concurrency was needed to avoid non-
termination when dealing with potentially partial inputs (infinite Gray code
[21]). In the present paper, we apply $\mathrm{CFP}$ to another problem in
computable analysis, the inversion of real valued matrices. Here, not non-
termination is the issue, but the potential gain in efficiency through
concurrent computation. In both applications the interaction between
concurrent threads is limited to winning a race: The result of the thread
terminating first will be selected and the other killed. Nevertheless,
controlling this form of concurrency at the logical level poses serious
challenges.

The paper is organized as follows: In Sec. 2 we introduce the main elements of
the system $\mathrm{IFP}$ [18] our method of program extraction is based on,
and in Sec. 3 we instantiate $\mathrm{IFP}$ to the setting of real numbers. In
Sec. 4 we present the system $\mathrm{CFP}$ that extends $\mathrm{IFP}$ by
logical operators permitting the extraction of concurrent programs. To be able
to carry out our case study, we adjust $\mathrm{CFP}$ to allow for more than
two concurrent threads and iterated ‘monadic’ concurrency. Finally, Sec. 5
presents the proof of matrix inversion through Gaussian elimination where
pivoting, that is selecting a nonzero entry in a nonzero vector, is done
concurrently.

###  2 Intuitionistic fixed point logic

Our basic logical system for program extraction is $\mathrm{IFP}$, which is
based on many-sorted intuitionistic first-order logic with equality and least
and greatest fixed points. A detailed definition of its syntax, semantics and
proof calculus, as well as applications to program extraction can be found in
[18]. We highlight the most important points.

The _syntax_ of $\mathrm{IFP}$ is parametric in a set of sorts (which we
usually suppress), a set of constants and function symbols, and a set of
predicate constants (all with fixed arities). _Formulas_ $A,B$, _predicates_
$P,Q$, and _operators_ $\Phi,\Psi$ are defined simultaneously:

_Formulas_ are $\bot,\top$ (falsity and truth), $s=t$ where $s,t$ are first-
order terms of the same sort, $P(\vec{t})$ where $\vec{t}$ is a tuple of
first-order terms whose length is the arity of the predicate $P$, $A\land B$,
$A\lor B$, $A\to B$, and $\forall x\,A$, $\exists x\,A$ where $x$ is a first-
order variable of a fixed sort.

_Predicates_ are predicate variables, predicate constants, both of fixed
arities, $\lambda\vec{x}\,A$ (abstraction) where $\vec{x}$ is a tuple of
first-order variables and $\mu\,\Phi$, $\nu\,\Phi$. The common arity of the
latter two constructs is the arity of the operator $\Phi$.

_Operators_ are of the form $\lambda X\,P$ where $X$ is a predicate variable
of the same arity as $P$ which occurs freely in $P$ only at strictly positive
positions, that is, not in the left part of an implication. The arity of
$\lambda X\,P$ is the common arity of $X$ and $P$.

The application, $\Phi(Q)$, of an operator $\Phi=\lambda X\,P$ to a predicate
$Q$ of the same arity is defined as $P[Q/X]$. A definition
$P\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\mu\Phi$ will also be written as
$P\stackrel{{\scriptstyle\mu}}{{=}}\Phi(P)$. The notation
$P\stackrel{{\scriptstyle\nu}}{{=}}\Phi(P)$ has a similar meaning. If
$\Phi=\lambda X\lambda\vec{x}\,A$, then we also write
$P(\vec{x})\stackrel{{\scriptstyle\mu}}{{=}}A[P/X]$ and
$P(\vec{x})\stackrel{{\scriptstyle\nu}}{{=}}A[P/X]$ instead of
$P\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\mu\Phi$ and
$P\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\nu\Phi$. We furthermore use the
set-theoretic notations $P\subseteq Q$ for $\forall x\,(P(x)\to Q(x))$ and
$P\cap Q$ for $\lambda x\,(P(x)\land Q(x))$, as well as the bounded
quantifiers $\forall x\in P\,A$ and $\exists x\in P\,A$ for $\forall
x\,(P(x)\to A)$ and $\exists x\,(P(x)\land A)$. In Sects. 4 and 5 we will also
use finitely iterated conjunctions and disjunctions which we define as

$\displaystyle\bigvee_{1\leq i\leq n}A(i)$
$\displaystyle\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}$ $\displaystyle
A_{1}\land(A_{2}\land\ldots(A_{n}\land\top)\ldots)$
$\displaystyle\bigwedge_{1\leq i\leq n}A(i)$
$\displaystyle\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}$ $\displaystyle
A_{1}\lor(A_{2}\lor\ldots(A_{n}\lor\bot)\ldots).$

The _semantics_ of $\mathrm{IFP}$ has a classical and a constructive part.

The _classical semantics_ is as usual for classical first-order predicate
logic, that is, sorts are interpreted as sets (called carrier sets), function
symbols as (set-theoretic) functions, and predicate constants as subsets of
the corresponding cartesian products of carrier sets. Operators are
interpreted as monotone predicate transformers and the predicates $\mu\,\Phi$
and $\nu\,\Phi$ as their least and greatest fixed point, also called inductive
and coinductive definitions. No assumptions of computability or constructivity
are made at this point.

The _constructive semantics_ consist of a realizability interpretation of
formulas and (co)inductive predicates. The space of potential realizers is an
effective Scott-domain [22], $D$, defined by the recursive domain equation

$D=(\mathbf{Nil}+\mathbf{Left}(D)+\mathbf{Right}(D)+\mathbf{Pair}(D\times
D)+\mathbf{Fun}(D\to D))_{\bot}$ (1)

This means that $D$ is the disjoint union of the components labelled by the
constructors $\mathbf{Nil},\mathbf{Left},\ldots$. $D$ contains its own
function space, $(D\to D)$, which would not be possible, set-theoretically,
but is a standard construction in domain theory, since $(D\to D)$ consists of
continuous functions only. Continuity refers to the Scott topology which is
generated by a partial order $\sqsubseteq$ on $D$ which has $\bot$ as its
least element (representing ‘undefined’). Thanks to the function space
component, $D$ carries the structure of a PCA (partial combinatory algebra)
and can therefore interpret simple recursive types defined by the grammar

$\rho,\sigma::=\alpha\mid\mathbf{1}\mid\rho\times\sigma\mid\rho+\sigma\mid\rho\Rightarrow\sigma\mid\mathbf{fix}\,\alpha\,.\,\rho$
(2)

where $\alpha$ ranges over type variables and in
$\mathbf{fix}\,\alpha\,.\,\rho$, $\rho$ must be strictly positive in $\alpha$.
Hence, every type $\rho$ denotes a subdomain $D(\rho)$. To define the
semantics of a formula $A$ we first define a type $\tau(A)$ that represents
the ‘propositional skeleton’ of $A$. Then the semantics of $A$ is defined as a
set $\mathbf{R}(A)\subseteq D(\tau(A))$ of realizers of $A$, essentially
following Kleene [23] and Kreisel [24] but, if possible, simplifying realizers
in order to avoid junk in extracted programs. We will usually write
‘$a\,\mathbf{r}\,A$’ (‘$a$ realizes $A$’) for ‘$a\in\mathbf{R}(A)$’ and omit
the type information about $a$. For the simplification of realizers, _Harrop
formulas_ play a special role. These are formulas that do not contain
disjunctions or free predicate variables at strictly positive positions. For
example, $\bot$, equations and formulas of the form every $P(\vec{t})$ where
$P$ is a predicate constant are Harrop, and so is every negated formula since
we view negation as implication to falsity. The realizability interpretation
of an implication $A\to B$ where $A$ and $B$ are both non-Harrop is, as
expected,

$c\,\mathbf{r}\,(A\to B)\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\forall
a\,(a\,\mathbf{r}\,A\to(c\,a)\,\mathbf{r}\,B)$

while if $A$ is Harrop it is

$b\,\mathbf{r}\,(A\to
B)\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\mathbf{H}(A)\to
b\,\mathbf{r}\,B\,.$

Here $\mathbf{H}(A)$ means $\exists a\,(a\,\mathbf{r}\,A)$ or, equivalently
$\mathbf{Nil}\,\mathbf{r}\,A$ since, for Harrop formulas, $\mathbf{Nil}$ (an
element of $D$ signalling trivial computational content) is the only possible
realizer. An even more restricted class of formulas are _non-computational
(nc)_ formulas which do not contain free predicate variables or disjunctions
at all. These formulas coincide with their realizability interpretation, that
is, $\mathbf{H}(A)$ is identical to $A$ for nc formulas $A$. Since first-order
variables may range over abstract objects without computable structure,
quantifiers have to be interpreted uniformly, that is,

$\displaystyle a\,\mathbf{r}\,\forall x\,A(x)$
$\displaystyle\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}$
$\displaystyle\forall x\,(a\,\mathbf{r}\,A(x))$ $\displaystyle
a\,\mathbf{r}\,\exists x\,A(x)$
$\displaystyle\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}$
$\displaystyle\exists x\,(a\,\mathbf{r}\,A(x))\,.$

Hence, the realizer of a universal formula does not depend on the quantified
variable, and the realizer of an existential formula does not carry a witness.

The realizability interpretation of a least or greatest fixed point is the
least or greatest fixed point of the realizability interpretation of the
corresponding operator. For example, in the presence of a constant $0$ and a
successor function $(+1)$ we can define the natural numbers as the least
predicate containing $0$ and being closed under $(+1)$,

$\mathbf{N}(x)\stackrel{{\scriptstyle\mu}}{{=}}x=0\lor\exists\,y\,(x=y+1\land\mathbf{N}(y))$
(3)

The realizability interpretation of $\mathbf{N}$ is

$\begin{array}[]{l}n\,\mathbf{r}\,\mathbf{N}(x)\
\stackrel{{\scriptstyle\mu}}{{=}}\ (n=\mathbf{Left}(\mathbf{Nil})\land x=0)\
\lor\\\ \hskip 57.00005pt(n=\mathbf{Right}(m)\land\exists
y\,(m\,\mathbf{r}\,\mathbf{N}(y)\land x=y+1))\end{array}$ (4)

Therefore, $n\,\mathbf{r}\,\mathbf{N}(x)$ means that $x$ is a natural number
and $n$ is the unary representation of $x$ where zero and successor are
modelled by $\mathbf{Left}(\mathbf{Nil})$ and $\mathbf{Right}(\\_)$. Examples
of coinductive definitions will be given in Sect. 3.

The guiding principle for the _proof rules_ of $\mathrm{IFP}$ is that they
must be sound for the classical and the constructive semantics. This is
achieved through the usual rules for intuitionistic logic, and rules
expressing the least resp. greatest fixed point property of $\mu\,\Phi$ resp.
$\nu\,\Phi$. For the natural numbers these are equivalent to the closure under
$0$ and successor and the usual induction rule that infers, for an arbitrary
predicate $P$, from $P(0)$ and $\forall x\,(P(x)\to P(x+1))$ that
$\mathbf{N}\subseteq P$, that is, $\forall x\,(\mathbf{N}(x)\to P(x))$.

Regarding _axioms_ one has a fair amount of flexibility. Any closed formula
$A$ that is true in the intended classical interpretation and for which one
has a program $M$ that realizes it can be taken as an axiom. In particular
every classically true nc formula can be taken as an axiom. More generally,
any closed Harrop formula that is equivalent to its realizability
interpretation, may be taken as an axiom if we accept it as true in the
intended interpretation. A large class of formulas enjoying this property is
the class of _admissible Harrop formulas_ , which is the least class that
contains all nc formulas, is closed under conjunction and quantification and
under implication, $A\to B$ where $B$ is admissibly Harrop and the formula $A$
is equivalent to its realizability interpretation (for example, that is the
case if $A$ is of the form $\mathbf{N}(t)$). An important and useful axiom is
a generalization of _Brouwer’s thesis_ [25] which can be stated as the
following nc formula

$\mathbf{BT}\qquad\forall
x\,(\neg\mathbf{Path}_{\prec}(x)\to\mathbf{Acc}_{\prec}(x))\,.$ (5)

This refers to some nc relation $\prec$ and relates two ways of expressing
that an element $x$ is wellfounded with respect to $\prec$: The first way,
$\neg\mathbf{Path}_{\prec}(x)$, says that there is no descending path starting
with $x$ where the existence of a path can be expressed coinductively as

$\mathbf{Path}_{\prec}(x)\stackrel{{\scriptstyle\nu}}{{=}}\exists y\prec
x\,\mathbf{Path}_{\prec}(y)\,.$ (6)

The second way, $\mathbf{Acc}_{\prec}(x)$, expresses wellfoundedness
inductively as the accessible part of $\prec$:

$\mathbf{Acc}_{\prec}(x)\stackrel{{\scriptstyle\mu}}{{=}}\forall y\prec
x\,\mathbf{Acc}_{\prec}(y)$ (7)

$\mathbf{BT}$ is stronger and more general than Brouwer’s original thesis. The
precise relationship is explained in [18]. As an example we show:

###### Lemma 1

Brouwer’s thesis, (5), implies Markov’s Principle, that is, the schema

$\forall x\in\mathbf{N}(A(x)\lor\neg A(x))\land\neg\neg\exists
x\in\mathbf{N}\,A(x)\to\exists x\in\mathbf{N}\,A(x)\,.$ (8)

######  Proof 2.1.

To prove (8) set $y\prec
x\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}y=x+1\land\neg A(x)$. Then,
clearly, $\neg\neg\exists x\in\mathbf{N}\,A(x)$ implies
$\neg\mathbf{Path}_{\prec}(0)$ (if $\mathbf{Path}_{\prec}(0)$, then $\forall
x\in\mathbf{N}\,\mathbf{Path}_{\prec}(x)$ follows by induction on
$x\in\mathbf{N}$, hence $\forall x\in\mathbf{N}\neg A(x)$). Therefore, by (5),
$\mathbf{Acc}_{\prec}(0)$. We set
$P(x)\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}x\in\mathbf{N}\to\exists
y\in\mathbf{N}\,A(y)$, with the goal to prove $\mathbf{Acc}_{\prec}\subseteq
P$, by wellfounded induction on $\prec$, that is, strictly positive induction
on $\mathbf{Acc}_{\prec}$. Therefore, we assume, as induction hypothesis,
$\forall y\prec x\,P(y)$, and have to show $P(x)$. Hence let $x\in\mathbf{N}$.
Since $A$ is assumed to be decidable, we can do case analysis on $A(x)$. If
$A(x)$ holds, then we are done. Otherwise, $x+1\prec x$ and therefore $P(x+1)$
holds by the induction hypothesis. Since $x+1\in\mathbf{N}$, it follows
$\exists y\in\mathbf{N}\,A(y)$, thus completing the inductive proof of
$\mathbf{Acc}_{\prec}\subseteq P$. Hence $P(0)$ which means $\exists
x\in\mathbf{N}\,A(x)$.

Since Markov’s Principle, and hence $\mathbf{BT}$, is not generally accepted
in constructive mathematics, we will mark uses of $\mathbf{BT}$ in the
following.

_Program extraction_ is based on the soundness theorem for the constructive
semantics:

######  Theorem 2.2 (Soundness).

From an $\mathrm{IFP}$ proof of a formula $A$ one can extract a closed program
$M:\tau(A)$ such that $M\,\mathbf{r}\,A$ is provable.

A detailed proof can be found in [18].

The realizers extracted from proofs are given as programs in a simple
functional programming language, that is, an enriched lambda calculus given by
the grammar

$\displaystyle M,N,L::=a,b,c\ \ \text{(variables)}$ $\displaystyle\quad|\
\lambda a.\,M\ |\ M\,N\ |\ \mathbf{rec}\,M\ |\ \bot$ $\displaystyle\quad|\
\mathbf{Nil}\ |\ \mathbf{Left}(M)\ |\ \mathbf{Right}(M)\ |\
\mathbf{Pair}(M,N)$ $\displaystyle\quad|\ \mathbf{case}\,M\,\mathbf{of}\,\\{\
Cl_{1},\ldots,Cl_{n}\\}$

The $Cl_{i}$ are clauses of the form $C(a_{1},\ldots,a_{k})\to N$ where $C$ is
a constructor
($\in\\{\mathbf{Nil},\mathbf{Left},\mathbf{Right},\mathbf{Pair}\\}$). A
program $\mathbf{rec}\,M$ denotes the least fixed point of the function
defined by $M$. Details of the denotational semantics of programs can be found
in [18]. There, also a matching operational semantics is given.

A system similar to $\mathrm{IFP}$ is $\mathrm{TCF}$ (Theory of Computable
Functionals), which is the formal system underlying the interactive proof
system Minlog [26, 8]. A comprehensive account of $\mathrm{TCF}$ and examples
of program extraction in Minlog can be found in [26]. The main difference
between $\mathrm{IFP}$ and $\mathrm{TCF}$ is that while $\mathrm{IFP}$
concentrates on the integration of abstract and constructive mathematics, the
focus in $\mathrm{TCF}$ is on higher type computable functionals as a standard
model.

In the following, if we say of a formula that it “holds” or “implies” another
formula we always mean that the corresponding formulas are provable in the
formal system in question, which will be $\mathrm{IFP}$ in the next two
sections, and its concurrent variant, $\mathrm{CFP}$, thereafter.

###  3 Real numbers

We consider an instance of $\mathrm{IFP}$ with a sort $\iota$ for real
numbers, the constants $0$ and $1$ and function symbols for addition
subtraction, multiplication, division, and absolute value, as well as relation
constants $<$ and $\leq$. Furthermore, we assume the axioms of a real closed
field as a set of nc formulas, as well as the _Archimedean axiom_ that says
that there are no infinite numbers, that is, by repeatedly subtracting $1$ any
real number will eventually become negative. Setting $y\prec x\
\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\ 0\leq y\ \land\ y=x-1$, this can
be expressed as the nc formula

$\forall x\,\neg\mathbf{Path}_{\prec}(x)\,.$ (9)

Hence, real numbers are given abstractly and axiomatically. In particular, no
programs for computing the field operations are available. However, we can use
(3) to define the natural numbers as a subset $\mathbf{N}$ of the reals and
prove, for example, that they are closed under addition,

$\forall x,y\,(\mathbf{N}(x)\land\mathbf{N}(y)\to\mathbf{N}(x+y))\,.$ (10)

The extracted program will add (unary representations of) natural numbers. To
extract programs for (exact) real number computation, we need to be able to
approximate real numbers by rational numbers. Therefore we define the
predicate

$\mathbf{C}(x)\ \stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\ \forall
n\in\mathbf{N}\,\exists q\in\mathbf{Q}\,|x-q|\leq 2^{-n}$ (11)

where $\mathbf{Q}$ is a predicate characterising the rational numbers, for
example,

$\mathbf{Q}(x)\ \stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\ \exists
y,z,u\in\mathbf{N}\ x=\frac{y-z}{u+1}\,.$ (12)

We call a real number $x$ satisfying $\mathbf{C}(x)$ _constructive_. A
realizer of $\mathbf{C}(x)$ is a fast Cauchy sequence, that is, a sequence $f$
of rational numbers converging quickly to $x$:

$f\,\mathbf{r}\,\mathbf{C}(x)\ \leftrightarrow\ \forall
n\in\mathbf{N}\,|x-f(n)|\leq 2^{-n}\,.$ (13)

The realizers of $\mathbf{C}(x)$ are sequences of rational numbers implemented
as _functions_ from the natural numbers to the rationals. To obtain as
realizers sequences that are implemented as infinite _streams_ , one can use
the following coinductive predicate:

$\mathbf{C^{\prime}}(x)\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\mathbf{C^{\prime}}(x,0)\hbox{,
where }\ \mathbf{C^{\prime}}(x,n)\stackrel{{\scriptstyle\nu}}{{=}}\exists
q\in\mathbf{Q}|x-q|\leq 2^{-n}\land\mathbf{C^{\prime}}(x,n+1)$ (14)

Then a realizer of $\mathbf{C^{\prime}}(x)$ is an infinite stream of rationals
$q_{0}:q_{1}:\ldots$ such that $|x-q_{n}|\leq 2^{-n}$ for all $n$. It is easy
to prove that the predicates $\mathbf{C}$ and $\mathbf{C^{\prime}}$ are
equivalent. From the proof of this equivalence one can extract programs that
translate between the function and the stream representation of Cauchy
sequences.

In [18] it is shown that $\mathbf{C}$ is also equivalent to the coinductive
predicate

$\mathbf{S}(x)\stackrel{{\scriptstyle\nu}}{{=}}\exists
d\in\\{-1,0,1\\}\,(|d/2-x|\leq 1/2\wedge\mathbf{S}(2x-d))\,.$ (15)

A realizer of $\mathbf{S}(x)$ is a signed digit representations of $x$. The
programs extracted from the proof of the equivalence of $\mathbf{C}$ and
$\mathbf{S}$ provide translations between the Cauchy and the signed digit
representations. The coinductive characterization of the signed digit
representation has been generalized to continuous functions [27] and compact
sets [28] and corresponding translations have been extracted.

A predicate of arity $(\iota)$ is called a _ring_ if it contains $0$ and $1$
and is closed under addition, subtraction and multiplication. A ring that is
closed under division by elements that are apart from $0$ is called a _field_
, where the _apartness relation_ between real numbers is defined as

$x\,\,{\not\,\not=}\,\,y\ \stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\ \exists
k\in\mathbf{N}\,|x-y|\geq 2^{-k}$ (16)

Note that, in our setting, rings and fields are automatically ordered and
satisfy the Archimedean axiom (9). A _constructive field_ is a field $F$ whose
elements are all constructive, that is, $F\subseteq\mathbf{C}$.

######  Lemma 3.3.

$\mathbf{Q}$, $\mathbf{C}$, $\mathbf{C^{\prime}}$, and $\mathbf{S}$ are
constructive fields.

Recall that statements about validity of formulas are to be understood as
provability in $\mathrm{IFP}$. Therefore, a constructive field provides, via
program extraction, implementations of the field operations with respect to
the real number representation defined by the field. Since closure under the
multiplicative inverse is required only for numbers that are apart from $0$,
the extracted inversion program has as extra argument a natural number $k$
that guarantees that $|x|\geq 2^{-k}$. In the following, we show that this
extra argument can be omitted if one is willing to accept the generalized
Brouwer’s Thesis, $\mathbf{BT}$.

Using $\mathbf{BT}$, the Archimedean axiom (9) becomes $\forall
x\,\mathbf{Acc}_{\prec}(x)$ (where, as in (9), $y\prec x\
\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\ 0\leq y\ \land\ y=x-1$), and this
can in turn be used to prove the following two induction rules, called
_Archimedean Induction_ [18]. Both rules are parametrized by a positive
rational number $q$. In (17), $P$ is an arbitrary predicate. In (18), $R$ is a
ring and $B$ is arbitrary.

$\forall x\neq 0\,P(x)\forall x\neq 0\,((|x|\leq q\to P(2x))\to P(x))$ (17)
$\forall x\in R\setminus\\{0\\}\,B(x)\forall x\in
R\setminus\\{0\\}\,(B(x)\lor(|x|\leq q\land(B(2x)\to B(x))))$ (18)

Unlike (9), the Archimedean Induction rules do have computational content:

######  Lemma 3.4 ($\mathbf{BT}$, [18]).

(17) and (18) are provable.

If $s$ realizes the premise of (17), then the extracted program realizing the
conclusion is $\mathbf{rec}\,s$.

If $s$ realizes the premise of (18), then the extracted program realizing the
conclusion is

$\chi\,a\stackrel{{\scriptstyle\mathrm{rec}}}{{=}}\mathbf{case}\,s\,a\,\mathbf{of}\,\\{\mathbf{Left}(b)\to
b;\mathbf{Right}(f)\to f(\chi\,(\mathbf{mult}_{2}(a)))\\}$

where $\mathbf{mult}_{2}$ is extracted from a proof that $R$ is closed under
doubling.

######  Proof 3.5.

(17) can be inferred from $\forall x\,\mathbf{Acc}_{\prec}(x)$ using
properties of the function $x\mapsto 2^{-x}$.

(18) follows directly from (17), since with
$P(x)\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}R(x)\to B(x)$, the premise of
(18) implies the premise of (17).

######  Lemma 3.6 ($\mathbf{BT}$).

Non-zero elements of a constructive fields are apart from zero.

######  Proof 3.7.

Let $F$ be a constructive field. We have to show $\forall x\in
F\setminus\\{0\\}\,x\,{\not\,\not=}\,0$. We use Archmedean Induction (18) with
$q=3$ and the fact that $2x\,{\not\,\not=}\,0\to x\,{\not\,\not=}\,0$ to
reduce this task to showing that for every $x\in F\setminus\\{0\\}$,
$x\,{\not\,\not=}\,0$ or $|x|\leq 3$. Using the constructivity of $F$, we have
$q\in\mathbf{Q}$ such that $|x-q|\leq 1$. If $|q|>2$, then $|x|\geq 1$, hence
$x\,{\not\,\not=}\,0$. If $|q|\leq 2$, then $|x|\leq 3$.

Since the implication $2x\,\,{\not\,\not=}\,\,0\to x\,\,{\not\,\not=}\,\,0$ is
realized by the successor function, the program extracted from the above proof
is (after trivial simplifications)

$\displaystyle\varphi_{1}(f)$ $\displaystyle=$
$\displaystyle\mathbf{if}\,|\mathbf{approx}(f,0)|>2\,\mathbf{then}\,0\,\mathbf{else}\,1+\varphi_{1}(\mathbf{mult}_{2}(f))$

where $\mathbf{approx}$ realizes the constructivity of $F$, that is, if $f$
realizes $F(x)$ and $k\in\mathbf{N}$, then $\mathbf{approx}(f,k)$ is a
rational number whose distance to $x$ is at most $2^{-k}$.

_Remark._ It may seem strange that we introduce constructive analysis in an
axiomatic way; however, this approach is not uncommon in constructive
mathematics. For example, [3] introduces constructive axioms for the real
line, [29, 30] study an axiomatic theory of apartness and nearness, and [31]
gives a constructive axiomatic presentation of limit spaces. In our case, the
rational for an axiomatic approach to the real numbers is that it allows us to
separate computationally irrelevant properties of the real numbers such as
algebraic identities and the Archimedean axiom from computationally relevant
ones such as inclusion of the integers and approximability by rationals.

###  4 Concurrency

In [20], the system $\mathrm{CFP}$ (concurrent fixed point logic) is
introduced that extends $\mathrm{IFP}$ by a logical operator
${\mathbf{\downdownarrows}}$ permitting the extraction of programs with two
concurrent threads. However, to do Gaussian elimination concurrently, we need
$n$ threads where $n$ varies through all positive numbers less or equal the
dimension of the matrix to be inverted. We will first sketch the essential
features of $\mathrm{CFP}$ and then describe an extension that caters for this
more general form of concurrency.

####  1 $\mathrm{CFP}$

$\mathrm{CFP}$ extends $\mathrm{IFP}$ by two logical operators, $A|_{B}$
(restriction) and ${\mathbf{\downdownarrows}}(A)$ (two-threaded concurrency).
Ultimately, we are interested only in the latter but the former is needed to
derive concurrency in a non-trivial way.

$A|_{B}$ (read ‘$A$ restricted to $B$’) is a strengthening of the reverse
implication $B\to A$. The two differ only in their realizability semantics
(the following explanation is valid if $B$ is non-computational and $A$ has
only realizers that are defined ($\neq\bot$)): A realizer of $A|_{B}$ is a
‘conditional partial realizer’ of $A$, that is, some $a\in\tau(A)$ such that

  * (i)

if the restriction $B$ holds, then $a$ is defined, and

  * (ii)

if $a$ is defined, then $a$ realizes $A$.

In contrast, for $a$ to realize $B\to A$ it suffices that if $B$ holds, then
$a$ realizes $A$; condition (ii) may fail, that is, if we only know that $a$
is defined, we cannot be sure that $a$ realizes $A$. For example, if $A$ is
$B\lor C$, then $\mathbf{Left}(\mathbf{Nil})$ realizes $B\to A$ but not
$A|_{B}$ unless $B$ holds. The technical definition permits arbitrary $B$ but
requires $A$ to satisfy a syntactic condition, called ‘strictness’, that
ensures that $A$ has only defined realizers.

Before defining strictness we need to extend the Harrop property to
$\mathrm{CFP}$ formulas. Harropness is defined as for $\mathrm{IFP}$ but
stipulating in addition that formulas of the form $A|_{B}$ or
${\mathbf{\downdownarrows}}(A)$ are always non-Harrop. Now strictness is
defined as follows: A non-Harrop implication is strict if the premise is non-
Harrop. Formulas of the form $\diamond x\,A$
($\diamond\in\\{\forall,\exists\\}$) or $\Box(\lambda X\lambda\vec{x}\,A)$
($\Box\in\\{\mu,\nu\\}$) are _strict_ if $A$ is strict. Formulas of other
forms (e.g., $B|_{A}$, ${\mathbf{\downdownarrows}}(A)$, $X(\vec{t})$) are not
strict.

For formulas of the for $A|_{B}$ or ${\mathbf{\downdownarrows}}(A)$ to be
wellformed, we require $A$ to be strict. In the following it is always assumed
that the strictness requirement is fulfilled.

Realizability for restriction is defined as

$\displaystyle a\,\mathbf{r}\,(A|_{B})$
$\displaystyle\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}$
$\displaystyle(\mathbf{r}(B)\to a\neq\bot)\land(a\neq\bot\to
a\,\mathbf{r}\,A)$

where $\mathbf{r}(B)\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\exists
b\,b\,\mathbf{r}\,B$ (‘$B$ is realizable’).

${\mathbf{\downdownarrows}}(A)$ (read ‘concurrently $A$’) is not distinguished
from $A$ in the classical semantics but realizers of this formula can be
computed by two processes which run concurrently, at least one of which has to
terminate, and each of terminating one has to deliver a realizer of $A$. To
model this denotationally, the domain and the programming language are
extended by a binary constructor $\mathbf{Amb}$ which (denotationally) is an
exact copy of the constructor $\mathbf{Pair}$. However, operationally,
$\mathbf{Amb}$ is interpreted as a version of McCarthy’s ambiguity operator
amb [32] that corresponds to globally angelic choice [33]. Realizability of
${\mathbf{\downdownarrows}}(A)$ is defined as

$c\ \mathbf{r}\
{\mathbf{\downdownarrows}}(A)\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}c=\mathbf{Amb}(a,b)\land
a,b:\tau(A)\land(a\neq\bot\lor b\neq\bot)\ \land\\\ (a\neq\bot\to
a\,\mathbf{r}\,A)\land(b\neq\bot\to b\,\mathbf{r}\,A).$

We also set
$\tau({\mathbf{\downdownarrows}}(A))\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\mathbf{A}(\tau(A))$
where $\mathbf{A}$ is a new type constructor with
$D(\mathbf{A}(\rho))\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\\{\mathbf{Amb}(a,b)\mid
a,b\in D(\rho)\\}\cup\\{\bot\\}$.

The proof rules for restriction and concurrency are as follows:

$(A_{0}\vee A_{1})|_{B}B\to A_{0}\vee A_{1}\ \ \ \neg B\to A_{0}\wedge A_{1}$

$\begin{array}[]{ll}A^{\prime}|_{B}A|_{B}\ \ \
A\to(A^{\prime}|_{B})&A|_{B}A\\\ \\\ A|_{B^{\prime}}A|_{B}\ \ \ B^{\prime}\to
B&AA|_{B}\ \ \ B\end{array}$
$\begin{array}[]{ll}A|_{\mathbf{False}}&A|_{\neg\neg B}A|_{B}\end{array}$

${\mathbf{\downdownarrows}}(A)A|_{C}\ \ \ \ A|_{\neg C}\qquad\
{\mathbf{\downdownarrows}}(A)A$

$\ {\mathbf{\downdownarrows}}(B)A\to B\ \ \ {\mathbf{\downdownarrows}}(A)\ \ \
\ \ $

Using the rules (Rest-stab) and (Rest-antimon) on can show that the rule
(Conc-lem) is equivalent to

${\mathbf{\downdownarrows}}(A)\neg\neg(B\lor C)\ \ \ \ A|_{B}\ \ \ \ A|_{C}$
(19)

We also have a variant of the Archimedean Induction which we call _Archimedean
Induction with restriction_. It applies to rings $R$, strict predicates $B$
and rational numbers $q>0$:

$\forall x\in R\,(B(x)|_{x\neq 0})\forall x\in R\,(B(x)\lor(|x|\leq
q\land(B(2x)\to B(x))))$ (20)

To extract programs from $\mathrm{CFP}$ proofs, the programming language for
$\mathrm{IFP}$ needs, in addition to the new constructor $\mathbf{Amb}$, a
strict version of application $M{\downarrow}N$ which is undefined if the
argument $N$ is. As indicated earlier, denotationally, $\mathbf{Amb}$ is just
a constructor (like $\mathbf{Pair}$). However, the operational semantics
interprets $\mathbf{Amb}$ as globally angelic choice, which matches the
realizability interpretation of the concurrency operator
${\mathbf{\downdownarrows}}$, as shown in [20].

######  Theorem 4.8 (Soundness of CFP).

From a $\mathrm{CFP}$ proof of a formula $A$ one can extract a closed program
$M:\tau(A)$ such that $M\,\mathbf{r}\,A$ is provable.

######  Proof 4.9.

The realizability of the new version (20) of Archimedean Induction is shown in
the Lemma below. All other rules have simple realizers that can be explicitly
defined [20]. For example, (Conc-lem) and (Conc-class-or), rules which permit
to derive concurrency with a form of the law of excluded middle, are realized
by the constructor $\mathbf{Amb}$.

######  Lemma 4.10.

Archimedean Induction with Restriction is realizable. If $s$ realizes the
premise of (20), then $\chi$, defined recursively by

$\chi\,a=\mathbf{case}\,s\,a\,\mathbf{of}\,\\{\mathbf{Left}(b)\to
b;\mathbf{Right}(f)\to f{\downarrow}(\chi\,(\mathbf{mult}_{2}\,a))\\},$

realizes the conclusion.

######  Proof 4.11.

Assuming $a\,\mathbf{r}\,R(x)$ we have to show

  * (1)

$x\neq 0\to\chi\,a\neq\bot$.

  * (2)

$\chi\,a\neq\bot\to(\chi\,a)\,\mathbf{r}\,B(x)$.

For (1) it suffices to show (1’) $\forall x\neq 0\,\forall
a\,(a\,\mathbf{r}\,R(x)\to(\chi\,a)\,\mathbf{r}\,B(x))$ since
$(\chi\,a)\,\mathbf{r}\,B(x)$ implies $\chi\,a\neq\bot$, by the strictness of
$B(x)$.

We show (1’) by Archimedean Induction (17). Let $x\neq 0$ and assume, as i.h.,

$|x|\leq q\to\forall
a^{\prime}\,(a^{\prime}\,\mathbf{r}\,R(2x)\to(\chi\,a^{\prime})\,\mathbf{r}\,B(2x))$

We have to show $\forall
a\,(a\,\mathbf{r}\,R(x)\to(\chi\,a)\,\mathbf{r}\,B(x))$. Assume
$a\,\mathbf{r}\,R(x)$. Then $(s\,a)\,\mathbf{r}\,(B(x)\lor(|x|\leq
q\land(B(2x)\to B(x))))$. If $s\,a=\mathbf{Left}(b)$ where
$b\,\mathbf{r}\,B(x)$, then $\chi\,a=b$ and we are done. If
$s\,a=\mathbf{Right}(f)$ where $|x|\leq q$ and $f\,\mathbf{r}\,(B(2x)\to
B(x))$, then $a^{\prime}\,\mathbf{r}\,R(2x)$ for
$a^{\prime}=\mathbf{mult}_{2}\,a$. Thus, by i.h.,
$(\chi\,a^{\prime})\,\mathbf{r}\,B(2x)$ and therefore
$(f(\chi\,a^{\prime}))\,\mathbf{r}\,B(x)$. Since $\chi\,a^{\prime}\neq\bot$ by
the strictness of $B(2x)$, we have $\chi\,a=f(\chi\,a^{\prime})$ and we are
done.

To prove (2), we consider the approximations of $\chi$,

$\displaystyle\chi_{0}\,a$ $\displaystyle=$ $\displaystyle\bot$
$\displaystyle\chi_{n+1}\,a$ $\displaystyle=$
$\displaystyle\mathbf{case}\,s\,a\,\mathbf{of}\,\\{\mathbf{Left}(b)\to
b;\mathbf{Right}(f)\to f{\downarrow}(\chi_{n}\,(\mathbf{mult}_{2}\,a))\\}$

By continuity, if $\chi\,a\neq\bot$, then $\chi_{n}\,a\neq\bot$ for some
$n\in\mathbf{N}$. Therefore, it suffices to show

$\forall n\in\mathbf{N}\,\forall
x,a\,(a\,\mathbf{r}\,R(x)\land\chi_{n}\,a\neq\bot\to(\chi\,a)\,\mathbf{r}\,B(x))$

We induce on $n$. The induction base is trivial since $\chi_{0}\,a=\bot$. For
the step assume $a\,\mathbf{r}\,R(x)$ and $\chi_{n+1}\,a\neq\bot$. Then
$(s\,a)\,\mathbf{r}\,(B(x)\lor(|x|\leq q\land(B(2x)\to B(x))))$. If
$s\,a=\mathbf{Left}(b)$ where $b\,\mathbf{r}\,B(x)$, then $\chi\,a=b$ and we
are done. If $s\,a=\mathbf{Right}(f)$ where $|x|\leq q$ and
$f\,\mathbf{r}\,(B(2x)\to B(x))$, then
$\chi_{n+1}\,a=f{\downarrow}(\chi_{n}\,a^{\prime})$ for
$a^{\prime}=\mathbf{mult}_{2}\,a$. It follows $\chi_{n}\,a^{\prime}\neq\bot$.
By i.h., $(\chi\,a^{\prime})\,\mathbf{r}\,B(2x)$ and therefore
$(f\,(\chi\,a^{\prime}))\,\mathbf{r}\,B(x)$. But
$f\,(\chi\,a^{\prime})=f{\downarrow}(\chi\,a^{\prime})=\chi\,a$ since
$\chi\,a^{\prime}\neq\bot$.

The proof above can also be viewed as an instance of Scott-induction with the
admissible predicate $\lambda d\,.\,\forall
a\,(d\,a\neq\bot\to(\chi\,a)\,\mathbf{r}\,B(x))$ applied to $d=\chi$.

##### Remarks.

Thanks to the rule (Rest-stab), one can use classical logic for the right
argument of a restriction. The rules (Rest-bind) and (Rest-return) show that
restriction behaves like a monad in its left argument. On the other hand, the
concurrency operator does not enjoy this property since a corresponding bind-
rule is missing. Instead, one has only the weaker rule (Conc-mp) which can
also be seen as a monotonicity rule. This shortcoming will be addressed in
Sect. 3.

######  Lemma 4.12 ($\mathbf{BT}$).

Elements $x$ of a constructive field satisfy $x\,\,{\not\,\not=}\,\,0|_{x\neq
0}$.

The realizer extracted from the proof is the program $\varphi_{1}$ of Lemma
3.6.

######  Proof 4.13.

The proof is the same as for Lemma 3.6, noticing that for the proof of the
premise, the assumption $x\neq 0$ is not used.

_Remark._ In contrast to Lemma 4.12, the formula $\forall
x\,(\mathbf{C}(x)\to(x=0|_{x=0}))$ is not realizable (where $x=0$ is again an
atomic nc formula). This can be seen by a simple (domain-theoretic) continuity
argument. If $\psi$ were a realizer then, $\psi(\lambda
n\,.\,0)=\mathbf{Nil}$, since $\lambda n\,.\,0$ realizes $\mathbf{C}(0)$ and
$0=0$ is realizable i.e. holds. Since $\psi$ is continuous there is some
$k\in\mathbf{N}$ such that $\psi(f)=\mathbf{Nil}$ where $f(n)=0$ if $n<k$ and
$f(n)=2^{-(k+1)}$ if $n\geq k$. Clearly $f$ realizes $\mathbf{C}(2^{-(k+1)})$,
but $\mathbf{Nil}$ does not realize the false equation $2^{-(k+1)}=0$.

The following lemma is crucial for concurrent Gaussian elimination.

######  Lemma 4.14 ($\mathbf{BT}$).

If elements $x,y$ of a constructive field are not both $0$, then,
concurrently, one of them is apart from $0$, that is,
${\mathbf{\downdownarrows}}(x\,\,{\not\,\not=}\,\,0\lor
y\,\,{\not\,\not=}\,\,0)$.

The extracted program is

$\displaystyle\varphi_{2}(f,g)$ $\displaystyle=$
$\displaystyle\mathbf{Amb}(\mathbf{Left}{\downarrow}(\varphi_{1}(f)),\mathbf{Right}{\downarrow}(\varphi_{1}(g)))\,.$

######  Proof 4.15.

By Lemma 4.12 and the fact that restriction is monotone in its left argument
(which follows from the rule (Rest-bind)), we have
$(x\,\,{\not\,\not=}\,\,0\lor y\,\,{\not\,\not=}\,\,0)|_{x\neq 0}$ as well as
$(x\,\,{\not\,\not=}\,\,0\lor y\,\,{\not\,\not=}\,\,0)|_{y\neq 0}$. Since not
both $x$ and $y$ are $0$, we can apply rule (Rest-class-or).

_Remarks._ Intuitively, the extracted program $\varphi_{2}$ consists of two
processes $\alpha=\mathbf{Left}{\downarrow}(\varphi_{1}(f))$ and
$\beta=\mathbf{Right}{\downarrow}(\varphi_{1}(g))$ which search concurrently
for approximations to $x$ and $y$ respectively, until $\alpha$ finds a $k$
where $|f(k)|>2^{-k}$ or $\beta$ finds an $l$ where $|g(l)|>2^{-l}$, returning
the numbers with a corresponding flag $\mathbf{Left}$ or $\mathbf{Right}$.
Both, or only one of the searches might be successful and which of the
successful search results is taken is decided nondeterministically.

In this particular situation, concurrency could be avoided (even without
synchronization or interleaving): Since not both $x$ and $y$ are $0$,
$x^{2}+y^{2}$ is nonzero and hence apart from $0$. Computing sufficiently good
approximations to $x^{2}+y^{2}$ and $x^{2}$ and comparing them, one can decide
whether $x$ or $y$ is apart from $0$. However, to compute approximations of
$x^{2}+y^{2}$, both, $x$ and $y$ need to be equally well approximated, thus
the overall computation time is the _sum_ of the computation times for $x$ and
$y$. However, using concurrency the computation time will be the _minimum_.
Imagine $x$ and $y$ being very small positive reals and the realizer $f$ of
$F(x)$ providing very fast, but the realizer $g$ of $F(y)$ very slow
approximations. Then the extracted concurrent program will terminate fast with
a result $\mathbf{Left}(k)$ (computed by the process $\alpha$ searching $f$).
Hence, this example illustrates the fact that concurrent realizability not
only supports a proper treatment of partiality, as in the case study on
infinite Gray code [20], but also enables us to exploit the efficiency gain of
concurrency at the logical level.

####  2 Finitely threaded concurrency

$\mathrm{CFP}$ can be easily generalized to concurrency with an arbitrary
finite number of threads. We generalize the operator
${\mathbf{\downdownarrows}}$ to ${\mathbf{\downdownarrows}}_{n}$, where $n$ is
a positive natural number (so that ${\mathbf{\downdownarrows}}$ corresponds to
${\mathbf{\downdownarrows}}_{2}$), and allow the constructor $\mathbf{Amb}$ to
take an arbitrary positive but finite number of arguments. We define that $a$
realizes ${\mathbf{\downdownarrows}}_{n}(A)$ if $a$ is of the form
$\mathbf{Amb}(a_{1},\ldots,a_{m})$ with $1\leq m\leq n$ such that at least one
$a_{i}$ is defined and all defined $a_{i}$ realize $A$:

$\displaystyle a\,\mathbf{r}\,{\mathbf{\downdownarrows}}_{n}(A)$
$\displaystyle\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}$
$\displaystyle\bigvee_{1\leq m\leq
n}\,(a=\mathbf{Amb}(a_{1},\ldots,a_{m})\land$
$\displaystyle\qquad\quad\bigvee_{1\leq i\leq
m}a_{i}\neq\bot\land\bigwedge_{1\leq i\leq m}(a_{i}\neq\bot\to
a_{i}\,\mathbf{r}\,A))$

The proof rules for ${\mathbf{\downdownarrows}}_{n}$ are similar to those for
${\mathbf{\downdownarrows}}$:

${\mathbf{\downdownarrows}}_{n}(A)\neg\neg\bigvee_{1\leq i\leq
n}B(i)\qquad\bigwedge_{1\leq i\leq n}A|_{B(i)}$

${\mathbf{\downdownarrows}}_{n}(A)A\qquad{\mathbf{\downdownarrows}}_{n}(B)A\to
B\qquad{\mathbf{\downdownarrows}}_{n}(A)$

######  Lemma 4.16 ($\mathbf{BT}$).

If elements $x_{1},\ldots,x_{n}$ of a constructive field are not all $0$,
then, $n$-concurrently, one of them is apart from $0$, that is,
${\mathbf{\downdownarrows}}_{n}(x_{1}\,\,{\not\,\not=}\,\,0\lor\ldots\lor
x_{n}\,\,{\not\,\not=}\,\,0)$.

Setting
$\mathbf{In}_{i}\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\lambda\,a\,.\,\mathbf{Right}^{i-1}(\mathbf{Left}(a))$
for $i\in\\{1,\ldots,n\\}$, the extracted program is

$\displaystyle\varphi_{3}(f_{1},\ldots,f_{n})$ $\displaystyle=$
$\displaystyle\mathbf{Amb}(\mathbf{In}_{1}{\downarrow}(\varphi_{1}(f_{1})),\ldots,\mathbf{In}_{n}{\downarrow}(\varphi_{1}(f_{n})))\,.$

######  Proof 4.17.

Similar to Lemma 4.14 using the rules for ${\mathbf{\downdownarrows}}_{n}$.

_Remark._ We treated the index $n$ as a parameter on the meta-level, i.e.
${\mathbf{\downdownarrows}}_{n}$ is an operator for every $n$. On the other
hand, in a stringent formalization, one has to treat $n$ as a formal
parameter, i.e. ${\mathbf{\downdownarrows}}_{n}(A)$ is a formula with a free
variable $n$. Finitely iterated conjunctions and disjunctions have to be
formalized in a similar way. This can be easily done, using formal inductive
definitions, however we refrain from carrying this out, since it would obscure
the presentation and impede the understanding of what follows.

####  3 Monadic concurrency

The concurrency operators ${\mathbf{\downdownarrows}}$ and
${\mathbf{\downdownarrows}}_{n}$ were sufficient for the examples studied so
far, since these did not involve iterated concurrent computation, i.e. we did
not use the result of one concurrent computation as a parameter for another
one. In other words, we did not use concurrency ‘in sequence’. However, such
sequencing will be required in our concurrent modelling of Gaussian
elimination (Sect. 5) since the choices of previous pivot elements influence
the choice of the next one.

The problem of sequencing becomes apparent if we nest non-determinism as
defined by ${\mathbf{\downdownarrows}}_{n}$ since this increases the index $n$
bounding the number of processes. More precisely, the rule

${\mathbf{\downdownarrows}}_{n^{2}}(A){\mathbf{\downdownarrows}}_{n}({\mathbf{\downdownarrows}}_{n}(A)\lor\mathbf{False})$

is realizable, but this is optimal - we cannot lower the number $n^{2}$ in the
conclusion to $n$. Mathematically, the problem is that
${\mathbf{\downdownarrows}}_{n}$ is not a monad. However, we can turn
${\mathbf{\downdownarrows}}_{n}$ into a monad by an inductive definition:

${\mathbf{\downdownarrows}}^{*}_{n}(A)\stackrel{{\scriptstyle\mu}}{{=}}{\mathbf{\downdownarrows}}_{n}(A\lor{\mathbf{\downdownarrows}}^{*}_{n}(A))$

Clearly, $a\,\mathbf{r}\,{\mathbf{\downdownarrows}}^{*}_{n}(A)$ holds iff $a$
is of the form $\mathbf{Amb}(a_{1},\ldots,a_{m})$ for some $1\leq m\leq n$
such that at least one $a_{i}$ is defined and all defined $a_{i}$ realize
$A\lor{\mathbf{\downdownarrows}}^{*}_{n}(A)$.

Note that ${\mathbf{\downdownarrows}}^{*}_{n}(A)$ is wellformed for arbitrary
formulas $A$, not only strict ones.

######  Lemma 4.18.

The following rules follow from the rules for ${\mathbf{\downdownarrows}}_{n}$
and are hence realizable (for arbitrary formulas):

$\ {\mathbf{\downdownarrows}}^{*}_{n}(A)A\qquad\
{\mathbf{\downdownarrows}}^{*}_{n}(B)A\to{\mathbf{\downdownarrows}}^{*}_{n}(B)\
\ \ {\mathbf{\downdownarrows}}_{n}(A)$

$\
{\mathbf{\downdownarrows}}^{*}_{n}(B)A\to{\mathbf{\downdownarrows}}^{*}_{n}(B)\
\ \ {\mathbf{\downdownarrows}}^{*}_{n}(A)$

######  Proof 4.19.

(Conc-return-n*) follows immediately from the definition of
${\mathbf{\downdownarrows}}^{*}_{n}$.

To show (Conc-weak-bind), assume $A\to{\mathbf{\downdownarrows}}^{*}_{n}(B)$
and ${\mathbf{\downdownarrows}}_{n}(A)$. Then also $A\to
B\lor{\mathbf{\downdownarrows}}^{*}_{n}(B)$ and hence, by (Conc-mp-n),
${\mathbf{\downdownarrows}}_{n}(B\lor{\mathbf{\downdownarrows}}^{*}_{n}(B))$.
It follows ${\mathbf{\downdownarrows}}^{*}_{n}(B)$, by the definition of
${\mathbf{\downdownarrows}}^{*}_{n}$.

To prove (Conc-bind), we assume $A\to{\mathbf{\downdownarrows}}^{*}_{n}(B)$
and show
${\mathbf{\downdownarrows}}^{*}_{n}(A)\to{\mathbf{\downdownarrows}}^{*}_{n}(B)$
by strictly positive induction on the definition of
${\mathbf{\downdownarrows}}^{*}_{n}(A)$. Hence, it suffices to show
$A\lor{\mathbf{\downdownarrows}}^{*}_{n}(B)\to{\mathbf{\downdownarrows}}^{*}_{n}(B)$,
which follows from the assumption $A\to{\mathbf{\downdownarrows}}^{*}_{n}(B)$.

We characterize realizability of ${\mathbf{\downdownarrows}}^{*}_{n}(A)$ by
term rewriting. Call $\mathbf{Amb}(\vec{a})$ _sound_ if
$\forall\,i\,(a_{i}\neq\bot\to\exists\,b\,(a_{i}=\mathbf{Left}(b)\lor
a_{i}=\mathbf{Right}(b))$. Now define

$\displaystyle a\to_{n}a^{\prime}$
$\displaystyle\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}$
$\displaystyle\exists\,m\leq n\exists\,\vec{a}=a_{1},\ldots,a_{m}\land
a=\mathbf{Amb}(\vec{a})\ \hbox{sound}\land$
$\displaystyle\qquad\bigvee_{i}(\exists\,b\,a_{i}=a^{\prime}=\mathbf{Left}(b)\lor
a_{i}=\mathbf{Right}(a^{\prime}))$

######  Lemma 4.20.

$a\,\mathbf{r}\,{\mathbf{\downdownarrows}}^{*}_{n}(A)$ iff $a$ is reducible
w.r.t. $\to_{n}$ and every reduction sequence
$a\to_{n}a^{\prime}\to_{n}\ldots$ terminates and ends with some
$\mathbf{Left}(b)$ such that $b\,\mathbf{r}\,A$.

######  Proof 4.21.

“only if”: Induction on
$a\,\mathbf{r}\,{\mathbf{\downdownarrows}}^{*}_{n}(A)$. Assume
$a\,\mathbf{r}\,{\mathbf{\downdownarrows}}^{*}_{n}(A)$. Then
$a=\mathbf{Amb}(\vec{a})$ and $a$ is reducible. Let
$a\to_{n}a^{\prime}\to_{n}\ldots$ be a reduction sequence. Case
$a_{i}=a^{\prime}=\mathbf{Left}(b)$. Then $a^{\prime}$ is not further
reducible and $b\,\mathbf{r}\,A$, hence we are done. Case
$a_{i}=\mathbf{Right}(a^{\prime})$ and
$a^{\prime}\,\mathbf{r}\,{\mathbf{\downdownarrows}}^{*}_{n}(A)$. Then the
induction hypothesis applies. “if”: Assume that $a$ is reducible and every
reduction sequence $a\to_{n}a^{\prime}\to_{n}\ldots$ terminates and ends with
some $\mathbf{Left}(b)$ where $b\,\mathbf{r}\,A$. This means that the relation
$\to_{n}$ restricted to iterated reducts of $a$ is wellfounded. We show
$a\,\mathbf{r}\,{\mathbf{\downdownarrows}}^{*}_{n}(A)$ by induction on
$\to_{n}$. Since $a$ is reducible, $a\to_{n}a^{\prime}$ for some $a^{\prime}$.
Hence $a=\mathbf{Amb}(\vec{a})$ and either $a_{i}=a^{\prime}=\mathbf{Left}(b)$
for some $b$, or else $a_{i}=\mathbf{Right}(a^{\prime})$. Hence the first part
of the definition of $a\,\mathbf{r}\,{\mathbf{\downdownarrows}}^{*}_{n}(A)$
holds. For the second part assume $a_{i}\neq\bot$. Since
$\mathbf{Amb}(\vec{a})$ is sound, either $a_{i}=\mathbf{Left}(b)$ or
$a_{i}=\mathbf{Right}(b)$. Assume $a_{i}=\mathbf{Left}(b)$. We have to show
$b\,\mathbf{r}\,A$. Since $a\to_{n}\mathbf{Left}(b)$ it follows that
$\mathbf{Left}(b)$ terminates a reductions sequence starting with $a$. Hence
$b\,\mathbf{r}\,A$, by assumption. Finally, assume
$a_{0}=\mathbf{Right}(a^{\prime})$. We have to show
$a^{\prime}\,\mathbf{r}\,{\mathbf{\downdownarrows}}^{*}_{n}(A)$. Since
$a\to_{n}a^{\prime}$ this holds by induction hypothesis.

The characterization of $a\,\mathbf{r}\,{\mathbf{\downdownarrows}}^{*}_{n}(A)$
given in Lemma 4.20 shows that $a$ can be viewed as a nondeterministic process
requiring at most $n$ processes running concurrently (or in parallel). Each
step $a\to_{n}a^{\prime}$ represents such a non-deterministic computation. The
fact that _every_ reduction sequence will lead to a realizer of $A$ means that
after each step all other computations running in parallel may safely be
abandoned since no backtracking will be necessary.

###  5 Gaussian elimination

By a _matrix_ we mean a quadratic matrix with real coefficients. A matrix is
_non-singular_ if its columns are linearly independent. Let $F$ be a
constructive field of reals (see Sect. 3). A matrix $A$ is called _$F$ matrix_
if all the coefficients of $A$ are in $F$. We prove that every non-singular
$F$ matrix has an $F$ left inverse, and extract from the proof a concurrent
version of the well-known matrix inversion algorithm based on Gaussian
elimination. The proof is concurrent, because the non-zero element of a column
(the pivot) is computed concurrently.

We fix a dimension $n\in\mathbf{N}$ and let $k,l$ range over
$\mathbf{N}_{n}\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\\{1,\ldots,n\\}$,
the set of valid matrix indices. For a matrix $A$ we let $A(k,l)$ be its entry
at the $k$-th row and $l$-th column. We denote matrix multiplication by $A\ast
B$, i.e.

$(A\ast B)(k,l)=\sum_{i=1}^{n}A(k,i)\cdot B(i,l)$

By $E$ we denote the unit matrix, i.e.

$E(k,l)\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\left\\{\begin{array}[]{ll}1&\hbox{if
$k=l$}\\\ 0&\hbox{otherwise}\end{array}\right.$

We call an $F$ matrix _invertible_ if there exists an $F$ matrix $B$ such that
$B\ast A=E$.

To formalize the above, one may add sorts for vectors and matrices and a
function for accessing their entries. Furthermore, a function symbol for
matrix multiplication which needs three arguments, two for the matrices to be
multiplied and one for the dimension. The formula for matrix multiplication
can then be stated as an axiom since it is admissibly Harrop (see Sect. 2).
Furthermore, one postulates admissible Harrop axioms for the existence of
explicitly defined matrices, for example,

$\forall n\in\mathbf{N}\exists E\forall i,j\in\\{1,\ldots,n\\}((i=j\to
E(i,j)=1)\land(i\neq j\to E(i,j)=0)\,.$

The notion of linear independence can be expressed as a Harrop formula as
well. There are many alternative formalization which, essentially, lead to the
same result, in particular, the extracted program will be the same.

######  Theorem 5.22 (Gaussian elimination).

Every non-singular $F$ matrix is invertible.

######  Proof 5.23.

For matrices $A$, $B$ and $i\in\\{0,\ldots,n\\}$ we set

$A\stackrel{{\scriptstyle
i}}{{=}}B\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\forall k,l\,(l>i\to
A(k,l)=B(k,l))$

($A$ and $B$ coincide on the columns $i+1,\ldots,n$). Hence
$A\stackrel{{\scriptstyle 0}}{{=}}B$ means $A=B$ whereas
$A\stackrel{{\scriptstyle n}}{{=}}B$ always holds. To prove the theorem, it
suffices to show:

##### Claim.

For all $i\in\\{0,\ldots,n\\}$, if $A$ is a non-singular $F$ matrix such that
$A\stackrel{{\scriptstyle i}}{{=}}E$, then $A$ is invertible.

We prove the Claim by induction on $i$.

_In the proof, we need to bear in mind that, since we want to use concurrent
pivoting (Lemma 4.16), and we iterate the argument, we can only hope to prove
invertibility of $A$ $\omega$-concurrently, that is, we prove in fact_

$\forall i\in\\{0,\ldots,n\\}\,\forall\,A\in F_{\mathrm{ns}}^{n\times
n}\,(A\stackrel{{\scriptstyle
i}}{{=}}E\to{\mathbf{\downdownarrows}}^{*}_{n}(\exists B\in
F_{\mathrm{ns}}^{n\times n}\,B\ast A=E))$

_where $A\in F_{(\mathrm{ns})}^{n\times n}$ means that $A$ is an
$n$-dimensional (non-singular) $F$ matrix._

The base case, $i=0$, is easy, since the hypothesis $A\stackrel{{\scriptstyle
0}}{{=}}E$ means $A=E$. Therefore, we can take
$B\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}E$.

For the step, assume $i>0$ and let $A\in F_{\mathrm{ns}}^{n\times n}$ such
that $A\stackrel{{\scriptstyle i}}{{=}}E$. It suffices to show that there is
$C\in F_{\mathrm{ns}}^{n\times n}$ such that $C\ast A\stackrel{{\scriptstyle
i-1}}{{=}}E$. Since then $C\ast A\in F_{\mathrm{ns}}^{n\times n}$, and
therefore, by induction hypothesis, we find $B\in F_{\mathrm{ns}}^{n\times
n}$, with $B\ast(C\ast A)=E$. Hence $(B\ast C)\ast A=E$, by the associativity
of matrix multiplication.

_Thanks to the rule (Conc-weak-bind), it suffices to find the matrix $C$
concurrently, that is, it suffices to prove
${\mathbf{\downdownarrows}}_{n}(\exists\,C\in F_{ns}^{n\times n}\,C\ast
A\stackrel{{\scriptstyle i-1}}{{=}}E)$, since the induction hypothesis
implies_

$(\exists\,C\in F_{ns}^{n\times n}\,C\ast A\stackrel{{\scriptstyle
i-1}}{{=}}E)\to{\mathbf{\downdownarrows}}^{*}_{n}(\exists B\in F_{ns}^{n\times
n}\,B\ast A=E).$

Since $A$ is non-singular and $A\stackrel{{\scriptstyle i}}{{=}}E$, it is not
the case that $A(k,i)=0$ for all $k\leq i$. Because otherwise the $n$-tuple
$(\alpha_{1},\ldots,\alpha_{n})$ with $\alpha_{l}=0$ for $l<i$, $\alpha_{i}=1$
and $\alpha_{l}=-A(l,i)$ for $l>i$ would linearly combine the columns of $A$
to the zero-vector, that is $\sum_{l=1}^{n}\alpha_{l}\cdot A(k,l)=0$ for all
$k$.

Therefore, by Lemma 4.16, we find, concurrently, $k_{0}\leq i$ such that
$A(k_{0},i)\,{\not\,\not=}\,0$. Hence, there exists $\alpha\in F$ such that
$A(k_{0},i)\cdot\alpha=1$. Define the matrix $C_{1}$ by

$C_{1}(k,l)\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\left\\{\begin{array}[]{ll}\alpha&\hbox{if
$k=l=k_{0}$}\\\ 1&\hbox{if $k=l\neq k_{0}$}\\\
0&\hbox{otherwise}\end{array}\right.$

and set $A_{1}\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}C_{1}\ast A$
(multiplying the $k_{0}$-th row by $\alpha$). Clearly,
$A_{1}\stackrel{{\scriptstyle i}}{{=}}E$ and $A_{1}(k_{0},i)=1$. Further,
define

$C_{2}(k,l)\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\left\\{\begin{array}[]{ll}1&\hbox{if
$k=l\not\in\\{k_{0},i\\}$ or $(k,l)\in\\{(k_{0},i),(i,k_{0})\\}$}\\\
0&\hbox{otherwise}\end{array}\right.$

and set $A_{2}\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}C_{2}\ast A_{1}$
(swapping rows $k_{0}$ and $i$). Clearly, $A_{2}\stackrel{{\scriptstyle
i}}{{=}}E$ and $A_{2}(i,i)=1$. Finally, define

$C_{3}(k,l)\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}\left\\{\begin{array}[]{ll}-A_{2}(k,i)&\hbox{if
$k\neq i$ and $l=i$}\\\ 1&\hbox{if $k=l$}\\\
0&\hbox{otherwise}\end{array}\right.$

and set $A_{3}\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}C_{3}\ast A_{2}$
(subtracting the $A_{2}(k,i)$ multiple of row $i$ from row $k$, for each
$k\neq i$). Clearly, $A_{3}\stackrel{{\scriptstyle i-1}}{{=}}E$, and
$C\stackrel{{\scriptstyle\mathrm{Def}}}{{=}}C_{3}\ast C_{2}\ast C_{1}$ is a
non-singular $F$ matrix since $C_{1},C_{2},C_{3}$ are. By associativity of
matrix multiplication we have $C\ast A=A_{3}\stackrel{{\scriptstyle
i-1}}{{=}}E$. This completes the proof of the claim and hence the theorem.
The above proof is written in such a detail that its formalization is
straightforward and a program can be extracted. We did this (by hand since
$\mathrm{CFP}$ has yet to be implemented), with the lazy functional
programming language Haskell as target language. In [20] it is shown how
$\mathbf{Amb}$ can be interpreted as concurrency using the Haskell library
`Control.Concurrent`.

Since Thm. 5.22 is stated w.r.t. an arbitrary constructive field $F$, the
extracted program is polymorphic in (realizers of) $F$. We tested the
extracted matrix inversion program with respect to the constructive fields
$\mathbf{Q}$ (rational numbers (12)), $\mathbf{C}$ (fast rational Cauchy
sequences implemented as functions (11)), and $\mathbf{C^{\prime}}$ (fast
rational Cauchy sequences implemented as streams (14)), running it with
matrices some of whose entries are nonzero but very close to zero and hard to
compute [34].

The result was that $\mathbf{Q}$ is hopeless since exact rational numbers
become huge, in terms of the size of their representation as fractions, and
thus computationally unmanageable. $\mathbf{C}$ and $\mathbf{C^{\prime}}$
performed similarly with $\mathbf{C^{\prime}}$ being slightly faster since the
stream representation can exploit memoization effects and Haskell’s laziness.

We also compared the extracted programs with a variant where concurrency is
explicitly modelled through interleaving Cauchy sequences or digit streams.
Here, one notices the effect that the slowest Cauchy sequence (the one whose
computation consumes most time) determines the overall run time, instead of
the fastest as it is the case with true concurrency.

###  6 Conclusion

This paper aimed to demonstrate the potential of constructive mathematics
regarding program extraction, not only as a possibility in principle, but as a
viable method that is able to capture computational paradigms that are crucial
in current programming practice. We used $\mathrm{CFP}$, an extension of a
logic for program extraction by primitives for partiality and concurrency, to
extract a concurrent program for matrix inversion based on Gaussian
elimination. Although the proof of the correctness of the logic is quite
involved, the extension is very simple and consists of just two new logical
operators, restriction, a strengthening of implication that is able to control
partiality, and an operator that permits computation with a fixed number of
concurrent threads. The case study on Gaussian elimination showed that proofs
in this system are very close to usual mathematical practice.

The system $\mathrm{CFP}$ uses the axiom $\mathbf{BT}$, a generalization of
Brouwer’s Thesis, which can also be viewed as an abstract form of bar
induction. $\mathbf{BT}$ was used to turn the Archimedean axiom for real
numbers into an induction schema which in turn allowed us to prove that
nonzero elements of a constructive field are apart from zero. The usual proof
of the latter result requires Markov’s principle and the axiom of countable
choice. Moreover, the introduction rule for the concurrency operator is a form
of the law of excluded middle. For these reasons, $\mathrm{CFP}$ has to be
regarded as a semi-constructive system, which begs the question to which
extent our results can be regarded constructively valid. Classical logic could
be partially avoided by negative translation, however, its use has
computational significance since it allows us to undertake searches without
having a constructive bound for the search. Replacing these unbounded searches
by algorithms that use constructively obtained (worst-case) bounds may result
in a dramatic loss of efficiency since the computation of these bounds may be
expensive and useless since the search usually stops far earlier than
predicted by the bound (see [35] for examples). It is an interesting problem
to find a formal system that is fully constructive but, at the same time,
allows for efficient program extraction as in our semi-constructive system.

### Acknowledgements

This work has received funding from the European Union’s Horizon 2020 research
and innovation programme under the Marie Sklodowska-Curie grant agreement No
731143 (CID). We also acknowledge support by the JSPS Core-to-Core Program (A.
Advanced Research Networks) and JSPS KAKENHI grant number 15K00015.

## References

  * [1] E. Bishop and D. Bridges, _Constructive Analysis_. Grundlehren der mathematischen Wissenschaften 279, Springer (1985).
  * [2] D. Bridges, Constructive mathematics: a foundation for computable analysis, _Theoretical Computer Science_. 219, 95–109 (1999).
  * [3] D. Bridges and S. Reeves, Constructive mathematics in theory and programming practice, _Philosophia Mathematica_. 7(3), 65–104 (1999).
  * [4] R. L. Constable, _Implementing Mathematics with the Nuprl Proof Development System_. Prentice–Hall, New Jersey (1986).
  * [5] Coq.  The Coq Proof Assistant.  URL https://coq.inria.fr .
  * [6] Agda.  Official website.  URL http://wiki.portal.chalmers.se/agda/ .
  * [7] S. Berghofer.  Program Extraction in simply-typed Higher Order Logic.  In _Types for Proofs and Programs (TYPES’02)_ , vol. 2646, _Lecture Notes in Computer Science_ , pp. 21–38, Springer (2003).
  * [8] U. Berger, K. Miyamoto, H. Schwichtenberg, and M. Seisenberger.  Minlog - a tool for program extraction for supporting algebra and coalgebra.  In _CALCO-Tools_ , vol. 6859, _LNCS_ , pp. 393–399, Springer (2011).  Doi:10.1007/978-3-642-22944-2_29.
  * [9] R. Constable and C. Murthy.  Finding computational content in classical proofs.  In eds. G. Huet and G. Plotkin, _Logical Frameworks_ , pp. 341–362, Cambridge University Press (1991).
  * [10] M. Parigot.  $\lambda\mu$–calculus: an algorithmic interpretation of classical natural deduction.  In _Proceedings of Logic Programming and Automatic Reasoning, St. Petersburg_ , vol. 624, _LNCS_ , pp. 190–201, Springer (1992).
  * [11] U. Berger, H. Schwichtenberg, and W. Buchholz, Refined program extraction from classical proofs, _Annals of Pure and Applied Logic_. 114, 3–25 (2002).
  * [12] S. Berardi, M. Bezem, and T. Coquand, On the computational content of the axiom of choice, _The Journal of Symbolic Logic_. 63(2), 600–622 (1998).
  * [13] U. Berger and P. Oliva.  Modified bar recursion and classical dependent choice.  In _Logic Colloquium 2001_. Springer (2001).
  * [14] J.-L. Krivine, Dependent choice, ‘quote’ and the clock, _Theoretical Computer Science_. 308, 259–276 (2003).
  * [15] U. Berger.  A computational interpretation of open induction.  In _Proc. of the Nineteenth Annual IEEE Symposium on Logic in Computer Science_ , pp. 326–334, IEEE Computer Society (2004).  ISBN 0-7695-2192-4.
  * [16] M. Seisenberger, Programs from proofs using classical dependent choice, _Annals of Pure and Applied Logic_. 153(1–3), 97–110 (2008).
  * [17] P. Schuster, Induction in algebra: A first case study, _Logical Methods in Computer Science_. 9(3:20), 1–19 (2013).
  * [18] U. Berger and H. Tsuiki, Intuitionistic fixed point logic, _Annals of Pure and Applied Logic_. 172(3), 1–56 (2021).
  * [19] T. Powell, P. Schuster, and F. Wiesnet.  A universal algorithm for Krull’s theorem.  To appear: Information and Computation (2021).
  * [20] U. Berger and H. Tsuiki.  Extracting total Amb programs from proofs.  In _Proceeding of the European Symposium on Programming (ESOP 2022)_ (2022).  To appear: LNCS. Full version at https://arxiv.org/abs/2104.14669.
  * [21] H. Tsuiki, Real Number Computation through Gray Code Embedding, _Theoretical Computer Science_. 284(2), 467–485 (2002).
  * [22] G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott, _Continuous Lattices and Domains_. vol. 93, _Encyclopedia of Mathematics and its Applications_ , Cambridge University Press (2003).
  * [23] S. C. Kleene, On the interpretation of intuitionistic number theory, _The Journal of Symbolic Logic_. 10, 109–124 (1945).
  * [24] G. Kreisel, Interpretation of analysis by means of constructive functionals of finite types, _Constructivity in Mathematics_. pp. 101–128 (1959).
  * [25] V. Veldman, Brouwer’s real thesis on bars, _Philosophia Scientiæ, Constructivism: Mathematics, Logic, Philosophy and Linguistics_. 6, 21–42 (2001).
  * [26] H. Schwichtenberg and S. S. Wainer, _Proofs and Computations_. Cambridge University Press (2012).
  * [27] U. Berger, From coinductive proofs to exact real arithmetic: theory and applications, _Logical Methods in Comput. Sci._ 7(1), 1–24 (2011).
  * [28] U. Berger and D. Spreen, A coinductive approach to computing with compact sets, _Journal of Logic and Analysis_. 8 (2016).
  * [29] D. Bridges and L. Vita, Apartness spaces as a framework for constructive topology, _Annals of Pure and Applied Logic_. 119, 61–83 (2003).
  * [30] D. Bridges, H. Ishihara, P. Schuster, and L. Vita, Apartness, compactness and nearness, _Theoretical Computer Science_. 405, 3–10 (2008).
  * [31] I. Petrakis, Limit spaces with approximations, _Annals of Pure and Applied Logic_. 167, 737–752 (2016).
  * [32] J. McCarthy.  A basis for a mathematical theory of computation.  In eds. P. Braffort and D. Hirschberg, _Computer Programming and Formal Systems_ , vol. 35, _Studies in Logic and the Foundations of Mathematics_ , pp. 33 – 70. Elsevier (1963).  https://doi.org/10.1016/S0049-237X(08)72018-4.
  * [33] W. Clinger and C. Halpern.  Alternative semantics for McCarthy’s amb.  In ed. W. G. Brookes S.D., Roscoe A.W., _Seminar on Concurrency. CONCURRENCY 1984_ , vol. 197, _Lecture Notes in Computer Science_ , Springer (1985).  10.1007/3-540-15670-4_22.
  * [34] U. Berger.  CFP (concurrent fixed point logic) repository.  URL https://github.com/ujberger/cfp .
  * [35] D. Pattinson, Constructive domains with classical witnesses, _Logical Methods in Computer Science_. 17(1), 19:1–19:30 (2021).


# Some density results involving the average order of a finite group

Mihai-Silviu Lazorec

(March 4, 2023)

###### Abstract

Let $o(G)$ be the average of the element orders of a finite group $G$. A
research topic concerning this quantity is understanding the relation between
$o(G)$ and $o(H)$, where $H$ is a subgroup of $G$. Let $\mathscr{N}$ be the
class of finite nilpotent groups and let $L(G)$ be the subgroup lattice of
$G$. In this paper, we show that the set $\\{\frac{o(G)}{o(H)}\ |\
G\in\mathscr{N},H\in L(G)\\}$ is dense in $[0,\infty)$. Other density results
are outlined throughout the paper.

MSC (2010): Primary 20D15; Secondary 20D60, 40A05.

Key words: element orders, $p$-groups, nilpotent groups, density of a set

##  1 Introduction

Let $G$ be a finite group. In [5], A. Jaikin-Zapirain finds a super-
logarithmic lower bound for the number of conjugacy classes $k(G)$ of $G$,
when $G$ is nilpotent. More exactly, Theorem 1.1 of the same paper states that

$k(G)>10^{-4}\cdot\frac{\log_{2}\log_{2}n}{\log_{2}\log_{2}\log_{2}n}\cdot\log_{2}n,$

where $G$ is a nilpotent group of order $n\geq 5$. One of the tools which
plays a significant role in the proof of the above result is the so-called
average order of $G$, i.e. the quantity

$o(G)=\frac{1}{|G|}\sum\limits_{x\in G}|x|,$

where $|x|$ denotes the order of an element $x\in G$. Among others, the author
proves that $o(G)\geq o(Z(G))$, for any finite group $G$, and suggests that it
would be interesting to further investigate the relation between the average
order of $G$ and the average orders of its subgroups by answering the
following question:

Question 1.1. Let $G$ be a finite ($p$-)group and let $N$ be a normal
(abelian) subgroup of $G$. Is it true that $o(G)\geq o(N)^{\frac{1}{2}}?$

Question 1.1 remained unanswered for nearly a decade. During 2021, E.I.
Khukhro, A. Moretó and M. Zarrin published the paper [6] which provides a
negative answer to a generalized version of Jaikin-Zapirain’s question. More
exactly, Theorem 1.2 of [6] states that given a real number $c>0$ and a prime
number $p\geq\frac{3}{c}$, one can construct a $p$-group $G$ with a normal
abelian subgroup $N$ such that $o(G)<o(N)^{c}$. Hence, for $c=\frac{1}{2}$, it
is clear that there are counterexamples to Question 1.1. By following the
notations in [6], these counterexamples are constructed by taking $G$ to be a
semidirect product of a homocyclic group $U_{s}$ of exponent $p^{s}$, where
$s=p+1$, and a so-called secretive $p$-group $P$ (see [11] and Lemma 4.1 of
[6]), while $N$ is set to be $U_{s}$.

Let $\mathscr{F}$ be the class of all finite groups, let $\mathscr{N}$ be the
class of all finite nilpotent groups and let $L(G)$ be the subgroup lattice of
a finite group $G$. For a subset $A$ of $\mathbb{R}$, we denote by
$\overline{A}$ the closure of $A$ with respect to the usual topology
$\tau_{\mathbb{R}}$ of $\mathbb{R}$. If we work with a different topology, say
$\tau$, we denote the closure of $A$, with respect to $\tau$, by
$\overline{A}_{\tau}$.

This paper also aims to investigate the relation between $o(G)$ and $o(H)$,
where $H\in L(G)$, by studying the density of the set

$O_{\mathscr{C}}=\bigg{\\{}\frac{o(G)}{o(H)}\ \bigg{|}\ G\in\mathscr{C},H\in
L(G)\bigg{\\}}$

in $[0,\infty)$, where $\mathscr{C}$ is a specific class of finite groups. We
manage to show that $O_{\mathscr{F}}$ is dense in $[0,\infty)$ as a
consequence of our main result which is even stronger and states that:

Theorem 1.2. The set $O_{\mathscr{N}}$ is dense in $[0,\infty)$.

An immediate consequence of Theorem 1.2 is obtained as follows. Let
$\mathscr{C}$ be a class of finite groups such that
$\mathscr{N}\subseteq\mathscr{C}$. Then $O_{\mathscr{N}}\subseteq
O_{\mathscr{C}}\subseteq[0,\infty)$, so
$\overline{O_{\mathscr{N}}}\subseteq\overline{O_{\mathscr{C}}}\subseteq\overline{[0,\infty)}$.
Since $[0,\infty)$ is a closed set and
$\overline{O_{\mathscr{N}}}=[0,\infty)$, we get:

Corollary 1.3. Let $\mathscr{C}$ be a class of finite groups such that
$\mathscr{N}\subseteq\mathscr{C}$. Then $O_{\mathscr{C}}$ is dense in
$[0,\infty)$. In particular, $O_{\mathscr{F}}$ is dense in $[0,\infty)$.

We end the introduction by mentioning that the average order of a finite group
$G$ may be also expressed as

$o(G)=\frac{\psi(G)}{|G|},$

where $\psi(G)=\sum\limits_{x\in G}|x|$ is the sum of element orders of $G$.
During the last years, there was a growing interest in investigating this
invariant. We refer the reader to [4] for a recent survey including relevant
results concerning the sum of element orders of a finite group.

##  2 Proof of Theorem 1.2 and other results concerning the density of some
sets

As it was suggested in the first section, to obtain the density of
$O_{\mathscr{F}}$ in $[0,\infty)$, it would be sufficient to find a class of
groups $\mathscr{C}\subseteq\mathscr{F}$ such that
$\overline{O_{\mathscr{C}}}=[0,\infty)$. It is clear that
$\overline{O_{\mathscr{C}}}\subseteq[0,\infty)$. So, once we choose a
candidate for the class $\mathscr{C}$, it suffices to show that each
$a\in[0,\infty)$ is an adherent point of $O_{\mathscr{C}}$, i.e. there is a
sequence of groups $(G_{n})_{n\geq 1}\subset\mathscr{C}$ and a corresponding
sequence $(H_{n})_{n\geq 1}$, where $H_{n}\in L(G_{n})$, for all $n\geq 1$,
such that

$\displaystyle\lim_{n\to\infty}\frac{o(G_{n})}{o(H_{n})}=a.$

Our candidate for $\mathscr{C}$ is $\mathscr{N}$ and, in what follows, we
justify this option. To expand our reasoning, we include the following
preliminary result which is a consequence of the Proposition outlined on p.
863 of [7].

Lemma 2.1. Let $(x_{n})_{n\geq 1}$ be a sequence of positive real numbers such
that

$\displaystyle\lim_{n\to\infty}x_{n}=0\text{ \ and \
}\sum\limits_{n=1}^{\infty}x_{n}=\infty.$

Then the set containing the sums of all finite subsequences of $(x_{n})_{n\geq
1}$ is dense in $[0,\infty)$.

We denote the $n$th prime number by $p_{n}$. Lemma 2.1 is the main tool that
is going to be used to show that each $a\in[1,\infty)$ is an adherent point of
$O_{\mathscr{N}}$. Once this is done, it remains to cover the points
$a\in[0,1)$. For the first part, the main idea is to apply Lemma 2.1 for a
sequence $(x_{n})_{n\geq 1}$, where
$x_{n}=\ln\frac{o(\widetilde{G_{n}})}{o(\widetilde{H_{n}})}$. We are going to
show that some suitable candidates for $(\widetilde{G_{n}})_{n\geq 1}$ and
$(\widetilde{H_{n}})_{n\geq 1}$, such that the sequence $(x_{n})_{n\geq 1}$
defined above satisfies the hypotheses of Lemma 2.1, are
$\widetilde{G_{n}}=C_{p_{n}}^{m}$ and $\widetilde{H_{n}}=C_{p_{n}}^{m-1}$ for
a fixed integer $m\geq 2$ (see the proof of Claim 2.5 below). Consequently, by
applying Lemma 2.1 and some calculus properties, we deduce that there exists a
sequence $(G_{n})_{n\geq 1}$ of finite abelian groups and a corresponding
sequence of subgroups $(H_{n})_{n\geq 1}$ such that

$\displaystyle\lim_{n\to\infty}\frac{o(G_{n})}{o(H_{n})}=a\in[1,\infty).$

This means that $[1,\infty)\subseteq\overline{O_{\mathscr{A}}}$, where
$\mathscr{A}$ is the class of finite abelian groups. The reverse inclusion
also holds because $\frac{o(G)}{o(H)}\geq 1$ for any finite abelian group $G$
and any $H\in L(G)$. Indeed, since $G$ is self dual (see Chapter 8 of [9] or
[2]), we know that for any $H\in L(G)$, there is $K\in L(G)$ such that
$H\cong\frac{G}{K}$. Hence,

$\frac{o(G)}{o(H)}=\frac{o(G)}{o(\frac{G}{K})}=\frac{1}{|K|}\cdot\frac{\psi(G)}{\psi(\frac{G}{K})}=\frac{\sum\limits_{x\in
G}|x|}{\sum\limits_{x\in G}|xK|}\geq 1,$

so $O_{\mathscr{A}}\subseteq[1,\infty)$ and this leads to
$\overline{O_{\mathscr{A}}}\subseteq[1,\infty)$. Thus, we state the following
result.

Corollary 2.2. The set $O_{\mathscr{A}}$ is dense in $[1,\infty)$.

We mention that Corollary 2.2 also holds if we replace $\mathscr{A}$ with a
class $\widetilde{\mathscr{C}}$ of finite groups such that
$O_{\mathscr{A}}\subseteq O_{\widetilde{\mathscr{C}}}\subseteq[1,\infty)$.

Finally, concerning the adherence property of the points $a\in[0,1)$, we will
mainly work with sequences formed of specific direct products of finite
$p$-groups. Each such direct product has two main components: one is abelian,
while the other one is a counterexample to Question 1.1 (see the proof of
Claim 2.7 below). All finite groups that were highlighted in the last
paragraphs are nilpotent and this consequently explains why our choice for
$\mathscr{C}$ is $\mathscr{N}$.

The following preliminary result includes some number theoretic and calculus
properties which are going to be used further.

Lemma 2.3.

  * i)

Let $G_{1}$ and $G_{2}$ be finite groups. If $(|G_{1}|,|G_{2}|)=1$, then

$o(G_{1}\times G_{2})=o(G_{1})\cdot o(G_{2}).$

  * ii)

$\sum\limits_{n=1}^{\infty}\frac{1}{p_{n}}=\infty.$

  * iii)

Let $(x_{n})_{n\geq 1},(y_{n})_{n\geq 1}$ be sequences of positive real
numbers. If

$\displaystyle\lim_{n\to\infty}\frac{x_{n}}{y_{n}}\in(0,\infty),$

then the series $\sum\limits_{n=1}^{\infty}x_{n}$ and
$\sum\limits_{n=1}^{\infty}y_{n}$ have the same nature.

  * iv)

Let $(X,\tau)$ and $(Y,\tau^{\prime})$ be topological spaces, let
$f:X\longrightarrow Y$ be a continuous function and let $A,B\subseteq X$. If
$\overline{A}_{\tau}=\overline{B}_{\tau}$, then
$\overline{f(A)}_{\tau^{\prime}}=\overline{f(B)}_{\tau^{\prime}}$.

Concerning the previous lemma, we mention that item i) states that the average
order is a multiplicative function. This is a consequence of the
multiplicativity of the sum of element orders (see Lemma 2.1 of [1]). A short
proof of item ii) may be found in [8]. For item iii), one can check Theorem
10.9 of [3], while item iv) is easily obtained using the characterization of
the continuity of a function in terms of closure (see Proposition 6.12 of
[10]).

Let $I=[1,\infty)$. Denote by $\tau_{I}$ the subspace topology on $I$. For a
subset $A$ of $\mathbb{R}$, the closure of $A$ with respect to $\tau_{I}$ is
$\overline{A}_{\tau_{I}}=\overline{A}\cap I.$ By Corollary 2.2, we have
$\overline{O_{\mathscr{A}}}=I$. We deduce that

$\overline{O_{\mathscr{A}}}_{\tau_{I}}=\overline{I}_{\tau_{I}}.$ (1)

Since the function

$f:(I,\tau_{I})\longrightarrow(\mathbb{R},\tau_{\mathbb{R}}),\text{ \ given by
\ }f(x)=\frac{1}{x},\ \forall\ x\in I,$

is continuous, by Lemma 2.3, iv), and (1), we get

$\overline{\bigg{\\{}\frac{o(H)}{o(G)}\ \bigg{|}\ G\in\mathscr{A},H\in
L(G)\bigg{\\}}}=\overline{(0,1]}=[0,1].$

Therefore, one can state the following result.

Corollary 2.4. The set

$\bigg{\\{}\frac{o(H)}{o(G)}\ \bigg{|}\ G\in\mathscr{A},H\in L(G)\bigg{\\}}$

is dense in $[0,1]$.

We proceed now with the proof of the main result.

Proof of Theorem 1.2. Recall that $p_{n}$ denotes the $n$th prime number. We
are going to complete some preliminary steps towards achieving our goal.

Claim 2.5. Let $m\geq 2$ be an integer. The set

$\Bigg{\\{}\frac{o\big{(}{{\mathrel{\mathop{{\buildrel{}\over{\mbox{\Large$\times$}}}}\limits_{{n\in
I}}}{}\\!}{}\\!}C_{p_{n}}^{m}\big{)}}{o\big{(}{{\mathrel{\mathop{{\buildrel{}\over{\mbox{\Large$\times$}}}}\limits_{{n\in
I}}}{}\\!}{}\\!}C_{p_{n}}^{m-1}\big{)}}\ \Bigg{|}\
I\subset\mathbb{N}^{*},|I|<\infty\Bigg{\\}}$

is dense in $[1,\infty)$.

Proof. Consider the sequence $(x_{n})_{n\geq 1}$, where
$x_{n}=\ln\frac{o(C_{p_{n}}^{m})}{o(C_{p_{n}}^{m-1})}$, for all $n\geq 1$. We
have

$x_{n}=\ln\frac{p_{n}^{m+1}-p_{n}+1}{p_{n}^{m+1}-p_{n}^{m}+p_{n}^{m-1}}\in(0,\infty).$

As $n$ approaches infinity, we get

$\displaystyle\lim_{n\to\infty}x_{n}=\ln 1=0.$ (2)

Further, take the sequence $(y_{n})_{n\geq 1}$ given by
$y_{n}=\frac{1}{p_{n}}$, for all $n\geq 1$. Then

$\displaystyle\lim_{n\to\infty}\frac{x_{n}}{y_{n}}=\displaystyle\lim_{n\to\infty}\bigg{(}p_{n}\cdot\ln\frac{p_{n}^{m+1}-p_{n}+1}{p_{n}^{m+1}-p_{n}^{m}+p_{n}^{m-1}}\bigg{)}=1\in(0,\infty).$

By Lemma 2.3, ii), iii), we have

$\sum\limits_{n=1}^{\infty}x_{n}=\infty.$ (3)

According to (2) and (3), the sequence $(x_{n})_{n\geq 1}$ satisfies the
hypotheses of Lemma 2.1. Hence, we have

$\overline{\bigg{\\{}\sum\limits_{n\in I}x_{n}\ \bigg{|}\
I\subset\mathbb{N}^{*},|I|<\infty\bigg{\\}}}=[0,\infty)\Longleftrightarrow\overline{\bigg{\\{}\ln\bigg{(}\prod_{n\in
I}\frac{o(C_{p_{n}}^{m})}{o(C_{p_{n}}^{m-1})}\bigg{)}\ \bigg{|}\
I\subset\mathbb{N}^{*},|I|<\infty\bigg{\\}}}=[0,\infty).$ (4)

Since, by Lemma 2.3, i), the average order is a multiplicative function, (4)
becomes

$\overline{\Bigg{\\{}\ln\frac{o\big{(}{{\mathrel{\mathop{{\buildrel{}\over{\mbox{\Large$\times$}}}}\limits_{{n\in
I}}}{}\\!}{}\\!}C_{p_{n}}^{m}\big{)}}{o\big{(}{{\mathrel{\mathop{{\buildrel{}\over{\mbox{\Large$\times$}}}}\limits_{{n\in
I}}}{}\\!}{}\\!}C_{p_{n}}^{m-1}\big{)}}\ \Bigg{|}\
I\subset\mathbb{N}^{*},|I|<\infty\Bigg{\\}}}=[0,\infty).$ (5)

Finally, since

$exp:(\mathbb{R},\tau_{\mathbb{R}})\longrightarrow(\mathbb{R},\tau_{\mathbb{R}}),\text{
\ given by \ }exp(x)=e^{x},\forall\ x\in\mathbb{R},$

is continuous and (5) highlights the equality of two closed sets of
$(\mathbb{R},\tau_{\mathbb{R}})$, we apply Lemma 2.3, iv), to finish the proof
of our claim, i.e.

$\overline{\Bigg{\\{}\frac{o\big{(}{{\mathrel{\mathop{{\buildrel{}\over{\mbox{\Large$\times$}}}}\limits_{{n\in
I}}}{}\\!}{}\\!}C_{p_{n}}^{m}\big{)}}{o\big{(}{{\mathrel{\mathop{{\buildrel{}\over{\mbox{\Large$\times$}}}}\limits_{{n\in
I}}}{}\\!}{}\\!}C_{p_{n}}^{m-1}\big{)}}\ \Bigg{|}\
I\subset\mathbb{N}^{*},|I|<\infty\Bigg{\\}}}=[1,\infty).$

Claim 2.6. Let $m\geq 2$ and let $J$ be a finite non-empty subset of
$\mathbb{N}^{*}$. The set

$\Bigg{\\{}\frac{o\big{(}{{\mathrel{\mathop{{\buildrel{}\over{\mbox{\Large$\times$}}}}\limits_{{n\in
I}}}{}\\!}{}\\!}C_{p_{n}}^{m}\big{)}}{o\big{(}{{\mathrel{\mathop{{\buildrel{}\over{\mbox{\Large$\times$}}}}\limits_{{n\in
I}}}{}\\!}{}\\!}C_{p_{n}}^{m-1}\big{)}}\ \Bigg{|}\
I\subset\mathbb{N}^{*}\setminus J,|I|<\infty\Bigg{\\}}$

is dense in $[1,\infty)$.

Proof. This is obtained by repeating the proof of Claim 2.5 for the sequence
$(\widetilde{x_{n}})_{n\in\mathbb{N}^{*}\setminus J}$, where
$\widetilde{x_{n}}=\ln\frac{o(C_{p_{n}}^{m})}{o(C_{p_{n}}^{m-1})}$, for all
$n\in\mathbb{N}^{*}\setminus J$. The same reasoning can be repeated since
$(\widetilde{x_{n}})_{n\in\mathbb{N}^{*}\setminus J}$ is obtained by removing
a finite number of terms from the original sequence $(x_{n})_{n\geq 1}$ taken
in the proof of Claim 2.5, so
$(\widetilde{x_{n}})_{n\in\mathbb{N}^{*}\setminus J}$ also satisfies the
hypotheses of Lemma 2.1.

Claim 2.7. Any $a\in[0,1)$ is an adherent point of $O_{\mathscr{N}}$.

Proof. Suppose that $a=0$. As we outlined in the first section, for $n\geq 4$
(i.e. for a prime greater than or equal to 7), if we take
$G_{n}=U_{s_{n}}P_{n}$ to be a semidirect product of a homocyclic group
$U_{s_{n}}$ of exponent $p_{n}^{s_{n}}$, where $s_{n}=p_{n}+1$, and a
secretive $p_{n}$-group $P_{n}$, one has $o(G)<o(U_{s_{n}})^{\frac{1}{2}}$.
According to the proof of Theorem 1.2 of [6], the following inequalities hold:

$o(G_{n})<p_{n}^{3}\text{ \ and \ }o(U_{s_{n}})\geq p_{n}^{p_{n}},\ \forall\
n\geq 4.$

Hence,

$\frac{o(G_{n})}{o(U_{s_{n}})}<\frac{p_{n}^{3}}{p_{n}^{p_{n}}}.$ (6)

As $n$ approaches infinity, (6) leads us to

$\displaystyle\lim_{n\to\infty}\frac{o(G_{n})}{o(U_{s_{n}})}=0,$ (7)

so $a=0$ is an adherent point of $O_{\mathscr{N}}$.

Let $a\in(0,1)$. By (7), there is a sufficiently large $N$ such that
$a\geq\frac{o(G_{N})}{o(U_{s_{N}})}$. Consequently,
$a\cdot\frac{o(U_{s_{N}})}{o(G_{N})}\in[1,\infty)$. If we take $J=\\{N\\}$ in
Claim 2.6, it follows that there is a sequence of finite abelian groups
$(\widetilde{G_{n}})_{n\geq 1}$ and a corresponding sequence
$(\widetilde{H_{n}})_{n\geq 1}$, where $\widetilde{H_{n}}\in
L(\widetilde{G_{n}})$ for all $n\geq 1$, such that

$\displaystyle\lim_{n\to\infty}\frac{o(\widetilde{G_{n}})}{o(\widetilde{H_{n}})}=a\cdot\frac{o(U_{s_{N}})}{o(G_{N})}.$
(8)

Finally, we consider the sequences $(G_{N}\times\widetilde{G_{n}})_{n\geq 1}$
and $(U_{s_{N}}\times\widetilde{H_{n}})_{n\geq 1}$. Note that
$(|G_{N}|,|\widetilde{G_{n}}|)=(|U_{s_{N}}|,|\widetilde{H_{n}}|)=1$, for all
$n\geq 1$. Hence, by Lemma 2.3, i), and (8), we conclude that

$\displaystyle\lim_{n\to\infty}\frac{o(G_{N}\times\widetilde{G_{n}})}{o(U_{s_{N}}\times\widetilde{H_{n}})}=\frac{o(G_{N})}{o(U_{s_{N}})}\cdot\displaystyle\lim_{n\to\infty}\frac{o(\widetilde{G_{n}})}{o(\widetilde{H_{n}})}=a.$

Hence, any $a\in(0,1)$ is also an adherent point of $O_{\mathscr{N}}$ and this
concludes the proof of our claim.

By Claims 2.5 and 2.7, it follows that
$[0,\infty)\subseteq\overline{O_{\mathscr{N}}}$. Since the reverse inclusion
also holds, the proof of Theorem 1.2 is complete.

We end our paper by posing a question concerning the class $\mathscr{P}$ of
finite $p$-groups. If the answer would be affirmative, our main result would
also follow since $\mathscr{P}\subset\mathscr{N}$.

Question 2.8. Is the set $O_{\mathscr{P}}$ dense in $[0,\infty)$?

Acknowledgements. The author is grateful to the reviewers for their remarks
which improve the previous version of the paper. This work was supported by a
grant of the ”Alexandru Ioan Cuza” University of Iasi, within the Research
Grants program, Grant UAIC, code GI-UAIC-2021-01.

## References

  * [1] H. Amiri, S.M. Jafarian Amiri, Sum of element orders on finite groups of the same order, J. Algebra Appl. 10 (2) (2011), 187-190.
  * [2] L. An, J. Ding, Q. Zhang, Finite self dual groups, J. Algebra 341 (1) (2011), 35-44.
  * [3] T.M. Apostol, Calculus. Vol. I: One-variable calculus, with an introduction to linear algebra, 2nd edition, John Wiley & Sons, Inc., New York, 1967.
  * [4] M. Herzog, P. Longobardi, M. Maj, New criteria for solvability, nilpotency and other properties of finite groups in terms of the order elements or subgroups, Int. J. Group Theory 12 (1) (2023), 35-44.
  * [5] A. Jaikin-Zapirain, On the number of conjugacy classes of finite nilpotent groups, Adv. Math. 227 (2011), 1129-1143.
  * [6] E.I. Khukhro, A. Moretó, M. Zarrin, The average element order and the number of conjugacy classes of finite groups, J. Algebra 569 (2021), 1-11.
  * [7] Z. Nitecki, Cantorvals and subsum sets of null sequences, Amer. Math. Monthly 122 (2015), 862-870.
  * [8] I. Niven, A Proof of the Divergence $\sum 1/p$, Amer. Math. Monthly 78 (1971), 272-273.
  * [9] R. Schmidt, Subgroup lattices of groups, de Gruyter Expositions in Mathematics 14, de Gruyter, Berlin, 1994.
  * [10] W.A. Sutherland, Introduction to Metric and Topological Spaces, 2nd edition, Oxford University Press, 2009.
  * [11] G.E. Wall, Secretive prime-power groups of large rank, Bull. Aust. Math. Soc. 12 (1975), 363-369.

Mihai-Silviu Lazorec

Faculty of Mathematics

”Al.I. Cuza” University

Iaşi, Romania

e-mail<EMAIL_ADDRESS>